Kani fails to verify harness with `for` loop with bounded iterations

[celinval]

I tried this code after looking into how Kani is handling Option::ok_or():

/// Dummy function with a for loop that only runs 2 iterations.
fn bounded_loop<T: Default>(b: bool, other: T) -> T {
    let mut ret = other;
    for i in 0..2 {
        ret = match b {
            true => T::default(),
            false => ret,
        };
    }
    return ret;
}

/// Harness that should succeed. We add a conservative loop bound.
#[kani::proof]
#[kani::unwind(10)]
fn harness() {
    let _ = bounded_loop(kani::any(), ());
}

using the following command line invocation:

kani harness.rs

with Kani version: 0.20

I expected to see this happen: The verification should succeed.
Instead, this happened: Verification fails due to unwinding assertion failure.

Open here for a few notes:

Possibly related issue

I bumped into this issue while debugging a failure in #2149 where Kani incorrectly identifies a loop in Option::ok_or(). Verification may fail if user sets a low loop bound. This is an example of the original issue:

fn loop_free<T: Default>(b: bool, other: T) -> T {
    match b {
        true => T::default(),
        false => other,
    }
}

#[kani::proof]
#[kani::unwind(2)]
fn check_our_ok_or() {
    let b : bool = kani::any();
    let _ = loop_free(b, 5));
}

See diffblue/cbmc#7506 for the related CBMC issue.

With that in mind, I decided to see what would happen if the problematic code was inside a loop, and it looks like things just don't work.

Drop support

I believe both issues are related to the CFG generated when the code includes drop statements. Since the function bounded_loop is generic, its MIR will include drop statements for cases where the type T must be dropped. The drop statement is added to a basic block at the end (in order of declaration) of the function.

If we add Copy to the function signature, the issue goes away and the CFG is much simpler.

fn bounded_loop<T: Default + Copy>(b: bool, other: T) -> T;

[celinval]

I forgot to mention that if we remove the unwind attribute, Kani doesn't seem to terminate. Very large bounds, such as 1000 will also trigger an unwinding assertion failure.