diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 186 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 495 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 601 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 763 | ||||
| -rw-r--r-- | src/gen_lib/sail_values_word.lem | 1030 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 280 |
6 files changed, 1701 insertions, 1654 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 426b0811..e9684414 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -2,10 +2,13 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values -val return : forall 'a. 'a -> outcome 'a +type MR 'a 'r = outcome_r 'a 'r +type M 'a = outcome 'a + +val return : forall 'a 'r. 'a -> MR 'a 'r let return a = Done a -val bind : forall 'a 'b. outcome 'a -> ('a -> outcome 'b) -> outcome 'b +val bind : forall 'a 'b 'r. MR 'a 'r -> ('a -> MR 'b 'r) -> MR 'b 'r let rec bind m f = match m with | Done a -> f a | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (bind o f,opt)) @@ -19,25 +22,65 @@ let rec bind m f = match m with | Escape descr -> Escape descr | Fail descr -> Fail descr | Error descr -> Error descr + | Return a -> Return a | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (bind o f ,opt)) end - -type M 'a = outcome 'a - let inline (>>=) = bind -val (>>) : forall 'b. M unit -> M 'b -> M 'b +val (>>) : forall 'b 'r. MR unit 'r -> MR 'b 'r -> MR 'b 'r let inline (>>) m n = m >>= fun _ -> n val exit : forall 'a 'b. 'b -> M 'a let exit s = Fail Nothing -val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU) +val assert_exp : bool -> string -> M unit +let assert_exp exp msg = if exp then Done () else Fail (Just msg) + +val early_return : forall 'r. 'r -> MR unit 'r +let early_return r = Return r + +val liftR : forall 'a 'r. M 'a -> MR 'a 'r +let rec liftR m = match m with + | Done a -> Done a + | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (liftR o,opt)) + | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (liftR o,opt)) + | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (liftR o,opt)) + | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (liftR o,opt)) + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (liftR o,opt)) + | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (liftR o,opt)) + | Footprint o_s -> Footprint (let (o,opt) = o_s in (liftR o,opt)) + | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (liftR o,opt)) + | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (liftR o,opt)) + | Escape descr -> Escape descr + | Fail descr -> Fail descr + | Error descr -> Error descr + | Return _ -> Error "uncaught early return" +end + +val catch_early_return : forall 'a 'r. MR 'a 'a -> M 'a +let rec catch_early_return m = match m with + | Done a -> Done a + | Read_mem descr k -> Read_mem descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) + | Read_reg descr k -> Read_reg descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) + | Write_memv descr k -> Write_memv descr (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) + | Excl_res k -> Excl_res (fun v -> let (o,opt) = k v in (catch_early_return o,opt)) + | Write_ea descr o_s -> Write_ea descr (let (o,opt) = o_s in (catch_early_return o,opt)) + | Barrier descr o_s -> Barrier descr (let (o,opt) = o_s in (catch_early_return o,opt)) + | Footprint o_s -> Footprint (let (o,opt) = o_s in (catch_early_return o,opt)) + | Write_reg descr o_s -> Write_reg descr (let (o,opt) = o_s in (catch_early_return o,opt)) + | Internal descr o_s -> Internal descr (let (o,opt) = o_s in (catch_early_return o,opt)) + | Escape descr -> Escape descr + | Fail descr -> Fail descr + | Error descr -> Error descr + | Return a -> Done a +end + +val read_mem : forall 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b let read_mem dir rk addr sz = - let addr = address_lifted_of_bitv addr in + let addr = address_lifted_of_bitv (bits_of addr) in let sz = natFromInteger sz in let k memory_value = - let bitv = internal_mem_value dir memory_value in + let bitv = of_bits (internal_mem_value dir memory_value) in (Done bitv,Nothing) in Read_mem (rk,addr,sz) k @@ -46,22 +89,22 @@ let excl_result () = let k successful = (return successful,Nothing) in Excl_res k -val write_mem_ea : write_kind -> vector bitU -> integer -> M unit +val write_mem_ea : forall 'a. Bitvector 'a => write_kind -> 'a -> integer -> M unit let write_mem_ea wk addr sz = - let addr = address_lifted_of_bitv addr in + let addr = address_lifted_of_bitv (bits_of addr) in let sz = natFromInteger sz in Write_ea (wk,addr,sz) (Done (),Nothing) -val write_mem_val : vector bitU -> M bool +val write_mem_val : forall 'a. Bitvector 'a => 'a -> M bool let write_mem_val v = - let v = external_mem_value v in + let v = external_mem_value (bits_of v) in let k successful = (return successful,Nothing) in Write_memv v k -val read_reg_aux : reg_name -> M (vector bitU) +val read_reg_aux : forall 'a. Bitvector 'a => reg_name -> M 'a let read_reg_aux reg = let k reg_value = - let v = internal_reg_value reg_value in + let v = of_bits (internal_reg_value reg_value) in (Done v,Nothing) in Read_reg reg k @@ -71,34 +114,40 @@ let read_reg_range reg i j = read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) let read_reg_bit reg i = read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v -> - return (extract_only_bit v) + return (extract_only_element v) let read_reg_field reg regfield = - read_reg_aux (external_reg_field_whole reg regfield) + read_reg_aux (external_reg_field_whole reg regfield.field_name) let read_reg_bitfield reg regfield = - read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> - return (extract_only_bit v) + read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v -> + return (extract_only_element v) -val write_reg_aux : reg_name -> vector bitU -> M unit +let reg_deref = read_reg + +val write_reg_aux : forall 'a. Bitvector 'a => reg_name -> 'a -> M unit let write_reg_aux reg_name v = - let regval = external_reg_value reg_name v in + let regval = external_reg_value reg_name (bits_of v) in Write_reg (reg_name,regval) (Done (), Nothing) 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 (natFromInteger i,natFromInteger j)) v -let write_reg_bit reg i bit = +let write_reg_pos reg i v = let iN = natFromInteger i in - write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg)) + 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) v -let write_reg_bitfield reg regfield bit = - write_reg_aux (external_reg_field_whole reg regfield) - (Vector [bit] 0 (is_inc_of_reg reg)) + 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 (natFromInteger i,natFromInteger j)) v - + write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger 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 +let write_reg_ref (reg, v) = write_reg reg v val barrier : barrier_kind -> M unit let barrier bk = Barrier bk (Done (), Nothing) @@ -108,26 +157,89 @@ val footprint : M unit let footprint = Footprint (Done (),Nothing) -val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'vars) -> M 'vars +val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e +let rec iter_aux i f xs = match xs with + | x :: xs -> f i x >> iter_aux (i + 1) f xs + | [] -> return () + end + +val iteri : forall 'regs 'e 'a. (integer -> 'a -> MR unit 'e) -> list 'a -> MR unit 'e +let iteri f xs = iter_aux 0 f xs + +val iter : forall 'regs 'e 'a. ('a -> MR unit 'e) -> list 'a -> MR unit 'e +let iter f xs = iteri (fun _ x -> f x) xs + + +val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r let rec foreachM_inc (i,stop,by) vars body = - if i <= stop + 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 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'vars) -> M 'vars +val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r let rec foreachM_dec (i,stop,by) vars body = - if i >= stop + 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 -let write_two_regs r1 r2 vec = +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 'vars 'r. 'vars -> ('vars -> bool) -> + ('vars -> MR 'vars 'r) -> MR 'vars 'r +let rec while_PM vars cond body = + if cond vars then + body vars >>= fun vars -> while_PM vars cond body + else return vars + +val while_MP : forall 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> + ('vars -> 'vars) -> MR 'vars 'r +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 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> + ('vars -> MR 'vars 'r) -> MR 'vars 'r +let rec while_MM vars cond body = + cond vars >>= fun cond_val -> + if cond_val then + body vars >>= fun vars -> while_MM 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 'vars 'r. 'vars -> ('vars -> bool) -> + ('vars -> MR 'vars 'r) -> MR 'vars 'r +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 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> + ('vars -> 'vars) -> MR 'vars 'r +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 'vars 'r. 'vars -> ('vars -> MR bool 'r) -> + ('vars -> MR 'vars 'r) -> MR 'vars 'r +let rec until_MM vars cond body = + body vars >>= fun vars -> + cond vars >>= fun cond_val -> + if cond_val then return vars else until_MM vars cond body + +(*let write_two_regs r1 r2 vec = let is_inc = let is_inc_r1 = is_inc_of_reg r1 in let is_inc_r2 = is_inc_of_reg r2 in @@ -146,4 +258,4 @@ let write_two_regs r1 r2 vec = if is_inc then slice vec (size_r1 - start_vec) (size_vec - start_vec) else slice vec (start_vec - size_r1) (start_vec - size_vec) in - write_reg r1 r1_v >> write_reg r2 r2_v + write_reg r1 r1_v >> write_reg r2 r2_v*) diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem new file mode 100644 index 00000000..826ea98f --- /dev/null +++ b/src/gen_lib/sail_operators.lem @@ -0,0 +1,495 @@ +open import Pervasives_extra +open import Machine_word +open import Sail_impl_base +open import Sail_values + +(*** Bit vector operations *) + +let bitvector_length = length + +let set_bitvector_start = set_vector_start +let reset_bitvector_start = reset_vector_start + +let set_bitvector_start_to_length = set_vector_start_to_length + +let bitvector_concat = vector_concat +let inline (^^^) = bitvector_concat + +let bitvector_subrange_inc = vector_subrange_inc +let bitvector_subrange_dec = vector_subrange_dec + +let vector_subrange_bl (start, v, i, j) = + let v' = slice v i j in + get_elems v' +let vector_subrange_bl_dec = vector_subrange_bl + +let bitvector_access_inc = vector_access_inc +let bitvector_access_dec = vector_access_dec +let bitvector_update_pos_inc = vector_update_pos_inc +let bitvector_update_pos_dec = vector_update_pos_dec +let bitvector_update_subrange_inc = vector_update_subrange_inc +let bitvector_update_subrange_dec = vector_update_subrange_dec + +let extract_only_bit = extract_only_element + +let norm_dec = reset_vector_start +let adjust_start_index (start, v) = set_vector_start (start, v) + +let cast_vec_bool v = bitU_to_bool (extract_only_element v) +let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false +let cast_boolvec_bitvec (Vector bs start inc) = + Vector (List.map bool_to_bitU bs) start inc +let cast_vec_bl (Vector bs start inc) = bs + +let pp_bitu_vector (Vector elems start inc) = + let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in + "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc + + +let most_significant = function + | (Vector (b :: _) _ _) -> b + | _ -> failwith "most_significant applied to empty vector" + end + +let bitwise_not (Vector bs start is_inc) = + Vector (bitwise_not_bitlist bs) start is_inc + +let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) = + let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in + Vector (reverse revbs) start is_inc + +let bitwise_and = bitwise_binop (&&) +let bitwise_or = bitwise_binop (||) +let bitwise_xor = bitwise_binop xor + +let unsigned_big = unsigned + +let signed v : integer = + match most_significant v with + | B1 -> 0 - (1 + (unsigned (bitwise_not v))) + | B0 -> unsigned v + | BU -> failwith "signed applied to vector with undefined bits" + end + +let hardware_mod (a: integer) (b:integer) : integer = + if a < 0 && b < 0 + then (abs a) mod (abs b) + else if (a < 0 && b >= 0) + then (a mod b) - b + else a mod b + +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) +let hardware_quot (a:integer) (b:integer) : integer = + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) + +let quot_signed = hardware_quot + + +let signed_big = signed + +let to_num sign = if sign then signed else unsigned + +let max_64u = (integerPow 2 64) - 1 +let max_64 = (integerPow 2 63) - 1 +let min_64 = 0 - (integerPow 2 63) +let max_32u = (4294967295 : integer) +let max_32 = (2147483647 : integer) +let min_32 = (0 - 2147483648 : integer) +let max_8 = (127 : integer) +let min_8 = (0 - 128 : integer) +let max_5 = (31 : integer) +let min_5 = (0 - 32 : integer) + +let get_max_representable_in sign (n : integer) : integer = + if (n = 64) then match sign with | true -> max_64 | false -> max_64u end + else if (n=32) then match sign with | true -> max_32 | false -> max_32u end + else if (n=8) then max_8 + else if (n=5) then max_5 + else match sign with | true -> integerPow 2 ((natFromInteger n) -1) + | false -> integerPow 2 (natFromInteger n) + end + +let get_min_representable_in _ (n : integer) : integer = + if n = 64 then min_64 + else if n = 32 then min_32 + else if n = 8 then min_8 + else if n = 5 then min_5 + else 0 - (integerPow 2 (natFromInteger n)) + +let to_norm_vec is_inc ((len : integer),(n : integer)) = + let start = if is_inc then 0 else len - 1 in + Vector (bits_of_int (len, n)) start is_inc + +let to_vec_big = to_norm_vec + +let to_vec_inc (start, len, n) = set_vector_start (start, to_norm_vec true (len, n)) +let to_vec_norm_inc (len, n) = to_norm_vec true (len, n) +let to_vec_dec (start, len, n) = set_vector_start (start, to_norm_vec false (len, n)) +let to_vec_norm_dec (len, n) = to_norm_vec false (len, n) + +let cast_0_vec = to_vec_dec +let cast_1_vec = to_vec_dec +let cast_01_vec = to_vec_dec + +let to_vec_undef is_inc (len : integer) = + Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc + +let to_vec_inc_undef = to_vec_undef true +let to_vec_dec_undef = to_vec_undef false + +let exts (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,signed vec)) +let extz (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,unsigned vec)) + +let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec)) +let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec)) + +(* TODO *) +let extz_bl (start, len, bits) = Vector bits start false +let exts_bl (start, len, bits) = Vector bits start false + + +let quot = hardware_quot +let modulo (l,r) = hardware_mod l r + +let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = + let (l',r') = (to_num sign l, to_num sign r) in + let n = op l' r' in + to_norm_vec is_inc (size * (length l),n) + + +(* add_vec + * add_vec_signed + * minus_vec + * multiply_vec + * multiply_vec_signed + *) +let add_VVV = arith_op_vec integerAdd false 1 +let addS_VVV = arith_op_vec integerAdd true 1 +let minus_VVV = arith_op_vec integerMinus false 1 +let mult_VVV = arith_op_vec integerMult false 2 +let multS_VVV = arith_op_vec integerMult true 2 + +let mult_vec (l, r) = mult_VVV l r +let mult_svec (l, r) = multS_VVV l r + +let add_vec (l, r) = add_VVV l r +let sub_vec (l, r) = minus_VVV l r + +let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r = + arith_op_vec op sign size l (to_norm_vec is_inc (length l,r)) + +(* add_vec_range + * add_vec_range_signed + * minus_vec_range + * mult_vec_range + * mult_vec_range_signed + *) +let add_VIV = arith_op_vec_range integerAdd false 1 +let addS_VIV = arith_op_vec_range integerAdd true 1 +let minus_VIV = arith_op_vec_range integerMinus false 1 +let mult_VIV = arith_op_vec_range integerMult false 2 +let multS_VIV = arith_op_vec_range integerMult true 2 + +let add_vec_int (l, r) = add_VIV l r +let sub_vec_int (l, r) = minus_VIV l r + +let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) = + arith_op_vec op sign size (to_norm_vec is_inc (length r, l)) r + +(* add_range_vec + * add_range_vec_signed + * minus_range_vec + * mult_range_vec + * mult_range_vec_signed + *) +let add_IVV = arith_op_range_vec integerAdd false 1 +let addS_IVV = arith_op_range_vec integerAdd true 1 +let minus_IVV = arith_op_range_vec integerMinus false 1 +let mult_IVV = arith_op_range_vec integerMult false 2 +let multS_IVV = arith_op_range_vec integerMult true 2 + +let arith_op_range_vec_range op sign l r = op l (to_num sign r) + +(* add_range_vec_range + * add_range_vec_range_signed + * minus_range_vec_range + *) +let add_IVI = arith_op_range_vec_range integerAdd false +let addS_IVI = arith_op_range_vec_range integerAdd true +let minus_IVI = arith_op_range_vec_range integerMinus false + +let arith_op_vec_range_range op sign l r = op (to_num sign l) r + +(* add_vec_range_range + * add_vec_range_range_signed + * minus_vec_range_range + *) +let add_VII = arith_op_vec_range_range integerAdd false +let addS_VII = arith_op_vec_range_range integerAdd true +let minus_VII = arith_op_vec_range_range integerMinus false + + + +let arith_op_vec_vec_range op sign l r = + let (l',r') = (to_num sign l,to_num sign r) in + op l' r' + +(* add_vec_vec_range + * add_vec_vec_range_signed + *) +let add_VVI = arith_op_vec_vec_range integerAdd false +let addS_VVI = arith_op_vec_vec_range integerAdd true + +let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r = + let l' = to_num sign l in + let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in + to_norm_vec is_inc (length l * size,n) + +(* add_vec_bit + * add_vec_bit_signed + * minus_vec_bit_signed + *) +let add_VBV = arith_op_vec_bit integerAdd false 1 +let addS_VBV = arith_op_vec_bit integerAdd true 1 +let minus_VBV = arith_op_vec_bit integerMinus true 1 + +let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r = + let len = length l in + let act_size = len * size in + let (l_sign,r_sign) = (to_num sign l,to_num sign r) in + let (l_unsign,r_unsign) = (to_num false l,to_num false r) in + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size_num = to_norm_vec is_inc (act_size,n) in + let one_more_size_u = to_norm_vec is_inc (act_size + 1,n_unsign) in + let overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then B0 else B1 in + let c_out = most_significant one_more_size_u in + (correct_size_num,overflow,c_out) + +(* add_overflow_vec + * add_overflow_vec_signed + * minus_overflow_vec + * minus_overflow_vec_signed + * mult_overflow_vec + * mult_overflow_vec_signed + *) +let addO_VVV = arith_op_overflow_vec integerAdd false 1 +let addSO_VVV = arith_op_overflow_vec integerAdd true 1 +let minusO_VVV = arith_op_overflow_vec integerMinus false 1 +let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 +let multO_VVV = arith_op_overflow_vec integerMult false 2 +let multSO_VVV = arith_op_overflow_vec integerMult true 2 + +let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) + (Vector _ _ is_inc as l) r_bit = + let act_size = length l * size in + let l' = to_num sign l in + let l_u = to_num false l in + let (n,nu,changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l',l_u,false) + | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" + end in +(* | _ -> assert false *) + let correct_size_num = to_norm_vec is_inc (act_size,n) in + let one_larger = to_norm_vec is_inc (act_size + 1,nu) in + let overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then B0 else B1 + else B0 in + (correct_size_num,overflow,most_significant one_larger) + +(* add_overflow_vec_bit_signed + * minus_overflow_vec_bit + * minus_overflow_vec_bit_signed + *) +let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 +let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 +let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 + +type shift = LL_shift | RR_shift | LLL_shift + +let shift_op_vec op (Vector bs start is_inc,(n : integer)) = + let n = natFromInteger n in + match op with + | LL_shift (*"<<"*) -> + Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc + | RR_shift (*">>"*) -> + Vector (List.replicate n B0 ++ sublist bs (0,n-1)) start is_inc + | LLL_shift (*"<<<"*) -> + Vector (sublist bs (n,List.length bs - 1) ++ sublist bs (0,n-1)) start is_inc + end + +let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) +let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) +let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) + +let shiftl = bitwise_leftshift + +let rec arith_op_no0 (op : integer -> integer -> integer) l r = + if r = 0 + then Nothing + else Just (op l r) + +let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r = + let act_size = length l * size in + let (l',r') = (to_num sign l,to_num sign r) in + let n = arith_op_no0 op l' r' in + let (representable,n') = + match n with + | Just n' -> + (n' <= get_max_representable_in sign act_size && + n' >= get_min_representable_in sign act_size, n') + | _ -> (false,0) + end in + if representable + then to_norm_vec is_inc (act_size,n') + else Vector (List.replicate (natFromInteger act_size) BU) start is_inc + +let mod_VVV = arith_op_vec_no0 hardware_mod false 1 +let quot_VVV = arith_op_vec_no0 hardware_quot false 1 +let quotS_VVV = arith_op_vec_no0 hardware_quot true 1 + +let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = + let rep_size = length r * size in + let act_size = length l * size in + let (l',r') = (to_num sign l,to_num sign r) in + let (l_u,r_u) = (to_num false l,to_num false r) in + let n = arith_op_no0 op l' r' in + let n_u = arith_op_no0 op l_u r_u in + let (representable,n',n_u') = + match (n, n_u) with + | (Just n',Just n_u') -> + ((n' <= get_max_representable_in sign rep_size && + n' >= (get_min_representable_in sign rep_size)), n', n_u') + | _ -> (true,0,0) + end in + let (correct_size_num,one_more) = + if representable then + (to_norm_vec is_inc (act_size,n'),to_norm_vec is_inc (act_size + 1,n_u')) + else + (Vector (List.replicate (natFromInteger act_size) BU) start is_inc, + Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in + let overflow = if representable then B0 else B1 in + (correct_size_num,overflow,most_significant one_more) + +let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 +let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 + +let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = + arith_op_vec_no0 op sign size l (to_norm_vec is_inc (length l,r)) + +let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 + +(* Assumes decreasing bit vectors *) +let duplicate (bit, length) = + Vector (repeat [bit] length) (length - 1) false + +let replicate_bits (v, count) = + Vector (repeat (get_elems v) count) ((length v * count) - 1) false + +let compare_op op (l,r) = (op l r) + +let lt = compare_op (<) +let gt = compare_op (>) +let lteq = compare_op (<=) +let gteq = compare_op (>=) + +let compare_op_vec op sign (l,r) = + let (l',r') = (to_num sign l, to_num sign r) in + compare_op op (l',r') + +let lt_vec = compare_op_vec (<) true +let gt_vec = compare_op_vec (>) true +let lteq_vec = compare_op_vec (<=) true +let gteq_vec = compare_op_vec (>=) true + +let lt_vec_signed = compare_op_vec (<) true +let gt_vec_signed = compare_op_vec (>) true +let lteq_vec_signed = compare_op_vec (<=) true +let gteq_vec_signed = compare_op_vec (>=) true +let lt_vec_unsigned = compare_op_vec (<) false +let gt_vec_unsigned = compare_op_vec (>) false +let lteq_vec_unsigned = compare_op_vec (<=) false +let gteq_vec_unsigned = compare_op_vec (>=) false + +let lt_svec = lt_vec_signed + +let compare_op_vec_range op sign (l,r) = + compare_op op ((to_num sign l),r) + +let lt_vec_range = compare_op_vec_range (<) true +let gt_vec_range = compare_op_vec_range (>) true +let lteq_vec_range = compare_op_vec_range (<=) true +let gteq_vec_range = compare_op_vec_range (>=) true + +let compare_op_range_vec op sign (l,r) = + compare_op op (l, (to_num sign r)) + +let lt_range_vec = compare_op_range_vec (<) true +let gt_range_vec = compare_op_range_vec (>) true +let lteq_range_vec = compare_op_range_vec (<=) true +let gteq_range_vec = compare_op_range_vec (>=) true + +val eq : forall 'a. Eq 'a => 'a * 'a -> bool +let eq (l,r) = (l = r) +let eq_range (l,r) = (l = r) + +val eq_vec : forall 'a. vector 'a * vector 'a -> bool +let eq_vec (l,r) = (l = r) +let eq_bit (l,r) = (l = r) +let eq_vec_range (l,r) = eq (to_num false l,r) +let eq_range_vec (l,r) = eq (l, to_num false r) +let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) + +let neq (l,r) = not (eq (l,r)) +let neq_bit (l,r) = not (eq_bit (l,r)) +let neq_range (l,r) = not (eq_range (l,r)) +let neq_vec (l,r) = not (eq_vec (l,r)) +let neq_vec_vec (l,r) = not (eq_vec_vec (l,r)) +let neq_vec_range (l,r) = not (eq_vec_range (l,r)) +let neq_range_vec (l,r) = not (eq_range_vec (l,r)) + + +val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a +let make_indexed_vector entries default start length dir = + let length = natFromInteger length in + Vector (List.foldl replace (replicate length default) entries) start dir + +(* +val make_bit_vector_undef : integer -> vector bitU +let make_bitvector_undef length = + Vector (replicate (natFromInteger length) BU) 0 true + *) + +(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) + +let mask (start, n, Vector bits _ dir) = + let current_size = List.length bits in + Vector (drop (current_size - (natFromInteger n)) bits) start dir + + +(* Register operations *) + +(*let update_reg_range i j reg_val new_val = update reg_val i j new_val +let update_reg_pos i reg_val bit = update_pos reg_val i bit +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update current_field_value i j new_val in + regfield.set_field reg_val new_field_value +(*let write_reg_field_pos regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update_pos current_field_value i bit in + regfield.set_field reg_val new_field_value*)*) diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem new file mode 100644 index 00000000..74d0acf7 --- /dev/null +++ b/src/gen_lib/sail_operators_mwords.lem @@ -0,0 +1,601 @@ +open import Pervasives_extra +open import Machine_word +open import Sail_impl_base +open import Sail_values + +(* Translating between a type level number (itself 'n) and an integer *) + +let size_itself_int x = integerFromNat (size_itself x) + +(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n), + the actual integer is ignored. *) + +val make_the_value : forall 'n. integer -> itself 'n +let inline make_the_value x = the_value + +(*** Bit vector operations *) + +let bitvector_length bs = integerFromNat (word_length bs) + +(*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a +let set_bitvector_start (new_start, Bitvector bs _ is_inc) = + Bitvector bs new_start is_inc + +let reset_bitvector_start v = + set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1), v) + +let set_bitvector_start_to_length v = + set_bitvector_start (bvlength v - 1, v) + +let bitvector_concat (Bitvector bs start is_inc, Bitvector bs' _ _) = + Bitvector (word_concat bs bs') start is_inc*) + +let bitvector_concat (bs, bs') = word_concat bs bs' + +let inline (^^^) = bitvector_concat + +val bvslice : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b +let bvslice is_inc start bs i j = + let iN = natFromInteger i in + let jN = natFromInteger j in + let startN = natFromInteger start in + let top = word_length bs - 1 in + let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in + word_extract lo hi bs + +let bitvector_subrange_inc (start, v, i, j) = bvslice true start v i j +let bitvector_subrange_dec (start, v, i, j) = bvslice false start v i j + +let vector_subrange_bl_dec (start, v, i, j) = + let v' = slice (bvec_to_vec false start v) i j in + get_elems v' + +(* this is for the vector slicing introduced in vector-concat patterns: i and j +index into the "raw data", the list of bits. Therefore getting the bit list is +easy, but the start index has to be transformed to match the old vector start +and the direction. *) +val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b +let bvslice_raw bs i j = + let iN = natFromInteger i in + let jN = natFromInteger j in + (*let bits =*) word_extract iN jN bs (*in + let len = integerFromNat (word_length bits) in + Bitvector bits (if is_inc then 0 else len - 1) is_inc*) + +val bvupdate_aux : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> list bitU -> bitvector 'a +let bvupdate_aux is_inc start bs i j bs' = + let bits = update_aux is_inc start (List.map to_bitU (bitlistFromWord bs)) i j bs' in + wordFromBitlist (List.map of_bitU bits) + (*let iN = natFromInteger i in + let jN = natFromInteger j in + let startN = natFromInteger start in + let top = word_length bs - 1 in + let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in + word_update bs lo hi bs'*) + +val bvupdate : forall 'a 'b. Size 'a => bool -> integer -> bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a +let bvupdate is_inc start bs i j bs' = + bvupdate_aux is_inc start bs i j (List.map to_bitU (bitlistFromWord bs')) + +val bvaccess : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU +let bvaccess is_inc start bs n = bool_to_bitU ( + let top = integerFromNat (word_length bs) - 1 in + if is_inc then getBit bs (natFromInteger (top + start - n)) + else getBit bs (natFromInteger (top + n - start))) + +val bvupdate_pos : forall 'a. Size 'a => bool -> integer -> bitvector 'a -> integer -> bitU -> bitvector 'a +let bvupdate_pos is_inc start v n b = + bvupdate_aux is_inc start v n n [b] + +let bitvector_access_inc (start, v, i) = bvaccess true start v i +let bitvector_access_dec (start, v, i) = bvaccess false start v i +let bitvector_update_pos_dec (start, v, i, b) = bvupdate_pos false start v i b +let bitvector_update_subrange_dec (start, v, i, j, v') = bvupdate false start v i j v' + +val extract_only_bit : bitvector ty1 -> bitU +let extract_only_bit elems = + let l = word_length elems in + if l = 1 then + bool_to_bitU (msb elems) + else if l = 0 then + failwith "extract_single_bit called for empty vector" + else + failwith "extract_single_bit called for vector with more bits" + + +let norm_dec v = v (*reset_bitvector_start*) +let adjust_start_index (start, v) = v (*set_bitvector_start (start, v)*) + +let cast_vec_bool v = bitU_to_bool (extract_only_bit v) +let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false) +let cast_boolvec_bitvec (Vector bs start inc) = + vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc) +let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v) + +let pp_bitu_vector (Vector elems start inc) = + let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in + "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc + + +let most_significant v = + if word_length v = 0 then + failwith "most_significant applied to empty vector" + else + bool_to_bitU (msb v) + +let bitwise_not_bitlist = List.map bitwise_not_bit + +let bitwise_not bs = lNot bs + +let bitwise_binop op (bsl, bsr) = (op bsl bsr) + +let bitwise_and x = bitwise_binop lAnd x +let bitwise_or x = bitwise_binop lOr x +let bitwise_xor x = bitwise_binop lXor x + +(*let unsigned bs : integer = unsignedIntegerFromWord bs*) +let unsigned_big = unsigned + +let signed v : integer = signedIntegerFromWord v + +let hardware_mod (a: integer) (b:integer) : integer = + if a < 0 && b < 0 + then (abs a) mod (abs b) + else if (a < 0 && b >= 0) + then (a mod b) - b + else a mod b + +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) +let hardware_quot (a:integer) (b:integer) : integer = + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) + +let quot_signed = hardware_quot + + +let signed_big = signed + +let to_num sign = if sign then signed else unsigned + +let max_64u = (integerPow 2 64) - 1 +let max_64 = (integerPow 2 63) - 1 +let min_64 = 0 - (integerPow 2 63) +let max_32u = (4294967295 : integer) +let max_32 = (2147483647 : integer) +let min_32 = (0 - 2147483648 : integer) +let max_8 = (127 : integer) +let min_8 = (0 - 128 : integer) +let max_5 = (31 : integer) +let min_5 = (0 - 32 : integer) + +let get_max_representable_in sign (n : integer) : integer = + if (n = 64) then match sign with | true -> max_64 | false -> max_64u end + else if (n=32) then match sign with | true -> max_32 | false -> max_32u end + else if (n=8) then max_8 + else if (n=5) then max_5 + else match sign with | true -> integerPow 2 ((natFromInteger n) -1) + | false -> integerPow 2 (natFromInteger n) + end + +let get_min_representable_in _ (n : integer) : integer = + if n = 64 then min_64 + else if n = 32 then min_32 + else if n = 8 then min_8 + else if n = 5 then min_5 + else 0 - (integerPow 2 (natFromInteger n)) + +val to_bin_aux : natural -> list bitU +let rec to_bin_aux x = + if x = 0 then [] + else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) +let to_bin n = List.reverse (to_bin_aux n) + +val pad_zero : list bitU -> integer -> list bitU +let rec pad_zero bits n = + if n = 0 then bits else pad_zero (B0 :: bits) (n -1) + + +let rec add_one_bit_ignore_overflow_aux bits = match bits with + | [] -> [] + | B0 :: bits -> B1 :: bits + | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits + | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" +end + +let add_one_bit_ignore_overflow bits = + List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) + +val to_norm_vec : forall 'a. Size 'a => integer -> bitvector 'a +let to_norm_vec (n : integer) = wordFromInteger n +(* + (* Bitvector length is determined by return type *) + let bits = wordFromInteger n in + let len = integerFromNat (word_length bits) in + let start = if is_inc then 0 else len - 1 in + (*if integerFromNat (word_length bits) = len then*) + Bitvector bits start is_inc + (*else + failwith "Vector length mismatch in to_vec"*) +*) + +let to_vec_big = to_norm_vec + +let to_vec_inc (start, len, n) = to_norm_vec n +let to_vec_norm_inc (len, n) = to_norm_vec n +let to_vec_dec (start, len, n) = to_norm_vec n +let to_vec_norm_dec (len, n) = to_norm_vec n + +(* TODO: Think about undefined bit(vector)s *) +let to_vec_undef is_inc (len : integer) = + (* Bitvector *) + (failwith "undefined bitvector") + (* (if is_inc then 0 else len-1) is_inc *) + +let to_vec_inc_undef = to_vec_undef true +let to_vec_dec_undef = to_vec_undef false + +let exts (start, len, vec) = to_norm_vec (signed vec) +val extz : forall 'a 'b. Size 'a, Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b +let extz (start, len, vec) = to_norm_vec (unsigned vec) + +let exts_big (start, len, vec) = to_vec_big (signed_big vec) +let extz_big (start, len, vec) = to_vec_big (unsigned_big vec) + +(* TODO *) +let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) +let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) + +let quot = hardware_quot +let modulo (l,r) = hardware_mod l r + +(* TODO: this, and the definitions that use it, currently require Size for + to_vec, which I'd rather avoid in favour of library versions; the + double-size results for multiplication may be a problem *) +let arith_op_vec op sign (size : integer) l r = + let (l',r') = (to_num sign l, to_num sign r) in + let n = op l' r' in + to_norm_vec n + + +(* add_vec + * add_vec_signed + * minus_vec + * multiply_vec + * multiply_vec_signed + *) +let add_VVV = arith_op_vec integerAdd false 1 +let addS_VVV = arith_op_vec integerAdd true 1 +let minus_VVV = arith_op_vec integerMinus false 1 +let mult_VVV = arith_op_vec integerMult false 2 +let multS_VVV = arith_op_vec integerMult true 2 + +let mult_vec (l, r) = mult_VVV l r +let mult_svec (l, r) = multS_VVV l r + +let add_vec (l, r) = add_VVV l r +let sub_vec (l, r) = minus_VVV l r + +val arith_op_vec_range : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'b +let arith_op_vec_range op sign size l r = + arith_op_vec op sign size l ((to_norm_vec r) : bitvector 'a) + +(* add_vec_range + * add_vec_range_signed + * minus_vec_range + * mult_vec_range + * mult_vec_range_signed + *) +let add_VIV = arith_op_vec_range integerAdd false 1 +let addS_VIV = arith_op_vec_range integerAdd true 1 +let minus_VIV = arith_op_vec_range integerMinus false 1 +let mult_VIV = arith_op_vec_range integerMult false 2 +let multS_VIV = arith_op_vec_range integerMult true 2 + +let add_vec_int (l, r) = add_VIV l r +let sub_vec_int (l, r) = minus_VIV l r + +val arith_op_range_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'b +let arith_op_range_vec op sign size l r = + arith_op_vec op sign size ((to_norm_vec l) : bitvector 'a) r + +(* add_range_vec + * add_range_vec_signed + * minus_range_vec + * mult_range_vec + * mult_range_vec_signed + *) +let add_IVV = arith_op_range_vec integerAdd false 1 +let addS_IVV = arith_op_range_vec integerAdd true 1 +let minus_IVV = arith_op_range_vec integerMinus false 1 +let mult_IVV = arith_op_range_vec integerMult false 2 +let multS_IVV = arith_op_range_vec integerMult true 2 + +let arith_op_range_vec_range op sign l r = op l (to_num sign r) + +(* add_range_vec_range + * add_range_vec_range_signed + * minus_range_vec_range + *) +let add_IVI x = arith_op_range_vec_range integerAdd false x +let addS_IVI x = arith_op_range_vec_range integerAdd true x +let minus_IVI x = arith_op_range_vec_range integerMinus false x + +let arith_op_vec_range_range op sign l r = op (to_num sign l) r + +(* add_vec_range_range + * add_vec_range_range_signed + * minus_vec_range_range + *) +let add_VII x = arith_op_vec_range_range integerAdd false x +let addS_VII x = arith_op_vec_range_range integerAdd true x +let minus_VII x = arith_op_vec_range_range integerMinus false x + + + +let arith_op_vec_vec_range op sign l r = + let (l',r') = (to_num sign l,to_num sign r) in + op l' r' + +(* add_vec_vec_range + * add_vec_vec_range_signed + *) +let add_VVI x = arith_op_vec_vec_range integerAdd false x +let addS_VVI x = arith_op_vec_vec_range integerAdd true x + +let arith_op_vec_bit op sign (size : integer) l r = + let l' = to_num sign l in + let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in + to_norm_vec n + +(* add_vec_bit + * add_vec_bit_signed + * minus_vec_bit_signed + *) +let add_VBV x = arith_op_vec_bit integerAdd false 1 x +let addS_VBV x = arith_op_vec_bit integerAdd true 1 x +let minus_VBV x = arith_op_vec_bit integerMinus true 1 x + +(* TODO: these can't be done directly in Lem because of the one_more size calculation +val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool +let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r = + let len = bvlength l in + let act_size = len * size in + let (l_sign,r_sign) = (to_num sign l,to_num sign r) in + let (l_unsign,r_unsign) = (to_num false l,to_num false r) in + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size_num = to_vec_ord is_inc (act_size,n) in + let one_more_size_u = to_vec_ord is_inc (act_size + 1,n_unsign) in + let overflow = + if n <= get_max_representable_in sign len && + n >= get_min_representable_in sign len + then B0 else B1 in + let c_out = most_significant one_more_size_u in + (correct_size_num,overflow,c_out) + +(* add_overflow_vec + * add_overflow_vec_signed + * minus_overflow_vec + * minus_overflow_vec_signed + * mult_overflow_vec + * mult_overflow_vec_signed + *) +let addO_VVV = arith_op_overflow_vec integerAdd false 1 +let addSO_VVV = arith_op_overflow_vec integerAdd true 1 +let minusO_VVV = arith_op_overflow_vec integerMinus false 1 +let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 +let multO_VVV = arith_op_overflow_vec integerMult false 2 +let multSO_VVV = arith_op_overflow_vec integerMult true 2 + +val arith_op_overflow_vec_bit : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> + bitvector 'a -> bitU -> bitvector 'b * bitU * bool +let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) + (Bitvector _ _ is_inc as l) r_bit = + let act_size = bvlength l * size in + let l' = to_num sign l in + let l_u = to_num false l in + let (n,nu,changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l',l_u,false) + | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" + end in +(* | _ -> assert false *) + let correct_size_num = to_vec_ord is_inc (act_size,n) in + let one_larger = to_vec_ord is_inc (act_size + 1,nu) in + let overflow = + if changed + then + if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size + then B0 else B1 + else B0 in + (correct_size_num,overflow,most_significant one_larger) + +(* add_overflow_vec_bit_signed + * minus_overflow_vec_bit + * minus_overflow_vec_bit_signed + *) +let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 +let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 +let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 +*) +type shift = LL_shift | RR_shift | LLL_shift + +let shift_op_vec op (bs, (n : integer)) = + let n = natFromInteger n in + match op with + | LL_shift (*"<<"*) -> + shiftLeft bs n + | RR_shift (*">>"*) -> + shiftRight bs n + | LLL_shift (*"<<<"*) -> + rotateLeft n bs + end + +let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*) +let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*) +let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*) + +let shiftl = bitwise_leftshift + +let rec arith_op_no0 (op : integer -> integer -> integer) l r = + if r = 0 + then Nothing + else Just (op l r) +(* TODO +let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r = + let act_size = bvlength l * size in + let (l',r') = (to_num sign l,to_num sign r) in + let n = arith_op_no0 op l' r' in + let (representable,n') = + match n with + | Just n' -> + (n' <= get_max_representable_in sign act_size && + n' >= get_min_representable_in sign act_size, n') + | _ -> (false,0) + end in + if representable + then to_vec_ord is_inc (act_size,n') + else Vector (List.replicate (natFromInteger act_size) BU) start is_inc + +let mod_VVV = arith_op_vec_no0 hardware_mod false 1 +let quot_VVV = arith_op_vec_no0 hardware_quot false 1 +let quotS_VVV = arith_op_vec_no0 hardware_quot true 1 + +let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = + let rep_size = length r * size in + let act_size = length l * size in + let (l',r') = (to_num sign l,to_num sign r) in + let (l_u,r_u) = (to_num false l,to_num false r) in + let n = arith_op_no0 op l' r' in + let n_u = arith_op_no0 op l_u r_u in + let (representable,n',n_u') = + match (n, n_u) with + | (Just n',Just n_u') -> + ((n' <= get_max_representable_in sign rep_size && + n' >= (get_min_representable_in sign rep_size)), n', n_u') + | _ -> (true,0,0) + end in + let (correct_size_num,one_more) = + if representable then + (to_vec_ord is_inc (act_size,n'),to_vec_ord is_inc (act_size + 1,n_u')) + else + (Vector (List.replicate (natFromInteger act_size) BU) start is_inc, + Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in + let overflow = if representable then B0 else B1 in + (correct_size_num,overflow,most_significant one_more) + +let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 +let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 + +let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = + arith_op_vec_no0 op sign size l (to_vec_ord is_inc (length l,r)) + +let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 +*) + +let duplicate (bit, length) = + vec_to_bvec (Vector (repeat [bit] length) (length - 1) false) + +(* TODO: replace with better native versions *) +let replicate_bits (v, count) = + let v = bvec_to_vec true 0 v in + vec_to_bvec (Vector (repeat (get_elems v) count) ((length v * count) - 1) false) + +let compare_op op (l,r) = (op l r) + +let lt = compare_op (<) +let gt = compare_op (>) +let lteq = compare_op (<=) +let gteq = compare_op (>=) + +let compare_op_vec op sign (l,r) = + let (l',r') = (to_num sign l, to_num sign r) in + compare_op op (l',r') + +let lt_vec x = compare_op_vec (<) true x +let gt_vec x = compare_op_vec (>) true x +let lteq_vec x = compare_op_vec (<=) true x +let gteq_vec x = compare_op_vec (>=) true x + +let lt_vec_signed x = compare_op_vec (<) true x +let gt_vec_signed x = compare_op_vec (>) true x +let lteq_vec_signed x = compare_op_vec (<=) true x +let gteq_vec_signed x = compare_op_vec (>=) true x +let lt_vec_unsigned x = compare_op_vec (<) false x +let gt_vec_unsigned x = compare_op_vec (>) false x +let lteq_vec_unsigned x = compare_op_vec (<=) false x +let gteq_vec_unsigned x = compare_op_vec (>=) false x + +let lt_svec = lt_vec_signed + +let compare_op_vec_range op sign (l,r) = + compare_op op ((to_num sign l),r) + +let lt_vec_range x = compare_op_vec_range (<) true x +let gt_vec_range x = compare_op_vec_range (>) true x +let lteq_vec_range x = compare_op_vec_range (<=) true x +let gteq_vec_range x = compare_op_vec_range (>=) true x + +let compare_op_range_vec op sign (l,r) = + compare_op op (l, (to_num sign r)) + +let lt_range_vec x = compare_op_range_vec (<) true x +let gt_range_vec x = compare_op_range_vec (>) true x +let lteq_range_vec x = compare_op_range_vec (<=) true x +let gteq_range_vec x = compare_op_range_vec (>=) true x + +val eq : forall 'a. Eq 'a => 'a * 'a -> bool +let eq (l,r) = (l = r) +let eq_range (l,r) = (l = r) + +val eq_vec : forall 'a. Size 'a => bitvector 'a * bitvector 'a -> bool +let eq_vec (l,r) = eq (to_num false l, to_num false r) +let eq_bit (l,r) = eq (l, r) +let eq_vec_range (l,r) = eq (to_num false l,r) +let eq_range_vec (l,r) = eq (l, to_num false r) +(*let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)*) + +let neq (l,r) = not (eq (l,r)) +let neq_bit (l,r) = not (eq_bit (l,r)) +let neq_range (l,r) = not (eq_range (l,r)) +let neq_vec (l,r) = not (eq_vec (l,r)) +(*let neq_vec_vec (l,r) = not (eq_vec_vec (l,r))*) +let neq_vec_range (l,r) = not (eq_vec_range (l,r)) +let neq_range_vec (l,r) = not (eq_range_vec (l,r)) + + +val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a +let make_indexed_vector entries default start length dir = + let length = natFromInteger length in + Vector (List.foldl replace (replicate length default) entries) start dir + +(* +val make_bit_vector_undef : integer -> vector bitU +let make_bitvector_undef length = + Vector (replicate (natFromInteger length) BU) 0 true + *) + +(* let bitwise_not_range_bit n = bitwise_not (to_vec_ord defaultDir n) *) + +(* TODO *) +val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b +let mask (start, _, w) = (zeroExtend w) + +(* Register operations *) + +(*let update_reg_range reg i j reg_val new_val = bvupdate (reg.reg_is_inc) (reg.reg_start) reg_val i j new_val +let update_reg_pos reg i reg_val bit = bvupdate_pos (reg.reg_is_inc) (reg.reg_start) reg_val i bit +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = bvupdate (regfield.field_is_inc) (regfield.field_start) current_field_value i j new_val in + regfield.set_field reg_val new_field_value +(*let write_reg_field_pos regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = bvupdate_pos (regfield.field_is_inc) (regfield.field_start) current_field_value i bit in + regfield.set_field reg_val new_field_value*)*) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 121f6cc8..98ac2522 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,4 +1,7 @@ +(* Version of sail_values.lem that uses Lem's machine words library *) + open import Pervasives_extra +open import Machine_word open import Sail_impl_base @@ -8,6 +11,44 @@ type nn = natural val pow : integer -> integer -> integer let pow m n = m ** (natFromInteger n) +let pow2 n = pow 2 n + +let add_int (l,r) = integerAdd l r +let add_signed (l,r) = integerAdd l r +let sub_int (l,r) = integerMinus l r +let mult_int (l,r) = integerMult l r +let quotient_int (l,r) = integerDiv l r +let quotient_nat (l,r) = natDiv l r +let power_int_nat (l,r) = integerPow l r +let power_int_int (l, r) = integerPow l (natFromInteger r) +let negate_int i = integerNegate i +let min_int (l, r) = integerMin l r +let max_int (l, r) = integerMax l r + +let add_real (l, r) = realAdd l r +let sub_real (l, r) = realMinus l r +let mult_real (l, r) = realMult l r +let div_real (l, r) = realDiv l r +let negate_real r = realNegate r +let abs_real r = realAbs r +let power_real (b, e) = realPowInteger b e + +let or_bool (l, r) = (l || r) +let and_bool (l, r) = (l && r) +let xor_bool (l, r) = xor l r + +let list_append (l, r) = l ++ r +let list_length xs = integerFromNat (List.length xs) +let list_take (n, xs) = List.take (natFromInteger n) xs +let list_drop (n, xs) = List.drop (natFromInteger n) xs + +val repeat : forall 'a. list 'a -> integer -> list 'a +let rec repeat xs n = + if n <= 0 then [] + else xs ++ repeat xs (n-1) + +let duplicate_to_list (bit, length) = repeat [bit] length + let rec replace bs ((n : integer),b') = match bs with | [] -> [] | b :: bs -> @@ -15,6 +56,7 @@ let rec replace bs ((n : integer),b') = match bs with else b :: replace bs (n - 1,b') end +let upper n = n (*** Bits *) type bitU = B0 | B1 | BU @@ -29,6 +71,15 @@ instance (Show bitU) let show = showBitU end +class (BitU 'a) + val to_bitU : 'a -> bitU + val of_bitU : bitU -> 'a +end + +instance (BitU bitU) + let to_bitU b = b + let of_bitU b = b +end let bitU_to_bool = function | B0 -> false @@ -36,6 +87,15 @@ let bitU_to_bool = function | BU -> failwith "to_bool applied to BU" end +let bool_to_bitU b = if b then B1 else B0 + +instance (BitU bool) + let to_bitU = bool_to_bitU + let of_bitU = bitU_to_bool +end + +let cast_bit_bool = bitU_to_bool + let bit_lifted_of_bitU = function | B0 -> Bitl_zero | B1 -> Bitl_one @@ -66,14 +126,12 @@ let bitwise_not_bit = function | BU -> BU end -let inline (~) = bitwise_not_bit +(* let inline (~) = bitwise_not_bit *) val is_one : integer -> bitU let is_one i = if i = 1 then B1 else B0 -let bool_to_bitU b = if b then B1 else B0 - let bitwise_binop_bit op = function | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) @@ -98,6 +156,56 @@ let inline (|.) x y = bitwise_or_bit (x,y) val (+.) : bitU -> bitU -> bitU let inline (+.) x y = bitwise_xor_bit (x,y) +val to_bin_aux : natural -> list bitU +let rec to_bin_aux x = + if x = 0 then [] + else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) +let to_bin n = List.reverse (to_bin_aux n) + +val of_bin : list bitU -> natural +let of_bin 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 "of_bin: bitvector has undefined bits" + end) + (0,0) bits in + sum + +val bitlist_to_integer : list bitU -> integer +let bitlist_to_integer bs = integerFromNatural (of_bin bs) + +val pad_zero : list bitU -> integer -> list bitU +let rec pad_zero bits n = + if n <= 0 then bits else pad_zero (B0 :: bits) (n -1) + +let bitwise_not_bitlist = List.map bitwise_not_bit + +let rec add_one_bit_ignore_overflow_aux bits = match bits with + | [] -> [] + | B0 :: bits -> B1 :: bits + | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits + | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" +end + +let add_one_bit_ignore_overflow bits = + List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) + +let bits_of_nat ((len : integer),(n : natural)) = + let bits = to_bin n in + let len_bits = integerFromNat (List.length bits) in + let longer = len - len_bits in + if longer < 0 then drop (natFromInteger (abs (longer))) bits + else pad_zero bits longer + +let bits_of_int ((len : integer),(n : integer)) = + let bits = bits_of_nat (len, naturalFromInteger (abs n)) in + if n > (0 : integer) + then bits + else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits)) (*** Vectors *) @@ -112,6 +220,7 @@ let get_dir (Vector _ _ ord) = ord let get_start (Vector _ s _) = s let get_elems (Vector elems _ _) = elems let length (Vector bs _ _) = integerFromNat (length bs) +let vector_length = length instance forall 'a. Show 'a => (Show (vector 'a)) let show = showVector @@ -125,17 +234,17 @@ let bool_of_dir = function (*** Vector operations *) -val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a -let set_vector_start new_start (Vector bs _ is_inc) = +val set_vector_start : forall 'a. (integer * vector 'a) -> vector 'a +let set_vector_start (new_start, Vector bs _ is_inc) = Vector bs new_start is_inc let reset_vector_start v = - set_vector_start (if (get_dir v) then 0 else (length v - 1)) v + set_vector_start (if (get_dir v) then 0 else (length v - 1), v) let set_vector_start_to_length v = - set_vector_start (length v - 1) v + set_vector_start (length v - 1, v) -let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = +let vector_concat (Vector bs start is_inc, Vector bs' _ _) = Vector (bs ++ bs') start is_inc let inline (^^) = vector_concat @@ -152,14 +261,19 @@ let update_sublist xs (i,j) xs' = let (prefix,_fromItoJ) = List.splitAt i toJ in prefix ++ xs' ++ suffix -val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a -let slice (Vector bs start is_inc) i j = +val slice_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a +let slice_aux is_inc start bs i j = let iN = natFromInteger i in let jN = natFromInteger j in let startN = natFromInteger start in - let subvector_bits = - sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in - Vector subvector_bits i is_inc + sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) + +val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a +let slice (Vector bs start is_inc) i j = + Vector (slice_aux is_inc start bs i j) i is_inc + +let vector_subrange_inc (start, v, i, j) = slice v i j +let vector_subrange_dec (start, v, i, j) = slice v i j (* this is for the vector slicing introduced in vector-concat patterns: i and j index into the "raw data", the list of bits. Therefore getting the bit list is @@ -174,503 +288,115 @@ let slice_raw (Vector bs start is_inc) i j = Vector bits (if is_inc then 0 else len - 1) is_inc -val update_aux : forall 'a. vector 'a -> integer -> integer -> list 'a -> vector 'a -let update_aux (Vector bs start is_inc) i j bs' = +val update_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a -> list 'a +let update_aux is_inc start bs i j bs' = let iN = natFromInteger i in let jN = natFromInteger j in let startN = natFromInteger start in - let bits = - (update_sublist bs) - (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' in - Vector bits start is_inc + update_sublist bs + (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a -let update v i j (Vector bs' _ _) = - update_aux v i j bs' +let update (Vector bs start is_inc) i j (Vector bs' _ _) = + Vector (update_aux is_inc start bs i j bs') start is_inc + +let vector_update_subrange_inc (start, v, i, j, v') = update v i j v' +let vector_update_subrange_dec (start, v, i, j, v') = update v i j v' + +val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a +let access_aux is_inc start xs n = + if is_inc then List_extra.nth xs (natFromInteger (n - start)) + else List_extra.nth xs (natFromInteger (start - n)) val access : forall 'a. vector 'a -> integer -> 'a -let access (Vector bs start is_inc) n = - if is_inc then List_extra.nth bs (natFromInteger (n - start)) - else List_extra.nth bs (natFromInteger (start - n)) +let access (Vector bs start is_inc) n = access_aux is_inc start bs n + +let vector_access_inc (start, v, i) = access v i +let vector_access_dec (start, v, i) = access v i val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a let update_pos v n b = - update_aux v n n [b] - + update v n n (Vector [b] 0 false) -(*** Bit vector operations *) +let vector_update_pos_inc (start, v, i, x) = update_pos v i x +let vector_update_pos_dec (start, v, i, x) = update_pos v i x -let extract_only_bit (Vector elems _ _) = match elems with - | [] -> failwith "extract_single_bit called for empty vector" +let extract_only_element (Vector elems _ _) = match elems with + | [] -> failwith "extract_only_element called for empty vector" | [e] -> e - | _ -> failwith "extract_single_bit called for vector with more bits" + | _ -> failwith "extract_only_element called for vector with more elements" end -let pp_bitu_vector (Vector elems start inc) = - let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in - "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc - - -let most_significant = function - | (Vector (b :: _) _ _) -> b - | _ -> failwith "most_significant applied to empty vector" - end - -let bitwise_not_bitlist = List.map bitwise_not_bit - -let bitwise_not (Vector bs start is_inc) = - Vector (bitwise_not_bitlist bs) start is_inc +(*** Bitvectors *) -let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) = - let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in - Vector (reverse revbs) start is_inc - -let bitwise_and = bitwise_binop (&&) -let bitwise_or = bitwise_binop (||) -let bitwise_xor = bitwise_binop xor - -let unsigned (Vector bs _ _) : integer = - let (sum,_) = - List.foldr - (fun b (acc,exp) -> - match b with - | B1 -> (acc + integerPow 2 exp,exp + 1) - | B0 -> (acc, exp + 1) - | BU -> failwith "unsigned: vector has undefined bits" - end) - (0,0) bs in - sum - -let unsigned_big = unsigned - -let signed v : integer = - match most_significant v with - | B1 -> 0 - (1 + (unsigned (bitwise_not v))) - | B0 -> unsigned v - | BU -> failwith "signed applied to vector with undefined bits" - end - -let hardware_mod (a: integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) mod (abs b) - else if (a < 0 && b >= 0) - then (a mod b) - b - else a mod b - -(* There are different possible answers for integer divide regarding -rounding behaviour on negative operands. Positive operands always -round down so derive the one we want (trucation towards zero) from -that *) -let hardware_quot (a:integer) (b:integer) : integer = - let q = (abs a) / (abs b) in - if ((a<0) = (b<0)) then - q (* same sign -- result positive *) - else - integerNegate q (* different sign -- result negative *) - -let quot_signed = hardware_quot - - -let signed_big = signed - -let to_num sign = if sign then signed else unsigned - -let max_64u = (integerPow 2 64) - 1 -let max_64 = (integerPow 2 63) - 1 -let min_64 = 0 - (integerPow 2 63) -let max_32u = (4294967295 : integer) -let max_32 = (2147483647 : integer) -let min_32 = (0 - 2147483648 : integer) -let max_8 = (127 : integer) -let min_8 = (0 - 128 : integer) -let max_5 = (31 : integer) -let min_5 = (0 - 32 : integer) - -let get_max_representable_in sign (n : integer) : integer = - if (n = 64) then match sign with | true -> max_64 | false -> max_64u end - else if (n=32) then match sign with | true -> max_32 | false -> max_32u end - else if (n=8) then max_8 - else if (n=5) then max_5 - else match sign with | true -> integerPow 2 ((natFromInteger n) -1) - | false -> integerPow 2 (natFromInteger n) - end - -let get_min_representable_in _ (n : integer) : integer = - if n = 64 then min_64 - else if n = 32 then min_32 - else if n = 8 then min_8 - else if n = 5 then min_5 - else 0 - (integerPow 2 (natFromInteger n)) - -val to_bin_aux : natural -> list bitU -let rec to_bin_aux x = - if x = 0 then [] - else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) -let to_bin n = List.reverse (to_bin_aux n) - -val pad_zero : list bitU -> integer -> list bitU -let rec pad_zero bits n = - if n = 0 then bits else pad_zero (B0 :: bits) (n -1) - - -let rec add_one_bit_ignore_overflow_aux bits = match bits with - | [] -> [] - | B0 :: bits -> B1 :: bits - | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits - | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" +(* element list * start * has increasing direction *) +type bitvector 'a = mword 'a (* Bitvector of mword 'a * integer * bool *) +declare isabelle target_sorts bitvector = `len` + +class (Bitvector 'a) + val bits_of : 'a -> list bitU + val of_bits : list bitU -> 'a + val unsigned : 'a -> integer + (* The first two parameters of the following specify indexing: + indexing order and start index *) + val get_bit : bool -> integer -> 'a -> integer -> bitU + val set_bit : bool -> integer -> 'a -> integer -> bitU -> 'a + val get_bits : bool -> integer -> 'a -> integer -> integer -> list bitU + val set_bits : bool -> integer -> 'a -> integer -> integer -> list bitU -> 'a end -let add_one_bit_ignore_overflow bits = - List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) - - -let to_vec is_inc ((len : integer),(n : integer)) = - let start = if is_inc then 0 else len - 1 in - let bits = to_bin (naturalFromInteger (abs n)) in - let len_bits = integerFromNat (List.length bits) in - let longer = len - len_bits in - let bits' = - if longer < 0 then drop (natFromInteger (abs (longer))) bits - else pad_zero bits longer in - if n > (0 : integer) - then Vector bits' start is_inc - else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits')) - start is_inc - -let to_vec_big = to_vec - -let to_vec_inc = to_vec true -let to_vec_dec = to_vec false - -let to_vec_undef is_inc (len : integer) = - Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc - -let to_vec_inc_undef = to_vec_undef true -let to_vec_dec_undef = to_vec_undef false - -let exts (len, vec) = to_vec (get_dir vec) (len,signed vec) -let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec) - -let exts_big (len, vec) = to_vec_big (get_dir vec) (len, signed_big vec) -let extz_big (len, vec) = to_vec_big (get_dir vec) (len, unsigned_big vec) - -let add = integerAdd -let add_signed = integerAdd -let minus = integerMinus -let multiply = integerMult -let modulo = hardware_mod -let quot = hardware_quot -let power = integerPow - -let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = - let (l',r') = (to_num sign l, to_num sign r) in - let n = op l' r' in - to_vec is_inc (size * (length l),n) - - -(* add_vec - * add_vec_signed - * minus_vec - * multiply_vec - * multiply_vec_signed - *) -let add_VVV = arith_op_vec integerAdd false 1 -let addS_VVV = arith_op_vec integerAdd true 1 -let minus_VVV = arith_op_vec integerMinus false 1 -let mult_VVV = arith_op_vec integerMult false 2 -let multS_VVV = arith_op_vec integerMult true 2 - -let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r = - arith_op_vec op sign size l (to_vec is_inc (length l,r)) - -(* add_vec_range - * add_vec_range_signed - * minus_vec_range - * mult_vec_range - * mult_vec_range_signed - *) -let add_VIV = arith_op_vec_range integerAdd false 1 -let addS_VIV = arith_op_vec_range integerAdd true 1 -let minus_VIV = arith_op_vec_range integerMinus false 1 -let mult_VIV = arith_op_vec_range integerMult false 2 -let multS_VIV = arith_op_vec_range integerMult true 2 - -let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) = - arith_op_vec op sign size (to_vec is_inc (length r, l)) r - -(* add_range_vec - * add_range_vec_signed - * minus_range_vec - * mult_range_vec - * mult_range_vec_signed - *) -let add_IVV = arith_op_range_vec integerAdd false 1 -let addS_IVV = arith_op_range_vec integerAdd true 1 -let minus_IVV = arith_op_range_vec integerMinus false 1 -let mult_IVV = arith_op_range_vec integerMult false 2 -let multS_IVV = arith_op_range_vec integerMult true 2 - -let arith_op_range_vec_range op sign l r = op l (to_num sign r) - -(* add_range_vec_range - * add_range_vec_range_signed - * minus_range_vec_range - *) -let add_IVI = arith_op_range_vec_range integerAdd false -let addS_IVI = arith_op_range_vec_range integerAdd true -let minus_IVI = arith_op_range_vec_range integerMinus false - -let arith_op_vec_range_range op sign l r = op (to_num sign l) r - -(* add_vec_range_range - * add_vec_range_range_signed - * minus_vec_range_range - *) -let add_VII = arith_op_vec_range_range integerAdd false -let addS_VII = arith_op_vec_range_range integerAdd true -let minus_VII = arith_op_vec_range_range integerMinus false - - - -let arith_op_vec_vec_range op sign l r = - let (l',r') = (to_num sign l,to_num sign r) in - op l' r' - -(* add_vec_vec_range - * add_vec_vec_range_signed - *) -let add_VVI = arith_op_vec_vec_range integerAdd false -let addS_VVI = arith_op_vec_vec_range integerAdd true - -let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r = - let l' = to_num sign l in - let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - to_vec is_inc (length l * size,n) - -(* add_vec_bit - * add_vec_bit_signed - * minus_vec_bit_signed - *) -let add_VBV = arith_op_vec_bit integerAdd false 1 -let addS_VBV = arith_op_vec_bit integerAdd true 1 -let minus_VBV = arith_op_vec_bit integerMinus true 1 - -let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r = - let len = length l in - let act_size = len * size in - let (l_sign,r_sign) = (to_num sign l,to_num sign r) in - let (l_unsign,r_unsign) = (to_num false l,to_num false r) in - let n = op l_sign r_sign in - let n_unsign = op l_unsign r_unsign in - let correct_size_num = to_vec is_inc (act_size,n) in - let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in - let overflow = - if n <= get_max_representable_in sign len && - n >= get_min_representable_in sign len - then B0 else B1 in - let c_out = most_significant one_more_size_u in - (correct_size_num,overflow,c_out) - -(* add_overflow_vec - * add_overflow_vec_signed - * minus_overflow_vec - * minus_overflow_vec_signed - * mult_overflow_vec - * mult_overflow_vec_signed - *) -let addO_VVV = arith_op_overflow_vec integerAdd false 1 -let addSO_VVV = arith_op_overflow_vec integerAdd true 1 -let minusO_VVV = arith_op_overflow_vec integerMinus false 1 -let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 -let multO_VVV = arith_op_overflow_vec integerMult false 2 -let multSO_VVV = arith_op_overflow_vec integerMult true 2 - -let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) - (Vector _ _ is_inc as l) r_bit = - let act_size = length l * size in - let l' = to_num sign l in - let l_u = to_num false l in - let (n,nu,changed) = match r_bit with - | B1 -> (op l' 1, op l_u 1, true) - | B0 -> (l',l_u,false) - | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" - end in -(* | _ -> assert false *) - let correct_size_num = to_vec is_inc (act_size,n) in - let one_larger = to_vec is_inc (act_size + 1,nu) in - let overflow = - if changed - then - if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then B0 else B1 - else B0 in - (correct_size_num,overflow,most_significant one_larger) - -(* add_overflow_vec_bit_signed - * minus_overflow_vec_bit - * minus_overflow_vec_bit_signed - *) -let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 -let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 -let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 - -type shift = LL_shift | RR_shift | LLL_shift - -let shift_op_vec op (Vector bs start is_inc,(n : integer)) = - let n = natFromInteger n in - match op with - | LL_shift (*"<<"*) -> - Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc - | RR_shift (*">>"*) -> - Vector (List.replicate n B0 ++ sublist bs (0,n-1)) start is_inc - | LLL_shift (*"<<<"*) -> - Vector (sublist bs (n,List.length bs - 1) ++ sublist bs (0,n-1)) start is_inc - end - -let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) -let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) -let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) - -let rec arith_op_no0 (op : integer -> integer -> integer) l r = - if r = 0 - then Nothing - else Just (op l r) - -let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r = - let act_size = length l * size in - let (l',r') = (to_num sign l,to_num sign r) in - let n = arith_op_no0 op l' r' in - let (representable,n') = - match n with - | Just n' -> - (n' <= get_max_representable_in sign act_size && - n' >= get_min_representable_in sign act_size, n') - | _ -> (false,0) - end in - if representable - then to_vec is_inc (act_size,n') - else Vector (List.replicate (natFromInteger act_size) BU) start is_inc - -let mod_VVV = arith_op_vec_no0 hardware_mod false 1 -let quot_VVV = arith_op_vec_no0 hardware_quot false 1 -let quotS_VVV = arith_op_vec_no0 hardware_quot true 1 - -let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = - let rep_size = length r * size in - let act_size = length l * size in - let (l',r') = (to_num sign l,to_num sign r) in - let (l_u,r_u) = (to_num false l,to_num false r) in - let n = arith_op_no0 op l' r' in - let n_u = arith_op_no0 op l_u r_u in - let (representable,n',n_u') = - match (n, n_u) with - | (Just n',Just n_u') -> - ((n' <= get_max_representable_in sign rep_size && - n' >= (get_min_representable_in sign rep_size)), n', n_u') - | _ -> (true,0,0) - end in - let (correct_size_num,one_more) = - if representable then - (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u')) - else - (Vector (List.replicate (natFromInteger act_size) BU) start is_inc, - Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in - let overflow = if representable then B0 else B1 in - (correct_size_num,overflow,most_significant one_more) - -let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 -let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 - -let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = - arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r)) - -let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 - -val repeat : forall 'a. list 'a -> integer -> list 'a -let rec repeat xs n = - if n = 0 then [] - else xs ++ repeat xs (n-1) - -(* -let duplicate bit length = - Vector (repeat [bit] length) (if dir then 0 else length - 1) dir - *) - -let compare_op op (l,r) = bool_to_bitU (op l r) - -let lt = compare_op (<) -let gt = compare_op (>) -let lteq = compare_op (<=) -let gteq = compare_op (>=) - - -let compare_op_vec op sign (l,r) = - let (l',r') = (to_num sign l, to_num sign r) in - compare_op op (l',r') - -let lt_vec = compare_op_vec (<) true -let gt_vec = compare_op_vec (>) true -let lteq_vec = compare_op_vec (<=) true -let gteq_vec = compare_op_vec (>=) true - -let lt_vec_signed = compare_op_vec (<) true -let gt_vec_signed = compare_op_vec (>) true -let lteq_vec_signed = compare_op_vec (<=) true -let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false -let gt_vec_unsigned = compare_op_vec (>) false -let lteq_vec_unsigned = compare_op_vec (<=) false -let gteq_vec_unsigned = compare_op_vec (>=) false - -let compare_op_vec_range op sign (l,r) = - compare_op op ((to_num sign l),r) - -let lt_vec_range = compare_op_vec_range (<) true -let gt_vec_range = compare_op_vec_range (>) true -let lteq_vec_range = compare_op_vec_range (<=) true -let gteq_vec_range = compare_op_vec_range (>=) true - -let compare_op_range_vec op sign (l,r) = - compare_op op (l, (to_num sign r)) +instance forall 'a. BitU 'a => (Bitvector (list 'a)) + let bits_of v = List.map to_bitU v + let of_bits v = List.map of_bitU v + let unsigned v = bitlist_to_integer (List.map to_bitU v) + let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n) + let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b] + let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j) + let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map of_bitU v') +end -let lt_range_vec = compare_op_range_vec (<) true -let gt_range_vec = compare_op_range_vec (>) true -let lteq_range_vec = compare_op_range_vec (<=) true -let gteq_range_vec = compare_op_range_vec (>=) true +instance forall 'a. BitU 'a => (Bitvector (vector 'a)) + let bits_of v = List.map to_bitU (get_elems v) + let of_bits v = Vector (List.map of_bitU v) (integerFromNat (List.length v) - 1) false + let unsigned v = unsigned (get_elems v) + let get_bit is_inc start v n = to_bitU (access v n) + let set_bit is_inc start v n b = update_pos v n (of_bitU b) + let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j)) + let set_bits is_inc start v i j v' = update v i j (Vector (List.map of_bitU v') (integerFromNat (List.length v') - 1) false) +end -let eq (l,r) = bool_to_bitU (l = r) -let eq_range (l,r) = bool_to_bitU (l = r) -let eq_vec (l,r) = bool_to_bitU (l = r) -let eq_bit (l,r) = bool_to_bitU (l = r) -let eq_vec_range (l,r) = eq (to_num false l,r) -let eq_range_vec (l,r) = eq (l, to_num false r) -let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) +instance forall 'a. Size 'a => (Bitvector (mword 'a)) + let bits_of v = List.map to_bitU (bitlistFromWord v) + let of_bits v = wordFromBitlist (List.map of_bitU v) + let unsigned v = unsignedIntegerFromWord v + let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n) + let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [of_bitU b]) + let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j + let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map of_bitU v')) +end -let neq (l,r) = bitwise_not_bit (eq (l,r)) -let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r)) -let neq_range (l,r) = bitwise_not_bit (eq_range (l,r)) -let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) -let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) -let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) +(*let showBitvector (Bitvector elems start inc) = + "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc +let bvget_dir (Bitvector _ _ ord) = ord +let bvget_start (Bitvector _ s _) = s +let bvget_elems (Bitvector elems _ _) = elems -val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a -let make_indexed_vector entries default start length dir = - let length = natFromInteger length in - Vector (List.foldl replace (replicate length default) entries) start dir +instance forall 'a. (Show (bitvector 'a)) + let show = showBitvector +end*) -(* -val make_bit_vector_undef : integer -> vector bitU -let make_bitvector_undef length = - Vector (replicate (natFromInteger length) BU) 0 true - *) +let bvec_to_vec is_inc start bs = + let bits = List.map bool_to_bitU (bitlistFromWord bs) in + Vector bits start is_inc -(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) +let vec_to_bvec (Vector elems start is_inc) = + (*let word =*) wordFromBitlist (List.map bitU_to_bool elems) (*in + Bitvector word start is_inc*) -let mask (n,Vector bits start dir) = - let current_size = List.length bits in - Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir +(*** Vector operations *) +(* Bytes and addresses *) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) let rec byte_chunks n list = match (n,list) with @@ -679,37 +405,37 @@ let rec byte_chunks n list = match (n,list) with | _ -> failwith "byte_chunks not given enough bits" end -val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU +val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> list bitU let bitv_of_byte_lifteds dir v = let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in let len = integerFromNat (List.length bits) in - Vector bits (if dir then 0 else len - 1) dir + bits (*Vector bits (if dir then 0 else len - 1) dir*) -val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU +val bitv_of_bytes : bool -> list Sail_impl_base.byte -> list bitU let bitv_of_bytes dir v = let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in let len = integerFromNat (List.length bits) in - Vector bits (if dir then 0 else len - 1) dir + bits (*Vector bits (if dir then 0 else len - 1) dir*) -val byte_lifteds_of_bitv : vector bitU -> list byte_lifted -let byte_lifteds_of_bitv (Vector bits length is_inc) = +val byte_lifteds_of_bitv : list bitU -> list byte_lifted +let byte_lifteds_of_bitv bits = let bits = List.map bit_lifted_of_bitU bits in byte_lifteds_of_bit_lifteds bits -val bytes_of_bitv : vector bitU -> list byte -let bytes_of_bitv (Vector bits length is_inc) = +val bytes_of_bitv : list bitU -> list byte +let bytes_of_bitv bits = let bits = List.map bit_of_bitU bits in bytes_of_bits bits val bit_lifteds_of_bitUs : list bitU -> list bit_lifted let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits -val bit_lifteds_of_bitv : vector bitU -> list bit_lifted -let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs (get_elems v) +val bit_lifteds_of_bitv : list bitU -> list bit_lifted +let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v -val address_lifted_of_bitv : vector bitU -> address_lifted +val address_lifted_of_bitv : list bitU -> address_lifted let address_lifted_of_bitv v = let byte_lifteds = byte_lifteds_of_bitv v in let maybe_address_integer = @@ -719,11 +445,17 @@ let address_lifted_of_bitv v = end in Address_lifted byte_lifteds maybe_address_integer -val address_of_bitv : vector bitU -> address +val address_of_bitv : list bitU -> address let address_of_bitv v = let bytes = bytes_of_bitv v in address_of_byte_list bytes +let rec reverse_endianness_bl bits = + if List.length bits <= 8 then bits else + list_append(reverse_endianness_bl(list_drop(8, bits)), list_take(8, bits)) + +val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a +let reverse_endianness v = of_bits (reverse_endianness_bl (bits_of v)) (*** Registers *) @@ -740,6 +472,20 @@ type register = | UndefinedRegister of integer (* length *) | RegisterPair of register * register +type register_ref 'regstate 'a = + <| reg_name : string; + reg_start : integer; + reg_is_inc : bool; + read_from : 'regstate -> 'a; + write_to : 'regstate -> 'a -> 'regstate |> + +type field_ref 'regtype 'a = + <| field_name : string; + field_start : integer; + field_is_inc : bool; + get_field : 'regtype -> 'a; + set_field : 'regtype -> 'a -> 'regtype |> + let name_of_reg = function | Register name _ _ _ _ -> name | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" @@ -815,11 +561,11 @@ let rec external_reg_value reg_name v = rv_start = external_start; rv_start_internal = internal_start |> -val internal_reg_value : register_value -> vector bitU +val internal_reg_value : register_value -> list bitU let internal_reg_value v = - Vector (List.map bitU_of_bit_lifted v.rv_bits) - (integerFromNat v.rv_start_internal) - (v.rv_dir = D_increasing) + List.map bitU_of_bit_lifted v.rv_bits + (*(integerFromNat v.rv_start_internal) + (v.rv_dir = D_increasing)*) let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = @@ -866,7 +612,7 @@ let internal_mem_value direction bytes = val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars let rec foreach_inc (i,stop,by) vars body = - if i <= stop + 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 @@ -874,7 +620,7 @@ let rec foreach_inc (i,stop,by) vars body = val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars let rec foreach_dec (i,stop,by) vars body = - if i >= stop + 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 @@ -884,7 +630,7 @@ let assert' b msg_opt = | Just msg -> msg | Nothing -> "unspecified error" end in - if bitU_to_bool b then () else failwith msg + if b then () else failwith msg (* convert numbers unsafely to naturals *) @@ -902,8 +648,9 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) = toNatural n4, toNatural n5) - -type regfp = +(* Let the following types be generated by Sail per spec, using either bitlists + or machine words as bitvector representation *) +(*type regfp = | RFull of (string) | RSlice of (string * integer * integer) | RSliceBit of (string * integer) @@ -945,7 +692,7 @@ end let niafp_to_nia reginfo = function | NIAFP_successor -> NIA_successor - | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) + | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv (bits_of v)) | NIAFP_LR -> NIA_LR | NIAFP_CTR -> NIA_CTR | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) @@ -953,9 +700,7 @@ end let diafp_to_dia reginfo = function | DIAFP_none -> DIA_none - | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) + | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv (bits_of v)) | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) end - -let max = uncurry max -let min = uncurry min +*) diff --git a/src/gen_lib/sail_values_word.lem b/src/gen_lib/sail_values_word.lem deleted file mode 100644 index 048bf30a..00000000 --- a/src/gen_lib/sail_values_word.lem +++ /dev/null @@ -1,1030 +0,0 @@ -(* Version of sail_values.lem that uses Lem's machine words library *) - -open import Pervasives_extra -open import Machine_word -open import Sail_impl_base - - -type ii = integer -type nn = natural - -val pow : integer -> integer -> integer -let pow m n = m ** (natFromInteger n) - -let rec replace bs ((n : integer),b') = match bs with - | [] -> [] - | b :: bs -> - if n = 0 then b' :: bs - else b :: replace bs (n - 1,b') - end - - -(*** Bits *) -type bitU = B0 | B1 | BU - -let showBitU = function - | B0 -> "O" - | B1 -> "I" - | BU -> "U" -end - -instance (Show bitU) - let show = showBitU -end - - -let bitU_to_bool = function - | B0 -> false - | B1 -> true - | BU -> failwith "to_bool applied to BU" - end - -let bit_lifted_of_bitU = function - | B0 -> Bitl_zero - | B1 -> Bitl_one - | BU -> Bitl_undef - end - -let bitU_of_bit = function - | Bitc_zero -> B0 - | Bitc_one -> B1 - end - -let bit_of_bitU = function - | B0 -> Bitc_zero - | B1 -> Bitc_one - | BU -> failwith "bit_of_bitU: BU" - end - -let bitU_of_bit_lifted = function - | Bitl_zero -> B0 - | Bitl_one -> B1 - | Bitl_undef -> BU - | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" - end - -let bitwise_not_bit = function - | B1 -> B0 - | B0 -> B1 - | BU -> BU - end - -let inline (~) = bitwise_not_bit - -val is_one : integer -> bitU -let is_one i = - if i = 1 then B1 else B0 - -let bool_to_bitU b = if b then B1 else B0 - -let bitwise_binop_bit op = function - | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) - | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) - | (x,y) -> bool_to_bitU (op (bitU_to_bool x) (bitU_to_bool y)) - end - -val bitwise_and_bit : bitU * bitU -> bitU -let bitwise_and_bit = bitwise_binop_bit (&&) - -val bitwise_or_bit : bitU * bitU -> bitU -let bitwise_or_bit = bitwise_binop_bit (||) - -val bitwise_xor_bit : bitU * bitU -> bitU -let bitwise_xor_bit = bitwise_binop_bit xor - -val (&.) : bitU -> bitU -> bitU -let inline (&.) x y = bitwise_and_bit (x,y) - -val (|.) : bitU -> bitU -> bitU -let inline (|.) x y = bitwise_or_bit (x,y) - -val (+.) : bitU -> bitU -> bitU -let inline (+.) x y = bitwise_xor_bit (x,y) - - - -(*** Vectors *) - -(* element list * start * has increasing direction *) -type vector 'a = Vector of list 'a * integer * bool - -let showVector (Vector elems start inc) = - "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc - -let get_dir (Vector _ _ ord) = ord -let get_start (Vector _ s _) = s -let get_elems (Vector elems _ _) = elems -let length (Vector bs _ _) = integerFromNat (length bs) - -instance forall 'a. Show 'a => (Show (vector 'a)) - let show = showVector -end - -let dir is_inc = if is_inc then D_increasing else D_decreasing -let bool_of_dir = function - | D_increasing -> true - | D_decreasing -> false - end - -(*** Vector operations *) - -val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a -let set_vector_start new_start (Vector bs _ is_inc) = - Vector bs new_start is_inc - -let reset_vector_start v = - set_vector_start (if (get_dir v) then 0 else (length v - 1)) v - -let set_vector_start_to_length v = - set_vector_start (length v - 1) v - -let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = - Vector (bs ++ bs') start is_inc - -let inline (^^) = vector_concat - -val sublist : forall 'a. list 'a -> (nat * nat) -> list 'a -let sublist xs (i,j) = - let (toJ,_suffix) = List.splitAt (j+1) xs in - let (_prefix,fromItoJ) = List.splitAt i toJ in - fromItoJ - -val update_sublist : forall 'a. list 'a -> (nat * nat) -> list 'a -> list 'a -let update_sublist xs (i,j) xs' = - let (toJ,suffix) = List.splitAt (j+1) xs in - let (prefix,_fromItoJ) = List.splitAt i toJ in - prefix ++ xs' ++ suffix - -val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a -let slice (Vector bs start is_inc) i j = - let iN = natFromInteger i in - let jN = natFromInteger j in - let startN = natFromInteger start in - let subvector_bits = - sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in - Vector subvector_bits i is_inc - -(* this is for the vector slicing introduced in vector-concat patterns: i and j -index into the "raw data", the list of bits. Therefore getting the bit list is -easy, but the start index has to be transformed to match the old vector start -and the direction. *) -val slice_raw : forall 'a. vector 'a -> integer -> integer -> vector 'a -let slice_raw (Vector bs start is_inc) i j = - let iN = natFromInteger i in - let jN = natFromInteger j in - let bits = sublist bs (iN,jN) in - let len = integerFromNat (List.length bits) in - Vector bits (if is_inc then 0 else len - 1) is_inc - - -val update_aux : forall 'a. vector 'a -> integer -> integer -> list 'a -> vector 'a -let update_aux (Vector bs start is_inc) i j bs' = - let iN = natFromInteger i in - let jN = natFromInteger j in - let startN = natFromInteger start in - let bits = - (update_sublist bs) - (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' in - Vector bits start is_inc - -val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a -let update v i j (Vector bs' _ _) = - update_aux v i j bs' - -val access : forall 'a. vector 'a -> integer -> 'a -let access (Vector bs start is_inc) n = - if is_inc then List_extra.nth bs (natFromInteger (n - start)) - else List_extra.nth bs (natFromInteger (start - n)) - -val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a -let update_pos v n b = - update_aux v n n [b] - -(*** Bitvectors *) - -(* element list * start * has increasing direction *) -type bitvector 'a = Bitvector of mword 'a * integer * bool - -let showBitvector (Bitvector elems start inc) = - "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc - -let bvget_dir (Bitvector _ _ ord) = ord -let bvget_start (Bitvector _ s _) = s -let bvget_elems (Bitvector elems _ _) = elems -let bvlength (Bitvector bs _ _) = integerFromNat (word_length bs) - -instance forall 'a. Show 'a => (Show (bitvector 'a)) - let show = showBitvector -end - -(*** Vector operations *) - -val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a -let set_bitvector_start new_start (Bitvector bs _ is_inc) = - Bitvector bs new_start is_inc - -let reset_bitvector_start v = - set_bitvector_start (if (bvget_dir v) then 0 else (bvlength v - 1)) v - -let set_bitvector_start_to_length v = - set_bitvector_start (bvlength v - 1) v - -let bitvector_concat (Bitvector bs start is_inc) (Bitvector bs' _ _) = - Bitvector (word_concat bs bs') start is_inc - -let inline (^^^) = bitvector_concat - -val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -let bvslice (Bitvector bs start is_inc) i j = - let iN = natFromInteger i in - let jN = natFromInteger j in - let startN = natFromInteger start in - let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in - let subvector_bits = word_extract lo hi bs in - Bitvector subvector_bits i is_inc - -(* this is for the vector slicing introduced in vector-concat patterns: i and j -index into the "raw data", the list of bits. Therefore getting the bit list is -easy, but the start index has to be transformed to match the old vector start -and the direction. *) -val bvslice_raw : forall 'a 'b. Size 'b => bitvector 'a -> integer -> integer -> bitvector 'b -let bvslice_raw (Bitvector bs start is_inc) i j = - let iN = natFromInteger i in - let jN = natFromInteger j in - let bits = word_extract iN jN bs in - let len = integerFromNat (word_length bits) in - Bitvector bits (if is_inc then 0 else len - 1) is_inc - -val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a -let bvupdate_aux (Bitvector bs start is_inc) i j bs' = - let iN = natFromInteger i in - let jN = natFromInteger j in - let startN = natFromInteger start in - let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in - let bits = word_update bs lo hi bs' in - Bitvector bits start is_inc - -val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a -let bvupdate v i j (Bitvector bs' _ _) = - bvupdate_aux v i j bs' - -(* TODO: decide between nat/natural, change either here or in machine_word *) -val getBit' : forall 'a. mword 'a -> nat -> bool -let getBit' w n = getBit w (naturalFromNat n) - -val bvaccess : forall 'a. bitvector 'a -> integer -> bool -let bvaccess (Bitvector bs start is_inc) n = - if is_inc then getBit' bs (natFromInteger (n - start)) - else getBit' bs (natFromInteger (start - n)) - -val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bool -> bitvector 'a -let bvupdate_pos v n b = - bvupdate_aux v n n (wordFromNatural (if b then 1 else 0)) - -(*** Bit vector operations *) - -let extract_only_bit (Bitvector elems _ _) = - let l = word_length elems in - if l = 1 then - msb elems - else if l = 0 then - failwith "extract_single_bit called for empty vector" - else - failwith "extract_single_bit called for vector with more bits" - -let pp_bitu_vector (Vector elems start inc) = - let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in - "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc - - -let most_significant (Bitvector v _ _) = - if word_length v = 0 then - failwith "most_significant applied to empty vector" - else - msb v - -let bitwise_not_bitlist = List.map bitwise_not_bit - -let bitwise_not (Bitvector bs start is_inc) = - Bitvector (lNot bs) start is_inc - -let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) = - Bitvector (op bsl bsr) start is_inc - -let bitwise_and = bitwise_binop lAnd -let bitwise_or = bitwise_binop lOr -let bitwise_xor = bitwise_binop lXor - -let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs -let unsigned_big = unsigned - -let signed (Bitvector v _ _) : integer = signedIntegerFromWord v - -let hardware_mod (a: integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) mod (abs b) - else if (a < 0 && b >= 0) - then (a mod b) - b - else a mod b - -(* There are different possible answers for integer divide regarding -rounding behaviour on negative operands. Positive operands always -round down so derive the one we want (trucation towards zero) from -that *) -let hardware_quot (a:integer) (b:integer) : integer = - let q = (abs a) / (abs b) in - if ((a<0) = (b<0)) then - q (* same sign -- result positive *) - else - ~q (* different sign -- result negative *) - -let quot_signed = hardware_quot - - -let signed_big = signed - -let to_num sign = if sign then signed else unsigned - -let max_64u = (integerPow 2 64) - 1 -let max_64 = (integerPow 2 63) - 1 -let min_64 = 0 - (integerPow 2 63) -let max_32u = (4294967295 : integer) -let max_32 = (2147483647 : integer) -let min_32 = (0 - 2147483648 : integer) -let max_8 = (127 : integer) -let min_8 = (0 - 128 : integer) -let max_5 = (31 : integer) -let min_5 = (0 - 32 : integer) - -let get_max_representable_in sign (n : integer) : integer = - if (n = 64) then match sign with | true -> max_64 | false -> max_64u end - else if (n=32) then match sign with | true -> max_32 | false -> max_32u end - else if (n=8) then max_8 - else if (n=5) then max_5 - else match sign with | true -> integerPow 2 ((natFromInteger n) -1) - | false -> integerPow 2 (natFromInteger n) - end - -let get_min_representable_in _ (n : integer) : integer = - if n = 64 then min_64 - else if n = 32 then min_32 - else if n = 8 then min_8 - else if n = 5 then min_5 - else 0 - (integerPow 2 (natFromInteger n)) - -val to_bin_aux : natural -> list bitU -let rec to_bin_aux x = - if x = 0 then [] - else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) -let to_bin n = List.reverse (to_bin_aux n) - -val pad_zero : list bitU -> integer -> list bitU -let rec pad_zero bits n = - if n = 0 then bits else pad_zero (B0 :: bits) (n -1) - - -let rec add_one_bit_ignore_overflow_aux bits = match bits with - | [] -> [] - | B0 :: bits -> B1 :: bits - | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits - | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" -end - -let add_one_bit_ignore_overflow bits = - List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) - -let to_vec is_inc ((len : integer),(n : integer)) = - let start = if is_inc then 0 else len - 1 in - let bits = wordFromInteger n in - if integerFromNat (word_length bits) = len then - Bitvector bits start is_inc - else - failwith "Vector length mismatch in to_vec" - -let to_vec_big = to_vec - -let to_vec_inc = to_vec true -let to_vec_dec = to_vec false -(* TODO?? -let to_vec_undef is_inc (len : integer) = - Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc - -let to_vec_inc_undef = to_vec_undef true -let to_vec_dec_undef = to_vec_undef false -*) -let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec) -let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec) - -let exts_big (len, vec) = to_vec_big (bvget_dir vec) (len, signed_big vec) -let extz_big (len, vec) = to_vec_big (bvget_dir vec) (len, unsigned_big vec) - -let add = integerAdd -let add_signed = integerAdd -let minus = integerMinus -let multiply = integerMult -let modulo = hardware_mod -let quot = hardware_quot -let power = integerPow - -(* TODO: this, and the definitions that use it, currently requires Size for - to_vec, which I'd rather avoid *) -let arith_op_vec op sign (size : integer) (Bitvector _ _ is_inc as l) r = - let (l',r') = (to_num sign l, to_num sign r) in - let n = op l' r' in - to_vec is_inc (size * (bvlength l),n) - - -(* add_vec - * add_vec_signed - * minus_vec - * multiply_vec - * multiply_vec_signed - *) -let add_VVV = arith_op_vec integerAdd false 1 -let addS_VVV = arith_op_vec integerAdd true 1 -let minus_VVV = arith_op_vec integerMinus false 1 -let mult_VVV = arith_op_vec integerMult false 2 -let multS_VVV = arith_op_vec integerMult true 2 - -val arith_op_vec_range : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> integer -> bitvector 'a -let arith_op_vec_range op sign size (Bitvector _ _ is_inc as l) r = - arith_op_vec op sign size l (to_vec is_inc (bvlength l,r)) - -(* add_vec_range - * add_vec_range_signed - * minus_vec_range - * mult_vec_range - * mult_vec_range_signed - *) -let add_VIV = arith_op_vec_range integerAdd false 1 -let addS_VIV = arith_op_vec_range integerAdd true 1 -let minus_VIV = arith_op_vec_range integerMinus false 1 -let mult_VIV = arith_op_vec_range integerMult false 2 -let multS_VIV = arith_op_vec_range integerMult true 2 - -val arith_op_range_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> integer -> bitvector 'a -> bitvector 'a -let arith_op_range_vec op sign size l (Bitvector _ _ is_inc as r) = - arith_op_vec op sign size (to_vec is_inc (bvlength r, l)) r - -(* add_range_vec - * add_range_vec_signed - * minus_range_vec - * mult_range_vec - * mult_range_vec_signed - *) -let add_IVV = arith_op_range_vec integerAdd false 1 -let addS_IVV = arith_op_range_vec integerAdd true 1 -let minus_IVV = arith_op_range_vec integerMinus false 1 -let mult_IVV = arith_op_range_vec integerMult false 2 -let multS_IVV = arith_op_range_vec integerMult true 2 - -let arith_op_range_vec_range op sign l r = op l (to_num sign r) - -(* add_range_vec_range - * add_range_vec_range_signed - * minus_range_vec_range - *) -let add_IVI = arith_op_range_vec_range integerAdd false -let addS_IVI = arith_op_range_vec_range integerAdd true -let minus_IVI = arith_op_range_vec_range integerMinus false - -let arith_op_vec_range_range op sign l r = op (to_num sign l) r - -(* add_vec_range_range - * add_vec_range_range_signed - * minus_vec_range_range - *) -let add_VII = arith_op_vec_range_range integerAdd false -let addS_VII = arith_op_vec_range_range integerAdd true -let minus_VII = arith_op_vec_range_range integerMinus false - - - -let arith_op_vec_vec_range op sign l r = - let (l',r') = (to_num sign l,to_num sign r) in - op l' r' - -(* add_vec_vec_range - * add_vec_vec_range_signed - *) -let add_VVI = arith_op_vec_vec_range integerAdd false -let addS_VVI = arith_op_vec_vec_range integerAdd true - -let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l)r = - let l' = to_num sign l in - let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - to_vec is_inc (bvlength l * size,n) - -(* add_vec_bit - * add_vec_bit_signed - * minus_vec_bit_signed - *) -let add_VBV = arith_op_vec_bit integerAdd false 1 -let addS_VBV = arith_op_vec_bit integerAdd true 1 -let minus_VBV = arith_op_vec_bit integerMinus true 1 - -val arith_op_overflow_vec : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'a * bitU * bool -let rec arith_op_overflow_vec op sign size (Bitvector _ _ is_inc as l) r = - let len = bvlength l in - let act_size = len * size in - let (l_sign,r_sign) = (to_num sign l,to_num sign r) in - let (l_unsign,r_unsign) = (to_num false l,to_num false r) in - let n = op l_sign r_sign in - let n_unsign = op l_unsign r_unsign in - let correct_size_num = to_vec is_inc (act_size,n) in - let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in - let overflow = - if n <= get_max_representable_in sign len && - n >= get_min_representable_in sign len - then B0 else B1 in - let c_out = most_significant one_more_size_u in - (correct_size_num,overflow,c_out) - -(* add_overflow_vec - * add_overflow_vec_signed - * minus_overflow_vec - * minus_overflow_vec_signed - * mult_overflow_vec - * mult_overflow_vec_signed - *) -let addO_VVV = arith_op_overflow_vec integerAdd false 1 -let addSO_VVV = arith_op_overflow_vec integerAdd true 1 -let minusO_VVV = arith_op_overflow_vec integerMinus false 1 -let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 -let multO_VVV = arith_op_overflow_vec integerMult false 2 -let multSO_VVV = arith_op_overflow_vec integerMult true 2 - -val arith_op_overflow_vec_bit : forall 'a. Size 'a => (integer -> integer -> integer) -> bool -> integer -> - bitvector 'a -> bitU -> bitvector 'a * bitU * bool -let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) - (Bitvector _ _ is_inc as l) r_bit = - let act_size = bvlength l * size in - let l' = to_num sign l in - let l_u = to_num false l in - let (n,nu,changed) = match r_bit with - | B1 -> (op l' 1, op l_u 1, true) - | B0 -> (l',l_u,false) - | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" - end in -(* | _ -> assert false *) - let correct_size_num = to_vec is_inc (act_size,n) in - let one_larger = to_vec is_inc (act_size + 1,nu) in - let overflow = - if changed - then - if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then B0 else B1 - else B0 in - (correct_size_num,overflow,most_significant one_larger) - -(* add_overflow_vec_bit_signed - * minus_overflow_vec_bit - * minus_overflow_vec_bit_signed - *) -let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 -let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 -let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 - -type shift = LL_shift | RR_shift | LLL_shift - -let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) = - let n = natFromInteger n in - match op with - | LL_shift (*"<<"*) -> - Bitvector (shiftLeft bs (naturalFromNat n)) start is_inc - | RR_shift (*">>"*) -> - Bitvector (shiftRight bs (naturalFromNat n)) start is_inc - | LLL_shift (*"<<<"*) -> - Bitvector (rotateLeft (naturalFromNat n) bs) start is_inc - end - -let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) -let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) -let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) - -let rec arith_op_no0 (op : integer -> integer -> integer) l r = - if r = 0 - then Nothing - else Just (op l r) -(* TODO -let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Bitvector _ start is_inc) as l) r = - let act_size = bvlength l * size in - let (l',r') = (to_num sign l,to_num sign r) in - let n = arith_op_no0 op l' r' in - let (representable,n') = - match n with - | Just n' -> - (n' <= get_max_representable_in sign act_size && - n' >= get_min_representable_in sign act_size, n') - | _ -> (false,0) - end in - if representable - then to_vec is_inc (act_size,n') - else Vector (List.replicate (natFromInteger act_size) BU) start is_inc - -let mod_VVV = arith_op_vec_no0 hardware_mod false 1 -let quot_VVV = arith_op_vec_no0 hardware_quot false 1 -let quotS_VVV = arith_op_vec_no0 hardware_quot true 1 - -let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = - let rep_size = length r * size in - let act_size = length l * size in - let (l',r') = (to_num sign l,to_num sign r) in - let (l_u,r_u) = (to_num false l,to_num false r) in - let n = arith_op_no0 op l' r' in - let n_u = arith_op_no0 op l_u r_u in - let (representable,n',n_u') = - match (n, n_u) with - | (Just n',Just n_u') -> - ((n' <= get_max_representable_in sign rep_size && - n' >= (get_min_representable_in sign rep_size)), n', n_u') - | _ -> (true,0,0) - end in - let (correct_size_num,one_more) = - if representable then - (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u')) - else - (Vector (List.replicate (natFromInteger act_size) BU) start is_inc, - Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in - let overflow = if representable then B0 else B1 in - (correct_size_num,overflow,most_significant one_more) - -let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 -let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 - -let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = - arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r)) - -let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 -*) -val repeat : forall 'a. list 'a -> integer -> list 'a -let rec repeat xs n = - if n = 0 then [] - else xs ++ repeat xs (n-1) - -(* -let duplicate bit length = - Vector (repeat [bit] length) (if dir then 0 else length - 1) dir - *) - -let compare_op op (l,r) = bool_to_bitU (op l r) - -let lt = compare_op (<) -let gt = compare_op (>) -let lteq = compare_op (<=) -let gteq = compare_op (>=) - - -let compare_op_vec op sign (l,r) = - let (l',r') = (to_num sign l, to_num sign r) in - compare_op op (l',r') - -let lt_vec = compare_op_vec (<) true -let gt_vec = compare_op_vec (>) true -let lteq_vec = compare_op_vec (<=) true -let gteq_vec = compare_op_vec (>=) true - -let lt_vec_signed = compare_op_vec (<) true -let gt_vec_signed = compare_op_vec (>) true -let lteq_vec_signed = compare_op_vec (<=) true -let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false -let gt_vec_unsigned = compare_op_vec (>) false -let lteq_vec_unsigned = compare_op_vec (<=) false -let gteq_vec_unsigned = compare_op_vec (>=) false - -let compare_op_vec_range op sign (l,r) = - compare_op op ((to_num sign l),r) - -let lt_vec_range = compare_op_vec_range (<) true -let gt_vec_range = compare_op_vec_range (>) true -let lteq_vec_range = compare_op_vec_range (<=) true -let gteq_vec_range = compare_op_vec_range (>=) true - -let compare_op_range_vec op sign (l,r) = - compare_op op (l, (to_num sign r)) - -let lt_range_vec = compare_op_range_vec (<) true -let gt_range_vec = compare_op_range_vec (>) true -let lteq_range_vec = compare_op_range_vec (<=) true -let gteq_range_vec = compare_op_range_vec (>=) true - -let eq (l,r) = bool_to_bitU (l = r) -let eq_range (l,r) = bool_to_bitU (l = r) -let eq_vec (l,r) = bool_to_bitU (l = r) -let eq_bit (l,r) = bool_to_bitU (l = r) -let eq_vec_range (l,r) = eq (to_num false l,r) -let eq_range_vec (l,r) = eq (l, to_num false r) -let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) - -let neq (l,r) = bitwise_not_bit (eq (l,r)) -let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r)) -let neq_range (l,r) = bitwise_not_bit (eq_range (l,r)) -let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) -let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) -let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) - - -val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a -let make_indexed_vector entries default start length dir = - let length = natFromInteger length in - Vector (List.foldl replace (replicate length default) entries) start dir - -(* -val make_bit_vector_undef : integer -> vector bitU -let make_bitvector_undef length = - Vector (replicate (natFromInteger length) BU) 0 true - *) - -(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) - -let mask (n,Vector bits start dir) = - let current_size = List.length bits in - Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir - - -val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) -let rec byte_chunks n list = match (n,list) with - | (0,_) -> [] - | (n+1, a::b::c::d::e::f::g::h::rest) -> [a;b;c;d;e;f;g;h] :: byte_chunks n rest - | _ -> failwith "byte_chunks not given enough bits" -end - -val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU -let bitv_of_byte_lifteds dir v = - let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in - let len = integerFromNat (List.length bits) in - Vector bits (if dir then 0 else len - 1) dir - -val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU -let bitv_of_bytes dir v = - let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in - let len = integerFromNat (List.length bits) in - Vector bits (if dir then 0 else len - 1) dir - - -val byte_lifteds_of_bitv : vector bitU -> list byte_lifted -let byte_lifteds_of_bitv (Vector bits length is_inc) = - let bits = List.map bit_lifted_of_bitU bits in - byte_lifteds_of_bit_lifteds bits - -val bytes_of_bitv : vector bitU -> list byte -let bytes_of_bitv (Vector bits length is_inc) = - let bits = List.map bit_of_bitU bits in - bytes_of_bits bits - -val bit_lifteds_of_bitUs : list bitU -> list bit_lifted -let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits - -val bit_lifteds_of_bitv : vector bitU -> list bit_lifted -let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs (get_elems v) - - -val address_lifted_of_bitv : vector bitU -> address_lifted -let address_lifted_of_bitv v = - let byte_lifteds = byte_lifteds_of_bitv v in - let maybe_address_integer = - match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with - | Just bs -> Just (integer_of_byte_list bs) - | _ -> Nothing - end in - Address_lifted byte_lifteds maybe_address_integer - -val address_of_bitv : vector bitU -> address -let address_of_bitv v = - let bytes = bytes_of_bitv v in - address_of_byte_list bytes - - - -(*** Registers *) - -type register_field = string -type register_field_index = string * (integer * integer) (* name, start and end *) - -type register = - | Register of string * (* name *) - integer * (* length *) - integer * (* start index *) - bool * (* is increasing *) - list register_field_index - | UndefinedRegister of integer (* length *) - | RegisterPair of register * register - -let name_of_reg = function - | Register name _ _ _ _ -> name - | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" - | RegisterPair _ _ -> failwith "name_of_reg RegisterPair" -end - -let size_of_reg = function - | Register _ size _ _ _ -> size - | UndefinedRegister size -> size - | RegisterPair _ _ -> failwith "size_of_reg RegisterPair" -end - -let start_of_reg = function - | Register _ _ start _ _ -> start - | UndefinedRegister _ -> failwith "start_of_reg UndefinedRegister" - | RegisterPair _ _ -> failwith "start_of_reg RegisterPair" -end - -let is_inc_of_reg = function - | Register _ _ _ is_inc _ -> is_inc - | UndefinedRegister _ -> failwith "is_inc_of_reg UndefinedRegister" - | RegisterPair _ _ -> failwith "in_inc_of_reg RegisterPair" -end - -let dir_of_reg = function - | Register _ _ _ is_inc _ -> dir is_inc - | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister" - | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair" -end - -let size_of_reg_nat reg = natFromInteger (size_of_reg reg) -let start_of_reg_nat reg = natFromInteger (start_of_reg reg) - -val register_field_indices_aux : register -> register_field -> maybe (integer * integer) -let rec register_field_indices_aux register rfield = - match register with - | Register _ _ _ _ rfields -> List.lookup rfield rfields - | RegisterPair r1 r2 -> - let m_indices = register_field_indices_aux r1 rfield in - if isJust m_indices then m_indices else register_field_indices_aux r2 rfield - | UndefinedRegister _ -> Nothing - end - -val register_field_indices : register -> register_field -> integer * integer -let register_field_indices register rfield = - match register_field_indices_aux register rfield with - | Just indices -> indices - | Nothing -> failwith "Invalid register/register-field combination" - end - -let register_field_indices_nat reg regfield= - let (i,j) = register_field_indices reg regfield in - (natFromInteger i,natFromInteger j) - -let rec external_reg_value reg_name v = - let (internal_start, external_start, direction) = - match reg_name with - | Reg _ start size dir -> - (start, (if dir = D_increasing then start else (start - (size +1))), dir) - | Reg_slice _ reg_start dir (slice_start, slice_end) -> - ((if dir = D_increasing then slice_start else (reg_start - slice_start)), - slice_start, dir) - | Reg_field _ reg_start dir _ (slice_start, slice_end) -> - ((if dir = D_increasing then slice_start else (reg_start - slice_start)), - slice_start, dir) - | Reg_f_slice _ reg_start dir _ _ (slice_start, slice_end) -> - ((if dir = D_increasing then slice_start else (reg_start - slice_start)), - slice_start, dir) - end in - let bits = bit_lifteds_of_bitv v in - <| rv_bits = bits; - rv_dir = direction; - rv_start = external_start; - rv_start_internal = internal_start |> - -val internal_reg_value : register_value -> vector bitU -let internal_reg_value v = - Vector (List.map bitU_of_bit_lifted v.rv_bits) - (integerFromNat v.rv_start_internal) - (v.rv_dir = D_increasing) - - -let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = - match d with - (*This is the case the thread/concurrecny model expects, so no change needed*) - | D_increasing -> (i,j) - | D_decreasing -> let slice_i = start - i in - let slice_j = (i - j) + slice_i in - (slice_i,slice_j) - end - -let external_reg_whole reg = - Reg (name_of_reg reg) (start_of_reg_nat reg) (size_of_reg_nat reg) (dir_of_reg reg) - -let external_reg_slice reg (i,j) = - let start = start_of_reg_nat reg in - let dir = dir_of_reg reg in - Reg_slice (name_of_reg reg) start dir (external_slice dir start (i,j)) - -let external_reg_field_whole reg rfield = - let (m,n) = register_field_indices_nat reg rfield in - let start = start_of_reg_nat reg in - let dir = dir_of_reg reg in - Reg_field (name_of_reg reg) start dir rfield (external_slice dir start (m,n)) - -let external_reg_field_slice reg rfield (i,j) = - let (m,n) = register_field_indices_nat reg rfield in - let start = start_of_reg_nat reg in - let dir = dir_of_reg reg in - Reg_f_slice (name_of_reg reg) start dir rfield - (external_slice dir start (m,n)) - (external_slice dir start (i,j)) - -let external_mem_value v = - byte_lifteds_of_bitv v $> List.reverse - -let internal_mem_value direction bytes = - List.reverse bytes $> bitv_of_byte_lifteds direction - - - - - -val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_inc (i,stop,by) vars body = - if i <= stop - then let vars = body i vars in - foreach_inc (i + by,stop,by) vars body - else vars - -val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_dec (i,stop,by) vars body = - if i >= stop - 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 - | Just msg -> msg - | Nothing -> "unspecified error" - end in - if bitU_to_bool b then () else failwith msg - -(* convert numbers unsafely to naturals *) - -class (ToNatural 'a) val toNatural : 'a -> natural end -(* eta-expanded for Isabelle output, otherwise it breaks *) -instance (ToNatural integer) let toNatural = (fun n -> naturalFromInteger n) end -instance (ToNatural int) let toNatural = (fun n -> naturalFromInt n) end -instance (ToNatural nat) let toNatural = (fun n -> naturalFromNat n) end -instance (ToNatural natural) let toNatural = (fun n -> n) end - -let toNaturalFiveTup (n1,n2,n3,n4,n5) = - (toNatural n1, - toNatural n2, - toNatural n3, - toNatural n4, - toNatural n5) - - -type regfp = - | RFull of (string) - | RSlice of (string * integer * integer) - | RSliceBit of (string * integer) - | RField of (string * string) - -type niafp = - | NIAFP_successor - | NIAFP_concrete_address of vector bitU - | NIAFP_LR - | NIAFP_CTR - | NIAFP_register of regfp - -(* only for MIPS *) -type diafp = - | DIAFP_none - | DIAFP_concrete of vector bitU - | DIAFP_reg of regfp - -let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function - | RFull name -> - let (start,length,direction,_) = reg_info name Nothing in - Reg name start length direction - | RSlice (name,i,j) -> - let i = natFromInteger i in - let j = natFromInteger j in - let (start,length,direction,_) = reg_info name Nothing in - let slice = external_slice direction start (i,j) in - Reg_slice name start direction slice - | RSliceBit (name,i) -> - let i = natFromInteger i in - let (start,length,direction,_) = reg_info name Nothing in - let slice = external_slice direction start (i,i) in - Reg_slice name start direction slice - | RField (name,field_name) -> - let (start,length,direction,span) = reg_info name (Just field_name) in - let slice = external_slice direction start span in - Reg_field name start direction field_name slice -end - -let niafp_to_nia reginfo = function - | NIAFP_successor -> NIA_successor - | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) - | NIAFP_LR -> NIA_LR - | NIAFP_CTR -> NIA_CTR - | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) -end - -let diafp_to_dia reginfo = function - | DIAFP_none -> DIA_none - | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) - | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) -end - diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 88e29522..fa0fcd24 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -6,48 +6,88 @@ open import Sail_values type memstate = map integer memory_byte type tagstate = map integer bitU -type regstate = map string (vector bitU) - -type sequential_state = <| regstate : regstate; - memstate : memstate; - tagstate : tagstate; - write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool|> - -type M 'a = sequential_state -> list ((either 'a string) * sequential_state) - -val return : forall 'a. 'a -> M 'a +(* type regstate = map string (vector bitU) *) + +type sequential_state 'regs = + <| regstate : 'regs; + memstate : memstate; + tagstate : tagstate; + write_ea : maybe (write_kind * integer * integer); + last_exclusive_operation_was_load : bool|> + +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 |> + +(* State, nondeterminism and exception monad with result type 'a + and exception type 'e. *) +type ME 'regs 'a 'e = sequential_state 'regs -> list ((either 'a 'e) * sequential_state 'regs) + +(* By default, we use strings to distinguish between different types of exceptions *) +type M 'regs 'a = ME 'regs 'a string + +(* For early return, we abuse exceptions by throwing and catching + the return value. The exception type is "either 'r string", where "Right e" + represents a proper exception and "Left r" an early return of value "r". *) +type MR 'regs 'a 'r = ME 'regs 'a (either 'r string) + +val liftR : forall 'a 'r 'regs. M 'regs 'a -> MR 'regs 'a 'r +let liftR m s = List.map (function + | (Left a, s') -> (Left a, s') + | (Right e, s') -> (Right (Right e), s') + end) (m s) + +val return : forall 'regs 'a 'e. 'a -> ME 'regs 'a 'e let return a s = [(Left a,s)] -val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b -let bind m f (s : sequential_state) = +val bind : forall 'regs 'a 'b 'e. ME 'regs 'a 'e -> ('a -> ME 'regs 'b 'e) -> ME 'regs 'b 'e +let bind m f (s : sequential_state 'regs) = List.concatMap (function | (Left a, s') -> f a s' | (Right e, s') -> [(Right e, s')] end) (m s) let inline (>>=) = bind -val (>>): forall 'b. M unit -> M 'b -> M 'b +val (>>): forall 'regs 'b 'e. ME 'regs unit 'e -> ME 'regs 'b 'e -> ME 'regs 'b 'e let inline (>>) m n = m >>= fun _ -> n -val exit : forall 'e 'a. 'e -> M 'a -let exit _ s = [(Right "exit",s)] +val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a +let exit _ s = [(Right "exit", s)] + +val assert_exp : forall 'regs. bool -> string -> M 'regs unit +let assert_exp exp msg s = if exp then [(Left (), s)] else [(Right msg, s)] +val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r +let early_return r s = [(Right (Left r), s)] + +val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a +let catch_early_return m s = + List.map + (function + | (Right (Left a), s') -> (Left a, s') + | (Right (Right e), s') -> (Right e, s') + | (Left a, s') -> (Left a, s') + end) (m s) val range : integer -> integer -> list integer -let rec range i j = - if i = j then [i] +let rec range i j = + if j < i then [] + else if i = j then [i] else i :: range (i+1) j -val get_reg : sequential_state -> string -> vector bitU -let get_reg state reg = Map_extra.find reg state.regstate +val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a +let get_reg state reg = reg.read_from state.regstate -val set_reg : sequential_state -> string -> vector bitU -> sequential_state -let set_reg state reg bitv = - <| state with regstate = Map.insert reg bitv state.regstate |> +val set_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a -> sequential_state 'regs +let set_reg state reg v = + <| state with regstate = reg.write_to state.regstate v |> -let is_exclusive = function +let is_exclusive = function | Sail_impl_base.Read_plain -> false | Sail_impl_base.Read_reserve -> true | Sail_impl_base.Read_acquire -> false @@ -63,13 +103,12 @@ let is_exclusive = function end -val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU) +val read_mem : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b let read_mem dir read_kind addr sz state = - let addr = integer_of_address (address_of_bitv addr) in + let addr = unsigned addr in let addrs = range addr (addr+sz-1) in let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in - let value = Sail_values.internal_mem_value dir memory_value in - + let value = of_bits (Sail_values.internal_mem_value dir memory_value) in if is_exclusive read_kind then [(Left value, <| state with last_exclusive_operation_was_load = true |>)] else [(Left value, state)] @@ -77,42 +116,40 @@ let read_mem dir read_kind addr sz state = (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : bool -> read_kind -> vector bitU -> M bitU +val read_tag : forall 'regs 'a. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU let read_tag dir read_kind addr state = - let addr = (integer_of_address (address_of_bitv addr)) / cap_alignment in + let addr = (unsigned addr) / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with | Just t -> t | Nothing -> B0 end in - (* TODO Should reading a tag set the exclusive flag? *) if is_exclusive read_kind then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)] else [(Left tag, state)] -val excl_result : unit -> M bool +val excl_result : forall 'regs. unit -> M 'regs bool let excl_result () state = let success = (Left true, <| state with last_exclusive_operation_was_load = false |>) in (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else [] -val write_mem_ea : write_kind -> vector bitU -> integer -> M unit +val write_mem_ea : forall 'regs 'a. Bitvector 'a => write_kind -> 'a -> integer -> M 'regs unit let write_mem_ea write_kind addr sz state = - let addr = integer_of_address (address_of_bitv addr) in - [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)] + [(Left (), <| state with write_ea = Just (write_kind,unsigned addr,sz) |>)] -val write_mem_val : vector bitU -> M bool +val write_mem_val : forall 'a 'regs 'b. Bitvector 'a => 'a -> M 'regs bool let write_mem_val v state = let (write_kind,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 v in + let v = external_mem_value (bits_of v) in let addresses_with_value = List.zip addrs v in let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) state.memstate addresses_with_value in [(Left true, <| state with memstate = memstate |>)] -val write_tag : bitU -> M bool +val write_tag : forall 'regs. bitU -> M 'regs bool let write_tag t state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" @@ -121,71 +158,156 @@ let write_tag t state = let tagstate = Map.insert taddr t state.tagstate in [(Left true, <| state with tagstate = tagstate |>)] -val read_reg : register -> M (vector bitU) +val read_reg : forall 'regs 'a. register_ref 'regs 'a -> M 'regs 'a let read_reg reg state = - let v = Map_extra.find (name_of_reg reg) state.regstate in + let v = reg.read_from state.regstate in + [(Left v,state)] +(*let read_reg_range reg i j state = + let v = slice (get_reg state (name_of_reg reg)) i j in + [(Left (vec_to_bvec v),state)] +let read_reg_bit reg i state = + let v = access (get_reg state (name_of_reg reg)) i in [(Left v,state)] -let read_reg_range reg i j = - read_reg reg >>= fun rv -> - return (slice rv i j) -let read_reg_bit reg i = - read_reg_range reg i i >>= fun v -> - return (extract_only_bit v) let read_reg_field reg regfield = let (i,j) = register_field_indices reg regfield in read_reg_range reg i j let read_reg_bitfield reg regfield = let (i,_) = register_field_indices reg regfield in - read_reg_bit reg i + read_reg_bit reg i *) -val write_reg : register -> vector bitU -> M unit +let reg_deref = read_reg + +val write_reg : forall 'regs 'a. register_ref 'regs 'a -> 'a -> M 'regs unit let write_reg reg v state = - [(Left (),<| state with regstate = Map.insert (name_of_reg reg) v state.regstate |>)] -let write_reg_range reg i j v = - read_reg reg >>= fun current_value -> - let new_value = update current_value i j v in - write_reg reg new_value -let write_reg_bit reg i bit = - write_reg_range reg i i (Vector [bit] i (is_inc_of_reg reg)) -let write_reg_field reg regfield = - let (i,j) = register_field_indices reg regfield in - write_reg_range reg i j -let write_reg_bitfield reg regfield = - let (i,_) = register_field_indices reg regfield in - write_reg_bit reg i -let write_reg_field_range reg regfield i j v = - read_reg_field reg regfield >>= fun current_field_value -> - let new_field_value = update current_field_value i j v in - write_reg_field reg regfield new_field_value - - -val barrier : barrier_kind -> M unit + [(Left (), <| state with regstate = reg.write_to state.regstate v |>)] + +let write_reg_ref (reg, v) = write_reg reg v + +val update_reg : forall 'regs 'a 'b. register_ref 'regs 'a -> ('a -> 'b -> 'a) -> 'b -> M 'regs unit +let update_reg reg f v state = + let current_value = get_reg state reg in + let new_value = f current_value v in + [(Left (), set_reg state reg new_value)] + +let write_reg_field reg regfield = update_reg reg regfield.set_field + +val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a +let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) (reg.reg_start) reg_val i j (bits_of new_val) +let write_reg_range reg i j = update_reg reg (update_reg_range reg i j) + +let update_reg_pos reg i reg_val x = update_pos reg_val i x +let write_reg_pos reg i = update_reg reg (update_reg_pos reg i) + +let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) (reg.reg_start) reg_val i (to_bitU bit) +let write_reg_bit reg i = update_reg reg (update_reg_bit reg i) + +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = set_bits (regfield.field_is_inc) (regfield.field_start) current_field_value i j (bits_of new_val) in + regfield.set_field reg_val new_field_value +let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j) + +let update_reg_field_pos regfield i reg_val x = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update_pos current_field_value i x in + regfield.set_field reg_val new_field_value +let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i) + +let update_reg_field_bit regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = set_bit (regfield.field_is_inc) (regfield.field_start) current_field_value i (to_bitU bit) in + regfield.set_field reg_val new_field_value +let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i) + +val barrier : forall 'regs. barrier_kind -> M 'regs unit let barrier _ = return () -val footprint : M unit -let footprint = return () +val footprint : forall 'regs. M 'regs unit +let footprint s = return () s + +val iter_aux : forall 'regs 'e 'a. integer -> (integer -> 'a -> ME 'regs unit 'e) -> list 'a -> ME '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 () + end +val iteri : forall 'regs 'e 'a. (integer -> 'a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e +let iteri f xs = iter_aux 0 f xs -val foreachM_inc : forall 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'vars) -> M 'vars +val iter : forall 'regs 'e 'a. ('a -> ME 'regs unit 'e) -> list 'a -> ME 'regs unit 'e +let iter f xs = iteri (fun _ x -> f x) xs + +val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e let rec foreachM_inc (i,stop,by) vars body = - if i <= stop + 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 'vars. (integer * integer * integer) -> 'vars -> - (integer -> 'vars -> M 'vars) -> M 'vars +val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e let rec foreachM_dec (i,stop,by) vars body = - if i >= stop + 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 -let write_two_regs r1 r2 vec = +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 -> ME 'regs 'vars 'e) -> ME 'regs '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 + +val while_MP : forall 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> + ('vars -> 'vars) -> ME 'regs '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 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> + ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e +let rec while_MM vars cond body = + cond vars >>= fun cond_val -> + if cond_val then + body vars >>= fun vars -> while_MM 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 'regs 'vars 'e. 'vars -> ('vars -> bool) -> + ('vars -> ME 'regs 'vars 'e) -> ME 'regs '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 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> + ('vars -> 'vars) -> ME 'regs '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 'regs 'vars 'e. 'vars -> ('vars -> ME 'regs bool 'e) -> + ('vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e +let rec until_MM vars cond body = + body vars >>= fun vars -> + cond vars >>= fun cond_val -> + if cond_val then return vars else until_MM vars cond body + +(*let write_two_regs r1 r2 bvec state = + let vec = bvec_to_vec bvec in let is_inc = let is_inc_r1 = is_inc_of_reg r1 in let is_inc_r2 = is_inc_of_reg r2 in @@ -204,4 +326,6 @@ let write_two_regs r1 r2 vec = if is_inc then slice vec (size_r1 - start_vec) (size_vec - start_vec) else slice vec (start_vec - size_r1) (start_vec - size_vec) in - write_reg r1 r1_v >> write_reg r2 r2_v + let state1 = set_reg state (name_of_reg r1) r1_v in + let state2 = set_reg state1 (name_of_reg r2) r2_v in + [(Left (), state2)]*) |