diff options
| -rw-r--r-- | src/gen_lib/sail2_prompt_monad.lem | 110 | ||||
| -rw-r--r-- | src/gen_lib/sail2_state_lifting.lem | 28 | ||||
| -rw-r--r-- | src/gen_lib/sail2_state_monad.lem | 93 |
3 files changed, 110 insertions, 121 deletions
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem index 78b1615e..991d3895 100644 --- a/src/gen_lib/sail2_prompt_monad.lem +++ b/src/gen_lib/sail2_prompt_monad.lem @@ -8,19 +8,17 @@ type address = list bitU type monad 'regval 'a 'e = | Done of 'a - (* Read a number of bytes from memory, returned in little endian order *) - | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e) - (* Read the tag of a memory address *) - | Read_tag of address * (bitU -> monad 'regval 'a 'e) - (* Tell the system a write is imminent, at address lifted, of size nat *) + (* Read a number of bytes from memory, returned in little endian order, + together with a tag. *) + | Read_mem of read_kind * address * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e) + (* Tell the system a write is imminent, at the given address and with the + given size. *) | Write_ea of write_kind * address * nat * monad 'regval 'a 'e (* Request the result of store-exclusive *) | Excl_res of (bool -> 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 given address. *) - | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e) + (* Request to write a memory value of the given size together with a tag + at the given address. *) + | Write_mem of write_kind * address * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e) (* Tell the system to dynamically recalculate dependency footprint *) | Footprint of monad 'regval 'a 'e (* Request a memory barrier *) @@ -38,26 +36,36 @@ type monad 'regval 'a 'e = (* Exception of type 'e *) | Exception of 'e +type event 'regval = + | E_read_mem of read_kind * address * nat * (list memory_byte * bitU) + | E_write_mem of write_kind * address * nat * list memory_byte * bitU * bool + | E_write_ea of write_kind * address * nat + | E_excl_res of bool + | E_barrier of barrier_kind + | E_footprint + | E_read_reg of register_name * 'regval + | E_write_reg of register_name * 'regval + | E_undefined of bool + | E_print of string + val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e let return a = Done a val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e let rec bind m f = match m with | Done a -> f a - | 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_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) - | Write_ea wk a sz k -> Write_ea wk a sz (bind k f) - | Footprint k -> Footprint (bind k f) - | Barrier bk k -> Barrier bk (bind k f) - | Write_reg r v k -> Write_reg r v (bind k f) - | Print msg k -> Print msg (bind k f) - | Fail descr -> Fail descr - | Exception e -> Exception e + | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f) + | Write_mem wk a sz v t k -> Write_mem wk a sz v 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) + | Write_ea wk a sz k -> Write_ea wk a sz (bind k f) + | Footprint k -> Footprint (bind k f) + | Barrier bk k -> Barrier bk (bind k f) + | Write_reg r v k -> Write_reg r v (bind k f) + | Print msg k -> Print msg (bind k f) + | Fail descr -> Fail descr + | Exception e -> Exception e end val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e @@ -74,21 +82,19 @@ let throw e = Exception e val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2 let rec try_catch m h = match m with - | Done a -> Done a - | 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_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) - | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h) - | Footprint k -> Footprint (try_catch k h) - | Barrier bk k -> Barrier bk (try_catch k h) - | Write_reg r v k -> Write_reg r v (try_catch k h) - | Print msg k -> Print msg (try_catch k h) - | Fail descr -> Fail descr - | Exception e -> h e + | Done a -> Done a + | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h) + | Write_mem wk a sz v t k -> Write_mem wk a sz v 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) + | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h) + | Footprint k -> Footprint (try_catch k h) + | Barrier bk k -> Barrier bk (try_catch k h) + | Write_reg r v k -> Write_reg r v (try_catch k h) + | Print msg k -> Print msg (try_catch k h) + | Fail descr -> Fail descr + | Exception e -> h e end (* For early return, we abuse exceptions by throwing and catching @@ -126,19 +132,19 @@ let maybe_fail msg = function | Nothing -> Fail msg end -val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e +val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e let read_mem_bytes rk addr sz = Read_mem rk (bits_of addr) (nat_of_int sz) return -val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e +val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e let read_mem rk addr sz = bind (read_mem_bytes rk addr sz) - (fun bytes -> - maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))) - -val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e -let read_tag addr = Read_tag (bits_of addr) return + (fun (bytes, tag) -> + match of_bits (bits_of_mem_bytes bytes) with + | Just v -> return (v, tag) + | Nothing -> Fail "bits_of_mem_bytes" + end) val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e let excl_result () = @@ -148,15 +154,13 @@ let excl_result () = val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ()) -val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e -let write_mem_val v = match mem_bytes_of_bits v with - | Just v -> Write_memv v return - | Nothing -> Fail "write_mem_val" +val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => + write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e +let write_mem wk addr sz v tag = match mem_bytes_of_bits v with + | Just v -> Write_mem wk (bits_of addr) (nat_of_int sz) v tag return + | Nothing -> Fail "write_mem" end -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 = let k v = diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem index 039343e2..42e2c0f3 100644 --- a/src/gen_lib/sail2_state_lifting.lem +++ b/src/gen_lib/sail2_state_lifting.lem @@ -9,19 +9,17 @@ open import {isabelle} `Sail2_state_monad_lemmas` val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e let rec liftState ra s = match s with - | (Done a) -> returnS a - | (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_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)) - | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k) - | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) - | (Footprint k) -> liftState ra k - | (Barrier _ k) -> liftState ra k - | (Print _ k) -> liftState ra k (* TODO *) - | (Fail descr) -> failS descr - | (Exception e) -> throwS e + | (Done a) -> returnS a + | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) + | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v 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)) + | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) + | (Write_ea _ _ _ k) -> liftState ra k + | (Footprint k) -> liftState ra k + | (Barrier _ k) -> liftState ra k + | (Print _ k) -> liftState ra k (* TODO *) + | (Fail descr) -> failS descr + | (Exception e) -> throwS e end diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem index 30b296cc..89b29fa5 100644 --- a/src/gen_lib/sail2_state_monad.lem +++ b/src/gen_lib/sail2_state_monad.lem @@ -11,17 +11,13 @@ type tagstate = map integer bitU type sequential_state 'regs = <| regstate : 'regs; memstate : memstate; - tagstate : tagstate; - write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool |> + tagstate : tagstate |> val init_state : forall 'regs. 'regs -> sequential_state 'regs let init_state regs = <| regstate = regs; memstate = Map.empty; - tagstate = Map.empty; - write_ea = Nothing; - last_exclusive_operation_was_load = false |> + tagstate = Map.empty |> type ex 'e = | Failure of string @@ -124,66 +120,57 @@ let read_tagS addr = readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate))) (* Read bytes from memory and return in little endian order *) -val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e -let read_mem_bytesS read_kind addr sz = +val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e +let read_mem_bytesS _ addr sz = maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> let sz = integerFromNat sz in let addrs = index_list addr (addr+sz-1) 1 in let read_byte s addr = Map.lookup addr s.memstate in - readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function - | Just mem_val -> - updateS (fun s -> - if read_is_exclusive read_kind - then <| s with last_exclusive_operation_was_load = true |> - else s) >>$ - returnS mem_val - | Nothing -> failS "read_memS" + let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in + readS (fun s -> + (just_list (List.map (read_byte s) addrs), + List.foldl and_bit B1 (List.map (read_tag s) addrs))) >>$= + (function + | (Just mem_val, tag) -> returnS (mem_val, tag) + | _ -> failS "read_memS" end)) -val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e +val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e let read_memS rk a sz = - read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes -> - maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes))) + read_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) -> + maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val -> + returnS (mem_val, tag))) val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e -let excl_resultS () = - readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load -> - updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$ - chooseS (if excl_load then {false; true} else {false})) - -val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e -let write_mem_eaS write_kind addr sz = +let excl_resultS = + (* TODO: This used to be more deterministic, checking a flag in the state + whether an exclusive load has occurred before. However, this does not + seem very precise; it might be safer to overapproximate the possible + behaviours by always making a nondeterministic choice. *) + undefined_boolS + +(* Write little-endian list of bytes to given address *) +val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e +let write_mem_bytesS _ addr sz v t = maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> let sz = integerFromNat sz in - updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)) - -(* Write little-endian list of bytes to previously announced address *) -val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e -let write_mem_bytesS v = - readS (fun s -> s.write_ea) >>$= (function - | Nothing -> failS "write ea has not been announced yet" - | Just (_, addr, sz) -> - let addrs = index_list addr (addr+sz-1) 1 in - (*let v = external_mem_value (bits_of v) in*) - let a_v = List.zip addrs v in - let write_byte mem (addr, v) = Map.insert addr v mem in - updateS (fun s -> - <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$ - returnS true - end) - -val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e -let write_mem_valS v = match mem_bytes_of_bits v with - | Just v -> write_mem_bytesS v - | Nothing -> failS "write_mem_val" + let addrs = index_list addr (addr+sz-1) 1 in + (*let v = external_mem_value (bits_of v) in*) + let a_v = List.zip addrs v in + let write_byte mem (addr, v) = Map.insert addr v mem in + let write_tag mem addr = Map.insert addr t mem in + updateS (fun s -> + <| s with memstate = List.foldl write_byte s.memstate a_v; + tagstate = List.foldl write_tag s.tagstate addrs |>) >>$ + returnS true) + +val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => + write_kind -> 'a -> nat -> 'b -> bitU -> monadS 'regs bool 'e +let write_memS wk addr sz v t = match mem_bytes_of_bits v with + | Just v -> write_mem_bytesS wk addr sz v t + | Nothing -> failS "write_mem" end -val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e -let write_tagS addr t = - maybe_failS "unsigned" (unsigned addr) >>$= (fun addr -> - updateS (fun s -> <| s with tagstate = Map.insert 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) |