Fix cargo invocations to only use pkg_args where appropriate (#3984)

## Summary

When we invoke `cargo rustc` in `kani-driver`, we have some options in a
`pkg_args` variable, and some in `kani_compiler_flags`. This PR removes
a couple of uses of `pkg_args` that should have really been
`kani_compiler_flags`, and provides documentation about the difference.

## Explanation
Hopefully the documentation in the code is sufficient to understand the
difference (please suggest changes if it's not!), but here's a longer
explanation:

`cargo kani` invokes [cargo
rustc](https://doc.rust-lang.org/cargo/commands/cargo-rustc.html),
described as follows:

> cargo rustc [options] [-- args]
> The specified target for the current package (or package specified by
-p if provided) will be compiled along with all of its dependencies. The
specified args will all be passed to the final compiler invocation, not
any of the dependencies.

Our `pkg_args` variable is what we provide for `-- args`, i.e., the
arguments that we want to provide to kani-compiler when it compiles the
package under verification, but *not its dependencies.*

The docs then say:

> To pass flags to all compiler processes spawned by Cargo, use the
RUSTFLAGS [environment
variable](https://doc.rust-lang.org/cargo/reference/environment-variables.html)

We use the `RUSTFLAGS` environment variable to provide the
`kani_compiler_flags` that should be passed when we invoke
`kani-compiler` on the package to verify *and its dependencies.*

So we should use `kani_compiler_flags` when the dependencies of the
target package should receive the flag, and `pkg_args` when it
shouldn't. I concluded that the only argument that it makes sense to
provide in `pkg_args` is `--reachability`, because when `--reachability`
isn't provided it defaults to `None`, which is the behavior we want.
(Otherwise, we'd run Kani harnesses that we find in dependencies, or if
autoharness is running, generate automatic harnesses for functions in
dependencies, neither of which we want). Dependencies can get all of the
other compiler arguments, since they don't do anything with them when
`--reachability=None` anyway.

## Commit by Commit

- `--no-assert-contracts` is already provided in `kani_compiler_flags`,
and never should have been in `pkg_args` in the first place.
- Having `--backend=llbc` as a `pkg_arg` means that it doesn't get
provided to dependencies, so that when we run Kani's compiler on
dependencies, we'd actually enter the cprover compiler interface. Move
it to compiler args so that it gets passed to the target crate and its
dependencies.
- Autoharness should also use `kani_compiler_flags`, but that involves a
larger refactor than I want to do this close to a release, so added a
TODO for now.
- Add documentation explaining the difference between `pkg_args` and
`kani_compiler_flags`.

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

Author: carolynzech

kani-compiler/src/kani_compiler.rs

@@ -111,6 +111,7 @@ impl Callbacks for KaniCompiler {
             let queries = self.queries.clone();
             move |_cfg| backend(queries)
         }));
+        // `kani-driver` passes the `kani-compiler` specific arguments through llvm-args, so extract them here.
         args.extend(config.opts.cg.llvm_args.iter().cloned());
         let args = Arguments::parse_from(args);
         init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. }));

kani-compiler/src/main.rs

@@ -72,10 +72,15 @@ fn main() {
 
 /// Return whether we should run our flavour of the compiler, and which arguments to pass to rustc.
 ///
-/// We add a `--kani-compiler` argument to run the Kani version of the compiler, which needs to be
+/// `kani-driver` adds a `--kani-compiler` argument to run the Kani version of the compiler, which needs to be
 /// filtered out before passing the arguments to rustc.
-///
 /// All other Kani arguments are today located inside `--llvm-args`.
+///
+/// This function returns `true` for rustc invocations that originate from our rustc / cargo rustc invocations in `kani-driver`.
+/// It returns `false` for rustc invocations that cargo adds in the process of executing the `kani-driver` rustc command.
+/// For example, if we are compiling a crate that has a build.rs file, cargo will compile and run that build script
+/// (c.f. https://doc.rust-lang.org/cargo/reference/build-scripts.html#life-cycle-of-a-build-script).
+/// The build script should be compiled with normal rustc, not the Kani compiler.
 pub fn is_kani_compiler(args: Vec<String>) -> (bool, Vec<String>) {
     assert!(!args.is_empty(), "Arguments should always include executable name");
     const KANI_COMPILER: &str = "--kani-compiler";

kani-driver/src/autoharness/mod.rs

@@ -154,6 +154,8 @@ impl KaniSession {
     }
 
     /// 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]) {
         for func in included {
             self.pkg_args

kani-driver/src/call_cargo.rs

@@ -182,14 +182,19 @@ crate-type = ["lib"]
             cargo_args.push("-v".into());
         }
 
-        // Arguments that will only be passed to the target package.
+        // Arguments that will only be passed to the target package (the package under verification)
+        // and not its dependencies, c.f. https://doc.rust-lang.org/cargo/commands/cargo-rustc.html.
+        // The difference between pkg_args and rustc_args is that rustc_args are also provided when
+        // we invoke rustc on the target package's dependencies.
+        // We do not provide the `--reachability` argument to dependencies so that it has the default value `None`
+        // (c.f. kani-compiler::args::ReachabilityType) and we skip codegen for the dependency.
+        // 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.)
         self.pkg_args.push(self.reachability_arg());
-        if let Some(backend_arg) = self.backend_arg() {
-            self.pkg_args.push(backend_arg);
-        }
-        if self.args.no_assert_contracts {
-            self.pkg_args.push("--no-assert-contracts".into());
-        }
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;

kani-driver/src/call_single_file.rs

@@ -53,9 +53,6 @@ impl KaniSession {
     ) -> Result<()> {
         let mut kani_args = self.kani_compiler_flags();
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
-            kani_args.push("--backend=llbc".into());
-        }
 
         let lib_path = lib_folder().unwrap();
         let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
@@ -100,14 +97,6 @@ impl KaniSession {
         to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())])
     }
 
-    pub fn backend_arg(&self) -> Option<String> {
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
-            Some(to_rustc_arg(vec!["--backend=llbc".into()]))
-        } else {
-            None
-        }
-    }
-
     /// 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![check_version()];
@@ -150,6 +139,10 @@ impl KaniSession {
             flags.push("--ub-check=uninit".into());
         }
 
+        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            flags.push("--backend=llbc".into());
+        }
+
         if self.args.print_llbc {
             flags.push("--print-llbc".into());
         }

kani-driver/src/session.rs

@@ -34,7 +34,7 @@ pub struct KaniSession {
     /// Automatically verify functions in the crate, in addition to running manual harnesses.
     pub auto_harness: bool,
 
-    /// The arguments that will be passed to the target package, i.e. kani_compiler.
+    /// The arguments that will be passed only to the target package, not its dependencies.
     pub pkg_args: Vec<String>,
 
     /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from