diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 69 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 531 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 571 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 611 | ||||
| -rw-r--r-- | src/gen_lib/sail_values_word.lem | 1030 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 1 |
6 files changed, 1187 insertions, 1626 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 0944f42b..5c539354 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,19 +22,57 @@ 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 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 : bool -> read_kind -> vector bitU -> integer -> M (vector bitU) let read_mem dir rk addr sz = let addr = address_lifted_of_bitv addr in @@ -73,9 +114,9 @@ let read_reg_bit reg i = read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun 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 -> + read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v -> return (extract_only_element v) let reg_deref = read_reg @@ -93,12 +134,12 @@ let write_reg_bit reg i bit = let iN = natFromInteger i in write_reg_aux (external_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg)) let write_reg_field reg regfield v = - write_reg_aux (external_reg_field_whole reg regfield) v + write_reg_aux (external_reg_field_whole reg regfield.field_name) v let write_reg_bitfield reg regfield bit = - write_reg_aux (external_reg_field_whole reg regfield) + 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 @@ -110,8 +151,8 @@ 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 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 then @@ -120,8 +161,8 @@ let rec foreachM_inc (i,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 then diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem new file mode 100644 index 00000000..3919d540 --- /dev/null +++ b/src/gen_lib/sail_operators.lem @@ -0,0 +1,531 @@ +open import Pervasives_extra +open import Machine_word +open import Sail_impl_base +open import Sail_values + +(*** Bit vector operations *) + +let bvlength = 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 (v, i, j) = + let v' = slice v i j in + get_elems v' + +let bitvector_access_inc = vector_access_inc +let bitvector_access_dec = vector_access_dec +let bitvector_update_pos_dec = update_pos +let bitvector_update_dec = vector_update_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 (start, len, b) = Vector (repeat [b] len) start false + +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 + +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 + ~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 = 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 (start, len, n) = set_vector_start (start, to_vec true (len, n)) +let to_vec_norm_inc (len, n) = to_vec true (len, n) +let to_vec_dec (start, len, n) = set_vector_start (start, to_vec false (len, n)) +let to_vec_norm_dec (len, n) = to_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_vec (get_dir vec) (len,signed vec)) +let extz (start, len, vec) = set_vector_start (start, to_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 add (l,r) = integerAdd l r +let add_signed (l,r) = integerAdd l r +let sub (l,r) = integerMinus l r +let mult (l,r) = integerMult l r +let quotient (l,r) = integerDiv l r +let modulo (l,r) = hardware_mod l r +let quot = hardware_quot +let power (l,r) = integerPow l r + +let sub_int = sub +let mult_int = mult + +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 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_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_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 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_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) + +(* Assumes decreasing bit vectors *) +let duplicate (bit, length) = + Vector (repeat [bit] length) (length - 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_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 diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem new file mode 100644 index 00000000..87d805f6 --- /dev/null +++ b/src/gen_lib/sail_operators_mwords.lem @@ -0,0 +1,571 @@ +open import Pervasives_extra +open import Machine_word +open import Sail_impl_base +open import Sail_values + +(*** Bit vector operations *) + +let bvlength (Bitvector 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 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 + +let bitvector_subrange_inc (v, i, j) = bvslice v i j +let bitvector_subrange_dec (v, i, j) = bvslice v i j + +let vector_subrange_bl (v, i, j) = + let v' = slice (bvec_to_vec 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 (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 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a +let bvupdate v i j (Bitvector bs' _ _) = + bvupdate_aux v i j bs' + +val bvaccess : forall 'a. bitvector 'a -> integer -> bitU +let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU ( + 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 -> bitU -> bitvector 'a +let bvupdate_pos v n b = + bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1) + +let bitvector_access_inc (v, i) = bvaccess v i +let bitvector_access_dec (v, i) = bvaccess v i +let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b +let bitvector_update_dec (v, i, j, v') = bvupdate v i j v' + +val extract_only_bit : bitvector ty1 -> bitU +let extract_only_bit (Bitvector 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 = reset_bitvector_start +let adjust_start_index (start, v) = set_bitvector_start (start, v) + +let cast_vec_bool v = bitU_to_bool (extract_only_bit v) +let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false) + +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 + bool_to_bitU (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)) + +val to_vec_ord : forall 'a. Size 'a => bool -> (integer * integer) -> bitvector 'a +let to_vec_ord is_inc ((len : integer), (n : integer)) = + (* 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_vec_ord + +let to_vec_inc (start, len, n) = set_bitvector_start (start, to_vec_ord true (len, n)) +let to_vec_norm_inc (len, n) = to_vec_ord true (len, n) +let to_vec_dec (start, len, n) = set_bitvector_start (start, to_vec_ord false (len, n)) +let to_vec_norm_dec (len, n) = to_vec_ord false (len, 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) = set_bitvector_start (start, to_vec_ord (bvget_dir vec) (len, signed vec)) +val extz : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b +let extz (start, len, vec) = set_bitvector_start (start, to_vec_ord (bvget_dir vec) (len, unsigned vec)) + +let exts_big (start, len, vec) = set_bitvector_start (start, to_vec_big (bvget_dir vec) (len, signed_big vec)) +let extz_big (start, len, vec) = set_bitvector_start (start, to_vec_big (bvget_dir vec) (len, unsigned_big vec)) + +(* TODO *) +let extz_bl (start, len, bits) = set_bitvector_start (start, vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)) +let exts_bl (start, len, bits) = set_bitvector_start (start, vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)) + +let add (l,r) = integerAdd l r +let add_signed (l,r) = integerAdd l r +let sub (l,r) = integerMinus l r +let mult (l,r) = integerMult l r +let quotient (l,r) = integerDiv l r +let modulo (l,r) = hardware_mod l r +let quot = hardware_quot +let power (l,r) = integerPow l r + +let sub_int = sub +let mult_int = mult + +(* 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) (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_ord is_inc (size, 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 (Bitvector _ _ is_inc as l) r = + arith_op_vec op sign size l ((to_vec_ord is_inc (size, 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 (Bitvector _ _ is_inc as r) = + arith_op_vec op sign size ((to_vec_ord is_inc (size, 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 = 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_ord is_inc (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 + +(* 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 (Bitvector bs start is_inc,(n : integer)) = + let n = natFromInteger n in + match op with + | LL_shift (*"<<"*) -> + Bitvector (shiftLeft bs n) start is_inc + | RR_shift (*">>"*) -> + Bitvector (shiftRight bs n) start is_inc + | LLL_shift (*"<<<"*) -> + Bitvector (rotateLeft 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 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) + +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. bitvector 'a * bitvector '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_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, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index eb5cdef5..eeec7440 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -17,6 +17,13 @@ let bool_xor (l, r) = xor l r let list_append (l, r) = l ++ r +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 -> @@ -137,17 +144,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 @@ -173,6 +180,9 @@ let slice (Vector bs start is_inc) i j = sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in Vector subvector_bits i is_inc +let vector_subrange_inc (v, i, j) = slice v i j +let vector_subrange_dec (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 easy, but the start index has to be transformed to match the old vector start @@ -200,6 +210,9 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector ' let update v i j (Vector bs' _ _) = update_aux v i j bs' +let vector_update_inc (v, i, j, v') = update v i j v' +let vector_update_dec (v, i, j, v') = update v i j v' + 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)) @@ -212,6 +225,12 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a let update_pos v n b = update_aux v n n [b] +let extract_only_element (Vector elems _ _) = match elems with + | [] -> failwith "extract_only_element called for empty vector" + | [e] -> e + | _ -> failwith "extract_only_element called for vector with more elements" +end + (*** Bitvectors *) (* element list * start * has increasing direction *) @@ -224,7 +243,6 @@ let showBitvector (Bitvector elems start 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 (bitvector 'a)) let show = showBitvector @@ -240,581 +258,8 @@ let vec_to_bvec (Vector elems start is_inc) = (*** 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 norm_dec = reset_bitvector_start -let adjust_dec = reset_bitvector_start - -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 - -let bitvector_subrange_inc (v, i, j) = bvslice v i j -let bitvector_subrange_dec (v, i, j) = bvslice v i j - -let vector_subrange_bl (v, i, j) = - let v' = slice (bvec_to_vec 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 (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 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a -let bvupdate v i j (Bitvector bs' _ _) = - bvupdate_aux v i j bs' - -val bvaccess : forall 'a. bitvector 'a -> integer -> bitU -let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU ( - 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 -> bitU -> bitvector 'a -let bvupdate_pos v n b = - bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1) - -let bitvector_access_inc (v, i) = bvaccess v i -let bitvector_access_dec (v, i) = bvaccess v i -let bitvector_update_pos_dec (v, i, b) = bvupdate_pos v i b -let bitvector_update_dec (v, i, j, v') = bvupdate v i j v' - -(*** Bit vector operations *) - -let extract_only_element (Vector elems _ _) = match elems with - | [] -> failwith "extract_only_element called for empty vector" - | [e] -> e - | _ -> failwith "extract_only_element called for vector with more elements" -end - -val extract_only_bit : bitvector ty1 -> bitU -let extract_only_bit (Bitvector 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 cast_vec_bool v = bitU_to_bool (extract_only_bit v) -let cast_bit_vec b = vec_to_bvec (Vector [b] 0 false) - -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 - bool_to_bitU (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 - 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" -end - -let add_one_bit_ignore_overflow bits = - List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) - -let to_vec is_inc ((n : integer)) = - (* 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_vec - -let to_vec_inc = to_vec true -let to_vec_dec = to_vec false - -let cast_0_vec = to_vec_dec -let cast_1_vec = to_vec_dec -let cast_01_vec = to_vec_dec - -(* 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 (vec) = to_vec (bvget_dir vec) (signed vec) -let extz (vec) = to_vec (bvget_dir vec) (unsigned vec) - -let exts_big (vec) = to_vec_big (bvget_dir vec) (signed_big vec) -let extz_big (vec) = to_vec_big (bvget_dir vec) (unsigned_big vec) - -let extz_bl (bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) - -let add (l,r) = integerAdd l r -let add_signed (l,r) = integerAdd l r -let sub (l,r) = integerMinus l r -let multiply (l,r) = integerMult l r -let quotient (l,r) = integerDiv l r -let modulo (l,r) = hardware_mod l r -let quot = hardware_quot -let power (l,r) = integerPow l r - -let sub_int = sub -let mul_int = multiply - -(* 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) (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 (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 mul_vec (l, r) = mult_VVV l r -let mul_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 (Bitvector _ _ is_inc as l) r = - arith_op_vec op sign size l ((to_vec is_inc (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 (Bitvector _ _ is_inc as r) = - arith_op_vec op sign size ((to_vec is_inc (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 = 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 (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 - -(* 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 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 '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 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 n) start is_inc - | RR_shift (*">>"*) -> - Bitvector (shiftRight bs n) start is_inc - | LLL_shift (*"<<<"*) -> - Bitvector (rotateLeft 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 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 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) = - vec_to_bvec (Vector (repeat [bit] length) (length - 1) false) - -let duplicate_to_list (bit, length) = repeat [bit] length - -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. bitvector 'a * bitvector '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_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) *) - -(* TODO *) -val mask : forall 'a 'b. Size 'b => bitvector 'a -> bitvector 'b -let mask (Bitvector w i dir) = (Bitvector (zeroExtend w) i dir) +(* Bytes and addresses *) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) let rec byte_chunks n list = match (n,list) with @@ -885,11 +330,13 @@ type register = | RegisterPair of register * register type register_ref 'regstate 'a = - <| read_from : 'regstate -> 'a; + <| reg_name : string; + read_from : 'regstate -> 'a; write_to : 'regstate -> 'a -> 'regstate |> type field_ref 'regtype 'a = - <| get_field : 'regtype -> 'a; + <| field_name : string; + get_field : 'regtype -> 'a; set_field : 'regtype -> 'a -> 'regtype |> let name_of_reg = function 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 3cbcd4c8..4543bbcf 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,6 +1,7 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values +open import Sail_operators_mwords (* 'a is result type *) |