Add UB checks for ptr_offset_from* intrinsics

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

@@ -7,9 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::{GotocCtx, utils};
 use crate::intrinsics::Intrinsic;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
-use cbmc::goto_program::{
-    ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
-};
+use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::ty::TypingEnv;
 use rustc_middle::ty::layout::ValidityRequirement;
 use rustc_smir::rustc_internal;
@@ -425,10 +423,6 @@ impl GotocCtx<'_> {
             Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi),
             Intrinsic::PrefAlignOf => codegen_intrinsic_const!(),
             Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
-            Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc),
-            Intrinsic::PtrOffsetFromUnsigned => {
-                self.codegen_ptr_offset_from_unsigned(fargs, place, loc)
-            }
             Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
             Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc),
             Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf),
@@ -546,7 +540,10 @@ impl GotocCtx<'_> {
                 assert!(self.place_ty_stable(place).kind().is_unit());
                 self.codegen_write_bytes(fargs, farg_types, loc)
             }
-            Intrinsic::SizeOfVal | Intrinsic::MinAlignOfVal => {
+            Intrinsic::PtrOffsetFrom
+            | Intrinsic::PtrOffsetFromUnsigned
+            | Intrinsic::SizeOfVal
+            | Intrinsic::MinAlignOfVal => {
                 unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str)
             }
             // Unimplemented
@@ -1025,77 +1022,6 @@ impl GotocCtx<'_> {
         self.codegen_expr_to_place_stable(p, dst_ptr, loc)
     }
 
-    /// ptr_offset_from returns the offset between two pointers
-    /// <https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html>
-    fn codegen_ptr_offset_from(&mut self, fargs: Vec<Expr>, p: &Place, loc: Location) -> Stmt {
-        let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs);
-
-        // Check that computing `offset` in bytes would not overflow an `isize`
-        // These checks may allow a wrapping-around behavior in CBMC:
-        // https://github.com/model-checking/kani/issues/1150
-        let overflow_check = self.codegen_assert_assume(
-            offset_overflow.overflowed.not(),
-            PropertyClass::ArithmeticOverflow,
-            "attempt to compute offset in bytes which would overflow an `isize`",
-            loc,
-        );
-
-        let offset_expr = self.codegen_expr_to_place_stable(p, offset_expr, loc);
-        Stmt::block(vec![overflow_check, offset_expr], loc)
-    }
-
-    /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known.
-    /// The logic is similar to `ptr_offset_from` but the return value is a `usize`.
-    /// See <https://github.com/rust-lang/rust/issues/95892> for more details
-    fn codegen_ptr_offset_from_unsigned(
-        &mut self,
-        fargs: Vec<Expr>,
-        p: &Place,
-        loc: Location,
-    ) -> Stmt {
-        let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs);
-
-        // Check that computing `offset` in bytes would not overflow an `isize`
-        // These checks may allow a wrapping-around behavior in CBMC:
-        // https://github.com/model-checking/kani/issues/1150
-        let overflow_check = self.codegen_assert_assume(
-            offset_overflow.overflowed.not(),
-            PropertyClass::ArithmeticOverflow,
-            "attempt to compute offset in bytes which would overflow an `isize`",
-            loc,
-        );
-
-        let non_negative_check = self.codegen_assert_assume(
-            offset_overflow.result.is_non_negative(),
-            PropertyClass::SafetyCheck,
-            "attempt to compute unsigned offset with negative distance",
-            loc,
-        );
-
-        let offset_expr =
-            self.codegen_expr_to_place_stable(p, offset_expr.cast_to(Type::size_t()), loc);
-        Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc)
-    }
-
-    /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers.
-    /// This function implements the common logic between them.
-    fn codegen_ptr_offset_from_expr(
-        &mut self,
-        mut fargs: Vec<Expr>,
-    ) -> (Expr, ArithmeticOverflowResult) {
-        let dst_ptr = fargs.remove(0);
-        let src_ptr = fargs.remove(0);
-
-        // Compute the offset with standard substraction using `isize`
-        let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t());
-        let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t());
-        let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr);
-
-        // Re-compute the offset with standard substraction (no casts this time)
-        let ptr_offset_expr = dst_ptr.sub(src_ptr);
-        (ptr_offset_expr, offset_overflow)
-    }
-
     /// A transmute is a bitcast from the argument type to the return type.
     /// <https://doc.rust-lang.org/std/intrinsics/fn.transmute.html>
     ///

kani-compiler/src/kani_middle/kani_functions.rs

@@ -83,6 +83,10 @@ pub enum KaniModel {
     IsSlicePtrInitialized,
     #[strum(serialize = "OffsetModel")]
     Offset,
+    #[strum(serialize = "PtrOffsetFromModel")]
+    PtrOffsetFrom,
+    #[strum(serialize = "PtrSubPtrModel")]
+    PtrSubPtr,
     #[strum(serialize = "RunContractModel")]
     RunContract,
     #[strum(serialize = "RunLoopContractModel")]

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

@@ -167,6 +167,8 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> {
                     let model = match intrinsic {
                         Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal],
                         Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal],
+                        Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom],
+                        Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr],
                         // The rest is handled in codegen.
                         _ => {
                             return self.super_terminator(term);

kani-driver/src/cbmc_property_renderer.rs

@@ -61,7 +61,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
         ("NaN on /", Some("NaN on division")),
         ("NaN on *", Some("NaN on multiplication")),
     ]);
-    map.insert("pointer", vec![("same object violation", None)]);
     map.insert("pointer_arithmetic", vec![
         ("pointer relation: deallocated dynamic object", None),
         ("pointer relation: dead object", None),

library/kani_core/src/models.rs

@@ -45,6 +45,57 @@ macro_rules! generate_models {
                 }
             }
 
+            /// Implements core::intrinsics::ptr_offfset_from with safety checks in place.
+            ///
+            /// From original documentation:
+            ///
+            /// # Safety
+            ///
+            /// If any of the following conditions are violated, the result is Undefined Behavior:
+            ///
+            /// * `self` and `origin` must either
+            ///
+            ///   * point to the same address, or
+            ///   * both be *derived from* a pointer to the same allocated object,
+            ///     and the memory range between
+            ///     the two pointers must be in bounds of that object.
+            ///
+            /// * The distance between the pointers, in bytes, must be an exact multiple
+            ///   of the size of `T`.
+            ///
+            /// # Panics
+            ///
+            /// This function panics if `T` is a Zero-Sized Type ("ZST").
+            #[kanitool::fn_marker = "PtrOffsetFromModel"]
+            pub unsafe fn ptr_offset_from<T>(ptr1: *const T, ptr2: *const T) -> isize {
+                // This is not a safety condition.
+                kani::assert(core::mem::size_of::<T>() > 0, "Cannot compute offset of a ZST");
+                if ptr1 == ptr2 {
+                    0
+                } else {
+                    kani::safety_check(
+                        kani::mem::same_allocation_internal(ptr1, ptr2),
+                        "Offset result and original pointer should point to the same allocation",
+                    );
+                    // The offset must fit in isize since this represents the same allocation.
+                    let offset_bytes = ptr1.addr().wrapping_sub(ptr2.addr()) as isize;
+                    let t_size = size_of::<T>() as isize;
+                    kani::safety_check(
+                        offset_bytes % t_size == 0,
+                        "Expected the distance between the pointers, in bytes, to be a
+                        multiple of the size of `T`",
+                    );
+                    offset_bytes / t_size
+                }
+            }
+
+            #[kanitool::fn_marker = "PtrSubPtrModel"]
+            pub unsafe fn ptr_sub_ptr<T>(ptr1: *const T, ptr2: *const T) -> usize {
+                let offset = ptr_offset_from(ptr1, ptr2);
+                kani::safety_check(offset >= 0, "Expected non-negative distance between pointers");
+                offset as usize
+            }
+
             /// An offset model that checks UB.
             #[kanitool::fn_marker = "OffsetModel"]
             pub fn offset<T, P: Ptr<T>, O: ToISize>(ptr: P, offset: O) -> P {

tests/expected/arbitrary/ptrs/pointer_inbounds.rs

@@ -9,8 +9,6 @@
 //! Kani will detect the usage of MaybeUninit and fail the verification.
 extern crate kani;
 
-use kani::PointerGenerator;
-
 #[kani::proof]
 fn check_inbounds() {
     let mut generator = kani::pointer_generator::<char, 3>();
@@ -48,9 +46,9 @@ fn check_overlap() {
     kani::cover!(ptr_1 == ptr_2, "Same");
     kani::cover!(ptr_1 == unsafe { ptr_2.byte_add(1) }, "Overlap");
 
-    let distance = unsafe { ptr_1.offset_from(ptr_2) };
+    let distance = unsafe { ptr_1.byte_offset_from(ptr_2) };
     kani::cover!(distance > 0, "Greater");
     kani::cover!(distance < 0, "Smaller");
 
-    assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements");
+    assert!(distance >= -8 && distance <= 8, "Expected a maximum distance of 8 bytes");
 }

tests/expected/intrinsics/offset-same-object/expected

@@ -1,2 +1 @@
-FAILURE\
-"same object violation"
+Failed Checks: Offset result and original pointer should point to the same allocation

tests/expected/intrinsics/ptr_offset_from_unsigned/expected

@@ -1 +1 @@
-Failed Checks: attempt to compute unsigned offset with negative distance
+Failed Checks: Expected non-negative distance between pointers

tests/expected/offset-bounds-check/offset_from.expected

@@ -0,0 +1,6 @@
+Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize
+Failed Checks: Offset result and original pointer should point to the same allocation
+
+Verification failed for - check_offset_from_diff_alloc
+Verification failed for - check_offset_from_oob_ptr
+Complete - 2 successfully verified harnesses, 2 failures, 4 total.

tests/expected/offset-bounds-check/offset_from.rs

@@ -0,0 +1,47 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani offset operations correctly detect out-of-bound access.
+
+/// Verification should fail because safety violation is not a regular panic.
+#[kani::proof]
+#[kani::should_panic]
+fn check_offset_from_oob_ptr() {
+    let val = 10u128;
+    let ptr: *const u128 = &val;
+    let ptr_oob: *const u128 = ptr.wrapping_add(10);
+    // SAFETY: This is not safe!
+    let _offset = unsafe { ptr_oob.offset_from(ptr) };
+}
+
+#[kani::proof]
+fn check_offset_from_diff_alloc() {
+    let val1 = 10u128;
+    let val2 = 0u128;
+    let ptr1: *const u128 = &val1;
+    let ptr2: *const u128 = &val2;
+    // SAFETY: This is not safe!
+    let offset = unsafe { ptr1.offset_from(ptr2) };
+    assert!(offset != 0);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_offset_from_unit_panic() {
+    let val1 = kani::any();
+    let val2 = kani::any();
+    let ptr1: *const () = &val1 as *const _ as *const ();
+    let ptr2: *const () = &val2 as *const _ as *const ();
+    // SAFETY: This is safe but will panic...
+    let _offset = unsafe { ptr1.offset_from(ptr2) };
+}
+
+#[kani::proof]
+fn check_offset_from_same_dangling() {
+    let val = 10u128;
+    let ptr: *const u128 = &val;
+    let ptr_oob_1: *const u128 = ptr.wrapping_add(10);
+    let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5);
+    // SAFETY: This is safe since the pointer is the same!
+    let offset = unsafe { ptr_oob_1.offset_from(ptr_oob_2) };
+    assert_eq!(offset, 0);
+}

tests/expected/offset-bounds-check/sub_ptr.expected

@@ -0,0 +1,29 @@
+Checking harness check_sub_ptr_same_dangling...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_sub_ptr_unit_panic...
+Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+
+Checking harness check_sub_ptr_negative_result...
+Failed Checks: Expected non-negative distance between pointers
+VERIFICATION:- FAILED
+
+Checking harness check_sub_ptr_diff_alloc...
+Failed Checks: Offset result and original pointer should point to the same allocation
+VERIFICATION:- FAILED
+
+Checking harness check_sub_ptr_oob_ptr...
+Failed Checks: Offset result and original pointer should point to the same allocation
+VERIFICATION:- FAILED
+
+Checking harness check_sub_ptr_self_oob...
+Failed Checks: Offset result and original pointer should point to the same allocation
+VERIFICATION:- FAILED
+
+Summary:
+Verification failed for - check_sub_ptr_negative_result
+Verification failed for - check_sub_ptr_diff_alloc
+Verification failed for - check_sub_ptr_oob_ptr
+Verification failed for - check_sub_ptr_self_oob
+Complete - 2 successfully verified harnesses, 4 failures, 6 total.

tests/expected/offset-bounds-check/sub_ptr.rs

@@ -0,0 +1,70 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order.
+
+#![feature(ptr_sub_ptr)]
+
+#[kani::proof]
+fn check_sub_ptr_self_oob() {
+    let val = 10u128;
+    let ptr: *const u128 = &val;
+    let ptr_oob: *const u128 = ptr.wrapping_add(10);
+    // SAFETY: This is not safe!
+    let _offset = unsafe { ptr_oob.sub_ptr(ptr) };
+}
+
+#[kani::proof]
+fn check_sub_ptr_oob_ptr() {
+    let val = 10u128;
+    let ptr: *const u128 = &val;
+    let ptr_oob: *const u128 = ptr.wrapping_sub(10);
+    // SAFETY: This is not safe!
+    let _offset = unsafe { ptr.sub_ptr(ptr_oob) };
+}
+
+#[kani::proof]
+fn check_sub_ptr_diff_alloc() {
+    let val1 = kani::any();
+    let val2 = kani::any();
+    let ptr1: *const u128 = &val1;
+    let ptr2: *const u128 = &val2;
+    // SAFETY: This is not safe!
+    let _offset = unsafe { ptr1.sub_ptr(ptr2) };
+}
+
+#[kani::proof]
+fn check_sub_ptr_negative_result() {
+    let val: [u8; 10] = kani::any();
+    let ptr_first: *const _ = &val[0];
+    let ptr_last: *const _ = &val[9];
+    // SAFETY: This is safe!
+    let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) };
+
+    // SAFETY: This is not safe!
+    let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) };
+
+    // Just use the result.
+    assert!(offset_ok != offset_not_ok);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_sub_ptr_unit_panic() {
+    let val1 = kani::any();
+    let val2 = kani::any();
+    let ptr1: *const () = &val1 as *const _ as *const ();
+    let ptr2: *const () = &val2 as *const _ as *const ();
+    // SAFETY: This is safe but will panic...
+    let _offset = unsafe { ptr1.sub_ptr(ptr2) };
+}
+
+#[kani::proof]
+fn check_sub_ptr_same_dangling() {
+    let val = 10u128;
+    let ptr: *const u128 = &val;
+    let ptr_oob_1: *const u128 = ptr.wrapping_add(10);
+    let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5);
+    // SAFETY: This is safe since the pointer is the same!
+    let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) };
+    assert_eq!(offset, 0);
+}

tests/expected/offset-from-distance-check/expected

@@ -0,0 +1,3 @@
+Failed Checks: Expected the distance between the pointers, in bytes, to be a
+                        multiple of the size of `T`
+VERIFICATION:- FAILED