Move all rustc arguments to kani-driver (#2174)

Move all rustc arguments to kani-driver

1. It's good to have one source of truth.
2. This is needed for us to properly support caching compiler artifacts

Author: celinval

Cargo.lock

@@ -523,6 +523,8 @@ dependencies = [
  "rustc-demangle",
  "serde",
  "serde_json",
+ "strum",
+ "strum_macros",
  "toml",
  "tracing",
  "tracing-subscriber",

kani-compiler/src/main.rs

@@ -47,48 +47,9 @@ use rustc_hir::definitions::DefPathHash;
 use rustc_interface::Config;
 use rustc_session::config::ErrorOutputType;
 use session::json_panic_hook;
+use std::env;
 use std::ffi::OsStr;
-use std::path::PathBuf;
 use std::rc::Rc;
-use std::{env, fs};
-
-/// This function generates all rustc configurations required by our goto-c codegen.
-fn rustc_gotoc_flags(lib_path: &str) -> Vec<String> {
-    // The option below provides a mechanism by which definitions in the
-    // standard library can be overriden. See
-    // https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Globally.20override.20an.20std.20macro/near/268873354
-    // for more details.
-    let kani_std_rlib = PathBuf::from(lib_path).join("libstd.rlib");
-    let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
-    let args = vec![
-        "-C",
-        "overflow-checks=on",
-        "-C",
-        "panic=abort",
-        "-Z",
-        "unstable-options",
-        "-Z",
-        "panic_abort_tests=yes",
-        "-Z",
-        "trim-diagnostic-paths=no",
-        "-Z",
-        "human_readable_cgu_names",
-        "-Z",
-        "always-encode-mir",
-        "--cfg=kani",
-        "-Z",
-        "crate-attr=feature(register_tool)",
-        "-Z",
-        "crate-attr=register_tool(kanitool)",
-        "-L",
-        lib_path,
-        "--extern",
-        "kani",
-        "--extern",
-        kani_std_wrapper.as_str(),
-    ];
-    args.iter().map(|s| s.to_string()).collect()
-}
 
 /// Main function. Configure arguments and run the compiler.
 fn main() -> Result<(), &'static str> {
@@ -152,35 +113,9 @@ impl Callbacks for KaniCallbacks {
     }
 }
 
-/// The Kani root folder has all binaries inside bin/ and libraries inside lib/.
-/// This folder can also be used as a rustc sysroot.
-fn kani_root() -> PathBuf {
-    match env::current_exe() {
-        Ok(exe_path) => {
-            let mut path = fs::canonicalize(&exe_path).unwrap_or(exe_path);
-            // Current folder (bin/)
-            path.pop();
-            // Top folder
-            path.pop();
-            path
-        }
-        Err(e) => panic!("Failed to get current exe path: {e}"),
-    }
-}
-
 /// Generate the arguments to pass to rustc_driver.
 fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
     let mut rustc_args = vec![String::from("rustc")];
-    if args.get_flag(parser::GOTO_C) {
-        let mut default_path = kani_root();
-        default_path.push("lib");
-        let gotoc_args = rustc_gotoc_flags(
-            args.get_one::<String>(parser::KANI_LIB)
-                .unwrap_or(&default_path.to_str().unwrap().to_string()),
-        );
-        rustc_args.extend_from_slice(&gotoc_args);
-    }
-
     if args.get_flag(parser::RUSTC_VERSION) {
         rustc_args.push(String::from("--version"))
     }
@@ -192,9 +127,6 @@ fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
     if let Some(extra_flags) = args.get_raw(parser::RUSTC_OPTIONS) {
         extra_flags.for_each(|arg| rustc_args.push(convert_arg(arg)));
     }
-    let sysroot = sysroot_path(args);
-    rustc_args.push(String::from("--sysroot"));
-    rustc_args.push(convert_arg(sysroot.as_os_str()));
     tracing::debug!(?rustc_args, "Compile");
     rustc_args
 }
@@ -205,72 +137,6 @@ fn convert_arg(arg: &OsStr) -> String {
     arg.to_str().expect(format!("[Error] Cannot parse argument \"{arg:?}\".").as_str()).to_string()
 }
 
-/// Get the sysroot, for our specific version of Rust nightly.
-///
-/// Rust normally finds its sysroot by looking at where itself (the `rustc`
-/// executable) is located. This will fail for us because we're `kani-compiler`
-/// and not located under the rust sysroot.
-///
-/// We do know the actual name of the toolchain we need, however.
-/// We look for our toolchain in the usual place for rustup.
-///
-/// We previously used to pass `--sysroot` in `KANIFLAGS` from `kani-driver`,
-/// but this failed to have effect when building a `build.rs` file.
-/// This wasn't used anywhere but passing down here, so we've just migrated
-/// the code to find the sysroot path directly into this function.
-///
-/// This function will soon be removed.
-#[deprecated]
-fn toolchain_sysroot_path() -> PathBuf {
-    // If we're installed normally, we'll find `$KANI/toolchain` as a symlink to our desired toolchain
-    {
-        let kani_root = kani_root();
-        let toolchain_path = kani_root.join("toolchain");
-        if toolchain_path.exists() {
-            return toolchain_path;
-        }
-    }
-
-    // rustup sets some environment variables during build, but this is not clearly documented.
-    // https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
-    // We're using RUSTUP_TOOLCHAIN here, which is going to be set by our `rust-toolchain.toml` file.
-    // This is a *compile-time* constant, not a dynamic lookup at runtime, so this is reliable.
-    let toolchain = env!("RUSTUP_TOOLCHAIN");
-
-    // We use the home crate to do a *runtime* determination of where rustup toolchains live
-    let rustup = home::rustup_home().expect("Couldn't find RUSTUP_HOME");
-    let path = rustup.join("toolchains").join(toolchain);
-
-    if !path.exists() {
-        panic!("Couldn't find Kani Rust toolchain {toolchain}. Tried: {}", path.display());
-    }
-    path
-}
-
-/// Get the sysroot relative to the binary location.
-///
-/// Kani uses a custom sysroot. The `std` library and dependencies are compiled in debug mode and
-/// include the entire MIR definitions needed by Kani.
-///
-/// We do provide a `--sysroot` option that users may want to use instead.
-#[allow(deprecated)]
-fn sysroot_path(args: &ArgMatches) -> PathBuf {
-    let sysroot_arg = args.get_one::<String>(parser::SYSROOT);
-    let path = if let Some(s) = sysroot_arg {
-        PathBuf::from(s)
-    } else if !args.get_flag(parser::GOTO_C) {
-        toolchain_sysroot_path()
-    } else {
-        kani_root()
-    };
-
-    if !path.exists() {
-        panic!("Couldn't find Kani Rust toolchain {:?}.", path.display());
-    }
-    tracing::debug!(?path, ?sysroot_arg, "Sysroot path.");
-    path
-}
-
 /// Find the stub mapping for the given harness.
 ///
 /// This function is necessary because Kani currently allows a harness to be

kani-driver/Cargo.toml

@@ -32,6 +32,8 @@ rustc-demangle = "0.1.21"
 pathdiff = "0.2.1"
 rayon = "1.5.3"
 comfy-table = "6.0.0"
+strum = {version = "0.24.0"}
+strum_macros = {version = "0.24.0"}
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
 tracing-tree = "0.2.2"

kani-driver/src/call_cargo.rs

@@ -2,11 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::KaniArgs;
-use crate::session::{KaniSession, ReachabilityMode};
+use crate::session::KaniSession;
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{Message, Metadata, MetadataCommand, Package};
-use std::ffi::OsString;
+use std::ffi::{OsStr, OsString};
 use std::fs;
 use std::io::BufReader;
 use std::path::{Path, PathBuf};
@@ -58,8 +58,9 @@ impl KaniSession {
             fs::remove_dir_all(&target_dir)?;
         }
 
-        let mut kani_args = self.kani_specific_flags();
-        let rustc_args = self.kani_rustc_flags();
+        let kani_args = self.kani_compiler_flags();
+        let mut rustc_args = self.kani_rustc_flags();
+        rustc_args.push("--kani-flags".into());
 
         let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
         if let Some(path) = &self.args.cargo.manifest_path {
@@ -99,21 +100,8 @@ impl KaniSession {
         }
 
         // Arguments that will only be passed to the target package.
-        let mut pkg_args: Vec<OsString> = vec![];
-        match self.reachability_mode() {
-            ReachabilityMode::ProofHarnesses => {
-                pkg_args.extend(["--".into(), "--reachability=harnesses".into()]);
-            }
-            ReachabilityMode::AllPubFns => {
-                pkg_args.extend(["--".into(), "--reachability=pub_fns".into()]);
-            }
-            ReachabilityMode::Tests => {
-                pkg_args.extend(["--".into(), "--reachability=tests".into()]);
-            }
-        }
-
-        // Only joing them at the end. All kani flags must come first.
-        kani_args.extend_from_slice(&rustc_args);
+        let mut pkg_args: Vec<String> = vec![];
+        pkg_args.extend(["--".to_string(), format!("--reachability={}", self.reachability_mode())]);
 
         let mut found_target = false;
         let packages = packages_to_verify(&self.args, &metadata);
@@ -125,8 +113,10 @@ impl KaniSession {
                     .args(&target.to_args())
                     .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
-                    .env("RUSTFLAGS", "--kani-flags")
-                    .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "))
+                    .env("KANIFLAGS", kani_args.join(" "))
+                    // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
+                    // https://doc.rust-lang.org/cargo/reference/environment-variables.html
+                    .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
                     .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
                 self.run_cargo(cmd)?;

kani-driver/src/call_single_file.rs

@@ -6,7 +6,7 @@ use std::ffi::OsString;
 use std::path::Path;
 use std::process::Command;
 
-use crate::session::{KaniSession, ReachabilityMode};
+use crate::session::{base_folder, lib_folder, KaniSession};
 
 impl KaniSession {
     /// Used by `kani` and not `cargo-kani` to process a single Rust file into a `.symtab.json`
@@ -17,15 +17,8 @@ impl KaniSession {
         crate_name: &String,
         outdir: &Path,
     ) -> Result<()> {
-        let mut kani_args = self.kani_specific_flags();
-        kani_args.push(
-            match self.reachability_mode() {
-                ReachabilityMode::ProofHarnesses => "--reachability=harnesses",
-                ReachabilityMode::AllPubFns => "--reachability=pub_fns",
-                ReachabilityMode::Tests => "--reachability=tests",
-            }
-            .into(),
-        );
+        let mut kani_args = self.kani_compiler_flags();
+        kani_args.push(format!("--reachability={}", self.reachability_mode()));
 
         let mut rustc_args = self.kani_rustc_flags();
         rustc_args.push(file.into());
@@ -65,10 +58,9 @@ impl KaniSession {
         Ok(())
     }
 
-    /// These arguments are arguments passed to kani-compiler that are `kani` specific.
-    /// These are also used by call_cargo to pass as the env var KANIFLAGS.
-    pub fn kani_specific_flags(&self) -> Vec<OsString> {
-        let mut flags = vec![OsString::from("--goto-c")];
+    /// 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![];
 
         if self.args.debug {
             flags.push("--log-level=debug".into());
@@ -93,19 +85,57 @@ impl KaniSession {
             flags.push("--enable-stubbing".into());
         }
         if let Some(harness) = &self.args.harness {
-            flags.push(format!("--harness={harness}").into());
+            flags.push(format!("--harness={harness}"));
         }
 
+        // This argument will select the Kani flavour of the compiler. It will be removed before
+        // rustc driver is invoked.
+        flags.push("--goto-c".into());
+
         #[cfg(feature = "unsound_experiments")]
         flags.extend(self.args.unsound_experiments.process_args());
 
         flags
     }
 
-    /// These arguments are arguments passed to kani-compiler that are `rustc` specific.
-    /// These are also used by call_cargo to pass as the env var KANIFLAGS.
+    /// This function generates all rustc configurations required by our goto-c codegen.
     pub fn kani_rustc_flags(&self) -> Vec<OsString> {
-        let mut flags = Vec::<OsString>::new();
+        let lib_path = lib_folder().unwrap();
+        let kani_std_rlib = lib_path.join("libstd.rlib");
+        let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
+        let sysroot = base_folder().unwrap();
+        let args = vec![
+            "-C",
+            "overflow-checks=on",
+            "-C",
+            "panic=abort",
+            "-C",
+            "symbol-mangling-version=v0",
+            "-Z",
+            "unstable-options",
+            "-Z",
+            "panic_abort_tests=yes",
+            "-Z",
+            "trim-diagnostic-paths=no",
+            "-Z",
+            "human_readable_cgu_names",
+            "-Z",
+            "always-encode-mir",
+            "--cfg=kani",
+            "-Z",
+            "crate-attr=feature(register_tool)",
+            "-Z",
+            "crate-attr=register_tool(kanitool)",
+            "--sysroot",
+            sysroot.to_str().unwrap(),
+            "-L",
+            lib_path.to_str().unwrap(),
+            "--extern",
+            "kani",
+            "--extern",
+            kani_std_wrapper.as_str(),
+        ];
+        let mut flags: Vec<_> = args.iter().map(OsString::from).collect();
         if self.args.use_abs {
             flags.push("-Z".into());
             flags.push("force-unstable-if-unmarked=yes".into()); // ??
@@ -124,9 +154,6 @@ impl KaniSession {
             }
         }
 
-        flags.push("-C".into());
-        flags.push("symbol-mangling-version=v0".into());
-
         // e.g. compiletest will set 'compile-flags' here and we should pass those down to rustc
         // and we fail in `tests/kani/Match/match_bool.rs`
         if let Ok(str) = std::env::var("RUSTFLAGS") {