proof_for_contracts making false positive failures with memcpy on drop

[ShoyuVanilla]

I found this while working on model-checking/verify-rust-std#234

I tried this code:

#[cfg(kani)]
pub mod verify {
    #[kani::ensures(|_| unsafe { *src == *dst })]
    pub fn foo(src: *const u8, dst: *mut u8) {
        struct CopyOnDrop {
            src: *const u8,
            dst: *mut u8,
        }

        impl Drop for CopyOnDrop {
            fn drop(&mut self) {
                unsafe {
                    std::ptr::copy_nonoverlapping(self.src, self.dst, 1);
                }
            }
        }

        let _drop_guard = CopyOnDrop { src, dst };
    }

    #[kani::proof]
    pub fn check_foo() {
        let src = 42;
        let mut dst = 0;
        foo(&raw const src, &raw mut dst);
        assert!(src == dst);
    }

    #[kani::proof_for_contract(foo)]
    pub fn check_foo_contract() {
        let src = 42;
        let mut dst = 0;
        foo(&raw const src, &raw mut dst);
    }
}

using the following command line invocation:

cargo kani -Zfunction-contracts

with Kani version: 0.57.0

I expected to see this happen: Both harnesses succeed

Instead, this happened: check_foo_contract falis with the following;

Check 16: memcpy.assigns.2
         - Status: FAILURE
         - Description: "Check that array_replace((const void *)(char *)dst, ...) is allowed by the assigns clause"
         - Location: <builtin-library-memcpy>:46 in function memcpy

[BusyBeaver-42]

Hi @ShoyuVanilla, when writing a contract for a function, if it writes to some memory then you have to declare it in the contract using the modifies macro (see also write sets).

In your case, you have to write your contract like this.

#[kani::modifies(dst)]
#[kani::ensures(|_| unsafe { *src == *dst })]
pub fn foo(src: *const u8, dst: *mut u8) {
    // snip
}

[ShoyuVanilla]

Oh, thanks! I should have read the docs more carefully 😅