Loop Contracts Issue: Arith. Overflow in prev(i) + i

[MinghuaWang]

I tried this code:

#![feature(stmt_expr_attributes)]
#![feature(proc_macro_hygiene)]

#[kani::requires(x < 10)]
fn func(x: usize) -> Option<usize> {
    let mut i: usize = 0;
    let mut r: usize = x;
    let N: usize = 7;
    #[kani::loop_invariant((i <= N && i >=0) && (on_entry(i) == 0 && prev(i) + 1 == i )) ]
    while i < N {
        i = i + 1;
    }
    if r + i >= x + N {
        Some(r)
    } else {
        None
    }
}

#[kani::proof]
fn harness() {
    let a = kani::any_where(|x: &usize| *x < 10);
    kani::assert(func(a).is_some(), "func(a) is some");
}

using the following command line invocation:

kani main.rs -Z loop-contracts -Z function-contracts 

with Kani version: 0.62.0

I expected to see this happen: VERIFICATION SUCCESS

Instead, this happened:

 ** 1 of 333 failed (9 unreachable)
Failed Checks: attempt to add with overflow
 File: "src/main.rs", line 9, in func::{closure#3}::{closure#0}::{closure#1}

VERIFICATION:- FAILED

Writing loop contracts can be a bit confusing and may not be very intuitive. For example, even though I have already included i <= N && i >= 0 in the loop invariants, why am I still getting an "add with overflow" error reported on line 9?

[MinghuaWang]

Perhaps this is because CBMC havoced the variable i within the if (i < N) block before executing i = i + 1? Is there any way to address this false alarm?"

[thanhnguyen-aws]

Hello, thanks for creating this issue. I created an PR to fix this bug. However, together with the PR, the invariant needs to be changed into

#[kani::loop_invariant((i <= N && i >=0) && (on_entry(i) == 0 && prev(i) < N && prev(i) + 1 == i )  ) ]

Explanation: The overfow is caused by prev(i) + 1, note that Kani also checks for overflow of expressions inside the loop_invariant and each operand of the and expression is checked from left to right. Therefore, the invariant prev(i) < N must be added before the addition to ensure that overflow cannot happen.