From 6b032f48f4dfc5a0882b5c21d5729d730371c38b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 10 Mar 2023 14:27:00 -0800 Subject: [PATCH 1/5] Pass `--cfg=kani` to build scripts --- kani-driver/src/call_cargo.rs | 5 +++++ .../build-rs-conditional/Cargo.toml | 9 ++++++++ .../cargo-kani/build-rs-conditional/build.rs | 11 ++++++++++ .../build-rs-conditional/src/lib.rs | 22 +++++++++++++++++++ 4 files changed, 47 insertions(+) create mode 100644 tests/cargo-kani/build-rs-conditional/Cargo.toml create mode 100644 tests/cargo-kani/build-rs-conditional/build.rs create mode 100644 tests/cargo-kani/build-rs-conditional/src/lib.rs diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 30dac09eddaa..f6bbf913566e 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -99,6 +99,11 @@ impl KaniSession { cargo_args.push("-v".into()); } + // Propagate `--cfg=kani` to build scripts. + cargo_args.push("-Zhost-config".into()); + cargo_args.push("-Ztarget-applies-to-host".into()); + cargo_args.push("--config=host.rustflags=[\"--cfg=kani\"]".into()); + // Arguments that will only be passed to the target package. let mut pkg_args: Vec = vec![]; pkg_args.extend(["--".to_string(), self.reachability_arg()]); diff --git a/tests/cargo-kani/build-rs-conditional/Cargo.toml b/tests/cargo-kani/build-rs-conditional/Cargo.toml new file mode 100644 index 000000000000..136bae92250e --- /dev/null +++ b/tests/cargo-kani/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/cargo-kani/build-rs-conditional/build.rs b/tests/cargo-kani/build-rs-conditional/build.rs new file mode 100644 index 000000000000..0b083ff95f02 --- /dev/null +++ b/tests/cargo-kani/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/cargo-kani/build-rs-conditional/src/lib.rs b/tests/cargo-kani/build-rs-conditional/src/lib.rs new file mode 100644 index 000000000000..1c48a6b26ed9 --- /dev/null +++ b/tests/cargo-kani/build-rs-conditional/src/lib.rs @@ -0,0 +1,22 @@ +// 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. + +#[cfg(kani)] +mod verify { + /// Running `cargo kani` should verify that "RUNNING_KANI" is equals to "Yes" + #[kani::proof] + fn check() { + assert_eq!(env!("RUNNING_KANI"), "Yes"); + } +} + +#[cfg(test)] +mod test { + /// Running `cargo test` should check that "RUNNING_KANI" is "No". + #[test] + fn check() { + assert_eq!(env!("RUNNING_KANI"), "No"); + } +} From 675595f4b9a6605c1125b87e61163fe4162b28e7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 10 Mar 2023 14:37:49 -0800 Subject: [PATCH 2/5] Add expected file --- tests/cargo-kani/build-rs-conditional/expected | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 tests/cargo-kani/build-rs-conditional/expected diff --git a/tests/cargo-kani/build-rs-conditional/expected b/tests/cargo-kani/build-rs-conditional/expected new file mode 100644 index 000000000000..ecca82c5ffa1 --- /dev/null +++ b/tests/cargo-kani/build-rs-conditional/expected @@ -0,0 +1,7 @@ +Checking harness verify::check... + +verify::check.assertion\ +Status: SUCCESS\ +Description: "assertion failed: env!("RUNNING_KANI") == "Yes"" + +VERIFICATION:- SUCCESSFUL From 67e35a2c06802178a7b66db16f2a72ca981da5a9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 4 Jul 2023 13:38:00 -0700 Subject: [PATCH 3/5] Ensure we run cargo with a nightly version Also add support to the playback command and use a script to test the fix. Inside the Kani test folder, rustup will pick up the version from our toolchain configuration file. --- kani-driver/src/call_cargo.rs | 26 ++++++++++++------- kani-driver/src/concrete_playback/playback.rs | 12 ++++++--- kani-driver/src/session.rs | 8 ++++++ .../cargo-kani/build-rs-conditional/expected | 7 ----- .../build-rs-conditional/Cargo.toml | 0 .../build-rs-conditional/build.rs | 0 .../build-rs-conditional/build_rs.sh | 25 ++++++++++++++++++ .../build-rs-conditional/config.yml | 4 +++ .../build-rs-conditional/expected | 16 ++++++++++++ .../build-rs-conditional/src/lib.rs | 8 +++--- 10 files changed, 84 insertions(+), 22 deletions(-) delete mode 100644 tests/cargo-kani/build-rs-conditional/expected rename tests/{cargo-kani => script-based-pre}/build-rs-conditional/Cargo.toml (100%) rename tests/{cargo-kani => script-based-pre}/build-rs-conditional/build.rs (100%) 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 rename tests/{cargo-kani => script-based-pre}/build-rs-conditional/src/lib.rs (71%) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index f6bbf913566e..2c4f8b5e9c3b 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}; @@ -78,8 +78,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()); @@ -99,11 +98,6 @@ impl KaniSession { cargo_args.push("-v".into()); } - // Propagate `--cfg=kani` to build scripts. - cargo_args.push("-Zhost-config".into()); - cargo_args.push("-Ztarget-applies-to-host".into()); - cargo_args.push("--config=host.rustflags=[\"--cfg=kani\"]".into()); - // Arguments that will only be passed to the target package. let mut pkg_args: Vec = vec![]; pkg_args.extend(["--".to_string(), self.reachability_arg()]); @@ -115,7 +109,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) @@ -256,6 +251,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..f8bc5bdf7a17 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,12 @@ 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()); + + // Propagate `--cfg=kani` to build scripts. + cargo_args.push("-Zhost-config".into()); + cargo_args.push("-Ztarget-applies-to-host".into()); + cargo_args.push("--config=host.rustflags=[\"--cfg=kani\"]".into()); // These have to be the last arguments to cargo test. if !args.playback.test_args.is_empty() { @@ -124,7 +129,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 47cbb0914eaf..9a29239d48fe 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-kani/build-rs-conditional/expected b/tests/cargo-kani/build-rs-conditional/expected deleted file mode 100644 index ecca82c5ffa1..000000000000 --- a/tests/cargo-kani/build-rs-conditional/expected +++ /dev/null @@ -1,7 +0,0 @@ -Checking harness verify::check... - -verify::check.assertion\ -Status: SUCCESS\ -Description: "assertion failed: env!("RUNNING_KANI") == "Yes"" - -VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/build-rs-conditional/Cargo.toml b/tests/script-based-pre/build-rs-conditional/Cargo.toml similarity index 100% rename from tests/cargo-kani/build-rs-conditional/Cargo.toml rename to tests/script-based-pre/build-rs-conditional/Cargo.toml diff --git a/tests/cargo-kani/build-rs-conditional/build.rs b/tests/script-based-pre/build-rs-conditional/build.rs similarity index 100% rename from tests/cargo-kani/build-rs-conditional/build.rs rename to tests/script-based-pre/build-rs-conditional/build.rs 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/cargo-kani/build-rs-conditional/src/lib.rs b/tests/script-based-pre/build-rs-conditional/src/lib.rs similarity index 71% rename from tests/cargo-kani/build-rs-conditional/src/lib.rs rename to tests/script-based-pre/build-rs-conditional/src/lib.rs index 1c48a6b26ed9..70df880fdc8b 100644 --- a/tests/cargo-kani/build-rs-conditional/src/lib.rs +++ b/tests/script-based-pre/build-rs-conditional/src/lib.rs @@ -1,14 +1,16 @@ // 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. +//! 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() { + 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()); } } @@ -16,7 +18,7 @@ mod verify { mod test { /// Running `cargo test` should check that "RUNNING_KANI" is "No". #[test] - fn check() { + fn check_not_kani() { assert_eq!(env!("RUNNING_KANI"), "No"); } } From 7ae873381cd3bc154ffbf47fa5960149459185d1 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 4 Jul 2023 14:38:27 -0700 Subject: [PATCH 4/5] Update test --- tests/cargo-ui/verbose-cmds/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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... From b03d22ef7380d580a09c31756cc1bb5639abb14b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 6 Jul 2023 14:15:01 -0700 Subject: [PATCH 5/5] Remove redundant arguments from playback --- kani-driver/src/concrete_playback/playback.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index f8bc5bdf7a17..bb060cea58bd 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -116,11 +116,6 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { cargo_args.append(&mut args.cargo.to_cargo_args()); cargo_args.append(&mut cargo_config_args()); - // Propagate `--cfg=kani` to build scripts. - cargo_args.push("-Zhost-config".into()); - cargo_args.push("-Ztarget-applies-to-host".into()); - cargo_args.push("--config=host.rustflags=[\"--cfg=kani\"]".into()); - // These have to be the last arguments to cargo test. if !args.playback.test_args.is_empty() { cargo_args.push("--".into());