1 files changed, 35 insertions, 1 deletions

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 61809cf1..430ee562 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -5,10 +5,12 @@ open import Sail_values
 (* 'a is result type *)
 
 type memstate = map integer memory_byte
+type tagstate = map integer bitU
 type regstate = map string (vector bitU)
 
 type sequential_state = <| regstate : regstate;
                            memstate : memstate; 
+                           tagstate : tagstate;
                            write_ea : maybe (write_kind * integer * integer);
                            last_exclusive_operation_was_load : bool|>
 
@@ -63,7 +65,31 @@ let read_mem dir read_kind addr sz state =
   if is_exclusive 
   then [(Left value, <| state with last_exclusive_operation_was_load = true |>)]
   else [(Left value, state)]
-  
+
+(* caps are aligned at 32 bytes *)
+let cap_alignment = (32 : integer)
+
+val read_tag : bool -> read_kind -> vector bitU -> M bitU
+let read_tag dir read_kind addr state =
+  let addr = (integer_of_address (address_of_bitv addr)) / cap_alignment in
+  let tag = match (Map.lookup addr state.tagstate) with
+    | 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
+  then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)]
+  else [(Left tag, state)]
+
 val excl_result : unit -> M bool
 let excl_result () state =
   let success =
@@ -87,6 +113,14 @@ let write_mem_val v state =
                             state.memstate addresses_with_value in
   [(Left true,  <| state with memstate = memstate |>)]
 
+val write_tag : bitU -> M bool
+let write_tag t state =
+  let (write_kind,addr,sz) = match state.write_ea with
+    | Nothing -> failwith "write ea has not been announced yet"
+    | Just write_ea -> write_ea end in
+  let taddr = addr / cap_alignment in
+  let tagstate = Map.insert taddr t state.tagstate in
+  [(Left true,  <| state with tagstate = tagstate |>)]
 
 val read_reg : register -> M (vector bitU)
 let read_reg reg state =