Update aarch64_small to build with new barriers

Make sure barrier changes don't affect other models for now

4 files changed, 84 insertions, 57 deletions

diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail
index be4a2cba..884a9e81 100644
--- a/aarch64_small/aarch64_regfp.sail
+++ b/aarch64_small/aarch64_regfp.sail
@@ -183,7 +183,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
     (GenerateExceptionEL1(imm))  => not_implemented("GenerateExceptionEL1"),
     (GenerateExceptionEL2(imm))  => not_implemented("GenerateExceptionEL2"),
     (GenerateExceptionEL3(imm))  => not_implemented("GenerateExceptionEL3"),
-    (DebugBreakpoint(comment))  => not_implemented("DebugBreakpoint"),
+    (DebugBreakpoint(comment))   => not_implemented("DebugBreakpoint"),
     (ExternalDebugBreakpoint())  => not_implemented("ExternalDebugBreakpoint"),
     (DebugSwitchToExceptionLevel(target_level))  => not_implemented("DebugSwitchToExceptionLevel"),
     (MoveSystemImmediate(operand,field))  =>
@@ -223,23 +223,23 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
       },
     (ClearExclusiveMonitor(imm))  => (), /*ClearExclusiveLocal*/
     (Barrier(op,domain,types))  => {
-      let (dom, typ) =
+      let (dom, typ) : (a64_barrier_domain, a64_barrier_type) =
         (match domain {
-          MBReqDomain_Nonshareable   => A64_NonShare
-          MBReqDomain_InnerShareable => A64_InnerShare
-          MBReqDomain_OuterShareable => A64_OuterShare
+	  MBReqDomain_Nonshareable   => A64_NonShare,
+	  MBReqDomain_InnerShareable => A64_InnerShare,
+	  MBReqDomain_OuterShareable => A64_OuterShare,
           MBReqDomain_FullSystem     => A64_FullShare
         },
         match types {
-          MBReqTypes_Reads  => A64_barrier_LD
-          MBReqTypes_Writes => A64_barrier_ST
+	  MBReqTypes_Reads  => A64_barrier_LD,
+	  MBReqTypes_Writes => A64_barrier_ST,
           MBReqTypes_All    => A64_barrier_all
         })
       in {
       ik = match op {
-        MemBarrierOp_DSB => IK_barrier(Barrier_DSB (dom, typ))
-        MemBarrierOp_DMB => IK_barrier(Barrier_DMB (dom, typ))
-        MemBarrierOp_ISB => IK_barrier(Barrier_ISB)
+	MemBarrierOp_DSB => IK_barrier(Barrier_DSB(dom, typ)),
+	MemBarrierOp_DMB => IK_barrier(Barrier_DMB(dom, typ)),
+	MemBarrierOp_ISB => IK_barrier(Barrier_ISB())
       };
       }
     },
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index d3d82c6d..66f05086 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -576,37 +576,37 @@ function BigEndianReverse (value) = {
 /* external */ val DataMemoryBarrier_FullShWrites  : unit -> unit effect {barr}
 /* external */ val DataMemoryBarrier_FullShAll     : unit -> unit effect {barr}
 
-function DataMemoryBarrier_NonShReads    = __barrier(Barrier_DMB (A64_NonShare,   A64_barrier_LD))
-function DataMemoryBarrier_NonShWrites   = __barrier(Barrier_DMB (A64_NonShare,   A64_barrier_ST))
-function DataMemoryBarrier_NonShAll      = __barrier(Barrier_DMB (A64_NonShare,   A64_barrier_all))
-function DataMemoryBarrier_InnerShReads  = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_LD))
-function DataMemoryBarrier_InnerShWrites = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_ST))
-function DataMemoryBarrier_InnerShAll    = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_all))
-function DataMemoryBarrier_OuterShReads  = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_LD))
-function DataMemoryBarrier_OuterShWrites = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_ST))
-function DataMemoryBarrier_OuterShAll    = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_all))
-function DataMemoryBarrier_FullShReads   = __barrier(Barrier_DMB (A64_FullShare,  A64_barrier_LD))
-function DataMemoryBarrier_FullShWrites  = __barrier(Barrier_DMB (A64_FullShare,  A64_barrier_ST))
-function DataMemoryBarrier_FullShAll     = __barrier(Barrier_DMB (A64_FullShare,  A64_barrier_all))
+function DataMemoryBarrier_NonShReads()    = __barrier(Barrier_DMB (A64_NonShare,   A64_barrier_LD))
+function DataMemoryBarrier_NonShWrites()   = __barrier(Barrier_DMB (A64_NonShare,   A64_barrier_ST))
+function DataMemoryBarrier_NonShAll()      = __barrier(Barrier_DMB (A64_NonShare,   A64_barrier_all))
+function DataMemoryBarrier_InnerShReads()  = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_LD))
+function DataMemoryBarrier_InnerShWrites() = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_ST))
+function DataMemoryBarrier_InnerShAll()    = __barrier(Barrier_DMB (A64_InnerShare, A64_barrier_all))
+function DataMemoryBarrier_OuterShReads()  = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_LD))
+function DataMemoryBarrier_OuterShWrites() = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_ST))
+function DataMemoryBarrier_OuterShAll()    = __barrier(Barrier_DMB (A64_OuterShare, A64_barrier_all))
+function DataMemoryBarrier_FullShReads()   = __barrier(Barrier_DMB (A64_FullShare,  A64_barrier_LD))
+function DataMemoryBarrier_FullShWrites()  = __barrier(Barrier_DMB (A64_FullShare,  A64_barrier_ST))
+function DataMemoryBarrier_FullShAll()     = __barrier(Barrier_DMB (A64_FullShare,  A64_barrier_all))
 
 val DataMemoryBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr, escape}
 function DataMemoryBarrier(domain, types) =
 {
   match (domain, types) {
-    (MBReqDomain_Nonshareable, MBReqTypes_Reads)  => DataMemoryBarrier_NonShReads()
-    (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataMemoryBarrier_NonShWrites()
-    (MBReqDomain_Nonshareable, MBReqTypes_All)    => DataMemoryBarrier_NonShAll()
+    (MBReqDomain_Nonshareable, MBReqTypes_Reads)  => DataMemoryBarrier_NonShReads(),
+    (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataMemoryBarrier_NonShWrites(),
+    (MBReqDomain_Nonshareable, MBReqTypes_All)    => DataMemoryBarrier_NonShAll(),
 
-    (MBReqDomain_InnerShareable, MBReqTypes_Reads)  => DataMemoryBarrier_InnerShReads()
-    (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataMemoryBarrier_InnerShWrites()
-    (MBReqDomain_InnerShareable, MBReqTypes_All)    => DataMemoryBarrier_InnerShAll()
+    (MBReqDomain_InnerShareable, MBReqTypes_Reads)  => DataMemoryBarrier_InnerShReads(),
+    (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataMemoryBarrier_InnerShWrites(),
+    (MBReqDomain_InnerShareable, MBReqTypes_All)    => DataMemoryBarrier_InnerShAll(),
 
-    (MBReqDomain_OuterShareable, MBReqTypes_Reads)  => DataMemoryBarrier_OuterShReads()
-    (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataMemoryBarrier_OuterShWrites()
-    (MBReqDomain_OuterShareable, MBReqTypes_All)    => DataMemoryBarrier_OuterShAll()
+    (MBReqDomain_OuterShareable, MBReqTypes_Reads)  => DataMemoryBarrier_OuterShReads(),
+    (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataMemoryBarrier_OuterShWrites(),
+    (MBReqDomain_OuterShareable, MBReqTypes_All)    => DataMemoryBarrier_OuterShAll(),
 
-    (MBReqDomain_FullSystem, MBReqTypes_Reads)  => DataMemoryBarrier_FullShReads()
-    (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataMemoryBarrier_FullShWrites()
+    (MBReqDomain_FullSystem, MBReqTypes_Reads)  => DataMemoryBarrier_FullShReads(),
+    (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataMemoryBarrier_FullShWrites(),
     (MBReqDomain_FullSystem, MBReqTypes_All)    => DataMemoryBarrier_FullShAll()
   };
 }
@@ -626,37 +626,37 @@ function DataMemoryBarrier(domain, types) =
 /* external */ val DataSynchronizationBarrier_FullShWrites  : unit -> unit effect {barr}
 /* external */ val DataSynchronizationBarrier_FullShAll     : unit -> unit effect {barr}
 
-function DataSynchronizationBarrier_NonShReads    = __barrier(Barrier_DSB (A64_NonShare,   A64_barrier_LD))
-function DataSynchronizationBarrier_NonShWrites   = __barrier(Barrier_DSB (A64_NonShare,   A64_barrier_ST))
-function DataSynchronizationBarrier_NonShAll      = __barrier(Barrier_DSB (A64_NonShare,   A64_barrier_all))
-function DataSynchronizationBarrier_InnerShReads  = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_LD))
-function DataSynchronizationBarrier_InnerShWrites = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_ST))
-function DataSynchronizationBarrier_InnerShAll    = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_all))
-function DataSynchronizationBarrier_OuterShReads  = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_LD))
-function DataSynchronizationBarrier_OuterShWrites = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_ST))
-function DataSynchronizationBarrier_OuterShAll    = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_all))
-function DataSynchronizationBarrier_FullShReads   = __barrier(Barrier_DSB (A64_FullShare,  A64_barrier_LD))
-function DataSynchronizationBarrier_FullShWrites  = __barrier(Barrier_DSB (A64_FullShare,  A64_barrier_ST))
-function DataSynchronizationBarrier_FullShAll     = __barrier(Barrier_DSB (A64_FullShare,  A64_barrier_all))
+function DataSynchronizationBarrier_NonShReads()    = __barrier(Barrier_DSB (A64_NonShare,   A64_barrier_LD))
+function DataSynchronizationBarrier_NonShWrites()   = __barrier(Barrier_DSB (A64_NonShare,   A64_barrier_ST))
+function DataSynchronizationBarrier_NonShAll()      = __barrier(Barrier_DSB (A64_NonShare,   A64_barrier_all))
+function DataSynchronizationBarrier_InnerShReads()  = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_LD))
+function DataSynchronizationBarrier_InnerShWrites() = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_ST))
+function DataSynchronizationBarrier_InnerShAll()    = __barrier(Barrier_DSB (A64_InnerShare, A64_barrier_all))
+function DataSynchronizationBarrier_OuterShReads()  = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_LD))
+function DataSynchronizationBarrier_OuterShWrites() = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_ST))
+function DataSynchronizationBarrier_OuterShAll()    = __barrier(Barrier_DSB (A64_OuterShare, A64_barrier_all))
+function DataSynchronizationBarrier_FullShReads()   = __barrier(Barrier_DSB (A64_FullShare,  A64_barrier_LD))
+function DataSynchronizationBarrier_FullShWrites()  = __barrier(Barrier_DSB (A64_FullShare,  A64_barrier_ST))
+function DataSynchronizationBarrier_FullShAll()     = __barrier(Barrier_DSB (A64_FullShare,  A64_barrier_all))
 
 val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit effect {barr,escape}
 function DataSynchronizationBarrier(domain, types) =
 {
   match (domain, types) {
-    (MBReqDomain_Nonshareable, MBReqTypes_Reads)  => DataSynchronizationBarrier_NonShReads()
-    (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataSynchronizationBarrier_NonShWrites()
-    (MBReqDomain_Nonshareable, MBReqTypes_All)    => DataSynchronizationBarrier_NonShAll()
+    (MBReqDomain_Nonshareable, MBReqTypes_Reads)  => DataSynchronizationBarrier_NonShReads(),
+    (MBReqDomain_Nonshareable, MBReqTypes_Writes) => DataSynchronizationBarrier_NonShWrites(),
+    (MBReqDomain_Nonshareable, MBReqTypes_All)    => DataSynchronizationBarrier_NonShAll(),
 
-    (MBReqDomain_InnerShareable, MBReqTypes_Reads)  => DataSynchronizationBarrier_InnerShReads()
-    (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_InnerShWrites()
-    (MBReqDomain_InnerShareable, MBReqTypes_All)    => DataSynchronizationBarrier_InnerShAll()
+    (MBReqDomain_InnerShareable, MBReqTypes_Reads)  => DataSynchronizationBarrier_InnerShReads(),
+    (MBReqDomain_InnerShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_InnerShWrites(),
+    (MBReqDomain_InnerShareable, MBReqTypes_All)    => DataSynchronizationBarrier_InnerShAll(),
 
-    (MBReqDomain_OuterShareable, MBReqTypes_Reads)  => DataSynchronizationBarrier_OuterShReads()
-    (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_OuterShWrites()
-    (MBReqDomain_OuterShareable, MBReqTypes_All)    => DataSynchronizationBarrier_OuterShAll()
+    (MBReqDomain_OuterShareable, MBReqTypes_Reads)  => DataSynchronizationBarrier_OuterShReads(),
+    (MBReqDomain_OuterShareable, MBReqTypes_Writes) => DataSynchronizationBarrier_OuterShWrites(),
+    (MBReqDomain_OuterShareable, MBReqTypes_All)    => DataSynchronizationBarrier_OuterShAll(),
 
-    (MBReqDomain_FullSystem, MBReqTypes_Reads)  => DataSynchronizationBarrier_FullShReads()
-    (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataSynchronizationBarrier_FullShWrites()
+    (MBReqDomain_FullSystem, MBReqTypes_Reads)  => DataSynchronizationBarrier_FullShReads(),
+    (MBReqDomain_FullSystem, MBReqTypes_Writes) => DataSynchronizationBarrier_FullShWrites(),
     (MBReqDomain_FullSystem, MBReqTypes_All)    => DataSynchronizationBarrier_FullShAll()
   };
 }
@@ -1038,7 +1038,7 @@ function Hint_Yield() -> unit = ()
 
 /** FUNCTION:shared/functions/system/InstructionSynchronizationBarrier */
 /* external */ val InstructionSynchronizationBarrier : unit -> unit effect {barr}
-function InstructionSynchronizationBarrier () = __barrier(Barrier_ISB)
+function InstructionSynchronizationBarrier () = __barrier(Barrier_ISB())
 /** FUNCTION:shared/functions/system/InterruptPending */
 
 function InterruptPending () -> boolean = not_implemented_extern("InterruptPending")
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index d94112ad..b938d7bb 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -20,6 +20,8 @@ $include <flow.sail>
 $include <arith.sail>
 $include <option.sail>
 $include <vector_dec.sail>
+
+$define AARCH64_SMALL
 $include <regfp.sail>
 
 infix 7 >>
diff --git a/lib/regfp.sail b/lib/regfp.sail
index 070ff524..e9c85ba8 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -73,6 +73,7 @@ enum a64_barrier_type = {
   A64_barrier_ST
 }
 
+$ifdef AARCH64_SMALL
 union barrier_kind = {
   Barrier_Sync : unit,
   Barrier_LwSync : unit,
@@ -95,6 +96,30 @@ union barrier_kind = {
   Barrier_RISCV_i : unit,
   Barrier_x86_MFENCE : unit
 }
+$else
+enum barrier_kind = {
+  Barrier_Sync,
+  Barrier_LwSync,
+  Barrier_Eieio,
+  Barrier_Isync,
+  Barrier_DMB,
+  Barrier_DSB,
+  Barrier_ISB,
+  Barrier_MIPS_SYNC,
+  Barrier_RISCV_rw_rw,
+  Barrier_RISCV_r_rw,
+  Barrier_RISCV_r_r,
+  Barrier_RISCV_rw_w,
+  Barrier_RISCV_w_w,
+  Barrier_RISCV_w_rw,
+  Barrier_RISCV_rw_r,
+  Barrier_RISCV_r_w,
+  Barrier_RISCV_w_r,
+  Barrier_RISCV_tso,
+  Barrier_RISCV_i,
+  Barrier_x86_MFENCE
+}
+$endif
 
 enum trans_kind = {
   Transaction_start,