Spurious capacity overflow with CBMC 5.71

[zhassan-aws]

This test is derived from https://github.com/model-checking/kani/blob/main/tests/kani/Refs/main.rs

I tried this code:

use std::collections::BTreeMap;

#[kani::proof]
#[kani::unwind(2)]
fn main() {
    let arguments: BTreeMap<(), ()> = BTreeMap::new();
    let _ = arguments.values().collect::<Vec<_>>()
            .into_iter()
            .map(|_| 5)
            .collect::<Vec<_>>();
}

using the following command line invocation:

kani btreemap.rs

with Kani version: bb268b1 and CBMC 5.71.0

I expected to see this happen: Verification successful

Instead, this happened: a capacity overflow check fails:

SUMMARY:
 ** 1 of 1148 failed (15 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/home/ubuntu/.rustup/toolchains/nightly-2022-11-06-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/raw_vec.rs", line 518, in alloc::raw_vec::capacity_overflow

VERIFICATION:- FAILED
Verification Time: 3.296982s

With CBMC 5.70.0, this test passes:

SUMMARY:
 ** 0 of 1151 failed (20 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 44.638622s

[zhassan-aws]

Blocker for #1941

[tautschnig]

This is also happening with the very latest CBMC version (which has additional fixes on top of 5.71.0). I'll investigate.

[tautschnig]

The CBMC change altering the result is diffblue/cbmc@633875b. As a consequence of this change we no longer simplify (struct Unit **)8 - (struct Unit **)8 to zero, but instead leave the expression intact. It seems the back-end isn't handling this correctly (even though we should likely put back a variant of the previous simplification rule).

[tautschnig]

diffblue/cbmc#7398 addresses this problem.