Value-dependent failure with vec! initialization

[lancelet]

I tried this code:

#[kani::proof]
fn vec_failure() {
    let value: u8 = 1;   /* set to zero and it passes */
    let count: u16 = kani::any();
    let vector: Vec<u8> = vec![value; count as usize];
}

using the following command line invocation:

cargo kani

with Kani version:

$ cargo kani --version
cargo-kani 0.56.0

$ kani --version
kani 0.56.0

When it is run with value = 1, it produces the following failure:

Check 168: std::intrinsics::write_bytes::<u8>.precondition_instance.1
	 - Status: FAILURE
	 - Description: "memset destination region writeable"
	 - Location: ../../../runner/.rustup/toolchains/nightly-2024-10-03-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/intrinsics.rs:3496:9 in function std::intrinsics::write_bytes::<u8>

But when run with value = 0, it succeeds.

I expected uniform behavior in both cases, but perhaps the intrinsics special-case zero somehow?

[lancelet]

Workaround

In case anyone encounters this... I found that I could get this to pass by mocking out std::intrinsics::write_bytes:

    fn mock_write_bytes<T>(dst: *mut T, val: u8, count: usize) {}

    #[kani::proof]
    #[kani::stub(std::intrinsics::write_bytes, mock_write_bytes)]
    fn vec_failure() {
        let value: u8 = 1; /* set to zero and it passes */
        let count: u16 = kani::any();
        let vector: Vec<u8> = vec![value; count as usize];
    }

And then run with:

cargo kani --harness vec_failure -Z stubbing

However, because stubbing requires --harness, this isn't very scalable.

[zhassan-aws]

Hi @lancelet. Thanks for creating this issue. This is likely a duplicated of #90.

Thanks for the workaround!