From 042a3039762acf48ddc2d2215bc1beb8fd5cbd20 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 7 Jul 2023 17:44:28 -0700 Subject: [PATCH] Add "kani" configuration key to enable conditional compilation in build 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 --- kani-driver/src/call_cargo.rs | 21 +++++++++++++--- kani-driver/src/concrete_playback/playback.rs | 7 +++--- kani-driver/src/session.rs | 8 ++++++ tests/cargo-ui/verbose-cmds/expected | 2 +- .../build-rs-conditional/Cargo.toml | 9 +++++++ .../build-rs-conditional/build.rs | 11 ++++++++ .../build-rs-conditional/build_rs.sh | 25 +++++++++++++++++++ .../build-rs-conditional/config.yml | 4 +++ .../build-rs-conditional/expected | 16 ++++++++++++ .../build-rs-conditional/src/lib.rs | 24 ++++++++++++++++++ 10 files changed, 119 insertions(+), 8 deletions(-) create mode 100644 tests/script-based-pre/build-rs-conditional/Cargo.toml create mode 100644 tests/script-based-pre/build-rs-conditional/build.rs create mode 100755 tests/script-based-pre/build-rs-conditional/build_rs.sh create mode 100644 tests/script-based-pre/build-rs-conditional/config.yml create mode 100644 tests/script-based-pre/build-rs-conditional/expected create mode 100644 tests/script-based-pre/build-rs-conditional/src/lib.rs 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"); + } +}