Support DMB/DSB domains

2 files changed, 109 insertions, 129 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 74e43a8f..3413494e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -579,74 +579,13 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ ->
             NIA_indirect_address
          | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
-       let readk_to_readk = function
-                         | "Read_plain" ->             Read_plain
-                         | "Read_reserve" ->           Read_reserve
-                         | "Read_acquire" ->           Read_acquire
-                         | "Read_exclusive" ->         Read_exclusive
-                         | "Read_exclusive_acquire" -> Read_exclusive_acquire
-                         | "Read_stream" ->            Read_stream 
-                         | "Read_RISCV_acquire"                  -> Read_RISCV_acquire
-                         | "Read_RISCV_strong_acquire"           -> Read_RISCV_strong_acquire
-                         | "Read_RISCV_reserved"                 -> Read_RISCV_reserved
-                         | "Read_RISCV_reserved_acquire"         -> Read_RISCV_reserved_acquire
-                         | "Read_RISCV_reserved_strong_acquire"  -> Read_RISCV_reserved_strong_acquire
-                         | "Read_X86_locked"                     -> Read_X86_locked
-                         | r -> failwith ("unknown read kind: " ^ r) end in
-       let writek_to_writek = function
-                         | "Write_plain" ->             Write_plain
-                         | "Write_conditional" ->       Write_conditional
-                         | "Write_release" ->           Write_release
-                         | "Write_exclusive" ->         Write_exclusive
-                         | "Write_exclusive_release" -> Write_exclusive_release 
-                         | "Write_RISCV_release"                    -> Write_RISCV_release
-                         | "Write_RISCV_strong_release"             -> Write_RISCV_strong_release
-                         | "Write_RISCV_conditional"                -> Write_RISCV_conditional
-                         | "Write_RISCV_conditional_release"        -> Write_RISCV_conditional_release
-                         | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release
-                         | "Write_X86_locked"                       -> Write_X86_locked
-                         | w -> failwith ("unknown write kind: " ^ w) end in
-       let ik_to_ik = function
-         | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _
-           (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) ->
-            IK_barrier (match b with
-                        | "Barrier_Sync" ->   Barrier_Sync
-                        | "Barrier_LwSync" -> Barrier_LwSync
-                        | "Barrier_Eieio" ->  Barrier_Eieio
-                        | "Barrier_Isync" ->  Barrier_Isync
-                        | "Barrier_DMB" ->    Barrier_DMB
-                        | "Barrier_DMB_ST" -> Barrier_DMB_ST
-                        | "Barrier_DMB_LD" -> Barrier_DMB_LD
-                        | "Barrier_DSB" ->    Barrier_DSB
-                        | "Barrier_DSB_ST" -> Barrier_DSB_ST
-                        | "Barrier_DSB_LD" -> Barrier_DSB_LD
-                        | "Barrier_ISB" ->    Barrier_ISB
-                        | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC
-                        | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE
-                        end)
-         | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _
-           (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) ->
-            IK_mem_read(readk_to_readk r)
-         | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _
-           (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) ->
-            IK_mem_write(writek_to_writek w)
-         | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _
-           (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ;
-                                (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) ->
-            IK_mem_rmw(readk_to_readk readk, writek_to_writek writek)
-         | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ ->
-            IK_branch
-         | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
-            IK_simple
-         | _ -> failwith "Analysis returned unexpected instruction kind"
-       end in
        let (regs1,regs2,regs3,nias,dia,ik) =
          (List.map reg_to_reg_name regs1,
           List.map reg_to_reg_name regs2,
           List.map reg_to_reg_name regs3,
           List.map nia_to_nia nias,
           dia_to_dia dia,
-          ik_to_ik ik) in
+          fromInterpValue ik) in
        ((regs1,regs2,regs3,nias,dia,ik), events)
      | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end)
   | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed"
diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index bd3a3eb7..f3cdfbc9 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -136,58 +136,86 @@ instance (Show write_kind)
   end
 end
 
+type a64_barrier_domain =
+  A64_FullShare
+  | A64_InnerShare
+  | A64_OuterShare
+  | A64_NonShare
+
+type a64_barrier_type =
+  A64_barrier_all
+  | A64_barrier_LD
+  | A64_barrier_ST
+
 type barrier_kind =
   (* Power barriers *)
-  Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
+  Barrier_Sync of unit | Barrier_LwSync of unit | Barrier_Eieio of unit | Barrier_Isync of unit
   (* AArch64 barriers *)
-  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
-  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
-  | Barrier_TM_COMMIT
+  | Barrier_DMB of (a64_barrier_domain * a64_barrier_type)
+  | Barrier_DSB of (a64_barrier_domain * a64_barrier_type)
+  | Barrier_ISB of unit
+  | Barrier_TM_COMMIT of unit
   (* MIPS barriers *)
-  | Barrier_MIPS_SYNC
+  | Barrier_MIPS_SYNC of unit
   (* RISC-V barriers *)
-  | 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_RISCV_rw_rw of unit
+  | Barrier_RISCV_r_rw of unit
+  | Barrier_RISCV_r_r of unit
+  | Barrier_RISCV_rw_w of unit
+  | Barrier_RISCV_w_w of unit
+  | Barrier_RISCV_w_rw of unit
+  | Barrier_RISCV_rw_r of unit
+  | Barrier_RISCV_r_w of unit
+  | Barrier_RISCV_w_r of unit
+  | Barrier_RISCV_tso of unit
+  | Barrier_RISCV_i of unit
   (* X86 *)
-  | Barrier_x86_MFENCE
+  | Barrier_x86_MFENCE of unit
 
+let string_a64_barrier_domain = function
+  | A64_FullShare  -> "A64_FullShare"
+  | A64_InnerShare -> "A64_InnerShare"
+  | A64_OuterShare -> "A64_OuterShare"
+  | A64_NonShare   -> "A64_NonShare"
+end
+
+instance (Show a64_barrier_domain)
+  let show = string_a64_barrier_domain
+end
+
+let string_a64_barrier_type = function
+  | A64_barrier_all -> "A64_barrier_all"
+  | A64_barrier_LD  -> "A64_barrier_LD"
+  | A64_barrier_ST  -> "A64_barrier_ST"
+end
+
+instance (Show a64_barrier_type)
+  let show = string_a64_barrier_type
+end
 
 instance (Show barrier_kind)
   let show = function
-    | Barrier_Sync -> "Barrier_Sync"
-    | Barrier_LwSync -> "Barrier_LwSync"
-    | Barrier_Eieio -> "Barrier_Eieio"
-    | Barrier_Isync -> "Barrier_Isync"
-    | Barrier_DMB -> "Barrier_DMB"
-    | Barrier_DMB_ST -> "Barrier_DMB_ST"
-    | Barrier_DMB_LD -> "Barrier_DMB_LD"
-    | Barrier_DSB -> "Barrier_DSB"
-    | Barrier_DSB_ST -> "Barrier_DSB_ST"
-    | Barrier_DSB_LD -> "Barrier_DSB_LD"
-    | Barrier_ISB -> "Barrier_ISB"
-    | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT"
-    | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
-    | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw"
-    | Barrier_RISCV_r_rw  -> "Barrier_RISCV_r_rw"
-    | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
-    | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
-    | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
-    | Barrier_RISCV_w_rw  -> "Barrier_RISCV_w_rw"
-    | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
-    | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
-    | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
-    | Barrier_RISCV_tso   -> "Barrier_RISCV_tso"
-    | Barrier_RISCV_i     -> "Barrier_RISCV_i"
-    | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
+    | Barrier_Sync () -> "Barrier_Sync"
+    | Barrier_LwSync () -> "Barrier_LwSync"
+    | Barrier_Eieio () -> "Barrier_Eieio"
+    | Barrier_Isync () -> "Barrier_Isync"
+    | Barrier_DMB (dom,typ) -> "Barrier_DMB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")"
+    | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")"
+    | Barrier_ISB () -> "Barrier_ISB"
+    | Barrier_TM_COMMIT () -> "Barrier_TM_COMMIT"
+    | Barrier_MIPS_SYNC () -> "Barrier_MIPS_SYNC"
+    | Barrier_RISCV_rw_rw () -> "Barrier_RISCV_rw_rw"
+    | Barrier_RISCV_r_rw ()  -> "Barrier_RISCV_r_rw"
+    | Barrier_RISCV_r_r ()   -> "Barrier_RISCV_r_r"
+    | Barrier_RISCV_rw_w ()  -> "Barrier_RISCV_rw_w"
+    | Barrier_RISCV_w_w ()   -> "Barrier_RISCV_w_w"
+    | Barrier_RISCV_w_rw ()  -> "Barrier_RISCV_w_rw"
+    | Barrier_RISCV_rw_r ()  -> "Barrier_RISCV_rw_r"
+    | Barrier_RISCV_r_w ()   -> "Barrier_RISCV_r_w"
+    | Barrier_RISCV_w_r ()   -> "Barrier_RISCV_w_r"
+    | Barrier_RISCV_tso ()   -> "Barrier_RISCV_tso"
+    | Barrier_RISCV_i ()     -> "Barrier_RISCV_i"
+    | Barrier_x86_MFENCE ()  -> "Barrier_x86_MFENCE"
   end
 end
 
@@ -304,32 +332,45 @@ instance (EnumerationType write_kind)
   end
 end
 
+instance (EnumerationType a64_barrier_domain)
+  let toNat = function
+    | A64_FullShare  -> 0
+    | A64_InnerShare -> 1
+    | A64_OuterShare -> 2
+    | A64_NonShare   -> 3
+  end
+end
+
+instance (EnumerationType a64_barrier_type)
+  let toNat = function
+    | A64_barrier_all -> 0
+    | A64_barrier_LD  -> 1
+    | A64_barrier_ST  -> 2
+  end
+end
+
 instance (EnumerationType barrier_kind)
   let toNat = function
-    | Barrier_Sync -> 0
-    | Barrier_LwSync -> 1
-    | Barrier_Eieio ->2
-    | Barrier_Isync -> 3
-    | Barrier_DMB -> 4
-    | Barrier_DMB_ST -> 5
-    | Barrier_DMB_LD -> 6
-    | Barrier_DSB -> 7
-    | Barrier_DSB_ST -> 8
-    | Barrier_DSB_LD -> 9
-    | Barrier_ISB -> 10
-    | Barrier_TM_COMMIT -> 11
-    | Barrier_MIPS_SYNC -> 12
-    | Barrier_RISCV_rw_rw -> 13
-    | Barrier_RISCV_r_rw -> 14
-    | Barrier_RISCV_r_r -> 15
-    | Barrier_RISCV_rw_w -> 16
-    | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_w_rw -> 18
-    | Barrier_RISCV_rw_r -> 19
-    | Barrier_RISCV_r_w -> 20
-    | Barrier_RISCV_w_r -> 21
-    | Barrier_RISCV_tso -> 22
-    | Barrier_RISCV_i -> 23
-    | Barrier_x86_MFENCE -> 24
+    | Barrier_Sync () -> 0
+    | Barrier_LwSync () -> 1
+    | Barrier_Eieio () -> 2
+    | Barrier_Isync () -> 3
+    | Barrier_DMB (dom,typ) -> 4  + (toNat dom) + (4 * (toNat typ)) (* 4-15 *)
+    | Barrier_DSB (dom,typ) -> 16 + (toNat dom) + (4 * (toNat typ)) (* 16-27 *)
+    | Barrier_ISB () -> 28
+    | Barrier_TM_COMMIT () -> 29
+    | Barrier_MIPS_SYNC () -> 30
+    | Barrier_RISCV_rw_rw () -> 31
+    | Barrier_RISCV_r_rw () -> 32
+    | Barrier_RISCV_r_r () -> 33
+    | Barrier_RISCV_rw_w () -> 34
+    | Barrier_RISCV_w_w () -> 35
+    | Barrier_RISCV_w_rw () -> 36
+    | Barrier_RISCV_rw_r () -> 37
+    | Barrier_RISCV_r_w () -> 38
+    | Barrier_RISCV_w_r () -> 39
+    | Barrier_RISCV_tso () -> 40
+    | Barrier_RISCV_i () -> 41
+    | Barrier_x86_MFENCE () -> 42
   end
 end