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.

6 files changed, 23 insertions, 24 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index 2f2d43ef..56aa6e87 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -32,7 +32,7 @@ datatype 'regval event =
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
   | e_write_memv "memory_byte list" bool
-  | e_write_tagv bitU bool
+  | e_write_tag "bitU list" bitU bool
   (* Tell the system to dynamically recalculate dependency footprint *)
   | e_footprint
   (* Request a memory barrier *)
@@ -50,7 +50,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T"
 | Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T"
 | Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T"
-| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \<in> T"
+| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \<in> T"
 | Footprint: "((Footprint k), e_footprint, k) \<in> T"
 | Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T"
 | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
@@ -79,7 +79,7 @@ lemma Traces_cases:
   | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
   | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces"
   | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv val v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a val v # t'" and "(k v, t', m') \<in> Traces"
   | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \<in> Traces"
   | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
   | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \<in> Traces"
diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy
index 746fd315..291157f5 100644
--- a/lib/isabelle/State_monad_lemmas.thy
+++ b/lib/isabelle/State_monad_lemmas.thy
@@ -274,7 +274,7 @@ lemma no_throw_mem_builtins:
   "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s"
   "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s"
   "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
-  "\<And>t s. ignore_throw (write_tagS t) s = write_tagS t s"
+  "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
   unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 920277f6..12915271 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -42,10 +42,10 @@ val MEMval_conditional     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b
 val MEMval_tag             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e
 val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e
 
-let MEMval _ size v                   = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional _ size v       = write_mem_val v >>= fun b -> return (if b then true else false)
-let MEMval_tag  _ size t v            = write_mem_val v >>= fun _ -> write_tag_val (bitU_of_bool t) >>= fun _ -> return ()
-let MEMval_tag_conditional _ size t v = write_mem_val v >>= fun b -> write_tag_val (bitU_of_bool t) >>= fun _ -> return (if b then true else false)
+let MEMval _ size v                      = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional _ size v          = write_mem_val v >>= fun b -> return (if b then true else false)
+let MEMval_tag addr size t v             = write_mem_val v >>= fun _ -> write_tag addr (bitU_of_bool t) >>= fun _ -> return ()
+let MEMval_tag_conditional addr size t v = write_mem_val v >>= fun b -> write_tag addr (bitU_of_bool t) >>= fun _ -> return (if b then true else false)
 
 val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e
 
@@ -86,9 +86,12 @@ val undefined_vector : forall 'a. integer -> 'a -> list 'a
 let undefined_vector len u = repeat [u] len
 val undefined_bitvector : forall 'a. Bitvector 'a => integer -> 'a
 let undefined_bitvector len = of_bits (repeat [B0] len)
+val undefined_bits : forall 'a. Bitvector 'a => integer -> 'a
 let undefined_bits len = undefined_bitvector len
 let undefined_bit () = B0
 let undefined_real () = realFromFrac 0 1
 let undefined_range i j = i
 let undefined_atom i = i
 let undefined_nat () = (0:ii)
+
+let skip () = return ()
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)