Add "kani" configuration key to enable conditional compilation in bui…

…ld scripts (#2297)

We now pass `--cfg=kani` to build scripts, which allow users to use constructs such as `if cfg!(kani)` to conditionally compile their build scripts.

The build script may have logic that is not redundant to Kani, or even unsupported. Users can now change how their build works based on conditional compilation.

Co-authored-by: Kareem Khazem <karkhaz@amazon.com>

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