From b739b186aaf736c7857b5e96351791972149aba8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Aug 2026 21:20:04 +0000 Subject: [PATCH] Allow zero-sized offsets on dangling pointers in ptr contracts The requires/ensures clauses of the pointer arithmetic operations (<*mut T>::{offset,add,sub}, <*const T>::{offset,add,sub}, NonNull::{add,sub}, NonNull::offset_from_unsigned) demanded same_allocation unconditionally (modulo a ZST escape), although the documented semantics explicitly permit zero-sized offsets on any pointer, including dangling ones: "The computed offset, count * size_of::() bytes, must not overflow isize" and only "if the computed offset is non-zero, then self must be derived from a pointer to some allocated object". The stricter-than-documented clauses are violated by legitimate std code: slices are allowed to be backed by dangling pointers when empty (e.g. slice::from_raw_parts(ptr, 0) for arbitrary aligned non-null ptr), and Iter::new then computes ptr.add(0), and len() computes end.offset_from_unsigned(begin) on two equal dangling pointers. With dependency contracts asserted (the Kani default since model-checking/kani#3802), the slice::iter::verify::verify_tup harnesses fail on these clauses; evaluating same_allocation on an allocation-less pointer is additionally a Kani unsupported construct ("Kani does not support reasoning about pointer to unallocated memory"). The CI configuration currently masks this with --no-assert-contracts. Add the documented escape hatches: `count == 0 ||` ahead of the same-allocation disjunct of offset/add/sub requires and ensures (matching the precedent already present in NonNull::offset), and an equal-address escape in NonNull::offset_from_unsigned (matching the precedent in <*const T>::offset_from). The unconditional clauses were introduced with the original contracts in 014965a3b54 ("Contracts and Harnesses for `<*mut T>::add`, `sub` and `offset`" #113), 688b15bfa09 ("Contracts & Harnesses for `non_null::sub` and `non_null::sub_ptr` and `non_null::offset_from`" #93) and siblings. Verified (Kani 152c6a8c + CBMC 6.10.0): * slice::iter::verify::verify_tup::{check_next_back_unchecked, check_advance_back_by} now pass with contracts asserted; * all 265 proof harnesses matching non_null_check_{add,sub, offset_from_unsigned} and ptr::verify::check_{mut,const}_{add,sub, offset} pass both with and without --no-assert-contracts. Co-authored-by: Kiro --- library/core/src/ptr/const_ptr.rs | 12 ++++++------ library/core/src/ptr/mut_ptr.rs | 12 ++++++------ library/core/src/ptr/non_null.rs | 16 +++++++++++++--- 3 files changed, 25 insertions(+), 15 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 084b0c21c2f77..f364e4490e59e 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -358,12 +358,12 @@ impl *const T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - (core::mem::size_of::() == 0 || core::ub_checks::same_allocation(self, self.wrapping_offset(count))) + (count == 0 || core::mem::size_of::() == 0 || core::ub_checks::same_allocation(self, self.wrapping_offset(count))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] + #[ensures(|result| count == 0 || (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *const T where T: Sized, @@ -884,12 +884,12 @@ impl *const T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count)))) + (count == 0 || (core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] + #[ensures(|result| count == 0 || (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1022,12 +1022,12 @@ impl *const T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count)))) + (count == 0 || (core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] + #[ensures(|result| count == 0 || (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 5422a4ade0088..7d406b1d25406 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -364,12 +364,12 @@ impl *mut T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_offset(count)))) + (count == 0 || (core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_offset(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| count == 0 || (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *mut T where T: Sized, @@ -988,12 +988,12 @@ impl *mut T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count)))) + (count == 0 || (core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| count == 0 || (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1128,12 +1128,12 @@ impl *mut T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count)))) + (count == 0 || (core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| count == 0 || (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 775034399717d..8a967b13a7a16 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -693,7 +693,10 @@ impl NonNull { #[requires(count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::() as isize).is_some() // check wrapping add - && core::ub_checks::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))] + // Zero-sized offsets (`count * size_of::() == 0`) are always + // permitted, including on dangling pointers, per the documentation. + && (count == 0 || core::mem::size_of::() == 0 + || core::ub_checks::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize))))] #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where @@ -784,7 +787,10 @@ impl NonNull { #[requires( count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize && - core::ub_checks::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count)) + // Zero-sized offsets (`count * size_of::() == 0`) are always + // permitted, including on dangling pointers, per the documentation. + (count == 0 || core::mem::size_of::() == 0 || + core::ub_checks::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count))) )] #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(-(count as isize)))] pub const unsafe fn sub(self, count: usize) -> Self @@ -1032,7 +1038,11 @@ impl NonNull { #[rustc_const_stable(feature = "const_ptr_sub_ptr", since = "1.87.0")] #[requires( self.as_ptr().addr().checked_sub(subtracted.as_ptr().addr()).is_some() && - core::ub_checks::same_allocation(self.as_ptr(), subtracted.as_ptr()) && + // Pointers with equal addresses trivially satisfy the + // same-allocation requirement (a zero-sized span), including + // dangling pointers such as those of empty slices. + (self.as_ptr().addr() == subtracted.as_ptr().addr() || + core::ub_checks::same_allocation(self.as_ptr(), subtracted.as_ptr())) && (self.as_ptr().addr()) >= (subtracted.as_ptr().addr()) && (self.as_ptr().addr() - subtracted.as_ptr().addr()) % core::mem::size_of::() == 0 )]