Add out of bounds check for offset intrinsics

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -38,7 +38,7 @@ pub enum PropertyClass {
     /// Overflow panics that can be generated by Intrisics.
     /// NOTE: Not all uses of this are found by rust-analyzer because of the use of macros. Try grep instead.
     ///
-    /// SPECIAL BEHAVIOR: None TODO: Why should this exist?
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck.
     ArithmeticOverflow,
     /// The Rust `assume` instrinsic is `assert`'d by Kani, and gets this property class.
     ///
@@ -67,13 +67,13 @@ pub enum PropertyClass {
     /// That is, they do not depend on special instrumentation that Kani performs that wouldn't
     /// otherwise be observable.
     Assertion,
-    /// Another instrinsic check.
+    /// Another intrinsic check.
     ///
-    /// SPECIAL BEHAVIOR: None TODO: Why should this exist?
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck
     ExactDiv,
-    /// Another instrinsic check.
+    /// Another intrinsic check.
     ///
-    /// SPECIAL BEHAVIOR: None TODO: Why should this exist?
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck
     FiniteCheck,
     /// Checks added by Kani compiler to determine whether a property (e.g.
     /// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable
@@ -82,6 +82,7 @@ pub enum PropertyClass {
     /// E.g., things that trigger UB or unstable behavior.
     ///
     /// SPECIAL BEHAVIOR: Assertions that may not exist when running code normally (i.e. not under Kani)
+    /// This is not caught by `#[should_panic]`.
     SafetyCheck,
     /// Checks to ensure that Kani's code generation is correct.
     ///

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -1015,7 +1015,7 @@ impl GotocCtx<'_> {
     ///
     /// This function handles code generation for the `arith_offset` intrinsic.
     ///     <https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html>
-    /// According to the documenation, the operation is always safe.
+    /// According to the documentation, the operation is always safe.
     fn codegen_arith_offset(&mut self, mut fargs: Vec<Expr>, p: &Place, loc: Location) -> Stmt {
         let src_ptr = fargs.remove(0);
         let offset = fargs.remove(0);

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -356,7 +356,7 @@ impl GotocCtx<'_> {
 
     fn codegen_rvalue_binary_op(
         &mut self,
-        ty: Ty,
+        _ty: Ty,
         op: &BinOp,
         e1: &Operand,
         e2: &Operand,
@@ -405,42 +405,15 @@ impl GotocCtx<'_> {
             }
             // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
             BinOp::Offset => {
+                // We don't need to check for UB since we handled user calls of offset already
+                // via rustc_intrinsic transformation pass.
+                //
+                // This operation may still be used by other Kani instrumentation which should
+                // ensure safety.
+                // We should consider adding sanity checks if `debug_assertions` are enabled.
                 let ce1 = self.codegen_operand_stable(e1);
                 let ce2 = self.codegen_operand_stable(e2);
-
-                // Check that computing `offset` in bytes would not overflow
-                let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
-                    ce2.clone().cast_to(Type::ssize_t()),
-                    pointee_type_stable(ty).unwrap(),
-                    Type::ssize_t(),
-                    "offset",
-                    loc,
-                );
-
-                // Check that the computation would not overflow an `isize` which is UB:
-                // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
-                // These checks may allow a wrapping-around behavior in CBMC:
-                // https://github.com/model-checking/kani/issues/1150
-                // Note(std): We don't check that the starting or resulting pointer stay
-                // within bounds of the object they point to. Doing so causes spurious
-                // failures due to the usage of these intrinsics in the standard library.
-                // See <https://github.com/model-checking/kani/issues/1233> for more details.
-                // Note that this is one of the safety conditions for `offset`:
-                // <https://doc.rust-lang.org/std/primitive.pointer.html#safety-2>
-
-                let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes);
-                let overflow_check = self.codegen_assert_assume(
-                    overflow_res.overflowed.not(),
-                    PropertyClass::ArithmeticOverflow,
-                    "attempt to compute offset which would overflow",
-                    loc,
-                );
-                let res = ce1.clone().plus(ce2);
-                Expr::statement_expression(
-                    vec![bytes_overflow_check, overflow_check, res.as_stmt(loc)],
-                    ce1.typ().clone(),
-                    loc,
-                )
+                ce1.clone().plus(ce2)
             }
         }
     }

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -134,22 +134,36 @@ impl GotocHook for Assert {
 
         let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);
 
-        // Since `cond` might have side effects, assign it to a temporary
-        // variable so that it's evaluated once, then assert and assume it
-        // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
-        let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
         Stmt::block(
             vec![
                 reach_stmt,
-                decl,
-                gcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc),
+                gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
         )
     }
 }
 
+struct UnsupportedCheck;
+impl GotocHook for UnsupportedCheck {
+    fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        check_hook(PropertyClass::UnsupportedConstruct, gcx, fargs, target, span)
+    }
+}
+
 struct SafetyCheck;
 impl GotocHook for SafetyCheck {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
@@ -160,24 +174,12 @@ impl GotocHook for SafetyCheck {
         &self,
         gcx: &mut GotocCtx,
         _instance: Instance,
-        mut fargs: Vec<Expr>,
+        fargs: Vec<Expr>,
         _assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 2);
-        let cond = fargs.remove(0).cast_to(Type::bool());
-        let msg = fargs.remove(0);
-        let msg = gcx.extract_const_message(&msg).unwrap();
-        let target = target.unwrap();
-        let caller_loc = gcx.codegen_caller_span_stable(span);
-        Stmt::block(
-            vec![
-                gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
-                Stmt::goto(bb_label(target), caller_loc),
-            ],
-            caller_loc,
-        )
+        check_hook(PropertyClass::SafetyCheck, gcx, fargs, target, span)
     }
 }
 
@@ -205,10 +207,15 @@ impl GotocHook for Check {
 
         let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);
 
+        // Since `cond` might have side effects, assign it to a temporary
+        // variable so that it's evaluated once, then assert and assume it
+        // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
+        let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
         Stmt::block(
             vec![
                 reach_stmt,
-                gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc),
+                decl,
+                gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
@@ -709,6 +716,7 @@ pub fn fn_hooks() -> GotocHooks {
         (KaniHook::IsAllocated, Rc::new(IsAllocated)),
         (KaniHook::PointerObject, Rc::new(PointerObject)),
         (KaniHook::PointerOffset, Rc::new(PointerOffset)),
+        (KaniHook::UnsupportedCheck, Rc::new(UnsupportedCheck)),
         (KaniHook::UntrackedDeref, Rc::new(UntrackedDeref)),
         (KaniHook::InitContracts, Rc::new(InitContracts)),
         (KaniHook::FloatToIntInRange, Rc::new(FloatToIntInRange)),
@@ -747,3 +755,25 @@ impl GotocHooks {
         }
     }
 }
+
+fn check_hook(
+    prop_class: PropertyClass,
+    gcx: &mut GotocCtx,
+    mut fargs: Vec<Expr>,
+    target: Option<BasicBlockIdx>,
+    span: Span,
+) -> Stmt {
+    assert_eq!(fargs.len(), 2);
+    let msg = fargs.pop().unwrap();
+    let cond = fargs.pop().unwrap().cast_to(Type::bool());
+    let msg = gcx.extract_const_message(&msg).unwrap();
+    let target = target.unwrap();
+    let caller_loc = gcx.codegen_caller_span_stable(span);
+    Stmt::block(
+        vec![
+            gcx.codegen_assert_assume(cond, prop_class, &msg, caller_loc),
+            Stmt::goto(bb_label(target), caller_loc),
+        ],
+        caller_loc,
+    )
+}

kani-compiler/src/kani_middle/kani_functions.rs

@@ -81,6 +81,8 @@ pub enum KaniModel {
     IsSliceChunkPtrInitialized,
     #[strum(serialize = "IsSlicePtrInitializedModel")]
     IsSlicePtrInitialized,
+    #[strum(serialize = "OffsetModel")]
+    Offset,
     #[strum(serialize = "RunContractModel")]
     RunContract,
     #[strum(serialize = "RunLoopContractModel")]
@@ -140,6 +142,8 @@ pub enum KaniHook {
     PointerOffset,
     #[strum(serialize = "SafetyCheckHook")]
     SafetyCheck,
+    #[strum(serialize = "UnsupportedCheckHook")]
+    UnsupportedCheck,
     #[strum(serialize = "UntrackedDerefHook")]
     UntrackedDeref,
 }

kani-compiler/src/kani_middle/transform/body.rs

@@ -434,6 +434,11 @@ impl MutableBody {
     ) {
         self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term;
     }
+
+    /// Remove the given statement.
+    pub fn remove_stmt(&mut self, bb: BasicBlockIdx, stmt: usize) {
+        self.blocks[bb].statements.remove(stmt);
+    }
 }
 
 // TODO: Remove this enum, since we now only support kani's assert.