Add "kani" configuration key to enable conditional compilation in build scripts

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<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,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

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/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...

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]
+

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");
+    }
+}

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/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");
+    }
+}