From 0bb1325e5f5e20dfdc89f292fd4bf71e6362066a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 6 Jun 2024 20:02:22 -0700 Subject: [PATCH] Add a regression test for running `verify-std` command. (#3236) In #3226, we added a new command that allow Kani to verify properties in a custom standard library. In this PR, we create a script test that create a modified version of the standard library and runs Kani against it. I also moved the script based tests to run after the more generic regression jobs. I think the script jobs are a bit harder to debug, they may take longer, and they are usually very specific to a few features. So probably best if we run the more generic tests first. --- Cargo.toml | 1 + kani-driver/src/call_cargo.rs | 2 + scripts/kani-regression.sh | 2 +- .../verify_std_cmd/config.yml | 4 + .../verify_std_cmd/verify_std.expected | 11 +++ .../verify_std_cmd/verify_std.sh | 91 +++++++++++++++++++ 6 files changed, 110 insertions(+), 1 deletion(-) create mode 100644 tests/script-based-pre/verify_std_cmd/config.yml create mode 100644 tests/script-based-pre/verify_std_cmd/verify_std.expected create mode 100755 tests/script-based-pre/verify_std_cmd/verify_std.sh diff --git a/Cargo.toml b/Cargo.toml index e4ff44f42ddc..641cbaf961be 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -68,4 +68,5 @@ exclude = [ "tests/script-based-pre", "tests/script-based-pre/build-cache-bin/target/new_dep", "tests/script-based-pre/build-cache-dirty/target/new_dep", + "tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std", ] diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index ebf61e153c46..a1d976d73150 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -57,6 +57,8 @@ impl KaniSession { let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path)); rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into()); rustc_args.push(self.reachability_arg().into()); + // Ignore global assembly, since `compiler_builtins` has some. + rustc_args.push(to_rustc_arg(vec!["--ignore-global-asm".to_string()]).into()); let mut cargo_args: Vec = vec!["build".into()]; cargo_args.append(&mut cargo_config_args()); diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index dcced313ce0b..d3bb0f7efb45 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -49,7 +49,6 @@ RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-trai # Declare testing suite information (suite and mode) TESTS=( - "script-based-pre exec" "kani kani" "expected expected" "ui expected" @@ -59,6 +58,7 @@ TESTS=( "smack kani" "cargo-kani cargo-kani" "cargo-ui cargo-kani" + "script-based-pre exec" "coverage coverage-based" "kani-docs cargo-kani" "kani-fixme kani-fixme" diff --git a/tests/script-based-pre/verify_std_cmd/config.yml b/tests/script-based-pre/verify_std_cmd/config.yml new file mode 100644 index 000000000000..f6e398303b79 --- /dev/null +++ b/tests/script-based-pre/verify_std_cmd/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: verify_std.sh +expected: verify_std.expected diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected new file mode 100644 index 000000000000..aa965f50cdf2 --- /dev/null +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -0,0 +1,11 @@ +[TEST] Run kani verify-std +Checking harness kani::check_success... +VERIFICATION:- SUCCESSFUL + +Checking harness kani::check_panic... +VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) + +Checking harness num::verify::check_non_zero... +VERIFICATION:- SUCCESSFUL + +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh new file mode 100755 index 000000000000..9e18ed72ca2a --- /dev/null +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -0,0 +1,91 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Test `kani verify-std` subcommand. +# 1. Make a copy of the rust standard library. +# 2. Add a few Kani definitions to it + a few harnesses +# 3. Execute Kani + +set +e + +TMP_DIR="tmp_dir" + +rm -rf ${TMP_DIR} +mkdir ${TMP_DIR} + +# Create a custom standard library. +echo "[TEST] Copy standard library from the current toolchain" +SYSROOT=$(rustc --print sysroot) +STD_PATH="${SYSROOT}/lib/rustlib/src/rust/library" +cp -r "${STD_PATH}" "${TMP_DIR}" + +# Insert a small harness in one of the standard library modules. +CORE_CODE=' +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod kani { + pub use kani_core::proof; + + #[rustc_diagnostic_item = "KaniAnyRaw"] + #[inline(never)] + pub fn any_raw_inner() -> T { + loop {} + } + + #[inline(never)] + #[rustc_diagnostic_item = "KaniAssert"] + pub const fn assert(cond: bool, msg: &'\''static str) { + let _ = cond; + let _ = msg; + } + + #[kani_core::proof] + #[kani_core::should_panic] + fn check_panic() { + let num: u8 = any_raw_inner(); + assert!(num != 0, "Found zero"); + } + + #[kani_core::proof] + fn check_success() { + let orig: u8 = any_raw_inner(); + let mid = orig as i8; + let new = mid as u8; + assert!(orig == new, "Conversion round trip works"); + } +} +' + +STD_CODE=' +#[cfg(kani)] +mod verify { + use core::kani; + #[kani::proof] + fn check_non_zero() { + let orig: u32 = kani::any_raw_inner(); + if let Some(val) = core::num::NonZeroU32::new(orig) { + assert!(orig == val.into()); + } else { + assert!(orig == 0); + }; + } +} +' + +echo "[TEST] Modify library" +echo "${CORE_CODE}" >> ${TMP_DIR}/library/core/src/lib.rs +echo "${STD_CODE}" >> ${TMP_DIR}/library/std/src/num.rs + +# Note: Prepending with sed doesn't work on MacOs the same way it does in linux. +# sed -i '1s/^/#![cfg_attr(kani, feature(kani))]\n/' ${TMP_DIR}/library/std/src/lib.rs +cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs +echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs +cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs + +echo "[TEST] Run kani verify-std" +export RUST_BACKTRACE=1 +kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" + +# Cleanup +rm -r ${TMP_DIR}