diff options
Diffstat (limited to 'src/gen_lib/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 767 |
1 files changed, 256 insertions, 511 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 121f6cc8..bd18cf81 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -1,4 +1,7 @@ +(* Version of sail_values.lem that uses Lem's machine words library *) + open import Pervasives_extra +open import Machine_word open import Sail_impl_base @@ -8,6 +11,44 @@ type nn = natural val pow : integer -> integer -> integer let pow m n = m ** (natFromInteger n) +let pow2 n = pow 2 n + +let add_int (l,r) = integerAdd l r +let add_signed (l,r) = integerAdd l r +let sub_int (l,r) = integerMinus l r +let mult_int (l,r) = integerMult l r +let quotient_int (l,r) = integerDiv l r +let quotient_nat (l,r) = natDiv l r +let power_int_nat (l,r) = integerPow l r +let power_int_int (l, r) = integerPow l (natFromInteger r) +let negate_int i = integerNegate i +let min_int (l, r) = integerMin l r +let max_int (l, r) = integerMax l r + +let add_real (l, r) = realAdd l r +let sub_real (l, r) = realMinus l r +let mult_real (l, r) = realMult l r +let div_real (l, r) = realDiv l r +let negate_real r = realNegate r +let abs_real r = realAbs r +let power_real (b, e) = realPowInteger b e + +let or_bool (l, r) = (l || r) +let and_bool (l, r) = (l && r) +let xor_bool (l, r) = xor l r + +let list_append (l, r) = l ++ r +let list_length xs = integerFromNat (List.length xs) +let list_take (n, xs) = List.take (natFromInteger n) xs +let list_drop (n, xs) = List.drop (natFromInteger n) xs + +val repeat : forall 'a. list 'a -> integer -> list 'a +let rec repeat xs n = + if n <= 0 then [] + else xs ++ repeat xs (n-1) + +let duplicate_to_list (bit, length) = repeat [bit] length + let rec replace bs ((n : integer),b') = match bs with | [] -> [] | b :: bs -> @@ -15,6 +56,7 @@ let rec replace bs ((n : integer),b') = match bs with else b :: replace bs (n - 1,b') end +let upper n = n (*** Bits *) type bitU = B0 | B1 | BU @@ -29,6 +71,15 @@ instance (Show bitU) let show = showBitU end +class (BitU 'a) + val to_bitU : 'a -> bitU + val of_bitU : bitU -> 'a +end + +instance (BitU bitU) + let to_bitU b = b + let of_bitU b = b +end let bitU_to_bool = function | B0 -> false @@ -36,6 +87,15 @@ let bitU_to_bool = function | BU -> failwith "to_bool applied to BU" end +let bool_to_bitU b = if b then B1 else B0 + +instance (BitU bool) + let to_bitU = bool_to_bitU + let of_bitU = bitU_to_bool +end + +let cast_bit_bool = bitU_to_bool + let bit_lifted_of_bitU = function | B0 -> Bitl_zero | B1 -> Bitl_one @@ -66,14 +126,12 @@ let bitwise_not_bit = function | BU -> BU end -let inline (~) = bitwise_not_bit +(* let inline (~) = bitwise_not_bit *) val is_one : integer -> bitU let is_one i = if i = 1 then B1 else B0 -let bool_to_bitU b = if b then B1 else B0 - let bitwise_binop_bit op = function | (BU,_) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) | (_,BU) -> BU (*Do we want to do this or to respect | of I and & of B0 rules?*) @@ -98,6 +156,56 @@ let inline (|.) x y = bitwise_or_bit (x,y) val (+.) : bitU -> bitU -> bitU let inline (+.) x y = bitwise_xor_bit (x,y) +val to_bin_aux : natural -> list bitU +let rec to_bin_aux x = + if x = 0 then [] + else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) +let to_bin n = List.reverse (to_bin_aux n) + +val of_bin : list bitU -> natural +let of_bin bits = + let (sum,_) = + List.foldr + (fun b (acc,exp) -> + match b with + | B1 -> (acc + naturalPow 2 exp, exp + 1) + | B0 -> (acc, exp + 1) + | BU -> failwith "of_bin: bitvector has undefined bits" + end) + (0,0) bits in + sum + +val bitlist_to_integer : list bitU -> integer +let bitlist_to_integer bs = integerFromNatural (of_bin bs) + +val pad_zero : list bitU -> integer -> list bitU +let rec pad_zero bits n = + if n <= 0 then bits else pad_zero (B0 :: bits) (n -1) + +let bitwise_not_bitlist = List.map bitwise_not_bit + +let rec add_one_bit_ignore_overflow_aux bits = match bits with + | [] -> [] + | B0 :: bits -> B1 :: bits + | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits + | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" +end + +let add_one_bit_ignore_overflow bits = + List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) + +let bits_of_nat ((len : integer),(n : natural)) = + let bits = to_bin n in + let len_bits = integerFromNat (List.length bits) in + let longer = len - len_bits in + if longer < 0 then drop (natFromInteger (abs (longer))) bits + else pad_zero bits longer + +let bits_of_int ((len : integer),(n : integer)) = + let bits = bits_of_nat (len, naturalFromInteger (abs n)) in + if n > (0 : integer) + then bits + else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits)) (*** Vectors *) @@ -112,6 +220,7 @@ let get_dir (Vector _ _ ord) = ord let get_start (Vector _ s _) = s let get_elems (Vector elems _ _) = elems let length (Vector bs _ _) = integerFromNat (length bs) +let vector_length = length instance forall 'a. Show 'a => (Show (vector 'a)) let show = showVector @@ -125,17 +234,17 @@ let bool_of_dir = function (*** Vector operations *) -val set_vector_start : forall 'a. integer -> vector 'a -> vector 'a -let set_vector_start new_start (Vector bs _ is_inc) = +val set_vector_start : forall 'a. (integer * vector 'a) -> vector 'a +let set_vector_start (new_start, Vector bs _ is_inc) = Vector bs new_start is_inc let reset_vector_start v = - set_vector_start (if (get_dir v) then 0 else (length v - 1)) v + set_vector_start (if (get_dir v) then 0 else (length v - 1), v) let set_vector_start_to_length v = - set_vector_start (length v - 1) v + set_vector_start (length v - 1, v) -let vector_concat (Vector bs start is_inc) (Vector bs' _ _) = +let vector_concat (Vector bs start is_inc, Vector bs' _ _) = Vector (bs ++ bs') start is_inc let inline (^^) = vector_concat @@ -152,14 +261,19 @@ let update_sublist xs (i,j) xs' = let (prefix,_fromItoJ) = List.splitAt i toJ in prefix ++ xs' ++ suffix -val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a -let slice (Vector bs start is_inc) i j = +val slice_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a +let slice_aux is_inc start bs i j = let iN = natFromInteger i in let jN = natFromInteger j in let startN = natFromInteger start in - let subvector_bits = - sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) in - Vector subvector_bits i is_inc + sublist bs (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) + +val slice : forall 'a. vector 'a -> integer -> integer -> vector 'a +let slice (Vector bs start is_inc) i j = + Vector (slice_aux is_inc start bs i j) i is_inc + +let vector_subrange_inc (start, v, i, j) = slice v i j +let vector_subrange_dec (start, v, i, j) = slice v i j (* this is for the vector slicing introduced in vector-concat patterns: i and j index into the "raw data", the list of bits. Therefore getting the bit list is @@ -174,503 +288,115 @@ let slice_raw (Vector bs start is_inc) i j = Vector bits (if is_inc then 0 else len - 1) is_inc -val update_aux : forall 'a. vector 'a -> integer -> integer -> list 'a -> vector 'a -let update_aux (Vector bs start is_inc) i j bs' = +val update_aux : forall 'a. bool -> integer -> list 'a -> integer -> integer -> list 'a -> list 'a +let update_aux is_inc start bs i j bs' = let iN = natFromInteger i in let jN = natFromInteger j in let startN = natFromInteger start in - let bits = - (update_sublist bs) - (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' in - Vector bits start is_inc + update_sublist bs + (if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN)) bs' val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector 'a -let update v i j (Vector bs' _ _) = - update_aux v i j bs' +let update (Vector bs start is_inc) i j (Vector bs' _ _) = + Vector (update_aux is_inc start bs i j bs') start is_inc + +let vector_update_subrange_inc (start, v, i, j, v') = update v i j v' +let vector_update_subrange_dec (start, v, i, j, v') = update v i j v' + +val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a +let access_aux is_inc start xs n = + if is_inc then List_extra.nth xs (natFromInteger (n - start)) + else List_extra.nth xs (natFromInteger (start - n)) val access : forall 'a. vector 'a -> integer -> 'a -let access (Vector bs start is_inc) n = - if is_inc then List_extra.nth bs (natFromInteger (n - start)) - else List_extra.nth bs (natFromInteger (start - n)) +let access (Vector bs start is_inc) n = access_aux is_inc start bs n + +let vector_access_inc (start, v, i) = access v i +let vector_access_dec (start, v, i) = access v i val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a let update_pos v n b = - update_aux v n n [b] - + update v n n (Vector [b] 0 false) -(*** Bit vector operations *) +let vector_update_pos_inc (start, v, i, x) = update_pos v i x +let vector_update_pos_dec (start, v, i, x) = update_pos v i x -let extract_only_bit (Vector elems _ _) = match elems with - | [] -> failwith "extract_single_bit called for empty vector" +let extract_only_element (Vector elems _ _) = match elems with + | [] -> failwith "extract_only_element called for empty vector" | [e] -> e - | _ -> failwith "extract_single_bit called for vector with more bits" + | _ -> failwith "extract_only_element called for vector with more elements" end -let pp_bitu_vector (Vector elems start inc) = - let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in - "Vector [" ^ elems_pp ^ "] " ^ show start ^ " " ^ show inc - - -let most_significant = function - | (Vector (b :: _) _ _) -> b - | _ -> failwith "most_significant applied to empty vector" - end - -let bitwise_not_bitlist = List.map bitwise_not_bit - -let bitwise_not (Vector bs start is_inc) = - Vector (bitwise_not_bitlist bs) start is_inc +(*** Bitvectors *) -let bitwise_binop op (Vector bsl start is_inc, Vector bsr _ _) = - let revbs = foldl (fun acc pair -> bitwise_binop_bit op pair :: acc) [] (zip bsl bsr) in - Vector (reverse revbs) start is_inc - -let bitwise_and = bitwise_binop (&&) -let bitwise_or = bitwise_binop (||) -let bitwise_xor = bitwise_binop xor - -let unsigned (Vector bs _ _) : integer = - let (sum,_) = - List.foldr - (fun b (acc,exp) -> - match b with - | B1 -> (acc + integerPow 2 exp,exp + 1) - | B0 -> (acc, exp + 1) - | BU -> failwith "unsigned: vector has undefined bits" - end) - (0,0) bs in - sum - -let unsigned_big = unsigned - -let signed v : integer = - match most_significant v with - | B1 -> 0 - (1 + (unsigned (bitwise_not v))) - | B0 -> unsigned v - | BU -> failwith "signed applied to vector with undefined bits" - end - -let hardware_mod (a: integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) mod (abs b) - else if (a < 0 && b >= 0) - then (a mod b) - b - else a mod b - -(* There are different possible answers for integer divide regarding -rounding behaviour on negative operands. Positive operands always -round down so derive the one we want (trucation towards zero) from -that *) -let hardware_quot (a:integer) (b:integer) : integer = - let q = (abs a) / (abs b) in - if ((a<0) = (b<0)) then - q (* same sign -- result positive *) - else - integerNegate q (* different sign -- result negative *) - -let quot_signed = hardware_quot - - -let signed_big = signed - -let to_num sign = if sign then signed else unsigned - -let max_64u = (integerPow 2 64) - 1 -let max_64 = (integerPow 2 63) - 1 -let min_64 = 0 - (integerPow 2 63) -let max_32u = (4294967295 : integer) -let max_32 = (2147483647 : integer) -let min_32 = (0 - 2147483648 : integer) -let max_8 = (127 : integer) -let min_8 = (0 - 128 : integer) -let max_5 = (31 : integer) -let min_5 = (0 - 32 : integer) - -let get_max_representable_in sign (n : integer) : integer = - if (n = 64) then match sign with | true -> max_64 | false -> max_64u end - else if (n=32) then match sign with | true -> max_32 | false -> max_32u end - else if (n=8) then max_8 - else if (n=5) then max_5 - else match sign with | true -> integerPow 2 ((natFromInteger n) -1) - | false -> integerPow 2 (natFromInteger n) - end - -let get_min_representable_in _ (n : integer) : integer = - if n = 64 then min_64 - else if n = 32 then min_32 - else if n = 8 then min_8 - else if n = 5 then min_5 - else 0 - (integerPow 2 (natFromInteger n)) - -val to_bin_aux : natural -> list bitU -let rec to_bin_aux x = - if x = 0 then [] - else (if x mod 2 = 1 then B1 else B0) :: to_bin_aux (x / 2) -let to_bin n = List.reverse (to_bin_aux n) - -val pad_zero : list bitU -> integer -> list bitU -let rec pad_zero bits n = - if n = 0 then bits else pad_zero (B0 :: bits) (n -1) - - -let rec add_one_bit_ignore_overflow_aux bits = match bits with - | [] -> [] - | B0 :: bits -> B1 :: bits - | B1 :: bits -> B0 :: add_one_bit_ignore_overflow_aux bits - | BU :: _ -> failwith "add_one_bit_ignore_overflow: undefined bit" +(* element list * start * has increasing direction *) +type bitvector 'a = mword 'a (* Bitvector of mword 'a * integer * bool *) +declare isabelle target_sorts bitvector = `len` + +class (Bitvector 'a) + val bits_of : 'a -> list bitU + val of_bits : list bitU -> 'a + val unsigned : 'a -> integer + (* The first two parameters of the following specify indexing: + indexing order and start index *) + val get_bit : bool -> integer -> 'a -> integer -> bitU + val set_bit : bool -> integer -> 'a -> integer -> bitU -> 'a + val get_bits : bool -> integer -> 'a -> integer -> integer -> list bitU + val set_bits : bool -> integer -> 'a -> integer -> integer -> list bitU -> 'a end -let add_one_bit_ignore_overflow bits = - List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) - - -let to_vec is_inc ((len : integer),(n : integer)) = - let start = if is_inc then 0 else len - 1 in - let bits = to_bin (naturalFromInteger (abs n)) in - let len_bits = integerFromNat (List.length bits) in - let longer = len - len_bits in - let bits' = - if longer < 0 then drop (natFromInteger (abs (longer))) bits - else pad_zero bits longer in - if n > (0 : integer) - then Vector bits' start is_inc - else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits')) - start is_inc - -let to_vec_big = to_vec - -let to_vec_inc = to_vec true -let to_vec_dec = to_vec false - -let to_vec_undef is_inc (len : integer) = - Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc - -let to_vec_inc_undef = to_vec_undef true -let to_vec_dec_undef = to_vec_undef false - -let exts (len, vec) = to_vec (get_dir vec) (len,signed vec) -let extz (len, vec) = to_vec (get_dir vec) (len,unsigned vec) - -let exts_big (len, vec) = to_vec_big (get_dir vec) (len, signed_big vec) -let extz_big (len, vec) = to_vec_big (get_dir vec) (len, unsigned_big vec) - -let add = integerAdd -let add_signed = integerAdd -let minus = integerMinus -let multiply = integerMult -let modulo = hardware_mod -let quot = hardware_quot -let power = integerPow - -let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r = - let (l',r') = (to_num sign l, to_num sign r) in - let n = op l' r' in - to_vec is_inc (size * (length l),n) - - -(* add_vec - * add_vec_signed - * minus_vec - * multiply_vec - * multiply_vec_signed - *) -let add_VVV = arith_op_vec integerAdd false 1 -let addS_VVV = arith_op_vec integerAdd true 1 -let minus_VVV = arith_op_vec integerMinus false 1 -let mult_VVV = arith_op_vec integerMult false 2 -let multS_VVV = arith_op_vec integerMult true 2 - -let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r = - arith_op_vec op sign size l (to_vec is_inc (length l,r)) - -(* add_vec_range - * add_vec_range_signed - * minus_vec_range - * mult_vec_range - * mult_vec_range_signed - *) -let add_VIV = arith_op_vec_range integerAdd false 1 -let addS_VIV = arith_op_vec_range integerAdd true 1 -let minus_VIV = arith_op_vec_range integerMinus false 1 -let mult_VIV = arith_op_vec_range integerMult false 2 -let multS_VIV = arith_op_vec_range integerMult true 2 - -let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) = - arith_op_vec op sign size (to_vec is_inc (length r, l)) r - -(* add_range_vec - * add_range_vec_signed - * minus_range_vec - * mult_range_vec - * mult_range_vec_signed - *) -let add_IVV = arith_op_range_vec integerAdd false 1 -let addS_IVV = arith_op_range_vec integerAdd true 1 -let minus_IVV = arith_op_range_vec integerMinus false 1 -let mult_IVV = arith_op_range_vec integerMult false 2 -let multS_IVV = arith_op_range_vec integerMult true 2 - -let arith_op_range_vec_range op sign l r = op l (to_num sign r) - -(* add_range_vec_range - * add_range_vec_range_signed - * minus_range_vec_range - *) -let add_IVI = arith_op_range_vec_range integerAdd false -let addS_IVI = arith_op_range_vec_range integerAdd true -let minus_IVI = arith_op_range_vec_range integerMinus false - -let arith_op_vec_range_range op sign l r = op (to_num sign l) r - -(* add_vec_range_range - * add_vec_range_range_signed - * minus_vec_range_range - *) -let add_VII = arith_op_vec_range_range integerAdd false -let addS_VII = arith_op_vec_range_range integerAdd true -let minus_VII = arith_op_vec_range_range integerMinus false - - - -let arith_op_vec_vec_range op sign l r = - let (l',r') = (to_num sign l,to_num sign r) in - op l' r' - -(* add_vec_vec_range - * add_vec_vec_range_signed - *) -let add_VVI = arith_op_vec_vec_range integerAdd false -let addS_VVI = arith_op_vec_vec_range integerAdd true - -let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r = - let l' = to_num sign l in - let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - to_vec is_inc (length l * size,n) - -(* add_vec_bit - * add_vec_bit_signed - * minus_vec_bit_signed - *) -let add_VBV = arith_op_vec_bit integerAdd false 1 -let addS_VBV = arith_op_vec_bit integerAdd true 1 -let minus_VBV = arith_op_vec_bit integerMinus true 1 - -let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Vector _ _ is_inc as l) r = - let len = length l in - let act_size = len * size in - let (l_sign,r_sign) = (to_num sign l,to_num sign r) in - let (l_unsign,r_unsign) = (to_num false l,to_num false r) in - let n = op l_sign r_sign in - let n_unsign = op l_unsign r_unsign in - let correct_size_num = to_vec is_inc (act_size,n) in - let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in - let overflow = - if n <= get_max_representable_in sign len && - n >= get_min_representable_in sign len - then B0 else B1 in - let c_out = most_significant one_more_size_u in - (correct_size_num,overflow,c_out) - -(* add_overflow_vec - * add_overflow_vec_signed - * minus_overflow_vec - * minus_overflow_vec_signed - * mult_overflow_vec - * mult_overflow_vec_signed - *) -let addO_VVV = arith_op_overflow_vec integerAdd false 1 -let addSO_VVV = arith_op_overflow_vec integerAdd true 1 -let minusO_VVV = arith_op_overflow_vec integerMinus false 1 -let minusSO_VVV = arith_op_overflow_vec integerMinus true 1 -let multO_VVV = arith_op_overflow_vec integerMult false 2 -let multSO_VVV = arith_op_overflow_vec integerMult true 2 - -let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (size : integer) - (Vector _ _ is_inc as l) r_bit = - let act_size = length l * size in - let l' = to_num sign l in - let l_u = to_num false l in - let (n,nu,changed) = match r_bit with - | B1 -> (op l' 1, op l_u 1, true) - | B0 -> (l',l_u,false) - | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit" - end in -(* | _ -> assert false *) - let correct_size_num = to_vec is_inc (act_size,n) in - let one_larger = to_vec is_inc (act_size + 1,nu) in - let overflow = - if changed - then - if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size - then B0 else B1 - else B0 in - (correct_size_num,overflow,most_significant one_larger) - -(* add_overflow_vec_bit_signed - * minus_overflow_vec_bit - * minus_overflow_vec_bit_signed - *) -let addSO_VBV = arith_op_overflow_vec_bit integerAdd true 1 -let minusO_VBV = arith_op_overflow_vec_bit integerMinus false 1 -let minusSO_VBV = arith_op_overflow_vec_bit integerMinus true 1 - -type shift = LL_shift | RR_shift | LLL_shift - -let shift_op_vec op (Vector bs start is_inc,(n : integer)) = - let n = natFromInteger n in - match op with - | LL_shift (*"<<"*) -> - Vector (sublist bs (n,List.length bs -1) ++ List.replicate n B0) start is_inc - | RR_shift (*">>"*) -> - Vector (List.replicate n B0 ++ sublist bs (0,n-1)) start is_inc - | LLL_shift (*"<<<"*) -> - Vector (sublist bs (n,List.length bs - 1) ++ sublist bs (0,n-1)) start is_inc - end - -let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) -let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) -let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) - -let rec arith_op_no0 (op : integer -> integer -> integer) l r = - if r = 0 - then Nothing - else Just (op l r) - -let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector _ start is_inc) as l) r = - let act_size = length l * size in - let (l',r') = (to_num sign l,to_num sign r) in - let n = arith_op_no0 op l' r' in - let (representable,n') = - match n with - | Just n' -> - (n' <= get_max_representable_in sign act_size && - n' >= get_min_representable_in sign act_size, n') - | _ -> (false,0) - end in - if representable - then to_vec is_inc (act_size,n') - else Vector (List.replicate (natFromInteger act_size) BU) start is_inc - -let mod_VVV = arith_op_vec_no0 hardware_mod false 1 -let quot_VVV = arith_op_vec_no0 hardware_quot false 1 -let quotS_VVV = arith_op_vec_no0 hardware_quot true 1 - -let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r = - let rep_size = length r * size in - let act_size = length l * size in - let (l',r') = (to_num sign l,to_num sign r) in - let (l_u,r_u) = (to_num false l,to_num false r) in - let n = arith_op_no0 op l' r' in - let n_u = arith_op_no0 op l_u r_u in - let (representable,n',n_u') = - match (n, n_u) with - | (Just n',Just n_u') -> - ((n' <= get_max_representable_in sign rep_size && - n' >= (get_min_representable_in sign rep_size)), n', n_u') - | _ -> (true,0,0) - end in - let (correct_size_num,one_more) = - if representable then - (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u')) - else - (Vector (List.replicate (natFromInteger act_size) BU) start is_inc, - Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in - let overflow = if representable then B0 else B1 in - (correct_size_num,overflow,most_significant one_more) - -let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1 -let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1 - -let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r = - arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r)) - -let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1 - -val repeat : forall 'a. list 'a -> integer -> list 'a -let rec repeat xs n = - if n = 0 then [] - else xs ++ repeat xs (n-1) - -(* -let duplicate bit length = - Vector (repeat [bit] length) (if dir then 0 else length - 1) dir - *) - -let compare_op op (l,r) = bool_to_bitU (op l r) - -let lt = compare_op (<) -let gt = compare_op (>) -let lteq = compare_op (<=) -let gteq = compare_op (>=) - - -let compare_op_vec op sign (l,r) = - let (l',r') = (to_num sign l, to_num sign r) in - compare_op op (l',r') - -let lt_vec = compare_op_vec (<) true -let gt_vec = compare_op_vec (>) true -let lteq_vec = compare_op_vec (<=) true -let gteq_vec = compare_op_vec (>=) true - -let lt_vec_signed = compare_op_vec (<) true -let gt_vec_signed = compare_op_vec (>) true -let lteq_vec_signed = compare_op_vec (<=) true -let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false -let gt_vec_unsigned = compare_op_vec (>) false -let lteq_vec_unsigned = compare_op_vec (<=) false -let gteq_vec_unsigned = compare_op_vec (>=) false - -let compare_op_vec_range op sign (l,r) = - compare_op op ((to_num sign l),r) - -let lt_vec_range = compare_op_vec_range (<) true -let gt_vec_range = compare_op_vec_range (>) true -let lteq_vec_range = compare_op_vec_range (<=) true -let gteq_vec_range = compare_op_vec_range (>=) true - -let compare_op_range_vec op sign (l,r) = - compare_op op (l, (to_num sign r)) +instance forall 'a. BitU 'a => (Bitvector (list 'a)) + let bits_of v = List.map to_bitU v + let of_bits v = List.map of_bitU v + let unsigned v = bitlist_to_integer (List.map to_bitU v) + let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n) + let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b] + let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j) + let set_bits is_inc start v i j v' = update_aux is_inc start v i j (List.map of_bitU v') +end -let lt_range_vec = compare_op_range_vec (<) true -let gt_range_vec = compare_op_range_vec (>) true -let lteq_range_vec = compare_op_range_vec (<=) true -let gteq_range_vec = compare_op_range_vec (>=) true +instance forall 'a. BitU 'a => (Bitvector (vector 'a)) + let bits_of v = List.map to_bitU (get_elems v) + let of_bits v = Vector (List.map of_bitU v) (integerFromNat (List.length v) - 1) false + let unsigned v = unsigned (get_elems v) + let get_bit is_inc start v n = to_bitU (access v n) + let set_bit is_inc start v n b = update_pos v n (of_bitU b) + let get_bits is_inc start v i j = List.map to_bitU (get_elems (slice v i j)) + let set_bits is_inc start v i j v' = update v i j (Vector (List.map of_bitU v') (integerFromNat (List.length v') - 1) false) +end -let eq (l,r) = bool_to_bitU (l = r) -let eq_range (l,r) = bool_to_bitU (l = r) -let eq_vec (l,r) = bool_to_bitU (l = r) -let eq_bit (l,r) = bool_to_bitU (l = r) -let eq_vec_range (l,r) = eq (to_num false l,r) -let eq_range_vec (l,r) = eq (l, to_num false r) -let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) +instance forall 'a. Size 'a => (Bitvector (mword 'a)) + let bits_of v = List.map to_bitU (bitlistFromWord v) + let of_bits v = wordFromBitlist (List.map of_bitU v) + let unsigned v = unsignedIntegerFromWord v + let get_bit is_inc start v n = to_bitU (access_aux is_inc start (bitlistFromWord v) n) + let set_bit is_inc start v n b = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) n n [of_bitU b]) + let get_bits is_inc start v i j = slice_aux is_inc start (List.map to_bitU (bitlistFromWord v)) i j + let set_bits is_inc start v i j v' = wordFromBitlist (update_aux is_inc start (bitlistFromWord v) i j (List.map of_bitU v')) +end -let neq (l,r) = bitwise_not_bit (eq (l,r)) -let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r)) -let neq_range (l,r) = bitwise_not_bit (eq_range (l,r)) -let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) -let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) -let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) +(*let showBitvector (Bitvector elems start inc) = + "Bitvector " ^ show elems ^ " " ^ show start ^ " " ^ show inc +let bvget_dir (Bitvector _ _ ord) = ord +let bvget_start (Bitvector _ s _) = s +let bvget_elems (Bitvector elems _ _) = elems -val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> bool -> vector 'a -let make_indexed_vector entries default start length dir = - let length = natFromInteger length in - Vector (List.foldl replace (replicate length default) entries) start dir +instance forall 'a. (Show (bitvector 'a)) + let show = showBitvector +end*) -(* -val make_bit_vector_undef : integer -> vector bitU -let make_bitvector_undef length = - Vector (replicate (natFromInteger length) BU) 0 true - *) +let bvec_to_vec is_inc start bs = + let bits = List.map bool_to_bitU (bitlistFromWord bs) in + Vector bits start is_inc -(* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *) +let vec_to_bvec (Vector elems start is_inc) = + (*let word =*) wordFromBitlist (List.map bitU_to_bool elems) (*in + Bitvector word start is_inc*) -let mask (n,Vector bits start dir) = - let current_size = List.length bits in - Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir +(*** Vector operations *) +(* Bytes and addresses *) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) let rec byte_chunks n list = match (n,list) with @@ -679,37 +405,37 @@ let rec byte_chunks n list = match (n,list) with | _ -> failwith "byte_chunks not given enough bits" end -val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> vector bitU +val bitv_of_byte_lifteds : bool -> list Sail_impl_base.byte_lifted -> list bitU let bitv_of_byte_lifteds dir v = let bits = foldl (fun x (Byte_lifted y) -> x ++ (List.map bitU_of_bit_lifted y)) [] v in let len = integerFromNat (List.length bits) in - Vector bits (if dir then 0 else len - 1) dir + bits (*Vector bits (if dir then 0 else len - 1) dir*) -val bitv_of_bytes : bool -> list Sail_impl_base.byte -> vector bitU +val bitv_of_bytes : bool -> list Sail_impl_base.byte -> list bitU let bitv_of_bytes dir v = let bits = foldl (fun x (Byte y) -> x ++ (List.map bitU_of_bit y)) [] v in let len = integerFromNat (List.length bits) in - Vector bits (if dir then 0 else len - 1) dir + bits (*Vector bits (if dir then 0 else len - 1) dir*) -val byte_lifteds_of_bitv : vector bitU -> list byte_lifted -let byte_lifteds_of_bitv (Vector bits length is_inc) = +val byte_lifteds_of_bitv : list bitU -> list byte_lifted +let byte_lifteds_of_bitv bits = let bits = List.map bit_lifted_of_bitU bits in byte_lifteds_of_bit_lifteds bits -val bytes_of_bitv : vector bitU -> list byte -let bytes_of_bitv (Vector bits length is_inc) = +val bytes_of_bitv : list bitU -> list byte +let bytes_of_bitv bits = let bits = List.map bit_of_bitU bits in bytes_of_bits bits val bit_lifteds_of_bitUs : list bitU -> list bit_lifted let bit_lifteds_of_bitUs bits = List.map bit_lifted_of_bitU bits -val bit_lifteds_of_bitv : vector bitU -> list bit_lifted -let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs (get_elems v) +val bit_lifteds_of_bitv : list bitU -> list bit_lifted +let bit_lifteds_of_bitv v = bit_lifteds_of_bitUs v -val address_lifted_of_bitv : vector bitU -> address_lifted +val address_lifted_of_bitv : list bitU -> address_lifted let address_lifted_of_bitv v = let byte_lifteds = byte_lifteds_of_bitv v in let maybe_address_integer = @@ -719,11 +445,17 @@ let address_lifted_of_bitv v = end in Address_lifted byte_lifteds maybe_address_integer -val address_of_bitv : vector bitU -> address +val address_of_bitv : list bitU -> address let address_of_bitv v = let bytes = bytes_of_bitv v in address_of_byte_list bytes +let rec reverse_endianness_bl bits = + if List.length bits <= 8 then bits else + list_append(reverse_endianness_bl(list_drop(8, bits)), list_take(8, bits)) + +val reverse_endianness : forall 'a. Bitvector 'a => 'a -> 'a +let reverse_endianness v = of_bits (reverse_endianness_bl (bits_of v)) (*** Registers *) @@ -740,6 +472,20 @@ type register = | UndefinedRegister of integer (* length *) | RegisterPair of register * register +type register_ref 'regstate 'a = + <| reg_name : string; + reg_start : integer; + reg_is_inc : bool; + read_from : 'regstate -> 'a; + write_to : 'regstate -> 'a -> 'regstate |> + +type field_ref 'regtype 'a = + <| field_name : string; + field_start : integer; + field_is_inc : bool; + get_field : 'regtype -> 'a; + set_field : 'regtype -> 'a -> 'regtype |> + let name_of_reg = function | Register name _ _ _ _ -> name | UndefinedRegister _ -> failwith "name_of_reg UndefinedRegister" @@ -815,11 +561,11 @@ let rec external_reg_value reg_name v = rv_start = external_start; rv_start_internal = internal_start |> -val internal_reg_value : register_value -> vector bitU +val internal_reg_value : register_value -> list bitU let internal_reg_value v = - Vector (List.map bitU_of_bit_lifted v.rv_bits) - (integerFromNat v.rv_start_internal) - (v.rv_dir = D_increasing) + List.map bitU_of_bit_lifted v.rv_bits + (*(integerFromNat v.rv_start_internal) + (v.rv_dir = D_increasing)*) let external_slice (d:direction) (start:nat) ((i,j):(nat*nat)) = @@ -866,17 +612,17 @@ let internal_mem_value direction bytes = val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars let rec foreach_inc (i,stop,by) vars body = - if i <= stop + if (by > 0 && i <= stop) || (by < 0 && stop <= i) then let vars = body i vars in foreach_inc (i + by,stop,by) vars body else vars val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars -> (integer -> 'vars -> 'vars) -> 'vars -let rec foreach_dec (i,stop,by) vars body = - if i >= stop +let rec foreach_dec (stop,i,by) vars body = + if (by > 0 && i >= stop) || (by < 0 && stop >= i) then let vars = body i vars in - foreach_dec (i - by,stop,by) vars body + foreach_dec (stop,i - by,by) vars body else vars let assert' b msg_opt = @@ -884,7 +630,7 @@ let assert' b msg_opt = | Just msg -> msg | Nothing -> "unspecified error" end in - if bitU_to_bool b then () else failwith msg + if b then () else failwith msg (* convert numbers unsafely to naturals *) @@ -902,8 +648,9 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) = toNatural n4, toNatural n5) - -type regfp = +(* Let the following types be generated by Sail per spec, using either bitlists + or machine words as bitvector representation *) +(*type regfp = | RFull of (string) | RSlice of (string * integer * integer) | RSliceBit of (string * integer) @@ -945,7 +692,7 @@ end let niafp_to_nia reginfo = function | NIAFP_successor -> NIA_successor - | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) + | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv (bits_of v)) | NIAFP_LR -> NIA_LR | NIAFP_CTR -> NIA_CTR | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) @@ -953,9 +700,7 @@ end let diafp_to_dia reginfo = function | DIAFP_none -> DIA_none - | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) + | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv (bits_of v)) | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) end - -let max = uncurry max -let min = uncurry min +*) |