diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 7 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 10 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 92 |
3 files changed, 82 insertions, 27 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 826ea98f..83746c0b 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -40,6 +40,9 @@ 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 @@ -150,10 +153,6 @@ let extz (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec)) let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec)) -(* TODO *) -let extz_bl (start, len, bits) = Vector bits start false -let exts_bl (start, len, bits) = Vector bits start false - let quot = hardware_quot let modulo (l,r) = hardware_mod l r diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 74d0acf7..ff25c37b 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -111,6 +111,9 @@ let cast_bit_vec_basic (start, len, b) = vec_to_bvec (Vector [b] start false) let cast_boolvec_bitvec (Vector bs start inc) = vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc) let cast_vec_bl v = List.map bool_to_bitU (bitlistFromWord v) +let cast_int_vec n = wordFromInteger n +let cast_bl_vec (start, len, bs) = wordFromBitlist (List.map bitU_to_bool bs) +let cast_bl_svec (start, len, bs) = cast_int_vec (bitlist_to_signed bs) let pp_bitu_vector (Vector elems start inc) = let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in @@ -210,7 +213,7 @@ end let add_one_bit_ignore_overflow bits = List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits)) - + val to_norm_vec : forall 'a. Size 'a => integer -> bitvector 'a let to_norm_vec (n : integer) = wordFromInteger n (* @@ -247,10 +250,6 @@ let extz (start, len, vec) = to_norm_vec (unsigned vec) let exts_big (start, len, vec) = to_vec_big (signed_big vec) let extz_big (start, len, vec) = to_vec_big (unsigned_big vec) -(* TODO *) -let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) -let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false) - let quot = hardware_quot let modulo (l,r) = hardware_mod l r @@ -442,6 +441,7 @@ let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*) let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*) let shiftl = bitwise_leftshift +let shiftr = bitwise_rightshift let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 98ac2522..231b9c8e 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -156,6 +156,9 @@ let inline (|.) x y = bitwise_or_bit (x,y) val (+.) : bitU -> bitU -> bitU let inline (+.) x y = bitwise_xor_bit (x,y) + +(*** Bit lists ***) + val to_bin_aux : natural -> list bitU let rec to_bin_aux x = if x = 0 then [] @@ -175,14 +178,36 @@ let of_bin bits = (0,0) bits in sum -val bitlist_to_integer : list bitU -> integer -let bitlist_to_integer bs = integerFromNatural (of_bin bs) +let bitwise_not_bitlist = List.map bitwise_not_bit -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) +val bitlist_to_unsigned : list bitU -> integer +let bitlist_to_unsigned bs = integerFromNatural (of_bin bs) -let bitwise_not_bitlist = List.map bitwise_not_bit +val bitlist_to_signed : list bitU -> integer +let bitlist_to_signed 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" + 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 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) = + match bits with + | BU :: _ -> failwith "exts_bl: undefined bit" + | B1 :: _ -> ext_bl B1 (len, bits) + | _ -> ext_bl B0 (len, bits) + end let rec add_one_bit_ignore_overflow_aux bits = match bits with | [] -> [] @@ -194,19 +219,50 @@ 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 int_to_bin n = + let bits_abs = B0 :: to_bin (naturalFromInteger (abs n)) in + if n >= (0 : integer) then bits_abs + else add_one_bit_ignore_overflow (bitwise_not_bitlist 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 nibble_of_bits = function + | (B0, B0, B0, B0) -> Just #'0' + | (B0, B0, B0, B1) -> Just #'1' + | (B0, B0, B1, B0) -> Just #'2' + | (B0, B0, B1, B1) -> Just #'3' + | (B0, B1, B0, B0) -> Just #'4' + | (B0, B1, B0, B1) -> Just #'5' + | (B0, B1, B1, B0) -> Just #'6' + | (B0, B1, B1, B1) -> Just #'7' + | (B1, B0, B0, B0) -> Just #'8' + | (B1, B0, B0, B1) -> Just #'9' + | (B1, B0, B1, B0) -> Just #'A' + | (B1, B0, B1, B1) -> Just #'B' + | (B1, B1, B0, B0) -> Just #'C' + | (B1, B1, B0, B1) -> Just #'D' + | (B1, B1, B1, B0) -> Just #'E' + | (B1, B1, B1, B1) -> Just #'F' + | _ -> Nothing + end -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)) +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 s = hexstring_of_bits bs in + match (n, s) with + | (Just n, Just s) -> Just (n :: s) + | _ -> Nothing + end + | _ -> Nothing + end +let show_bitlist bs = + match hexstring_of_bits bs with + | Just s -> toString (#'0' :: #'x' :: s) + | Nothing -> show bs + end (*** Vectors *) @@ -348,7 +404,7 @@ 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_integer (List.map to_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) |