Add tag memory to Lem shallow embedding

2 files changed, 52 insertions, 15 deletions

diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem
index ad1231b6..73dc42ed 100644
--- a/mips/mips_extras_embed_sequential.lem
+++ b/mips/mips_extras_embed_sequential.lem
@@ -6,14 +6,21 @@ open import State
 
 val MEMr             : (vector bitU * integer) -> M (vector bitU)
 val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
-val MEMr_tag         : (vector bitU * integer) -> M (vector bitU)
-val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU)
+val MEMr_tag         : (vector bitU * integer) -> M (bitU * vector bitU)
+val MEMr_tag_reserve : (vector bitU * integer) -> M (bitU * vector bitU)
 
 let MEMr (addr,size)             = read_mem false Read_plain addr size
 let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
 
-let MEMr_tag (addr,size)         = read_mem false Read_plain addr size
-let MEMr_tag_reserve (addr,size) = read_mem false Read_reserve addr size
+let MEMr_tag (addr,size) =
+  read_mem false Read_plain addr size >>= fun v ->
+  read_tag false Read_plain addr >>= fun t ->
+  return (t, v)
+
+let MEMr_tag_reserve (addr,size) =
+  read_mem false Read_plain addr size >>= fun v ->
+  read_tag false Read_plain addr >>= fun t ->
+  return (t, v)
 
 
 val MEMea                 : (vector bitU * integer) -> M unit
@@ -30,17 +37,13 @@ let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
 
 val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
-val MEMval_tag             : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
-
-let MEMval (_,_,v)                 = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)     = write_mem_val v >>= fun b -> return (if b then B1 else B0)
-let MEMval_tag (_,_,v)             = write_mem_val v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+val MEMval_tag             : (vector bitU * integer * bitU * vector bitU) -> M unit
+val MEMval_tag_conditional : (vector bitU * integer * bitU * vector bitU) -> M bitU
 
-(* TODO *)
-val TAGw : (vector bitU * vector bitU) -> M unit
-let TAGw (addr, tag) = failwith "TAGw not implemented"
+let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+let MEMval_tag (_,_,t,v)             = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then B1 else B0)
 
 val MEM_sync  : unit -> M unit
 
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 =