diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt.lem | 13 | ||||
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 6 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 19 |
5 files changed, 36 insertions, 4 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 9642c714..1d8623df 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -30,6 +30,19 @@ end declare {isabelle} termination_argument foreachM = automatic +val bool_of_bitU_undef : forall 'rv 'e. bitU -> monad 'rv bool 'e +let bool_of_bitU_undef = function + | B0 -> return false + | B1 -> return true + | BU -> undefined_bool () +end + +val bools_of_bitUs : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e +let bools_of_bitUs bits = + foreachM bits [] + (fun b bools -> + bool_of_bitU_undef b >>= (fun b -> + return (bools ++ [b]))) val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 0966f911..b4b8436f 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -29,6 +29,7 @@ type monad 'regval 'a 'e = | Read_reg of register_name * ('regval -> monad 'regval 'a 'e) (* Request to write register *) | Write_reg of register_name * 'regval * monad 'regval 'a 'e + | Undefined of (bool -> monad 'regval 'a 'e) (*Result of a failed assert with possible error message to report*) | Fail of string | Error of string @@ -48,6 +49,7 @@ let rec bind m f = match m with | Write_tagv t k -> Write_tagv 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) @@ -64,6 +66,9 @@ let inline (>>) m n = m >>= fun (_ : unit) -> n val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e let exit () = Fail "exit" +val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e +let undefined_bool () = Undefined return + val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e let assert_exp exp msg = if exp then Done () else Fail msg @@ -79,6 +84,7 @@ let rec try_catch m h = match m with | Write_tagv t k -> Write_tagv 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) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index fce595e0..edb8da88 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -622,6 +622,7 @@ type register_ref 'regstate 'regval 'a = of_regval : 'regval -> maybe 'a; regval_of : 'a -> 'regval |> +(* Register accessors: pair of functions for reading and writing register values *) type register_accessors 'regstate 'regval = ((string -> 'regstate -> maybe 'regval) * (string -> 'regval -> 'regstate -> maybe 'regstate)) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 1366e605..85fa15e8 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -17,6 +17,7 @@ let rec liftState ra s = match s with | (Write_tagv t k) -> bindS (write_tagS 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 diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 8ff39d62..26179244 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -13,15 +13,20 @@ type sequential_state 'regs = memstate : memstate; tagstate : tagstate; write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool|> + last_exclusive_operation_was_load : bool; + (* Random bool generator for use as an undefined bit oracle *) + next_bool : nat -> (bool * nat); + seed : nat |> -val init_state : forall 'regs. 'regs -> sequential_state 'regs -let init_state regs = +val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs +let init_state regs o s = <| regstate = regs; memstate = Map.empty; tagstate = Map.empty; write_ea = Nothing; - last_exclusive_operation_was_load = false |> + last_exclusive_operation_was_load = false; + next_bool = o; + seed = s |> type ex 'e = | Failure of string @@ -63,6 +68,12 @@ let updateS f = (fun s -> returnS () (f s)) val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e let failS msg s = [(Ex (Failure msg), s)] +val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e +let undefined_boolS () = + readS (fun s -> s.next_bool (s.seed)) >>$= (fun (b, seed) -> + updateS (fun s -> <| s with seed = seed |>) >>$ + returnS b) + val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e let exitS () = failS "exit" |