Add Write_mem event/outcome without tag

The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.

3 files changed, 43 insertions, 18 deletions

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index cf2fd151..7a55056c 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -18,8 +18,9 @@ type monad 'regval 'a 'e =
   | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
-  (* Request to write a memory value of the given size together with a tag
-     at the given address. *)
+  (* Request to write a memory value of the given size at the given address,
+     with or without a tag. *)
+  | Write_mem of write_kind * nat * nat * list memory_byte * (bool -> monad 'regval 'a 'e)
   | Write_memt of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
@@ -43,6 +44,7 @@ type monad 'regval 'a 'e =
 type event 'regval =
   | E_read_mem of read_kind * nat * nat * list memory_byte
   | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * nat * nat * list memory_byte * bool
   | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool
   | E_write_ea of write_kind * nat * nat
   | E_excl_res of bool
@@ -63,6 +65,7 @@ let rec bind m f = match m with
   | Done a -> f a
   | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> bind (k v) f)
   | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> bind (k v) f)
+  | Write_mem wk a sz v k ->    Write_mem wk a sz v    (fun v -> bind (k v) f)
   | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> bind (k v) f)
   | Read_reg descr k ->         Read_reg descr         (fun v -> bind (k v) f)
   | Excl_res k ->               Excl_res               (fun v -> bind (k v) f)
@@ -96,6 +99,7 @@ let rec try_catch m h = match m with
   | Done a -> Done a
   | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> try_catch (k v) h)
   | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> try_catch (k v) h)
+  | Write_mem wk a sz v k ->    Write_mem wk a sz v    (fun v -> try_catch (k v) h)
   | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> try_catch (k v) h)
   | Read_reg descr k ->         Read_reg descr         (fun v -> try_catch (k v) h)
   | Excl_res k ->               Excl_res               (fun v -> try_catch (k v) h)
@@ -188,8 +192,17 @@ let write_mem_ea wk addr sz =
     (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
 
 val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e
+let write_mem wk addr sz v =
+  match (mem_bytes_of_bits v, nat_of_bv addr) with
+    | (Just v, Just addr) ->
+       Write_mem wk addr (nat_of_int sz) v return
+    | _ -> Fail "write_mem"
+  end
+
+val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
   write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e
-let write_mem wk addr sz v tag =
+let write_memt wk addr sz v tag =
   match (mem_bytes_of_bits v, nat_of_bv addr) with
     | (Just v, Just addr) ->
        Write_memt wk addr (nat_of_int sz) v tag return
@@ -259,6 +272,8 @@ val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event
 let emitEvent m e = match (e, m) with
   | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
      if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
+     if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
   | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
      if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
   | (E_read_reg r v, Read_reg r' k) ->
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index a055bfe0..98a5390d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -9,13 +9,14 @@ open import {isabelle} `Sail2_state_monad_lemmas`
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
 let rec liftState ra m = match m with
   | (Done a)                   -> returnS a
-  | (Read_mem rk a sz k)       -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
-  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)     (fun v -> liftState ra (k v))
-  | (Write_memt wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
-  | (Read_reg r k)             -> bindS (read_regvalS ra r)            (fun v -> liftState ra (k v))
-  | (Excl_res k)               -> bindS (excl_resultS ())              (fun v -> liftState ra (k v))
-  | (Choose _ k)               -> bindS (choose_boolS ())              (fun v -> liftState ra (k v))
-  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)          (liftState ra k)
+  | (Read_mem rk a sz k)       -> bindS (read_mem_bytesS rk a sz)       (fun v -> liftState ra (k v))
+  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)      (fun v -> liftState ra (k v))
+  | (Write_mem wk a sz v k)    -> bindS (write_mem_bytesS wk a sz v)    (fun v -> liftState ra (k v))
+  | (Write_memt wk a sz v t k) -> bindS (write_memt_bytesS wk a sz v t) (fun v -> liftState ra (k v))
+  | (Read_reg r k)             -> bindS (read_regvalS ra r)             (fun v -> liftState ra (k v))
+  | (Excl_res k)               -> bindS (excl_resultS ())               (fun v -> liftState ra (k v))
+  | (Choose _ k)               -> bindS (choose_boolS ())               (fun v -> liftState ra (k v))
+  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)           (liftState ra k)
   | (Write_ea _ _ _ k)         -> liftState ra k
   | (Footprint k)              -> liftState ra k
   | (Barrier _ k)              -> liftState ra k
@@ -32,6 +33,8 @@ let emitEventS ra e s = match e with
   | E_read_memt _ addr sz (v, tag) ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
      if v' = v && tag' = tag then Just s else Nothing)
+  | E_write_mem _ addr sz v success ->
+     if success then Just (put_mem_bytes addr sz v B0 s) else Nothing
   | E_write_memt _ addr sz v tag success ->
      if success then Just (put_mem_bytes addr sz v tag s) else Nothing
   | E_read_reg r v ->
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 18e57b30..3042700c 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -162,27 +162,34 @@ let excl_resultS =
 
 (* Write little-endian list of bytes to given address *)
 val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
-let put_mem_bytes addr sz v t s =
+let put_mem_bytes addr sz v tag s =
   let addrs = genlist (fun n -> addr + n) sz in
   let a_v = List.zip addrs v in
   let write_byte mem (addr, v) = Map.insert addr v mem in
-  let write_tag mem addr = Map.insert addr t mem in
+  let write_tag mem addr = Map.insert addr tag mem in
   <| s with memstate = List.foldl write_byte s.memstate a_v;
             tagstate = List.foldl write_tag s.tagstate addrs |>
 
-val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
-let write_mem_bytesS _ addr sz v t =
+val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_memt_bytesS _ addr sz v t =
   updateS (put_mem_bytes addr sz v t) >>$
   returnS true
 
-val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> nat -> 'b -> bitU -> monadS 'regs bool 'e
-let write_memS wk addr sz v t =
+val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS wk addr sz v = write_memt_bytesS wk addr sz v B0
+
+val write_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> bitU -> monadS 'regs bool 'e
+let write_memtS wk addr sz v t =
   match (nat_of_bv addr, mem_bytes_of_bits v) with
-    | (Just addr, Just v) -> write_mem_bytesS wk addr sz v t
+    | (Just addr, Just v) -> write_memt_bytesS wk addr (nat_of_int sz) v t
     | _ -> failS "write_mem"
   end
 
+val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e
+let write_memS wk addr sz v = write_memtS wk addr sz v B0
+
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
 let read_regS reg = readS (fun s -> reg.read_from s.regstate)