Merge branch 'sail2' into rmem_interpreter

1 files changed, 26 insertions, 0 deletions

diff --git a/src/lem_interp/sail2_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index eadc85bf..bd3a3eb7 100644
--- a/src/lem_interp/sail2_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
@@ -203,6 +203,30 @@ instance (Show trans_kind)
   end
 end
 
+(* cache maintenance instructions *)
+type cache_op_kind =
+  (* AArch64 DC *)
+  | Cache_op_D_IVAC | Cache_op_D_ISW  | Cache_op_D_CSW  |  Cache_op_D_CISW
+  | Cache_op_D_ZVA  | Cache_op_D_CVAC | Cache_op_D_CVAU | Cache_op_D_CIVAC
+  (* AArch64 IC *)
+  | Cache_op_I_IALLUIS | Cache_op_I_IALLU | Cache_op_I_IVAU
+
+instance (Show cache_op_kind)
+  let show = function
+  | Cache_op_D_IVAC    -> "Cache_op_D_IVAC"
+  | Cache_op_D_ISW     -> "Cache_op_D_ISW"
+  | Cache_op_D_CSW     -> "Cache_op_D_CSW"
+  | Cache_op_D_CISW    -> "Cache_op_D_CISW"
+  | Cache_op_D_ZVA     -> "Cache_op_D_ZVA"
+  | Cache_op_D_CVAC    -> "Cache_op_D_CVAC"
+  | Cache_op_D_CVAU    -> "Cache_op_D_CVAU"
+  | Cache_op_D_CIVAC   -> "Cache_op_D_CIVAC"
+  | Cache_op_I_IALLUIS -> "Cache_op_I_IALLUIS"
+  | Cache_op_I_IALLU   -> "Cache_op_I_IALLU"
+  | Cache_op_I_IVAU    -> "Cache_op_I_IVAU"
+  end
+end
+
 type instruction_kind =
   | IK_barrier   of barrier_kind
   | IK_mem_read  of read_kind
@@ -213,6 +237,7 @@ type instruction_kind =
   and branch/jump (single nia of kind NIA_concrete_address) *)
   | IK_trans     of trans_kind
   | IK_simple    of unit
+  | IK_cache_op  of cache_op_kind
 
 
 instance (Show instruction_kind)
@@ -224,6 +249,7 @@ instance (Show instruction_kind)
     | IK_branch ()            -> "IK_branch"
     | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
     | IK_simple ()            -> "IK_simple"
+    | IK_cache_op cache_kind  -> "IK_cache_op " ^ (show cache_kind)
   end
 end