Fix playback with build scripts

kani-driver/src/call_single_file.rs

@@ -136,12 +136,6 @@ impl KaniSession {
             }
         }
 
-        // e.g. compiletest will set 'compile-flags' here and we should pass those down to rustc
-        // and we fail in `tests/kani/Match/match_bool.rs`
-        if let Ok(str) = std::env::var("RUSTFLAGS") {
-            flags.extend(str.split(' ').map(OsString::from));
-        }
-
         // This argument will select the Kani flavour of the compiler. It will be removed before
         // rustc driver is invoked.
         flags.push("--kani-compiler".into());
@@ -154,7 +148,7 @@ pub fn base_rustc_flags(lib_path: PathBuf) -> Vec<OsString> {
     let kani_std_rlib = lib_path.join("libstd.rlib");
     let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
     let sysroot = base_folder().unwrap();
-    [
+    let mut flags = [
         "-C",
         "overflow-checks=on",
         "-C",
@@ -186,7 +180,15 @@ pub fn base_rustc_flags(lib_path: PathBuf) -> Vec<OsString> {
         kani_std_wrapper.as_str(),
     ]
     .map(OsString::from)
-    .to_vec()
+    .to_vec();
+
+    // e.g. compiletest will set 'compile-flags' here and we should pass those down to rustc
+    // and we fail in `tests/kani/Match/match_bool.rs`
+    if let Ok(str) = std::env::var("RUSTFLAGS") {
+        flags.extend(str.split(' ').map(OsString::from));
+    }
+
+    flags
 }
 
 /// This function can be used to convert Kani compiler specific arguments into a rustc one.

kani-driver/src/concrete_playback/playback.rs

@@ -99,7 +99,7 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
     let mut cargo_args: Vec<OsString> = vec!["test".into()];
 
     if args.playback.common_opts.verbose() {
-        cargo_args.push("--verbose".into());
+        cargo_args.push("-vv".into());
     } else if args.playback.common_opts.quiet {
         cargo_args.push("--quiet".into())
     }
@@ -113,6 +113,8 @@ 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());
 
     // These have to be the last arguments to cargo test.
     if !args.playback.test_args.is_empty() {

tests/script-based-pre/cargo_playback_build/config.yml

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

tests/script-based-pre/cargo_playback_build/playback_with_build.expected

@@ -0,0 +1,10 @@
+[TEST] Generate test...
+Checking harness harnesses::harness...
+VERIFICATION:- SUCCESSFUL
+
+[TEST] Run test...
+running 2 tests
+test harnesses::kani_concrete_playback_harness
+test test::print_os_name
+
+test result: ok. 2 passed; 0 failed;

tests/script-based-pre/cargo_playback_build/playback_with_build.sh

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

tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml

@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "sample_crate"
+version = "0.1.0"
+edition = "2021"

tests/script-based-pre/cargo_playback_build/sample_crate/build.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Export some variables to the harness
+
+use std::env::var;
+
+fn main() {
+    let target = if var("TARGET").unwrap().contains("linux") { "linux" } else { "other" };
+    println!(r#"cargo:rustc-cfg=TARGET_OS="{}""#, target);
+}

tests/script-based-pre/cargo_playback_build/sample_crate/src/lib.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test is used to test playback with a build configuration.
+
+#[cfg(TARGET_OS = "linux")]
+pub const OS_NAME: &'static str = "linux";
+
+#[cfg(not(TARGET_OS = "linux"))]
+pub const OS_NAME: &'static str = "other";
+
+#[cfg(kani)]
+mod harnesses {
+    use super::*;
+
+    #[kani::proof]
+    fn harness() {
+        kani::cover!(true, "Cover {OS_NAME}");
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use super::*;
+
+    #[test]
+    fn print_os_name() {
+        println!("OS: {OS_NAME}");
+        assert!(["linux", "other"].contains(&OS_NAME));
+    }
+}

tests/script-based-pre/cargo_playback_opts/playback_opts.expected

@@ -3,4 +3,4 @@
 [TEST] Only codegen test...
     Finished test
 [TEST] Executable
-sample_crate/target/debug/deps/sample_crate-
+debug/deps/sample_crate-

tests/script-based-pre/cargo_playback_opts/playback_opts.sh

@@ -12,7 +12,10 @@ cargo kani playback -Z concrete-playback --only-codegen -- kani_concrete_playbac
 
 echo "[TEST] Only codegen test..."
 output=$(cargo kani playback -Z concrete-playback --only-codegen --message-format=json -- kani_concrete_playback)
-executable=$(echo ${output} | jq 'select(.reason == "compiler-artifact") | .executable')
+
+# Cargo may generate 2 artifacts, one for the library and one for tests.
+executable=$(echo ${output} |
+    jq 'select(.reason == "compiler-artifact") | select(.executable != null) | .executable')
 
 echo "[TEST] Executable"
 echo ${executable}