move autoharness compiler flags to kani_compiler_flags

Carolyn Zech · Carolyn Zech · commit fda814bcdfad · 2025-04-17T13:01:28.000-04:00
diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs
@@ -9,7 +9,6 @@ use crate::args::autoharness_args::{
 };
 use crate::args::common::UnstableFeature;
 use crate::call_cbmc::VerificationStatus;
-use crate::call_single_file::to_rustc_arg;
 use crate::harness_runner::HarnessResult;
 use crate::list::collect_metadata::process_metadata;
 use crate::list::output::output_list_results;
@@ -151,23 +150,21 @@ fn print_skipped_table(table: &mut PrettyTable) {
 impl KaniSession {
     /// Enable autoharness mode.
     pub fn enable_autoharness(&mut self) {
-        self.auto_harness = true;
+        self.autoharness_compiler_flags = Some(vec![]);
         self.args.common_args.unstable_features.enable_feature(UnstableFeature::FunctionContracts);
         self.args.common_args.unstable_features.enable_feature(UnstableFeature::LoopContracts);
     }
 
     /// Add the compiler arguments specific to the `autoharness` subcommand.
-    /// TODO: this should really be appending onto the `kani_compiler_flags()` output instead of `pkg_args`.
-    /// It doesn't affect functionality since autoharness doesn't examine dependencies, but would still be better practice.
     pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) {
+        let mut args = vec![];
         for func in included {
-            self.pkg_args
-                .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)]));
+            args.push(format!("--autoharness-include-function {}", func));
         }
         for func in excluded {
-            self.pkg_args
-                .push(to_rustc_arg(vec![format!("--autoharness-exclude-function {}", func)]));
+            args.push(format!("--autoharness-exclude-function {}", func));
         }
+        self.autoharness_compiler_flags = Some(args);
     }
 
     /// Add global harness timeout and loop unwinding bounds if not provided.
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
@@ -194,7 +194,7 @@ crate-type = ["lib"]
         // 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.)
-        self.pkg_args.push(self.reachability_arg());
+        let pkg_args = vec!["--".into(), self.reachability_arg()];
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;
@@ -206,7 +206,7 @@ crate-type = ["lib"]
                 cmd.args(&cargo_args)
                     .args(vec!["-p", &package.id.to_string()])
                     .args(verification_target.to_args())
-                    .args(&self.pkg_args)
+                    .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
                     // https://doc.rust-lang.org/cargo/reference/environment-variables.html
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -151,6 +151,10 @@ impl KaniSession {
             flags.push("--no-assert-contracts".into());
         }
 
+        if let Some(args) = self.autoharness_compiler_flags.clone() {
+            flags.extend(args);
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
         flags
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
@@ -298,11 +298,11 @@ impl KaniSession {
             self.show_coverage_summary()?;
         }
 
-        if self.auto_harness {
+        if self.autoharness_compiler_flags.is_some() {
             self.print_autoharness_summary(automatic)?;
         }
 
-        if failing > 0 && !self.auto_harness {
+        if failing > 0 && self.autoharness_compiler_flags.is_none() {
             // Failure exit code without additional error message
             drop(self);
             std::process::exit(1);
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
@@ -31,11 +31,9 @@ pub struct KaniSession {
     /// The common command-line arguments
     pub args: VerificationArgs,
 
-    /// Automatically verify functions in the crate, in addition to running manual harnesses.
-    pub auto_harness: bool,
-
-    /// The arguments that will be passed only to the target package, not its dependencies.
-    pub pkg_args: Vec<String>,
+    /// The autoharness-specific compiler arguments.
+    /// Invariant: this field is_some() iff the autoharness subcommand is enabled.
+    pub autoharness_compiler_flags: Option<Vec<String>>,
 
     /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from
     /// a proof harness. Useful when attempting to verify things that were not annotated with kani
@@ -71,8 +69,7 @@ impl KaniSession {
 
         Ok(KaniSession {
             args,
-            auto_harness: false,
-            pkg_args: vec!["--".to_string()],
+            autoharness_compiler_flags: None,
             codegen_tests: false,
             kani_compiler: install.kani_compiler()?,
             kani_lib_c: install.kani_lib_c()?,
@@ -101,7 +98,7 @@ impl KaniSession {
     pub fn reachability_mode(&self) -> ReachabilityMode {
         if self.codegen_tests {
             ReachabilityMode::Tests
-        } else if self.auto_harness {
+        } else if self.autoharness_compiler_flags.is_some() {
             ReachabilityMode::AllFns
         } else {
             ReachabilityMode::ProofHarnesses

Original file line number	Diff line number	Diff line change
`@@ -151,6 +151,10 @@ impl KaniSession {`
`151`	`151`	`flags.push("--no-assert-contracts".into());`
`152`	`152`	`}`
`153`	`153`
	`154`	`+ if let Some(args) = self.autoharness_compiler_flags.clone() {`
	`155`	`+ flags.extend(args);`
	`156`	`+ }`
	`157`	`+`
`154`	`158`	`flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));`
`155`	`159`
`156`	`160`	`flags`
Original file line number	Diff line number	Diff line change
`@@ -298,11 +298,11 @@ impl KaniSession {`
`298`	`298`	`self.show_coverage_summary()?;`
`299`	`299`	`}`
`300`	`300`
`301`		`- if self.auto_harness {`
	`301`	`+ if self.autoharness_compiler_flags.is_some() {`
`302`	`302`	`self.print_autoharness_summary(automatic)?;`
`303`	`303`	`}`
`304`	`304`
`305`		`- if failing > 0 && !self.auto_harness {`
	`305`	`+ if failing > 0 && self.autoharness_compiler_flags.is_none() {`
`306`	`306`	`// Failure exit code without additional error message`
`307`	`307`	`drop(self);`
`308`	`308`	`std::process::exit(1);`