diff options
Diffstat (limited to 'src/gen_lib/0.11/sail2_prompt_monad.lem')
| -rw-r--r-- | src/gen_lib/0.11/sail2_prompt_monad.lem | 336 |
1 files changed, 0 insertions, 336 deletions
diff --git a/src/gen_lib/0.11/sail2_prompt_monad.lem b/src/gen_lib/0.11/sail2_prompt_monad.lem deleted file mode 100644 index 28c0a27e..00000000 --- a/src/gen_lib/0.11/sail2_prompt_monad.lem +++ /dev/null @@ -1,336 +0,0 @@ -open import Pervasives_extra -(*open import Sail_impl_base*) -open import Sail2_instr_kinds -open import Sail2_values - -type register_name = string -type address = list bitU - -type monad 'regval 'a 'e = - | Done of 'a - (* Read a number of bytes from memory, returned in little endian order, - with or without a tag. The first nat specifies the address, the second - the number of bytes. *) - | Read_mem of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e) - | Read_memt of read_kind * nat * 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 * nat * nat * monad 'regval 'a 'e - (* Request the result of store-exclusive *) - | Excl_res of (bool -> monad 'regval 'a 'e) - (* Request to write a memory value of the given size at the given address, - with or without a tag. *) - | Write_mem of write_kind * nat * nat * list memory_byte * (bool -> monad 'regval 'a 'e) - | Write_memt of write_kind * nat * 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 *) - | Barrier of barrier_kind * monad 'regval 'a 'e - (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of register_name * ('regval -> monad 'regval 'a 'e) - (* Request to write register *) - | Write_reg of register_name * 'regval * monad 'regval 'a 'e - (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string - argument may be used to provide information to the system about what the - Boolean is going to be used for. *) - | Choose of string * (bool -> monad 'regval 'a 'e) - (* Print debugging or tracing information *) - | Print of string * monad 'regval 'a 'e - (*Result of a failed assert with possible error message to report*) - | Fail of string - (* Exception of type 'e *) - | Exception of 'e - -type event 'regval = - | E_read_mem of read_kind * nat * nat * list memory_byte - | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU) - | E_write_mem of write_kind * nat * nat * list memory_byte * bool - | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool - | E_write_ea of write_kind * nat * 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_choose of string * bool - | E_print of string - -type trace 'regval = list (event 'regval) - -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_memt rk a sz k -> Read_memt rk a sz (fun v -> bind (k v) f) - | Write_mem wk a sz v k -> Write_mem wk a sz v (fun v -> bind (k v) f) - | Write_memt wk a sz v t k -> Write_memt 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) - | Choose descr k -> Choose descr (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 -let exit () = Fail "exit" - -val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e -let choose_bool descr = Choose descr return - -val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e -let undefined_bool () = choose_bool "undefined_bool" - -val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e -let assert_exp exp msg = if exp then Done () else Fail msg - -val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e -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_memt rk a sz k -> Read_memt rk a sz (fun v -> try_catch (k v) h) - | Write_mem wk a sz v k -> Write_mem wk a sz v (fun v -> try_catch (k v) h) - | Write_memt wk a sz v t k -> Write_memt 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) - | Choose descr k -> Choose descr (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 - the return value. The exception type is "either 'r 'e", where "Right e" - represents a proper exception and "Left r" an early return of value "r". *) -type monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e) - -val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e -let early_return r = throw (Left r) - -val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e -let catch_early_return m = - try_catch m - (function - | Left a -> return a - | Right e -> throw e - end) - -(* Lift to monad with early return by wrapping exceptions *) -val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e -let liftR m = try_catch m (fun e -> throw (Right e)) - -(* Catch exceptions in the presence of early returns *) -val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) -> monadR 'rv 'a 'r 'e2 -let try_catchR m h = - try_catch m - (function - | Left r -> throw (Left r) - | Right e -> h e - end) - -val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e -let maybe_fail msg = function - | Just a -> return a - | Nothing -> Fail msg -end - -val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e -let read_memt_bytes rk addr sz = - bind - (maybe_fail "nat_of_bv" (nat_of_bv addr)) - (fun addr -> Read_memt rk addr (nat_of_int sz) return) - -val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e -let read_memt rk addr sz = - bind - (read_memt_bytes rk addr sz) - (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 read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e -let read_mem_bytes rk addr sz = - bind - (maybe_fail "nat_of_bv" (nat_of_bv addr)) - (fun addr -> Read_mem rk addr (nat_of_int sz) return) - -val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e -let read_mem rk addr_sz addr sz = - bind - (read_mem_bytes rk addr sz) - (fun bytes -> - match of_bits (bits_of_mem_bytes bytes) with - | Just v -> return v - | Nothing -> Fail "bits_of_mem_bytes" - end) - -val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e -let excl_result () = - let k successful = (return successful) in - Excl_res k - -val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e -let write_mem_ea wk addr_size addr sz = - bind - (maybe_fail "nat_of_bv" (nat_of_bv addr)) - (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ())) - -val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => - write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e -let write_mem wk addr_size addr sz v = - match (mem_bytes_of_bits v, nat_of_bv addr) with - | (Just v, Just addr) -> - Write_mem wk addr (nat_of_int sz) v return - | _ -> Fail "write_mem" - end - -val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => - write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e -let write_memt wk addr sz v tag = - match (mem_bytes_of_bits v, nat_of_bv addr) with - | (Just v, Just addr) -> - Write_memt wk addr (nat_of_int sz) v tag return - | _ -> Fail "write_mem" - end - -val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e -let read_reg reg = - let k v = - match reg.of_regval v with - | Just v -> Done v - | Nothing -> Fail "read_reg: unrecognised value" - end - in - Read_reg reg.name k - -(* TODO -val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e -let read_reg_range reg i j = - read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j)) - -let read_reg_bit reg i = - read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v -> - return (extract_only_element v) - -let read_reg_field reg regfield = - read_reg_aux (external_reg_field_whole reg regfield) - -let read_reg_bitfield reg regfield = - read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> - return (extract_only_element v)*) - -let reg_deref = read_reg - -val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e -let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) - -(* TODO -let write_reg reg v = - write_reg_aux (external_reg_whole reg) v -let write_reg_range reg i j v = - write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v -let write_reg_pos reg i v = - let iN = nat_of_int i in - write_reg_aux (external_reg_slice reg (iN,iN)) [v] -let write_reg_bit = write_reg_pos -let write_reg_field reg regfield v = - write_reg_aux (external_reg_field_whole reg regfield.field_name) v -let write_reg_field_bit reg regfield bit = - write_reg_aux (external_reg_field_whole reg regfield.field_name) - (Vector [bit] 0 (is_inc_of_reg reg)) -let write_reg_field_range reg regfield i j v = - write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v -let write_reg_field_pos reg regfield i v = - write_reg_field_range reg regfield i i [v] -let write_reg_field_bit = write_reg_field_pos*) - -val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e -let barrier bk = Barrier bk (Done ()) - -val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e -let footprint _ = Footprint (Done ()) - -(* Event traces *) - -val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e) -let emitEvent m e = match (e, m) with - | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) -> - if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing - | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) -> - if rk' = rk && a' = a && sz' = sz then Just (k vt) else Nothing - | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) -> - if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing - | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) -> - if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing - | (E_read_reg r v, Read_reg r' k) -> - if r' = r then Just (k v) else Nothing - | (E_write_reg r v, Write_reg r' v' k) -> - if r' = r && v' = v then Just k else Nothing - | (E_write_ea wk a sz, Write_ea wk' a' sz' k) -> - if wk' = wk && a' = a && sz' = sz then Just k else Nothing - | (E_barrier bk, Barrier bk' k) -> - if bk' = bk then Just k else Nothing - | (E_print m, Print m' k) -> - if m' = m then Just k else Nothing - | (E_excl_res v, Excl_res k) -> Just (k v) - | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing - | (E_footprint, Footprint k) -> Just k - | _ -> Nothing -end - -val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e) -let rec runTrace t m = match t with - | [] -> Just m - | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t') -end - -declare {isabelle} termination_argument runTrace = automatic - -val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool -let final = function - | Done _ -> true - | Fail _ -> true - | Exception _ -> true - | _ -> false -end - -val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool -let hasTrace t m = match runTrace t m with - | Just m -> final m - | Nothing -> false -end - -val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool -let hasException t m = match runTrace t m with - | Just (Exception _) -> true - | _ -> false -end - -val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool -let hasFailure t m = match runTrace t m with - | Just (Fail _) -> true - | _ -> false -end - -(* Define a type synonym that also takes the register state as a type parameter, - in order to make switching to the state monad without changing generated - definitions easier, see also lib/hol/prompt_monad.lem. *) - -type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e -type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e |