diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index af06c456a7b6..0f4279a97a14 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 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(); + 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 distance_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 distance_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 distance_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![excessive_check_stmt, negative_check_stmt, expr_place], loc) + } else { + Stmt::block(vec![excessive_check_stmt, expr_place], loc) + } + } + /// `simd_shuffle` constructs a new vector from the elements of two input /// vectors, choosing values according to an input array of indexes. /// diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 88a2f3cd4a2c..bfb3313a5ae9 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,39 @@ 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, + ); + + 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, + "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, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 96770d562e79..cd87e13782e9 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 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/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); +} 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)