Unexpected Kani Panic: assign statement with unequal types

[QinyuanWu]

I'm working on the harness for NonNull::from_raw_parts and was experimenting with calling the API withtrait objects:

    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 from_raw_parts(data_pointer: NonNull<()>, metadata: <T as super::Pointee>::Metadata,) -> NonNull<T>
    #[kani::proof_for_contract(NonNull::from_raw_parts)]
    pub fn non_null_check_new_from_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::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap();
        let metadata = core::ptr::metadata(trait_object);

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

        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");
        }
    }

Contract on from_raw_parts:

    #[ensures(|result| !result.pointer.is_null())]
    pub const fn from_raw_parts(
        data_pointer: NonNull<()>,
        metadata: <T as super::Pointee>::Metadata,
    ) -> NonNull<T> {
        // SAFETY: The result of `ptr::from::raw_parts_mut` is non-null because `data_pointer` is.
        unsafe {
            NonNull::new_unchecked(super::from_raw_parts_mut(data_pointer.as_ptr(), metadata))
        }
    }

However I received the following compilation error:

Kani Rust Verifier 0.56.0 (standalone)
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/stmt.rs:172:9:
                                assertion `left == right` failed: Error: assign statement with unequal types lhs StructTag("tag-_120260832284995662991453413275889622457::FatPtr") rhs Pointer { typ: TypeDef { name: "_120260832284995662991453413275889622457Inner", typ: StructTag("tag-Unit") } }
                                  left: StructTag("tag-_120260832284995662991453413275889622457::FatPtr")
                                 right: Pointer { typ: TypeDef { name: "_120260832284995662991453413275889622457Inner", typ: StructTag("tag-Unit") } }.

error: Failed to compile `core` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/stmt.rs:172:9:
                                assertion `left == right` failed: Error: assign statement with unequal types lhs StructTag("tag-_120260832284995662991453413275889622457::FatPtr") rhs Pointer { typ: TypeDef { name: "_120260832284995662991453413275889622457Inner", typ: StructTag("tag-Unit") } }
                                  left: StructTag("tag-_120260832284995662991453413275889622457::FatPtr")
                                 right: Pointer { typ: TypeDef { name: "_120260832284995662991453413275889622457Inner", typ: StructTag("tag-Unit") } }.

It looks like the right side(NonNull object) is empty but I'm not sure what caused that. Is it because I initialized the value in the trait object to be kani::any()? Appreciate any guidance. Thank you! @zhassan-aws

[zhassan-aws]

Hi @QinyuanWu. This is a bug in Kani. Can you file an issue in the Kani repository? The issue should be reproducible outside of the verify-rust-std repository (i.e. try reproducing it by creating a Rust package using cargo new).

[QinyuanWu]

Kani issue opened: model-checking/kani#3631