From 4e158bb21274ba05fa1a30f7517967e165f28001 Mon Sep 17 00:00:00 2001
From: Hadrien Renaud <hadrien.renaud2@arm.com>
Date: Thu, 10 Oct 2024 15:51:55 +0100
Subject: [PATCH] [ASL+AArch64] Allow access to UDF under variant

---
 herd/AArch64ASLSem.ml | 2 ++
 herd/variant.ml       | 7 ++++++-
 herd/variant.mli      | 2 ++
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml
index 2b00ab1c5..e05315728 100644
--- a/herd/AArch64ASLSem.ml
+++ b/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
diff --git a/herd/variant.ml b/herd/variant.ml
index 737667be3..722fd8a01 100644
--- a/herd/variant.ml
+++ b/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]
diff --git a/herd/variant.mli b/herd/variant.mli
index 8ab36c19b..f4e56f91c 100644
--- a/herd/variant.mli
+++ b/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 *)