diff options
Diffstat (limited to 'src/gen_lib/sail_operators.lem')
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 290 |
1 files changed, 139 insertions, 151 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 9354f9d4..9b0857d9 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -4,20 +4,21 @@ open import Sail_values (*** Bit vector operations *) -val concat_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b, Bitvector 'c => 'a -> 'b -> 'c -let concat_bv l r = of_bits (bits_of l ++ bits_of r) +val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU +let concat_bv l r = (bits_of l ++ bits_of r) -val cons_bv : forall 'a 'b 'c. Bitvector 'a, Bitvector 'b => bitU -> 'a -> 'b -let cons_bv b v = of_bits (b :: bits_of v) +val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU +let cons_bv b v = b :: bits_of v -let bool_of_bv v = extract_only_element (bits_of v) -let cast_unit_bv b = of_bits [b] -let bv_of_bit len b = of_bits (extz_bits len [b]) -let int_of_bv sign = if sign then signed else unsigned +val cast_unit_bv : bitU -> list bitU +let cast_unit_bv b = [b] + +val bv_of_bit : integer -> bitU -> list bitU +let bv_of_bit len b = extz_bits len [b] let most_significant v = match bits_of v with | b :: _ -> b - | _ -> failwith "most_significant applied to empty vector" + | _ -> B0 (* Treat empty bitvector as all zeros *) end let get_max_representable_in sign (n : integer) : integer = @@ -36,135 +37,106 @@ let get_min_representable_in _ (n : integer) : integer = else if n = 5 then min_5 else 0 - (integerPow 2 (natFromInteger n)) -val bitwise_binop_bv : forall 'a. Bitvector 'a => - (bool -> bool -> bool) -> 'a -> 'a -> 'a -let bitwise_binop_bv op l r = of_bits (binop_bits op (bits_of l) (bits_of r)) - -let and_bv = bitwise_binop_bv (&&) -let or_bv = bitwise_binop_bv (||) -let xor_bv = bitwise_binop_bv xor -let not_bv v = of_bits (not_bits (bits_of v)) - -val arith_op_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b -let arith_op_bv op sign size l r = - let (l',r') = (int_of_bv sign l, int_of_bv sign r) in - let n = op l' r' in - of_int (size * length l) n - - -let add_bv = arith_op_bv integerAdd false 1 -let sadd_bv = arith_op_bv integerAdd true 1 -let sub_bv = arith_op_bv integerMinus false 1 -let mult_bv = arith_op_bv integerMult false 2 -let smult_bv = arith_op_bv 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_bv_int : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> integer -> 'b -let arith_op_bv_int op sign size l r = - let l' = int_of_bv sign l in - let n = op l' r in - of_int (size * length l) n - -let add_bv_int = arith_op_bv_int integerAdd false 1 -let sadd_bv_int = arith_op_bv_int integerAdd true 1 -let sub_bv_int = arith_op_bv_int integerMinus false 1 -let mult_bv_int = arith_op_bv_int integerMult false 2 -let smult_bv_int = arith_op_bv_int integerMult true 2 - -val arith_op_int_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> integer -> 'a -> 'b -let arith_op_int_bv op sign size l r = - let r' = int_of_bv sign r in - let n = op l r' in - of_int (size * length r) n - -let add_int_bv = arith_op_int_bv integerAdd false 1 -let sadd_int_bv = arith_op_int_bv integerAdd true 1 -let sub_int_bv = arith_op_int_bv integerMinus false 1 -let mult_int_bv = arith_op_int_bv integerMult false 2 -let smult_int_bv = arith_op_int_bv integerMult true 2 - -let arith_op_bv_bit op sign (size : integer) l r = - let l' = int_of_bv sign l in - let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in - of_int (size * length l) n - -let add_bv_bit = arith_op_bv_bit integerAdd false 1 -let sadd_bv_bit = arith_op_bv_bit integerAdd true 1 -let sub_bv_bit = arith_op_bv_bit integerMinus true 1 - -val arith_op_overflow_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> ('b * bitU * bitU) +val arith_op_bv_int : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a +let arith_op_bv_int op sign l r = + let r' = of_int (length l) r in + arith_op_bv op sign l r' + +val arith_op_int_bv : forall 'a 'b. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a +let arith_op_int_bv op sign l r = + let l' = of_int (length r) l in + arith_op_bv op sign l' r + +let arith_op_bv_bool op sign l r = arith_op_bv_int op sign l (if r then 1 else 0) +let arith_op_bv_bit op sign l r = Maybe.map (arith_op_bv_bool op sign l) (bool_of_bitU r) + +(* TODO (or just omit and define it per spec if needed) +val arith_op_overflow_bv : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU) let arith_op_overflow_bv op sign size l r = let len = length l in let act_size = len * size in - let (l_sign,r_sign) = (int_of_bv sign l,int_of_bv sign r) in - let (l_unsign,r_unsign) = (int_of_bv false l,int_of_bv false r) in - let n = op l_sign r_sign in - let n_unsign = op l_unsign r_unsign in - let correct_size = 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,overflow,c_out) + match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with + | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) -> + let n = op l_sign r_sign in + let n_unsign = op l_unsign r_unsign in + let correct_size = 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,overflow,c_out) + | (_, _, _, _) -> + (repeat [BU] act_size, BU, BU) + end let add_overflow_bv = arith_op_overflow_bv integerAdd false 1 -let add_overflow_bv_signed = arith_op_overflow_bv integerAdd true 1 +let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1 let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1 -let sub_overflow_bv_signed = arith_op_overflow_bv integerMinus true 1 +let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1 let mult_overflow_bv = arith_op_overflow_bv integerMult false 2 -let mult_overflow_bv_signed = arith_op_overflow_bv integerMult true 2 +let mults_overflow_bv = arith_op_overflow_bv integerMult true 2 -val arith_op_overflow_bv_bit : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> ('b * bitU * bitU) +val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a => + (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU) let arith_op_overflow_bv_bit op sign size l r_bit = let act_size = length l * size in - let l' = int_of_bv sign l in - let l_u = int_of_bv 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_bv_bit applied to undefined bit" - end in - let correct_size = 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,overflow,most_significant one_larger) + match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with + | (Just l', Just l_u, false) -> + let (n, nu, changed) = match r_bit with + | B1 -> (op l' 1, op l_u 1, true) + | B0 -> (l', l_u, false) + | BU -> (* unreachable due to check above *) + failwith "arith_op_overflow_bv_bit applied to undefined bit" + end in + let correct_size = 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, overflow, most_significant one_larger) + | (_, _, _) -> + (repeat [BU] act_size, BU, BU) + end let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1 -let add_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerAdd true 1 +let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1 let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1 -let sub_overflow_bv_bit_signed = arith_op_overflow_bv_bit integerMinus true 1 +let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*) type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot -val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> 'a +let invert_shift = function + | LL_shift -> RR_shift + | RR_shift -> LL_shift + | RR_shift_arith -> LL_shift + | LL_rot -> RR_rot + | RR_rot -> LL_rot +end + +val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU let shift_op_bv op v n = + let v = bits_of v in + if n = 0 then v else + let (op, n) = if n > 0 then (op, n) else (invert_shift op, ~n) in match op with | LL_shift -> - of_bits (get_bits true v n (length v - 1) ++ repeat [B0] n) + subrange_list 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)) + repeat [B0] n ++ subrange_list true v 0 (length v - n - 1) | RR_shift_arith -> - of_bits (repeat [most_significant v] n ++ get_bits true v 0 (length v - n - 1)) + repeat [most_significant v] n ++ subrange_list 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)) + subrange_list true v n (length v - 1) ++ subrange_list true v 0 (n - 1) | RR_rot -> - of_bits (get_bits false v 0 (n - 1) ++ get_bits false v n (length v - 1)) + subrange_list false v 0 (n - 1) ++ subrange_list false v n (length v - 1) end let shiftl_bv = shift_op_bv LL_shift (*"<<"*) @@ -173,10 +145,11 @@ let arith_shiftr_bv = shift_op_bv RR_shift_arith let rotl_bv = shift_op_bv LL_rot (*"<<<"*) let rotr_bv = shift_op_bv LL_rot (*">>>"*) -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 shiftl_mword w n = Machine_word.shiftLeft w (nat_of_int n) +let shiftr_mword w n = Machine_word.shiftRight w (nat_of_int n) +let arith_shiftr_mword w n = Machine_word.arithShiftRight w (nat_of_int n) +let rotl_mword w n = Machine_word.rotateLeft (nat_of_int n) w +let rotr_mword w n = Machine_word.rotateRight (nat_of_int n) w let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 @@ -184,27 +157,19 @@ let rec arith_op_no0 (op : integer -> integer -> integer) l r = else Just (op l r) val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b => - (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> 'b + (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b let arith_op_bv_no0 op sign size l r = - let act_size = length l * size in - let (l',r') = (int_of_bv sign l,int_of_bv 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 (of_int act_size n') else (of_bits (repeat [BU] act_size)) + Maybe.bind (int_of_bv sign l) (fun l' -> + Maybe.bind (int_of_bv sign r) (fun r' -> + if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r')))) let mod_bv = arith_op_bv_no0 hardware_mod false 1 let quot_bv = arith_op_bv_no0 hardware_quot false 1 -let quot_bv_signed = arith_op_bv_no0 hardware_quot true 1 +let quots_bv = arith_op_bv_no0 hardware_quot true 1 let mod_mword = Machine_word.modulo let quot_mword = Machine_word.unsignedDivide -let quot_mword_signed = Machine_word.signedDivide +let quots_mword = Machine_word.signedDivide let arith_op_bv_int_no0 op sign size l r = arith_op_bv_no0 op sign size l (of_int (length l) r) @@ -212,26 +177,49 @@ let arith_op_bv_int_no0 op sign size l r = let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1 let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1 -let replicate_bits_bv v count = of_bits (repeat (bits_of v) count) +let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r) +let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r) +let quots_mword_int l r = Machine_word.signedDivide l (wordFromInteger r) + +let replicate_bits_bv v count = repeat (bits_of v) count let duplicate_bit_bv bit len = replicate_bits_bv [bit] len val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let eq_bv l r = (unsigned l = unsigned r) +let eq_bv l r = (bits_of l = bits_of r) + +let eq_mword l r = (l = r) val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let neq_bv l r = (unsigned l <> unsigned r) - -val ucmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool -let ucmp_bv cmp l r = cmp (unsigned l) (unsigned r) - -val scmp_bv : forall 'a. Bitvector 'a => (integer -> integer -> bool) -> 'a -> 'a -> bool -let scmp_bv cmp l r = cmp (signed l) (signed r) - -let ult_bv = ucmp_bv (<) -let slt_bv = scmp_bv (<) -let ugt_bv = ucmp_bv (>) -let sgt_bv = scmp_bv (>) -let ulteq_bv = ucmp_bv (<=) -let slteq_bv = scmp_bv (<=) -let ugteq_bv = ucmp_bv (>=) -let sgteq_bv = scmp_bv (>=) +let neq_bv l r = not (eq_bv l r) + +let neq_mword l r = (l <> r) + +val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r)) +let ulteq_bv l r = (eq_bv l r) || (ult_bv l r) +let ugt_bv l r = not (ulteq_bv l r) +let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r) + +val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool +let slt_bv l r = + match (most_significant l, most_significant r) with + | (B0, B0) -> ult_bv l r + | (B0, B1) -> false + | (B1, B0) -> true + | (B1, B1) -> + let l' = add_one_bit_ignore_overflow (bits_of l) in + let r' = add_one_bit_ignore_overflow (bits_of r) in + ugt_bv l' r' + | (BU, BU) -> ult_bv l r + | (BU, _) -> true + | (_, BU) -> false + end +let slteq_bv l r = (eq_bv l r) || (slt_bv l r) +let sgt_bv l r = not (slteq_bv l r) +let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r) + +val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool +let ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r) + +val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool +let scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) |