From 50be9abdb9f5c2d00e9733dfeb1d79327122d060 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Sun, 23 Jul 2023 00:34:51 -0500 Subject: [PATCH 1/7] Implement unchecked shift checks in Kani --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 55 +++++++++++++++++-- 1 file changed, 50 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 22b26a3489b4..85885c2e65ce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -116,6 +116,14 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::BitXor => ce1.bitxor(ce2), BinOp::Div => ce1.div(ce2), BinOp::Rem => ce1.rem(ce2), + BinOp::ShlUnchecked => ce1.shl(ce2), + BinOp::ShrUnchecked => { + if self.operand_ty(e1).is_signed() { + ce1.ashr(ce2) + } else { + ce1.lshr(ce2) + } + } _ => unreachable!("Unexpected {:?}", op), } } @@ -343,11 +351,14 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => { self.codegen_scalar_binop(op, e1, e2) } - // We currently rely on CBMC's UB checks for shift which isn't always accurate. - // We should implement the checks ourselves. - // See https://github.com/model-checking/kani/issues/2374 - BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2), - BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2), + BinOp::ShlUnchecked | BinOp::ShrUnchecked => { + let result = self.codegen_unchecked_scalar_binop(op, e1, e2); + let check = self.check_unchecked_shift_distance(e1, e2, loc); + Expr::statement_expression( + vec![check, result.clone().as_stmt(loc)], + result.typ().clone(), + ) + } BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => { self.codegen_binop_with_overflow_check(op, e1, e2, loc) } @@ -455,6 +466,40 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Check for valid unchecked shift distance. + /// Shifts on an integer of type T are UB if shift distance < 0 or >= T::BITS. + fn check_unchecked_shift_distance( + &mut self, + value: &Operand<'tcx>, + distance: &Operand<'tcx>, + loc: Location, + ) -> Stmt { + let value_expr = self.codegen_operand(value); + let distance_expr = self.codegen_operand(distance); + let value_width = value_expr.typ().sizeof_in_bits(&self.symbol_table); + let value_width_expr = Expr::int_constant(value_width, distance_expr.typ().clone()); + + let excessive_distance_check = self.codegen_assert_assume( + distance_expr.clone().lt(value_width_expr), + PropertyClass::ArithmeticOverflow, + "attempt to shift by excessive shift distance", + loc, + ); + + // The first argument to the shift intrinsics determines the types of both arguments + if value_expr.typ().is_signed(self.symbol_table.machine_model()) { + let negative_distance_check = self.codegen_assert_assume( + distance_expr.is_non_negative(), + PropertyClass::ArithmeticOverflow, + "attempt to shift by negative distance", + loc, + ); + Stmt::block(vec![negative_distance_check, excessive_distance_check], loc) + } else { + excessive_distance_check + } + } + /// Create an initializer for a generator struct. fn codegen_rvalue_generator( &mut self, From eefab8151f5b9bc1b36e178f0a8d44ffe60843e7 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Sun, 23 Jul 2023 13:48:56 -0500 Subject: [PATCH 2/7] Add overflow checks for simd shift intrinsics --- .../codegen/intrinsic.rs | 81 ++++++++++++++++--- 1 file changed, 71 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4bd5566f9d7c..a8c0c44bbb3e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -538,16 +538,8 @@ impl<'tcx> GotocCtx<'tcx> { // TODO: `simd_div` and `simd_rem` don't check for overflow cases. // "simd_rem" => codegen_intrinsic_binop!(rem), - // TODO: `simd_shl` and `simd_shr` don't check overflow cases. - // - "simd_shl" => codegen_intrinsic_binop!(shl), - "simd_shr" => { - if fargs[0].typ().base_type().unwrap().is_signed(self.symbol_table.machine_model()) - { - codegen_intrinsic_binop!(ashr) - } else { - codegen_intrinsic_binop!(lshr) - } + "simd_shl" | "simd_shr" => { + self.codegen_simd_shift_with_distance_check(fargs, intrinsic, p, loc) } // "simd_shuffle#" => handled in an `if` preceding this match "simd_sub" => self.codegen_simd_op_with_overflow( @@ -1560,6 +1552,75 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(vec![expr_place, check_stmt], loc) } + /// Intrinsics which encode a SIMD bitshift. + /// Also checks for valid shift distance. Shifts on an integer of type T are UB if shift + /// distance < 0 or >= T::BITS. + fn codegen_simd_shift_with_distance_check( + &mut self, + mut fargs: Vec, + intrinsic: &str, + p: &Place<'tcx>, + loc: Location, + ) -> Stmt { + let values = fargs.remove(0); + let distances = fargs.remove(0); + + let values_len = values.typ().len().unwrap(); + let distances_len = distances.typ().len().unwrap(); + assert_eq!(values_len, distances_len, "expected same length vectors"); + + let value_type = values.typ().base_type().unwrap(); + let distance_type = distances.typ().base_type().unwrap(); + let value_width = value_type.sizeof_in_bits(&self.symbol_table); + let value_width_expr = Expr::int_constant(value_width, distance_type.clone()); + let value_is_signed = value_type.is_signed(self.symbol_table.machine_model()); + + let mut excessive_check = Expr::bool_false(); + let mut negative_check = Expr::bool_false(); + for i in 0..distances_len { + let index = Expr::int_constant(i, Type::ssize_t()); + let distance = distances.clone().index_array(index); + let excessive_distance_cond = distance.clone().ge(value_width_expr.clone()); + excessive_check = excessive_check.or(excessive_distance_cond); + if value_is_signed { + let negative_distance_cond = distance.is_negative(); + negative_check = negative_check.or(negative_distance_cond); + } + } + let excessive_check_stmt = self.codegen_assert_assume( + excessive_check.not(), + PropertyClass::ArithmeticOverflow, + format!("attempt {intrinsic} with excessive shift distance").as_str(), + loc, + ); + + let op_fun = match intrinsic { + "simd_shl" => Expr::shl, + "simd_shr" => { + if value_is_signed { + Expr::ashr + } else { + Expr::lshr + } + } + _ => unreachable!("expected a simd shift intrinsic"), + }; + let res = op_fun(values, distances); + let expr_place = self.codegen_expr_to_place(p, res); + + if value_is_signed { + let negative_check_stmt = self.codegen_assert_assume( + negative_check.not(), + PropertyClass::ArithmeticOverflow, + format!("attempt {intrinsic} with negative shift distance").as_str(), + loc, + ); + Stmt::block(vec![expr_place, excessive_check_stmt, negative_check_stmt], loc) + } else { + Stmt::block(vec![expr_place, excessive_check_stmt], loc) + } + } + /// `simd_shuffle` constructs a new vector from the elements of two input /// vectors, choosing values according to an input array of indexes. /// From a567e688d0b9ea32bebfa8eeac978b57dd0fb8f2 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Sun, 23 Jul 2023 21:22:17 -0500 Subject: [PATCH 3/7] Remove CBMC undefined-shift-check flag Checks are now implemented in Kani --- kani-driver/src/call_cbmc.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index daddfdf62f1c..14ac3f8721fa 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -167,7 +167,6 @@ impl KaniSession { args.push("--div-by-zero-check".into()); args.push("--float-overflow-check".into()); args.push("--nan-check".into()); - args.push("--undefined-shift-check".into()); // With PR #647 we use Rust's `-C overflow-checks=on` instead of: // --unsigned-overflow-check // --signed-overflow-check From 949ee7856d292bd0c027fdd9beb41c24be4805c0 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Sun, 23 Jul 2023 14:06:23 -0500 Subject: [PATCH 4/7] Fix/update tests Remove tests for shifting a negative value as that is not UB in rust. --- .../simd-shl-operand-negative/expected | 2 -- .../simd-shl-operand-negative/main.rs | 27 ------------------- .../simd-shl-shift-negative/expected | 2 +- .../simd-shl-shift-negative/main.rs | 1 - .../simd-shl-shift-too-large/expected | 2 +- .../simd-shl-shift-too-large/main.rs | 1 - .../simd-shr-shift-negative/expected | 2 +- .../simd-shr-shift-negative/main.rs | 1 - .../simd-shr-shift-too-large/expected | 2 +- .../simd-shr-shift-too-large/main.rs | 1 - .../Intrinsics/SIMD/Operators/bitshift.rs | 1 - tests/ui/cbmc_checks/signed-overflow/expected | 1 - .../unexpected-failures/expected | 6 ++--- 13 files changed, 7 insertions(+), 42 deletions(-) delete mode 100644 tests/expected/intrinsics/simd-shl-operand-negative/expected delete mode 100644 tests/expected/intrinsics/simd-shl-operand-negative/main.rs diff --git a/tests/expected/intrinsics/simd-shl-operand-negative/expected b/tests/expected/intrinsics/simd-shl-operand-negative/expected deleted file mode 100644 index b437e2374575..000000000000 --- a/tests/expected/intrinsics/simd-shl-operand-negative/expected +++ /dev/null @@ -1,2 +0,0 @@ -FAILURE\ -shift operand is negative \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shl-operand-negative/main.rs b/tests/expected/intrinsics/simd-shl-operand-negative/main.rs deleted file mode 100644 index 3d7969d8d4b6..000000000000 --- a/tests/expected/intrinsics/simd-shl-operand-negative/main.rs +++ /dev/null @@ -1,27 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Checks that `simd_shl` returns a failure if the operand is negative. -//! Note: The "operand is negative" property isn't checked for `simd_shr`, only -//! for `simd_shl`. -#![feature(repr_simd, platform_intrinsics)] - -#[repr(simd)] -#[allow(non_camel_case_types)] -#[derive(Clone, Copy, PartialEq, Eq)] -pub struct i32x2(i32, i32); - -extern "platform-intrinsic" { - fn simd_shl(x: T, y: T) -> T; -} - -#[kani::proof] -fn test_simd_shl() { - let value = kani::any(); - let values = i32x2(value, value); - let shift = kani::any(); - kani::assume(shift >= 0); - kani::assume(shift < 32); - let shifts = i32x2(shift, shift); - let _result = unsafe { simd_shl(values, shifts) }; -} diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/expected b/tests/expected/intrinsics/simd-shl-shift-negative/expected index 0e4e9fadb811..c3b2e1184e06 100644 --- a/tests/expected/intrinsics/simd-shl-shift-negative/expected +++ b/tests/expected/intrinsics/simd-shl-shift-negative/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance is negative \ No newline at end of file +attempt simd_shl with negative shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs index ebde0284a497..0c7116b30567 100644 --- a/tests/expected/intrinsics/simd-shl-shift-negative/main.rs +++ b/tests/expected/intrinsics/simd-shl-shift-negative/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shl() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift < 32); diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/expected b/tests/expected/intrinsics/simd-shl-shift-too-large/expected index 65d41d1518fc..2c50f584f06c 100644 --- a/tests/expected/intrinsics/simd-shl-shift-too-large/expected +++ b/tests/expected/intrinsics/simd-shl-shift-too-large/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance too large \ No newline at end of file +attempt simd_shl with excessive shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs index e7cffe4ebb92..fff9aadf1900 100644 --- a/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs +++ b/tests/expected/intrinsics/simd-shl-shift-too-large/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shl() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift >= 0); diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/expected b/tests/expected/intrinsics/simd-shr-shift-negative/expected index 0e4e9fadb811..49a75a18308e 100644 --- a/tests/expected/intrinsics/simd-shr-shift-negative/expected +++ b/tests/expected/intrinsics/simd-shr-shift-negative/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance is negative \ No newline at end of file +attempt simd_shr with negative shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs index ca8cbbc3e0d7..580f0337db25 100644 --- a/tests/expected/intrinsics/simd-shr-shift-negative/main.rs +++ b/tests/expected/intrinsics/simd-shr-shift-negative/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shr() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift < 32); diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/expected b/tests/expected/intrinsics/simd-shr-shift-too-large/expected index 65d41d1518fc..adc26e269699 100644 --- a/tests/expected/intrinsics/simd-shr-shift-too-large/expected +++ b/tests/expected/intrinsics/simd-shr-shift-too-large/expected @@ -1,2 +1,2 @@ FAILURE\ -shift distance too large \ No newline at end of file +attempt simd_shr with excessive shift distance \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs index 87718ec48553..3d9cd5e0c919 100644 --- a/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs +++ b/tests/expected/intrinsics/simd-shr-shift-too-large/main.rs @@ -16,7 +16,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shr() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift >= 0); diff --git a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs index cd2c7ceb756a..1041f918123f 100644 --- a/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs +++ b/tests/kani/Intrinsics/SIMD/Operators/bitshift.rs @@ -23,7 +23,6 @@ extern "platform-intrinsic" { #[kani::proof] fn test_simd_shl() { let value = kani::any(); - kani::assume(value >= 0); let values = i32x2(value, value); let shift = kani::any(); kani::assume(shift >= 0); diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index 143dd683f76f..70669b325e9e 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -8,4 +8,3 @@ Failed Checks: attempt to calculate the remainder with overflow Failed Checks: attempt to shift left with overflow Failed Checks: attempt to shift right with overflow Failed Checks: arithmetic overflow on signed shl -Failed Checks: shift operand is negative diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected index 6cd10b4bafd5..b3a4cb77c6ae 100644 --- a/tests/ui/should-panic-attribute/unexpected-failures/expected +++ b/tests/ui/should-panic-attribute/unexpected-failures/expected @@ -1,9 +1,9 @@ -undefined-shift\ +arithmetic_overflow\ Status: FAILURE\ -Description: "shift distance too large" +Description: "attempt to shift by excessive shift distance" Failed Checks: panicked on the `1` arm! Failed Checks: panicked on the `0` arm! -Failed Checks: shift distance too large +Failed Checks: attempt to shift by excessive shift distance VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) From 7a875696d4e5379d862409324917fe43e218f735 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Thu, 27 Jul 2023 19:50:13 -0500 Subject: [PATCH 5/7] Fix order of items in `Stmt::block`s Co-authored-by: Celina G. Val --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index a8c0c44bbb3e..7ce95afac37b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1615,9 +1615,9 @@ impl<'tcx> GotocCtx<'tcx> { format!("attempt {intrinsic} with negative shift distance").as_str(), loc, ); - Stmt::block(vec![expr_place, excessive_check_stmt, negative_check_stmt], loc) + Stmt::block(vec![excessive_check_stmt, negative_check_stmt, expr_place], loc) } else { - Stmt::block(vec![expr_place, excessive_check_stmt], loc) + Stmt::block(vec![excessive_check_stmt, expr_place], loc) } } From eb8af252dce7af44342cea2b56d7ece0a7d0c4d0 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Mon, 24 Jul 2023 01:13:17 -0500 Subject: [PATCH 6/7] Use signed-ness of discance rather than value --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 8 ++++---- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 3 +-- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 7ce95afac37b..e651440c4ac3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1573,7 +1573,7 @@ impl<'tcx> GotocCtx<'tcx> { let distance_type = distances.typ().base_type().unwrap(); let value_width = value_type.sizeof_in_bits(&self.symbol_table); let value_width_expr = Expr::int_constant(value_width, distance_type.clone()); - let value_is_signed = value_type.is_signed(self.symbol_table.machine_model()); + let distance_is_signed = distance_type.is_signed(self.symbol_table.machine_model()); let mut excessive_check = Expr::bool_false(); let mut negative_check = Expr::bool_false(); @@ -1582,7 +1582,7 @@ impl<'tcx> GotocCtx<'tcx> { let distance = distances.clone().index_array(index); let excessive_distance_cond = distance.clone().ge(value_width_expr.clone()); excessive_check = excessive_check.or(excessive_distance_cond); - if value_is_signed { + if distance_is_signed { let negative_distance_cond = distance.is_negative(); negative_check = negative_check.or(negative_distance_cond); } @@ -1597,7 +1597,7 @@ impl<'tcx> GotocCtx<'tcx> { let op_fun = match intrinsic { "simd_shl" => Expr::shl, "simd_shr" => { - if value_is_signed { + if distance_is_signed { Expr::ashr } else { Expr::lshr @@ -1608,7 +1608,7 @@ impl<'tcx> GotocCtx<'tcx> { let res = op_fun(values, distances); let expr_place = self.codegen_expr_to_place(p, res); - if value_is_signed { + if distance_is_signed { let negative_check_stmt = self.codegen_assert_assume( negative_check.not(), PropertyClass::ArithmeticOverflow, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 85885c2e65ce..51ca00c68e9a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -486,8 +486,7 @@ impl<'tcx> GotocCtx<'tcx> { loc, ); - // The first argument to the shift intrinsics determines the types of both arguments - if value_expr.typ().is_signed(self.symbol_table.machine_model()) { + if distance_expr.typ().is_signed(self.symbol_table.machine_model()) { let negative_distance_check = self.codegen_assert_assume( distance_expr.is_non_negative(), PropertyClass::ArithmeticOverflow, From bac1926be54b082de80ce7470218ae0baef51270 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Fri, 28 Jul 2023 22:32:12 -0500 Subject: [PATCH 7/7] Test expected results when shifting negative vals --- .../BitwiseShiftOperators/shift_neg_vals.rs | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 tests/kani/BitwiseShiftOperators/shift_neg_vals.rs diff --git a/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs b/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs new file mode 100644 index 000000000000..288698a0fbee --- /dev/null +++ b/tests/kani/BitwiseShiftOperators/shift_neg_vals.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Ensure that shifting negative values yields the expected results. + +#[kani::proof] +#[kani::unwind(5)] +fn sheck_shl() { + let val: i32 = kani::any(); + let dist: u8 = kani::any(); + kani::assume(dist < 32); + assert_eq!(val << dist, val.wrapping_mul(2_i32.wrapping_pow(dist.into()))); +} + +#[kani::proof] +#[kani::unwind(5)] +fn check_shr() { + let val: i32 = kani::any(); + let dist: u8 = kani::any(); + kani::assume(dist < 32); + let result = (val as i64).div_euclid(2_i64.pow(dist.into())); + assert_eq!(val >> dist, result as i32); +}