Add kani_core library placeholder and build logic (rust-lang#3227)

While at it, I also added a `--skip-libs` to skip rebuilding the Kani
libraries and standard library at every `cargo build-dev` execution.

We usually only need to rebuild the libraries when we make changes to
them or when we update the Rust toolchain. Rebuilding them can be quite
time consuming when you are making changes to Kani.

Towards rust-lang#3226 rust-lang#3153

Co-authored-by: Jaisurya Nanduri <[email protected]>

Author: celinval

Cargo.lock

@@ -468,6 +468,13 @@ dependencies = [
  "os_info",
 ]
 
+[[package]]
+name = "kani_core"
+version = "0.51.0"
+dependencies = [
+ "kani_macros",
+]
+
 [[package]]
 name = "kani_macros"
 version = "0.52.0"

Cargo.toml

@@ -43,6 +43,7 @@ members = [
   "kani-driver",
   "kani-compiler",
   "kani_metadata",
+  "library/kani_core",
 ]
 
 # This indicates what package to e.g. build with 'cargo build' without --workspace

library/kani_core/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "kani_core"
+version = "0.51.0"
+edition = "2021"
+license = "MIT OR Apache-2.0"
+publish = false
+
+[dependencies]
+kani_macros = { path = "../kani_macros", features = ["no_core"] }

library/kani_core/src/lib.rs

@@ -0,0 +1,5 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This is placeholder for the new `kani_core` library.
+#![feature(no_core)]

library/kani_macros/Cargo.toml

@@ -19,4 +19,7 @@ syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] }
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.
-rustc_private=true
+rustc_private = true
+
+[features]
+no_core = []

tools/build-kani/src/main.rs

@@ -19,7 +19,13 @@ fn main() -> Result<()> {
     let args = parser::ArgParser::parse();
 
     match args.subcommand {
-        parser::Commands::BuildDev(build_parser) => build_lib(&build_bin(&build_parser.args)?),
+        parser::Commands::BuildDev(build_parser) => {
+            let bin_folder = &build_bin(&build_parser.args)?;
+            if !build_parser.skip_libs {
+                build_lib(&bin_folder)?;
+            }
+            Ok(())
+        }
         parser::Commands::Bundle(bundle_parser) => {
             let version_string = bundle_parser.version;
             let kani_string = format!("kani-{version_string}");

tools/build-kani/src/parser.rs

@@ -17,6 +17,10 @@ pub struct BuildDevParser {
     /// Arguments to be passed down to cargo when building cargo binaries.
     #[clap(value_name = "ARG", allow_hyphen_values = true)]
     pub args: Vec<String>,
+    /// Do not re-build Kani libraries. Only use this if you know there has been no changes to Kani
+    /// libraries or the underlying Rust compiler.
+    #[clap(long)]
+    pub skip_libs: bool,
 }
 
 #[derive(Args, Debug, Eq, PartialEq)]

tools/build-kani/src/sysroot.rs

@@ -55,18 +55,29 @@ pub fn kani_playback_lib() -> PathBuf {
     path_buf!(kani_sysroot(), "playback/lib")
 }
 
+/// Returns the path to where Kani libraries for no_core is kept.
+pub fn kani_no_core_lib() -> PathBuf {
+    path_buf!(kani_sysroot(), "no_core/lib")
+}
+
 /// Returns the path to where Kani's pre-compiled binaries are stored.
 fn kani_sysroot_bin() -> PathBuf {
     path_buf!(kani_sysroot(), "bin")
 }
 
+/// Returns the build target
+fn build_target() -> &'static str {
+    env!("TARGET")
+}
+
 /// Build the `lib/` folder and `lib-playback/` for the new sysroot.
 /// - The `lib/` folder contains the sysroot for verification.
 /// - The `lib-playback/` folder contains the sysroot used for playback.
 pub fn build_lib(bin_folder: &Path) -> Result<()> {
     let compiler_path = bin_folder.join("kani-compiler");
     build_verification_lib(&compiler_path)?;
-    build_playback_lib(&compiler_path)
+    build_playback_lib(&compiler_path)?;
+    build_no_core_lib(&compiler_path)
 }
 
 /// Build the `lib/` folder for the new sysroot used during verification.
@@ -75,34 +86,40 @@ 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 --build-std"];
-    build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args)
+    let packages = ["std", "kani", "kani_macros"];
+    let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &compiler_args)?;
+    copy_artifacts(&artifacts, &kani_sysroot_lib(), true)
 }
 
 /// Build the `lib-playback/` folder that will be used during counter example playback.
 /// This will include Kani's libraries compiled with `concrete-playback` feature enabled.
 fn build_playback_lib(compiler_path: &Path) -> Result<()> {
     let extra_args =
         ["--features=std/concrete_playback,kani/concrete_playback", "-Z", "build-std=std,test"];
-    build_kani_lib(compiler_path, &kani_playback_lib(), &extra_args, &[])
+    let packages = ["std", "kani", "kani_macros"];
+    let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &[])?;
+    copy_artifacts(&artifacts, &kani_playback_lib(), true)
+}
+
+/// Build the no core library folder that will be used during std verification.
+fn build_no_core_lib(compiler_path: &Path) -> Result<()> {
+    let extra_args = ["--features=kani_macros/no_core"];
+    let packages = ["kani_core", "kani_macros"];
+    let artifacts = build_kani_lib(compiler_path, &packages, &extra_args, &[])?;
+    copy_artifacts(&artifacts, &kani_no_core_lib(), false)
 }
 
 fn build_kani_lib(
     compiler_path: &Path,
-    output_path: &Path,
+    packages: &[&str],
     extra_cargo_args: &[&str],
     extra_rustc_args: &[&str],
-) -> Result<()> {
+) -> Result<Vec<Artifact>> {
     // Run cargo build with -Z build-std
-    let target = env!("TARGET");
+    let target = build_target();
     let target_dir = env!("KANI_BUILD_LIBS");
     let args = [
         "build",
-        "-p",
-        "std",
-        "-p",
-        "kani",
-        "-p",
-        "kani_macros",
         "-Z",
         "unstable-options",
         "--target-dir",
@@ -137,6 +154,7 @@ fn build_kani_lib(
         .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f"))
         .env("RUSTC", compiler_path)
         .args(args)
+        .args(packages.iter().copied().flat_map(|pkg| ["-p", pkg]))
         .args(extra_cargo_args)
         .stdout(Stdio::piped())
         .spawn()
@@ -152,20 +170,24 @@ fn build_kani_lib(
     }
 
     // Create sysroot folder hierarchy.
-    copy_artifacts(&artifacts, output_path, target)
+    Ok(artifacts)
 }
 
 /// Copy all the artifacts to their correct place to generate a valid sysroot.
-fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, target: &str) -> Result<()> {
-    // Create sysroot folder hierarchy.
+fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, copy_std: bool) -> Result<()> {
+    // Create sysroot folder.
     sysroot_lib.exists().then(|| fs::remove_dir_all(sysroot_lib));
-    let std_path = path_buf!(&sysroot_lib, "rustlib", target, "lib");
-    fs::create_dir_all(&std_path).expect(&format!("Failed to create {std_path:?}"));
+    fs::create_dir_all(sysroot_lib)?;
 
     //  Copy Kani libraries into sysroot top folder.
     copy_libs(&artifacts, &sysroot_lib, &is_kani_lib);
+
     //  Copy standard libraries into rustlib/<target>/lib/ folder.
-    copy_libs(&artifacts, &std_path, &is_std_lib);
+    if copy_std {
+        let std_path = path_buf!(&sysroot_lib, "rustlib", build_target(), "lib");
+        fs::create_dir_all(&std_path).expect(&format!("Failed to create {std_path:?}"));
+        copy_libs(&artifacts, &std_path, &is_std_lib);
+    }
     Ok(())
 }