Unexpected kani panic: assign statement with unequal types

[QinyuanWu]

This issue is related to the NonNull module verification.

This is a POC:

#![feature(ptr_metadata)]

use std::ptr::NonNull;

trait SampleTrait {
    fn get_value(&self) -> i32;
}

struct SampleStruct {
    value: i32,
}

impl SampleTrait for SampleStruct {
    fn get_value(&self) -> i32 {
        self.value
    }
}

#[cfg(kani)]
#[kani::proof]
fn main() {

    // 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 = std::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");
    }
}

using the following command line invocation:

cargo kani

with Kani version: 0.56.0
Platform: MacOS M2

I expected to see verification results but received the following compilation error:

error: Failed to compile `kani_bugs` 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-_80076268767659083946749461790619121878::FatPtr") rhs Pointer { typ: TypeDef { name: "_80076268767659083946749461790619121878Inner", typ: StructTag("tag-Unit") } }
                                  left: StructTag("tag-_80076268767659083946749461790619121878::FatPtr")
                                 right: Pointer { typ: TypeDef { name: "_80076268767659083946749461790619121878Inner", typ: StructTag("tag-Unit") } }.

This issue still persists with assigning sample_struct with a concrete value such as:

let sample_struct = SampleStruct { value: 5 };

@zhassan-aws