Build custom sysroot with --always-encode-mir on (rust-lang#1717)

* Build sysroot and repurpose make-kani-release

This change builds a custom sysroot for Kani. This new sysroot will contain a "lib/" folder with Kani libraries as well as the standard libraries compiled with --always-encode-mir. This enable us to fully traverse the std MIR and fix the missing functions errors.

Other changes to the build were described in the issue here: rust-lang#1605 (comment)

* Add pre-compiled libraries to the bundle.

The size of the bundle did increase quite a bit on my linux machine. It went from 24MB to 67MB.

This is still pretty far from GitHub's max size of 2GB:
https://docs.github.com/en/repositories/releasing-projects-on-github/about-releases#storage-and-bandwidth-quotas

Author: celinval

.cargo/config.toml

@@ -1,6 +1,26 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+# Command aliases
+[alias]
+# Build kani with development configuration.
+build-dev = "run -p build-kani -- build-dev"
+# Build kani release bundle.
+bundle = "run -p build-kani -- bundle"
+
+# Constants used by different processes.
+# These constants should be evaluated during compilation via `env!()`.
+[env]
+# Path to the repository root.
+KANI_REPO_ROOT={value = "", relative = true}
+# Path to the sysroot build. This folder will contain a bin/ and a lib/ folder.
+KANI_SYSROOT ={value = "target/kani", relative = true}
+# Target for building Kani's libraries. Their configuration is different than the binary build, so we must use
+# something different than regular `target/`.
+KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
+# Build Kani library without `build-std`.
+KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
+
 [target.'cfg(all())']
 rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
 

.github/workflows/kani.yml

@@ -28,7 +28,7 @@ jobs:
           os: ${{ matrix.os }}
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
@@ -47,7 +47,7 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
@@ -64,7 +64,7 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani using release mode
-        run: cargo build --release
+        run: cargo build-dev -- --release
 
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
@@ -83,7 +83,7 @@ jobs:
           os: ubuntu-20.04
 
       - name: Build Kani
-        run: cargo build
+        run: cargo build-dev
 
       - name: Install book runner dependencies
         run: ./scripts/setup/install_bookrunner_deps.sh
@@ -133,7 +133,7 @@ jobs:
 
       - name: Build release bundle
         run: |
-          cargo run -p make-kani-release -- latest
+          cargo bundle -- latest
           cargo package -p kani-verifier
 
       - name: Build container test

.github/workflows/release.yml

@@ -80,7 +80,7 @@ jobs:
 
       - name: Build release bundle
         run: |
-          cargo run -p make-kani-release -- ${{ needs.Release.outputs.version }}
+          cargo bundle
 
       - name: Upload artifact
         uses: actions/upload-release-asset@v1
@@ -113,7 +113,7 @@ jobs:
 
       - name: 'Build release bundle'
         run: |
-          cargo run -p make-kani-release -- ${{ needs.Release.outputs.version }}
+          cargo bundle
           cargo package -p kani-verifier
 
       - name: 'Login to GitHub Container Registry'

Cargo.lock

@@ -89,6 +89,16 @@ dependencies = [
  "walkdir",
 ]
 
+[[package]]
+name = "build-kani"
+version = "0.11.0"
+dependencies = [
+ "anyhow",
+ "cargo_metadata",
+ "clap 3.2.22",
+ "which",
+]
+
 [[package]]
 name = "camino"
 version = "1.1.1"
@@ -135,12 +145,51 @@ dependencies = [
  "ansi_term",
  "atty",
  "bitflags",
- "strsim",
- "textwrap",
+ "strsim 0.8.0",
+ "textwrap 0.11.0",
  "unicode-width",
  "vec_map",
 ]
 
+[[package]]
+name = "clap"
+version = "3.2.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "86447ad904c7fb335a790c9d7fe3d0d971dc523b8ccd1561a520de9a85302750"
+dependencies = [
+ "atty",
+ "bitflags",
+ "clap_derive",
+ "clap_lex",
+ "indexmap",
+ "once_cell",
+ "strsim 0.10.0",
+ "termcolor",
+ "textwrap 0.15.1",
+]
+
+[[package]]
+name = "clap_derive"
+version = "3.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ea0c8bce528c4be4da13ea6fead8965e95b6073585a2f05204bd8f4119f82a65"
+dependencies = [
+ "heck 0.4.0",
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "clap_lex"
+version = "0.2.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2850f2f5a82cbf437dd5af4d49848fbdfc27c157c3d010345776f952765261c5"
+dependencies = [
+ "os_str_bytes",
+]
+
 [[package]]
 name = "compiletest"
 version = "0.0.0"
@@ -312,7 +361,7 @@ dependencies = [
  "ar",
  "atty",
  "bitflags",
- "clap",
+ "clap 2.34.0",
  "cprover_bindings",
  "home",
  "kani_metadata",
@@ -337,7 +386,7 @@ version = "0.11.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
- "clap",
+ "clap 2.34.0",
  "console",
  "glob",
  "kani_metadata",
@@ -426,14 +475,6 @@ dependencies = [
  "cfg-if",
 ]
 
-[[package]]
-name = "make-kani-release"
-version = "0.1.0"
-dependencies = [
- "anyhow",
- "which",
-]
-
 [[package]]
 name = "matchers"
 version = "0.1.0"
@@ -553,6 +594,12 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "os_str_bytes"
+version = "6.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9ff7415e9ae3fff1225851df9e0d9e4e5479f947619774677a63572e55e80eff"
+
 [[package]]
 name = "parking_lot"
 version = "0.12.1"
@@ -810,13 +857,19 @@ version = "0.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
 
+[[package]]
+name = "strsim"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
+
 [[package]]
 name = "structopt"
 version = "0.3.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0c6b5c64445ba8094a6ab0c3cd2ad323e07171012d9c98b0b15651daf1787a10"
 dependencies = [
- "clap",
+ "clap 2.34.0",
  "lazy_static",
  "structopt-derive",
 ]
@@ -864,6 +917,15 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "termcolor"
+version = "1.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755"
+dependencies = [
+ "winapi-util",
+]
+
 [[package]]
 name = "terminal_size"
 version = "0.1.17"
@@ -883,6 +945,12 @@ dependencies = [
  "unicode-width",
 ]
 
+[[package]]
+name = "textwrap"
+version = "0.15.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "949517c0cf1bf4ee812e2e07e08ab448e3ae0d23472aee8a06c985f0c8815b16"
+
 [[package]]
 name = "thread_local"
 version = "1.1.4"

Cargo.toml

@@ -40,7 +40,7 @@ members = [
   "library/std",
   "tools/bookrunner",
   "tools/compiletest",
-  "tools/make-kani-release",
+  "tools/build-kani",
   "kani-driver",
   "kani-compiler",
   "kani_metadata",

deny.toml

@@ -31,7 +31,7 @@ allow = [
 allow-osi-fsf-free = "neither"
 confidence-threshold = 0.8
 
-# All these exceptions should probably appear in: tools/make-kani-release/license-notes.txt
+# All these exceptions should probably appear in: tools/build-kani/license-notes.txt
 exceptions = [
     { name = "Inflector", allow=["BSD-2-Clause"] },
     { name = "unicode-ident", allow=["Unicode-DFS-2016"] },

kani-compiler/build.rs

@@ -3,7 +3,6 @@
 
 use std::env;
 use std::path::PathBuf;
-use std::process::Command;
 
 macro_rules! path_str {
     ($input:expr) => {
@@ -17,34 +16,6 @@ macro_rules! path_str {
     };
 }
 
-/// Build the target library, and setup cargo to rerun them if the source has changed.
-fn setup_lib(out_dir: &str, lib_out: &str, lib: &str) {
-    let kani_lib = vec!["..", "library", lib];
-    println!("cargo:rerun-if-changed={}", path_str!(kani_lib));
-
-    let mut kani_lib_toml = kani_lib;
-    kani_lib_toml.push("Cargo.toml");
-    let args = [
-        "build",
-        "--manifest-path",
-        &path_str!(kani_lib_toml),
-        "-Z",
-        "unstable-options",
-        "--out-dir",
-        lib_out,
-        "--target-dir",
-        out_dir,
-    ];
-    let result = Command::new("cargo")
-        .env("CARGO_ENCODED_RUSTFLAGS", "--cfg=kani")
-        .args(args)
-        .status()
-        .unwrap();
-    if !result.success() {
-        std::process::exit(1);
-    }
-}
-
 /// Configure the compiler to build kani-compiler binary. We currently support building
 /// kani-compiler with nightly only. We also link to the rustup rustc_driver library for now.
 pub fn main() {
@@ -58,12 +29,4 @@ pub fn main() {
     // in a relative location for a symlink to the local rust toolchain
     let origin = if cfg!(target_os = "macos") { "@loader_path" } else { "$ORIGIN" };
     println!("cargo:rustc-link-arg-bin=kani-compiler=-Wl,-rpath,{}/../toolchain/lib", origin);
-
-    // Compile kani library and export KANI_LIB_PATH variable with its relative location.
-    let out_dir = env::var("OUT_DIR").unwrap();
-    let lib_out = path_str!([&out_dir, "lib"]);
-    setup_lib(&out_dir, &lib_out, "kani");
-    setup_lib(&out_dir, &lib_out, "kani_macros");
-    setup_lib(&out_dir, &lib_out, "std");
-    println!("cargo:rustc-env=KANI_LIB_PATH={}", lib_out);
 }