Concrete playback requires nightly rustc

[celinval]

I tried the following:

$ cargo init dummy
$ cd dummy
$ cargo --version
cargo 1.63.0 (fd9c4297c 2022-07-01)

I added the following line to Cargo.toml

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

I opened src/main.rs

#[kani::proof]
fn force_failure() {
  assert!(kani::any());
}

using the following command line invocation:

cargo kani --enable-unstable --concrete-playback
cargo test

with Kani version: 0.9.0

I expected to see this happen: Cargo runs the new test and fail.

Instead, this happened: Cargo failed to build kani library with the following error:

error[E0554]: `#![feature]` may not be used on the stable release channel
 --> ~/.cargo/git/checkouts/kani-0ce0dacf5e98886d/281d0bb/library/kani/src/lib.rs:5:1
  |
5 | #![feature(rustc_attrs)]
  | ^^^^^^^^^^^^^^^^^^^^^^^^

[celinval]

We could guard the usage of rustc_attrs and rustc_diagnostic_item with cfg_attr, but I was wondering if there's a cleaner solution.

[celinval]

This is very similar to https://github.com/model-checking/kani/issues/1581. Same root cause.

[adpaco-aws]

I was wondering if there's a cleaner solution.

I haven't been able to find one, but IMHO the cfg_attr solution is quite clean already.

[celinval]

I was wondering if there's a cleaner solution.

I haven't been able to find one, but IMHO the cfg_attr solution is quite clean already.

We could probably use a macro or a proc_macro to do that. Unfortunately, https://github.com/model-checking/kani/pull/2199 has added another unstable feature.

I was wondering if we can modify the concrete_playback::any_raw_internal() to remove the transmute and use a loop instead. This only runs in the concrete execution so it shouldn't be a problem.

[jaisnan]

Would removing the transmute theoretically remove the dependency on nightly features entirely? If so, that seems like the cleanest solution and option.

But i imagine, we need incomplete_features for Arbitrary and that means we'll need nightly for arbitrary, is that correct?

[celinval]

The way we are doing transmute is the reason why we need the incomplete_features for arbitrary.

[celinval]

The transmute could be replaced by storing Any as described here: https://github.com/model-checking/kani/issues/1527