diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 3 | ||||
| -rw-r--r-- | src/gen_lib/prompt.lem | 6 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 556 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 459 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 22 | ||||
| -rw-r--r-- | src/initial_check.mli | 1 | ||||
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 6 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 85 | ||||
| -rw-r--r-- | src/process_file.ml | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 61 | ||||
| -rw-r--r-- | src/type_check.ml | 22 |
11 files changed, 506 insertions, 717 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index f1add52b..5756c954 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -864,9 +864,8 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = match typ_aux with | Typ_id id -> wrap (E_app (prepend_id "undefined_" id, [wrap (E_lit (mk_lit L_unit)) unit_typ])) typ - | Typ_app (_,[start;size;_;_]) when mwords && is_bitvector_typ typ -> + | Typ_app (_,[size;_;_]) when mwords && is_bitvector_typ typ -> wrap (E_app (mk_id "undefined_bitvector", - undefined_of_typ_args mwords l annot start @ undefined_of_typ_args mwords l annot size)) typ | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp i, _)]) when string_of_id atom = "atom" -> wrap (E_sizeof i) typ diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 744b6f7f..5019c2f7 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -86,12 +86,12 @@ let try_catchR m h = end) -val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'b 'e -let read_mem dir rk addr sz = +val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e +let read_mem rk addr sz = let addr = address_lifted_of_bitv (bits_of addr) in let sz = natFromInteger sz in let k memory_value = - let bitv = of_bits (internal_mem_value dir memory_value) in + let bitv = of_bits (internal_mem_value memory_value) in (Done bitv,Nothing) in Read_mem (rk,addr,sz) k diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 83746c0b..230ab84e 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -5,81 +5,27 @@ open import Sail_values (*** Bit vector operations *) -let bitvector_length = length +val concat_vec : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c +let concat_vec l r = of_bits (bits_of l ++ bits_of r) -let set_bitvector_start = set_vector_start -let reset_bitvector_start = reset_vector_start +val cons_vec : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b +let cons_vec b v = of_bits (b :: bits_of v) -let set_bitvector_start_to_length = set_vector_start_to_length +let bool_of_vec v = extract_only_element (bits_of v) +let vec_of_bit len b = of_bits (extz_bits len [b]) +let cast_unit_vec b = of_bits [b] -let bitvector_concat = vector_concat -let inline (^^^) = bitvector_concat - -let bitvector_subrange_inc = vector_subrange_inc -let bitvector_subrange_dec = vector_subrange_dec - -let vector_subrange_bl (start, v, i, j) = - let v' = slice v i j in - get_elems v' -let vector_subrange_bl_dec = vector_subrange_bl - -let bitvector_access_inc = vector_access_inc -let bitvector_access_dec = vector_access_dec -let bitvector_update_pos_inc = vector_update_pos_inc -let bitvector_update_pos_dec = vector_update_pos_dec -let bitvector_update_subrange_inc = vector_update_subrange_inc -let bitvector_update_subrange_dec = vector_update_subrange_dec - -let extract_only_bit = extract_only_element - -let norm_dec = reset_vector_start -let adjust_start_index (start, v) = set_vector_start (start, v) - -let cast_vec_bool v = bitU_to_bool (extract_only_element v) -let cast_bit_vec_basic (start, len, b) = Vector (repeat [b] len) start false -let cast_boolvec_bitvec (Vector bs start inc) = - Vector (List.map bool_to_bitU bs) start inc -let cast_vec_bl (Vector bs start inc) = bs -let cast_bl_vec (start, len, bs) = Vector (extz_bl (len, bs)) start false -let cast_bl_svec (start, len, bs) = Vector (bits_of_int (len, bitlist_to_signed bs)) start false -let cast_int_vec n = of_bits (int_to_bin n) - -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 +let most_significant v = match bits_of v with + | b :: _ -> b | _ -> failwith "most_significant applied to empty vector" end -let bitwise_not (Vector bs start is_inc) = - Vector (bitwise_not_bitlist bs) start is_inc - -let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) = - let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in - Vector (reverse revbs) start is_inc - -let bitwise_and = bitwise_binop (&&) -let bitwise_or = bitwise_binop (||) -let bitwise_xor = bitwise_binop xor - -let unsigned_big = unsigned - -let signed v : integer = - match most_significant v with - | B1 -> 0 - (1 + (unsigned (bitwise_not v))) - | B0 -> unsigned v - | BU -> failwith "signed applied to vector with undefined bits" - end - let hardware_mod (a: integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) mod (abs b) - else if (a < 0 && b >= 0) - then (a mod b) - b - else a mod b + 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 @@ -92,12 +38,8 @@ let hardware_quot (a:integer) (b:integer) : integer = 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 int_of_vec sign = if sign then signed else unsigned +let vec_of_int len n = of_bits (bits_of_int len n) let max_64u = (integerPow 2 64) - 1 let max_64 = (integerPow 2 63) - 1 @@ -126,225 +68,155 @@ let get_min_representable_in _ (n : integer) : integer = else if n = 5 then min_5 else 0 - (integerPow 2 (natFromInteger n)) -let to_norm_vec is_inc ((len : integer),(n : integer)) = - let start = if is_inc then 0 else len - 1 in - Vector (bits_of_int (len, n)) start is_inc - -let to_vec_big = to_norm_vec +val bitwise_binop_vec : forall 'a. Bitvector 'a => + (bool -> bool -> bool) -> 'a -> 'a -> 'a +let bitwise_binop_vec op l r = of_bits (binop_bits op (bits_of l) (bits_of r)) -let to_vec_inc (start, len, n) = set_vector_start (start, to_norm_vec true (len, n)) -let to_vec_norm_inc (len, n) = to_norm_vec true (len, n) -let to_vec_dec (start, len, n) = set_vector_start (start, to_norm_vec false (len, n)) -let to_vec_norm_dec (len, n) = to_norm_vec false (len, n) +let and_vec = bitwise_binop_vec (&&) +let or_vec = bitwise_binop_vec (||) +let xor_vec = bitwise_binop_vec xor +let not_vec v = of_bits (not_bits (bits_of v)) -let cast_0_vec = to_vec_dec -let cast_1_vec = to_vec_dec -let cast_01_vec = to_vec_dec - -let to_vec_undef is_inc (len : integer) = - Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc - -let to_vec_inc_undef = to_vec_undef true -let to_vec_dec_undef = to_vec_undef false - -let exts (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,signed vec)) -let extz (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,unsigned vec)) - -let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec)) -let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec)) - - -let quot = hardware_quot -let modulo (l,r) = hardware_mod l r - -let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = - let (l',r') = (to_num sign l, to_num sign r) in +val arith_op_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b +let arith_op_vec op sign size l r = + let (l',r') = (int_of_vec sign l, int_of_vec sign r) in let n = op l' r' in - to_norm_vec is_inc (size * (length l),n) - - -(* add_vec - * add_vec_signed - * minus_vec - * multiply_vec - * multiply_vec_signed - *) -let add_VVV = arith_op_vec integerAdd false 1 -let addS_VVV = arith_op_vec integerAdd true 1 -let minus_VVV = arith_op_vec integerMinus false 1 -let mult_VVV = arith_op_vec integerMult false 2 -let multS_VVV = arith_op_vec integerMult true 2 - -let mult_vec (l, r) = mult_VVV l r -let mult_svec (l, r) = multS_VVV l r - -let add_vec (l, r) = add_VVV l r -let sub_vec (l, r) = minus_VVV l r - -let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r = - arith_op_vec op sign size l (to_norm_vec is_inc (length l,r)) - -(* add_vec_range - * add_vec_range_signed - * minus_vec_range - * mult_vec_range - * mult_vec_range_signed - *) -let add_VIV = arith_op_vec_range integerAdd false 1 -let addS_VIV = arith_op_vec_range integerAdd true 1 -let minus_VIV = arith_op_vec_range integerMinus false 1 -let mult_VIV = arith_op_vec_range integerMult false 2 -let multS_VIV = arith_op_vec_range integerMult true 2 - -let add_vec_int (l, r) = add_VIV l r -let sub_vec_int (l, r) = minus_VIV l r - -let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) = - arith_op_vec op sign size (to_norm_vec is_inc (length r, l)) r - -(* add_range_vec - * add_range_vec_signed - * minus_range_vec - * mult_range_vec - * mult_range_vec_signed - *) -let add_IVV = arith_op_range_vec integerAdd false 1 -let addS_IVV = arith_op_range_vec integerAdd true 1 -let minus_IVV = arith_op_range_vec integerMinus false 1 -let mult_IVV = arith_op_range_vec integerMult false 2 -let multS_IVV = arith_op_range_vec integerMult true 2 - -let arith_op_range_vec_range op sign l r = op l (to_num sign r) - -(* add_range_vec_range - * add_range_vec_range_signed - * minus_range_vec_range - *) -let add_IVI = arith_op_range_vec_range integerAdd false -let addS_IVI = arith_op_range_vec_range integerAdd true -let minus_IVI = arith_op_range_vec_range integerMinus false - -let arith_op_vec_range_range op sign l r = op (to_num sign l) r - -(* add_vec_range_range - * add_vec_range_range_signed - * minus_vec_range_range - *) -let add_VII = arith_op_vec_range_range integerAdd false -let addS_VII = arith_op_vec_range_range integerAdd true -let minus_VII = arith_op_vec_range_range integerMinus false - - - -let arith_op_vec_vec_range op sign l r = - let (l',r') = (to_num sign l,to_num sign r) in - op l' r' - -(* add_vec_vec_range - * add_vec_vec_range_signed - *) -let add_VVI = arith_op_vec_vec_range integerAdd false -let addS_VVI = arith_op_vec_vec_range integerAdd true - -let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r = - let l' = to_num sign l in + of_bits (bits_of_int (size * length l) n) + + +let add_vec = arith_op_vec integerAdd false 1 +let addS_vec = arith_op_vec integerAdd true 1 +let sub_vec = arith_op_vec integerMinus false 1 +let mult_vec = arith_op_vec integerMult false 2 +let multS_vec = arith_op_vec integerMult true 2 + +let inline add_mword = Machine_word.plus +let inline sub_mword = Machine_word.minus +val mult_mword : forall 'a 'b. Size 'b => mword 'a -> mword 'a -> mword 'b +let mult_mword l r = times (zeroExtend l) (zeroExtend r) + +val arith_op_vec_int : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> 'a -> integer -> 'b +let arith_op_vec_int op sign size l r = + let l' = int_of_vec sign l in + let n = op l' r in + of_bits (bits_of_int (size * length l) n) + +let add_vec_int = arith_op_vec_int integerAdd false 1 +let addS_vec_int = arith_op_vec_int integerAdd true 1 +let sub_vec_int = arith_op_vec_int integerMinus false 1 +let mult_vec_int = arith_op_vec_int integerMult false 2 +let multS_vec_int = arith_op_vec_int integerMult true 2 + +val arith_op_int_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b +let arith_op_int_vec op sign size l r = + let r' = int_of_vec sign r in + let n = op l r' in + of_bits (bits_of_int (size * length r) n) + +let add_int_vec = arith_op_int_vec integerAdd false 1 +let addS_int_vec = arith_op_int_vec integerAdd true 1 +let sub_int_vec = arith_op_int_vec integerMinus false 1 +let mult_int_vec = arith_op_int_vec integerMult false 2 +let multS_int_vec = arith_op_int_vec integerMult true 2 + +let arith_op_vec_bit op sign (size : integer) l r = + let l' = int_of_vec sign l in let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - to_norm_vec is_inc (length l * size,n) + of_bits (bits_of_int (size * length l) 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 add_vec_bit = arith_op_vec_bit integerAdd false 1 +let addS_vec_bit = arith_op_vec_bit integerAdd true 1 +let sub_vec_bit = 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 = +val arith_op_overflow_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU) +let arith_op_overflow_vec op sign size 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 (l_sign,r_sign) = (int_of_vec sign l,int_of_vec sign r) in + let (l_unsign,r_unsign) = (int_of_vec false l,int_of_vec false r) in let n = op l_sign r_sign in let n_unsign = op l_unsign r_unsign in - let correct_size_num = to_norm_vec is_inc (act_size,n) in - let one_more_size_u = to_norm_vec is_inc (act_size + 1,n_unsign) in + let correct_size = bits_of_int act_size n in + let one_more_size_u = bits_of_int (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 = + (of_bits correct_size,overflow,c_out) + +let add_overflow_vec = arith_op_overflow_vec integerAdd false 1 +let add_overflow_vec_signed = arith_op_overflow_vec integerAdd true 1 +let sub_overflow_vec = arith_op_overflow_vec integerMinus false 1 +let sub_overflow_vec_signed = arith_op_overflow_vec integerMinus true 1 +let mult_overflow_vec = arith_op_overflow_vec integerMult false 2 +let mult_overflow_vec_signed = arith_op_overflow_vec integerMult true 2 + +val arith_op_overflow_vec_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU) +let arith_op_overflow_vec_bit op sign size 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 l' = int_of_vec sign l in + let l_u = int_of_vec false l in let (n,nu,changed) = match r_bit with | B1 -> (op l' 1, op l_u 1, true) | B0 -> (l',l_u,false) | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" end in -(* | _ -> assert false *) - let correct_size_num = to_norm_vec is_inc (act_size,n) in - let one_larger = to_norm_vec is_inc (act_size + 1,nu) in + let correct_size = bits_of_int act_size n in + let one_larger = bits_of_int (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) + (of_bits correct_size,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 +let add_overflow_vec_bit = arith_op_overflow_vec_bit integerAdd false 1 +let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerAdd true 1 +let sub_overflow_vec_bit = arith_op_overflow_vec_bit integerMinus false 1 +let sub_overflow_vec_bit_signed = arith_op_overflow_vec_bit integerMinus true 1 -type shift = LL_shift | RR_shift | LLL_shift +type shift = LL_shift | RR_shift | LL_rot | RR_rot -let shift_op_vec op (Vector bs start is_inc,(n : integer)) = - let n = natFromInteger n in +val shift_op_vec : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a +let shift_op_vec op v n = 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 + | LL_shift -> + of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n) + | RR_shift -> + of_bits (repeat [B0] n ++ get_bits true v 0 (length v - n - 1)) + | LL_rot -> + of_bits (get_bits true v n (length v - 1) ++ get_bits true v 0 (n - 1)) + | RR_rot -> + of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1)) 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 = shift_op_vec LL_shift (*"<<"*) +let shiftr = shift_op_vec RR_shift (*">>"*) +let rotl = shift_op_vec LL_rot (*"<<<"*) +let rotr = shift_op_vec LL_rot (*">>>"*) -let shiftl = bitwise_leftshift +let shiftl_mword w n = Machine_word.shiftLeft w (natFromInteger n) +let shiftr_mword w n = Machine_word.shiftRight w (natFromInteger n) +let rotl_mword w n = Machine_word.rotateLeft (natFromInteger n) w +let rotr_mword w n = Machine_word.rotateRight (natFromInteger n) w 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 = +val arith_op_vec_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b +let arith_op_vec_no0 op sign size l r = let act_size = length l * size in - let (l',r') = (to_num sign l,to_num sign r) in + let (l',r') = (int_of_vec sign l,int_of_vec sign r) in let n = arith_op_no0 op l' r' in let (representable,n') = match n with @@ -353,19 +225,23 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector n' >= get_min_representable_in sign act_size, n') | _ -> (false,0) end in - if representable - then to_norm_vec is_inc (act_size,n') - else Vector (List.replicate (natFromInteger act_size) BU) start is_inc + of_bits (if representable then bits_of_int act_size n' else repeat [BU] act_size) -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 mod_vec = arith_op_vec_no0 hardware_mod false 1 +let quot_vec = arith_op_vec_no0 hardware_quot false 1 +let quot_vec_signed = 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 mod_mword = Machine_word.modulo +let quot_mword = Machine_word.unsignedDivide +let quot_mword_signed = Machine_word.signedDivide + +val arith_op_overflow_vec_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU) +let arith_op_overflow_vec_no0 op sign size 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 (l',r') = (int_of_vec sign l,int_of_vec sign r) in + let (l_u,r_u) = (int_of_vec false l,int_of_vec 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') = @@ -375,120 +251,54 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = n' >= (get_min_representable_in sign rep_size)), n', n_u') | _ -> (true,0,0) end in - let (correct_size_num,one_more) = + let (correct_size,one_more) = if representable then - (to_norm_vec is_inc (act_size,n'),to_norm_vec is_inc (act_size + 1,n_u')) + (bits_of_int act_size n', bits_of_int (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 + (repeat [BU] act_size, repeat [BU] (act_size + 1)) in let overflow = if representable then B0 else B1 in - (correct_size_num,overflow,most_significant one_more) + (of_bits correct_size,overflow,most_significant one_more) + +let quot_overflow_vec = arith_op_overflow_vec_no0 hardware_quot false 1 +let quot_overflow_vec_signed = arith_op_overflow_vec_no0 hardware_quot true 1 + +let arith_op_vec_int_no0 op sign size l r = + arith_op_vec_no0 op sign size l (of_bits (bits_of_int (length l) r)) + +let quot_vec_int = arith_op_vec_int_no0 hardware_quot false 1 +let mod_vec_int = arith_op_vec_int_no0 hardware_mod false 1 + +let replicate_bits v count = of_bits (repeat v count) +let duplicate bit len = replicate_bits [bit] len + +let lt = (<) +let gt = (>) +let lteq = (<=) +let gteq = (>=) + +val eq : forall 'a. Eq 'a => 'a -> 'a -> bool +let eq l r = (l = r) + +val eq_vec : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let eq_vec l r = (unsigned l = unsigned r) + +val neq : forall 'a. Eq 'a => 'a -> 'a -> bool +let neq l r = (l <> r) + +val neq_vec : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let neq_vec l r = (unsigned l <> unsigned r) + +val ucmp_vec : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool +let ucmp_vec cmp l r = cmp (unsigned l) (unsigned r) -let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 -let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 +val scmp_vec : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool +let scmp_vec cmp l r = cmp (signed l) (signed r) -let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = - arith_op_vec_no0 op sign size l (to_norm_vec is_inc (length l,r)) - -let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 - -(* Assumes decreasing bit vectors *) -let duplicate (bit, length) = - Vector (repeat [bit] length) (length - 1) false - -let replicate_bits (v, count) = - Vector (repeat (get_elems v) count) ((length v * count) - 1) false - -let compare_op op (l,r) = (op l r) - -let lt = compare_op (<) -let gt = compare_op (>) -let lteq = compare_op (<=) -let gteq = compare_op (>=) - -let compare_op_vec op sign (l,r) = - let (l',r') = (to_num sign l, to_num sign r) in - compare_op op (l',r') - -let lt_vec = compare_op_vec (<) true -let gt_vec = compare_op_vec (>) true -let lteq_vec = compare_op_vec (<=) true -let gteq_vec = compare_op_vec (>=) true - -let lt_vec_signed = compare_op_vec (<) true -let gt_vec_signed = compare_op_vec (>) true -let lteq_vec_signed = compare_op_vec (<=) true -let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false -let gt_vec_unsigned = compare_op_vec (>) false -let lteq_vec_unsigned = compare_op_vec (<=) false -let gteq_vec_unsigned = compare_op_vec (>=) false - -let lt_svec = lt_vec_signed - -let compare_op_vec_range op sign (l,r) = - compare_op op ((to_num sign l),r) - -let lt_vec_range = compare_op_vec_range (<) true -let gt_vec_range = compare_op_vec_range (>) true -let lteq_vec_range = compare_op_vec_range (<=) true -let gteq_vec_range = compare_op_vec_range (>=) true - -let compare_op_range_vec op sign (l,r) = - compare_op op (l, (to_num sign r)) - -let lt_range_vec = compare_op_range_vec (<) true -let gt_range_vec = compare_op_range_vec (>) true -let lteq_range_vec = compare_op_range_vec (<=) true -let gteq_range_vec = compare_op_range_vec (>=) true - -val eq : forall 'a. Eq 'a => 'a * 'a -> bool -let eq (l,r) = (l = r) -let eq_range (l,r) = (l = r) - -val eq_vec : forall 'a. vector 'a * vector 'a -> bool -let eq_vec (l,r) = (l = r) -let eq_bit (l,r) = (l = r) -let eq_vec_range (l,r) = eq (to_num false l,r) -let eq_range_vec (l,r) = eq (l, to_num false r) -let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) - -let neq (l,r) = not (eq (l,r)) -let neq_bit (l,r) = not (eq_bit (l,r)) -let neq_range (l,r) = not (eq_range (l,r)) -let neq_vec (l,r) = not (eq_vec (l,r)) -let neq_vec_vec (l,r) = not (eq_vec_vec (l,r)) -let neq_vec_range (l,r) = not (eq_vec_range (l,r)) -let neq_range_vec (l,r) = not (eq_range_vec (l,r)) - - -val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a -let make_indexed_vector entries default start length dir = - let length = natFromInteger length in - Vector (List.foldl replace (replicate length default) entries) start dir - -(* -val make_bit_vector_undef : integer -> vector bitU -let make_bitvector_undef length = - Vector (replicate (natFromInteger length) BU) 0 true - *) - -(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) - -let mask (start, n, Vector bits _ dir) = - let current_size = List.length bits in - Vector (drop (current_size - (natFromInteger n)) bits) start dir - - -(* Register operations *) - -(*let update_reg_range i j reg_val new_val = update reg_val i j new_val -let update_reg_pos i reg_val bit = update_pos reg_val i bit -let update_reg_field_range regfield i j reg_val new_val = - let current_field_value = regfield.get_field reg_val in - let new_field_value = update current_field_value i j new_val in - regfield.set_field reg_val new_field_value -(*let write_reg_field_pos regfield i reg_val bit = - let current_field_value = regfield.get_field reg_val in - let new_field_value = update_pos current_field_value i bit in - regfield.set_field reg_val new_field_value*)*) +let ult_vec = ucmp_vec (<) +let slt_vec = scmp_vec (<) +let ugt_vec = ucmp_vec (>) +let sgt_vec = scmp_vec (>) +let ulteq_vec = ucmp_vec (<=) +let slteq_vec = scmp_vec (<=) +let ugteq_vec = ucmp_vec (>=) +let sgteq_vec = scmp_vec (>=) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 231b9c8e..8aee556d 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -13,47 +13,47 @@ let pow m n = m ** (natFromInteger n) let pow2 n = pow 2 n -let add_int (l,r) = integerAdd l r -let add_signed (l,r) = integerAdd l r -let sub_int (l,r) = integerMinus l r -let mult_int (l,r) = integerMult l r -let quotient_int (l,r) = integerDiv l r -let quotient_nat (l,r) = natDiv l r -let power_int_nat (l,r) = integerPow l r -let power_int_int (l, r) = integerPow l (natFromInteger r) +(*let add_int l r = integerAdd l r +let add_signed l r = integerAdd l r +let sub_int l r = integerMinus l r +let mult_int l r = integerMult l r +let div_int l r = integerDiv l r +let div_nat l r = natDiv l r +let power_int_nat l r = integerPow l r +let power_int_int l r = integerPow l (natFromInteger r) let negate_int i = integerNegate i -let min_int (l, r) = integerMin l r -let max_int (l, r) = integerMax l r +let min_int l r = integerMin l r +let max_int l r = integerMax l r -let add_real (l, r) = realAdd l r -let sub_real (l, r) = realMinus l r -let mult_real (l, r) = realMult l r -let div_real (l, r) = realDiv l r +let add_real l r = realAdd l r +let sub_real l r = realMinus l r +let mult_real l r = realMult l r +let div_real l r = realDiv l r let negate_real r = realNegate r let abs_real r = realAbs r -let power_real (b, e) = realPowInteger b e +let power_real b e = realPowInteger b e*) -let or_bool (l, r) = (l || r) -let and_bool (l, r) = (l && r) -let xor_bool (l, r) = xor l r +let or_bool l r = (l || r) +let and_bool l r = (l && r) +let xor_bool l r = xor l r -let list_append (l, r) = l ++ r -let list_length xs = integerFromNat (List.length xs) -let list_take (n, xs) = List.take (natFromInteger n) xs -let list_drop (n, xs) = List.drop (natFromInteger n) xs +let append_list l r = l ++ r +let length_list xs = integerFromNat (List.length xs) +let take_list n xs = List.take (natFromInteger n) xs +let drop_list n xs = List.drop (natFromInteger n) xs val repeat : forall 'a. list 'a -> integer -> list 'a let rec repeat xs n = if n <= 0 then [] else xs ++ repeat xs (n-1) -let duplicate_to_list (bit, length) = repeat [bit] length +let duplicate_to_list bit length = repeat [bit] length -let rec replace bs ((n : integer),b') = match bs with +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') + else b :: replace bs (n - 1) b' end let upper n = n @@ -81,20 +81,20 @@ instance (BitU bitU) let of_bitU b = b end -let bitU_to_bool = function +let bool_of_bitU = function | B0 -> false | B1 -> true - | BU -> failwith "to_bool applied to BU" + | BU -> failwith "bool_of_bitU applied to BU" end -let bool_to_bitU b = if b then B1 else B0 +let bitU_of_bool b = if b then B1 else B0 instance (BitU bool) - let to_bitU = bool_to_bitU - let of_bitU = bitU_to_bool + let to_bitU = bitU_of_bool + let of_bitU = bool_of_bitU end -let cast_bit_bool = bitU_to_bool +let cast_bit_bool = bool_of_bitU let bit_lifted_of_bitU = function | B0 -> Bitl_zero @@ -120,93 +120,98 @@ let bitU_of_bit_lifted = function | Bitl_unknown -> failwith "bitU_of_bit_lifted Bitl_unknown" end -let bitwise_not_bit = function +let 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 bitwise_binop_bit op = function +let binop_bit op x y = match (x, y) with | (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)) + | (x,y) -> bitU_of_bool (op (bool_of_bitU x) (bool_of_bitU y)) end -val bitwise_and_bit : bitU * bitU -> bitU -let bitwise_and_bit = bitwise_binop_bit (&&) +val and_bit : bitU -> bitU -> bitU +let and_bit = binop_bit (&&) -val bitwise_or_bit : bitU * bitU -> bitU -let bitwise_or_bit = bitwise_binop_bit (||) +val or_bit : bitU -> bitU -> bitU +let or_bit = binop_bit (||) -val bitwise_xor_bit : bitU * bitU -> bitU -let bitwise_xor_bit = bitwise_binop_bit xor +val xor_bit : bitU -> bitU -> bitU +let xor_bit = binop_bit xor val (&.) : bitU -> bitU -> bitU -let inline (&.) x y = bitwise_and_bit (x,y) +let inline (&.) x y = and_bit x y val (|.) : bitU -> bitU -> bitU -let inline (|.) x y = bitwise_or_bit (x,y) +let inline (|.) x y = or_bit x y val (+.) : bitU -> bitU -> bitU -let inline (+.) x y = bitwise_xor_bit (x,y) +let inline (+.) x y = xor_bit x y (*** Bit lists ***) -val to_bin_aux : natural -> list bitU -let rec to_bin_aux x = +val bits_of_nat_aux : natural -> list bitU +let rec bits_of_nat_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) + else (if x mod 2 = 1 then B1 else B0) :: bits_of_nat_aux (x / 2) +let bits_of_nat n = List.reverse (bits_of_nat_aux n) -val of_bin : list bitU -> natural -let of_bin bits = +val nat_of_bits : list bitU -> natural +let nat_of_bits bits = let (sum,_) = List.foldr (fun b (acc,exp) -> match b with | B1 -> (acc + naturalPow 2 exp, exp + 1) | B0 -> (acc, exp + 1) - | BU -> failwith "of_bin: bitvector has undefined bits" + | BU -> failwith "nat_of_bits: bitvector has undefined bits" end) (0,0) bits in sum -let bitwise_not_bitlist = List.map bitwise_not_bit +let not_bits = List.map not_bit + +let binop_bits op bsl bsr = + foldr (fun (bl, br) acc -> binop_bit op bl br :: acc) [] (zip bsl bsr) -val bitlist_to_unsigned : list bitU -> integer -let bitlist_to_unsigned bs = integerFromNatural (of_bin bs) +let and_bits = binop_bits (&&) +let or_bits = binop_bits (||) +let xor_bits = binop_bits xor -val bitlist_to_signed : list bitU -> integer -let bitlist_to_signed bits = +val unsigned_of_bits : list bitU -> integer +let unsigned_of_bits bs = integerFromNatural (nat_of_bits bs) + +val signed_of_bits : list bitU -> integer +let signed_of_bits bits = match bits with - | B1 :: _ -> 0 - (1 + (bitlist_to_unsigned (bitwise_not_bitlist bits))) - | B0 :: _ -> bitlist_to_unsigned bits - | BU :: _ -> failwith "bitlist_to_signed applied to list with undefined bits" - | [] -> failwith "bitlist_to_signed applied to empty list" + | B1 :: _ -> 0 - (1 + (unsigned_of_bits (not_bits bits))) + | B0 :: _ -> unsigned_of_bits bits + | BU :: _ -> failwith "signed_of_bits applied to list with undefined bits" + | [] -> failwith "signed_of_bits applied to empty list" end val pad_bitlist : bitU -> list bitU -> integer -> list bitU let rec pad_bitlist b bits n = if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1) -let ext_bl pad (len, bits) = +let ext_bits pad len bits = let longer = len - (integerFromNat (List.length bits)) in if longer < 0 then drop (natFromInteger (abs (longer))) bits else pad_bitlist pad bits longer -let extz_bl (len, bits) = ext_bl B0 (len, bits) -let exts_bl (len, bits) = +let extz_bits len bits = ext_bits B0 len bits +let exts_bits len bits = match bits with - | BU :: _ -> failwith "exts_bl: undefined bit" - | B1 :: _ -> ext_bl B1 (len, bits) - | _ -> ext_bl B0 (len, bits) + | BU :: _ -> failwith "exts_bits: undefined bit" + | B1 :: _ -> ext_bits B1 len bits + | _ -> ext_bits B0 len bits end let rec add_one_bit_ignore_overflow_aux bits = match bits with @@ -219,15 +224,14 @@ end let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) -let int_to_bin n = - let bits_abs = B0 :: to_bin (naturalFromInteger (abs n)) in +let bitlist_of_int n = + let bits_abs = B0 :: bits_of_nat (naturalFromInteger (abs n)) in if n >= (0 : integer) then bits_abs - else add_one_bit_ignore_overflow (bitwise_not_bitlist bits_abs) + else add_one_bit_ignore_overflow (not_bits bits_abs) -let bits_of_nat ((len : integer),(n : natural)) = extz_bl (len, to_bin n) -let bits_of_int ((len : integer),(n : integer)) = exts_bl (len, int_to_bin n) +let bits_of_int len n = exts_bits len (bitlist_of_int n) -let nibble_of_bits = function +let char_of_nibble = function | (B0, B0, B0, B0) -> Just #'0' | (B0, B0, B0, B1) -> Just #'1' | (B0, B0, B1, B0) -> Just #'2' @@ -249,7 +253,7 @@ let nibble_of_bits = function let rec hexstring_of_bits bs = match bs with | b1 :: b2 :: b3 :: b4 :: bs -> - let n = nibble_of_bits (b1, b2, b3, b4) in + let n = char_of_nibble (b1, b2, b3, b4) in let s = hexstring_of_bits bs in match (n, s) with | (Just n, Just s) -> Just (n :: s) @@ -264,195 +268,179 @@ let show_bitlist bs = | Nothing -> show bs end -(*** Vectors *) +(*** List operations *) -(* element list * start * has increasing direction *) -type vector 'a = Vector of list 'a * integer * bool +let inline (^^) = append_list -let showVector (Vector elems start inc) = - "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc +val slice_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a +let slice_list_inc xs i j = + let (toJ,_suffix) = List.splitAt (natFromInteger j + 1) xs in + let (_prefix,fromItoJ) = List.splitAt (natFromInteger i) toJ in + fromItoJ -let get_dir (Vector _ _ ord) = ord -let get_start (Vector _ s _) = s -let get_elems (Vector elems _ _) = elems -let length (Vector bs _ _) = integerFromNat (length bs) -let vector_length = length +val slice_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a +let slice_list_dec xs i j = + let top = (length_list xs) - 1 in + slice_list_inc xs (top - i) (top - j) -instance forall 'a. Show 'a => (Show (vector 'a)) - let show = showVector -end +val slice_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a +let slice_list is_inc xs i j = if is_inc then slice_list_inc xs i j else slice_list_dec xs i j -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 +val update_slice_list_inc : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a +let update_slice_list_inc xs i j xs' = + let (toJ,suffix) = List.splitAt (natFromInteger j + 1) xs in + let (prefix,_fromItoJ) = List.splitAt (natFromInteger i) toJ in + prefix ++ xs' ++ suffix -(*** Vector operations *) +val update_slice_list_dec : forall 'a. list 'a -> integer -> integer -> list 'a -> list 'a +let update_slice_list_dec xs i j xs' = + let top = (length_list xs) - 1 in + update_slice_list_inc xs (top - i) (top - j) xs' -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 +val update_slice_list : forall 'a. bool -> list 'a -> integer -> integer -> list 'a -> list 'a +let update_slice_list is_inc xs i j xs' = + if is_inc then update_slice_list_inc xs i j xs' else update_slice_list_dec xs i j xs' -let reset_vector_start v = - set_vector_start (if (get_dir v) then 0 else (length v - 1), v) +val access_list_inc : forall 'a. list 'a -> integer -> 'a +let access_list_inc xs n = List_extra.nth xs (natFromInteger n) -let set_vector_start_to_length v = - set_vector_start (length v - 1, v) +val access_list_dec : forall 'a. list 'a -> integer -> 'a +let access_list_dec xs n = + let top = (length_list xs) - 1 in + access_list_inc xs (top - n) -let vector_concat (Vector bs start is_inc, Vector bs' _ _) = - Vector (bs ++ bs') start is_inc +val access_list : forall 'a. bool -> list 'a -> integer -> 'a +let access_list is_inc xs n = + if is_inc then access_list_inc xs n else access_list_dec xs n -let inline (^^) = vector_concat +val update_list_inc : forall 'a. list 'a -> integer -> 'a -> list 'a +let update_list_inc xs n x = List.update xs (natFromInteger n) x -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_list_dec : forall 'a. list 'a -> integer -> 'a -> list 'a +let update_list_dec xs n x = + let top = (length_list xs) - 1 in + update_list_inc xs (top - n) x -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 update_list : forall 'a. bool -> list 'a -> integer -> 'a -> list 'a +let update_list is_inc xs n x = + if is_inc then update_list_inc xs n x else update_list_dec xs n x -val slice_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a -let slice_aux is_inc start bs i j = - let iN = natFromInteger i in - let jN = natFromInteger j in - let startN = natFromInteger start in - sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) - -val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a -let slice (Vector bs start is_inc) i j = - Vector (slice_aux is_inc start bs i j) i is_inc - -let vector_subrange_inc (start, v, i, j) = slice v i j -let vector_subrange_dec (start, v, i, j) = slice v i j - -(* this is for the vector slicing introduced in vector-concat patterns: i and j -index into the "raw data", the list of bits. Therefore getting the bit list is -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. bool -> integer -> list 'a -> integer -> integer -> list 'a -> list 'a -let update_aux is_inc start bs i j bs' = - let iN = natFromInteger i in - let jN = natFromInteger j in - let startN = natFromInteger start in - update_sublist bs - (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' - -val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a -let update (Vector bs start is_inc) i j (Vector bs' _ _) = - Vector (update_aux is_inc start bs i j bs') start is_inc - -let vector_update_subrange_inc (start, v, i, j, v') = update v i j v' -let vector_update_subrange_dec (start, v, i, j, v') = update v i j v' - -val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a -let access_aux is_inc start xs n = - if is_inc then List_extra.nth xs (natFromInteger (n - start)) - else List_extra.nth xs (natFromInteger (start - n)) - -val access : forall 'a. vector 'a -> integer -> 'a -let access (Vector bs start is_inc) n = access_aux is_inc start bs n - -let vector_access_inc (start, v, i) = access v i -let vector_access_dec (start, v, i) = access v i - -val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a -let update_pos v n b = - update v n n (Vector [b] 0 false) - -let vector_update_pos_inc (start, v, i, x) = update_pos v i x -let vector_update_pos_dec (start, v, i, x) = update_pos v i x - -let extract_only_element (Vector elems _ _) = match elems with - | [] -> failwith "extract_only_element called for empty vector" +let extract_only_element = function + | [] -> failwith "extract_only_element called for empty list" | [e] -> e - | _ -> failwith "extract_only_element called for vector with more elements" + | _ -> failwith "extract_only_element called for list with more elements" end -(*** Bitvectors *) +(*** Machine words *) + +val length_mword : forall 'a. mword 'a -> integer +let length_mword w = integerFromNat (word_length w) + +val slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b +let slice_mword_dec w i j = word_extract (natFromInteger i) (natFromInteger j) w + +val slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b +let slice_mword_inc w i j = + let top = (length_mword w) - 1 in + slice_mword_dec w (top - i) (top - j) + +val slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b +let slice_mword is_inc w i j = if is_inc then slice_mword_inc w i j else slice_mword_dec w i j -(* element list * start * has increasing direction *) -type bitvector 'a = mword 'a (* Bitvector of mword 'a * integer * bool *) -declare isabelle target_sorts bitvector = `len` +val update_slice_mword_dec : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a +let update_slice_mword_dec w i j w' = word_update w (natFromInteger i) (natFromInteger j) w' + +val update_slice_mword_inc : forall 'a 'b. mword 'a -> integer -> integer -> mword 'b -> mword 'a +let update_slice_mword_inc w i j w' = + let top = (length_mword w) - 1 in + update_slice_mword_dec w (top - i) (top - j) w' + +val update_slice_mword : forall 'a 'b. bool -> mword 'a -> integer -> integer -> mword 'b -> mword 'a +let update_slice_mword is_inc w i j w' = + if is_inc then update_slice_mword_inc w i j w' else update_slice_mword_dec w i j w' + +val access_mword_dec : forall 'a. mword 'a -> integer -> bitU +let access_mword_dec w n = bitU_of_bool (getBit w (natFromInteger n)) + +val access_mword_inc : forall 'a. mword 'a -> integer -> bitU +let access_mword_inc w n = + let top = (length_mword w) - 1 in + access_mword_dec w (top - n) + +val access_mword : forall 'a. bool -> mword 'a -> integer -> bitU +let access_mword is_inc w n = + if is_inc then access_mword_inc w n else access_mword_dec w n + +val update_mword_dec : forall 'a. mword 'a -> integer -> bitU -> mword 'a +let update_mword_dec w n b = setBit w (natFromInteger n) (bool_of_bitU b) + +val update_mword_inc : forall 'a. mword 'a -> integer -> bitU -> mword 'a +let update_mword_inc w n b = + let top = (length_mword w) - 1 in + update_mword_dec w (top - n) b + +val update_mword : forall 'a. bool -> mword 'a -> integer -> bitU -> mword 'a +let update_mword is_inc w n b = + if is_inc then update_mword_inc w n b else update_mword_dec w n b + +(*** Bitvectors *) class (Bitvector 'a) val bits_of : 'a -> list bitU val of_bits : list bitU -> 'a + val length : 'a -> integer val unsigned : 'a -> integer - (* The first two parameters of the following specify indexing: - indexing order and start index *) - val get_bit : bool -> integer -> 'a -> integer -> bitU - val set_bit : bool -> integer -> 'a -> integer -> bitU -> 'a - val get_bits : bool -> integer -> 'a -> integer -> integer -> list bitU - val set_bits : bool -> integer -> 'a -> integer -> integer -> list bitU -> 'a + val signed : 'a -> integer + (* The first parameter specifies the indexing order (true is increasing) *) + val get_bit : bool -> 'a -> integer -> bitU + val set_bit : bool -> 'a -> integer -> bitU -> 'a + val get_bits : bool -> 'a -> integer -> integer -> list bitU + val set_bits : bool -> 'a -> integer -> integer -> list bitU -> 'a end instance forall 'a. BitU 'a => (Bitvector (list 'a)) let bits_of v = List.map to_bitU v let of_bits v = List.map of_bitU v - let unsigned v = bitlist_to_unsigned (List.map to_bitU v) - let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n) - let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b] - let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j) - let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map of_bitU v') -end - -instance forall 'a. BitU 'a => (Bitvector (vector 'a)) - let bits_of v = List.map to_bitU (get_elems v) - let of_bits v = Vector (List.map of_bitU v) (integerFromNat (List.length v) - 1) false - let unsigned v = unsigned (get_elems v) - let get_bit is_inc start v n = to_bitU (access v n) - let set_bit is_inc start v n b = update_pos v n (of_bitU b) - let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j)) - let set_bits is_inc start v i j v' = update v i j (Vector (List.map of_bitU v') (integerFromNat (List.length v') - 1) false) + let length v = length_list v + let unsigned v = unsigned_of_bits (List.map to_bitU v) + let signed v = signed_of_bits (List.map to_bitU v) + let get_bit is_inc v n = to_bitU (access_list is_inc v n) + let set_bit is_inc v n b = update_list is_inc v n (of_bitU b) + let get_bits is_inc v i j = List.map to_bitU (slice_list is_inc v i j) + let set_bits is_inc v i j v' = update_slice_list is_inc v i j (List.map of_bitU v') end instance forall 'a. Size 'a => (Bitvector (mword 'a)) let bits_of v = List.map to_bitU (bitlistFromWord v) let of_bits v = wordFromBitlist (List.map of_bitU v) + let length v = integerFromNat (word_length v) let unsigned v = unsignedIntegerFromWord v - let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n) - let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [of_bitU b]) - let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j - let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map of_bitU v')) + let signed v = signedIntegerFromWord v + let get_bit = access_mword + let set_bit = update_mword + let get_bits is_inc v i j = get_bits is_inc (bitlistFromWord v) i j + let set_bits is_inc v i j v' = wordFromBitlist (set_bits is_inc (bitlistFromWord v) i j v') end -(*let showBitvector (Bitvector elems start inc) = - "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc +let access_vec_inc v n = get_bit true v n +let access_vec_dec v n = get_bit false v n -let bvget_dir (Bitvector _ _ ord) = ord -let bvget_start (Bitvector _ s _) = s -let bvget_elems (Bitvector elems _ _) = elems +let update_vec_inc v n b = set_bit true v n b +let update_vec_dec v n b = set_bit false v n b -instance forall 'a. (Show (bitvector 'a)) - let show = showBitvector -end*) +let subrange_vec_inc v i j = of_bits (get_bits true v i j) +let subrange_vec_dec v i j = of_bits (get_bits false v i j) -let bvec_to_vec is_inc start bs = - let bits = List.map bool_to_bitU (bitlistFromWord bs) in - Vector bits start is_inc +let update_subrange_vec_inc v i j v' = set_bits true v i j (bits_of v') +let update_subrange_vec_dec v i j v' = set_bits false v i j (bits_of v') -let vec_to_bvec (Vector elems start is_inc) = - (*let word =*) wordFromBitlist (List.map bitU_to_bool elems) (*in - Bitvector word start is_inc*) +val extz_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b +let extz_vec n v = of_bits (extz_bits n (bits_of v)) -(*** Vector operations *) +val exts_vec : forall 'a 'b. Bitvector 'a, Bitvector 'b => integer -> 'a -> 'b +let exts_vec n v = of_bits (exts_bits n (bits_of v)) -(* Bytes and addresses *) +(*** Bytes and addresses *) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) let rec byte_chunks n list = match (n,list) with @@ -461,18 +449,13 @@ let rec byte_chunks n list = match (n,list) with | _ -> failwith "byte_chunks not given enough bits" end -val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> list bitU -let bitv_of_byte_lifteds dir v = - let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in - let len = integerFromNat (List.length bits) in - bits (*Vector bits (if dir then 0 else len - 1) dir*) - -val bitv_of_bytes : bool -> list Sail_impl_base.byte -> list bitU -let bitv_of_bytes dir v = - let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in - let len = integerFromNat (List.length bits) in - bits (*Vector bits (if dir then 0 else len - 1) dir*) +val bitv_of_byte_lifteds : list Sail_impl_base.byte_lifted -> list bitU +let bitv_of_byte_lifteds v = + foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v +val bitv_of_bytes : list Sail_impl_base.byte -> list bitU +let bitv_of_bytes v = + foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v val byte_lifteds_of_bitv : list bitU -> list byte_lifted let byte_lifteds_of_bitv bits = @@ -506,12 +489,12 @@ let address_of_bitv v = let bytes = bytes_of_bitv v in address_of_byte_list bytes -let rec reverse_endianness_bl bits = +let rec reverse_endianness_list bits = if List.length bits <= 8 then bits else - list_append(reverse_endianness_bl(list_drop(8, bits)), list_take(8, bits)) + reverse_endianness_list (drop_list 8 bits) ++ take_list 8 bits val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a -let reverse_endianness v = of_bits (reverse_endianness_bl (bits_of v)) +let reverse_endianness v = of_bits (reverse_endianness_list (bits_of v)) (*** Registers *) @@ -567,7 +550,7 @@ let is_inc_of_reg = function end let dir_of_reg = function - | Register _ _ _ is_inc _ -> dir is_inc + | Register _ _ _ is_inc _ -> dir_of_bool is_inc | UndefinedRegister _ -> failwith "dir_of_reg UndefinedRegister" | RegisterPair _ _ -> failwith "dir_of_reg RegisterPair" end @@ -658,8 +641,8 @@ let external_reg_field_slice reg rfield (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 +let internal_mem_value bytes = + List.reverse bytes $> bitv_of_byte_lifteds diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index f9011323..df530bc7 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -127,12 +127,12 @@ let is_exclusive = function end -val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => bool -> read_kind -> 'a -> integer -> M 'regs 'b 'e -let read_mem dir read_kind addr sz state = +val read_mem : forall 'regs 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'regs 'b 'e +let read_mem read_kind addr sz state = let addr = unsigned addr in let addrs = range addr (addr+sz-1) in let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in - let value = of_bits (Sail_values.internal_mem_value dir memory_value) in + let value = of_bits (Sail_values.internal_mem_value memory_value) in if is_exclusive read_kind then [(Value value, <| state with last_exclusive_operation_was_load = true |>)] else [(Value value, state)] @@ -140,8 +140,8 @@ let read_mem dir read_kind addr sz state = (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : forall 'regs 'a 'e. Bitvector 'a => bool -> read_kind -> 'a -> M 'regs bitU 'e -let read_tag dir read_kind addr state = +val read_tag : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> M 'regs bitU 'e +let read_tag read_kind addr state = let addr = (unsigned addr) / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with | Just t -> t @@ -216,30 +216,30 @@ let update_reg reg f v state = let write_reg_field reg regfield = update_reg reg regfield.set_field val update_reg_range : forall 'regs 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'a -> integer -> integer -> 'a -> 'b -> 'a -let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) (reg.reg_start) reg_val i j (bits_of new_val) +let update_reg_range reg i j reg_val new_val = set_bits (reg.reg_is_inc) reg_val i j (bits_of new_val) let write_reg_range reg i j = update_reg reg (update_reg_range reg i j) -let update_reg_pos reg i reg_val x = update_pos reg_val i x +let update_reg_pos reg i reg_val x = update_list reg.reg_is_inc reg_val i x let write_reg_pos reg i = update_reg reg (update_reg_pos reg i) -let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) (reg.reg_start) reg_val i (to_bitU bit) +let update_reg_bit reg i reg_val bit = set_bit (reg.reg_is_inc) reg_val i (to_bitU bit) let write_reg_bit reg i = update_reg reg (update_reg_bit reg i) let update_reg_field_range regfield i j reg_val new_val = let current_field_value = regfield.get_field reg_val in - let new_field_value = set_bits (regfield.field_is_inc) (regfield.field_start) current_field_value i j (bits_of new_val) in + let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in regfield.set_field reg_val new_field_value let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j) let update_reg_field_pos regfield i reg_val x = let current_field_value = regfield.get_field reg_val in - let new_field_value = update_pos current_field_value i x in + let new_field_value = update_list regfield.field_is_inc current_field_value i x in regfield.set_field reg_val new_field_value let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i) let update_reg_field_bit regfield i reg_val bit = let current_field_value = regfield.get_field reg_val in - let new_field_value = set_bit (regfield.field_is_inc) (regfield.field_start) current_field_value i (to_bitU bit) in + let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in regfield.set_field reg_val new_field_value let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i) diff --git a/src/initial_check.mli b/src/initial_check.mli index 5466dece..755da523 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -68,6 +68,7 @@ val process_ast : order -> Parse_ast.defs -> unit defs val val_spec_ids : 'a defs -> IdSet.t +val extern_of_string : order -> id -> string -> unit def val val_spec_of_string : order -> id -> string -> unit def val exp_of_string : order -> string -> unit exp diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 368f7505..219677ac 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -102,6 +102,12 @@ type direction = | D_increasing | D_decreasing +let dir_of_bool is_inc = if is_inc then D_increasing else D_decreasing +let bool_of_dir = function + | D_increasing -> true + | D_decreasing -> false + end + (* at some point this should probably not mention bit_lifted anymore *) type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c776081c..a759162e 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -209,7 +209,6 @@ let rec lem_nexps_of_typ (Typ_aux (t,_)) = List.fold_left (fun s t -> NexpSet.union s (trec t)) NexpSet.empty ts | 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, _)]) -> @@ -266,19 +265,18 @@ let doc_typ_lem, doc_atomic_typ_lem = | _ -> app_typ atyp_needed ty and app_typ 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",_)),_) when !opt_mwords -> - string "bitvector " ^^ doc_nexp_lem (nexp_simp m) + string "mword " ^^ doc_nexp_lem (nexp_simp m) (* (match nexp_simp 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 elem_typ in + | _ -> string "list" ^^ space ^^ typ 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? *) @@ -341,11 +339,11 @@ let rec contains_t_pp_var ctxt (Typ_aux (t,a) as typ) = match t with | Typ_app (c,targs) -> if Ast_util.is_number typ then false else if is_bitvector_typ typ then - let (_,length,_,_) = vector_typ_args_of typ in - let length = nexp_simp length in - not (is_nexp_constant length || - (!opt_mwords && - match length with Nexp_aux (Nexp_var _,_) -> true | _ -> false)) + if !opt_mwords then + let (_,length,_,_) = vector_typ_args_of typ in + let length = nexp_simp length in + not (is_nexp_constant length || NexpSet.mem length ctxt.bound_nexps) + else false else List.exists (contains_t_arg_pp_var ctxt) targs and contains_t_arg_pp_var ctxt (Typ_arg_aux (targ, _)) = match targ with | Typ_arg_typ t -> contains_t_pp_var ctxt t @@ -393,7 +391,8 @@ let doc_lit_lem (L_aux(lit,l)) = | _ -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in - separate space (List.map string ["realFromFrac"; Big_int.to_string num; Big_int.to_string denom]) + parens (separate space (List.map string [ + "realFromFrac"; Big_int.to_string num; Big_int.to_string denom])) (* typ_doc is the doc for the type being quantified *) let doc_quant_item vars_included (QI_aux (qi, _)) = match qi with @@ -429,7 +428,7 @@ let rec typeclass_nexps (Typ_aux(t,_)) = | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2) | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) | Typ_app (Id_aux (Id "vector",_), - [_;Typ_arg_aux (Typ_arg_nexp size_nexp,_); + [Typ_arg_aux (Typ_arg_nexp size_nexp,_); _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) | Typ_app (Id_aux (Id "itself",_), [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) -> @@ -489,9 +488,7 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with if contains_t_pp_var ctxt typ then doc_p else parens (doc_op colon doc_p (doc_typ_lem typ)) | P_vector pats -> - let ppp = - (separate space) - [string "Vector";brackets (separate_map semi (doc_pat_lem ctxt true) pats);underscore;underscore] in + let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in if apat_needed then parens ppp else ppp | P_vector_concat pats -> raise (Reporting_basic.err_unreachable l @@ -598,6 +595,8 @@ let doc_exp_lem, doc_let_lem = (string "write_reg_field") (doc_lexp_deref_lem ctxt le ^^ space ^^ field_ref ^/^ expY e)) + | LEXP_deref re -> + liftR ((prefix 2 1) (string "write_reg") (expY re ^/^ expY e)) | _ -> liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem ctxt le ^/^ expY e))) | E_vector_append(le,re) -> @@ -605,15 +604,19 @@ let doc_exp_lem, doc_let_lem = "E_vector_append should have been rewritten before pretty-printing") | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re) | E_if(c,t,e) -> - let (E_aux (_,(_,cannot))) = c in + let indent = match e with + | E_aux (E_if _, _) -> 0 + | _ -> 2 in let epp = separate space [string "if";group (expY c)] ^^ break 1 ^^ (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^ - (prefix 2 1 (string "else") (expN e)) in + (prefix indent 1 (string "else") (expN e)) in if aexp_needed then parens (align epp) else epp | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> - raise (report l "E_for should have been removed till now") + raise (report l "E_for should have been rewritten before pretty-printing") + | E_loop _ -> + raise (report l "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in if aexp_needed then parens epp else epp @@ -698,18 +701,12 @@ let doc_exp_lem, doc_let_lem = | Some (env, _, _) when Env.is_extern f env "lem" -> string (Env.get_extern f env "lem"), true | _ -> doc_id_lem f, false in - let argspp = - (* TODO Update Sail library functions to not use tupled arguments, - then remove the special case here *) - if is_extern then - parens (align (separate_map (comma ^^ break 0) (expV true) args)) - else - align (separate_map (break 1) (expV true) args) in + let argspp = align (separate_map (break 1) (expV true) args) in let epp = align (call ^//^ argspp) in let (taepp,aexp_needed) = - let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in + let t = Env.expand_synonyms (env_of full_exp) (typ_of full_exp) in let eff = effect_of full_exp in - if typ_needs_printed (Env.base_typ_of (env_of full_exp) t) + if typ_needs_printed t then (align epp ^^ (doc_tannot_lem ctxt (effectful eff) t), true) else (epp, aexp_needed) in liftR (if aexp_needed then parens (align taepp) else taepp) @@ -735,7 +732,7 @@ let doc_exp_lem, doc_let_lem = | E_block [] -> string "()" | E_block exps -> raise (report l "Blocks should have been removed till now.") | E_nondet exps -> raise (report l "Nondet blocks not supported.") - | E_id id -> + | E_id id | E_ref id -> let env = env_of full_exp in let typ = typ_of full_exp in let eff = effect_of full_exp in @@ -793,11 +790,10 @@ let doc_exp_lem, doc_let_lem = if count = 20 then 0 else count + 1) (expN e,0) es in align (group expspp) in - let epp = - group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in + let epp = brackets expspp in let (epp,aexp_needed) = if is_bit_typ etyp && !opt_mwords then - let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in + let bepp = string "of_bits" ^^ space ^^ parens (align epp) in (bepp ^^ doc_tannot_lem ctxt false t, true) else (epp,aexp_needed) in if aexp_needed then parens (align epp) else epp @@ -811,22 +807,6 @@ let doc_exp_lem, doc_let_lem = brackets (separate_map semi (expN) exps) | E_case(e,pexps) -> let only_integers e = expY e in - (* - (* This is a hack, incomplete. It's because lem does not allow - pattern-matching on integers *) - let typ = typ_of e in - if Ast_util.is_number typ then - let e_pp = expY e in - align (string "toNatural" ^//^ e_pp) - else - (* TODO: Where does this come from?? *) - (match typ with - | Typ_aux (Typ_tup ([t1;t2;t3;t4;t5] as ts), _) when List.for_all Ast_util.is_number ts -> - let e_pp = expY e in - align (string "toNaturalFiveTup" ^//^ e_pp) - | _ -> expY e) - in*) - let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ (separate_map (break 1) (doc_case ctxt) pexps) ^/^ @@ -884,7 +864,8 @@ let doc_exp_lem, doc_let_lem = align (parens (string "early_return" ^//^ expV true r ^//^ ta)) | E_constraint _ -> string "true" | E_comment _ | E_comment_struc _ -> empty - | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ -> + | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ + | E_internal_exp_user _ | E_internal_value _ -> raise (Reporting_basic.err_unreachable l "unsupported internal expression encountered while pretty-printing") and let_exp ctxt (LB_aux(lb,_)) = match lb with @@ -1202,9 +1183,9 @@ let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) = | _, _ -> [pat], identity -let doc_rec_lem (Rec_aux(r,_)) = match r with - | Rec_nonrec -> space - | Rec_rec -> space ^^ string "rec" ^^ space +let doc_rec_lem force_rec (Rec_aux(r,_)) = match r with + | Rec_nonrec when not force_rec -> space + | _ -> space ^^ string "rec" ^^ space let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem typ) @@ -1312,11 +1293,11 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = auxiliary_functions ^^ hardline ^^ hardline ^^ (prefix 2 1) - ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"]) + ((separate space) [string "let" ^^ doc_rec_lem false r ^^ doc_id_lem id;equals;string "function"]) (clauses ^/^ string "end") | FCL_aux (FCL_Funcl(id,_),annot) :: _ when not (Env.is_extern id (env_of_annot annot) "lem") -> - string "let" ^^ (doc_rec_lem r) ^^ (doc_fundef_rhs_lem fd) + string "let" ^^ (doc_rec_lem (List.length fcls > 1) r) ^^ (doc_fundef_rhs_lem fd) | _ -> empty diff --git a/src/process_file.ml b/src/process_file.ml index 5c13642f..fc5e792f 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -142,7 +142,7 @@ let output_lem filename libs defs = let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in let types_module = (filename ^ "_embed_types" ^ seq_suffix) in let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in - let operators_module = if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" in + let operators_module = "Sail_operators" (* if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" *) in let libs = List.map (fun lib -> lib ^ seq_suffix) libs in let base_imports = [ "Pervasives_extra"; diff --git a/src/rewrites.ml b/src/rewrites.ml index 2e8ee407..19192bab 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -81,7 +81,7 @@ let fresh_id_pat pre ((l,annot)) = let get_loc_exp (E_aux (_,(l,_))) = l -let gen_vs (id, spec) = Initial_check.val_spec_of_string dec_ord (mk_id id) spec +let gen_vs (id, spec) = Initial_check.extern_of_string dec_ord (mk_id id) spec let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Some (env, typ, effect))) let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect @@ -1407,29 +1407,27 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with | Some (_, _, eff) -> effectful_effs eff | _ -> false -let rec rewrite_lexp_to_rhs (do_rewrite : tannot lexp -> bool) ((LEXP_aux(lexp,((l,_) as annot))) as le) = - if do_rewrite le then - match lexp with - | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ | LEXP_deref _ -> (le, (fun exp -> exp)) - | LEXP_vector (lexp, e) -> - let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in - (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot)))) - | LEXP_vector_range (lexp, e1, e2) -> - let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in - (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot)))) - | LEXP_field (lexp, id) -> - begin - let (lhs, rhs) = rewrite_lexp_to_rhs do_rewrite lexp in - let (LEXP_aux (_, lannot)) = lexp in - let env = env_of_annot lannot in - match Env.expand_synonyms env (typ_of_annot lannot) with - | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> - let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in - (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot)))) - | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) - end - | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) - else (le, (fun exp -> exp)) +let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) = + match lexp with + | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ | LEXP_deref _ -> (le, (fun exp -> exp)) + | LEXP_vector (lexp, e) -> + let (lhs, rhs) = rewrite_lexp_to_rhs lexp in + (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot)))) + | LEXP_vector_range (lexp, e1, e2) -> + let (lhs, rhs) = rewrite_lexp_to_rhs lexp in + (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot)))) + | LEXP_field (lexp, id) -> + begin + let (lhs, rhs) = rewrite_lexp_to_rhs lexp in + let (LEXP_aux (_, lannot)) = lexp in + let env = env_of_annot lannot in + match Env.expand_synonyms env (typ_of_annot lannot) with + | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env -> + let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in + (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot)))) + | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) + end + | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) let updates_vars exp = let e_assign ((_, lexp), (u, exp)) = @@ -1452,7 +1450,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | [] -> [] | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps when lexp_is_local_intro le env && not (lexp_is_effectful le) -> - let (le', re') = rewrite_lexp_to_rhs (fun _ -> true) le in + let (le', re') = rewrite_lexp_to_rhs le in let e' = re' (rewrite_base e) in let exps' = walker exps in let effects = union_eff_exps exps' in @@ -1506,7 +1504,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f (E_aux (E_block (List.map strip_exp (walker exps)), (l, ()))) (typ_of full_exp) | E_assign(le,e) when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) -> - let (le', re') = rewrite_lexp_to_rhs (fun _ -> true) le in + let (le', re') = rewrite_lexp_to_rhs le in let e' = re' (rewrite_base e) in let block = annot_exp (E_block []) l (env_of full_exp) unit_typ in check_exp (env_of full_exp) @@ -1551,7 +1549,7 @@ let rewrite_register_ref_writes (Defs defs) = if is_reftyp (typ_of exp) then Some exp else None with | _ -> None in let e_assign (lexp, exp) = - let (lhs, rhs) = rewrite_lexp_to_rhs (fun le -> lexp_ref_exp le = None) lexp in + let (lhs, rhs) = rewrite_lexp_to_rhs lexp in match lexp_ref_exp lhs with | Some (E_aux (_, annot) as lhs_exp) -> let lhs = LEXP_aux (LEXP_memory (mk_id "write_reg_ref", [lhs_exp]), annot) in @@ -2113,7 +2111,7 @@ let rewrite_simple_assignments defs = let env = env_of_annot annot in match e_aux with | E_assign (lexp, exp) -> - let (lexp, rhs) = rewrite_lexp_to_rhs (fun _ -> true) lexp in + let (lexp, rhs) = rewrite_lexp_to_rhs lexp in let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in check_exp env assign unit_typ | _ -> E_aux (e_aux, annot) @@ -2470,7 +2468,7 @@ let rewrite_defs_internal_lets = E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), (l, _))), _) when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) -> (* Rewrite assignments to local variables into let bindings *) - let (lhs, rhs) = rewrite_lexp_to_rhs (fun _ -> true) le in + let (lhs, rhs) = rewrite_lexp_to_rhs le in let (LEXP_aux (_, lannot)) = lhs in let ltyp = typ_of_annot lannot in let rhs = annot_exp (E_cast (ltyp, rhs exp)) l (env_of_annot lannot) ltyp in @@ -2957,13 +2955,14 @@ let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem = [ ("tuple_vector_assignments", rewrite_tuple_vector_assignments); ("tuple_assignments", rewrite_tuple_assignments); - (* ("simple_assignments", rewrite_simple_assignments); *) + ("simple_assignments", rewrite_simple_assignments); ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); ("guarded_pats", rewrite_defs_guarded_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); - ("register_ref_writes", rewrite_register_ref_writes); + (* ("register_ref_writes", rewrite_register_ref_writes); *) + ("fix_val_specs", rewrite_fix_val_specs); ("recheck_defs", recheck_defs); (* ("constraint", rewrite_constraint); *) (* ("remove_assert", rewrite_defs_remove_assert); *) diff --git a/src/type_check.ml b/src/type_check.ml index 10be3710..d4920c5a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2182,9 +2182,14 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ let tpat, env = bind_pat_no_guard env pat ptyp in (* Propagate constraint assertions on the lhs of monadic binds to the rhs *) let env = match bind_exp with - | E_aux (E_assert (E_aux (E_constraint nc, _), _), _) -> - typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"); - Env.add_constraint nc env + | E_aux (E_assert (constr_exp, _), _) -> + begin + match assert_constraint env constr_exp with + | Some nc -> + typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"); + Env.add_constraint nc env + | None -> env + end | _ -> env in let checked_body = crule check_exp env body typ in annot_exp (E_internal_plet (tpat, bind_exp, checked_body)) typ @@ -2906,9 +2911,14 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let tpat, env = bind_pat_no_guard env pat ptyp in (* Propagate constraint assertions on the lhs of monadic binds to the rhs *) let env = match bind_exp with - | E_aux (E_assert (E_aux (E_constraint nc, _), _), _) -> - typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"); - Env.add_constraint nc env + | E_aux (E_assert (constr_exp, _), _) -> + begin + match assert_constraint env constr_exp with + | Some nc -> + typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"); + Env.add_constraint nc env + | None -> env + end | _ -> env in let inferred_body = irule infer_exp env body in annot_exp (E_internal_plet (tpat, bind_exp, inferred_body)) (typ_of inferred_body) |