From dfc417cea131f3e8bb033f3e25b24c94f909c809 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 2 Mar 2018 00:28:56 +0000 Subject: 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. --- lib/isabelle/Prompt_monad_lemmas.thy | 6 +++--- lib/isabelle/State_monad_lemmas.thy | 2 +- mips/mips_extras.lem | 11 +++++++---- src/gen_lib/prompt_monad.lem | 12 ++++++------ src/gen_lib/state.lem | 2 +- src/gen_lib/state_monad.lem | 14 +++++--------- 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 \ 'rv event \ ('rv, 'a, ' | Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \ T" | Excl_res: "((Excl_res k), e_excl_res r, k r) \ T" | Write_memv: "((Write_memv v k), e_write_memv v r, k r) \ T" -| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \ T" +| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \ T" | Footprint: "((Footprint k), e_footprint, k) \ T" | Barrier: "((Barrier bk k), e_barrier bk, k) \ T" | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \ 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') \ 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') \ 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') \ 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') \ 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') \ Traces" | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \ 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') \ Traces" | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \ 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: "\BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" "\v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s" "\BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" - "\t s. ignore_throw (write_tagS t) s = write_tagS t s" + "\BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s" "\s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\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) -- cgit v1.2.3