Checking memory initialization in presence of copy and copy_nonoverlapping produces false positives

[artemagvanian]

Trying to verify the following code with memory initialization checks enabled (-Z uninit-checks):

#[derive(kani::Arbitrary)]
struct S(u32, u8);

#[kani::proof]
unsafe fn main() {
    let mut a: S = kani::any();
    let b: S = kani::any();
    let a_ptr = &mut a as *mut S;
    std::ptr::write_unaligned(a_ptr, b);
}

yield the following error:

Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`
 File: ".../.rustup/toolchains/nightly-2024-07-15-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/intrinsics.rs", line 2958, in std::intrinsics::copy_nonoverlapping::<u8>

with Kani version: 0.53.0

I expected to see this happen:

VERIFICATION:- SUCCESSFUL

According to the Rust documentaiton, both copy and copy_nonoverlapping are untyped:

The copy is “untyped” in the sense that data may be uninitialized or otherwise violate the requirements of T. The initialization state is preserved exactly.

However, Kani treats a copy as a read followed by a write, which triggers memory initialization checks while it shouldn't. This becomes evident since the source code of write_unaligned copies the data byte-by-byte.

pub const unsafe fn write_unaligned<T>(dst: *mut T, src: T) {
    // SAFETY: the caller must guarantee that `dst` is valid for writes.
    // `dst` cannot overlap `src` because the caller has mutable access
    // to `dst` while `src` is owned by this function.
    unsafe {
        copy_nonoverlapping(addr_of!(src) as *const u8, dst as *mut u8, mem::size_of::<T>());
        // We are calling the intrinsic directly to avoid function calls in the generated code.
        intrinsics::forget(src);
    }
}