summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/isabelle/Prompt_monad_lemmas.thy6
-rw-r--r--lib/isabelle/State_monad_lemmas.thy2
-rw-r--r--mips/mips_extras.lem11
-rw-r--r--src/gen_lib/prompt_monad.lem12
-rw-r--r--src/gen_lib/state.lem2
-rw-r--r--src/gen_lib/state_monad.lem14
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 21:02:00 +0000