From 30b689efbe49a153069483ea72e06f250f3a8985 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Aug 2026 21:26:14 +0000 Subject: [PATCH] Use addr_eq in NonNull contracts to support wide pointers Several postconditions in NonNull compared raw pointers with `==` or `core::ptr::eq`: as_ptr, new, new_unchecked, the slice as_mut_ptr, and - via ptr::eq - as_ref, as_mut, as_uninit_ref and as_uninit_mut. For wide pointers (T: ?Sized with dyn metadata) such comparisons also compare vtable pointers, whose identity is unspecified in Rust; Kani rejects them with "Reached unstable vtable comparison 'Eq'". With dependency contracts asserted (the Kani default since model-checking/kani#3802), any harness whose call graph evaluates these clauses on a trait-object NonNull fails, e.g. ptr::non_null::verify::non_null_check_from_raw_part_trait (the comparison surfaces in ptr::eq::, reached from as_ref's postcondition). Compare with core::ptr::addr_eq instead, which is well-defined for any pointer types. All these functions produce their result directly from `self`, so metadata is preserved by construction, and the accompanying comments already described the intent as address preservation. The casts in the as_uninit_* clauses need explicit turbofish types now that the comparison no longer constrains their type parameter. Verified (Kani 152c6a8c + CBMC 6.10.0): non_null_check_from_raw_part_trait now passes with contracts asserted - this was the last remaining verdict difference on a 125-harness sample between runs with and without --no-assert-contracts. The non_null_check_{as_ref,as_mut,as_uninit*,from_raw_part*,as_ptr,new} harnesses pass in both configurations, with one exception: non_null_check_as_uninit_slice_mut fails with contracts asserted both with and without this change (a pre-existing dereference/alignment issue reached via asserted contracts, tracked separately). Co-authored-by: Kiro --- library/core/src/ptr/non_null.rs | 33 ++++++++++++++++++++++---------- 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 775034399717d..f2baac3f7e7c7 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -174,7 +174,7 @@ impl NonNull { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure the pointer is valid to create a reference. - #[ensures(|result: &&MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure returned reference points to the correct memory location. + #[ensures(|result: &&MaybeUninit| core::ptr::addr_eq(*result, self.cast::>().as_ptr()))] // Ensure returned reference points to the correct memory location. pub const unsafe fn as_uninit_ref<'a>(self) -> &'a MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -199,7 +199,7 @@ impl NonNull { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure pointer is valid to create a mutable reference. - #[ensures(|result: &&mut MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure the returned reference points to the correct memory. + #[ensures(|result: &&mut MaybeUninit| core::ptr::addr_eq(*result, self.cast::>().as_ptr()))] // Ensure the returned reference points to the correct memory. pub const unsafe fn as_uninit_mut<'a>(self) -> &'a mut MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -243,7 +243,8 @@ impl NonNull { #[inline] #[track_caller] #[requires(!ptr.is_null())] - #[ensures(|result| result.as_ptr() == ptr)] + // See as_ptr regarding the use of addr_eq for wide-pointer support. + #[ensures(|result| core::ptr::addr_eq(result.as_ptr(), ptr))] pub const unsafe fn new_unchecked(ptr: *mut T) -> Self { // SAFETY: the caller must guarantee that `ptr` is non-null. unsafe { @@ -281,7 +282,8 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_new", since = "1.85.0")] #[inline] #[ensures(|result| result.is_some() == !ptr.is_null())] - #[ensures(|result| result.is_none() || result.expect("ptr is null!").as_ptr() == ptr)] + // See as_ptr regarding the use of addr_eq for wide-pointer support. + #[ensures(|result| result.is_none() || core::ptr::addr_eq(result.expect("ptr is null!").as_ptr(), ptr))] pub const fn new(ptr: *mut T) -> Option { if !ptr.is_null() { // SAFETY: The pointer is already checked and is not null @@ -420,8 +422,13 @@ impl NonNull { #[rustc_never_returns_null_ptr] #[must_use] #[inline(always)] - //Ensures address of resulting pointer is same as original - #[ensures(|result: &*mut T| *result == self.pointer as *mut T)] + // Ensures the address of the resulting pointer is the same as the + // original. `addr_eq` (rather than `==`) makes this well-defined for + // wide pointers too: comparing `*mut dyn Trait` with `==` also compares + // vtable pointers, whose identity is unspecified (and which Kani rejects + // with "unstable vtable comparison"). `as_ptr` is a representation-level + // conversion that trivially preserves metadata. + #[ensures(|result: &*mut T| core::ptr::addr_eq(*result, self.pointer))] pub const fn as_ptr(self) -> *mut T { // This is a transmute for the same reasons as `NonZero::get`. @@ -462,7 +469,12 @@ impl NonNull { #[must_use] #[inline(always)] #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure input is convertible to a reference - #[ensures(|result: &&T| core::ptr::eq(*result, self.as_ptr()))] // Ensure returned reference matches pointer + // addr_eq (rather than ptr::eq) so the clause is well-defined for + // wide pointers too: comparing *const dyn with == also compares vtable + // pointers, whose identity is unspecified (Kani: "unstable vtable + // comparison"). The reference is created from `self`, so metadata is + // preserved by construction. + #[ensures(|result: &&T| core::ptr::addr_eq(*result, self.as_ptr()))] // Ensure returned reference matches pointer pub const unsafe fn as_ref<'a>(&self) -> &'a T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -503,7 +515,8 @@ impl NonNull { #[inline(always)] #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // verify result (a mutable reference) is still associated with the same memory address as the raw pointer stored in self - #[ensures(|result: &&mut T| core::ptr::eq(*result, self.as_ptr()))] + // See as_ref regarding the use of addr_eq. + #[ensures(|result: &&mut T| core::ptr::addr_eq(*result, self.as_ptr()))] pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a mutable reference. @@ -1674,8 +1687,8 @@ impl NonNull<[T]> { #[must_use] #[unstable(feature = "slice_ptr_get", issue = "74265")] #[rustc_never_returns_null_ptr] - // Address preservation - #[ensures(|result: &*mut T| *result == self.pointer as *mut T)] + // Address preservation; see as_ptr regarding the use of addr_eq. + #[ensures(|result: &*mut T| core::ptr::addr_eq(*result, self.pointer))] pub const fn as_mut_ptr(self) -> *mut T { self.as_non_null_ptr().as_ptr() }