Mutable static variables usage in contract verification trigger UB

[celinval]

I tried this code:

static mut WRAP_COUNTER: Option<u32> = None;

/// This function is safe and should never crash. Counter starts at 0.
#[kani::modifies(std::ptr::addr_of!(WRAP_COUNTER))]
#[kani::ensures(|_| true)]
pub fn next() -> u32 {
    // Safe in single-threaded.
    unsafe {
        match &WRAP_COUNTER {
            Some(val) => {
                WRAP_COUNTER = Some(val.wrapping_add(1));
                *val
            }
            None => {
                WRAP_COUNTER = Some(0);
                0
            }
        }
    }
}

#[kani::proof_for_contract(next)]
fn check_next() {
    let _ret = next();
}

using the following command line invocation:

kani fixme.rs -Z function-contracts

with Kani version: 0.52.0

I expected to see this happen: Verification succeeds

Instead, this happened: Verification fails because WRAP_COUNTER is havoc and it can contain an invalid discriminant. Thus, the match statement unreachable block is reached.

Checking harness check_next...

VERIFICATION RESULT:
 ** 1 of 1359 failed
Failed Checks: unreachable code
 File: "static_mut.rs", line 14, in next_wrapper_5f5d0a::<std::option::Option<u32>>

VERIFICATION:- FAILED
Verification Time: 2.9701335s

[celinval]

Note that a normal harness where we havoc using kani::any() succeeds:

/// Without contracts, we can safely verify `next`.
#[kani::proof]
fn check_next_directly() {
    // First check that initial iteration returns 0 (base case).
    let first = next();
    assert_eq!(first, 0);

    // Havoc WRAP_COUNTER and invoke next.
    unsafe { WRAP_COUNTER = kani::any() };
    let ret = next();
    kani::cover!(ret == 0);
}

Result:

Checking harness check_next_directly...

VERIFICATION RESULT:
 ** 0 of 41 failed

 ** 1 of 1 cover properties satisfied

VERIFICATION:- SUCCESSFUL
Verification Time: 0.3075676s

[celinval]

One possible solution is to disable CBMC static havoc and initialize all reachable mutable static variables as part of the kani::internal::init_contracts() function.