Call to format! causes an infinite loop

[gshaurya18]

I tried this code:

fn identity(x: u32) -> u32 {
    // The following two lines cause kani to loop infinitely
    let helpful_log_message = format!("Called with: {}", x);
    println!("{}", helpful_log_message);
    // Directly calling println (without format) does not cause infinite looping
    // println!("Called with: {}", x);
    x
}

#[cfg(kani)]
#[kani::proof]
fn check_identity() {
    let x: u32 = kani::any();
    let y = identity(x);
    assert_eq!(x, y);
}

using the following command line invocation:

cargo-kani

with Kani version: kani was built on commit 054780c64a30192a49bc35c4f428323f07b0e85e on Amazon Linux 2, x86 In the following way:

git clone https://github.com/model-checking/kani.git
cd kani
git submodule update --init
./scripts/setup/al2/install_deps.sh
cargo build-dev -- --release

I expected to see this happen: Proof to terminate with "Verification SUCCESSFUL"

Instead, this happened:

Kani loops idenfinitely. Some logs [truncated]

aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/core/src/result.rs line 966 column 15 function std::result::Result::<std::ptr::NonNull<[u8]>, std::alloc::AllocError>::map_err::<std::collections::TryReserveError, {closure@alloc::raw_vec::RawVecInner::finish_grow::{closure#0}}> thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/core/src/result.rs line 2173 column 15 function <std::result::Result<std::ptr::NonNull<[u8]>, std::collections::TryReserveError> as std::ops::Try>::branch thread 0
aborting path on assume(false) at file src/lib.rs line 0 column 0 function alloc::raw_vec::RawVecInner::grow_amortized thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs line 550 column 9 function alloc::raw_vec::RawVecInner::<A>::reserve::do_reserve_and_handle::<std::alloc::Global> thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/collections/mod.rs line 93 column 10 function <std::collections::TryReserveErrorKind as std::clone::Clone>::clone thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs line 845 column 11 function alloc::raw_vec::handle_error thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/alloc.rs line 366 column 5 function std::alloc::handle_alloc_error::rt_error thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/alloc.rs line 407 column 13 function std::alloc::handle_alloc_error::rt_error thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/alloc.rs line 413 column 9 function std::alloc::handle_alloc_error thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs line 847 column 38 function alloc::raw_vec::handle_error thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs line 28 column 5 function alloc::raw_vec::capacity_overflow thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs line 846 column 29 function alloc::raw_vec::handle_error thread 0
aborting path on assume(false) at file <RUST_TOOLCHAIN>/lib/rustlib/src/rust/library/alloc/src/raw_vec/mod.rs line 558 column 17 function alloc::raw_vec::RawVecInner::<A>::reserve::do_reserve_and_handle::<std::alloc::Global

[gshaurya18]

On Amazon Linux 2023, the same proof succeeds

VERIFICATION:- SUCCESSFUL
Verification Time: 3.8319087s

Kani was installed as follows:

cargo install --locked kani-verifier
cargo kani setup
cargo-kani --version
cargo-kani 0.66.0

[zhassan-aws]

This is the culprit commit: f4d4a94.

Before this commit, verification completes in a few seconds.

[zhassan-aws]

Somehow, the upstream change (rust-lang/rust#148789) is causing the formatting code to fall on the verification path, even though the result of the format! call is not relevant to verification in this example.