Ensure we run cargo with a nightly version

Also add support to the playback command and use a script to test
the fix. Inside the Kani test folder, rustup will pick up the version
from our toolchain configuration file.

kani-driver/src/call_cargo.rs

@@ -5,7 +5,7 @@ use crate::args::VerificationArgs;
 use crate::call_single_file::to_rustc_arg;
 use crate::project::Artifact;
 use crate::session::KaniSession;
-use crate::util;
+use crate::{session, util};
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target};
@@ -78,8 +78,7 @@ impl KaniSession {
             cargo_args.push(format!("--features={}", features.join(",")).into());
         }
 
-        cargo_args.push("--target".into());
-        cargo_args.push(build_target.into());
+        cargo_args.append(&mut cargo_config_args());
 
         cargo_args.push("--target-dir".into());
         cargo_args.push(target_dir.into());
@@ -99,11 +98,6 @@ impl KaniSession {
             cargo_args.push("-v".into());
         }
 
-        // Propagate `--cfg=kani` to build scripts.
-        cargo_args.push("-Zhost-config".into());
-        cargo_args.push("-Ztarget-applies-to-host".into());
-        cargo_args.push("--config=host.rustflags=[\"--cfg=kani\"]".into());
-
         // Arguments that will only be passed to the target package.
         let mut pkg_args: Vec<String> = vec![];
         pkg_args.extend(["--".to_string(), self.reachability_arg()]);
@@ -115,7 +109,8 @@ impl KaniSession {
         for package in packages {
             for verification_target in package_targets(&self.args, package) {
                 let mut cmd = Command::new("cargo");
-                cmd.args(&cargo_args)
+                cmd.arg(session::toolchain_shorthand())
+                    .args(&cargo_args)
                     .args(vec!["-p", &package.name])
                     .args(&verification_target.to_args())
                     .args(&pkg_args)
@@ -256,6 +251,19 @@ impl KaniSession {
     }
 }
 
+pub fn cargo_config_args() -> Vec<OsString> {
+    [
+        "--target",
+        env!("TARGET"),
+        // Propagate `--cfg=kani` to build scripts.
+        "-Zhost-config",
+        "-Ztarget-applies-to-host",
+        "--config=host.rustflags=[\"--cfg=kani\"]",
+    ]
+    .map(OsString::from)
+    .to_vec()
+}
+
 /// Print the compiler message following the coloring schema.
 fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> {
     if use_rendered {

kani-driver/src/concrete_playback/playback.rs

@@ -5,6 +5,7 @@
 
 use crate::args::common::Verbosity;
 use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat};
+use crate::call_cargo::cargo_config_args;
 use crate::call_single_file::base_rustc_flags;
 use crate::session::{lib_playback_folder, InstallType};
 use crate::{session, util};
@@ -113,8 +114,12 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
     }
 
     cargo_args.append(&mut args.cargo.to_cargo_args());
-    cargo_args.push("--target".into());
-    cargo_args.push(env!("TARGET").into());
+    cargo_args.append(&mut cargo_config_args());
+
+    // Propagate `--cfg=kani` to build scripts.
+    cargo_args.push("-Zhost-config".into());
+    cargo_args.push("-Ztarget-applies-to-host".into());
+    cargo_args.push("--config=host.rustflags=[\"--cfg=kani\"]".into());
 
     // These have to be the last arguments to cargo test.
     if !args.playback.test_args.is_empty() {
@@ -124,7 +129,8 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
 
     // Arguments that will only be passed to the target package.
     let mut cmd = Command::new("cargo");
-    cmd.args(&cargo_args)
+    cmd.arg(session::toolchain_shorthand())
+        .args(&cargo_args)
         .env("RUSTC", &install.kani_compiler()?)
         // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
         // https://doc.rust-lang.org/cargo/reference/environment-variables.html

kani-driver/src/session.rs

@@ -291,6 +291,14 @@ pub fn base_folder() -> Result<PathBuf> {
         .to_path_buf())
 }
 
+/// Return the shorthand for the toolchain used by this Kani version.
+///
+/// This shorthand can be used to select the exact toolchain version that matches the one used to
+/// build the current Kani version.
+pub fn toolchain_shorthand() -> String {
+    format!("+{}", env!("RUSTUP_TOOLCHAIN"))
+}
+
 impl InstallType {
     pub fn new() -> Result<Self> {
         // Case 1: We've checked out the development repo and we're built under `target/kani`

tests/script-based-pre/build-rs-conditional/build_rs.sh

@@ -0,0 +1,25 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+TMP_DIR="/tmp/build-rs"
+
+rm -rf ${TMP_DIR}
+cp -r . ${TMP_DIR}
+pushd ${TMP_DIR} > /dev/null
+
+
+echo "[TEST] Run verification..."
+cargo kani --concrete-playback=inplace -Z concrete-playback
+
+echo "[TEST] Run playback..."
+cargo kani playback -Z concrete-playback --lib -- check_kani
+
+echo "[TEST] Run test..."
+cargo test --lib
+
+# Cleanup
+popd > /dev/null
+rm -r ${TMP_DIR}

tests/script-based-pre/build-rs-conditional/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: build_rs.sh
+expected: expected

tests/script-based-pre/build-rs-conditional/expected

@@ -0,0 +1,16 @@
+[TEST] Run verification...
+Checking harness verify::check_kani...
+Complete - 1 successfully verified harnesses, 0 failures, 1 total
+
+[TEST] Run playback...
+running 1 test\
+test verify::kani_concrete_playback_check_kani_\
+\
+test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 1 filtered out
+
+[TEST] Run test...
+running 1 test\
+test test::check_not_kani ... ok\
+\
+test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out
+

tests/cargo-kani/build-rs-conditional/src/lib.rs → tests/script-based-pre/build-rs-conditional/src/lib.rs

@@ -1,22 +1,24 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This tests ensures that build scripts are able to conditionally check if they are running under
-//! Kani.
+//! Kani (in both verification and playback mode).
 
 #[cfg(kani)]
 mod verify {
     /// Running `cargo kani` should verify that "RUNNING_KANI" is equals to "Yes"
     #[kani::proof]
-    fn check() {
+    fn check_kani() {
         assert_eq!(env!("RUNNING_KANI"), "Yes");
+        // Add a dummy cover so playback generates a test that should succeed.
+        kani::cover!(kani::any());
     }
 }
 
 #[cfg(test)]
 mod test {
     /// Running `cargo test` should check that "RUNNING_KANI" is "No".
     #[test]
-    fn check() {
+    fn check_not_kani() {
         assert_eq!(env!("RUNNING_KANI"), "No");
     }
 }