Concrete playback needs tweak for harnesses under cfg(test)

[zhassan-aws]

The current instructions for the concrete playback feature include adding kani in the dev-dependencies section. If the harness of interest is under #[cfg(test)], then cargo kani needs to be run with the --tests option. However, including --tests results in trying to compile the Kani crate with Kani! This fails with the following error:

error: duplicate diagnostic item found: `KaniAssume`.
  --> /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/499e35f/library/kani/src/lib.rs:44:1
   |
44 | pub fn assume(_cond: bool) {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: the diagnostic item is first defined in crate `kani`.

error: duplicate diagnostic item found: `KaniExpectFail`.
   --> /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/499e35f/library/kani/src/lib.rs:122:1
    |
122 | pub fn expect_fail(_cond: bool, _message: &'static str) {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: the diagnostic item is first defined in crate `kani`.

error: duplicate diagnostic item found: `KaniAssert`.
  --> /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/499e35f/library/kani/src/lib.rs:61:1
   |
61 | pub fn assert(_cond: bool, _msg: &'static str) {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: the diagnostic item is first defined in crate `kani`.

error: duplicate diagnostic item found: `KaniAnyRaw`.
   --> /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/499e35f/library/kani/src/lib.rs:115:1
    |
115 | fn any_raw_inner<T>() -> T {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: the diagnostic item is first defined in crate `kani`.

error: duplicate diagnostic item found: `KaniPanic`.
   --> /home/ubuntu/.cargo/git/checkouts/kani-0ce0dacf5e98886d/499e35f/library/kani/src/lib.rs:137:1
    |
137 | pub fn panic(message: &'static str) -> ! {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: the diagnostic item is first defined in crate `kani`.

Error: "Failed to compile crate."
error: could not compile `kani` due to 5 previous errors
Error: cargo exited with status exit status: 101

The workaround I've used is to remove kani from the dev-dependencies, before running cargo kani, then add it back before running debugging the generated harness.

Steps to reproduce:

1. cargo new --lib conc_playback
2. cd conc_playback
3. Add kani to dev-dependencies in Cargo.toml:

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

4. Run cargo kani --tests

[zhassan-aws]

One easy fix is to update the instructions to suggest conditionally adding kani as a dev dependency:

[target.'cfg(not(kani))'.dev-dependencies]
kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }

[celinval]

That's an interesting one... There's definitely a conflict between --tests and --concrete-playback.

It feels a bit counter intuitive to add kani under cfg(not(kani)). Another issue is that the --concrete-playback feature adds the test case in the same module as the proof harness. So this fix wouldn't work if the harness is inside a module guarded with #[cfg(kani)]:

#[cfg(kani)]
mod harnesses {
  #[kani:proof]
  fn my_harness() {}

  // Test will be here.
}

[jaisnan]

Ran into this issue while adding the concrete playback button for the extension, this causes all cfg(test) or #[test] cases to crash and it gives the same underlying error.

[carolynzech]

I've confirmed that #2464 did indeed fix this.

Steps:

cargo new --lib conc_playback
cd conc_playback
cargo kani --tests --concrete-playback inplace -Z concrete-playback
cargo kani playback

If you don't change the contents of src/lib.rs at all, Kani just exits with a message that there were no harnesses. I added a failing harness and tested that cargo kani --tests --concrete-playback inplace -Z concrete-playback generates a failing test and cargo kani playback plays it back correctly.