Split compiler flags to avoid dependency recompilation (#4211)

We currently pass all Kani options to `rustc` for use by the
`kani-compiler`. This means that the Cargo build cache will detect a
[compilation
fingerprint](https://doc.rust-lang.org/nightly/nightly-rustc/cargo/core/compiler/fingerprint/index.html)
change whenever these options change and have to fully recompile the
project (including all dependencies). However, for the majority of
options, this is wholly unnecessary, as they only affect our codegen of
the target crate once it’s already been lowered to MIR.

This PR now passes most of `kani-compiler`’s options only to the target
crate so that they don’t change how dependencies are built and we can
avoid their recompilation.

There are two exceptions:
- `--ignore-global-assembly`: this is needed even in dependencies
because [the check we
do](https://github.com/model-checking/kani/blob/2bdc9ba359ce26f80e6eb9b023b39266f726de8f/kani-compiler/src/kani_middle/mod.rs#L47-L60)
to detect global assembly happens even if we are skipping codegen.
- `--check-version`: this ensures we recompile everything when the user
upgrades Kani versions. While not strictly necessary, existing comments
understandably seem to want this behavior, and upgrades are rare enough
I don’t see it being a real issue.

Resolves #2230

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: AlexanderPortland

kani-driver/src/call_cargo.rs

@@ -77,10 +77,11 @@ crate-type = ["lib"]
     pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result<Vec<Artifact>> {
         let lib_path = lib_no_core_folder().unwrap();
         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());
+        rustc_args.push(to_rustc_arg(self.kani_compiler_local_flags()).into());
         // Ignore global assembly, since `compiler_builtins` has some.
-        rustc_args.push(to_rustc_arg(vec!["--ignore-global-asm".to_string()]).into());
+        rustc_args.push(
+            to_rustc_arg(vec!["--ignore-global-asm".to_string(), self.reachability_arg()]).into(),
+        );
 
         let mut cargo_args: Vec<OsString> = vec!["build".into()];
         cargo_args.append(&mut cargo_config_args());
@@ -145,7 +146,7 @@ crate-type = ["lib"]
 
         let lib_path = lib_folder().unwrap();
         let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
-        rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
+        rustc_args.push(to_rustc_arg(self.kani_compiler_dependency_flags()).into());
 
         let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
         if let Some(path) = &self.args.cargo.manifest_path {
@@ -192,10 +193,16 @@ crate-type = ["lib"]
         // This is the desired behavior because we only want to construct `CodegenUnits` for the target package;
         // i.e., if some dependency has harnesses, we don't want to run them.
 
-        // If you are adding a new `kani-compiler` argument, you likely want to put it `kani_compiler_flags()` instead,
-        // unless there a reason it shouldn't be passed to dependencies.
-        // (Note that at the time of writing, passing the other compiler args to dependencies is a no-op, since `--reachability=None` skips codegen anyway.)
-        let pkg_args = vec!["--".into(), self.reachability_arg()];
+        // If you are adding a new `kani-compiler` argument, you likely want to put it here, unless there is a specific
+        // reason it would be used in dependencies that are skipping reachability and codegen.
+        // Note that passing compiler args to dependencies is a currently no-op, since `--reachability=None` skips codegen
+        // anyway. However, this will cause unneeded recompilation of dependencies should those args change, and thus
+        // should be avoided if possible.
+        let mut kani_pkg_args = vec![self.reachability_arg()];
+        kani_pkg_args.extend(self.kani_compiler_local_flags());
+
+        // Convert package args to rustc args for passing
+        let pkg_args = vec!["--".into(), to_rustc_arg(kani_pkg_args)];
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;

kani-driver/src/call_single_file.rs

@@ -51,7 +51,7 @@ impl KaniSession {
         crate_name: &String,
         outdir: &Path,
     ) -> Result<()> {
-        let mut kani_args = self.kani_compiler_flags();
+        let mut kani_args = self.kani_compiler_local_flags();
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
 
         let lib_path = lib_folder().unwrap();
@@ -81,6 +81,7 @@ impl KaniSession {
         let mut cmd = Command::new(&self.kani_compiler);
         let kani_compiler_args = to_rustc_arg(kani_args);
         cmd.arg(kani_compiler_args).args(rustc_args);
+
         // This is only required for stable but is a no-op for nightly channels
         cmd.env("RUSTC_BOOTSTRAP", "1");
 
@@ -94,13 +95,26 @@ impl KaniSession {
 
     /// Create a compiler option that represents the reachability mode.
     pub fn reachability_arg(&self) -> String {
-        to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())])
+        format!("--reachability={}", self.reachability_mode())
     }
 
-    /// These arguments are arguments passed to kani-compiler that are `kani` compiler specific.
-    pub fn kani_compiler_flags(&self) -> Vec<String> {
+    /// The `kani-compiler`-specific arguments that should be passed when building all crates,
+    /// including dependencies.
+    pub fn kani_compiler_dependency_flags(&self) -> Vec<String> {
         let mut flags = vec![check_version()];
 
+        if self.args.ignore_global_asm {
+            flags.push("--ignore-global-asm".into());
+        }
+
+        flags
+    }
+
+    /// The `kani-compiler`-specific arguments that should be passed only to the local crate
+    /// being compiled.
+    pub fn kani_compiler_local_flags(&self) -> Vec<String> {
+        let mut flags = vec![];
+
         if self.args.common_args.debug {
             flags.push("--log-level=debug".into());
         } else if self.args.common_args.verbose {
@@ -116,9 +130,6 @@ impl KaniSession {
         if self.args.assertion_reach_checks() {
             flags.push("--assertion-reach-checks".into());
         }
-        if self.args.ignore_global_asm {
-            flags.push("--ignore-global-asm".into());
-        }
 
         if self.args.is_stubbing_enabled() {
             flags.push("--enable-stubbing".into());

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

@@ -1,14 +1,24 @@
 Initial compilation
-omplete - 2 successfully verified harnesses, 0 failures, 2 total.
+Complete - 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
+Run with a new argument that doesn't affect dependency compilation
+target/enable_checks.log:Compiled 1 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 with another new argument that doesn't affect dependency compilation
+target/no_assert_contracts.log:Compiled 1 crates
+target/no_assert_contracts.log:Checking harness check_u8_i16...
+target/no_assert_contracts.log:Checking harness check_u8_u32...
+target/no_assert_contracts.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new argument that affects dependency compilation
+target/ignore_asm.log:Compiled 2 crates
+target/ignore_asm.log:Checking harness check_u8_i16...
+target/ignore_asm.log:Checking harness check_u8_u32...
+target/ignore_asm.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...

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

@@ -24,7 +24,7 @@ function check_kani {
             2>&1 | tee "${log_file}"
     else
         cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
-            "${args}" 2>&1 | tee "${log_file}"
+            ${args} 2>&1 | tee "${log_file}"
     fi
 
     # Print information about the generated log file.
@@ -49,9 +49,17 @@ 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 that most codegen flags only recompile the target crate
+echo "Run with a new argument that doesn't affect dependency compilation"
 check_kani "" enable_checks.log
 
+echo "Run with another new argument that doesn't affect dependency compilation"
+check_kani "-Z function-contracts --no-assert-contracts" no_assert_contracts.log
+
+# But ensure that specific ones recompile dependencies too
+echo "Run with a new argument that affects dependency compilation"
+check_kani "-Z unstable-options --ignore-global-asm" ignore_asm.log
+
 echo "Run after change to the source code"
 echo '
 #[kani::proof]