diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index ce53584f3418..a2f46744e6d4 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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 { 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 { 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. diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index e401daf1c886..0a71d64fe50f 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -99,7 +99,7 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { let mut cargo_args: Vec = 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() { diff --git a/tests/script-based-pre/cargo_playback_build/config.yml b/tests/script-based-pre/cargo_playback_build/config.yml new file mode 100644 index 000000000000..694a78f2d39b --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/cargo_playback_build/playback_with_build.expected b/tests/script-based-pre/cargo_playback_build/playback_with_build.expected new file mode 100644 index 000000000000..3530fccd2b09 --- /dev/null +++ b/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; diff --git a/tests/script-based-pre/cargo_playback_build/playback_with_build.sh b/tests/script-based-pre/cargo_playback_build/playback_with_build.sh new file mode 100755 index 000000000000..a81dcf018661 --- /dev/null +++ b/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} diff --git a/tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml new file mode 100644 index 000000000000..c00d0ccc4bdb --- /dev/null +++ b/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" diff --git a/tests/script-based-pre/cargo_playback_build/sample_crate/build.rs b/tests/script-based-pre/cargo_playback_build/sample_crate/build.rs new file mode 100644 index 000000000000..3ae35a375292 --- /dev/null +++ b/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); +} diff --git a/tests/script-based-pre/cargo_playback_build/sample_crate/src/lib.rs b/tests/script-based-pre/cargo_playback_build/sample_crate/src/lib.rs new file mode 100644 index 000000000000..754446bda445 --- /dev/null +++ b/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)); + } +} diff --git a/tests/script-based-pre/cargo_playback_opts/playback_opts.expected b/tests/script-based-pre/cargo_playback_opts/playback_opts.expected index 571f9ef0dd9f..68b7daa3ee03 100644 --- a/tests/script-based-pre/cargo_playback_opts/playback_opts.expected +++ b/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- diff --git a/tests/script-based-pre/cargo_playback_opts/playback_opts.sh b/tests/script-based-pre/cargo_playback_opts/playback_opts.sh index 85853c55e366..1419a581597d 100755 --- a/tests/script-based-pre/cargo_playback_opts/playback_opts.sh +++ b/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}