Checking memory initialization in presence of copy and copy_nonoverlapping produces false positives #3347
Description
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);
}
}