Add a regression test for running verify-std command. (model-checki…

…ng#3236)

In model-checking#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

@@ -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",
 ]

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<OsString> = vec!["build".into()];
         cargo_args.append(&mut cargo_config_args());

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"

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

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.

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>() -> 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}