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. TODO: Replace this with `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. TODO: Replace this with `SafetyCheck`.
     ExactDiv,
-    /// Another instrinsic check.
+    /// Another intrinsic check.
     ///
-    /// SPECIAL BEHAVIOR: None TODO: Why should this exist?
+    /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `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,15 +134,46 @@ 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,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        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,
+                    PropertyClass::UnsupportedConstruct,
+                    &msg,
+                    caller_loc,
+                ),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
@@ -166,8 +197,8 @@ impl GotocHook for SafetyCheck {
         span: Span,
     ) -> Stmt {
         assert_eq!(fargs.len(), 2);
-        let cond = fargs.remove(0).cast_to(Type::bool());
-        let msg = fargs.remove(0);
+        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);
@@ -181,6 +212,7 @@ impl GotocHook for SafetyCheck {
     }
 }
 
+// TODO: Remove this and replace occurrences with `SanityCheck`.
 struct Check;
 impl GotocHook for Check {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
@@ -709,6 +741,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)),

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.

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

@@ -8,13 +8,21 @@
 
 use crate::intrinsics::Intrinsic;
 use crate::kani_middle::kani_functions::{KaniFunction, KaniModel};
-use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
+use crate::kani_middle::transform::body::{
+    InsertPosition, MutMirVisitor, MutableBody, SourceInstruction,
+};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
-use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
+use stable_mir::mir::{
+    BasicBlockIdx, BinOp, Body, ConstOperand, LocalDecl, Operand, Rvalue, StatementKind,
+    Terminator, TerminatorKind,
+};
+use stable_mir::ty::{
+    FnDef, GenericArgKind, GenericArgs, IntTy, MirConst, RigidTy, Span, Ty, TyKind, UintTy,
+};
 use std::collections::HashMap;
 use tracing::debug;
 
@@ -42,12 +50,14 @@ impl TransformPass for RustcIntrinsicsPass {
 
     /// Transform the function body by inserting checks one-by-one.
     /// For every unsafe dereference or a transmute operation, we check all values are valid.
-    fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+    fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
         debug!(function=?instance.name(), "transform");
         let mut new_body = MutableBody::from(body);
-        let mut visitor = ReplaceIntrinsicVisitor::new(&self.models, new_body.locals().to_vec());
+        let mut visitor =
+            ReplaceIntrinsicCallVisitor::new(&self.models, new_body.locals().to_vec());
         visitor.visit_body(&mut new_body);
-        (visitor.changed, new_body.into())
+        let changed = self.replace_lowered_intrinsics(tcx, &mut new_body);
+        (visitor.changed || changed, new_body.into())
     }
 }
 
@@ -63,21 +73,78 @@ impl RustcIntrinsicsPass {
         debug!(?models, "RustcIntrinsicsPass::new");
         RustcIntrinsicsPass { models }
     }
+
+    /// This function checks if we need to replace intrinsics that have been lowered.
+    fn replace_lowered_intrinsics(&self, tcx: TyCtxt, body: &mut MutableBody) -> bool {
+        // Do a reverse iteration on the instructions since we will replace Rvalues by a function
+        // call, which will split the basic block.
+        let mut changed = false;
+        let orig_bbs = body.blocks().len();
+        for bb in (0..orig_bbs).rev() {
+            let num_stmts = body.blocks()[bb].statements.len();
+            for stmt in (0..num_stmts).rev() {
+                changed |= self.replace_offset(tcx, body, bb, stmt);
+            }
+        }
+        changed
+    }
+
+    /// Replace a lowered offset intrinsic.
+    fn replace_offset(
+        &self,
+        tcx: TyCtxt,
+        body: &mut MutableBody,
+        bb: BasicBlockIdx,
+        stmt: usize,
+    ) -> bool {
+        let statement = &body.blocks()[bb].statements[stmt];
+        let StatementKind::Assign(place, rvalue) = &statement.kind else {
+            return false;
+        };
+        let Rvalue::BinaryOp(BinOp::Offset, op1, op2) = rvalue else { return false };
+        let mut source = SourceInstruction::Statement { idx: stmt, bb };
+
+        // Double check input parameters of `offset` operation.
+        let offset_ty = op2.ty(body.locals()).unwrap();
+        let pointer_ty = op1.ty(body.locals()).unwrap();
+        validate_offset(tcx, offset_ty, statement.span);
+        validate_raw_ptr(tcx, pointer_ty, statement.span);
+        tcx.dcx().abort_if_errors();
+
+        let pointee_ty = pointer_ty.kind().builtin_deref(true).unwrap().ty;
+        // The model takes the following parameters (PointeeType, PointerType, OffsetType).
+        let model = self.models[&KaniModel::Offset];
+        let params = vec![
+            GenericArgKind::Type(pointee_ty),
+            GenericArgKind::Type(pointer_ty),
+            GenericArgKind::Type(offset_ty),
+        ];
+        let instance = Instance::resolve(model, &GenericArgs(params)).unwrap();
+        body.insert_call(
+            &instance,
+            &mut source,
+            InsertPosition::After,
+            vec![op1.clone(), op2.clone()],
+            place.clone(),
+        );
+        body.remove_stmt(bb, stmt);
+        true
+    }
 }
 
-struct ReplaceIntrinsicVisitor<'a> {
+struct ReplaceIntrinsicCallVisitor<'a> {
     models: &'a HashMap<KaniModel, FnDef>,
     locals: Vec<LocalDecl>,
     changed: bool,
 }
 
-impl<'a> ReplaceIntrinsicVisitor<'a> {
+impl<'a> ReplaceIntrinsicCallVisitor<'a> {
     fn new(models: &'a HashMap<KaniModel, FnDef>, locals: Vec<LocalDecl>) -> Self {
-        ReplaceIntrinsicVisitor { models, locals, changed: false }
+        ReplaceIntrinsicCallVisitor { models, locals, changed: false }
     }
 }
 
-impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> {
+impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> {
     /// Replace the terminator for some rustc's intrinsics.
     ///
     /// In some cases, we replace a function call to a rustc intrinsic by a call to the
@@ -117,3 +184,33 @@ impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> {
         self.super_terminator(term);
     }
 }
+
+/// Validate whether the offset type is valid, i.e., `isize` or `usize`.
+///
+/// This will emit an error if the type is wrong but not abort.
+/// Invoke `tcx.dcx().abort_if_errors()` to abort execution.
+fn validate_offset(tcx: TyCtxt, offset_ty: Ty, span: Span) {
+    if !matches!(
+        offset_ty.kind(),
+        TyKind::RigidTy(RigidTy::Int(IntTy::Isize)) | TyKind::RigidTy(RigidTy::Uint(UintTy::Usize))
+    ) {
+        tcx.dcx().span_err(
+            rustc_internal::internal(tcx, span),
+            format!("Expected `isize` or `usize` for offset type. Found `{offset_ty}` instead"),
+        );
+    }
+}
+
+/// Validate that we have a raw pointer otherwise emit an error.
+///
+/// This will emit an error if the type is wrong but not abort.
+/// Invoke `tcx.dcx().abort_if_errors()` to abort execution.
+fn validate_raw_ptr(tcx: TyCtxt, ptr_ty: Ty, span: Span) {
+    let pointer_ty_kind = ptr_ty.kind();
+    if !pointer_ty_kind.is_raw_ptr() {
+        tcx.dcx().span_err(
+            rustc_internal::internal(tcx, span),
+            format!("Expected raw pointer for pointer type. Found `{ptr_ty}` instead"),
+        );
+    }
+}

library/kani_core/src/lib.rs

@@ -308,6 +308,20 @@ macro_rules! kani_intrinsics {
             assert!(cond, "Safety check failed: {msg}");
         }
 
+        /// This should indicate that Kani does not support a certain operation.
+        #[doc(hidden)]
+        #[allow(dead_code)]
+        #[kanitool::fn_marker = "UnsupportedCheckHook"]
+        #[inline(never)]
+        #[allow(clippy::diverging_sub_expression)]
+        pub(crate) fn unsupported(msg: &'static str) -> ! {
+            #[cfg(not(feature = "concrete_playback"))]
+            return kani_intrinsic();
+
+            #[cfg(feature = "concrete_playback")]
+            unimplemented!("Unsupported Kani operation: {msg}")
+        }
+
         /// An empty body that can be used to define Kani intrinsic functions.
         ///
         /// A Kani intrinsic is a function that is interpreted by Kani compiler.