Add flag to the compiler to build std library (no user visible change) (rust-lang#2676)

Parts of the compiler relies on the existence of some constructs that are available in the standard library and Kani library. However, they aren't available when we are actually building the standard library (`std-lib-regression.sh`) and the Kani libraries (when building the sysroot with `cargo build-dev`).

Thus, we introduce a flag to inform the compiler that we are currently building the standard library. This flag can then be used to properly enable / disable sysroot dependent code.

Author: celinval

kani-compiler/src/kani_compiler.rs

@@ -395,6 +395,7 @@ impl Callbacks for KaniCompiler {
             queries.write_json_symtab =
                 cfg!(feature = "write_json_symtab") || matches.get_flag(parser::WRITE_JSON_SYMTAB);
             queries.reachability_analysis = matches.reachability_type();
+            queries.build_std = matches.get_flag(parser::BUILD_STD);
 
             if let Some(features) = matches.get_many::<String>(parser::UNSTABLE_FEATURE) {
                 queries.unstable_features = features.cloned().collect::<Vec<_>>();

kani-compiler/src/kani_middle/provide.rs

@@ -6,7 +6,7 @@
 
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::stubbing;
-use crate::kani_queries::QueryDb;
+use crate::kani_queries::{QueryDb, ReachabilityType};
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_interface;
 use rustc_middle::{
@@ -18,9 +18,13 @@ use rustc_middle::{
 /// Sets up rustc's query mechanism to apply Kani's custom queries to code from
 /// the present crate.
 pub fn provide(providers: &mut Providers, queries: &QueryDb) {
-    providers.optimized_mir = run_mir_passes;
-    if queries.stubbing_enabled {
-        providers.collect_and_partition_mono_items = collect_and_partition_mono_items;
+    if queries.reachability_analysis != ReachabilityType::None && !queries.build_std {
+        // Don't override queries if we are only compiling our dependencies.
+        providers.optimized_mir = run_mir_passes;
+        if queries.stubbing_enabled {
+            // TODO: Check if there's at least one stub being applied.
+            providers.collect_and_partition_mono_items = collect_and_partition_mono_items;
+        }
     }
 }
 

kani-compiler/src/kani_queries/mod.rs

@@ -37,6 +37,9 @@ pub struct QueryDb {
     pub reachability_analysis: ReachabilityType,
     pub stubbing_enabled: bool,
     pub unstable_features: Vec<String>,
+    /// Flag that indicates that we are currently building the standard library.
+    /// Note that `kani` library will not be available if this is `true`.
+    pub build_std: bool,
 
     /// Information about all target harnesses.
     pub harnesses_info: HashMap<DefPathHash, PathBuf>,

kani-compiler/src/parser.rs

@@ -49,6 +49,9 @@ pub const ENABLE_STUBBING: &str = "enable-stubbing";
 /// Option name used to define unstable features.
 pub const UNSTABLE_FEATURE: &str = "unstable";
 
+/// Option used for building standard library.
+pub const BUILD_STD: &str = "build-std";
+
 /// Configure command options for the Kani compiler.
 pub fn parser() -> Command {
     let app = command!()
@@ -152,6 +155,12 @@ pub fn parser() -> Command {
                 .help("Enable an unstable feature")
                 .value_name("UNSTABLE_FEATURE")
                 .action(ArgAction::Append),
+        )
+        .arg(
+            Arg::new(BUILD_STD)
+                .long(BUILD_STD)
+                .help("Enable building the standard library.")
+                .action(ArgAction::SetTrue),
         );
     app
 }

scripts/std-lib-regression.sh

@@ -74,6 +74,7 @@ RUST_FLAGS=(
     "-Cllvm-args=--goto-c"
     "-Cllvm-args=--ignore-global-asm"
     "-Cllvm-args=--reachability=pub_fns"
+    "-Cllvm-args=--build-std"
 )
 export RUSTFLAGS="${RUST_FLAGS[@]}"
 export RUSTC="$KANI_DIR/target/kani/bin/kani-compiler"

tools/build-kani/src/sysroot.rs

@@ -74,7 +74,7 @@ pub fn build_lib(bin_folder: &Path) -> Result<()> {
 fn build_verification_lib(compiler_path: &Path) -> Result<()> {
     let extra_args =
         ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""];
-    let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm"];
+    let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std"];
     build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args)
 }