diff options
Diffstat (limited to 'src/gen_lib')
| -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 |
4 files changed, 418 insertions, 625 deletions
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) |