Concrete playback doesn't work when --cfg kani is required

[zhassan-aws]

I tried this code:

This test somewhat mimics how the Kani--Bolero integration works, where a function returns a symbolic value in kani mode and a random value otherwise:

fn main() {}

#[cfg(kani)]
fn gen_value() -> i32 {
    kani::any()
}

#[cfg(not(kani))]
fn gen_value() -> i32 {
    rand::random()
}


#[cfg_attr(kani, kani::proof)]
#[cfg_attr(not(kani), test)]
fn harness() {
    let x: i32 = gen_value();
    assert!(x != 50);
}

using the following command line invocation:

cargo kani --enable-unstable --concrete-playback=inplace

with Kani version: 0.18.0

Kani generated the following test:

#[test]
fn kani_concrete_playback_harness_5085686764756153187() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // 50
        vec![50, 0, 0, 0],
    ];
    kani::concrete_playback_run(concrete_vals, harness);
}

Now if I run this test with:

cargo test kani_concrete_playback_harness_5085686764756153187

or in the debugger, the assertion doesn't fail because the cfg(not(kani)) version of gen_value gets called. In addition, we get the following crash:

running 1 test
test kani_concrete_playback_harness_5085686764756153187 ... FAILED

failures:

---- kani_concrete_playback_harness_5085686764756153187 stdout ----
thread 'kani_concrete_playback_harness_5085686764756153187' panicked at 'At the end of concrete playback, there were still these concrete values left over `[[50, 0, 0, 0]]`. This either happened because: 1) Your code/harness changed after you generated this concrete playback unit test. 2) There's a bug in Kani. Please report the issue here: <https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md>', /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/c135fa9/library/kani/src/concrete_playback.rs:32:9
stack backtrace:
   0: rust_begin_unwind
             at /rustc/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/std/src/panicking.rs:575:5
   1: core::panicking::panic_fmt
             at /rustc/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/core/src/panicking.rs:65:14
   2: kani::concrete_playback::concrete_playback_run::{{closure}}
             at /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/c135fa9/library/kani/src/concrete_playback.rs:32:9
   3: std::thread::local::LocalKey<T>::try_with
             at /rustc/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/std/src/thread/local.rs:453:16
   4: std::thread::local::LocalKey<T>::with
             at /rustc/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/std/src/thread/local.rs:429:9
   5: kani::concrete_playback::concrete_playback_run
             at /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/c135fa9/library/kani/src/concrete_playback.rs:30:5
   6: conc_playback_cfg::kani_concrete_playback_harness_5085686764756153187
             at ./src/main.rs:26:5
   7: conc_playback_cfg::kani_concrete_playback_harness_5085686764756153187::{{closure}}
             at ./src/main.rs:21:57
   8: core::ops::function::FnOnce::call_once
             at /rustc/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/core/src/ops/function.rs:507:5
   9: core::ops::function::FnOnce::call_once
             at /rustc/70f8737b2f5d3bf7d6b784fad00b663b7ff9feda/library/core/src/ops/function.rs:507:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.


failures:
    kani_concrete_playback_harness_5085686764756153187

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 1 filtered out; finished in 0.01s

error: test failed, to rerun pass `--bin conc_playback_cfg`

To reproduce, create a cargo package with the above Rust code and add the following to Cargo.toml:

[dependencies]
rand = "0.8.5"

[dev-dependencies]
kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }

[zhassan-aws]

If I run with --cfg kani, I get a compilation failure:

$ RUSTFLAGS="--cfg kani" cargo test kani_concrete_playback_harness_5085686764756153187
# -- snip --
error[E0433]: failed to resolve: use of undeclared crate or module `kanitool`
  --> src/main.rs:14:18
   |
14 | #[cfg_attr(kani, kani::proof)]
   |                  ^^^^^^^^^^^ use of undeclared crate or module `kanitool`
   |
   = note: this error originates in the attribute macro `kani::proof` (in Nightly builds, run with -Z macro-backtrace for more info)

For more information about this error, try `rustc --explain E0433`.
error: could not compile `conc_playback_cfg` due to previous error

[celinval]

This seems to be a duplicate of #1610

[zhassan-aws]

Indeed. Closing this one.