You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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::<dyn SampleTrait>, 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 <kiro-agent@users.noreply.github.com>
#[requires(ub_checks::can_dereference(self.as_ptr()))]// Ensure the pointer is valid to create a reference.
177
-
#[ensures(|result: &&MaybeUninit<T>| core::ptr::eq(*result,self.cast().as_ptr()))]// Ensure returned reference points to the correct memory location.
177
+
#[ensures(|result: &&MaybeUninit<T>| core::ptr::addr_eq(*result,self.cast::<MaybeUninit<T>>().as_ptr()))]// Ensure returned reference points to the correct memory location.
#[requires(ub_checks::can_dereference(self.as_ptr()))]// Ensure pointer is valid to create a mutable reference.
202
-
#[ensures(|result: &&mutMaybeUninit<T>| core::ptr::eq(*result,self.cast().as_ptr()))]// Ensure the returned reference points to the correct memory.
202
+
#[ensures(|result: &&mutMaybeUninit<T>| core::ptr::addr_eq(*result,self.cast::<MaybeUninit<T>>().as_ptr()))]// Ensure the returned reference points to the correct memory.
0 commit comments