Add unchecked/SIMD bitshift checks and disable CBMC flag (#2630)

Co-authored-by: Celina G. Val <celinval@amazon.com>
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

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 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.
     ///

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,

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/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);
+}

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)