diff options
Diffstat (limited to 'src')
| -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 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 23 | ||||
| -rw-r--r-- | src/pretty_print.mli | 2 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 425 | ||||
| -rw-r--r-- | src/process_file.ml | 23 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
11 files changed, 1445 insertions, 1843 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 *) diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 0cdeb414..167e7de9 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -779,32 +779,35 @@ end (* the address_lifted types should go away here and be replaced by address *) type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event)) -type outcome 'a = +type outcome_r 'a 'r = (* Request to read memory, value is location to read, integer is size to read, followed by registers that were used in computing that size *) - | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a)) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r)) (* Tell the system a write is imminent, at address lifted, of size nat *) - | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a)) + | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r)) (* Request the result of store-exclusive *) - | Excl_res of (bool -> with_aux (outcome 'a)) + | Excl_res of (bool -> with_aux (outcome_r 'a 'r)) (* Request to write memory at last signalled address. Memory value should be 8 times the size given in ea signal *) - | Write_memv of memory_value * (bool -> with_aux (outcome 'a)) + | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r)) (* Request a memory barrier *) - | Barrier of barrier_kind * with_aux (outcome 'a) + | Barrier of barrier_kind * with_aux (outcome_r 'a 'r) (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of with_aux (outcome 'a) + | Footprint of with_aux (outcome_r 'a 'r) (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of reg_name * (register_value -> with_aux (outcome 'a)) + | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r)) (* Request to write register *) - | Write_reg of (reg_name * register_value) * with_aux (outcome 'a) + | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r) | Escape of maybe string (*Result of a failed assert with possible error message to report*) | Fail of maybe string - | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a) + (* Early return with value of type 'r *) + | Return of 'r + | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r) | Done of 'a | Error of string +type outcome 'a = outcome_r 'a unit type outcome_s 'a = with_aux (outcome 'a) (* first string : output of instruction_stack_to_string second string: output of local_variables_to_string *) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 37de5241..835d4648 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -52,4 +52,4 @@ val pat_to_string : 'a pat -> string val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit +val pp_defs_lem : bool -> bool -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 2971081e..7671c26b 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -148,44 +148,47 @@ let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with let doc_typ_lem, doc_atomic_typ_lem = (* following the structure of parser for precedence *) - let rec typ regtypes ty = fn_typ regtypes true ty - and typ' regtypes ty = fn_typ regtypes false ty - and fn_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with + let rec typ sequential mwords ty = fn_typ sequential mwords true ty + and typ' sequential mwords ty = fn_typ sequential mwords false ty + and fn_typ (sequential : bool) (mwords : bool) atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_fn(arg,ret,efct) -> (*let exc_typ = string "string" in*) let ret_typ = if effectful efct - then separate space [string "M";(*parens exc_typ;*) fn_typ regtypes true ret] - else separate space [fn_typ regtypes false ret] in - let tpp = separate space [tup_typ regtypes true arg; arrow;ret_typ] in + then separate space [string "M";(*parens exc_typ;*) fn_typ sequential mwords true ret] + else separate space [fn_typ sequential mwords false ret] in + let tpp = separate space [tup_typ sequential mwords true arg; arrow;ret_typ] in (* once we have proper excetions we need to know what the exceptions type is *) if atyp_needed then parens tpp else tpp - | _ -> tup_typ regtypes atyp_needed ty - and tup_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with + | _ -> tup_typ sequential mwords atyp_needed ty + and tup_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_tup typs -> - let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in + let tpp = separate_map (space ^^ star ^^ space) (app_typ sequential mwords false) typs in if atyp_needed then parens tpp else tpp - | _ -> app_typ regtypes atyp_needed ty - and app_typ regtypes atyp_needed ((Typ_aux (t, l)) as ty) = match t with + | _ -> app_typ sequential mwords atyp_needed ty + and app_typ sequential mwords atyp_needed ((Typ_aux (t, l)) as ty) = match t with | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_nexp m, _); Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with - | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> + | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when mwords -> string "bitvector " ^^ doc_nexp_lem (simplify_nexp m) (* (match simplify_nexp m with | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m] | _ -> raise (Reporting_basic.err_unreachable l "cannot pretty-print bitvector type with non-constant length")) *) - | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in + | _ -> string "vector" ^^ space ^^ typ sequential mwords elem_typ in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> (* TODO: Better distinguish register names and contents? *) (* fn_typ regtypes atyp_needed etyp *) - let tpp = (string "register_ref regstate " ^^ typ regtypes etyp) in + let tpp = + if sequential + then string "register_ref regstate " ^^ typ sequential mwords etyp + else string "register" in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") @@ -194,10 +197,10 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (string "integer") | Typ_app(id,args) -> - let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in + let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem sequential mwords) args) in if atyp_needed then parens tpp else tpp - | _ -> atomic_typ regtypes atyp_needed ty - and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with + | _ -> atomic_typ sequential mwords atyp_needed ty + and atomic_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_id (Id_aux (Id "bool",_)) -> string "bool" | Typ_id (Id_aux (Id "boolean",_)) -> string "bool" | Typ_id (Id_aux (Id "bit",_)) -> string "bitU" @@ -210,10 +213,10 @@ let doc_typ_lem, doc_atomic_typ_lem = | Typ_app _ | Typ_tup _ | Typ_fn _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) - let tpp = typ regtypes ty in + let tpp = typ sequential mwords ty in if atyp_needed then parens tpp else tpp - and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with - | Typ_arg_typ t -> app_typ regtypes true t + and doc_typ_arg_lem sequential mwords (Typ_arg_aux(t,_)) = match t with + | Typ_arg_typ t -> app_typ sequential mwords true t | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n) | Typ_arg_order o -> empty in typ', atomic_typ @@ -240,17 +243,17 @@ and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with | Typ_arg_nexp nexp -> not (is_nexp_constant (simplify_nexp nexp)) | _ -> false -let doc_tannot_lem regtypes eff typ = +let doc_tannot_lem sequential mwords eff typ = (* if contains_t_pp_var typ then empty else *) - let ta = doc_typ_lem regtypes typ in + let ta = doc_typ_lem sequential mwords typ in if eff then string " : _M " ^^ parens ta else string " : " ^^ ta (* doc_lit_lem gets as an additional parameter the type information from the * expression around it: that's a hack, but how else can we distinguish between * undefined values of different types ? *) -let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a = +let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a = match lit with | L_unit -> utf8string "()" | L_zero -> utf8string "B0" @@ -275,7 +278,7 @@ let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a = | _ -> parens ((utf8string "(failwith \"undefined value of unsupported type\")") ^^ - (doc_tannot_lem regtypes false typ))) + (doc_tannot_lem sequential mwords false typ))) | _ -> utf8string "(failwith \"undefined value of unsupported type\")") | L_string s -> utf8string ("\"" ^ s ^ "\"") | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *) @@ -295,9 +298,9 @@ let doc_typquant_lem (TypQ_aux(tq,_)) typ = match tq with string "forall " ^^ separate_map space doc_quant_item qs ^^ string ". " ^^ typ | _ -> empty -let doc_typschm_lem regtypes quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = - if quants then (doc_typquant_lem tq (doc_typ_lem regtypes t)) - else doc_typ_lem regtypes t +let doc_typschm_lem sequential mwords quants (TypSchm_aux(TypSchm_ts(tq,t),_)) = + if quants then (doc_typquant_lem tq (doc_typ_lem sequential mwords t)) + else doc_typ_lem sequential mwords t let is_ctor env id = match Env.lookup_id id env with | Enum _ | Union _ -> true @@ -306,37 +309,37 @@ let is_ctor env id = match Env.lookup_id id env with (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) -let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with +let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = match p with | P_app(id, ((_ :: _) as pats)) -> let ppp = doc_unop (doc_id_lem_ctor id) - (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in + (parens (separate_map comma (doc_pat_lem sequential mwords true) pats)) in if apat_needed then parens ppp else ppp | P_app(id,[]) -> doc_id_lem_ctor id - | P_lit lit -> doc_lit_lem regtypes true lit annot + | P_lit lit -> doc_lit_lem sequential mwords true lit annot | P_wild -> underscore | P_id id -> begin match id with | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *) | _ -> doc_id_lem id end - | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id]) + | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id]) | P_typ(typ,p) -> - let doc_p = doc_pat_lem regtypes true p in + let doc_p = doc_pat_lem sequential mwords true p in if contains_t_pp_var typ then doc_p - else parens (doc_op colon doc_p (doc_typ_lem regtypes typ)) + else parens (doc_op colon doc_p (doc_typ_lem sequential mwords typ)) | P_vector pats -> let ppp = (separate space) - [string "Vector";brackets (separate_map semi (doc_pat_lem regtypes true) pats);underscore;underscore] in + [string "Vector";brackets (separate_map semi (doc_pat_lem sequential mwords true) pats);underscore;underscore] in if apat_needed then parens ppp else ppp | P_vector_concat pats -> raise (Reporting_basic.err_unreachable l "vector concatenation patterns should have been removed before pretty-printing") | P_tup pats -> (match pats with - | [p] -> doc_pat_lem regtypes apat_needed p - | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats)) - | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*) - | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem regtypes true p) (doc_pat_lem regtypes true p') + | [p] -> doc_pat_lem sequential mwords apat_needed p + | _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats)) + | P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*) + | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p') | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *) let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with @@ -363,11 +366,11 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = - let rec top_exp regtypes (early_ret : bool) (aexp_needed : bool) + let rec top_exp sequential mwords (early_ret : bool) (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) = - let expY = top_exp regtypes early_ret true in - let expN = top_exp regtypes early_ret false in - let expV = top_exp regtypes early_ret in + let expY = top_exp sequential mwords early_ret true in + let expN = top_exp sequential mwords early_ret false in + let expV = top_exp sequential mwords early_ret in let liftR doc = if early_ret && effectful (effect_of full_exp) then separate space [string "liftR"; parens (doc)] @@ -389,12 +392,12 @@ let doc_exp_lem, doc_let_lem = doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field_range") - (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^ + (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^ field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e))) | _ -> liftR ((prefix 2 1) (string "write_reg_range") - (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e))) + (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e))) ) | LEXP_vector (le,e2) when is_bit_typ t -> (match le with @@ -408,16 +411,16 @@ let doc_exp_lem, doc_let_lem = doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field_bit") - (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e))) + (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e))) | _ -> liftR ((prefix 2 1) (string "write_reg_bit") - (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e)) + (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e)) ) (* | LEXP_field (le,id) when is_bit_typ t -> liftR ((prefix 2 1) (string "write_reg_bitfield") - (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *) + (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *) | LEXP_field ((LEXP_aux (_, lannot) as le),id) -> let field_ref = doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^ @@ -425,7 +428,7 @@ let doc_exp_lem, doc_let_lem = doc_id_lem id in liftR ((prefix 2 1) (string "write_reg_field") - (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ + (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e)) (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info -> (match alias_info with @@ -441,15 +444,15 @@ let doc_exp_lem, doc_let_lem = string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ expY e) *) | _ -> - liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes early_ret le ^/^ expY e))) + liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem sequential mwords early_ret le ^/^ expY e))) | E_vector_append(le,re) -> raise (Reporting_basic.err_unreachable l - "E_vector_access should have been rewritten before pretty-printing") + "E_vector_append should have been rewritten before pretty-printing") (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let (call,ta,aexp_needed) = if is_bitvector_typ t then if not (contains_t_pp_var t) - then ("bitvector_concat", doc_tannot_lem regtypes false t, true) + then ("bitvector_concat", doc_tannot_lem sequential mwords false t, true) else ("bitvector_concat", empty, aexp_needed) else ("vector_concat",empty,aexp_needed) in let epp = @@ -467,7 +470,7 @@ let doc_exp_lem, doc_let_lem = | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> raise (report l "E_for should have been removed till now") | E_let(leb,e) -> - let epp = let_exp regtypes early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in + let epp = let_exp sequential mwords early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in if aexp_needed then parens epp else epp | E_app(f,args) -> begin match f with @@ -506,7 +509,7 @@ let doc_exp_lem, doc_let_lem = let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let eff = effect_of full_exp in if contains_bitvector_typ t && not (contains_t_pp_var t) - then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true) + then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true) else (epp, aexp_needed) in if aexp_needed then parens (align taepp) else taepp | Id_aux (Id "length",_) -> @@ -544,7 +547,7 @@ let doc_exp_lem, doc_let_lem = let eff = effect_of full_exp in if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t) && not (contains_t_pp_var t) - then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true) + then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true) else (epp, aexp_needed) in liftR (if aexp_needed then parens (align taepp) else taepp) end @@ -563,20 +566,20 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else epp*) | E_vector_subrange (v,e1,e2) -> raise (Reporting_basic.err_unreachable l - "E_vector_access should have been rewritten before pretty-printing") + "E_vector_subrange should have been rewritten before pretty-printing") (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let eff = effect_of full_exp in let (epp,aexp_needed) = if has_effect eff BE_rreg then let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in if contains_bitvector_typ t && not (contains_t_pp_var t) - then (epp ^^ doc_tannot_lem regtypes true t, true) + then (epp ^^ doc_tannot_lem sequential mwords true t, true) else (epp, aexp_needed) else if is_bitvector_typ t then let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in if not (contains_t_pp_var t) - then (bepp ^^ doc_tannot_lem regtypes false t, true) + then (bepp ^^ doc_tannot_lem sequential mwords false t, true) else (bepp, aexp_needed) else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in if aexp_needed then parens (align epp) else epp *) @@ -591,7 +594,7 @@ let doc_exp_lem, doc_let_lem = let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in let (ta,aexp_needed) = if contains_bitvector_typ t && not (contains_t_pp_var t) - then (doc_tannot_lem regtypes (effectful eff) t, true) + then (doc_tannot_lem sequential mwords (effectful eff) t, true) else (empty, aexp_needed) in let epp = field_f ^^ space ^^ (expY fexp) in if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta) @@ -614,7 +617,7 @@ let doc_exp_lem, doc_let_lem = if has_effect eff BE_rreg then let epp = separate space [string "read_reg";doc_id_lem id] in if is_bitvector_typ base_typ && not (contains_t_pp_var base_typ) - then liftR (parens (epp ^^ doc_tannot_lem regtypes true base_typ)) + then liftR (parens (epp ^^ doc_tannot_lem sequential mwords true base_typ)) else liftR epp else if is_ctor env id then doc_id_lem_ctor id else doc_id_lem id @@ -626,7 +629,7 @@ let doc_exp_lem, doc_let_lem = | _ -> "read_reg_field" in let ta = if contains_bitvector_typ t && not (contains_t_pp_var t) - then doc_tannot_lem regtypes true t else empty in + then doc_tannot_lem sequential mwords true t else empty in let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in if aexp_needed then parens (align epp) else epp | Alias_pair(reg1,reg2) -> @@ -634,7 +637,7 @@ let doc_exp_lem, doc_let_lem = if has_effect eff BE_rreg then let ta = if contains_bitvector_typ t && not (contains_t_pp_var t) - then doc_tannot_lem regtypes true t else empty in + then doc_tannot_lem sequential mwords true t else empty in ("read_two_regs", ta) else ("RegisterPair", empty) in @@ -647,11 +650,11 @@ let doc_exp_lem, doc_let_lem = else let ta = if contains_bitvector_typ t && not (contains_t_pp_var t) - then doc_tannot_lem regtypes true t else empty in + then doc_tannot_lem sequential mwords true t else empty in separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in if aexp_needed then parens (align epp) else epp )*) - | E_lit lit -> doc_lit_lem regtypes false lit annot + | E_lit lit -> doc_lit_lem sequential mwords false lit annot | E_cast(typ,e) -> expV aexp_needed e (* (match annot with @@ -659,7 +662,7 @@ let doc_exp_lem, doc_let_lem = (* TODO: Does this case still exist with the new type checker? *) let epp = string "read_reg" ^^ space ^^ expY e in if contains_bitvector_typ t && not (contains_t_pp_var t) - then parens (epp ^^ doc_tannot_lem regtypes true t) else epp + then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp | Base((_,t),_,_,_,_,_) -> (match typ with | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> @@ -692,7 +695,7 @@ let doc_exp_lem, doc_let_lem = | _ -> raise (report l "cannot get record type") in let epp = anglebars (space ^^ (align (separate_map (semi_sp ^^ break 1) - (doc_fexp regtypes early_ret recordtyp) fexps)) ^^ space) in + (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in if aexp_needed then parens epp else epp | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> let (E_aux (_, (_, eannot))) = e in @@ -700,7 +703,7 @@ let doc_exp_lem, doc_let_lem = | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env -> tid | _ -> raise (report l "cannot get record type") in - anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes early_ret recordtyp) fexps)) + anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps)) | E_vector exps -> let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let (start, len, order, etyp) = @@ -731,11 +734,11 @@ let doc_exp_lem, doc_let_lem = let epp = group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in let (epp,aexp_needed) = - if is_bit_typ etyp then + if is_bit_typ etyp && mwords then let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in if contains_t_pp_var t then (bepp, aexp_needed) - else (bepp ^^ doc_tannot_lem regtypes false t, true) + else (bepp ^^ doc_tannot_lem sequential mwords false t, true) else (epp,aexp_needed) in if aexp_needed then parens (align epp) else epp (* *) @@ -792,18 +795,24 @@ let doc_exp_lem, doc_let_lem = align (group (call ^//^ brackets expspp ^/^ separate space [default_string;string start;string size;string dir_out])) in let (bepp, aexp_needed) = - if is_bitvector_typ t - then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem regtypes false t, true) + if is_bitvector_typ t && mwords + then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem sequential mwords false t, true) else (epp, aexp_needed) in if aexp_needed then parens (align bepp) else bepp | E_vector_update(v,e1,e2) -> let t = typ_of full_exp in - let call = if is_bitvector_typ t then "bvupdate_pos" else "update_pos" in + let call = + if is_bitvector_typ t (*&& mwords*) + then "bitvector_update_pos" + else "update_pos" in let epp = separate space [string call;expY v;expY e1;expY e2] in if aexp_needed then parens (align epp) else epp | E_vector_update_subrange(v,e1,e2,e3) -> let t = typ_of full_exp in - let call = if is_bitvector_typ t then "bvupdate" else "update" in + let call = + if is_bitvector_typ t (*&& mwords*) + then "bitvector_update" + else "update" in let epp = align (string call ^//^ group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^ group (expY e3)) in @@ -829,7 +838,7 @@ let doc_exp_lem, doc_let_lem = pattern-matching on integers *) let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ - (separate_map (break 1) (doc_case regtypes early_ret) pexps) ^/^ + (separate_map (break 1) (doc_case sequential mwords early_ret) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_exit e -> liftR (separate space [string "exit"; expY e;]) @@ -919,7 +928,7 @@ let doc_exp_lem, doc_let_lem = string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in let (epp,aexp_needed) = if contains_bitvector_typ t && not (contains_t_pp_var t) - then (parens epp ^^ doc_tannot_lem regtypes false t, true) + then (parens epp ^^ doc_tannot_lem sequential mwords false t, true) else (epp, aexp_needed) in if aexp_needed then parens (align epp) else epp | _ -> @@ -944,13 +953,13 @@ let doc_exp_lem, doc_let_lem = (separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2 | _ -> (separate space [expV b e1; string ">>= fun"; - doc_pat_lem regtypes true pat;arrow]) ^^ hardline ^^ expN e2 in + doc_pat_lem sequential mwords true pat;arrow]) ^^ hardline ^^ expN e2 in if aexp_needed then parens (align epp) else epp | E_internal_return (e1) -> separate space [string "return"; expY e1;] | E_sizeof nexp -> (match simplify_nexp nexp with - | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem regtypes false (L_aux (L_num i, l)) annot + | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem sequential mwords false (L_aux (L_num i, l)) annot | _ -> raise (Reporting_basic.err_unreachable l "pretty-printing non-constant sizeof expressions to Lem not supported")) @@ -960,34 +969,34 @@ let doc_exp_lem, doc_let_lem = | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable l "unsupported internal expression encountered while pretty-printing") - and let_exp regtypes early_ret (LB_aux(lb,_)) = match lb with + and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with | LB_val_explicit(_,pat,e) | LB_val_implicit(pat,e) -> prefix 2 1 - (separate space [string "let"; doc_pat_lem regtypes true pat; equals]) - (top_exp regtypes early_ret false e) + (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals]) + (top_exp sequential mwords early_ret false e) - and doc_fexp regtypes early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) = + and doc_fexp sequential mwords early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) = let fname = if prefix_recordtype then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id else doc_id_lem id in - group (doc_op equals fname (top_exp regtypes early_ret true e)) + group (doc_op equals fname (top_exp sequential mwords early_ret true e)) - and doc_case regtypes early_ret = function + and doc_case sequential mwords early_ret = function | Pat_aux(Pat_exp(pat,e),_) -> - group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow]) - (group (top_exp regtypes early_ret false e))) + group (prefix 3 1 (separate space [pipe; doc_pat_lem sequential mwords false pat;arrow]) + (group (top_exp sequential mwords early_ret false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting_basic.err_unreachable l "guarded pattern expression should have been rewritten before pretty-printing") - and doc_lexp_deref_lem regtypes early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with + and doc_lexp_deref_lem sequential mwords early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with | LEXP_field (le,id) -> - parens (separate empty [doc_lexp_deref_lem regtypes early_ret le;dot;doc_id_lem id]) + parens (separate empty [doc_lexp_deref_lem sequential mwords early_ret le;dot;doc_id_lem id]) | LEXP_vector(le,e) -> - parens ((separate space) [string "access";doc_lexp_deref_lem regtypes early_ret le; - top_exp regtypes early_ret true e]) + parens ((separate space) [string "access";doc_lexp_deref_lem sequential mwords early_ret le; + top_exp sequential mwords early_ret true e]) | LEXP_id id -> doc_id_lem id | LEXP_cast (typ,id) -> doc_id_lem id | _ -> @@ -996,9 +1005,9 @@ let doc_exp_lem, doc_let_lem = in top_exp, let_exp (*TODO Upcase and downcase type and constructors as needed*) -let doc_type_union_lem regtypes (Tu_aux(typ_u,_)) = match typ_u with +let doc_type_union_lem sequential mwords (Tu_aux(typ_u,_)) = match typ_u with | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of"; - parens (doc_typ_lem regtypes typ)] + parens (doc_typ_lem sequential mwords typ)] | Tu_id id -> separate space [pipe; doc_id_lem_ctor id] let rec doc_range_lem (BF_aux(r,_)) = match r with @@ -1006,16 +1015,16 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2)) | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) -let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with +let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with | TD_abbrev(id,nm,typschm) -> doc_op equals (concat [string "type"; space; doc_id_lem_type id]) - (doc_typschm_lem regtypes false typschm) + (doc_typschm_lem sequential mwords false typschm) | TD_record(id,nm,typq,fs,_) -> let fname fid = if prefix_recordtype then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] else doc_id_lem_type fid in let f_pp (typ,fid) = - concat [fname fid;space;colon;space;doc_typ_lem regtypes typ; semi] in + concat [fname fid;space;colon;space;doc_typ_lem sequential mwords typ; semi] in let rectyp = match typq with | TypQ_aux (TypQ_tq qs, _) -> let quant_item = function @@ -1032,7 +1041,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (Typ_arg_typ rectyp); mk_typ_arg (Typ_arg_typ ftyp)])) in - let rfannot = doc_tannot_lem regtypes false reftyp in + let rfannot = doc_tannot_lem sequential mwords false reftyp in let get, set = string "rec_val" ^^ dot ^^ fname fid, anglebars (space ^^ string "rec_val with " ^^ @@ -1040,12 +1049,14 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with doc_op equals (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) (anglebars (concat [space; + doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp; doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp; doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in doc_op equals (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq]) ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^ - separate_map hardline doc_field fs + if sequential && string_of_id id = "regstate" then empty + else separate_map hardline doc_field fs | TD_variant(id,nm,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty @@ -1058,7 +1069,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with | Id_aux ((Id "diafp"),_) -> empty | Id_aux ((Id "option"),_) -> empty | _ -> - let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in + let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in let typ_pp = (doc_op equals) @@ -1230,20 +1241,16 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with | TD_register(id,n1,n2,rs) -> match n1, n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> - let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); - doc_range_lem r;]) in - let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in - (*let doc_rfield (_,id) = - (doc_op equals) - (string "let" ^^ space ^^ doc_id_lem id) - (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*) let dir_b = i1 < i2 in let dir = string (if dir_b then "true" else "false") in let dir_suffix = (if dir_b then "_inc" else "_dec") in let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in - let tannot = doc_tannot_lem regtypes false vtyp in + let tannot = doc_tannot_lem sequential mwords false vtyp in + let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); + doc_range_lem r;]) in + let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in let doc_field (fr, fid) = let i, j = match fr with | BF_aux (BF_single i, _) -> (i, i) @@ -1255,32 +1262,21 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown), [mk_typ_arg (Typ_arg_typ (mk_id_typ id)); mk_typ_arg (Typ_arg_typ ftyp)])) in - let rfannot = doc_tannot_lem regtypes false reftyp in + let rfannot = doc_tannot_lem sequential mwords false reftyp in let get, set = "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")", "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in doc_op equals (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])]) (concat [ - space; langlebar; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline; + space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline; + space; space; space; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline; space; space; space; string (" set_field = (fun reg v -> " ^ set ^ ") "); ranglebar]) - (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^ - string (" get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^ - string (" set_field = (fun reg v -> " ^ set ^") |>") *) - (* doc_op equals - (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid; - space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *) in doc_op equals (concat [string "type";space;doc_id_lem id]) - (doc_typ_lem regtypes vtyp) + (doc_typ_lem sequential mwords vtyp) ^^ hardline ^^ - (* doc_op equals - (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) - (string "Register" ^^ space ^^ - align (separate space [string "regname"; doc_int size; doc_int i1; dir; - break 0 ^^ brackets (align doc_rids)])) - ^^ hardline ^^ *) doc_op equals (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"]) (string "reg") @@ -1289,25 +1285,54 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"]) (string "reg") ^^ hardline ^^ - separate_map hardline doc_field rs + (* if sequential then *) + (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^ + string (" get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^ + string (" set_field = (fun reg v -> " ^ set ^") |>") *) + (* doc_op equals + (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid; + space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *) + (* in *) + (* doc_op equals + (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) + (string "Register" ^^ space ^^ + align (separate space [string "regname"; doc_int size; doc_int i1; dir; + break 0 ^^ brackets (align doc_rids)])) + ^^ hardline ^^ *) + separate_map hardline doc_field rs + ^^ hardline ^^ + (* else *) + (*let doc_rfield (_,id) = + (doc_op equals) + (string "let" ^^ space ^^ doc_id_lem id) + (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*) + doc_op equals + (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) + (string "Register" ^^ space ^^ + align (separate space [string "regname"; doc_int size; doc_int i1; dir; + break 0 ^^ brackets (align doc_rids)])) + (*^^ hardline ^^ + separate_map hardline doc_field rs*) + | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices") + let doc_rec_lem (Rec_aux(r,_)) = match r with | Rec_nonrec -> space | Rec_rec -> space ^^ string "rec" ^^ space -let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with - | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem regtypes typ) +let doc_tannot_opt_lem sequential mwords (Typ_annot_opt_aux(t,_)) = match t with + | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem sequential mwords typ) -let doc_fun_body_lem regtypes exp = +let doc_fun_body_lem sequential mwords exp = let early_ret = contains_early_return exp in - let doc_exp = doc_exp_lem regtypes early_ret false exp in + let doc_exp = doc_exp_lem sequential mwords early_ret false exp in if early_ret then align (string "catch_early_return" ^//^ parens (doc_exp)) else doc_exp -let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow) - (doc_fun_body_lem regtypes exp)) +let doc_funcl_lem sequential mwords (FCL_aux(FCL_Funcl(id,pat,exp),_)) = + group (prefix 3 1 ((doc_pat_lem sequential mwords false pat) ^^ space ^^ arrow) + (doc_fun_body_lem sequential mwords exp)) let get_id = function | [] -> failwith "FD_function with empty list" @@ -1315,20 +1340,21 @@ let get_id = function module StringSet = Set.Make(String) -let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = +let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = match fcls with | [] -> failwith "FD_function with empty function list" - | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> + | [FCL_aux (FCL_Funcl(id,pat,exp),_)] + when not (Env.is_extern id (env_of exp)) -> (prefix 2 1) ((separate space) [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id); - (doc_pat_lem regtypes true pat); + (doc_pat_lem sequential mwords true pat); equals]) - (doc_fun_body_lem regtypes exp) - | _ -> - let id = get_id fcls in + (doc_fun_body_lem sequential mwords exp) + | FCL_aux (FCL_Funcl(id,_,exp),_) :: _ + when not (Env.is_extern id (env_of exp)) -> (* let sep = hardline ^^ pipe ^^ space in *) - match id with + (match id with | Id_aux (Id fname,idl) when fname = "execute" || fname = "initial_analysis" -> let (_,auxiliary_functions,clauses) = @@ -1354,7 +1380,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) P_aux (P_tup argspat,pannot),exp),annot) in let auxiliary_functions = auxiliary_functions ^^ hardline ^^ hardline ^^ - doc_fundef_lem regtypes (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in + doc_fundef_lem sequential mwords (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in (* Bind complex patterns to names so that we can pass them to the auxiliary function *) let name_pat idx (P_aux (p,a)) = match p with @@ -1366,13 +1392,13 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in let doc_arg idx (P_aux (p,(l,a))) = match p with | P_as (pat,id) -> doc_id_lem id - | P_lit lit -> doc_lit_lem regtypes false lit a + | P_lit lit -> doc_lit_lem sequential mwords false lit a | P_id id -> doc_id_lem id | _ -> string ("arg" ^ string_of_int idx) in let clauses = clauses ^^ (break 1) ^^ (separate space - [pipe;doc_pat_lem regtypes false named_pat;arrow; + [pipe;doc_pat_lem sequential mwords false named_pat;arrow; string aux_fname; parens (separate comma (List.mapi doc_arg named_argspat))]) in (already_used_fnames,auxiliary_functions,clauses) @@ -1385,73 +1411,75 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) | _ -> let clauses = (separate_map (break 1)) - (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in + (fun fcl -> separate space [pipe;doc_funcl_lem sequential mwords fcl]) fcls in (prefix 2 1) ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"]) - (clauses ^/^ string "end") - + (clauses ^/^ string "end")) + | _ -> empty -let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = + +let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) = match reg with | DEC_reg(typ,id) -> - empty - (* let env = env_of_annot annot in - (match typ with - | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env -> - separate space [string "let";doc_id_lem id;equals; - string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline - | _ -> - let rt = Env.base_typ_of env typ in - if is_vector_typ rt then - let (start, size, order, etyp) = vector_typ_args_of rt in - if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then - let o = if is_order_inc order then "true" else "false" in - (doc_op equals) - (string "let" ^^ space ^^ doc_id_lem id) - (string "Register" ^^ space ^^ - align (separate space [string_lit(doc_id_lem id); - doc_nexp (size); - doc_nexp (start); - string o; - string "[]"])) - ^/^ hardline + if sequential then empty + else + let env = env_of_annot annot in + (match typ with + | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env -> + separate space [string "let";doc_id_lem id;equals; + string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline + | _ -> + let rt = Env.base_typ_of env typ in + if is_vector_typ rt then + let (start, size, order, etyp) = vector_typ_args_of rt in + if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then + let o = if is_order_inc order then "true" else "false" in + (doc_op equals) + (string "let" ^^ space ^^ doc_id_lem id) + (string "Register" ^^ space ^^ + align (separate space [string_lit(doc_id_lem id); + doc_nexp (size); + doc_nexp (start); + string o; + string "[]"])) + ^/^ hardline + else raise (Reporting_basic.err_unreachable l + ("can't deal with register type " ^ string_of_typ typ)) else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ)) - else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ))) *) + ("can't deal with register type " ^ string_of_typ typ))) | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty -let doc_spec_lem regtypes (VS_aux (valspec,annot)) = +let doc_spec_lem mwords (VS_aux (valspec,annot)) = match valspec with | VS_extern_no_rename _ | VS_extern_spec _ -> empty (* ignore these at the moment *) | VS_val_spec (typschm,id) | VS_cast_spec (typschm,id) -> empty -(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *) +(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem mwords typschm] ^/^ hardline *) -let rec doc_def_lem regtypes def = match def with - | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty) +let rec doc_def_lem sequential mwords def = match def with + | DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty) | DEF_overload _ -> (empty,empty) - | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty) - | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty) + | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty) + | DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty) | DEF_default df -> (empty,empty) - | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline) - | DEF_val lbind -> (empty,group (doc_let_lem regtypes false lbind) ^/^ hardline) + | DEF_fundef f_def -> (empty,group (doc_fundef_lem sequential mwords f_def) ^/^ hardline) + | DEF_val lbind -> (empty,group (doc_let_lem sequential mwords false lbind) ^/^ hardline) | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" | DEF_kind _ -> (empty,empty) | DEF_comm (DC_comm s) -> (empty,comment (string s)) | DEF_comm (DC_comm_struct d) -> - let (typdefs,vdefs) = doc_def_lem regtypes d in + let (typdefs,vdefs) = doc_def_lem sequential mwords d in (empty,comment (typdefs ^^ hardline ^^ vdefs)) -let doc_defs_lem regtypes (Defs defs) = - let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in +let doc_defs_lem sequential mwords (Defs defs) = + let (typdefs,valdefs) = List.split (List.map (doc_def_lem sequential mwords) defs) in (separate empty typdefs,separate empty valdefs) let find_regtypes (Defs defs) = @@ -1470,7 +1498,7 @@ let find_registers (Defs defs) = | _ -> acc ) [] defs -let doc_regstate_lem regtypes registers = +let doc_regstate_lem mwords registers = let l = Parse_ast.Unknown in let annot = (l, None) in let regstate = match registers with @@ -1487,25 +1515,26 @@ let doc_regstate_lem regtypes registers = registers, false) in concat [ - doc_typdef_lem regtypes (TD_aux (regstate, annot)); hardline; + doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline; hardline; string "type _M 'a = M regstate 'a" ] -let doc_register_refs_lem regtypes registers = +let doc_register_refs_lem registers = let doc_register_ref (typ, id) = let idd = doc_id_lem id in let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in concat [string "let "; idd; string " = <|"; hardline; + string " reg_name = \""; idd; string "\";"; hardline; string " read_from = (fun s -> s."; field; string ");"; hardline; string " write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in separate_map hardline doc_register_ref registers -let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = - let regtypes = find_regtypes d in - let (typdefs,valdefs) = doc_defs_lem regtypes d in - let regstate_def = doc_regstate_lem regtypes (find_registers d) in - let register_refs = doc_register_refs_lem regtypes (find_registers d) in +let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_modules) d top_line = + (* let regtypes = find_regtypes d in *) + let (typdefs,valdefs) = doc_defs_lem sequential mwords d in + let regstate_def = doc_regstate_lem mwords (find_registers d) in + let register_refs = doc_register_refs_lem (find_registers d) in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; @@ -1523,8 +1552,16 @@ let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (p string "module SIA = Interp_ast"; hardline; hardline] else empty; - typdefs]); - (print types_seq_file) + typdefs; hardline; + hardline; + if sequential then + concat [regstate_def; hardline; + hardline; + register_refs] + else + concat [string "type _M 'a = M 'a"; hardline] + ]); + (* (print types_seq_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) @@ -1541,24 +1578,22 @@ let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (p string "module SIA = Interp_ast"; hardline; hardline] else empty; - typdefs; - hardline; + typdefs_seq; hardline; hardline; - regstate_def; + regstate_def; hardline; hardline; - hardline; - register_refs]); - (print prompt_file) + register_refs]); *) + (print defs_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline; + (fun lib -> separate space [string "open import";string lib]) defs_modules;hardline; hardline; valdefs]); - (print state_file) + (* (print state_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) state_modules;hardline; hardline; - valdefs]); + valdefs_seq]); *) diff --git a/src/process_file.ml b/src/process_file.ml index 6a3fc24c..46b6538e 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -134,10 +134,11 @@ let close_output_with_check (o, temp_file_name, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem filename libs libs_seq defs = +let output_lem filename libs defs = let generated_line = generated_line filename in let types_module = (filename ^ "_embed_types") in - let types_module_sequential = (filename ^ "_embed_types_sequential") in + let types_module_seq = (filename ^ "_embed_types_sequential") in + let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted (filename ^ "_embed_types.lem") in let ((ots,_, _) as ext_ots) = @@ -146,13 +147,15 @@ let output_lem filename libs libs_seq defs = open_output_with_check_unformatted (filename ^ "_embed.lem") in let ((os,_, _) as ext_os) = open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in - (Pretty_print.pp_defs_lem - (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"]) - (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"]) - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"; + (Pretty_print.pp_defs_lem false false + (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"]) + (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"; String.capitalize types_module] @ libs) - (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"; - String.capitalize types_module_sequential] @ libs_seq) + defs generated_line); + (Pretty_print.pp_defs_lem true true + (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"]) + (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"; + String.capitalize types_module_seq] @ libs_seq) defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_ots; @@ -205,9 +208,9 @@ let output1 libpath out_arg filename defs = close_output_with_check ext_o end | Lem_out None -> - output_lem f' [] [] defs + output_lem f' [] defs | Lem_out (Some lib) -> - output_lem f' [lib] [lib ^ "_sequential"] defs + output_lem f' [lib] defs | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; diff --git a/src/type_check.ml b/src/type_check.ml index 9e7a1ab3..fcabbb1c 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2566,7 +2566,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let else_branch' = crule check_exp (add_constraints (List.map nc_negate constrs) (add_flows false flows env)) else_branch (typ_of then_branch') in annot_exp (E_if (cond', then_branch', else_branch')) (typ_of then_branch') | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ()))) - | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "vector_append", [v1; v2]), (l, ()))) + | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ()))) | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ()))) | E_vector [] -> typ_error l "Cannot infer type of empty vector" | E_vector ((item :: items) as vec) -> |