Split compiler flags to avoid dependency recompilation

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]