Add unchecked/SIMD bitshift checks and disable CBMC flag

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.
  // <https://github.com/model-checking/kani/issues/1970>
  "simd_rem" => codegen_intrinsic_binop!(rem),
- // TODO: `simd_shl` and `simd_shr` don't check overflow cases.
- // <https://github.com/model-checking/kani/issues/1963>
- "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<Expr>,
+ 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.
  ///

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,

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

tests/expected/intrinsics/simd-shl-shift-negative/expected

@@ -1,2 +1,2 @@
 FAILURE\
-shift distance is negative
+attempt simd_shl with negative shift distance

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);

tests/expected/intrinsics/simd-shl-shift-too-large/expected

@@ -1,2 +1,2 @@
 FAILURE\
-shift distance too large
+attempt simd_shl with excessive shift distance

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);

tests/expected/intrinsics/simd-shr-shift-negative/expected

@@ -1,2 +1,2 @@
 FAILURE\
-shift distance is negative
+attempt simd_shr with negative shift distance

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);

tests/expected/intrinsics/simd-shr-shift-too-large/expected

@@ -1,2 +1,2 @@
 FAILURE\
-shift distance too large
+attempt simd_shr with excessive shift distance

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);

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);

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

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)