1 files changed, 18 insertions, 21 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index a089f8c5..fa0fcd24 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -87,22 +87,29 @@ let set_reg state reg v =
   <| state with regstate = reg.write_to state.regstate v |>
 
 
+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 : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b
 let read_mem dir read_kind addr sz state =
   let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
   let value = of_bits (Sail_values.internal_mem_value dir memory_value) in
-  let is_exclusive = match read_kind with
-    | 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
-  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)]
 
@@ -116,17 +123,7 @@ let read_tag dir read_kind addr state =
     | Just t -> t
     | Nothing -> B0
   end in
-  let is_exclusive = match read_kind with
-    | 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
-  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)]