diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 73 | ||||
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 39 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 58 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 133 | ||||
| -rw-r--r-- | src/gen_lib/state_monad.lem | 174 |
5 files changed, 198 insertions, 279 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 756bb699..728014eb 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -10,81 +10,38 @@ let rec iter_aux i f xs = match xs with | [] -> return () end +declare {isabelle} termination_argument iter_aux = automatic + val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e let iteri f xs = iter_aux 0 f xs val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e let iter f xs = iteri (fun _ x -> f x) xs +val foreachM : forall 'a 'rv 'vars 'e. + list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e +let rec foreachM [] vars _ = return vars +and foreachM (x :: xs) vars body = + body x vars >>= fun vars -> + foreachM xs vars body -val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec foreachM_inc (i,stop,by) vars body = - if (by > 0 && i <= stop) || (by < 0 && stop <= i) - then - body i vars >>= fun vars -> - foreachM_inc (i + by,stop,by) vars body - else return vars - - -val foreachM_dec : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec foreachM_dec (i,stop,by) vars body = - if (by > 0 && i >= stop) || (by < 0 && stop >= i) - then - body i vars >>= fun vars -> - foreachM_dec (i - by,stop,by) vars body - else return vars - -val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars -let rec while_PP vars cond body = - if cond vars then while_PP (body vars) cond body else vars - -val while_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec while_PM vars cond body = - if cond vars then - body vars >>= fun vars -> while_PM vars cond body - else return vars +declare {isabelle} termination_argument foreachM = automatic -val while_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> - ('vars -> 'vars) -> monad 'rv 'vars 'e -let rec while_MP vars cond body = - cond vars >>= fun cond_val -> - if cond_val then while_MP (body vars) cond body else return vars -val while_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> +val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec while_MM vars cond body = +let rec whileM vars cond body = cond vars >>= fun cond_val -> if cond_val then - body vars >>= fun vars -> while_MM vars cond body + body vars >>= fun vars -> whileM vars cond body else return vars -val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars -let rec until_PP vars cond body = - let vars = body vars in - if (cond vars) then vars else until_PP (body vars) cond body - -val until_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec until_PM vars cond body = - body vars >>= fun vars -> - if (cond vars) then return vars else until_PM vars cond body - -val until_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> - ('vars -> 'vars) -> monad 'rv 'vars 'e -let rec until_MP vars cond body = - let vars = body vars in - cond vars >>= fun cond_val -> - if cond_val then return vars else until_MP vars cond body - -val until_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> +val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec until_MM vars cond body = +let rec untilM vars cond body = body vars >>= fun vars -> cond vars >>= fun cond_val -> - if cond_val then return vars else until_MM vars cond body + if cond_val then return vars else untilM vars cond body (*let write_two_regs r1 r2 vec = let is_inc = diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index 38f79868..3c414d6e 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -4,17 +4,25 @@ open import Sail_instr_kinds open import Sail_values type register_name = string +type address = list bitU type monad 'regval 'a 'e = | Done of 'a - | Read_mem of read_kind * integer * integer * (list memory_byte -> monad 'regval 'a 'e) + (* 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 *) - | Write_ea of write_kind * integer * integer * monad 'regval 'a 'e + | 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 *) + 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) + (* 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 *) @@ -35,10 +43,13 @@ val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> mo 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_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) | 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) | Fail descr -> Fail descr @@ -63,10 +74,13 @@ val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 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_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) | 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) | Fail descr -> Fail descr @@ -106,11 +120,8 @@ let try_catchR m h = val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e let read_mem rk addr sz = - let addr = unsigned addr in - let k bytes = - let bitv = bits_of_bytes (List.reverse bytes) in - (Done bitv) in - Read_mem rk addr sz k + let k bytes = Done (bits_of_mem_bytes bytes) in + Read_mem rk (bits_of addr) (natFromInteger sz) k val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e let excl_result () = @@ -118,13 +129,11 @@ let excl_result () = Excl_res k 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 (unsigned addr) sz (Done ()) +let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (natFromInteger sz) (Done ()) val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e -let write_mem_val v = match bytes_of_bits v with - | Just v -> - let k successful = (return successful) in - Write_memv (List.reverse v) k +let write_mem_val v = match mem_bytes_of_bits v with + | Just v -> Write_memv v return | Nothing -> Fail "write_mem_val" end @@ -182,5 +191,5 @@ 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. monad 'rv unit 'e -let footprint = Footprint (Done ())*) +val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e +let footprint _ = Footprint (Done ()) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index b981bb91..ead63d62 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -205,18 +205,15 @@ let rec bits_of_nat_aux x = declare {isabelle} termination_argument bits_of_nat_aux = automatic let bits_of_nat n = List.reverse (bits_of_nat_aux n) -val nat_of_bits : list bitU -> natural -let nat_of_bits bits = - let (sum,_) = - List.foldr - (fun b (acc,exp) -> - match b with - | B1 -> (acc + naturalPow 2 exp, exp + 1) - | B0 -> (acc, exp + 1) - | BU -> failwith "nat_of_bits: bitvector has undefined bits" - end) - (0,0) bits in - sum +val nat_of_bits_aux : natural -> list bitU -> natural +let rec nat_of_bits_aux acc bs = match bs with + | [] -> acc + | B1 :: bs -> nat_of_bits_aux ((2 * acc) + 1) bs + | B0 :: bs -> nat_of_bits_aux (2 * acc) bs + | BU :: _ -> failwith "nat_of_bits_aux: bit list has undefined bits" +end +declare {isabelle} termination_argument nat_of_bits_aux = automatic +let nat_of_bits bits = nat_of_bits_aux 0 bits let not_bits = List.map not_bit @@ -543,6 +540,9 @@ let bytes_of_bits bs = byte_chunks (bits_of bs) val bits_of_bytes : forall 'a. Bitvector 'a => list memory_byte -> 'a let bits_of_bytes bs = of_bits (List.concat (List.map bits_of bs)) +let mem_bytes_of_bits bs = Maybe.map List.reverse (bytes_of_bits bs) +let bits_of_mem_bytes bs = bits_of_bytes (List.reverse bs) + (*val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU let bitv_of_byte_lifteds v = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v @@ -612,7 +612,7 @@ type register_ref 'regstate 'regval 'a = <| name : string; (*is_inc : bool;*) read_from : 'regstate -> 'a; - write_to : 'regstate -> 'a -> 'regstate; + write_to : 'a -> 'regstate -> 'regstate; of_regval : 'regval -> maybe 'a; regval_of : 'a -> 'regval |> @@ -750,24 +750,28 @@ let internal_mem_value bytes = List.reverse bytes $> bitv_of_byte_lifteds*) +val foreach : forall 'a 'vars. + (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars +let rec foreach [] vars _ = vars +and foreach (x :: xs) vars body = foreach xs (body x vars) body + +declare {isabelle} termination_argument foreach = automatic +val index_list : integer -> integer -> integer -> list integer +let rec index_list from to step = + if (step > 0 && from <= to) || (step < 0 && to <= from) then + from :: index_list (from + step) to step + else [] +val while : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars +let rec while vars cond body = + if cond vars then while (body vars) cond body else vars -val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_inc (i,stop,by) vars body = - if (by > 0 && i <= stop) || (by < 0 && stop <= i) - then let vars = body i vars in - foreach_inc (i + by,stop,by) vars body - else vars +val until : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars +let rec until vars cond body = + let vars = body vars in + if cond vars then vars else until (body vars) cond body -val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_dec (i,stop,by) vars body = - if (by > 0 && i >= stop) || (by < 0 && stop >= i) - then let vars = body i vars in - foreach_dec (i - by,stop,by) vars body - else vars let assert' b msg_opt = let msg = match msg_opt with diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index fba8d9b7..1740174e 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -11,12 +11,15 @@ open import {isabelle} `State_monad_extras` 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_memS rk a sz) (fun v -> liftState ra (k v)) - | (Write_memv descr k) -> bindS (write_mem_valS descr) (fun v -> liftState ra (k v)) - | (Read_reg descr k) -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v)) - | (Excl_res k) -> bindS (excl_resultS ()) (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) + | (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)) + | (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)) + | (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 | (Fail descr) -> failS descr | (Error descr) -> failS descr @@ -24,99 +27,43 @@ let rec liftState ra s = match s with end -(* TODO -val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e -let rec iter_aux i f xs = match xs with - | x :: xs -> f i x >> iter_aux (i + 1) f xs - | [] -> return () +val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e +let rec iterS_aux i f xs = match xs with + | x :: xs -> f i x >>$ iterS_aux (i + 1) f xs + | [] -> returnS () end -val iteri : forall 'regs 'e 'a. (integer -> 'a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e -let iteri f xs = iter_aux 0 f xs +declare {isabelle} termination_argument iterS_aux = automatic -val iter : forall 'regs 'e 'a. ('a -> M 'regs unit 'e) -> list 'a -> M 'regs unit 'e -let iter f xs = iteri (fun _ x -> f x) xs +val iteriS : forall 'rv 'a 'e. (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e +let iteriS f xs = iterS_aux 0 f xs -val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec foreachM_inc (i,stop,by) vars body = - if (by > 0 && i <= stop) || (by < 0 && stop <= i) - then - body i vars >>= fun vars -> - foreachM_inc (i + by,stop,by) vars body - else return vars +val iterS : forall 'rv 'a 'e. ('a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e +let iterS f xs = iteriS (fun _ x -> f x) xs +val foreachS : forall 'a 'rv 'vars 'e. + list 'a -> 'vars -> ('a -> 'vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e +let rec foreachS xs vars body = match xs with + | [] -> returnS vars + | x :: xs -> + body x vars >>$= fun vars -> + foreachS xs vars body +end -val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec foreachM_dec (i,stop,by) vars body = - if (by > 0 && i >= stop) || (by < 0 && stop >= i) - then - body i vars >>= fun vars -> - foreachM_dec (i - by,stop,by) vars body - else return vars - -val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars -let rec while_PP vars cond body = - if cond vars then while_PP (body vars) cond body else vars - -val while_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec while_PM vars cond body s = - if cond vars then - bind (body vars) (fun vars s' -> while_PM vars cond body s') s - else return vars s - -val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> - ('vars -> 'vars) -> M 'regs 'vars 'e -let rec while_MP vars cond body s = - bind - (cond vars) - (fun cond_val s' -> - if cond_val then while_MP (body vars) cond body s' else return vars s') s - -val while_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> - ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec while_MM vars cond body s = - bind - (cond vars) - (fun cond_val s' -> - if cond_val then - bind - (body vars) - (fun vars s'' -> while_MM vars cond body s'') s' - else return vars s') s - -val until_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars -let rec until_PP vars cond body = - let vars = body vars in - if (cond vars) then vars else until_PP (body vars) cond body +declare {isabelle} termination_argument foreachS = automatic -val until_PM : forall 'regs 'vars 'e. 'vars -> ('vars -> bool) -> - ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec until_PM vars cond body s = - bind - (body vars) - (fun vars s' -> - if (cond vars) then return vars s' else until_PM vars cond body s') s -val until_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> - ('vars -> 'vars) -> M 'regs 'vars 'e -let rec until_MP vars cond body s = - let vars = body vars in - bind - (cond vars) - (fun cond_val s' -> - if cond_val then return vars s' else until_MP vars cond body s') s +val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) -> + ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e +let rec whileS vars cond body s = + (cond vars >>$= (fun cond_val s' -> + if cond_val then + (body vars >>$= (fun vars s'' -> whileS vars cond body s'')) s' + else returnS vars s')) s -val until_MM : forall 'regs 'vars 'e. 'vars -> ('vars -> M 'regs bool 'e) -> - ('vars -> M 'regs 'vars 'e) -> M 'regs 'vars 'e -let rec until_MM vars cond body s = - bind - (body vars) - (fun vars s' -> - bind - (cond vars) - (fun cond_val s''-> - if cond_val then return vars s'' else until_MM vars cond body s'') s') s -*) +val untilS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) -> + ('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e +let rec untilS vars cond body s = + (body vars >>$= (fun vars s' -> + (cond vars >>$= (fun cond_val s'' -> + if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index f324a9f4..8ff39d62 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -24,7 +24,6 @@ let init_state regs = last_exclusive_operation_was_load = false |> type ex 'e = - | Exit | Failure of string | Throw of 'e @@ -49,12 +48,24 @@ let bindS m f (s : sequential_state 'regs) = val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e let seqS m n = bindS m (fun (_ : unit) -> n) -val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e -let exitS () s = [(Ex Exit, s)] +let inline (>>$=) = bindS +let inline (>>$) = seqS + +val chooseS : forall 'regs 'a 'e. list 'a -> monadS 'regs 'a 'e +let chooseS xs s = List.map (fun x -> (Value x, s)) xs + +val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e +let readS f = (fun s -> returnS (f s) s) + +val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e +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 exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e +let exitS () = failS "exit" + val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e let throwS e s = [(Ex (Throw e), s)] @@ -63,7 +74,6 @@ let try_catchS m h s = List.concatMap (function | (Value a, s') -> returnS a s' | (Ex (Throw e), s') -> h e s' - | (Ex Exit, s') -> [(Ex Exit, s')] | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')] end) (m s) @@ -99,85 +109,77 @@ let try_catchSR m h = | Right e -> h e end) -val range : integer -> integer -> list integer -let rec range i j = - if j < i then [] - else if i = j then [i] - else i :: range (i+1) j - -val get_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a -let get_regS state reg = reg.read_from state.regstate - -val set_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a -> sequential_state 'regs -let set_regS state reg v = - <| state with regstate = reg.write_to state.regstate v |> - - -val read_memS : forall 'regs 'e. read_kind -> integer -> integer -> monadS 'regs (list memory_byte) 'e -let read_memS read_kind addr sz s = - (*let addr = unsigned (bitv_of_address_lifted addr) in - let sz = integerFromNat sz in*) - let addrs = range addr (addr+sz-1) in - match just_list (List.map (fun addr -> Map.lookup addr s.memstate) addrs) with +val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e +let read_tagS addr = + readS (fun s -> fromMaybe B0 (Map.lookup (unsigned 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 = + let addr = unsigned addr in + 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 -> - let s' = + updateS (fun s -> if read_is_exclusive read_kind then <| s with last_exclusive_operation_was_load = true |> - else s - in - returnS (List.reverse mem_val) s' - | Nothing -> failS "read_memS" s - end - -(* caps are aligned at 32 bytes *) -let cap_alignment = (32 : integer) - -val read_tagS : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> monadS 'regs bitU 'e -let read_tagS read_kind addr state = - let addr = (unsigned addr) / cap_alignment in - let tag = match (Map.lookup addr state.tagstate) with - | Just t -> t - | Nothing -> B0 - end in - if read_is_exclusive read_kind - then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)] - else [(Value tag, state)] + else s) >>$ + returnS mem_val + | Nothing -> failS "read_memS" + end) + +val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e +let read_memS rk a sz = + read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes -> + returnS (bits_of_mem_bytes bytes)) val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e -let excl_resultS () state = - let success = - (Value true, <| state with last_exclusive_operation_was_load = false |>) in - (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else [] - -val write_mem_eaS : forall 'regs 'e. write_kind -> integer -> integer -> monadS 'regs unit 'e -let write_mem_eaS write_kind addr sz state = - (*let addr = unsigned (bitv_of_address_lifted addr) in - let sz = integerFromNat sz in*) - [(Value (), <| state with write_ea = Just (write_kind, addr, sz) |>)] - -val write_mem_valS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e -let write_mem_valS v state = - let (_,addr,sz) = match state.write_ea with - | Nothing -> failwith "write ea has not been announced yet" - | Just write_ea -> write_ea end in - let addrs = range addr (addr+sz-1) in - (*let v = external_mem_value (bits_of v) in*) - let addresses_with_value = List.zip addrs (List.reverse v) in - let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) - state.memstate addresses_with_value in - [(Value true, <| state with memstate = memstate |>)] +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 addr = unsigned addr in + 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" +end val write_tagS : forall 'regs 'e. bitU -> monadS 'regs bool 'e -let write_tagS t state = - let (_,addr,_) = match state.write_ea with - | Nothing -> failwith "write ea has not been announced yet" - | Just write_ea -> write_ea end in - let taddr = addr / cap_alignment in - let tagstate = Map.insert taddr t state.tagstate in - [(Value true, <| state with tagstate = tagstate |>)] +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 read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e -let read_regS reg s = [(Value (reg.read_from s.regstate), s)] +let read_regS reg = readS (fun s -> reg.read_from s.regstate) (* TODO let read_reg_range reg i j state = @@ -195,23 +197,23 @@ let read_reg_bitfield reg regfield = val read_regvalS : forall 'regs 'rv 'e. register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e -let read_regvalS (read, _) reg s = - match read reg s.regstate with - | Just v -> returnS v s - | Nothing -> failS ("read_regvalS " ^ reg) s - end +let read_regvalS (read, _) reg = + readS (fun s -> read reg s.regstate) >>$= (function + | Just v -> returnS v + | Nothing -> failS ("read_regvalS " ^ reg) + end) val write_regvalS : forall 'regs 'rv 'e. register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e -let write_regvalS (_, write) reg v s = - match write reg v s.regstate with - | Just rs' -> returnS () (<| s with regstate = rs' |>) - | Nothing -> failS ("write_regvalS " ^ reg) s - end +let write_regvalS (_, write) reg v = + readS (fun s -> write reg v s.regstate) >>$= (function + | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>) + | Nothing -> failS ("write_regvalS " ^ reg) + end) val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e -let write_regS reg v state = - [(Value (), <| state with regstate = reg.write_to state.regstate v |>)] +let write_regS reg v = + updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>) (* TODO val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e |