From d8c238ddac07ed8bf828596ff68198d0c63758f5 Mon Sep 17 00:00:00 2001
From: Christopher Pulte
Date: Tue, 22 Aug 2017 14:39:20 +0100
Subject: and fix that other places

---
 src/gen_lib/state.lem | 37 +++++++++++++++----------------------
 1 file changed, 15 insertions(+), 22 deletions(-)

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 2e29d19a..2ea1247e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -47,25 +47,27 @@ let set_reg state reg bitv =
   <| state with regstate = Map.insert reg bitv state.regstate |>
 
 
+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_reserved -> true
+  | Sail_impl_base.Read_RISCV_reserved_acquire -> 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 = integer_of_address (address_of_bitv 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 = 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
-    | Sail_impl_base.Read_RISCV_acquire -> false
-    | Sail_impl_base.Read_RISCV_reserved -> true
-    | Sail_impl_base.Read_RISCV_reserved_acquire -> true
-  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)]
 
@@ -79,17 +81,8 @@ 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)]
 
-- 
cgit v1.2.3