Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ASL+AArch64] Allow access to UDF under variant #1001

Merged
merged 1 commit into from
Oct 15, 2024
Merged

[ASL+AArch64] Allow access to UDF under variant #1001

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions herd/AArch64ASLSem.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -730,6 +730,8 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
"domain" ^= var (barrier_domain dom);
"types" ^= var (barrier_typ btyp);
] )
| I_UDF k when C.variant Variant.ASL_AArch64_UDF ->
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Out of curiosity, can't unconditionally handle UDF with that ASL code? Because if that's the case you don't really need the variant either, do you?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well the problem is that I'm really not able to match the behaviour of herd without the variant ASL:

In herd/AArch64Sem.ml:

        | I_UDF _ ->
           let (>>!) = M.(>>!) in
           let ft = Some FaultType.AArch64.UndefinedInstruction in
           let m_fault = mk_fault None Dir.R Annot.N ii ft None in
           let lbl_v = get_instr_label ii in
           m_fault >>| set_elr_el1 lbl_v ii >>! B.Fault [AArch64Base.elr_el1, lbl_v]

In the Arm ARM downloaded by herd (a bit out of date):

// Execute
// =======

// No operation.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah yes, I think this something that happens in decode.

Some ("udf/UDF_only_perm_undef.opn", stmt [ "imm16" ^= litbv 16 k ])
| i ->
let () =
if _dbg then
Expand Down
7 changes: 6 additions & 1 deletion herd/variant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,8 @@ type t =
| ASLType of [`Warn|`Silence|`TypeCheck]
(* Activate ASL experimental mode *)
| ASLExperimental
(* UDF control in AArch64 mode *)
| ASL_AArch64_UDF
(* Signed Int128 types *)
| S128
(* Strict interpretation of variant, e.g. -variant asl,strict *)
Expand All @@ -119,7 +121,7 @@ let tags =
"pte-squared"; "PhantomOnLoad"; "OptRfRMW"; "ConstrainedUnpredictable";
"exp"; "self"; "cos-opt"; "test"; "T[0-9][0-9]"; "asl"; "strict";
"warn"; "S128"; "ASLType+Warn"; "ASLType+Silence"; "ASLType+Check";
"ASL+Experimental"; "telechat"; "OldSolver"; "oota";]
"ASL+Experimental"; "ASL+AArch64+UDF"; "telechat"; "OldSolver"; "oota";]

let parse s = match Misc.lowercase s with
| "success" -> Some Success
Expand Down Expand Up @@ -173,6 +175,7 @@ let parse s = match Misc.lowercase s with
| "asltype+silence"-> Some (ASLType `Silence)
| "asltype+check" -> Some (ASLType `TypeCheck)
| "asl+experimental"|"asl+exp" -> Some ASLExperimental
| "asl+aarch64+udf" -> Some ASL_AArch64_UDF
| "s128" -> Some S128
| "strict" -> Some Strict
| "warn" -> Some Warn
Expand Down Expand Up @@ -276,6 +279,7 @@ let pp = function
| ASLType `Silence -> "ASLType+Silence"
| ASLType `TypeCheck -> "ASLType+Check"
| ASLExperimental -> "ASL+Experimental"
| ASL_AArch64_UDF -> "ASL+AArch64+UDF"
| Telechat -> "telechat"
| NV2 -> "NV2"
| OldSolver -> "OldSolver"
Expand Down Expand Up @@ -332,4 +336,5 @@ let set_sme_length r = function

let check_tag = function
| ASLExperimental -> [ASL;ASLExperimental;]
| ASL_AArch64_UDF -> [ASL;ASL_AArch64_UDF;]
| tag -> [tag]
2 changes: 2 additions & 0 deletions herd/variant.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,8 @@ type t =
| ASLType of [`Warn|`Silence|`TypeCheck]
(* Activate ASL experimental mode *)
| ASLExperimental
(* UDF control in ASL+AArch64 mode *)
| ASL_AArch64_UDF
(* Signed Int128 types *)
| S128
(* Strict interpretation of variant, e.g. -variant asl,strict *)
Expand Down