Unexpected failure when modifies attribute points to a ZST

[celinval]

I tried this code:

    #[requires(assert_valid_ptr(dst) && has_valid_value(dst))]
    #[modifies(dst)]
    pub unsafe fn replace<T>(dst: *mut T, src: T) -> T {
        std::ptr::replace(dst, src)
    }

    /// This one fails in the builtin-library
    #[kani::proof_for_contract(contracts::replace)]
    pub fn check_replace_unit() {
        check_replace_impl::<()>();
    }

    /// This one succeeds
    #[kani::proof_for_contract(contracts::replace)]
    pub fn check_replace_char() {
        check_replace_impl::<char>();
    }

    fn check_replace_impl<T: kani::Arbitrary + Eq + Clone>() {
        let mut dst = T::any();
        let orig = dst.clone();
        let src = T::any();
        let ret = unsafe { contracts::replace(&mut dst, src.clone()) };
        assert_eq!(ret, orig);
        assert_eq!(dst, src);
    }

using the following command line invocation:

kani contracts.rs

with Kani version: 0.51.0-dev (#3107)

I expected to see this happen: verification succeeds

Instead, this happened: Verification failed with the following failure:

SUMMARY:
 ** 1 of 1485 failed (3 unreachable)
Failed Checks: ptr NULL or writable up to size
 File: "<builtin-library-__CPROVER_contracts_library>", line 162, in __CPROVER_contracts_car_set_insert

[remi-delmas-3000]

#[modifies(dst)]
Does this mean that

1. the function modifies the contents of the location pointed to by dst or
2. the contents of dst ?

Assuming 1), this should be translated to __CPROVER_assigns(*dst) and CBMC will check that *dst is a valid location of size 0. Which may not be the case depending on how pointers to ZSTs are initialised in Rust.

[celinval]

In Rust, a 0 sized access is valid for any pointer, and the address of a ZST variable can be anything. #3134 changed Kani to implement that.

I believe CBMC still expects the pointer to point to a valid allocation, which is likely the reason why this is failing. If that's the case, we need to omit the assigns clause.

[carolynzech]

@celinval For this line:
#[requires(assert_valid_ptr(dst) && has_valid_value(dst))]
where are assert_valid_ptr and has_valid_value defined? I'm trying to reproduce the failure and it won't compile because the functions aren't in scope.
For now, I just commented out this requires clause, since it's not required to reproduce the issue anyway, but just curious.

[celinval]

I think those were old names