Add address to Write_tag outcome

The state monad currently assumes that tags are written to and read from
properly aligned addresses (since it does not know the capability size used in
the Sail model).  This change allows the Sail model to pass in the aligned
address(es) even if data is written to an unaligned address.  There might be
better ways to model tag writing, but this approach seems rather general.

3 files changed, 12 insertions, 16 deletions

diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index 747600a9..edbe1f03 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -19,8 +19,8 @@ type 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 last signalled address. *)
-  | Write_tagv of bitU * (bool -> monad 'regval 'a 'e)
+  (* Request to write the tag at given address. *)
+  | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -48,7 +48,7 @@ let rec bind m f = match m with
   | 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_tagv t k ->     Write_tagv t     (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)
@@ -84,7 +84,7 @@ let rec try_catch m h = match m with
   | 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_tagv t k ->     Write_tagv t     (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)
@@ -150,8 +150,8 @@ let write_mem_val v = match mem_bytes_of_bits v with
   | Nothing -> Fail "write_mem_val"
 end
 
-val write_tag_val : forall 'rv 'e. bitU -> monad 'rv bool 'e
-let write_tag_val b = Write_tagv b return
+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 =
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 3ae0d7ba..222cd715 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -14,7 +14,7 @@ let rec liftState ra s = match s with
   | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
   | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
   | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
-  | (Write_tagv t k)     -> bindS (write_tagS t)            (fun v -> liftState ra (k v))
+  | (Write_tag a t k)    -> bindS (write_tagS a 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))
   | (Undefined k)        -> bindS (undefined_boolS ())      (fun v -> liftState ra (k v))
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 26f912fd..9fcbd5ce 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -179,15 +179,11 @@ let write_mem_valS v = match mem_bytes_of_bits v with
   | Nothing -> failS "write_mem_val"
 end
 
-val write_tagS : forall 'regs 'e. bitU -> monadS 'regs bool 'e
-let write_tagS t =
-  readS (fun s -> s.write_ea) >>$= (function
-      | Nothing -> failS "write ea has not been announced yet"
-      | Just (_, addr, _) ->
-         (*let taddr = addr / cap_alignment in*)
-         updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
-         returnS true
-    end)
+val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e
+let write_tagS addr t =
+   (*let taddr = addr / cap_alignment in*)
+   updateS (fun s -> <| s with tagstate = Map.insert (unsigned addr) t s.tagstate |>) >>$
+   returnS true
 
 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)