Add --mir-linker flag and wire it up to the compiler (rust-lang#1652)

Since the MIR linker hasn't been hooked up yet, the compiler will fail
if this option is selected as shown by the new tests.

Author: celinval

Cargo.lock

@@ -380,6 +380,8 @@ dependencies = [
 name = "kani_queries"
 version = "0.10.0"
 dependencies = [
+ "strum",
+ "strum_macros",
  "tracing",
 ]
 

kani-compiler/kani_queries/Cargo.toml

@@ -13,3 +13,6 @@ unsound_experiments = []
 
 [dependencies]
 tracing = {version = "0.1"}
+strum = {version = "0.24.0"}
+strum_macros = {version = "0.24.0"}
+

kani-compiler/kani_queries/src/lib.rs

@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use std::sync::atomic::{AtomicBool, Ordering};
+#[cfg(not(feature = "unsound_experiments"))]
+use std::sync::Mutex;
+use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 
 #[cfg(feature = "unsound_experiments")]
 mod unsound_experiments;
@@ -12,6 +15,25 @@ use {
     std::sync::{Arc, Mutex},
 };
 
+#[derive(Debug, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
+#[strum(serialize_all = "snake_case")]
+pub enum ReachabilityType {
+    /// Start the cross-crate reachability analysis from all harnesses in the local crate.
+    Harnesses,
+    /// Use standard rustc monomorphizer algorithm.
+    Legacy,
+    /// Don't perform any reachability analysis. This will skip codegen for this crate.
+    None,
+    /// Start the cross-crate reachability analysis from all public functions in the local crate.
+    PubFns,
+}
+
+impl Default for ReachabilityType {
+    fn default() -> Self {
+        ReachabilityType::None
+    }
+}
+
 pub trait UserInput {
     fn set_symbol_table_passes(&mut self, passes: Vec<String>);
     fn get_symbol_table_passes(&self) -> Vec<String>;
@@ -28,6 +50,9 @@ pub trait UserInput {
     fn set_ignore_global_asm(&mut self, global_asm: bool);
     fn get_ignore_global_asm(&self) -> bool;
 
+    fn set_reachability_analysis(&mut self, reachability: ReachabilityType);
+    fn get_reachability_analysis(&self) -> ReachabilityType;
+
     #[cfg(feature = "unsound_experiments")]
     fn get_unsound_experiments(&self) -> Arc<Mutex<UnsoundExperiments>>;
 }
@@ -39,6 +64,7 @@ pub struct QueryDb {
     symbol_table_passes: Vec<String>,
     json_pretty_print: AtomicBool,
     ignore_global_asm: AtomicBool,
+    reachability_analysis: Mutex<ReachabilityType>,
     #[cfg(feature = "unsound_experiments")]
     unsound_experiments: Arc<Mutex<UnsoundExperiments>>,
 }
@@ -84,6 +110,14 @@ impl UserInput for QueryDb {
         self.ignore_global_asm.load(Ordering::Relaxed)
     }
 
+    fn set_reachability_analysis(&mut self, reachability: ReachabilityType) {
+        *self.reachability_analysis.get_mut().unwrap() = reachability;
+    }
+
+    fn get_reachability_analysis(&self) -> ReachabilityType {
+        *self.reachability_analysis.lock().unwrap()
+    }
+
     #[cfg(feature = "unsound_experiments")]
     fn get_unsound_experiments(&self) -> Arc<Mutex<UnsoundExperiments>> {
         self.unsound_experiments.clone()

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -8,7 +8,7 @@ use bitflags::_core::any::Any;
 use cbmc::goto_program::{symtab_transformer, Location};
 use cbmc::InternedString;
 use kani_metadata::KaniMetadata;
-use kani_queries::{QueryDb, UserInput};
+use kani_queries::{QueryDb, ReachabilityType, UserInput};
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
 use rustc_data_structures::fx::FxHashMap;
@@ -60,7 +60,7 @@ impl CodegenBackend for GotocCodegenBackend {
         super::utils::init();
 
         check_target(tcx.sess);
-        check_options(tcx.sess, need_metadata_module);
+        check_options(tcx.sess, need_metadata_module, self.queries.clone());
 
         let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1;
         let mut c = GotocCtx::new(tcx, self.queries.clone());
@@ -246,7 +246,7 @@ fn check_target(session: &Session) {
     session.abort_if_errors();
 }
 
-fn check_options(session: &Session, need_metadata_module: bool) {
+fn check_options(session: &Session, need_metadata_module: bool, queries: Rc<QueryDb>) {
     // The requirements for `min_global_align` and `endian` are needed to build
     // a valid CBMC machine model in function `machine_model_from_session` from
     // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -281,6 +281,14 @@ fn check_options(session: &Session, need_metadata_module: bool) {
         session.err("Kani cannot generate metadata module.");
     }
 
+    if queries.get_reachability_analysis() != ReachabilityType::Legacy {
+        let err_msg = format!(
+            "Using {} reachability mode is still unsupported.",
+            queries.get_reachability_analysis().as_ref()
+        );
+        session.err(&err_msg);
+    }
+
     session.abort_if_errors();
 }
 

kani-compiler/src/main.rs

@@ -33,12 +33,13 @@ mod unsound_experiments;
 
 use crate::session::init_session;
 use clap::ArgMatches;
-use kani_queries::{QueryDb, UserInput};
+use kani_queries::{QueryDb, ReachabilityType, UserInput};
 use rustc_driver::{Callbacks, RunCompiler};
 use std::env;
 use std::ffi::OsStr;
 use std::path::PathBuf;
 use std::rc::Rc;
+use std::str::FromStr as _;
 
 /// This function generates all rustc configurations required by our goto-c codegen.
 fn rustc_gotoc_flags(lib_path: &str) -> Vec<String> {
@@ -91,6 +92,9 @@ fn main() -> Result<(), &'static str> {
     queries.set_check_assertion_reachability(matches.is_present(parser::ASSERTION_REACH_CHECKS));
     queries.set_output_pretty_json(matches.is_present(parser::PRETTY_OUTPUT_FILES));
     queries.set_ignore_global_asm(matches.is_present(parser::IGNORE_GLOBAL_ASM));
+    queries.set_reachability_analysis(
+        ReachabilityType::from_str(matches.value_of(parser::REACHABILITY).unwrap()).unwrap(),
+    );
     #[cfg(feature = "unsound_experiments")]
     crate::unsound_experiments::arg_parser::add_unsound_experiment_args_to_queries(
         &mut queries,

kani-compiler/src/parser.rs

@@ -5,7 +5,9 @@ use clap::{
     app_from_crate, crate_authors, crate_description, crate_name, crate_version, App, AppSettings,
     Arg,
 };
+use kani_queries::ReachabilityType;
 use std::env;
+use strum::VariantNames as _;
 
 /// Option name used to set log level.
 pub const LOG_LEVEL: &str = "log-level";
@@ -40,6 +42,10 @@ pub const IGNORE_GLOBAL_ASM: &str = "ignore-global-asm";
 /// Option name used to override the sysroot.
 pub const SYSROOT: &str = "sysroot";
 
+/// Option name used to select which reachability analysis to perform.
+pub const REACHABILITY: &str = "reachability";
+pub const REACHABILITY_FLAG: &str = "--reachability";
+
 /// Option name used to pass extra rustc-options.
 pub const RUSTC_OPTIONS: &str = "rustc-options";
 
@@ -133,6 +139,14 @@ pub fn parser<'a, 'b>() -> App<'a, 'b> {
                 .long("--assertion-reach-checks")
                 .help("Check the reachability of every assertion."),
         )
+        .arg(
+            Arg::with_name(REACHABILITY)
+                .long(REACHABILITY_FLAG)
+                .possible_values(ReachabilityType::VARIANTS)
+                .required(false)
+                .default_value(ReachabilityType::None.as_ref())
+                .help("Selects the type of reachability analysis to perform."),
+        )
         .arg(
             Arg::with_name(PRETTY_OUTPUT_FILES)
                 .long("--pretty-json-files")
@@ -162,14 +176,24 @@ pub fn command_arguments(args: &Vec<String>) -> Vec<String> {
     assert!(!args.is_empty(), "Arguments should always include executable name");
     let has_kani_flags = args.iter().any(|arg| arg.eq(KANI_ARGS_FLAG));
     if has_kani_flags {
+        let mut filter_args = vec![KANI_ARGS_FLAG];
         let mut new_args: Vec<String> = Vec::new();
         new_args.push(args[0].clone());
+        // For cargo kani, --reachability is included as a rustc argument.
+        let reachability = args.iter().find(|arg| arg.starts_with(REACHABILITY_FLAG));
+        if let Some(value) = reachability {
+            new_args.push(value.clone());
+            filter_args.push(value)
+        }
+        // Add all the other kani specific arguments are inside $KANIFLAGS.
         let env_flags = env::var(KANIFLAGS_ENV_VAR).unwrap_or_default();
         new_args.extend(
             shell_words::split(&env_flags)
                 .expect(&format!("Cannot parse {} value '{}'", KANIFLAGS_ENV_VAR, env_flags)),
         );
-        new_args.extend(args[1..].iter().filter(|&arg| arg.ne(KANI_ARGS_FLAG)).cloned());
+        // Add the leftover arguments for rustc at the end.
+        new_args
+            .extend(args[1..].iter().filter(|&arg| !filter_args.contains(&arg.as_str())).cloned());
         new_args
     } else {
         args.clone()

kani-driver/src/args.rs

@@ -121,14 +121,19 @@ pub struct KaniArgs {
     /// Kani will only compile the crate. No verification will be performed
     #[structopt(long, hidden_short_help(true))]
     pub only_codegen: bool,
+    /// Enables experimental MIR Linker. This option will affect how Kani prunes the code to be
+    /// analyzed. Please report any missing function issue found here:
+    /// <https://github.com/model-checking/kani/issues/new/choose>
+    #[structopt(long, hidden = true, requires("enable-unstable"))]
+    pub mir_linker: bool,
     /// Compiles Kani harnesses in all features of all packages selected on the command-line.
     #[structopt(long)]
     pub all_features: bool,
     /// Run Kani on all packages in the workspace.
     #[structopt(long)]
     pub workspace: bool,
     /// Run Kani on the specified packages.
-    #[structopt(long, short)]
+    #[structopt(long, short, conflicts_with("workspace"))]
     pub package: Vec<String>,
 
     /// Specify the value used for loop unwinding in CBMC

kani-driver/src/call_cargo.rs

@@ -1,14 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use crate::args::KaniArgs;
+use crate::session::KaniSession;
 use anyhow::{Context, Result};
-use cargo_metadata::MetadataCommand;
+use cargo_metadata::{Metadata, MetadataCommand};
 use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
-use crate::session::KaniSession;
-
 /// The outputs of kani-compiler being invoked via cargo on a project.
 pub struct CargoOutputs {
     /// The directory where compiler outputs should be directed.
@@ -22,66 +22,67 @@ pub struct CargoOutputs {
     pub metadata: Vec<PathBuf>,
 }
 
-/// Finds the "target" directory while considering workspaces,
-fn find_target_dir() -> PathBuf {
-    fn maybe_get_target() -> Option<PathBuf> {
-        Some(MetadataCommand::new().exec().ok()?.target_directory.into())
-    }
-
-    maybe_get_target().unwrap_or(PathBuf::from("target"))
-}
-
 impl KaniSession {
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
     pub fn cargo_build(&self) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
-        let target_dir = self.args.target_dir.as_ref().unwrap_or(&find_target_dir()).clone();
+        let metadata = MetadataCommand::new().exec().expect("Failed to get cargo metadata.");
+        let target_dir = self
+            .args
+            .target_dir
+            .as_ref()
+            .unwrap_or(&metadata.target_directory.clone().into())
+            .clone();
         let outdir = target_dir.join(build_target).join("debug/deps");
 
-        let flag_env = {
-            let rustc_args = self.kani_rustc_flags();
-            crate::util::join_osstring(&rustc_args, " ")
-        };
-
-        let mut args: Vec<OsString> = Vec::new();
+        let mut kani_args = self.kani_specific_flags();
+        let rustc_args = self.kani_rustc_flags();
 
+        let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
         if self.args.tests {
-            args.push("test".into());
-            args.push("--no-run".into());
-        } else {
-            args.push("build".into());
-        }
-
-        for package in self.args.package.iter() {
-            args.push("--package".into());
-            args.push(package.into());
+            cargo_args.push("--tests".into());
         }
 
         if self.args.all_features {
-            args.push("--all-features".into());
+            cargo_args.push("--all-features".into());
         }
 
-        if self.args.workspace {
-            args.push("--workspace".into());
-        }
-
-        args.push("--target".into());
-        args.push(build_target.into());
+        cargo_args.push("--target".into());
+        cargo_args.push(build_target.into());
 
-        args.push("--target-dir".into());
-        args.push(target_dir.into());
+        cargo_args.push("--target-dir".into());
+        cargo_args.push(target_dir.into());
 
         if self.args.verbose {
-            args.push("-v".into());
+            cargo_args.push("-v".into());
+        }
+
+        // Arguments that will only be passed to the target package.
+        let mut pkg_args: Vec<OsString> = vec![];
+        if self.args.mir_linker {
+            // Only provide reachability flag to the target package.
+            pkg_args.push("--".into());
+            pkg_args.push("--reachability=harnesses".into());
+        } else {
+            // Pass legacy reachability to the target package and its dependencies.
+            kani_args.push("--reachability=legacy".into());
         }
 
-        let mut cmd = Command::new("cargo");
-        cmd.args(args)
-            .env("RUSTC", &self.kani_compiler)
-            .env("RUSTFLAGS", "--kani-flags")
-            .env("KANIFLAGS", flag_env);
+        // Only joing them at the end. All kani flags must come first.
+        kani_args.extend_from_slice(&rustc_args);
 
-        self.run_terminal(cmd)?;
+        let members = project_members(&self.args, &metadata);
+        for member in members {
+            let mut cmd = Command::new("cargo");
+            cmd.args(&cargo_args)
+                .args(vec!["-p", &member])
+                .args(&pkg_args)
+                .env("RUSTC", &self.kani_compiler)
+                .env("RUSTFLAGS", "--kani-flags")
+                .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "));
+
+            self.run_terminal(cmd)?;
+        }
 
         if self.args.dry_run {
             // mock an answer: mostly the same except we don't/can't expand the globs
@@ -110,3 +111,23 @@ fn glob(path: &Path) -> Result<Vec<PathBuf>> {
     let v: core::result::Result<Vec<PathBuf>, glob::GlobError> = results.collect();
     Ok(v?)
 }
+
+/// Extract the packages that should be verified.
+/// If --package <pkg> is given, return the list of packages selected.
+/// If --workspace is given, return the list of workspace members.
+/// If no argument provided, return the root package if there's one or all members.
+///   - I.e.: Do whatever cargo does when there's no default_members.
+///   - This is because `default_members` is not available in cargo metadata.
+///     See <https://github.com/rust-lang/cargo/issues/8033>.
+fn project_members(args: &KaniArgs, metadata: &Metadata) -> Vec<String> {
+    if !args.package.is_empty() {
+        args.package.clone()
+    } else {
+        match (args.workspace, metadata.root_package()) {
+            (true, _) | (_, None) => {
+                metadata.workspace_members.iter().map(|id| metadata[id].name.clone()).collect()
+            }
+            (_, Some(root_pkg)) => vec![root_pkg.name.clone()],
+        }
+    }
+}