Monad refactoring in Lem shallow embedding

- Merge tag reading/writing outcomes into memory value reading/writing outcomes
- Add effective address to Write_mem; this duplicates information in the
  Write_ea outcome that should come before, but it makes the effective address
  more conveniently available in events and traces, and it allows the following
  simplification in the state monad:
- Remove write_ea field from state record; the effective address is now
  expected as a parameter to the write_memS function
- Remove last_exclusive_operation_was_load field from state record; this was
  used to keep track of exclusive loads, but this was a a relatively coarse
  approximation anyway, so it might make more sense to track this in
  (architecture-specific) Sail code.  Overall, the state record now simply
  contains the fields regstate, memstate, tagstate.

1 files changed, 57 insertions, 53 deletions

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 78b1615e..991d3895 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -8,19 +8,17 @@ type address = list bitU
 
 type monad 'regval 'a 'e =
   | Done of 'a
-  (* Read a number of bytes from memory, returned in little endian order *)
-  | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
-  (* Read the tag of a memory address *)
-  | Read_tag of address * (bitU -> monad 'regval 'a 'e)
-  (* Tell the system a write is imminent, at address lifted, of size nat *)
+  (* Read a number of bytes from memory, returned in little endian order,
+     together with a tag. *)
+  | Read_mem of read_kind * address * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+  (* Tell the system a write is imminent, at the given address and with the
+     given size. *)
   | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal, given in little endian order *)
-  | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
-  (* Request to write the tag at given address. *)
-  | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
+  (* Request to write a memory value of the given size together with a tag
+     at the given address. *)
+  | Write_mem of write_kind * address * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -38,26 +36,36 @@ type monad 'regval 'a 'e =
   (* Exception of type 'e *)
   | Exception of 'e
 
+type event 'regval =
+  | E_read_mem of read_kind * address * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * address * nat * list memory_byte * bitU * bool
+  | E_write_ea of write_kind * address * nat
+  | E_excl_res of bool
+  | E_barrier of barrier_kind
+  | E_footprint
+  | E_read_reg of register_name * 'regval
+  | E_write_reg of register_name * 'regval
+  | E_undefined of bool
+  | E_print of string
+
 val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
 
 val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
 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_tag a k ->       Read_tag a       (fun v -> bind (k v) f)
-  | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
-  | Write_tag a t k ->    Write_tag a 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)
-  | Undefined k ->        Undefined        (fun v -> bind (k v) f)
-  | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
-  | Footprint k ->        Footprint        (bind k f)
-  | Barrier bk k ->       Barrier bk       (bind k f)
-  | Write_reg r v k ->    Write_reg r v    (bind k f)
-  | Print msg k ->        Print msg        (bind k f)
-  | Fail descr ->         Fail descr
-  | Exception e ->        Exception e
+  | Read_mem rk a sz k ->      Read_mem rk a sz      (fun v -> bind (k v) f)
+  | Write_mem wk a sz v t k -> Write_mem 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)
+  | Undefined k ->             Undefined             (fun v -> bind (k v) f)
+  | Write_ea wk a sz k ->      Write_ea wk a sz      (bind k f)
+  | Footprint k ->             Footprint             (bind k f)
+  | Barrier bk k ->            Barrier bk            (bind k f)
+  | Write_reg r v k ->         Write_reg r v         (bind k f)
+  | Print msg k ->             Print msg             (bind k f)
+  | Fail descr ->              Fail descr
+  | Exception e ->             Exception e
 end
 
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
@@ -74,21 +82,19 @@ let throw e = Exception e
 
 val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
 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_tag a k ->       Read_tag a       (fun v -> try_catch (k v) h)
-  | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
-  | Write_tag a t k ->    Write_tag a 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)
-  | Undefined k ->        Undefined        (fun v -> try_catch (k v) h)
-  | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
-  | Footprint k ->        Footprint        (try_catch k h)
-  | Barrier bk k ->       Barrier bk       (try_catch k h)
-  | Write_reg r v k ->    Write_reg r v    (try_catch k h)
-  | Print msg k ->        Print msg        (try_catch k h)
-  | Fail descr ->         Fail descr
-  | Exception e ->        h e
+  | Done a -> Done a
+  | Read_mem rk a sz k ->      Read_mem rk a sz      (fun v -> try_catch (k v) h)
+  | Write_mem wk a sz v t k -> Write_mem 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)
+  | Undefined k ->             Undefined             (fun v -> try_catch (k v) h)
+  | Write_ea wk a sz k ->      Write_ea wk a sz      (try_catch k h)
+  | Footprint k ->             Footprint             (try_catch k h)
+  | Barrier bk k ->            Barrier bk            (try_catch k h)
+  | Write_reg r v k ->         Write_reg r v         (try_catch k h)
+  | Print msg k ->             Print msg             (try_catch k h)
+  | Fail descr ->              Fail descr
+  | Exception e ->             h e
 end
 
 (* For early return, we abuse exceptions by throwing and catching
@@ -126,19 +132,19 @@ let maybe_fail msg = function
   | Nothing -> Fail msg
 end
 
-val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
+val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
 let read_mem_bytes rk addr sz =
   Read_mem rk (bits_of addr) (nat_of_int sz) return
 
-val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
+val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
 let read_mem rk addr sz =
   bind
     (read_mem_bytes rk addr sz)
-    (fun bytes ->
-       maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
-
-val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
-let read_tag addr = Read_tag (bits_of addr) return
+    (fun (bytes, tag) ->
+       match of_bits (bits_of_mem_bytes bytes) with
+         | Just v -> return (v, tag)
+         | Nothing -> Fail "bits_of_mem_bytes"
+       end)
 
 val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
 let excl_result () =
@@ -148,15 +154,13 @@ let excl_result () =
 val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
 let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
 
-val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
-let write_mem_val v = match mem_bytes_of_bits v with
-  | Just v -> Write_memv v return
-  | Nothing -> Fail "write_mem_val"
+val write_mem : 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 = match mem_bytes_of_bits v with
+  | Just v -> Write_mem wk (bits_of addr) (nat_of_int sz) v tag return
+  | Nothing -> Fail "write_mem"
 end
 
-val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
-let write_tag addr b = Write_tag (bits_of addr) b return
-
 val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
 let read_reg reg =
   let k v =