Enable build cache in cargo kani

Cargo.toml

@@ -66,4 +66,5 @@ exclude = [
   "tests/cargo-ui",
   "tests/slow",
   "tests/assess-scan-test-scaffold",
+  "tests/script-based-pre",
 ]

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -81,6 +81,10 @@ impl CodegenBackend for GotocCodegenBackend {
         provide::provide_extern(providers);
     }
 
+    fn print_version(&self) {
+        println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION"));
+    }
+
     fn codegen_crate(
         &self,
         tcx: TyCtxt,

kani-compiler/src/parser.rs

@@ -46,12 +46,6 @@ pub const ENABLE_STUBBING: &str = "enable-stubbing";
 /// Configure command options for the Kani compiler.
 pub fn parser() -> Command {
     let app = command!()
-        .arg(
-            Arg::new("kani-compiler-version")
-                .short('?')
-                .action(ArgAction::Version)
-                .help("Gets `kani-compiler` version."),
-        )
         .arg(
             Arg::new(KANI_LIB)
                 .long(KANI_LIB)
@@ -137,6 +131,12 @@ pub fn parser() -> Command {
                 .help("Instruct the compiler to perform stubbing.")
                 .requires(HARNESS)
                 .action(ArgAction::SetTrue),
+        )
+        .arg(
+            Arg::new("check-version")
+                .long("check-version")
+                .action(ArgAction::Set)
+                .help("Pass the kani version to the compiler to ensure cache coherence."),
         );
     #[cfg(feature = "unsound_experiments")]
     let app = crate::unsound_experiments::arg_parser::add_unsound_experiments_to_parser(app);

kani-driver/src/args.rs

@@ -113,6 +113,10 @@ pub struct KaniArgs {
     #[arg(long)]
     pub target_dir: Option<PathBuf>,
 
+    /// Force Kani to rebuild all packages before the verification.
+    #[arg(long)]
+    pub force_build: bool,
+
     /// Toggle between different styles of output
     #[arg(long, default_value = "regular", ignore_case = true, value_enum)]
     pub output_format: OutputFormat,

kani-driver/src/call_cargo.rs

@@ -51,9 +51,7 @@ impl KaniSession {
             .join("kani");
         let outdir = target_dir.join(build_target).join("debug/deps");
 
-        // Clean directory before building since we are unable to handle cache today.
-        // TODO: https://github.com/model-checking/kani/issues/1736
-        if target_dir.exists() {
+        if self.args.force_build && target_dir.exists() {
             fs::remove_dir_all(&target_dir)?;
         }
 

kani-driver/src/call_single_file.rs

@@ -66,7 +66,7 @@ impl KaniSession {
 
     /// These arguments are arguments passed to kani-compiler that are `kani` compiler specific.
     pub fn kani_compiler_flags(&self) -> Vec<String> {
-        let mut flags = vec![];
+        let mut flags = vec![check_version()];
 
         if self.args.debug {
             flags.push("--log-level=debug".into());
@@ -187,3 +187,11 @@ impl KaniSession {
 pub fn to_rustc_arg(kani_args: Vec<String>) -> String {
     format!(r#"-Cllvm-args={}"#, kani_args.join(" "))
 }
+
+/// Function that returns a `--check-version` argument to be added to the compiler flags.
+/// This is really just used to force the compiler to recompile everything from scratch when a user
+/// upgrades Kani. Cargo currently ignores the codegen backend version.
+/// See <https://github.com/model-checking/kani/issues/2140> for more context.
+fn check_version() -> String {
+    format!("--check-version={}", env!("CARGO_PKG_VERSION"))
+}

tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml

@@ -10,3 +10,16 @@ description = "Test that Kani correctly handle supported crate types"
 name = "lib"
 crate-type = ["lib", "rlib"]
 path = "../src/lib.rs"
+
+[package.metadata.kani.flags]
+# This test doesn't work with the cache due to naming conflict caused by
+# declaring ["lib", "rlib"] which is in fact redundant.
+# See https://github.com/rust-lang/cargo/issues/6313 for more details.
+#
+# This still works for a fresh build and it only prints a warning. Thus, we
+# force rebuild for now.
+#
+# Note that support for this case is deprecated. AFAIK, there is no plan to fix
+# cargo build cache for cases like this. Until then, we might as well check that
+# our support level matches cargo's.
+force-build = true

tests/script-based-pre/build-cache-bin/bin/Cargo.toml

@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "bin"
+version = "0.1.0"
+edition = "2021"

tests/script-based-pre/build-cache-bin/bin/src/lib.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn cover_bool() {
+    match kani::any() {
+        true => kani::cover!(true, "true"),
+        false => kani::cover!(true, "false"),
+    }
+}
+
+#[kani::proof]
+fn cover_option() {
+    match kani::any() {
+        Some(true) => kani::cover!(true, "true"),
+        Some(false) => kani::cover!(true, "false"),
+        None => kani::cover!(true, "none"),
+    }
+}

tests/script-based-pre/build-cache-bin/cache_works.expected

@@ -0,0 +1,21 @@
+Initial compilation
+target/initial.log:Compiled 1 crates
+target/initial.log:No harness verified
+Re-execute the same command
+target/same.log:Compiled 0 crates
+target/same.log:No harness verified
+Run with new arg that affects kani-driver workflow only
+target/driver_opt.log:Compiled 0 crates
+target/driver_opt.log:Checking harness cover_option...
+target/driver_opt.log:Checking harness cover_bool...
+target/driver_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new argument that affects compilation
+target/disable_checks.log:Compiled 1 crates
+target/disable_checks.log:Checking harness cover_option...
+target/disable_checks.log:Checking harness cover_bool...
+target/disable_checks.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with new dependency
+target/new_dep.log:Compiled 2 crates
+target/new_dep.log:Checking harness cover_option...
+target/new_dep.log:Checking harness cover_bool...
+target/new_dep.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.

tests/script-based-pre/build-cache-bin/cache_works.sh

@@ -0,0 +1,71 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Checks situations where running kani multiple times will work as expected when
+# the target crate is binary.
+#
+# The following checks should not trigger recompilation.
+# - Exact same input being invoked a second time.
+# - Different options that do not affect the compilation, only the Kani workt flow.
+# While the following should recompile the target.
+# - Pass a new argument that affects compilation
+# - Add a dependency
+set -e
+set -u
+
+ORIG=bin
+OUT_DIR=target
+MANIFEST=${OUT_DIR}/${ORIG}/Cargo.toml
+
+# Expects two arguments: "kani arguments" "output_file"
+function check_kani {
+    local args=$1
+    local log_file="${OUT_DIR}/$2"
+    # Run kani with the given arguments
+    if [ -z "${args}" ]
+    then
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            2>&1 | tee "${log_file}"
+    else
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            "${args}" 2>&1 | tee "${log_file}"
+    fi
+
+    # Print information about the generated log file.
+    # Check for occurrences of "Compiling" messages in the log files
+    local compiled=$(grep -c "Compiling" ${log_file})
+    echo "${log_file}:Compiled ${compiled} crates"
+
+    # Check which harnesses were verified
+    grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
+
+    # Check the verification summary
+    grep "successfully verified harnesses" -H ${log_file} || true
+}
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+mkdir -p ${OUT_DIR}
+# Move the original source to the output folder since it will be modified
+cp -r ${ORIG} ${OUT_DIR}
+
+echo "Initial compilation"
+check_kani --only-codegen initial.log
+
+echo "Re-execute the same command"
+check_kani --only-codegen same.log
+
+echo "Run with new arg that affects kani-driver workflow only"
+check_kani "" driver_opt.log
+
+echo "Run with a new argument that affects compilation"
+check_kani --no-assertion-reach-checks disable_checks.log
+
+echo "Run with new dependency"
+cargo new --lib ${OUT_DIR}/new_dep
+cargo add new_dep --manifest-path ${MANIFEST} --path ${OUT_DIR}/new_dep
+check_kani  --no-assertion-reach-checks new_dep.log
+
+# Try to leave a clean output folder at the end
+rm -rf ${OUT_DIR}

tests/script-based-pre/build-cache-bin/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: cache_works.sh
+expected: cache_works.expected

tests/script-based-pre/build-cache-dirty/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: rebuild.sh
+expected: rebuild.expected

tests/script-based-pre/build-cache-dirty/rebuild.expected

@@ -0,0 +1,23 @@
+Initial compilation
+omplete - 2 successfully verified harnesses, 0 failures, 2 total.
+target/initial.log:Compiled 2 crates
+target/initial.log:Checking harness check_u8_i16...
+target/initial.log:Checking harness check_u8_u32...
+target/initial.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new argument that affects compilation
+target/enable_checks.log:Compiled 2 crates
+target/enable_checks.log:Checking harness check_u8_i16...
+target/enable_checks.log:Checking harness check_u8_u32...
+target/enable_checks.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run after change to the source code
+target/changed_src.log:Compiled 1 crates
+target/changed_src.log:Checking harness noop_check...
+target/changed_src.log:Checking harness check_u8_i16...
+target/changed_src.log:Checking harness check_u8_u32...
+target/changed_src.log:Complete - 3 successfully verified harnesses, 0 failures, 3 total.
+Run with new dependency
+target/new_dep.log:Compiled 2 crates
+target/new_dep.log:Checking harness noop_check...
+target/new_dep.log:Checking harness check_u8_i16...
+target/new_dep.log:Checking harness check_u8_u32...
+target/new_dep.log:Complete - 3 successfully verified harnesses, 0 failures, 3 total.

tests/script-based-pre/build-cache-dirty/rebuild.sh

@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Checks situations where running kani multiple times should trigger a new build
+# The cases we cover here are:
+# - Pass a new argument that affects compilation
+# - Change the source code
+# - Add a dependency
+# Note: This should run in the folder where the script is.
+
+OUT_DIR=target
+MANIFEST=${OUT_DIR}/target_lib/Cargo.toml
+LIB_SRC=${OUT_DIR}/target_lib/src/lib.rs
+
+# Expects two arguments: "kani arguments" "output_file"
+function check_kani {
+    local args=$1
+    local log_file="${OUT_DIR}/$2"
+    # Run kani with the given arguments
+    if [ -z "${args}" ]
+    then
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            2>&1 | tee "${log_file}"
+    else
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            "${args}" 2>&1 | tee "${log_file}"
+    fi
+
+    # Print information about the generated log file.
+    # Check for occurrences of "Compiling" messages in the log files
+    local compiled=$(grep -c "Compiling" ${log_file})
+    echo "${log_file}:Compiled ${compiled} crates"
+
+    # Check which harnesses were verified
+    grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
+
+    # Check the verification summary
+    grep "successfully verified harnesses" -H ${log_file} || true
+}
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+mkdir -p ${OUT_DIR}
+
+# Copy the project so we don't make changes to the source code
+cp -r target_lib ${OUT_DIR}
+
+echo "Initial compilation"
+check_kani --no-assertion-reach-checks initial.log
+
+echo "Run with a new argument that affects compilation"
+check_kani "" enable_checks.log
+
+echo "Run after change to the source code"
+echo '
+#[kani::proof]
+fn noop_check() {}
+' >> ${LIB_SRC}
+check_kani "" changed_src.log
+
+echo "Run with new dependency"
+cargo new --lib ${OUT_DIR}/new_dep
+cargo add new_dep --manifest-path ${MANIFEST} --path ${OUT_DIR}/new_dep
+check_kani "" new_dep.log
+
+# Try to leave a clean output folder at the end
+rm -rf ${OUT_DIR}

tests/script-based-pre/build-cache-dirty/target_lib/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "target_lib"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+either = "1.8"

tests/script-based-pre/build-cache-dirty/target_lib/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! We don't use any of our dependencies to keep the test fast
+
+#[kani::proof]
+fn check_u8_u32() {
+    let before: u8 = kani::any();
+    let temp = before as u32;
+    let after: u8 = temp.try_into().unwrap();
+    assert_eq!(after, before);
+}
+
+#[kani::proof]
+fn check_u8_i16() {
+    let before: u8 = kani::any();
+    let temp = before as i16;
+    let after: u8 = temp.try_into().unwrap();
+    assert_eq!(after, before);
+}

tests/script-based-pre/build-cache-fresh/cache_works.expected

@@ -0,0 +1,16 @@
+Initial compilation
+target/initial.log:Compiled 1 crates
+target/initial.log:No harness verified
+Re-execute the same command
+target/same.log:Compiled 0 crates
+target/same.log:No harness verified
+Run with new arg that affects kani-driver workflow only
+target/driver_opt.log:Compiled 0 crates
+target/driver_opt.log:Checking harness cover_option...
+target/driver_opt.log:Checking harness cover_bool...
+target/driver_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new cbmc option
+target/cbmc_opt.log:Compiled 0 crates
+target/cbmc_opt.log:Checking harness cover_option...
+target/cbmc_opt.log:Checking harness cover_bool...
+target/cbmc_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.