diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 12 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 2 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 14 |
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) |