Trait Object Failed Check: Reached unstable vtable comparison 'Eq'

[QinyuanWu]

For the function NonNull::to_raw_parts, I have the following contract and harness:

    #[ensures(|(data_ptr, metadata)| !data_ptr.as_ptr().is_null())] //TODO: kani bug
    #[ensures(|(data_ptr, metadata)| self == NonNull::from_raw_parts(*data_ptr, *metadata))]
    pub const fn to_raw_parts(self) -> (NonNull<()>, <T as super::Pointee>::Metadata) {
        (self.cast(), super::metadata(self.as_ptr()))
    }

    trait SampleTrait {
        fn get_value(&self) -> i32;
    }
    
    struct SampleStruct {
        value: i32,
    }
    
    impl SampleTrait for SampleStruct {
        fn get_value(&self) -> i32 {
            self.value
        }
    }

    // pub const fn to_raw_parts(self) -> (NonNull<()>, <T as super::Pointee>::Metadata)
    #[kani::proof_for_contract(NonNull::to_raw_parts)]
    pub fn non_null_check_to_raw_parts() {
        // Create a SampleTrait object from SampleStruct
        let sample_struct = SampleStruct { value: kani::any() };
        let trait_object: &dyn SampleTrait = &sample_struct;

        // Get the raw data pointer and metadata for the trait object
        let trait_ptr = NonNull::from(trait_object).cast::<()>(); //both have eq failure
        //let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); //Question: what's the difference
        // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type
        let metadata = core::ptr::metadata(trait_object);

        // Create NonNull<dyn MyTrait> from the data pointer and metadata
        let nonnull_trait_object: NonNull<dyn SampleTrait> = NonNull::from_raw_parts(trait_ptr, metadata);
        let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object);

        unsafe {
            // Ensure trait method and member is preserved
            //kani::assert( trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), "trait method and member must correctly preserve");
            kani::assert( trait_object as *const dyn ptr::non_null::verify::SampleTrait == nonnull_trait_object.as_ptr(), "trait method and member must correctly preserve");
        }
    }

This produces the following failed check:

SUMMARY:
 ** 1 of 157 failed (2 unreachable)
Failed Checks: Reached unstable vtable comparison 'Eq'
 File: "/Users/owo/Desktop/verify-rust-std/library/core/src/ptr/non_null.rs", line 1733, in <ptr::non_null::NonNull<dyn ptr::non_null::verify::SampleTrait> as cmp::PartialEq>::eq

VERIFICATION:- FAILED
Verification Time: 0.27859333s

Summary:
Verification failed for - ptr::non_null::verify::non_null_check_to_raw_parts
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

line 1733:

#[stable(feature = "nonnull", since = "1.25.0")]
impl<T: ?Sized> PartialEq for NonNull<T> {
    #[inline]
    #[allow(ambiguous_wide_pointer_comparisons)]
    fn eq(&self, other: &Self) -> bool {
        self.as_ptr() == other.as_ptr() // line 1733
    }
}

It's unclear to me what the check means and what caused the failed check. Is it due to the implementation of PartialEq for NonNull<T>? Appreciate any guidance. @zhassan-aws

[celinval]

The problem I believe is with this line:

trait_object as *const dyn ptr::non_null::verify::SampleTrait == nonnull_trait_object.as_ptr()

This is because comparing wide pointers to traits is not well-defined. Can you compare the components of the wide pointer instead? I.e.: The decomposed_* elements.

[QinyuanWu]

@zhassan-aws As we discussed in the meeting I'm confused with @celinval suggested approach and would appreciate any detailed guidance. Thank you!

[QinyuanWu]

Also I discovered that the issue is not from the harness but from the ensures clause:

    /// Decompose a (possibly wide) pointer into its data pointer and metadata components.
    ///
    /// The pointer can be later reconstructed with [`NonNull::from_raw_parts`].
    #[ensures(|(data_ptr, metadata)| !data_ptr.as_ptr().is_null())]
    #[ensures(|(data_ptr, metadata)| self.as_ref() == NonNull::from_raw_parts(*data_ptr, *metadata))] // PartialEq error
    pub const fn to_raw_parts(self) -> (NonNull<()>, <T as super::Pointee>::Metadata) {
        (self.cast(), super::metadata(self.as_ptr()))
    }

The goal is to verify that the decomposed data can be used to reconstructed later as a pointer with [NonNull::from_raw_parts] and that the reconstructed pointer preserves the original data and metadata. Maybe there could be a different approach that works better to prove that we got the correct result for NonNull<()> and <T as super::Pointee>::Metadata?

[celinval]

Just to clarify, comparing wide pointers of trait objects is not a well defined operation, thus, in Kani we fail the verification. We could improve our handling by only rejecting cases where the data pointers are the same but the vtable pointers are not. I think that would cover this case.

The workaround would be something like this:

#[ensures(|(data_ptr, _)| self.as_ptr() as *const ())]

[QinyuanWu]

@celinval Thank you! Updated the clause to be

#[ensures(|(data_ptr, metadata)| self.as_ptr() as *const () == data_ptr.as_ptr() as *const ())]