Merge branch 'master' into experiments

11 files changed, 437 insertions, 1451 deletions

diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 23c34222..76880dbd 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -6,20 +6,20 @@ open import Sail_values
 
 
 class (ToFromInterpValue 'a)
-  val toInterpValue : 'a -> Interp.value
-  val fromInterpValue : Interp.value -> 'a
+  val toInterpValue : 'a -> Interp_ast.value
+  val fromInterpValue : Interp_ast.value -> 'a
 end
 
 let toInterValueBool = function
-  | true -> Interp.V_lit (L_aux (L_one) Unknown)
-  | false -> Interp.V_lit (L_aux (L_zero) Unknown)
+  | true -> Interp_ast.V_lit (L_aux (L_one) Unknown)
+  | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
 end
 let rec fromInterpValueBool v = match v with
-  | Interp.V_lit (L_aux (L_true) _)  -> true
-  | Interp.V_lit (L_aux (L_false) _) -> false
-  | Interp.V_lit (L_aux (L_one) _)  -> true
-  | Interp.V_lit (L_aux (L_zero) _) -> false
-  | Interp.V_tuple [v] -> fromInterpValueBool v
+  | Interp_ast.V_lit (L_aux (L_one) _)  -> true
+  | Interp_ast.V_lit (L_aux (L_true) _)  ->  true
+  | Interp_ast.V_lit (L_aux (L_zero) _) -> false
+  | Interp_ast.V_lit (L_aux (L_false) _) -> false
+  | Interp_ast.V_tuple [v] -> fromInterpValueBool v
   | v -> failwith ("fromInterpValue bool: unexpected value. " ^
                      Interp.debug_print_value v)
 end
@@ -29,10 +29,10 @@ instance (ToFromInterpValue bool)
 end
 
 
-let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown)
+let toInterpValueUnit () = Interp_ast.V_lit (L_aux (L_unit) Unknown)
 let rec fromInterpValueUnit v = match v with
-  | Interp.V_lit (L_aux (L_unit) _) -> ()
-  | Interp.V_tuple [v] -> fromInterpValueUnit v
+  | Interp_ast.V_lit (L_aux (L_unit) _) -> ()
+  | Interp_ast.V_tuple [v] -> fromInterpValueUnit v
   | v -> failwith ("fromInterpValue unit: unexpected value. " ^
                      Interp.debug_print_value v)
 end
@@ -44,8 +44,8 @@ end
 
 let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown)
 let rec fromInterpValueInteger v = match v with
-  | Interp.V_lit (L_aux (L_num i) _) -> i
-  | Interp.V_tuple [v] -> fromInterpValueInteger v
+  | Interp_ast.V_lit (L_aux (L_num i) _) -> i
+  | Interp_ast.V_tuple [v] -> fromInterpValueInteger v
   | v -> failwith ("fromInterpValue integer: unexpected value. " ^
                      Interp.debug_print_value v)
 end
@@ -57,8 +57,8 @@ end
 
 let toInterpValueString s = V_lit (L_aux (L_string s) Unknown)
 let rec fromInterpValueString v = match v with
-  | Interp.V_lit (L_aux (L_string s) _) -> s
-  | Interp.V_tuple [v] -> fromInterpValueString v
+  | Interp_ast.V_lit (L_aux (L_string s) _) -> s
+  | Interp_ast.V_tuple [v] -> fromInterpValueString v
   | v -> failwith ("fromInterpValue integer: unexpected value. " ^
                      Interp.debug_print_value v)
 end
@@ -69,17 +69,17 @@ end
 
 
 let toInterpValueBitU = function
-  | I     -> Interp.V_lit (L_aux (L_one) Unknown)
-  | O     -> Interp.V_lit (L_aux (L_zero) Unknown)
-  | Undef -> Interp.V_lit (L_aux (L_undef) Unknown)
+  | B1 -> Interp_ast.V_lit (L_aux (L_one) Unknown)
+  | B0 -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
+  | BU -> Interp_ast.V_lit (L_aux (L_undef) Unknown)
 end
 let rec fromInterpValueBitU v = match v with
-  | Interp.V_lit (L_aux (L_one) _)   -> I
-  | Interp.V_lit (L_aux (L_zero) _)  -> O
-  | Interp.V_lit (L_aux (L_undef) _) -> Undef
-  | Interp.V_lit (L_aux (L_true) _)   -> I
-  | Interp.V_lit (L_aux (L_false) _)  -> O
-  | Interp.V_tuple [v] -> fromInterpValueBitU v
+  | Interp_ast.V_lit (L_aux (L_one) _)   -> B1
+  | Interp_ast.V_lit (L_aux (L_zero) _)  -> B0
+  | Interp_ast.V_lit (L_aux (L_undef) _) -> BU
+  | Interp_ast.V_lit (L_aux (L_true) _)   -> B1
+  | Interp_ast.V_lit (L_aux (L_false) _)  -> B0 
+  | Interp_ast.V_tuple [v] -> fromInterpValueBitU v
   | v -> failwith ("fromInterpValue bitU: unexpected value. " ^
                      Interp.debug_print_value v)
 end
@@ -383,29 +383,33 @@ instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
 end
 
 
-module SI = Interp
-module SIA = Interp_ast
-
-
 let read_kindToInterpValue = function
   | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ())
-  | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
-  | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
-  | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ())
-  | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ())
-  | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ())
-  | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ())
-  | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ())
+  | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
+  | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ())
+  | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ())
+  | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ())
+  | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ())
+  | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ())
+  | Read_RISCV_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ())
+  | Read_RISCV_reserved -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ())
+  | Read_RISCV_reserved_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ())
+  | Read_RISCV_reserved_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ())
+  | Read_X86_locked -> V_ctor (Id_aux (Id "Read_X86_locked") Unknown) (T_id "read_kind") (C_Enum 11) (toInterpValue ())
   end
 let rec read_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain
-  | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag
-  | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve
   | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve
   | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire
   | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive
   | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire
   | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream
+  | V_ctor (Id_aux (Id "Read_RISCV_acquire") _) _ _ v -> Read_RISCV_acquire
+  | V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") _) _ _ v -> Read_RISCV_strong_acquire
+  | V_ctor (Id_aux (Id "Read_RISCV_reserved") _) _ _ v -> Read_RISCV_reserved
+  | V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") _) _ _ v -> Read_RISCV_reserved_acquire
+  | V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") _) _ _ v -> Read_RISCV_reserved_strong_acquire
+  | V_ctor (Id_aux (Id "Read_X86_locked") _) _ _ v -> Read_X86_locked
   | V_tuple [v] -> read_kindFromInterpValue v
   | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^
                      Interp.debug_print_value v)
@@ -418,21 +422,29 @@ end
 
 let write_kindToInterpValue = function
   | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ())
-  | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
-  | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
-  | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ())
-  | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ())
-  | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ())
-  | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ())
+  | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
+  | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ())
+  | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ())
+  | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ())
+  | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ())
+  | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ())
+  | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ())
+  | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ())
+  | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ())
+  | Write_X86_locked -> V_ctor (Id_aux (Id "Write_X86_locked") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ())
   end
 let rec write_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain
-  | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag
-  | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional
   | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional
   | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release
   | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive
   | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release
+  | V_ctor (Id_aux (Id "Write_RISCV_release") _) _ _ v -> Write_RISCV_release
+  | V_ctor (Id_aux (Id "Write_RISCV_strong_release") _) _ _ v -> Write_RISCV_strong_release
+  | V_ctor (Id_aux (Id "Write_RISCV_conditional") _) _ _ v -> Write_RISCV_conditional
+  | V_ctor (Id_aux (Id "Write_RISCV_conditional_release") _) _ _ v -> Write_RISCV_conditional_release
+  | V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") _) _ _ v -> Write_RISCV_conditional_strong_release
+  | V_ctor (Id_aux (Id "Write_X86_locked") _) _ _ v -> Write_X86_locked
   | V_tuple [v] -> write_kindFromInterpValue v
   | v -> failwith ("fromInterpValue write_kind: unexpected value " ^
                      Interp.debug_print_value v)
@@ -455,7 +467,15 @@ let barrier_kindToInterpValue = function
   | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ())
   | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ())
   | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ())
-  | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ())
+  | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ())
+  | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ())
+  | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ())
+  | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ())
+  | Barrier_RISCV_r_r -> V_ctor (Id_aux (Id "Barrier_RISCV_r_r") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ())
+  | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ())
+  | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ())
+  | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ())
+  | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 19) (toInterpValue ())
   end
 let rec barrier_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync
@@ -469,7 +489,15 @@ let rec barrier_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST
   | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD
   | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB
+  | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT
   | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC
+  | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw
+  | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw
+  | V_ctor (Id_aux (Id "Barrier_RISCV_r_r") _) _ _ v -> Barrier_RISCV_r_r
+  | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w
+  | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w
+  | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i
+  | V_ctor (Id_aux (Id "Barrier_x86_MFENCE") _) _ _ v -> Barrier_x86_MFENCE
   | V_tuple [v] -> barrier_kindFromInterpValue v
   | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^
                      Interp.debug_print_value v)
@@ -480,18 +508,41 @@ instance (ToFromInterpValue barrier_kind)
 end
 
 
+let trans_kindToInterpValue = function
+  | Transaction_start -> V_ctor (Id_aux (Id "Transaction_start") Unknown) (T_id "trans_kind") (C_Enum 0) (toInterpValue ())
+  | Transaction_commit -> V_ctor (Id_aux (Id "Transaction_commit") Unknown) (T_id "trans_kind") (C_Enum 1) (toInterpValue ())
+  | Transaction_abort -> V_ctor (Id_aux (Id "Transaction_abort") Unknown) (T_id "trans_kind") (C_Enum 2) (toInterpValue ())
+  end
+let rec trans_kindFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "Transaction_start") _) _ _ v -> Transaction_start
+  | V_ctor (Id_aux (Id "Transaction_commit") _) _ _ v -> Transaction_commit
+  | V_ctor (Id_aux (Id "Transaction_abort") _) _ _ v -> Transaction_abort
+  | V_tuple [v] -> trans_kindFromInterpValue v
+  | v -> failwith ("fromInterpValue trans_kind: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue trans_kind)
+  let toInterpValue = trans_kindToInterpValue
+  let fromInterpValue = trans_kindFromInterpValue
+end
+
+
 let instruction_kindToInterpValue = function
   | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
+  | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
+  | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
   end
 let rec instruction_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v)
+  | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch
+  | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple
   | V_tuple [v] -> instruction_kindFromInterpValue v
   | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^
@@ -503,18 +554,18 @@ instance (ToFromInterpValue instruction_kind)
 end
 
 let regfpToInterpValue = function
-  | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
+  | RFull v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
+  | RSlice v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
+  | RSliceBit v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
+  | RField v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
   end
 
 let rec regfpFromInterpValue v = match v with
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v)
-  | SI.V_tuple [v] -> regfpFromInterpValue v
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
+  | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") _) _ _ v -> RField (fromInterpValue v)
+  | Interp_ast.V_tuple [v] -> regfpFromInterpValue v
   | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v)
   end
 
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index d160e84a..213acea1 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -889,18 +889,25 @@ let shift_op_vec_int op (l,r) =
     let len = Array.length array in
     (match op with
      | "<<" ->
-       let left = Array.sub array r (len - r) in
-       let right = Array.make r Vzero in
-       let result = Array.append left right in
-       Vvector(result, start, ord)
+       if (r <= len) then
+         let left = Array.sub array r (len - r) in
+         let right = Array.make r Vzero in
+         let result = Array.append left right in
+         Vvector(result, start, ord)
+       else
+         Vvector(Array.make len Vzero, start, ord)
      | ">>" ->
-       let left = Array.make r Vzero in
-       let right = Array.sub array 0 (len - r) in
-       let result = Array.append left right in
-       Vvector(result, start, ord)
+       if (r <= len) then
+         let left = Array.make r Vzero in
+         let right = Array.sub array 0 (len - r) in
+         let result = Array.append left right in
+         Vvector(result, start, ord)
+       else
+         Vvector(Array.make len Vzero, start, ord)
      | "<<<" ->
-       let left = Array.sub array r (len - r) in
-       let right = Array.sub array 0 r in
+       let rmod = r mod len in
+       let left = Array.sub array rmod (len - rmod) in
+       let right = Array.sub array 0 rmod in
        let result = Array.append left right in
        Vvector(result, start, ord)
      | _ -> assert false)
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 69b9e301..2fff7344 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -79,7 +79,23 @@ let set_reg state reg v =
   <| state with regstate = reg.write_to state.regstate v |>
 
 
-val read_mem : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b
+let is_exclusive = function 
+  | Sail_impl_base.Read_plain -> false
+  | Sail_impl_base.Read_reserve -> true
+  | Sail_impl_base.Read_acquire -> false
+  | Sail_impl_base.Read_exclusive -> true
+  | Sail_impl_base.Read_exclusive_acquire -> true
+  | Sail_impl_base.Read_stream -> false
+  | Sail_impl_base.Read_RISCV_acquire -> false
+  | Sail_impl_base.Read_RISCV_strong_acquire -> false
+  | Sail_impl_base.Read_RISCV_reserved -> true
+  | Sail_impl_base.Read_RISCV_reserved_acquire -> true
+  | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true
+  | Sail_impl_base.Read_X86_locked -> true
+end
+
+
+val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
 let read_mem dir read_kind addr sz state =
   let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
@@ -94,7 +110,7 @@ let read_mem dir read_kind addr sz state =
     | Sail_impl_base.Read_stream -> false
   end in
 
-  if is_exclusive 
+  if is_exclusive read_kind
   then [(Left value, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Left value, state)]
 
@@ -118,7 +134,7 @@ let read_tag dir read_kind addr state =
   end in
 
   (* TODO Should reading a tag set the exclusive flag? *)
-  if is_exclusive
+  if is_exclusive read_kind
   then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Left tag, state)]
 
@@ -174,7 +190,23 @@ let reg_deref = read_reg
 
 val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit
 let write_reg reg v state =
-  [(Left (), <| state with regstate = reg.write_to state.regstate v |>)]
+  [(Left (),<| state with regstate = Map.insert (name_of_reg reg) v state.regstate |>)]
+let write_reg_range reg i j v =
+  read_reg reg >>= fun current_value ->
+  let new_value = update current_value i j v in
+  write_reg reg new_value
+let write_reg_bit reg i bit =
+  write_reg_range reg i i (Vector [bit] i (is_inc_of_reg reg))
+let write_reg_field reg regfield =
+  let (i,j) = register_field_indices reg regfield in  
+  write_reg_range reg i j
+let write_reg_bitfield reg regfield =
+  let (i,_) = register_field_indices reg regfield in  
+  write_reg_bit reg i
+let write_reg_field_range reg regfield i j v =
+  read_reg_field reg regfield >>= fun current_field_value ->
+  let new_field_value = update current_field_value i j v in
+  write_reg_field reg regfield new_field_value
 
 val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit
 let update_reg reg f v state =
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 301849cd..cc10b758 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1419,8 +1419,8 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
    | V_ctor (Id_aux cid _) t ckind v ->
      if id = cid
      then (match (pats,detaint v) with
-     | ([],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
-     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
+     | ([],(V_lit (L_aux L_unit _))) -> (true,false,eenv)
+     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,false,eenv)
      | ([p],_) -> match_pattern t_level p v
      | _ -> (false,false,eenv) end)
      else (false,false,eenv)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index e9533a2a..c982a30a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -471,7 +471,7 @@ let translate_address top_level end_flag thunk_name registers address =
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (address_error,events) =
-    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction
+    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str (V_list []) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -506,17 +506,16 @@ let intern_instruction direction (name,parms) =
   Interp_ast.V_ctor (Interp.id_of_string name) (mk_typ_id "ast") Interp_ast.C_Union
     (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms))
 
-let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
+let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) =
   let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
   let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
   let mode = make_mode true false debug in
   let int_mode = mode.internal_mode in
-  let intern_val = intern_instruction direction instruction in
-  let val_str = Interp.string_of_value intern_val in
-  let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
+  let val_str = Interp.string_of_value instruction in
+  let (arg,_) = Interp.to_exp int_mode Interp.eenv instruction in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (analysis_or_error,events) =
-    interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) internal_direction
+    interp_to_value_helper debug Nothing Ivh_analysis val_str (V_list []) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -574,6 +573,33 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
             NIA_register (reg_to_reg_name reg)
          | _ -> 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) _) _ _ _) ->
@@ -589,27 +615,19 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                         | "Barrier_DSB_ST" -> Barrier_DSB_ST
                         | "Barrier_DSB_LD" -> Barrier_DSB_LD
                         | "Barrier_ISB" ->    Barrier_ISB
-                        | "Barrier_MIPS_SYNC" ->    Barrier_MIPS_SYNC
+                        | "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 (match r with
-                         | "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
-                         end)
+            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 (match w with
-                         | "Write_plain" ->             Write_plain
-                         | "Write_conditional" ->       Write_conditional
-                         | "Write_release" ->           Write_release
-                         | "Write_exclusive" ->         Write_exclusive
-                         | "Write_exclusive_release" -> Write_exclusive_release
-                          end)
+            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_cond_branch") _) _ _ _ ->
             IK_cond_branch
          | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
@@ -681,7 +699,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (instr_decoded_error,events) =
-    interp_to_value_helper debug (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false
+    interp_to_value_helper debug (Just value) Ivh_decode val_str (V_list []) internal_direction registers [] false
       (fun _ -> Interp.resume 
           mode 
           (Interp.Thunk_frame 
@@ -689,9 +707,9 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
              top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in
   match (instr_decoded_error) with
     | Ivh_value instr -> 
-      let instr_external = interp_value_to_instr_external top_level instr in
+       (* let instr_external = interp_value_to_instr_external top_level instr in*) 
       let (instr_decoded_error,events) =
-        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr_external internal_direction
+        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr (*instr_external*) internal_direction
           registers [] false
         (fun _ -> Interp.resume 
             mode
@@ -700,7 +718,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
                   (Interp_ast.Unknown, Nothing)) 
                top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in
       match (instr_decoded_error) with
-        | Ivh_value _ -> IDE_instr instr_external instr
+      | Ivh_value _ -> IDE_instr instr (*instr_external*)
         | Ivh_value_after_exn v ->
           Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now"
         | Ivh_error err -> IDE_decode_error err
@@ -714,9 +732,9 @@ end
 let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = 
   let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
   match decode_to_instruction top_level registers value with
-  | IDE_instr instr instrv ->
+  | IDE_instr instr ->
      let mode = make_interpreter_mode true false in
-     let (arg,_) = Interp.to_exp mode Interp.eenv instrv in
+     let (arg,_) = Interp.to_exp mode Interp.eenv instr in
      Instr instr
            (IState (Interp.Thunk_frame
                       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
@@ -751,11 +769,11 @@ let instr_external_to_interp_value top_level instr =
   Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) 
                 (mk_typ_id "ast") Interp_ast.C_Union parmsV
 
-val instruction_to_istate : context -> instruction -> instruction_state 
-let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state  = 
+val instruction_to_istate : context -> Interp_ast.value -> instruction_state 
+let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state  = 
   let mode = make_interpreter_mode true false in
   let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in
-  let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in
+  let ast_node = fst (Interp.to_exp mode Interp.eenv instr) in
   (IState
      (Interp.Thunk_frame
         (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [ast_node])
@@ -1093,7 +1111,7 @@ and state_to_outcome_s pp_instruction_state mode state =
          (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state))
   )
 
-val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> Interp_ast.value -> Sail_impl_base.outcome_s unit
 let initial_outcome_s_of_instruction pp_instruction_state context mode instruction =
   let state = instruction_to_istate context instruction in
   state_to_outcome_s pp_instruction_state mode state
@@ -1223,136 +1241,13 @@ let nia_address_of_event nia_reg (event: event) : maybe (maybe address) =
   | _ -> Nothing
   end
 
-let nias_of_instruction 
-      thread_ism
-    (nia_address: list (maybe address)) (* Nothing for unknown/undef*)
-    (regs_in:     list reg_name)
-    (instruction: instruction)
-    : list nia
-  =
-  let (instruction_name, instruction_fields) = instruction in
-
-  let unknown_nia_address = List.elem Nothing nia_address in
-
-  let nias = [NIA_concrete_address addr | forall (addr MEM (List.mapMaybe id nia_address)) | true] in
-
-  (* it's a fact of the Power2.06B instruction pseudocode that in the B and Bc
-     cases there should be no Unknown values in nia_values, while in the Bclr
-     and Bcctr cases nia_values will just be Unknown and the semantics should
-     match the comments in the machineDefTypes definition of nia *)
-  (* All our other analysis is on the pseudocode directly, which is arguably
-     pleasingly robust.  We could replace the nias pattern match on
-     instruction_name with something in that style if the exhaustive interpreter
-     announced register dependencies to register writes (easy) and if it could
-     check the form of the register writes to LR and CTR matches the
-     machineDefTypes nia definition *)
-  match (thread_ism, instruction_name) with
-    | ("PPCGEN_ism", "B") ->
-       let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values 1" in
-       nias
-    | ("PPCGEN_ism", "Bc") ->
-       let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values 2" in
-       NIA_successor :: nias
-    | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ]
-    | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ]
-    | ("PPCGEN_ism", "Sc") ->
-       let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values 3" in
-       match instruction_fields with
-       | [(_, _, lev)] ->
-          (* LEV field is 7 bits long, pad it with false at beginning *)
-          if lev = [Bitc_zero;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one]
-                     (* (Interp_inter_imp.integer_of_byte_list (Interp_inter_imp.to_bytes (false :: bl))) = 63 *)
-          then []
-          else [NIA_successor]
-       | _ -> [ NIA_successor ]
-       end
-
-    (* AARch64 label branch (i.e. address must be known) although
-    these instructions take the address as an offset from PC, in here
-    we see the absolute address as it was extracted from the micro ops
-    just before write to PC *)
-    | ("AArch64HandSail", "BranchImmediate")   -> nias
-    | ("AArch64HandSail", "BranchConditional") -> NIA_successor :: nias
-    | ("AArch64HandSail", "CompareAndBranch")  -> NIA_successor :: nias
-    | ("AArch64HandSail", "TestBitAndBranch")  -> NIA_successor :: nias
-
-    (* AArch64 calculated address branch *)
-    | ("AArch64HandSail", "BranchRegister") ->
-        (* do some parsing of the ast fields to figure out which register holds
-           the branching address i.e. find n in "BR <Xn>". The ast constructor
-           from armV8.sail: (reg_index,BranchType) BranchRegister; *)
-        let n_integer =
-          match instruction_fields with
-          | [(_, _, n); _] -> integer_of_bit_list n
-          | _ -> fail
-          end
-        in
-        let () = ensure (0 <= n_integer && n_integer <= 31)
-                  "expected register number from 0 to 31"
-        in
-        if n_integer = 31 then
-          nias (* BR XZR *)
-        else
-          (* look for Xn (which we actually call Rn) in regs_in *)
-          let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in
-          [NIA_register r | forall (r MEM regs_in)
-                          | match r with
-                            | (Reg name _ _ _) -> name = n_reg
-                            | _ -> false
-                            end]
-
-
-    (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *)
-
-    | ("AArch64GenSail", "BranchImmediate")   -> nias
-    | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias
-    | ("AArch64GenSail", "CompareAndBranch")  -> NIA_successor :: nias
-    | ("AArch64GenSail", "TestBitAndBranch")  -> NIA_successor :: nias
-
-    (* AArch64 calculated address branch *)
-    | ("AArch64GenSail", "branch_unconditional_register") ->
-        (* do some parsing of the ast fields to figure out which register holds
-           the branching address i.e. find n in "BR <Xn>". The ast constructor
-           from armV8.sail: (reg_index,BranchType) BranchRegister; *)
-        let n_integer =
-          match instruction_fields with
-          | [(_, _, n); _] -> integer_of_bit_list n
-          | _ -> fail
-          end
-        in
-        let () = ensure (0 <= n_integer && n_integer <= 31)
-                  "expected register number from 0 to 31"
-        in
-        if n_integer = 31 then
-          nias (* BR XZR *)
-        else
-          (* look for Xn (which we actually call Rn) in regs_in *)
-          let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in
-          [NIA_register r | forall (r MEM regs_in)
-                          | match r with
-                            | (Reg name _ _ _) -> name = n_reg
-                            | _ -> false
-                            end]
-
-    (** end of hacky *)
-
-    | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias
-
-
-    | ("MIPS_ism", "B") -> fail
-
-    | (s1,s2) ->
-       let () = ensure (not unknown_nia_address)
-                       ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in
-        [ NIA_successor ]
-    end
-
 let interp_instruction_analysis 
+      top_level
       (interp_exhaustive : ((list (reg_name * register_value)) -> list event))
-      instruction nia_reg ism environment = 
+      instruction 
+      nia_reg 
+      (nias_function : (list (maybe address) -> list reg_name -> list nia))
+      ism environment = 
     
     let es = interp_exhaustive environment in
 
@@ -1363,7 +1258,7 @@ let interp_instruction_analysis
 
     let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
 
-    let nias = nias_of_instruction ism nia_address regs_in instruction in
+    let nias = nias_function nia_address regs_in in
 
     let dia = DIA_none in (* FIX THIS! *)
 
@@ -1377,6 +1272,41 @@ let interp_instruction_analysis
 
           if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
             inst_kind
+
+          else if
+            (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | IK_mem_write _ -> true
+                | IK_mem_rmw _   -> false
+                | IK_barrier _   -> false
+                | IK_cond_branch -> false
+                | IK_trans _     -> false
+                | IK_simple      -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_read _  -> true
+                | _              -> false
+                end) &&
+            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                match inst_kind' with
+                | IK_mem_write _ -> true
+                | _              -> false
+                end)
+          then
+            match
+              List.partition
+                (function IK_mem_read _ -> true | _ -> false end)
+                (inst_kind :: inst_kinds)
+            with
+            | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) ->
+                let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in
+                let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in
+                IK_mem_rmw (r, w)
+            | _ -> fail
+            end
+
           (* the TSTART instruction can also be aborted so it will have two kinds of events *)
           else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
                         inst_kind' = IK_trans Transaction_start) &&
@@ -1385,7 +1315,9 @@ let interp_instruction_analysis
                         || inst_kind' = IK_trans Transaction_abort)
           then
             IK_trans Transaction_start
-          else failwith "multiple instruction kinds"
+
+          else
+            failwith "multiple instruction kinds"
     end in
 
   (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
@@ -1401,29 +1333,29 @@ val print_and_fail_of_inequal : forall 'a. Show 'a =>
                                 (instruction -> string) ->
                                 (string * 'a) -> (string * 'a) -> unit
 let print_and_fail_if_inequal 
-      (print_endline,pp_instruction,instruction)
+      (print_endline,instruction)
       (name1,xs1) (name2,xs2) =
   if xs1 = xs2 then ()
   else 
     let () = print_endline (name1^": "^show xs1) in
     let () = print_endline (name2^": "^show xs2) in
-    failwith (name1^" and "^ name2^" inequal for instruction " ^ pp_instruction instruction)
+    failwith (name1^" and "^ name2^" inequal for instruction: \n" ^ Interp.string_of_value instruction)
 
 let interp_compare_analyses 
       print_endline
-      pp_instruction
       (non_pseudo_registers : set reg_name -> set reg_name)
       context
       endianness
       interp_exhaustive
-      instruction
+      (instruction : Interp_ast.value)
       nia_reg
+      (nias_function : (list (maybe address) -> list reg_name -> list nia))
       ism
       environment
       analysis_function
       reg_info = 
   let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = 
-    interp_instruction_analysis interp_exhaustive instruction nia_reg ism 
+    interp_instruction_analysis context interp_exhaustive instruction nia_reg nias_function ism 
                                 environment in
   let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) =
     (Set.fromList regs_in1,
@@ -1448,7 +1380,7 @@ let interp_compare_analyses
      non_pseudo_registers regs_out2S,
      non_pseudo_registers regs_feeding_address2S) in
 
-  let aux = (print_endline,pp_instruction,instruction) in
+  let aux = (print_endline,instruction) in
   let () = (print_and_fail_if_inequal aux)
              ("regs_in exhaustive",regs_in1S) 
              ("regs_in hand",regs_in2S) in
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index dcc9f537..07d9e2b3 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -104,6 +104,10 @@ end
   and the potential static effects from the funcl clause for this instruction 
   Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
 *)
+
+
+type instruction_field_value = list bit
+
 type instruction = (string * list (string * instr_parm_typ * instruction_field_value))
 
 let {coq} instructionEqual i1 i2 = match (i1,i2) with
@@ -117,7 +121,7 @@ let inline ~{coq} instructionInequal = unsafe_structural_inequality
 type v_kind = Bitv | Bytev
 
 type decode_error = 
-  | Unsupported_instruction_error of instruction
+  | Unsupported_instruction_error of Interp_ast.value
   | Not_an_instruction_error of opcode
   | Internal_error of string
 
@@ -264,12 +268,12 @@ val initial_instruction_state : context -> string -> list register_value -> inst
   (* string is a function name, list of value are the parameters to that function *)
 
 type instruction_or_decode_error =
-  | IDE_instr of instruction * Interp_ast.value
+  | IDE_instr of Interp_ast.value
   | IDE_decode_error of decode_error
 
 (** propose to remove the following type and use the above instead *)
 type i_state_or_error =
-  | Instr of instruction * instruction_state
+  | Instr of Interp_ast.value * instruction_state
   | Decode_error of decode_error
 
 
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 2a1783db..98b98a03 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -1198,12 +1198,16 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
           let opcode = Opcode (get_opcode pc) in
           let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
             | Instr(instruction,istate) ->
-              interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
+               let instruction = interp_value_to_instr_external context instruction in
+               interactf "\n**** Running: %s ****\n"
+                         (Printing_functions.instruction_to_string instruction);
               (instruction,istate)
             | Decode_error d ->
               (match d with
-              | Interp_interface.Unsupported_instruction_error instr ->
-                errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
+              | Interp_interface.Unsupported_instruction_error instruction ->
+                 let instruction = interp_value_to_instr_external context instruction in
+                 errorf "\n**** Encountered unsupported instruction %s ****\n"
+                        (Printing_functions.instruction_to_string instruction)
               | Interp_interface.Not_an_instruction_error op ->
                 (match op with
                 | Opcode bytes ->
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index e773bf5b..7750c16c 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -124,375 +124,13 @@ let register_state_zero register_data rbn : register_value =
   in register_value_zeros dir width start_index
 
 type model = PPC | AArch64 | MIPS
-(*
-let ppc_register_data_all =  [
-  (*Pseudo registers*)
-  ("CIA",   (D_increasing, 64, 0));
-  ("NIA",   (D_increasing, 64, 0));
-  ("mode64bit", (D_increasing, 1, 0));
-  ("bigendianmode", (D_increasing, 1, 0));
-  (* special registers *)
-  ("CR",    (D_increasing, 32, 32));
-  ("CTR",   (D_increasing, 64, 0 ));
-  ("LR",    (D_increasing, 64, 0 ));
-  ("XER",   (D_increasing, 64, 0 ));
-  ("VRSAVE",(D_increasing, 32, 32));
-  ("FPSCR", (D_increasing, 64, 0 ));
-  ("VSCR",  (D_increasing, 32, 96));
-
-  (* general purpose registers *)
-  ("GPR0",  (D_increasing, 64, 0 ));
-  ("GPR1",  (D_increasing, 64, 0 ));
-  ("GPR2",  (D_increasing, 64, 0 ));
-  ("GPR3",  (D_increasing, 64, 0 ));
-  ("GPR4",  (D_increasing, 64, 0 ));
-  ("GPR5",  (D_increasing, 64, 0 ));
-  ("GPR6",  (D_increasing, 64, 0 ));
-  ("GPR7",  (D_increasing, 64, 0 ));
-  ("GPR8",  (D_increasing, 64, 0 ));
-  ("GPR9",  (D_increasing, 64, 0 ));
-  ("GPR10", (D_increasing, 64, 0 ));
-  ("GPR11", (D_increasing, 64, 0 ));
-  ("GPR12", (D_increasing, 64, 0 ));
-  ("GPR13", (D_increasing, 64, 0 ));
-  ("GPR14", (D_increasing, 64, 0 ));
-  ("GPR15", (D_increasing, 64, 0 ));
-  ("GPR16", (D_increasing, 64, 0 ));
-  ("GPR17", (D_increasing, 64, 0 ));
-  ("GPR18", (D_increasing, 64, 0 ));
-  ("GPR19", (D_increasing, 64, 0 ));
-  ("GPR20", (D_increasing, 64, 0 ));
-  ("GPR21", (D_increasing, 64, 0 ));
-  ("GPR22", (D_increasing, 64, 0 ));
-  ("GPR23", (D_increasing, 64, 0 ));
-  ("GPR24", (D_increasing, 64, 0 ));
-  ("GPR25", (D_increasing, 64, 0 ));
-  ("GPR26", (D_increasing, 64, 0 ));
-  ("GPR27", (D_increasing, 64, 0 ));
-  ("GPR28", (D_increasing, 64, 0 ));
-  ("GPR29", (D_increasing, 64, 0 ));
-  ("GPR30", (D_increasing, 64, 0 ));
-  ("GPR31", (D_increasing, 64, 0 ));
-  (* vector registers *)
-  ("VR0",  (D_increasing, 128, 0 ));
-  ("VR1",  (D_increasing, 128, 0 ));
-  ("VR2",  (D_increasing, 128, 0 ));
-  ("VR3",  (D_increasing, 128, 0 ));
-  ("VR4",  (D_increasing, 128, 0 ));
-  ("VR5",  (D_increasing, 128, 0 ));
-  ("VR6",  (D_increasing, 128, 0 ));
-  ("VR7",  (D_increasing, 128, 0 ));
-  ("VR8",  (D_increasing, 128, 0 ));
-  ("VR9",  (D_increasing, 128, 0 ));
-  ("VR10", (D_increasing, 128, 0 ));
-  ("VR11", (D_increasing, 128, 0 ));
-  ("VR12", (D_increasing, 128, 0 ));
-  ("VR13", (D_increasing, 128, 0 ));
-  ("VR14", (D_increasing, 128, 0 ));
-  ("VR15", (D_increasing, 128, 0 ));
-  ("VR16", (D_increasing, 128, 0 ));
-  ("VR17", (D_increasing, 128, 0 ));
-  ("VR18", (D_increasing, 128, 0 ));
-  ("VR19", (D_increasing, 128, 0 ));
-  ("VR20", (D_increasing, 128, 0 ));
-  ("VR21", (D_increasing, 128, 0 ));
-  ("VR22", (D_increasing, 128, 0 ));
-  ("VR23", (D_increasing, 128, 0 ));
-  ("VR24", (D_increasing, 128, 0 ));
-  ("VR25", (D_increasing, 128, 0 ));
-  ("VR26", (D_increasing, 128, 0 ));
-  ("VR27", (D_increasing, 128, 0 ));
-  ("VR28", (D_increasing, 128, 0 ));
-  ("VR29", (D_increasing, 128, 0 ));
-  ("VR30", (D_increasing, 128, 0 ));
-  ("VR31", (D_increasing, 128, 0 ));
-  (* floating-point registers *)
-  ("FPR0",  (D_increasing, 64, 0 ));
-  ("FPR1",  (D_increasing, 64, 0 ));
-  ("FPR2",  (D_increasing, 64, 0 ));
-  ("FPR3",  (D_increasing, 64, 0 ));
-  ("FPR4",  (D_increasing, 64, 0 ));
-  ("FPR5",  (D_increasing, 64, 0 ));
-  ("FPR6",  (D_increasing, 64, 0 ));
-  ("FPR7",  (D_increasing, 64, 0 ));
-  ("FPR8",  (D_increasing, 64, 0 ));
-  ("FPR9",  (D_increasing, 64, 0 ));
-  ("FPR10", (D_increasing, 64, 0 ));
-  ("FPR11", (D_increasing, 64, 0 ));
-  ("FPR12", (D_increasing, 64, 0 ));
-  ("FPR13", (D_increasing, 64, 0 ));
-  ("FPR14", (D_increasing, 64, 0 ));
-  ("FPR15", (D_increasing, 64, 0 ));
-  ("FPR16", (D_increasing, 64, 0 ));
-  ("FPR17", (D_increasing, 64, 0 ));
-  ("FPR18", (D_increasing, 64, 0 ));
-  ("FPR19", (D_increasing, 64, 0 ));
-  ("FPR20", (D_increasing, 64, 0 ));
-  ("FPR21", (D_increasing, 64, 0 ));
-  ("FPR22", (D_increasing, 64, 0 ));
-  ("FPR23", (D_increasing, 64, 0 ));
-  ("FPR24", (D_increasing, 64, 0 ));
-  ("FPR25", (D_increasing, 64, 0 ));
-  ("FPR26", (D_increasing, 64, 0 ));
-  ("FPR27", (D_increasing, 64, 0 ));
-  ("FPR28", (D_increasing, 64, 0 ));
-  ("FPR29", (D_increasing, 64, 0 ));
-  ("FPR30", (D_increasing, 64, 0 ));
-  ("FPR31", (D_increasing, 64, 0 ));
-]
-
-let initial_stack_and_reg_data_of_PPC_elf_file e_entry all_data_memory =
-  (* set up initial registers, per 3.4.1 of 64-bit PowerPC ELF Application Binary Interface Supplement 1.9 *)
-
-  let auxiliary_vector_space = Nat_big_num.of_string "17592186042368" (*"0xffffffff800"*) in
-  (* notionally there should be at least an AT_NULL auxiliary vector entry there, but our examples will never read it *)
-
-  (* take start of stack roughly where running gdb on hello5 on bim says it is*)
-  let initial_GPR1_stack_pointer = Nat_big_num.of_string "17592186040320" (*"0xffffffff000"*) in
-  let initial_GPR1_stack_pointer_value =
-    Sail_impl_base.register_value_of_integer 64 0 Sail_impl_base.D_increasing initial_GPR1_stack_pointer in
-  (* ELF says we need an initial zero doubleword there *)
-  let initial_stack_data =
-    (* the code actually uses the stack, both above and below, so we map a bit more memory*)
-    (* this is a fairly big but arbitrary chunk *)
-    (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in
-        [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *)
-    (* this is the stack memory that test 1938 actually uses *)
-    [ ("initial_stack_data1", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128),
-       Lem_list.replicate 8 0 );
-      ("initial_stack_data2", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 8),
-       Lem_list.replicate 8  0 );
-      ("initial_stack_data3", Nat_big_num.add initial_GPR1_stack_pointer (Nat_big_num.of_int 16),
-       Lem_list.replicate 8  0 )] in
-  
-  (* read TOC from the second field of the function descriptor pointed to by e_entry*)
-  let initial_GPR2_TOC =
-    Sail_impl_base.register_value_of_address
-      (Sail_impl_base.address_of_byte_list
-         (List.map (fun b -> match b with Some b -> b | None -> failwith "Address had undefined")
-             (List.map byte_of_byte_lifted
-                (read_mem all_data_memory
-                   (Nat_big_num.add (Nat_big_num.of_int 8) e_entry) 8))))
-      Sail_impl_base.D_increasing in
-  (* these initial register values are all mandated to be zero, but that's handled by the generic zeroing below
-      let initial_GPR3_argc = (Nat_big_num.of_int 0) in
-      let initial_GPR4_argv = (Nat_big_num.of_int 0) in
-      let initial_GPR5_envp = (Nat_big_num.of_int 0) in
-      let initial_FPSCR = (Nat_big_num.of_int 0) in
-  *)
-  let initial_register_abi_data : (string * Sail_impl_base.register_value) list =
-    [ ("GPR1", initial_GPR1_stack_pointer_value);
-      ("GPR2", initial_GPR2_TOC);
-  (*
-    ("GPR3", initial_GPR3_argc);
-    ("GPR4", initial_GPR4_argv);
-    ("GPR5", initial_GPR5_envp);
-    ("FPSCR", initial_FPSCR);
-    *)
-    ] in
-
-  (initial_stack_data, initial_register_abi_data)
-
-
-let aarch64_reg bit_count name = (name, (D_decreasing, bit_count, bit_count - 1))
-
-let aarch64_PC_data = [aarch64_reg 64 "_PC"]
-
-(* most of the PSTATE fields are aliases to other registers so they
-   don't appear here *)
-let aarch64_PSTATE_data  = [
-  aarch64_reg 1 "PSTATE_nRW";
-  aarch64_reg 1 "PSTATE_E";
-  aarch64_reg 5 "PSTATE_M";
-]
-
-let aarch64_general_purpose_registers_data = [
-  aarch64_reg 64 "R0";
-  aarch64_reg 64 "R1";
-  aarch64_reg 64 "R2";
-  aarch64_reg 64 "R3";
-  aarch64_reg 64 "R4";
-  aarch64_reg 64 "R5";
-  aarch64_reg 64 "R6";
-  aarch64_reg 64 "R7";
-  aarch64_reg 64 "R8";
-  aarch64_reg 64 "R9";
-  aarch64_reg 64 "R10";
-  aarch64_reg 64 "R11";
-  aarch64_reg 64 "R12";
-  aarch64_reg 64 "R13";
-  aarch64_reg 64 "R14";
-  aarch64_reg 64 "R15";
-  aarch64_reg 64 "R16";
-  aarch64_reg 64 "R17";
-  aarch64_reg 64 "R18";
-  aarch64_reg 64 "R19";
-  aarch64_reg 64 "R20";
-  aarch64_reg 64 "R21";
-  aarch64_reg 64 "R22";
-  aarch64_reg 64 "R23";
-  aarch64_reg 64 "R24";
-  aarch64_reg 64 "R25";
-  aarch64_reg 64 "R26";
-  aarch64_reg 64 "R27";
-  aarch64_reg 64 "R28";
-  aarch64_reg 64 "R29";
-  aarch64_reg 64 "R30";
-]
-
-let aarch64_SIMD_registers_data = [
-  aarch64_reg 128 "V0";
-  aarch64_reg 128 "V1";
-  aarch64_reg 128 "V2";
-  aarch64_reg 128 "V3";
-  aarch64_reg 128 "V4";
-  aarch64_reg 128 "V5";
-  aarch64_reg 128 "V6";
-  aarch64_reg 128 "V7";
-  aarch64_reg 128 "V8";
-  aarch64_reg 128 "V9";
-  aarch64_reg 128 "V10";
-  aarch64_reg 128 "V11";
-  aarch64_reg 128 "V12";
-  aarch64_reg 128 "V13";
-  aarch64_reg 128 "V14";
-  aarch64_reg 128 "V15";
-  aarch64_reg 128 "V16";
-  aarch64_reg 128 "V17";
-  aarch64_reg 128 "V18";
-  aarch64_reg 128 "V19";
-  aarch64_reg 128 "V20";
-  aarch64_reg 128 "V21";
-  aarch64_reg 128 "V22";
-  aarch64_reg 128 "V23";
-  aarch64_reg 128 "V24";
-  aarch64_reg 128 "V25";
-  aarch64_reg 128 "V26";
-  aarch64_reg 128 "V27";
-  aarch64_reg 128 "V28";
-  aarch64_reg 128 "V29";
-  aarch64_reg 128 "V30";
-  aarch64_reg 128 "V31";
-]
-
-let aarch64_special_purpose_registers_data = [
-  aarch64_reg 32 "CurrentEL";
-  aarch64_reg 32 "DAIF";
-  aarch64_reg 32 "NZCV";
-  aarch64_reg 64 "SP_EL0";
-  aarch64_reg 64 "SP_EL1";
-  aarch64_reg 64 "SP_EL2";
-  aarch64_reg 64 "SP_EL3";
-  aarch64_reg 32 "SPSel";
-  aarch64_reg 32 "SPSR_EL1";
-  aarch64_reg 32 "SPSR_EL2";
-  aarch64_reg 32 "SPSR_EL3";
-  aarch64_reg 64 "ELR_EL1";
-  aarch64_reg 64 "ELR_EL2";
-  aarch64_reg 64 "ELR_EL3";
-]
-
-let aarch64_general_system_control_registers_data = [
-  aarch64_reg 64 "HCR_EL2";
-  aarch64_reg 64 "ID_AA64MMFR0_EL1";
-  aarch64_reg 64 "RVBAR_EL1";
-  aarch64_reg 64 "RVBAR_EL2";
-  aarch64_reg 64 "RVBAR_EL3";
-  aarch64_reg 32 "SCR_EL3";
-  aarch64_reg 32 "SCTLR_EL1";
-  aarch64_reg 32 "SCTLR_EL2";
-  aarch64_reg 32 "SCTLR_EL3";
-  aarch64_reg 64 "TCR_EL1";
-  aarch64_reg 32 "TCR_EL2";
-  aarch64_reg 32 "TCR_EL3";
-]
-
-let aarch64_debug_registers_data = [
-  aarch64_reg 32 "DBGPRCR_EL1";
-  aarch64_reg 32 "OSDLR_EL1";
-]
-
-let aarch64_performance_monitors_registers_data = []
-let aarch64_generic_timer_registers_data = []
-let aarch64_generic_interrupt_controller_CPU_interface_registers_data = []
-
-let aarch64_external_debug_registers_data = [
-  aarch64_reg 32 "EDSCR";
-]
-
-let aarch32_general_system_control_registers_data = [
-  aarch64_reg 32 "SCR";
-]
-
-let aarch32_debug_registers_data = [
-  aarch64_reg 32 "DBGOSDLR";
-  aarch64_reg 32 "DBGPRCR";
-]
-
-let aarch64_register_data_all =
-  aarch64_PC_data @
-  aarch64_PSTATE_data @
-  aarch64_general_purpose_registers_data @
-  aarch64_SIMD_registers_data @
-  aarch64_special_purpose_registers_data @
-  aarch64_general_system_control_registers_data @
-  aarch64_debug_registers_data @
-  aarch64_performance_monitors_registers_data @
-  aarch64_generic_timer_registers_data @
-  aarch64_generic_interrupt_controller_CPU_interface_registers_data @
-  aarch64_external_debug_registers_data @
-  aarch32_general_system_control_registers_data @
-  aarch32_debug_registers_data
-
-let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory =
-  let (reg_SP_EL0_direction, reg_SP_EL0_width, reg_SP_EL0_initial_index) =
-    List.assoc "SP_EL0" aarch64_register_data_all in
-  
-  (* we compiled a small program that prints out SP and run it a few
-      times on the Nexus9, these are the results:
-      0x0000007fe7f903e0
-      0x0000007fdcdbf3f0
-      0x0000007fcbe1ba90
-      0x0000007fcf378280
-      0x0000007fdd54b8d0
-      0x0000007fd961bc10
-      0x0000007ff3be6350
-      0x0000007fd6bf6ef0
-      0x0000007fff7676f0
-      0x0000007ff2c34560 *)
-  let initial_SP_EL0 = Nat_big_num.of_string "549739036672" (*"0x0000007fff000000"*) in
-  let initial_SP_EL0_value =
-    Sail_impl_base.register_value_of_integer
-      reg_SP_EL0_width
-      reg_SP_EL0_initial_index
-      reg_SP_EL0_direction
-      initial_SP_EL0
-  in
-
-  (* ELF says we need an initial zero doubleword there *)
-  (* the code actually uses the stack, both above and below, so we map a bit more memory*)
-  let initial_stack_data =
-    (* this is a fairly big but arbitrary chunk: *)
-    (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in
-        [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *)
-    
-    [ ("initial_stack_data1", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 16),  Lem_list.replicate 8 0);
-      ("initial_stack_data2", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 8),   Lem_list.replicate 8 0)
-    ]
-  in
-
-  let initial_register_abi_data : (string * Sail_impl_base.register_value) list =
-    [("SP_EL0", initial_SP_EL0_value)]
-  in
-
-  (initial_stack_data, initial_register_abi_data)
-*)
 
 let mips_register_data_all =  [
   (*Pseudo registers*)
   ("PC", (D_decreasing, 64, 63));
   ("branchPending", (D_decreasing, 1, 0));
   ("inBranchDelay", (D_decreasing, 1, 0));
+  ("inCCallDelay", (D_decreasing, 1, 0));
   ("delayedPC", (D_decreasing, 64, 63));
   ("nextPC", (D_decreasing, 64, 63));
   (* General purpose registers *)
@@ -748,50 +386,6 @@ let initial_system_state_of_elf_file name =
       let (isa_defs, isa_memory_access, isa_externs, isa_model, model_reg_d, startaddr,
            initial_stack_data, initial_register_abi_data, register_data_all) =
         match Nat_big_num.to_int e_machine with
-(*        | 21  (* EM_PPC64 *) ->
-          let startaddr =
-            let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in
-            match Abi_power64.abi_power64_compute_program_entry_point segments e_entry with
-            | Error.Fail s -> failwith "Failed computing entry point"
-            | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s)
-          in
-          let (initial_stack_data, initial_register_abi_data) =
-            initial_stack_and_reg_data_of_PPC_elf_file e_entry !data_mem in
-
-            (Power.defs,
-             (Power_extras.read_memory_functions,Power_extras.memory_writes,[],[],Power_extras.barrier_functions),
-             Power_extras.power_externs,
-             PPC,
-             D_increasing,
-             startaddr,
-             initial_stack_data,
-             initial_register_abi_data,
-             ppc_register_data_all)
-
-        | 183 (* EM_AARCH64 *) ->
-          let startaddr =
-            let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in
-            match Abi_aarch64_le.abi_aarch64_le_compute_program_entry_point segments e_entry with
-            | Error.Fail s -> failwith "Failed computing entry point"
-            | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s)
-          in
-          
-          let (initial_stack_data, initial_register_abi_data) =
-            initial_stack_and_reg_data_of_AAarch64_elf_file e_entry !data_mem in
-          
-          (ArmV8.defs,
-           (ArmV8_extras.aArch64_read_memory_functions,
-            ArmV8_extras.aArch64_memory_writes,
-	    ArmV8_extras.aArch64_memory_eas,
-	    ArmV8_extras.aArch64_memory_vals,
-            ArmV8_extras.aArch64_barrier_functions),
-           [],
-           AArch64,
-           D_decreasing,
-           startaddr,
-           initial_stack_data,
-           initial_register_abi_data,
-           aarch64_register_data_all) *)
         | 8 (* EM_MIPS *) ->
           let startaddr =
             let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
@@ -888,50 +482,6 @@ let initial_system_state_of_elf_file name =
       in
 
 
-      (* Now we examine the rest of the data memory,
-         removing the footprint of the symbols and chunking it into aligned chunks *)
-      
-      let rec remove_symbols_from_data_memory data_mem symbols =
-        match symbols with
-        | [] -> data_mem
-        | (name,address,size,bs)::symbols' ->
-          let data_mem' =
-            Mem.filter
-              (fun a v ->
-                 not (Nat_big_num.greater_equal a address &&
-                      Nat_big_num.less a (Nat_big_num.add (Nat_big_num.of_int (List.length bs)) address)))
-              data_mem in
-          remove_symbols_from_data_memory data_mem' symbols' in
-
-      let trimmed_data_memory : (Nat_big_num.num * memory_byte) list =
-        Mem.bindings (remove_symbols_from_data_memory !data_mem symbol_table) in
-
-      (* make sure that's ordered increasingly.... *)
-      let trimmed_data_memory =
-        List.sort (fun (a,b) (a',b') -> Nat_big_num.compare a a') trimmed_data_memory in
-
-      let aligned a n =  (* a mod n = 0 *)
-        let n_big = Nat_big_num.of_int n in
-        Nat_big_num.equal (Nat_big_num.modulus a n_big) ((Nat_big_num.of_int 0)) in
-
-      let isplus a' a n =   (* a' = a+n *)
-        Nat_big_num.equal a' (Nat_big_num.add (Nat_big_num.of_int n) a) in
-
-      let rec chunk_data_memory dm =
-        match dm with
-        | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::(a4,b4)::(a5,b5)::(a6,b6)::(a7,b7)::dm'  when
-            (aligned a0 8 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3 &&
-             isplus a4 a0 4 && isplus a5 a0 5 && isplus a6 a0 6 && isplus a7 a0 7) ->
-          (a0,8,[b0;b1;b2;b3;b4;b5;b6;b7]) :: chunk_data_memory dm'
-        | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::dm' when
-            (aligned a0 4 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3) ->
-              (a0,4,[b0;b1;b2;b3]) :: chunk_data_memory dm'
-        | (a0,b0)::(a1,b1)::dm' when
-            (aligned a0 2 && isplus a1 a0 1) ->
-              (a0,2,[b0;b1]) :: chunk_data_memory dm'
-        | (a0,b0)::dm' ->
-            (a0,1,[b0]):: chunk_data_memory dm'
-        | [] -> [] in
 
       let initial_register_state =
         fun rbn ->
@@ -1021,68 +571,10 @@ let stop_condition_met model instr =
       true
     | _ -> false)
 
-let is_branch model instruction =
-  let (name,_,_) = instruction in
-  match (model , name) with
-  | (PPC, "B") -> true
-  | (PPC, "Bc") -> true
-  | (PPC, "Bclr") -> true
-  | (PPC, "Bcctr") -> true
-  | (PPC, _) -> false
-  | (AArch64, "BranchImmediate") -> true
-  | (AArch64, "BranchConditional") -> true
-  | (AArch64, "CompareAndBranch") -> true
-  | (AArch64, "TestBitAndBranch") -> true
-  | (AArch64, "BranchRegister") -> true
-  | (AArch64, _) -> false
-  | (MIPS, _) -> false (*todo,fill this in*)
-
 let option_int_of_option_integer i = match i with
   | Some i -> Some (Nat_big_num.to_int i)
   | None -> None
 
-let set_next_instruction_address model =
-  match model with
-  | PPC ->
-    let cia = Reg.find "CIA" !reg in
-    let cia_addr = address_of_register_value cia in
-    (match cia_addr with
-    | Some cia_addr ->
-      let nia_addr = add_address_nat cia_addr 4 in 
-      let nia = register_value_of_address nia_addr Sail_impl_base.D_increasing in
-      reg := Reg.add "NIA" nia !reg
-    | _ -> failwith "CIA address contains unknown or undefined")
-  | AArch64 ->
-    let pc = Reg.find "_PC" !reg in
-    let pc_addr = address_of_register_value pc in
-    (match pc_addr with
-     | Some pc_addr ->
-       let n_addr = add_address_nat pc_addr 4 in
-       let n_pc = register_value_of_address n_addr D_decreasing in
-       reg := Reg.add "_PC" n_pc !reg
-     | _ -> failwith "_PC address contains unknown or undefined")
-  | MIPS -> 
-    let pc_addr       = address_of_register_value (Reg.find "PC" !reg) in
-    let branchPending = integer_of_register_value (Reg.find "branchPending" !reg) in
-    (match (pc_addr, option_int_of_option_integer branchPending) with
-     | (Some pc_val, Some 0) -> 
-       (* normal -- increment PC *)
-       let n_addr = add_address_nat pc_val 4 in
-       let n_pc = register_value_of_address n_addr D_decreasing in
-       begin
-         reg := Reg.add "nextPC" n_pc !reg;
-         reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
-       end
-     | (Some pc_val, Some 1) -> 
-       (* delay slot -- branch to delayed PC and clear branchPending *)
-       begin 
-         reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
-         reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg;
-         reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
-         reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
-       end
-     | (_, _) -> errorf "PC address contains unknown or undefined"; exit 1)
-
 let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
 
 let get_addr_trans_regs _ =
@@ -1192,68 +684,10 @@ let rec write_events = function
      | _ -> failwith "Only register write events expected");
     write_events events
 
-let fetch_instruction_opcode_and_update_ia model addr_trans =
-  match model with
-  | PPC ->
-    let cia = Reg.find "CIA" !reg in
-    let cia_addr = address_of_register_value cia in
-    (match cia_addr with
-     | Some cia_addr ->
-       let cia_a = integer_of_address cia_addr in
-       let opcode = (get_opcode cia_a) in
-       begin
-         reg := Reg.add "CIA" (Reg.find "NIA" !reg) !reg;
-         Opcode opcode
-       end
-     | None -> failwith "CIA address contains unknown or undefined")
-  | AArch64 ->
-    let pc = Reg.find "_PC" !reg in
-    let pc_addr = address_of_register_value pc in
-    (match pc_addr with
-     | Some pc_addr ->
-       let pc_a = integer_of_address pc_addr in
-       let opcode = (get_opcode pc_a) in
-       Opcode opcode
-     | None -> failwith "_PC address contains unknown or undefined")
-  | MIPS -> 
-    begin
-    reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
-    let nextPC  = Reg.find "nextPC" !reg in
-    let pc_addr = address_of_register_value nextPC in
-    (*let unused = interactf "PC: %s\n" (Printing_functions.register_value_to_string nextPC) in*)
-    (match pc_addr with
-    | Some pc_addr ->
-      let pc_a = match addr_trans (get_addr_trans_regs ()) pc_addr with
-        | Some a, Some events -> write_events (List.rev events); integer_of_address a
-        | Some a, None -> integer_of_address a
-        | None, Some events ->
-          write_events (List.rev events);
-          let nextPC  = Reg.find "nextPC" !reg in
-          reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
-          let pc_addr = address_of_register_value nextPC in
-          (match pc_addr with
-           | Some pc_addr ->
-             (match addr_trans (get_addr_trans_regs ()) pc_addr with
-              | Some a, Some events -> write_events (List.rev events); integer_of_address a
-              | Some a, None -> integer_of_address a
-              | None, _ -> failwith "Address translation failed twice")
-           | None -> failwith "no nextPc address")
-        | _ -> failwith "No address and no events from translate address"
-      in
-      let opcode = (get_opcode pc_a) in
-      begin
-        reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
-        Opcode opcode
-      end
-     | None -> errorf "nextPC contains unknown or undefined"; exit 1)
-    end
-  |  _ -> assert false
-
 let get_pc_address = function
   | MIPS -> Reg.find "PC" !reg
   | PPC  -> Reg.find "CIA" !reg
   | AArch64 -> Reg.find "_PC" !reg
-        
 
 let option_int_of_reg str =
   option_int_of_option_integer (integer_of_register_value (Reg.find str !reg))
@@ -1283,6 +717,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
             let npc_addr = add_address_nat pc_val 4 in
             let npc_reg = register_value_of_address npc_addr Sail_impl_base.D_decreasing in
             reg := Reg.add "nextPC" npc_reg !reg;
+            reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
           | Some 1 ->
             reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
             reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg;
@@ -1290,12 +725,14 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
           let opcode = Opcode (get_opcode pc) in
           let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
             | Instr(instruction,istate) ->
+               let instruction = interp_value_to_instr_external context instruction in
               interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
               (instruction,istate)
             | Decode_error d ->
               (match d with
-              | Interp_interface.Unsupported_instruction_error instr ->
-                errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
+              | Interp_interface.Unsupported_instruction_error instruction ->
+               let instruction = interp_value_to_instr_external context instruction in
+                errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instruction)
               | Interp_interface.Not_an_instruction_error op ->
                 (match op with
                 | Opcode bytes ->
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index cd2e7312..6dca80f4 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -124,375 +124,13 @@ let register_state_zero register_data rbn : register_value =
   in register_value_zeros dir width start_index
 
 type model = PPC | AArch64 | MIPS
-(*
-let ppc_register_data_all =  [
-  (*Pseudo registers*)
-  ("CIA",   (D_increasing, 64, 0));
-  ("NIA",   (D_increasing, 64, 0));
-  ("mode64bit", (D_increasing, 1, 0));
-  ("bigendianmode", (D_increasing, 1, 0));
-  (* special registers *)
-  ("CR",    (D_increasing, 32, 32));
-  ("CTR",   (D_increasing, 64, 0 ));
-  ("LR",    (D_increasing, 64, 0 ));
-  ("XER",   (D_increasing, 64, 0 ));
-  ("VRSAVE",(D_increasing, 32, 32));
-  ("FPSCR", (D_increasing, 64, 0 ));
-  ("VSCR",  (D_increasing, 32, 96));
-
-  (* general purpose registers *)
-  ("GPR0",  (D_increasing, 64, 0 ));
-  ("GPR1",  (D_increasing, 64, 0 ));
-  ("GPR2",  (D_increasing, 64, 0 ));
-  ("GPR3",  (D_increasing, 64, 0 ));
-  ("GPR4",  (D_increasing, 64, 0 ));
-  ("GPR5",  (D_increasing, 64, 0 ));
-  ("GPR6",  (D_increasing, 64, 0 ));
-  ("GPR7",  (D_increasing, 64, 0 ));
-  ("GPR8",  (D_increasing, 64, 0 ));
-  ("GPR9",  (D_increasing, 64, 0 ));
-  ("GPR10", (D_increasing, 64, 0 ));
-  ("GPR11", (D_increasing, 64, 0 ));
-  ("GPR12", (D_increasing, 64, 0 ));
-  ("GPR13", (D_increasing, 64, 0 ));
-  ("GPR14", (D_increasing, 64, 0 ));
-  ("GPR15", (D_increasing, 64, 0 ));
-  ("GPR16", (D_increasing, 64, 0 ));
-  ("GPR17", (D_increasing, 64, 0 ));
-  ("GPR18", (D_increasing, 64, 0 ));
-  ("GPR19", (D_increasing, 64, 0 ));
-  ("GPR20", (D_increasing, 64, 0 ));
-  ("GPR21", (D_increasing, 64, 0 ));
-  ("GPR22", (D_increasing, 64, 0 ));
-  ("GPR23", (D_increasing, 64, 0 ));
-  ("GPR24", (D_increasing, 64, 0 ));
-  ("GPR25", (D_increasing, 64, 0 ));
-  ("GPR26", (D_increasing, 64, 0 ));
-  ("GPR27", (D_increasing, 64, 0 ));
-  ("GPR28", (D_increasing, 64, 0 ));
-  ("GPR29", (D_increasing, 64, 0 ));
-  ("GPR30", (D_increasing, 64, 0 ));
-  ("GPR31", (D_increasing, 64, 0 ));
-  (* vector registers *)
-  ("VR0",  (D_increasing, 128, 0 ));
-  ("VR1",  (D_increasing, 128, 0 ));
-  ("VR2",  (D_increasing, 128, 0 ));
-  ("VR3",  (D_increasing, 128, 0 ));
-  ("VR4",  (D_increasing, 128, 0 ));
-  ("VR5",  (D_increasing, 128, 0 ));
-  ("VR6",  (D_increasing, 128, 0 ));
-  ("VR7",  (D_increasing, 128, 0 ));
-  ("VR8",  (D_increasing, 128, 0 ));
-  ("VR9",  (D_increasing, 128, 0 ));
-  ("VR10", (D_increasing, 128, 0 ));
-  ("VR11", (D_increasing, 128, 0 ));
-  ("VR12", (D_increasing, 128, 0 ));
-  ("VR13", (D_increasing, 128, 0 ));
-  ("VR14", (D_increasing, 128, 0 ));
-  ("VR15", (D_increasing, 128, 0 ));
-  ("VR16", (D_increasing, 128, 0 ));
-  ("VR17", (D_increasing, 128, 0 ));
-  ("VR18", (D_increasing, 128, 0 ));
-  ("VR19", (D_increasing, 128, 0 ));
-  ("VR20", (D_increasing, 128, 0 ));
-  ("VR21", (D_increasing, 128, 0 ));
-  ("VR22", (D_increasing, 128, 0 ));
-  ("VR23", (D_increasing, 128, 0 ));
-  ("VR24", (D_increasing, 128, 0 ));
-  ("VR25", (D_increasing, 128, 0 ));
-  ("VR26", (D_increasing, 128, 0 ));
-  ("VR27", (D_increasing, 128, 0 ));
-  ("VR28", (D_increasing, 128, 0 ));
-  ("VR29", (D_increasing, 128, 0 ));
-  ("VR30", (D_increasing, 128, 0 ));
-  ("VR31", (D_increasing, 128, 0 ));
-  (* floating-point registers *)
-  ("FPR0",  (D_increasing, 64, 0 ));
-  ("FPR1",  (D_increasing, 64, 0 ));
-  ("FPR2",  (D_increasing, 64, 0 ));
-  ("FPR3",  (D_increasing, 64, 0 ));
-  ("FPR4",  (D_increasing, 64, 0 ));
-  ("FPR5",  (D_increasing, 64, 0 ));
-  ("FPR6",  (D_increasing, 64, 0 ));
-  ("FPR7",  (D_increasing, 64, 0 ));
-  ("FPR8",  (D_increasing, 64, 0 ));
-  ("FPR9",  (D_increasing, 64, 0 ));
-  ("FPR10", (D_increasing, 64, 0 ));
-  ("FPR11", (D_increasing, 64, 0 ));
-  ("FPR12", (D_increasing, 64, 0 ));
-  ("FPR13", (D_increasing, 64, 0 ));
-  ("FPR14", (D_increasing, 64, 0 ));
-  ("FPR15", (D_increasing, 64, 0 ));
-  ("FPR16", (D_increasing, 64, 0 ));
-  ("FPR17", (D_increasing, 64, 0 ));
-  ("FPR18", (D_increasing, 64, 0 ));
-  ("FPR19", (D_increasing, 64, 0 ));
-  ("FPR20", (D_increasing, 64, 0 ));
-  ("FPR21", (D_increasing, 64, 0 ));
-  ("FPR22", (D_increasing, 64, 0 ));
-  ("FPR23", (D_increasing, 64, 0 ));
-  ("FPR24", (D_increasing, 64, 0 ));
-  ("FPR25", (D_increasing, 64, 0 ));
-  ("FPR26", (D_increasing, 64, 0 ));
-  ("FPR27", (D_increasing, 64, 0 ));
-  ("FPR28", (D_increasing, 64, 0 ));
-  ("FPR29", (D_increasing, 64, 0 ));
-  ("FPR30", (D_increasing, 64, 0 ));
-  ("FPR31", (D_increasing, 64, 0 ));
-]
-
-let initial_stack_and_reg_data_of_PPC_elf_file e_entry all_data_memory =
-  (* set up initial registers, per 3.4.1 of 64-bit PowerPC ELF Application Binary Interface Supplement 1.9 *)
-
-  let auxiliary_vector_space = Nat_big_num.of_string "17592186042368" (*"0xffffffff800"*) in
-  (* notionally there should be at least an AT_NULL auxiliary vector entry there, but our examples will never read it *)
-
-  (* take start of stack roughly where running gdb on hello5 on bim says it is*)
-  let initial_GPR1_stack_pointer = Nat_big_num.of_string "17592186040320" (*"0xffffffff000"*) in
-  let initial_GPR1_stack_pointer_value =
-    Sail_impl_base.register_value_of_integer 64 0 Sail_impl_base.D_increasing initial_GPR1_stack_pointer in
-  (* ELF says we need an initial zero doubleword there *)
-  let initial_stack_data =
-    (* the code actually uses the stack, both above and below, so we map a bit more memory*)
-    (* this is a fairly big but arbitrary chunk *)
-    (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in
-        [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *)
-    (* this is the stack memory that test 1938 actually uses *)
-    [ ("initial_stack_data1", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128),
-       Lem_list.replicate 8 0 );
-      ("initial_stack_data2", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 8),
-       Lem_list.replicate 8  0 );
-      ("initial_stack_data3", Nat_big_num.add initial_GPR1_stack_pointer (Nat_big_num.of_int 16),
-       Lem_list.replicate 8  0 )] in
-  
-  (* read TOC from the second field of the function descriptor pointed to by e_entry*)
-  let initial_GPR2_TOC =
-    Sail_impl_base.register_value_of_address
-      (Sail_impl_base.address_of_byte_list
-         (List.map (fun b -> match b with Some b -> b | None -> failwith "Address had undefined")
-             (List.map byte_of_byte_lifted
-                (read_mem all_data_memory
-                   (Nat_big_num.add (Nat_big_num.of_int 8) e_entry) 8))))
-      Sail_impl_base.D_increasing in
-  (* these initial register values are all mandated to be zero, but that's handled by the generic zeroing below
-      let initial_GPR3_argc = (Nat_big_num.of_int 0) in
-      let initial_GPR4_argv = (Nat_big_num.of_int 0) in
-      let initial_GPR5_envp = (Nat_big_num.of_int 0) in
-      let initial_FPSCR = (Nat_big_num.of_int 0) in
-  *)
-  let initial_register_abi_data : (string * Sail_impl_base.register_value) list =
-    [ ("GPR1", initial_GPR1_stack_pointer_value);
-      ("GPR2", initial_GPR2_TOC);
-  (*
-    ("GPR3", initial_GPR3_argc);
-    ("GPR4", initial_GPR4_argv);
-    ("GPR5", initial_GPR5_envp);
-    ("FPSCR", initial_FPSCR);
-    *)
-    ] in
-
-  (initial_stack_data, initial_register_abi_data)
-
-
-let aarch64_reg bit_count name = (name, (D_decreasing, bit_count, bit_count - 1))
-
-let aarch64_PC_data = [aarch64_reg 64 "_PC"]
-
-(* most of the PSTATE fields are aliases to other registers so they
-   don't appear here *)
-let aarch64_PSTATE_data  = [
-  aarch64_reg 1 "PSTATE_nRW";
-  aarch64_reg 1 "PSTATE_E";
-  aarch64_reg 5 "PSTATE_M";
-]
-
-let aarch64_general_purpose_registers_data = [
-  aarch64_reg 64 "R0";
-  aarch64_reg 64 "R1";
-  aarch64_reg 64 "R2";
-  aarch64_reg 64 "R3";
-  aarch64_reg 64 "R4";
-  aarch64_reg 64 "R5";
-  aarch64_reg 64 "R6";
-  aarch64_reg 64 "R7";
-  aarch64_reg 64 "R8";
-  aarch64_reg 64 "R9";
-  aarch64_reg 64 "R10";
-  aarch64_reg 64 "R11";
-  aarch64_reg 64 "R12";
-  aarch64_reg 64 "R13";
-  aarch64_reg 64 "R14";
-  aarch64_reg 64 "R15";
-  aarch64_reg 64 "R16";
-  aarch64_reg 64 "R17";
-  aarch64_reg 64 "R18";
-  aarch64_reg 64 "R19";
-  aarch64_reg 64 "R20";
-  aarch64_reg 64 "R21";
-  aarch64_reg 64 "R22";
-  aarch64_reg 64 "R23";
-  aarch64_reg 64 "R24";
-  aarch64_reg 64 "R25";
-  aarch64_reg 64 "R26";
-  aarch64_reg 64 "R27";
-  aarch64_reg 64 "R28";
-  aarch64_reg 64 "R29";
-  aarch64_reg 64 "R30";
-]
-
-let aarch64_SIMD_registers_data = [
-  aarch64_reg 128 "V0";
-  aarch64_reg 128 "V1";
-  aarch64_reg 128 "V2";
-  aarch64_reg 128 "V3";
-  aarch64_reg 128 "V4";
-  aarch64_reg 128 "V5";
-  aarch64_reg 128 "V6";
-  aarch64_reg 128 "V7";
-  aarch64_reg 128 "V8";
-  aarch64_reg 128 "V9";
-  aarch64_reg 128 "V10";
-  aarch64_reg 128 "V11";
-  aarch64_reg 128 "V12";
-  aarch64_reg 128 "V13";
-  aarch64_reg 128 "V14";
-  aarch64_reg 128 "V15";
-  aarch64_reg 128 "V16";
-  aarch64_reg 128 "V17";
-  aarch64_reg 128 "V18";
-  aarch64_reg 128 "V19";
-  aarch64_reg 128 "V20";
-  aarch64_reg 128 "V21";
-  aarch64_reg 128 "V22";
-  aarch64_reg 128 "V23";
-  aarch64_reg 128 "V24";
-  aarch64_reg 128 "V25";
-  aarch64_reg 128 "V26";
-  aarch64_reg 128 "V27";
-  aarch64_reg 128 "V28";
-  aarch64_reg 128 "V29";
-  aarch64_reg 128 "V30";
-  aarch64_reg 128 "V31";
-]
-
-let aarch64_special_purpose_registers_data = [
-  aarch64_reg 32 "CurrentEL";
-  aarch64_reg 32 "DAIF";
-  aarch64_reg 32 "NZCV";
-  aarch64_reg 64 "SP_EL0";
-  aarch64_reg 64 "SP_EL1";
-  aarch64_reg 64 "SP_EL2";
-  aarch64_reg 64 "SP_EL3";
-  aarch64_reg 32 "SPSel";
-  aarch64_reg 32 "SPSR_EL1";
-  aarch64_reg 32 "SPSR_EL2";
-  aarch64_reg 32 "SPSR_EL3";
-  aarch64_reg 64 "ELR_EL1";
-  aarch64_reg 64 "ELR_EL2";
-  aarch64_reg 64 "ELR_EL3";
-]
-
-let aarch64_general_system_control_registers_data = [
-  aarch64_reg 64 "HCR_EL2";
-  aarch64_reg 64 "ID_AA64MMFR0_EL1";
-  aarch64_reg 64 "RVBAR_EL1";
-  aarch64_reg 64 "RVBAR_EL2";
-  aarch64_reg 64 "RVBAR_EL3";
-  aarch64_reg 32 "SCR_EL3";
-  aarch64_reg 32 "SCTLR_EL1";
-  aarch64_reg 32 "SCTLR_EL2";
-  aarch64_reg 32 "SCTLR_EL3";
-  aarch64_reg 64 "TCR_EL1";
-  aarch64_reg 32 "TCR_EL2";
-  aarch64_reg 32 "TCR_EL3";
-]
-
-let aarch64_debug_registers_data = [
-  aarch64_reg 32 "DBGPRCR_EL1";
-  aarch64_reg 32 "OSDLR_EL1";
-]
-
-let aarch64_performance_monitors_registers_data = []
-let aarch64_generic_timer_registers_data = []
-let aarch64_generic_interrupt_controller_CPU_interface_registers_data = []
-
-let aarch64_external_debug_registers_data = [
-  aarch64_reg 32 "EDSCR";
-]
-
-let aarch32_general_system_control_registers_data = [
-  aarch64_reg 32 "SCR";
-]
-
-let aarch32_debug_registers_data = [
-  aarch64_reg 32 "DBGOSDLR";
-  aarch64_reg 32 "DBGPRCR";
-]
-
-let aarch64_register_data_all =
-  aarch64_PC_data @
-  aarch64_PSTATE_data @
-  aarch64_general_purpose_registers_data @
-  aarch64_SIMD_registers_data @
-  aarch64_special_purpose_registers_data @
-  aarch64_general_system_control_registers_data @
-  aarch64_debug_registers_data @
-  aarch64_performance_monitors_registers_data @
-  aarch64_generic_timer_registers_data @
-  aarch64_generic_interrupt_controller_CPU_interface_registers_data @
-  aarch64_external_debug_registers_data @
-  aarch32_general_system_control_registers_data @
-  aarch32_debug_registers_data
-
-let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory =
-  let (reg_SP_EL0_direction, reg_SP_EL0_width, reg_SP_EL0_initial_index) =
-    List.assoc "SP_EL0" aarch64_register_data_all in
-  
-  (* we compiled a small program that prints out SP and run it a few
-      times on the Nexus9, these are the results:
-      0x0000007fe7f903e0
-      0x0000007fdcdbf3f0
-      0x0000007fcbe1ba90
-      0x0000007fcf378280
-      0x0000007fdd54b8d0
-      0x0000007fd961bc10
-      0x0000007ff3be6350
-      0x0000007fd6bf6ef0
-      0x0000007fff7676f0
-      0x0000007ff2c34560 *)
-  let initial_SP_EL0 = Nat_big_num.of_string "549739036672" (*"0x0000007fff000000"*) in
-  let initial_SP_EL0_value =
-    Sail_impl_base.register_value_of_integer
-      reg_SP_EL0_width
-      reg_SP_EL0_initial_index
-      reg_SP_EL0_direction
-      initial_SP_EL0
-  in
-
-  (* ELF says we need an initial zero doubleword there *)
-  (* the code actually uses the stack, both above and below, so we map a bit more memory*)
-  let initial_stack_data =
-    (* this is a fairly big but arbitrary chunk: *)
-    (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in
-        [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *)
-    
-    [ ("initial_stack_data1", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 16),  Lem_list.replicate 8 0);
-      ("initial_stack_data2", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 8),   Lem_list.replicate 8 0)
-    ]
-  in
-
-  let initial_register_abi_data : (string * Sail_impl_base.register_value) list =
-    [("SP_EL0", initial_SP_EL0_value)]
-  in
-
-  (initial_stack_data, initial_register_abi_data)
-*)
 
 let mips_register_data_all =  [
   (*Pseudo registers*)
   ("PC", (D_decreasing, 64, 63));
   ("branchPending", (D_decreasing, 1, 0));
   ("inBranchDelay", (D_decreasing, 1, 0));
+  ("inCCallDelay", (D_decreasing, 1, 0));
   ("delayedPC", (D_decreasing, 64, 63));
   ("nextPC", (D_decreasing, 64, 63));
   (* General purpose registers *)
@@ -665,7 +303,7 @@ let cheri_register_data_all = mips_register_data_all @ [
 
 let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
   let initial_stack_data = [] in 
-  let initial_cap_val_int = Nat_big_num.of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *)
+  let initial_cap_val_int = Nat_big_num.of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *)
   let initial_cap_val_reg = Sail_impl_base.register_value_of_integer 129 128 D_decreasing  initial_cap_val_int in
   let initial_register_abi_data : (string * Sail_impl_base.register_value) list = [
     ("CP0Status", Sail_impl_base.register_value_of_integer 32 31 D_decreasing (Nat_big_num.of_string "0x00400000"));
@@ -748,50 +386,6 @@ let initial_system_state_of_elf_file name =
       let (isa_defs, isa_memory_access, isa_externs, isa_model, model_reg_d, startaddr,
            initial_stack_data, initial_register_abi_data, register_data_all) =
         match Nat_big_num.to_int e_machine with
-(*        | 21  (* EM_PPC64 *) ->
-          let startaddr =
-            let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in
-            match Abi_power64.abi_power64_compute_program_entry_point segments e_entry with
-            | Error.Fail s -> failwith "Failed computing entry point"
-            | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s)
-          in
-          let (initial_stack_data, initial_register_abi_data) =
-            initial_stack_and_reg_data_of_PPC_elf_file e_entry !data_mem in
-
-            (Power.defs,
-             (Power_extras.read_memory_functions,Power_extras.memory_writes,[],[],Power_extras.barrier_functions),
-             Power_extras.power_externs,
-             PPC,
-             D_increasing,
-             startaddr,
-             initial_stack_data,
-             initial_register_abi_data,
-             ppc_register_data_all)
-
-        | 183 (* EM_AARCH64 *) ->
-          let startaddr =
-            let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in
-            match Abi_aarch64_le.abi_aarch64_le_compute_program_entry_point segments e_entry with
-            | Error.Fail s -> failwith "Failed computing entry point"
-            | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s)
-          in
-          
-          let (initial_stack_data, initial_register_abi_data) =
-            initial_stack_and_reg_data_of_AAarch64_elf_file e_entry !data_mem in
-          
-          (ArmV8.defs,
-           (ArmV8_extras.aArch64_read_memory_functions,
-            ArmV8_extras.aArch64_memory_writes,
-	    ArmV8_extras.aArch64_memory_eas,
-	    ArmV8_extras.aArch64_memory_vals,
-            ArmV8_extras.aArch64_barrier_functions),
-           [],
-           AArch64,
-           D_decreasing,
-           startaddr,
-           initial_stack_data,
-           initial_register_abi_data,
-           aarch64_register_data_all) *)
         | 8 (* EM_MIPS *) ->
           let startaddr =
             let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
@@ -887,52 +481,6 @@ let initial_system_state_of_elf_file name =
         List.map (fun (name, (binding, fp)) -> (fp, name)) (StringMap.bindings map)
       in
 
-
-      (* Now we examine the rest of the data memory,
-         removing the footprint of the symbols and chunking it into aligned chunks *)
-      
-      let rec remove_symbols_from_data_memory data_mem symbols =
-        match symbols with
-        | [] -> data_mem
-        | (name,address,size,bs)::symbols' ->
-          let data_mem' =
-            Mem.filter
-              (fun a v ->
-                 not (Nat_big_num.greater_equal a address &&
-                      Nat_big_num.less a (Nat_big_num.add (Nat_big_num.of_int (List.length bs)) address)))
-              data_mem in
-          remove_symbols_from_data_memory data_mem' symbols' in
-
-      let trimmed_data_memory : (Nat_big_num.num * memory_byte) list =
-        Mem.bindings (remove_symbols_from_data_memory !data_mem symbol_table) in
-
-      (* make sure that's ordered increasingly.... *)
-      let trimmed_data_memory =
-        List.sort (fun (a,b) (a',b') -> Nat_big_num.compare a a') trimmed_data_memory in
-
-      let aligned a n =  (* a mod n = 0 *)
-        let n_big = Nat_big_num.of_int n in
-        Nat_big_num.equal (Nat_big_num.modulus a n_big) ((Nat_big_num.of_int 0)) in
-
-      let isplus a' a n =   (* a' = a+n *)
-        Nat_big_num.equal a' (Nat_big_num.add (Nat_big_num.of_int n) a) in
-
-      let rec chunk_data_memory dm =
-        match dm with
-        | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::(a4,b4)::(a5,b5)::(a6,b6)::(a7,b7)::dm'  when
-            (aligned a0 8 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3 &&
-             isplus a4 a0 4 && isplus a5 a0 5 && isplus a6 a0 6 && isplus a7 a0 7) ->
-          (a0,8,[b0;b1;b2;b3;b4;b5;b6;b7]) :: chunk_data_memory dm'
-        | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::dm' when
-            (aligned a0 4 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3) ->
-              (a0,4,[b0;b1;b2;b3]) :: chunk_data_memory dm'
-        | (a0,b0)::(a1,b1)::dm' when
-            (aligned a0 2 && isplus a1 a0 1) ->
-              (a0,2,[b0;b1]) :: chunk_data_memory dm'
-        | (a0,b0)::dm' ->
-            (a0,1,[b0]):: chunk_data_memory dm'
-        | [] -> [] in
-
       let initial_register_state =
         fun rbn ->
           try
@@ -1021,68 +569,10 @@ let stop_condition_met model instr =
       true
     | _ -> false)
 
-let is_branch model instruction =
-  let (name,_,_) = instruction in
-  match (model , name) with
-  | (PPC, "B") -> true
-  | (PPC, "Bc") -> true
-  | (PPC, "Bclr") -> true
-  | (PPC, "Bcctr") -> true
-  | (PPC, _) -> false
-  | (AArch64, "BranchImmediate") -> true
-  | (AArch64, "BranchConditional") -> true
-  | (AArch64, "CompareAndBranch") -> true
-  | (AArch64, "TestBitAndBranch") -> true
-  | (AArch64, "BranchRegister") -> true
-  | (AArch64, _) -> false
-  | (MIPS, _) -> false (*todo,fill this in*)
-
 let option_int_of_option_integer i = match i with
   | Some i -> Some (Nat_big_num.to_int i)
   | None -> None
 
-let set_next_instruction_address model =
-  match model with
-  | PPC ->
-    let cia = Reg.find "CIA" !reg in
-    let cia_addr = address_of_register_value cia in
-    (match cia_addr with
-    | Some cia_addr ->
-      let nia_addr = add_address_nat cia_addr 4 in 
-      let nia = register_value_of_address nia_addr Sail_impl_base.D_increasing in
-      reg := Reg.add "NIA" nia !reg
-    | _ -> failwith "CIA address contains unknown or undefined")
-  | AArch64 ->
-    let pc = Reg.find "_PC" !reg in
-    let pc_addr = address_of_register_value pc in
-    (match pc_addr with
-     | Some pc_addr ->
-       let n_addr = add_address_nat pc_addr 4 in
-       let n_pc = register_value_of_address n_addr D_decreasing in
-       reg := Reg.add "_PC" n_pc !reg
-     | _ -> failwith "_PC address contains unknown or undefined")
-  | MIPS -> 
-    let pc_addr       = address_of_register_value (Reg.find "PC" !reg) in
-    let branchPending = integer_of_register_value (Reg.find "branchPending" !reg) in
-    (match (pc_addr, option_int_of_option_integer branchPending) with
-     | (Some pc_val, Some 0) -> 
-       (* normal -- increment PC *)
-       let n_addr = add_address_nat pc_val 4 in
-       let n_pc = register_value_of_address n_addr D_decreasing in
-       begin
-         reg := Reg.add "nextPC" n_pc !reg;
-         reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
-       end
-     | (Some pc_val, Some 1) -> 
-       (* delay slot -- branch to delayed PC and clear branchPending *)
-       begin 
-         reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
-         reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg;
-         reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
-         reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
-       end
-     | (_, _) -> errorf "PC address contains unknown or undefined"; exit 1)
-
 let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
 
 let get_addr_trans_regs _ =
@@ -1192,68 +682,10 @@ let rec write_events = function
      | _ -> failwith "Only register write events expected");
     write_events events
 
-let fetch_instruction_opcode_and_update_ia model addr_trans =
-  match model with
-  | PPC ->
-    let cia = Reg.find "CIA" !reg in
-    let cia_addr = address_of_register_value cia in
-    (match cia_addr with
-     | Some cia_addr ->
-       let cia_a = integer_of_address cia_addr in
-       let opcode = (get_opcode cia_a) in
-       begin
-         reg := Reg.add "CIA" (Reg.find "NIA" !reg) !reg;
-         Opcode opcode
-       end
-     | None -> failwith "CIA address contains unknown or undefined")
-  | AArch64 ->
-    let pc = Reg.find "_PC" !reg in
-    let pc_addr = address_of_register_value pc in
-    (match pc_addr with
-     | Some pc_addr ->
-       let pc_a = integer_of_address pc_addr in
-       let opcode = (get_opcode pc_a) in
-       Opcode opcode
-     | None -> failwith "_PC address contains unknown or undefined")
-  | MIPS -> 
-    begin
-    reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
-    let nextPC  = Reg.find "nextPC" !reg in
-    let pc_addr = address_of_register_value nextPC in
-    (*let unused = interactf "PC: %s\n" (Printing_functions.register_value_to_string nextPC) in*)
-    (match pc_addr with
-    | Some pc_addr ->
-      let pc_a = match addr_trans (get_addr_trans_regs ()) pc_addr with
-        | Some a, Some events -> write_events (List.rev events); integer_of_address a
-        | Some a, None -> integer_of_address a
-        | None, Some events ->
-          write_events (List.rev events);
-          let nextPC  = Reg.find "nextPC" !reg in
-          reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
-          let pc_addr = address_of_register_value nextPC in
-          (match pc_addr with
-           | Some pc_addr ->
-             (match addr_trans (get_addr_trans_regs ()) pc_addr with
-              | Some a, Some events -> write_events (List.rev events); integer_of_address a
-              | Some a, None -> integer_of_address a
-              | None, _ -> failwith "Address translation failed twice")
-           | None -> failwith "no nextPc address")
-        | _ -> failwith "No address and no events from translate address"
-      in
-      let opcode = (get_opcode pc_a) in
-      begin
-        reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
-        Opcode opcode
-      end
-     | None -> errorf "nextPC contains unknown or undefined"; exit 1)
-    end
-  |  _ -> assert false
-
 let get_pc_address = function
   | MIPS -> Reg.find "PC" !reg
   | PPC  -> Reg.find "CIA" !reg
   | AArch64 -> Reg.find "_PC" !reg
-        
 
 let option_int_of_reg str =
   option_int_of_option_integer (integer_of_register_value (Reg.find str !reg))
@@ -1283,6 +715,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
             let npc_addr = add_address_nat pc_val 4 in
             let npc_reg = register_value_of_address npc_addr Sail_impl_base.D_decreasing in
             reg := Reg.add "nextPC" npc_reg !reg;
+            reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
           | Some 1 ->
             reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
             reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg;
@@ -1290,12 +723,14 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
           let opcode = Opcode (get_opcode pc) in
           let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
             | Instr(instruction,istate) ->
+               let instruction = interp_value_to_instr_external context instruction in
               interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
               (instruction,istate)
             | Decode_error d ->
               (match d with
-              | Interp_interface.Unsupported_instruction_error instr ->
-                errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
+              | Interp_interface.Unsupported_instruction_error instruction ->
+               let instruction = interp_value_to_instr_external context instruction in
+                errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instruction)
               | Interp_interface.Not_an_instruction_error op ->
                 (match op with
                 | Opcode bytes ->
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index eb2e1a4e..59e86ece 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -42,6 +42,29 @@
 
 open import Pervasives_extra
 
+
+
+class ( EnumerationType 'a ) 
+  val toNat : 'a -> nat
+end
+
+
+val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
+let ~{ocaml} enumeration_typeCompare e1 e2 =
+  compare (toNat e1) (toNat e2)
+let inline {ocaml} enumeration_typeCompare = defaultCompare
+
+ 
+default_instance forall 'a. EnumerationType 'a => (Ord 'a)
+  let compare = enumeration_typeCompare
+  let (<)  r1 r2 = (enumeration_typeCompare r1 r2) = LT
+  let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
+  let (>)  r1 r2 = (enumeration_typeCompare r1 r2) = GT
+  let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
+end
+
+
+
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
 instance forall 'a. Ord 'a => (Ord (maybe 'a))
   let compare = maybeCompare compare
@@ -214,6 +237,28 @@ instance (Ord byte)
   let (>=) = byteGreaterEq
 end
 
+let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) =
+  compare o1 o2
+let {ocaml} opcodeCompare = defaultCompare
+
+let ~{ocaml} opcodeLess b1 b2      = opcodeCompare b1 b2 =  LT
+let ~{ocaml} opcodeLessEq b1 b2    = opcodeCompare b1 b2 <> GT
+let ~{ocaml} opcodeGreater b1 b2   = opcodeCompare b1 b2 =  GT
+let ~{ocaml} opcodeGreaterEq b1 b2 = opcodeCompare b1 b2 <> LT
+
+let inline {ocaml} opcodeLess      = defaultLess
+let inline {ocaml} opcodeLessEq    = defaultLessEq
+let inline {ocaml} opcodeGreater   = defaultGreater
+let inline {ocaml} opcodeGreaterEq = defaultGreaterEq
+
+instance (Ord opcode)
+  let compare = opcodeCompare
+  let (<)  = opcodeLess
+  let (<=) = opcodeLessEq
+  let (>)  = opcodeGreater
+  let (>=) = opcodeGreaterEq
+end
+
 let addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
 (* this cannot be defaultCompare for OCaml because addresses contain big ints *)
 
@@ -419,6 +464,8 @@ end
 
 (* Data structures for building up instructions *)
 
+(* careful: changes in the read/write/barrier kinds have to be
+   reflected in deep_shallow_convert *)
 type read_kind =
   (* common reads *)
   | Read_plain
@@ -426,6 +473,12 @@ type read_kind =
   | Read_reserve
   (* AArch64 reads *)
   | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
+  (* RISC-V reads *)
+  | Read_RISCV_acquire  | Read_RISCV_strong_acquire
+  | Read_RISCV_reserved | Read_RISCV_reserved_acquire
+  | Read_RISCV_reserved_strong_acquire
+  (* x86 reads *)
+  | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
 
 instance (Show read_kind)
   let show = function
@@ -435,6 +488,12 @@ instance (Show read_kind)
     | 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"
   end
 end
 
@@ -445,6 +504,12 @@ type write_kind =
   | Write_conditional
   (* AArch64 writes *)
   | Write_release | Write_exclusive | Write_exclusive_release
+  (* RISC-V *)
+  | Write_RISCV_release     | Write_RISCV_strong_release
+  | Write_RISCV_conditional | Write_RISCV_conditional_release
+  | Write_RISCV_conditional_strong_release
+  (* x86 writes *)
+  | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)
 
 instance (Show write_kind)
   let show = function
@@ -453,6 +518,12 @@ instance (Show write_kind)
     | 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"
   end
 end
 
@@ -468,7 +539,12 @@ type barrier_kind =
   (* 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_i
+  (* X86 *)
+  | Barrier_x86_MFENCE
 
 
 instance (Show barrier_kind)
@@ -486,6 +562,13 @@ instance (Show barrier_kind)
     | 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_i     -> "Barrier_RISCV_i"
+    | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
   end
 end
 
@@ -502,15 +585,15 @@ instance (Show trans_kind)
 end
 
 type instruction_kind = 
-  | IK_barrier of barrier_kind 
-  | IK_mem_read of read_kind 
+  | IK_barrier   of barrier_kind
+  | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
-(* SS reinstating cond_branches
-at present branches are not distinguished in the instruction_kind;
-they just have particular nias (and will be IK_simple *)
-  | IK_cond_branch 
-(*  | IK_uncond_branch *)
-  | IK_trans of trans_kind
+  | IK_mem_rmw   of (read_kind * write_kind)
+  | IK_cond_branch
+  (* unconditional branches are not distinguished in the instruction_kind;
+  they just have particular nias (and will be IK_simple *)
+  (* | IK_uncond_branch *)
+  | IK_trans     of trans_kind
   | IK_simple
 
 
@@ -658,6 +741,13 @@ let ~{ocaml} barrier_number = function
     | 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_i -> 18
+    | Barrier_x86_MFENCE -> 19
   end
 
  let ~{ocaml} barrier_kindCompare bk1 bk2 =
@@ -743,21 +833,20 @@ instance (Ord barrier_kind)
   let (>=) = barrier_kindGreaterEq
 end
 
-
 type event = 
-| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
-| E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name)
-| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
-| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
-| E_excl_res
-| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
-| E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name)
-| E_barrier of barrier_kind
-| E_footprint 
-| E_read_reg of reg_name
-| E_write_reg of reg_name * register_value
-| E_escape
-| E_error of string 
+  | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
+  | E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name)
+  | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
+  | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
+  | E_excl_res
+  | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
+  | E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name)
+  | E_barrier of barrier_kind
+  | E_footprint 
+  | E_read_reg of reg_name
+  | E_write_reg of reg_name * register_value
+  | E_escape
+  | E_error of string 
 
 
 let eventCompare e1 e2 = 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2855adbc..ef91c684 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1294,9 +1294,9 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
              (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem None typq])
              ((*doc_typquant_lem typq*) ar_doc) in
          let make_id pat id =
-           separate space [string "SIA.Id_aux";
-                           parens (string "SIA.Id " ^^ string_lit (doc_id id));
-                           if pat then underscore else string "SIA.Unknown"] in
+           separate space [string "Interp_ast.Id_aux";
+                           parens (string "Interp_ast.Id " ^^ string_lit (doc_id id));
+                           if pat then underscore else string "Interp_ast.Unknown"] in
          let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
          let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
          let fromInterpValuePP =
@@ -1308,18 +1308,18 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
                     match tu with
                     | Tu_ty_id (ty,cid) ->
                        (separate space)
-                         [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                         [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
                           arrow;
                           doc_id_lem_ctor cid;
                           parens (string "fromInterpValue v")]
                     | Tu_id cid ->
                        (separate space)
-                         [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                         [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
                           arrow;
                           doc_id_lem_ctor cid])
                   ar) ^/^
 
-                  ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
+                  ((separate space) [pipe;string "Interp_ast.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
 
                  let failmessage =
                     (string_lit
@@ -1338,43 +1338,40 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
                     | Tu_ty_id (ty,cid) ->
                        (separate space)
                          [pipe;doc_id_lem_ctor cid;string "v";arrow;
-                          string "SI.V_ctor";
+                          string "Interp_ast.V_ctor";
                           parens (make_id false cid);
-                          parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                          string "SI.C_Union";
+                          parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id));
+                          string "Interp_ast.C_Union";
                           parens (string "toInterpValue v")]
                     | Tu_id cid ->
                        (separate space)
                          [pipe;doc_id_lem_ctor cid;arrow;
-                          string "SI.V_ctor";
+                          string "Interp_ast.V_ctor";
                           parens (make_id false cid);
-                          parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                          string "SI.C_Union";
+                          parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id));
+                          string "Interp_ast.C_Union";
                           parens (string "toInterpValue ()")])
                   ar) ^/^
                  string "end") in
          let fromToInterpValuePP =
+          toInterpValuePP ^^ hardline ^^ hardline ^^
+          fromInterpValuePP ^^ hardline ^^ hardline ^^           
            ((prefix 2 1)
               (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)])
               (concat [string "let toInterpValue = ";toInterpValueF;hardline;
                        string "let fromInterpValue = ";fromInterpValueF]))
            ^/^ string "end" in
-         typ_pp ^^ hardline ^^ hardline ^^
-           if !print_to_from_interp_value then
-           toInterpValuePP ^^ hardline ^^ hardline ^^
-             fromInterpValuePP ^^ hardline ^^ hardline ^^
-               fromToInterpValuePP ^^ hardline
-           else empty)
+         (typ_pp ^^ hardline,fromToInterpValuePP ^^ hardline))
   | TD_enum(id,nm,enums,_) ->
      (match id with
-      | Id_aux ((Id "read_kind"),_) -> empty
-      | Id_aux ((Id "write_kind"),_) -> empty
-      | Id_aux ((Id "barrier_kind"),_) -> empty
-      | Id_aux ((Id "trans_kind"),_) -> empty
-      | Id_aux ((Id "instruction_kind"),_) -> empty
-      | Id_aux ((Id "regfp"),_) -> empty
-      | Id_aux ((Id "niafp"),_) -> empty
-      | Id_aux ((Id "diafp"),_) -> empty
+      | Id_aux ((Id "read_kind"),_) -> (empty,empty)
+      | Id_aux ((Id "write_kind"),_) -> (empty,empty)
+      | Id_aux ((Id "barrier_kind"),_) -> (empty,empty)
+      | Id_aux ((Id "trans_kind"),_) -> (empty,empty)
+      | Id_aux ((Id "instruction_kind"),_) -> (empty,empty)
+      | Id_aux ((Id "regfp"),_) -> (empty,empty)
+      | Id_aux ((Id "niafp"),_) -> (empty,empty)
+      | Id_aux ((Id "diafp"),_) -> (empty,empty)
       | _ ->
          let rec range i j = if i > j then [] else i :: (range (i+1) j) in
          let nats = range 0 in
@@ -1385,9 +1382,9 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
          let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
          let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
          let make_id pat id =
-           separate space [string "SIA.Id_aux";
-                           parens (string "SIA.Id " ^^ string_lit (doc_id id));
-                           if pat then underscore else string "SIA.Unknown"] in
+           separate space [string "Interp_ast.Id_aux";
+                           parens (string "Interp_ast.Id " ^^ string_lit (doc_id id));
+                           if pat then underscore else string "Interp_ast.Unknown"] in
          let fromInterpValuePP =
            (prefix 2 1)
              (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"])
@@ -1395,7 +1392,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
                ((separate_map (break 1))
                   (fun (cid) ->
                     (separate space)
-                      [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                      [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
                        arrow;doc_id_lem_ctor cid]
                   )
                   enums
@@ -1403,7 +1400,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
                  (
                    (align
                       ((prefix 3 1)
-                         (separate space [pipe;string ("SI.V_lit (SIA.L_aux (SIA.L_num n) _)");arrow])
+                         (separate space [pipe;string ("Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _)");arrow])
                          (separate space [string "match";parens(string "natFromInteger n");string "with"] ^/^
                             (
                               ((separate_map (break 1))
@@ -1419,7 +1416,7 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
                    )
                  ) ^/^
 
-                  ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
+                  ((separate space) [pipe;string "Interp_ast.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
 
                    let failmessage =
                      (string_lit
@@ -1437,27 +1434,25 @@ let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
                   (fun (cid,number) ->
                     (separate space)
                       [pipe;doc_id_lem_ctor cid;arrow;
-                       string "SI.V_ctor";
+                       string "Interp_ast.V_ctor";
                        parens (make_id false cid);
-                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                       parens (string ("SI.C_Enum " ^ string_of_int number));
+                       parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id));
+                       parens (string ("Interp_ast.C_Enum " ^ string_of_int number));
                        parens (string "toInterpValue ()")])
                   (List.combine enums (nats ((List.length enums) - 1)))) ^/^
                  string "end") in
          let fromToInterpValuePP =
+           toInterpValuePP ^^ hardline ^^ hardline ^^
+           fromInterpValuePP ^^ hardline ^^ hardline ^^
            ((prefix 2 1)
              (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)])
              (concat [string "let toInterpValue = ";toInterpValueF;hardline;
                       string "let fromInterpValue = ";fromInterpValueF]))
            ^/^ string "end" in
-          typ_pp ^^ hardline ^^ hardline ^^
-            if !print_to_from_interp_value 
-            then toInterpValuePP ^^ hardline ^^ hardline ^^
-              fromInterpValuePP ^^ hardline ^^ hardline ^^
-                fromToInterpValuePP ^^ hardline
-            else empty)
+         (typ_pp ^^ hardline,
+          fromToInterpValuePP ^^ hardline))
   | TD_register(id,n1,n2,rs) ->
-    match n1, n2 with
+    match n1,n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
        let dir_b = i1 < i2 in
        let dir = (if dir_b then "true" else "false") in