diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 00bbe72d9865..82186e96a44e 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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}; @@ -79,8 +79,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()); @@ -111,7 +110,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) @@ -252,6 +252,19 @@ impl KaniSession { } } +pub fn cargo_config_args() -> Vec { + [ + "--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 { diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index 0a71d64fe50f..bb060cea58bd 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/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,7 @@ 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()); // These have to be the last arguments to cargo test. if !args.playback.test_args.is_empty() { @@ -124,7 +124,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 diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 646b7b6ae746..d0834cae2122 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -291,6 +291,14 @@ pub fn base_folder() -> Result { .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 { // Case 1: We've checked out the development repo and we're built under `target/kani` diff --git a/tests/cargo-ui/verbose-cmds/expected b/tests/cargo-ui/verbose-cmds/expected index a15f3ba25b6e..f883ef972cb3 100644 --- a/tests/cargo-ui/verbose-cmds/expected +++ b/tests/cargo-ui/verbose-cmds/expected @@ -1,5 +1,5 @@ CARGO_ENCODED_RUSTFLAGS= -cargo rustc +cargo +nightly Running: `goto-cc Running: `goto-instrument Checking harness dummy_harness... diff --git a/tests/script-based-pre/build-rs-conditional/Cargo.toml b/tests/script-based-pre/build-rs-conditional/Cargo.toml new file mode 100644 index 000000000000..136bae92250e --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/Cargo.toml @@ -0,0 +1,9 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "build-rs-conditional" +version = "0.1.0" +edition = "2021" + +[dependencies] + diff --git a/tests/script-based-pre/build-rs-conditional/build.rs b/tests/script-based-pre/build-rs-conditional/build.rs new file mode 100644 index 000000000000..0b083ff95f02 --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/build.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify that build scripts can check if they are running under `kani`. + +fn main() { + if cfg!(kani) { + println!("cargo:rustc-env=RUNNING_KANI=Yes"); + } else { + println!("cargo:rustc-env=RUNNING_KANI=No"); + } +} diff --git a/tests/script-based-pre/build-rs-conditional/build_rs.sh b/tests/script-based-pre/build-rs-conditional/build_rs.sh new file mode 100755 index 000000000000..f08fcf10cb79 --- /dev/null +++ b/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} diff --git a/tests/script-based-pre/build-rs-conditional/config.yml b/tests/script-based-pre/build-rs-conditional/config.yml new file mode 100644 index 000000000000..e34ed0cb5689 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/build-rs-conditional/expected b/tests/script-based-pre/build-rs-conditional/expected new file mode 100644 index 000000000000..55f309077721 --- /dev/null +++ b/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 + diff --git a/tests/script-based-pre/build-rs-conditional/src/lib.rs b/tests/script-based-pre/build-rs-conditional/src/lib.rs new file mode 100644 index 000000000000..70df880fdc8b --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/src/lib.rs @@ -0,0 +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 (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_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_not_kani() { + assert_eq!(env!("RUNNING_KANI"), "No"); + } +}