[ASL+AArch64] Allow access to UDF under variant

herd/AArch64ASLSem.ml

@@ -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 ->
+          Some ("udf/UDF_only_perm_undef.opn", stmt [ "imm16" ^= litbv 16 k ])
       | i ->
           let () =
             if _dbg then

herd/variant.ml

@@ -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 *)
@@ -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
@@ -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
@@ -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"
@@ -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]

herd/variant.mli

@@ -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 *)