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.

1 files changed, 5 insertions, 9 deletions

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)