diff --git a/.cargo/config.toml b/.cargo/config.toml index 6bfcaf40f56b..949746371898 100644 --- a/.cargo/config.toml +++ b/.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 -. diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 02788247388e..a522002e6697 100644 --- a/.github/workflows/kani.yml +++ b/.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 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index bf112bb3e6d3..6e0c2a6b8e75 100644 --- a/.github/workflows/release.yml +++ b/.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' diff --git a/Cargo.lock b/Cargo.lock index 9176b3a22fe2..23500d2ee906 100644 --- a/Cargo.lock +++ b/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" diff --git a/Cargo.toml b/Cargo.toml index f9b7a452295f..ced77ccb9e1c 100644 --- a/Cargo.toml +++ b/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", diff --git a/deny.toml b/deny.toml index 48cf1e625356..39be523ebd19 100644 --- a/deny.toml +++ b/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"] }, diff --git a/kani-compiler/build.rs b/kani-compiler/build.rs index c42fc62a55b8..f48a0a669828 100644 --- a/kani-compiler/build.rs +++ b/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); } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 3e0cf14ef3e6..d8aac04bd50d 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -31,15 +31,15 @@ mod parser; mod session; mod unsound_experiments; +use crate::parser::KaniCompilerParser; use crate::session::init_session; use clap::ArgMatches; 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 _; +use std::{env, fs}; /// This function generates all rustc configurations required by our goto-c codegen. fn rustc_gotoc_flags(lib_path: &str) -> Vec { @@ -94,9 +94,7 @@ 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(), - ); + queries.set_reachability_analysis(matches.reachability_type()); #[cfg(feature = "unsound_experiments")] crate::unsound_experiments::arg_parser::add_unsound_experiment_args_to_queries( &mut queries, @@ -128,12 +126,35 @@ struct KaniCallbacks {} /// Use default function implementations. 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 { - let gotoc_args = - rustc_gotoc_flags(args.value_of(parser::KANI_LIB).unwrap_or(std::env!("KANI_LIB_PATH"))); let mut rustc_args = vec![String::from("rustc")]; if args.is_present(parser::GOTO_C) { + let mut default_path = kani_root(); + if args.reachability_type() == ReachabilityType::Legacy { + default_path.push("legacy-lib") + } else { + default_path.push("lib"); + } + let gotoc_args = rustc_gotoc_flags( + args.value_of(parser::KANI_LIB).unwrap_or(default_path.to_str().unwrap()), + ); rustc_args.extend_from_slice(&gotoc_args); } @@ -148,7 +169,7 @@ fn generate_rustc_args(args: &ArgMatches) -> Vec { if let Some(extra_flags) = args.values_of_os(parser::RUSTC_OPTIONS) { extra_flags.for_each(|arg| rustc_args.push(convert_arg(arg))); } - let sysroot = sysroot_path(args.value_of(parser::SYSROOT)); + 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"); @@ -170,34 +191,53 @@ fn convert_arg(arg: &OsStr) -> String { /// and not located under the rust sysroot. /// /// We do know the actual name of the toolchain we need, however. -/// So if we don't have `--sysroot`, then we look for our toolchain -/// in the usual place for rustup. +/// 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. -fn sysroot_path(sysroot_arg: Option<&str>) -> PathBuf { +/// +/// This function will soon be removed. +#[deprecated] +fn toolchain_sysroot_path() -> PathBuf { // 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 {}. Tried: {}", toolchain, 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.value_of(parser::SYSROOT); let path = if let Some(s) = sysroot_arg { PathBuf::from(s) + } else if args.reachability_type() == ReachabilityType::Legacy + || !args.is_present(parser::GOTO_C) + { + toolchain_sysroot_path() } else { - // 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"); - rustup.join("toolchains").join(toolchain) + kani_root() }; - // If we ever have a problem with the above not being good enough, we can consider a third heuristic - // for finding our sysroot: readlink() on `../toolchain` from the location of our executable. - // At time of writing this would only work for release, not development, however, so I'm not going - // with this option yet. It would eliminate the need for the `home` crate however. if !path.exists() { - panic!("Couldn't find Kani Rust toolchain {}. Tried: {}", toolchain, path.display()); + panic!("Couldn't find Kani Rust toolchain {:?}.", path.display()); } tracing::debug!(?path, ?sysroot_arg, "Sysroot path."); path diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index 09addb28a9ee..a9e5742024b3 100644 --- a/kani-compiler/src/parser.rs +++ b/kani-compiler/src/parser.rs @@ -3,10 +3,11 @@ use clap::{ app_from_crate, crate_authors, crate_description, crate_name, crate_version, App, AppSettings, - Arg, + Arg, ArgMatches, }; use kani_queries::ReachabilityType; use std::env; +use std::str::FromStr; use strum::VariantNames as _; /// Option name used to set log level. @@ -163,6 +164,17 @@ pub fn parser<'a, 'b>() -> App<'a, 'b> { app } +pub trait KaniCompilerParser { + fn reachability_type(&self) -> ReachabilityType; +} + +impl<'a> KaniCompilerParser for ArgMatches<'a> { + fn reachability_type(&self) -> ReachabilityType { + self.value_of(REACHABILITY) + .map_or(ReachabilityType::None, |arg| ReachabilityType::from_str(arg).unwrap()) + } +} + /// Retrieves the arguments from the command line and process hack to incorporate CARGO arguments. /// /// The kani-compiler requires the flags related to the kani libraries to be diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 5282d52804c0..a72d49933247 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -106,11 +106,6 @@ impl KaniSession { pub fn kani_specific_flags(&self) -> Vec { let mut flags = vec![OsString::from("--goto-c")]; - if let Some(rlib) = &self.kani_rlib { - flags.push("--kani-lib".into()); - flags.push(rlib.into()); - } - if self.args.debug { flags.push("--log-level=debug".into()); } else if self.args.verbose { diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 2387a612ac60..bc27c244563c 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -21,9 +21,6 @@ pub struct KaniSession { /// The location we found the Kani C stub .c files pub kani_c_stubs: PathBuf, - /// The location we found our pre-built libraries - pub kani_rlib: Option, - /// The temporary files we littered that need to be cleaned up at the end of execution pub temporaries: RefCell>, } @@ -33,7 +30,7 @@ enum InstallType { /// We're operating in a a checked out repo that's been built locally. /// The path here is to the root of the repo. DevRepo(PathBuf), - /// We're operating from a release bundle (made with `make-kani-release`). + /// We're operating from a release bundle (made with `build-kani release`). /// The path here to where this release bundle has been unpacked. Release(PathBuf), } @@ -47,7 +44,6 @@ impl KaniSession { kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, kani_c_stubs: install.kani_c_stubs()?, - kani_rlib: install.kani_rlib()?, temporaries: RefCell::new(vec![]), }) } @@ -168,9 +164,10 @@ fn bin_folder() -> Result { impl InstallType { pub fn new() -> Result { - // Case 1: We've checked out the development repo and we're built under `target/` + // Case 1: We've checked out the development repo and we're built under `target/kani` let mut path = bin_folder()?; - if path.ends_with("target/debug") || path.ends_with("target/release") { + if path.ends_with("target/kani/bin") { + path.pop(); path.pop(); path.pop(); @@ -209,21 +206,6 @@ impl InstallType { self.base_path_with("library/kani/stubs/C") } - pub fn kani_rlib(&self) -> Result> { - match self { - Self::DevRepo(_repo) => { - // Awkwardly, there is not an easy way to determine the location of these outputs - // So we let kani-compiler default to hard-coding them for development builds. - Ok(None) - } - Self::Release(release) => { - // First-time setup should place these here. Note `lib` not `library` for built artifacts. - let path = release.join("lib"); - Ok(Some(expect_path(path)?)) - } - } - } - /// A common case is that our repo and release bundle have the same `subpath` fn base_path_with(&self, subpath: &str) -> Result { let path = match self { diff --git a/scripts/cargo-kani b/scripts/cargo-kani index 14b91dfbecc1..b3f85af666d1 100755 --- a/scripts/cargo-kani +++ b/scripts/cargo-kani @@ -8,15 +8,14 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" REPO_DIR="$(dirname $SCRIPT_DIR)" shopt -s nullglob -KANI_CANDIDATES=("$REPO_DIR"/target/*/kani-driver) +KANI_DRIVER="$REPO_DIR/target/kani/bin/kani-driver" -if [[ -z ${KANI_CANDIDATES:-""} ]] || [[ ${#KANI_CANDIDATES[@]} -ne 1 ]] +if [[ ! -x ${KANI_DRIVER} ]] then echo "ERROR: Could not find kani-driver binary." - echo "Looked for: '$REPO_DIR/target/*/kani-driver'" + echo "Looked for: '${KANI_DRIVER}'" echo "Was Kani successfully built first?" exit 1 fi -KANI_PATH=${KANI_CANDIDATES[0]} -exec -a cargo-kani "${KANI_PATH}" "$@" +exec -a cargo-kani "${KANI_DRIVER}" "$@" diff --git a/scripts/ci/copyright-exclude b/scripts/ci/copyright-exclude index e041186de4e1..5c823691b4bc 100644 --- a/scripts/ci/copyright-exclude +++ b/scripts/ci/copyright-exclude @@ -17,4 +17,4 @@ ignore kani-dependencies scripts/ci/copyright-exclude tests/remote-target-lists/.* -tools/make-kani-release/license-notes.txt +tools/build-kani/license-notes.txt diff --git a/scripts/kani b/scripts/kani index 1ed225b2cb8d..6b1106e39d0e 100755 --- a/scripts/kani +++ b/scripts/kani @@ -8,15 +8,14 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" REPO_DIR="$(dirname $SCRIPT_DIR)" shopt -s nullglob -KANI_CANDIDATES=("$REPO_DIR"/target/*/kani-driver) +KANI_DRIVER="$REPO_DIR/target/kani/bin/kani-driver" -if [[ -z ${KANI_CANDIDATES:-""} ]] || [[ ${#KANI_CANDIDATES[@]} -ne 1 ]] +if [[ ! -x ${KANI_DRIVER} ]] then echo "ERROR: Could not find kani-driver binary." - echo "Looked for: '$REPO_DIR/target/*/kani-driver'" + echo "Looked for: '${KANI_DRIVER}'" echo "Was Kani successfully built first?" exit 1 fi -KANI_PATH=${KANI_CANDIDATES[0]} -exec -a kani "${KANI_PATH}" "$@" +exec -a kani "${KANI_DRIVER}" "$@" diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh index 8590545324b0..96144487f916 100755 --- a/scripts/kani-perf.sh +++ b/scripts/kani-perf.sh @@ -9,7 +9,7 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" KANI_DIR=$SCRIPT_DIR/.. # Build Kani using release mode. -cargo build --release +cargo build-dev -- --release PERF_DIR="${KANI_DIR}/tests/perf" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 19e8c5bfec34..487389260533 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -30,9 +30,9 @@ ${SCRIPT_DIR}/kani-fmt.sh --check # Build all packages in the workspace if [[ "" != "${KANI_ENABLE_UNSOUND_EXPERIMENTS-}" ]]; then - cargo build --features unsound_experiments + cargo build-dev -- --features unsound_experiments else - cargo build + cargo build-dev fi # Unit tests diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index c53b8d67a081..2fe517a1d9ab 100755 --- a/scripts/std-lib-regression.sh +++ b/scripts/std-lib-regression.sh @@ -69,7 +69,7 @@ export RUST_BACKTRACE=1 export RUSTC_LOG=error export KANIFLAGS="--goto-c --ignore-global-asm --reachability=legacy" export RUSTFLAGS="--kani-flags" -export RUSTC="$KANI_DIR/target/debug/kani-compiler" +export RUSTC="$KANI_DIR/target/kani/bin/kani-compiler" # Compile rust to iRep $WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET diff --git a/src/setup.rs b/src/setup.rs index e369b0ef12e2..af1dd13c682d 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -36,22 +36,20 @@ pub fn setup(use_local_bundle: Option) -> Result<()> { let kani_dir = kani_dir(); let os = os_info::get(); - println!("[0/6] Running Kani first-time setup..."); + println!("[0/5] Running Kani first-time setup..."); - println!("[1/6] Ensuring the existence of: {}", kani_dir.display()); + println!("[1/5] Ensuring the existence of: {}", kani_dir.display()); std::fs::create_dir_all(&kani_dir)?; setup_kani_bundle(&kani_dir, use_local_bundle)?; - let toolchain_version = setup_rust_toolchain(&kani_dir)?; + setup_rust_toolchain(&kani_dir)?; setup_python_deps(&kani_dir, &os)?; - setup_build_kani_prelude(&kani_dir, toolchain_version)?; - os_hacks::setup_os_hacks(&kani_dir, &os)?; - println!("[6/6] Successfully completed Kani first-time setup."); + println!("[5/5] Successfully completed Kani first-time setup."); Ok(()) } @@ -62,7 +60,7 @@ fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option) -> Res let base_dir = kani_dir.parent().expect("No base directory?"); if let Some(pathstr) = use_local_bundle { - println!("[2/6] Installing local Kani bundle: {}", pathstr.to_string_lossy()); + println!("[2/5] Installing local Kani bundle: {}", pathstr.to_string_lossy()); let path = Path::new(&pathstr).canonicalize()?; // When given a local bundle, it's often "-latest" but we expect "-1.0" or something. // tar supports "stripping" the first directory from the bundle, so do that and @@ -75,7 +73,7 @@ fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option) -> Res .run()?; } else { let filename = download_filename(); - println!("[2/6] Downloading Kani release bundle: {}", &filename); + println!("[2/5] Downloading Kani release bundle: {}", &filename); fail_if_unsupported_target()?; let bundle = base_dir.join(filename); Command::new("curl") @@ -97,7 +95,7 @@ fn setup_rust_toolchain(kani_dir: &Path) -> Result { // Currently this means we require the bundle to have been unpacked first! let toolchain_version = std::fs::read_to_string(kani_dir.join("rust-toolchain-version")) .context("Reading release bundle rust-toolchain-version")?; - println!("[3/6] Installing rust toolchain version: {}", &toolchain_version); + println!("[3/5] Installing rust toolchain version: {}", &toolchain_version); Command::new("rustup").args(&["toolchain", "install", &toolchain_version]).run()?; let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); @@ -108,7 +106,7 @@ fn setup_rust_toolchain(kani_dir: &Path) -> Result { /// Install into the pyroot the python dependencies we need fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> { - println!("[4/6] Installing Kani python dependencies..."); + println!("[4/5] Installing Kani python dependencies..."); let pyroot = kani_dir.join("pyroot"); // TODO: this is a repetition of versions from kani/kani-dependencies @@ -132,46 +130,6 @@ fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> { Ok(()) } -/// Build the Kani prelude libaries locally -fn setup_build_kani_prelude(kani_dir: &Path, toolchain_version: String) -> Result<()> { - println!("[5/6] Building Kani library prelude..."); - // We need a workspace to build them in, otherwise repeated builds generate different hashes and `kani` can't find `kani_macros` - let contents = "[workspace]\nmembers = [\"kani\",\"kani_macros\",\"std\"]"; - std::fs::write(kani_dir.join("library").join("Cargo.toml"), contents)?; - - // A little helper for invoking Cargo repeatedly here - let cargo = |crate_name: &str| -> Result<()> { - let manifest = format!("library/{}/Cargo.toml", crate_name); - Command::new("cargo") - .args(&[ - &format!("+{}", toolchain_version), - "build", - "-Z", - "unstable-options", - "--manifest-path", - &manifest, - "--out-dir", - "lib", - "--target-dir", - "target", - ]) - .current_dir(&kani_dir) - // https://doc.rust-lang.org/cargo/reference/environment-variables.html - .env("CARGO_ENCODED_RUSTFLAGS", "--cfg=kani") - .run() - .with_context(|| format!("Failed to build Kani prelude library {}", crate_name)) - }; - - // We seem to need 3 invocations because of the behavior of the `--out-dir` flag. - // It only seems to produce the requested artifact, not its dependencies. - cargo("kani")?; - cargo("kani_macros")?; - cargo("std")?; - - std::fs::remove_dir_all(kani_dir.join("target"))?; - Ok(()) -} - // This ends the setup steps above. // // Just putting a bit of space between that and the helper functions below. diff --git a/tests/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/kani/Strings/copy_empty_string_by_intrinsic.rs index 2585b25f7dd8..a0c1bef7d003 100644 --- a/tests/kani/Strings/copy_empty_string_by_intrinsic.rs +++ b/tests/kani/Strings/copy_empty_string_by_intrinsic.rs @@ -1,7 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Make sure we can handle explicit copy_nonoverlapping on empty string +// kani-flags: --enable-unstable --mir-linker +//! Make sure we can handle explicit copy_nonoverlapping on empty string +//! This used to trigger an issue: https://github.com/model-checking/kani/issues/241 #![feature(rustc_private)] @@ -21,6 +23,12 @@ fn copy_string(s: &str, l: usize) { // Copy let src = from_raw_parts(s.as_ptr(), l).as_ptr(); copy_nonoverlapping(src, dest, l); + + // The chunk below causes the 3 failures at the top of the file + // Back to str, check length + let dest_slice: &[u8] = from_raw_parts(dest, l); + let dest_as_str: &str = str::from_utf8(dest_slice).unwrap(); + assert!(dest_as_str.len() == l); } } diff --git a/tests/kani/Strings/copy_empty_string_by_intrinsic_fixme.rs b/tests/kani/Strings/copy_empty_string_by_intrinsic_fixme.rs deleted file mode 100644 index ce95b5a8f043..000000000000 --- a/tests/kani/Strings/copy_empty_string_by_intrinsic_fixme.rs +++ /dev/null @@ -1,45 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Make sure we can handle explicit copy_nonoverlapping on empty string - -// TODO: https://github.com/model-checking/kani/issues/241 -// The copy_nonoverlapping succeeds, but the final copy back to a slice -// fails: -// [...copy_empty_string_by_intrinsic.assertion.2] line 1035 unreachable code: FAILURE -// [...copy_empty_string_by_intrinsic.assertion.1] line 1037 a panicking function std::result::unwrap_failed is invoked: FAILURE -// [...copy_string.assertion.2] line 28 assertion failed: dest_as_str.len() == l: FAILURE - -#![feature(rustc_private)] - -extern crate libc; - -use std::mem::size_of; -use std::ptr::copy_nonoverlapping; -use std::slice::from_raw_parts; -use std::str; - -fn copy_string(s: &str, l: usize) { - unsafe { - // Unsafe buffer - let size: libc::size_t = size_of::(); - let dest: *mut u8 = libc::malloc(size * l) as *mut u8; - - // Copy - let src = from_raw_parts(s.as_ptr(), l).as_ptr(); - copy_nonoverlapping(src, dest, l); - - // The chunk below causes the 3 failures at the top of the file - // Back to str, check length - let dest_slice: &[u8] = from_raw_parts(dest, l); - let dest_as_str: &str = str::from_utf8(dest_slice).unwrap(); - assert!(dest_as_str.len() == l); - } -} - -#[kani::proof] -fn main() { - // Verification fails for both of these cases. - copy_string("x", 1); - copy_string("", 0); -} diff --git a/tests/ui/mir-linker/expected b/tests/perf/string/expected similarity index 100% rename from tests/ui/mir-linker/expected rename to tests/perf/string/expected diff --git a/tests/ui/mir-linker/any_str.rs b/tests/perf/string/src/any_str.rs similarity index 89% rename from tests/ui/mir-linker/any_str.rs rename to tests/perf/string/src/any_str.rs index c70edf4598b5..3b58d56750a7 100644 --- a/tests/ui/mir-linker/any_str.rs +++ b/tests/perf/string/src/any_str.rs @@ -7,9 +7,9 @@ //! I.e.: Currently, this should fail with missing function definition. #[kani::proof] -#[kani::unwind(12)] +#[kani::unwind(4)] fn check_abs() { - let data: [u8; 8] = kani::any(); + let data: [u8; 3] = kani::any(); let mut string = String::from_utf8_lossy(&data).to_string(); let new_len = kani::any(); kani::assume(new_len <= 2); diff --git a/tools/bookrunner/src/util.rs b/tools/bookrunner/src/util.rs index 69f8a92d5104..a3bfbebf625f 100644 --- a/tools/bookrunner/src/util.rs +++ b/tools/bookrunner/src/util.rs @@ -149,7 +149,7 @@ pub fn parse_test_header(path: &Path) -> TestProps { /// Adds Kani to the current `PATH` environment variable. pub fn add_kani_to_path() { let cwd = env::current_dir().unwrap(); - let kani_bin = cwd.join("target").join("debug"); + let kani_bin = cwd.join("target").join("kani").join("bin"); let kani_scripts = cwd.join("scripts"); env::set_var( "PATH", diff --git a/tools/make-kani-release/Cargo.toml b/tools/build-kani/Cargo.toml similarity index 52% rename from tools/make-kani-release/Cargo.toml rename to tools/build-kani/Cargo.toml index 7f3fb7ce8f24..54a6a67cf4a3 100644 --- a/tools/make-kani-release/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -2,13 +2,15 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "make-kani-release" -version = "0.1.0" +name = "build-kani" +version = "0.11.0" edition = "2021" -description = "Contructs a Kani release bundle" +description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" publish = false [dependencies] anyhow = "1" +cargo_metadata = "0.15.0" +clap = { version = "3.2", features=["derive"] } which = "4" diff --git a/tools/make-kani-release/build.rs b/tools/build-kani/build.rs similarity index 100% rename from tools/make-kani-release/build.rs rename to tools/build-kani/build.rs diff --git a/tools/make-kani-release/license-notes.txt b/tools/build-kani/license-notes.txt similarity index 100% rename from tools/make-kani-release/license-notes.txt rename to tools/build-kani/license-notes.txt diff --git a/tools/make-kani-release/src/main.rs b/tools/build-kani/src/main.rs similarity index 67% rename from tools/make-kani-release/src/main.rs rename to tools/build-kani/src/main.rs index 7356c71461fd..bf1c71246bdf 100644 --- a/tools/make-kani-release/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -4,43 +4,53 @@ //! This file is a glorified shell script for constructing a Kani release bundle. //! We use Rust here just to aid in making the "script" more robust. //! -//! Run with `cargo run -p make-kani-release -- ` and this will produce +//! Run with `cargo run -p build-kani -- release` and this will produce //! (e.g.) `kani-1.0-x86_64-unknown-linux-gnu.tar.gz`. -use std::{ffi::OsString, path::Path, process::Command}; +mod parser; +mod sysroot; +use crate::sysroot::{ + build_bin, build_lib, build_lib_legacy, kani_sysroot_legacy_lib, kani_sysroot_lib, +}; use anyhow::{bail, Result}; +use clap::Parser; +use std::{ffi::OsString, path::Path, process::Command}; fn main() -> Result<()> { - let version_string = parse_args()?; - let kani_string = format!("kani-{}", version_string); - let bundle_name = format!("{}-{}.tar.gz", kani_string, env!("TARGET")); - let dir = Path::new(&kani_string); + let args = parser::ArgParser::parse(); - // Check everything is ready before we start copying files - prebundle(dir)?; + match args.subcommand { + parser::Commands::BuildDev(build_parser) => { + build_lib(); + build_lib_legacy(); + build_bin(&build_parser.args); + } + parser::Commands::Bundle(bundle_parser) => { + let version_string = bundle_parser.version; + let kani_string = format!("kani-{}", version_string); + let bundle_name = format!("{}-{}.tar.gz", kani_string, env!("TARGET")); + let dir = Path::new(&kani_string); - std::fs::create_dir(dir)?; + // Check everything is ready before we start copying files + println!("-- Build release bundle {bundle_name}"); + prebundle(dir)?; - bundle_kani(dir)?; - bundle_cbmc(dir)?; - // cbmc-viewer isn't bundled, it's pip install'd on first-time setup + std::fs::create_dir(dir)?; - create_release_bundle(dir, &bundle_name)?; + bundle_kani(dir)?; + bundle_cbmc(dir)?; + // cbmc-viewer isn't bundled, it's pip install'd on first-time setup - std::fs::remove_dir_all(dir)?; + create_release_bundle(dir, &bundle_name)?; - println!("\nSuccessfully built release bundle: {}", bundle_name); - Ok(()) -} + std::fs::remove_dir_all(dir)?; -/// Parse command line arguments, and return the only thing we expect: a version string -fn parse_args() -> Result { - let args: Vec<_> = std::env::args().collect(); - if args.len() != 2 { - bail!("Usage: cargo run -p make-kani-release -- "); + println!("\nSuccessfully built release bundle: {}", bundle_name); + } } - Ok(args[1].clone()) + + Ok(()) } /// Ensures everything is good to go before we begin to build the release bundle. @@ -62,8 +72,10 @@ fn prebundle(dir: &Path) -> Result<()> { } // Before we begin, ensure Kani is built successfully in release mode. - Command::new("cargo").args(&["build", "--release"]).run()?; - + build_bin(&["--release"]); + // And that libraries have been built too. + build_lib(); + build_lib_legacy(); Ok(()) } @@ -89,11 +101,15 @@ fn bundle_kani(dir: &Path) -> Result<()> { cp_dir(Path::new("./library/kani_macros"), &library)?; cp_dir(Path::new("./library/std"), &library)?; - // 4. Record the exact toolchain we use + // 4. Pre-compiled library files + cp_dir(&kani_sysroot_lib(), dir)?; + cp_dir(&kani_sysroot_legacy_lib(), dir)?; + + // 5. Record the exact toolchain we use std::fs::write(dir.join("rust-toolchain-version"), env!("RUSTUP_TOOLCHAIN"))?; // 5. Include a licensing note - cp(Path::new("tools/make-kani-release/license-notes.txt"), dir)?; + cp(Path::new("tools/build-kani/license-notes.txt"), dir)?; Ok(()) } @@ -105,7 +121,7 @@ fn bundle_cbmc(dir: &Path) -> Result<()> { // We depend on other scripts to set up our environment correctly first. // This means it's possible to erroneously use this script, which is not ideal. Fool-proof is best. // But the best fix would involve changing our CI process to do something like - // "make-kani-release" and then using *that* to run the test suite. + // "build-kani" and then using *that* to run the test suite. // That way, we could just specify here what versions to use, and not need it in other places. // I felt that would be too invasive of a change to make at this time, so we'll start @@ -135,6 +151,7 @@ fn create_release_bundle(dir: &Path, bundle: &str) -> Result<()> { trait AutoRun { fn run(&mut self) -> Result<()>; } + impl AutoRun for Command { fn run(&mut self) -> Result<()> { let status = self.status()?; @@ -145,15 +162,38 @@ impl AutoRun for Command { } } +fn expect_dir(path: &Path) -> Result<()> { + if !path.is_dir() { + bail!("{} isn't a directory", path.to_string_lossy()); + } + Ok(()) +} + /// Copy a single file to a directory fn cp(src: &Path, dst: &Path) -> Result<()> { - if !dst.is_dir() { - bail!("{} isn't a directory", dst.to_string_lossy()); - } + expect_dir(dst)?; let dst = dst.join(src.file_name().unwrap()); std::fs::copy(src, dst)?; Ok(()) } + +/// Copy files from `src` to `dst` that respect the given pattern. +pub fn cp_files

(src: &Path, dst: &Path, predicate: P) -> Result<()> +where + P: FnMut(&Path) -> bool, +{ + expect_dir(src)?; + expect_dir(dst)?; + let mut filter = predicate; + for item in std::fs::read_dir(src)? { + let path = item?.path(); + if filter(&path) { + cp(&path, dst)?; + } + } + Ok(()) +} + /// Invoke `cp -r` fn cp_dir(src: &Path, dst: &Path) -> Result<()> { let mut cmd = OsString::from("cp -r "); diff --git a/tools/build-kani/src/parser.rs b/tools/build-kani/src/parser.rs new file mode 100644 index 000000000000..3f9dfa0a1d42 --- /dev/null +++ b/tools/build-kani/src/parser.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This file contains a small parser for our build script. +use clap::{Args, Parser, Subcommand}; + +#[derive(Parser)] +#[clap(name = "build-kani")] +#[clap(about = "Builds Kani either for development or release.", long_about = None)] +pub struct ArgParser { + #[clap(subcommand)] + pub subcommand: Commands, +} + +#[derive(Args, Debug, Eq, PartialEq)] +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, +} + +#[derive(Args, Debug, Eq, PartialEq)] +pub struct BundleParser { + /// String version + #[clap(value_name = "VERSION", default_value(env!("CARGO_PKG_VERSION")))] + pub version: String, +} + +#[derive(Eq, PartialEq, Subcommand)] +pub enum Commands { + /// Build kani binaries and sysroot for development. + BuildDev(BuildDevParser), + /// Build Kani's release bundle. + Bundle(BundleParser), +} diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs new file mode 100644 index 000000000000..32d1f82cd550 --- /dev/null +++ b/tools/build-kani/src/sysroot.rs @@ -0,0 +1,217 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module has all the logic to build Kani's sysroot folder. +//! In this folder, you can find the following folders: +//! - `bin/`: Where all Kani binaries will be located. +//! - `lib/`: Kani libraries as well as rust standard libraries. +//! - `legacy-lib/`: Kani libraries built based on the the toolchain standard libraries. +//! +//! Rustc expects the sysroot to have a specific folder layout: +//! {SYSROOT}/rustlib//lib/ +//! +//! Note: We don't cross-compile. Target is the same as the host. + +use crate::{cp, cp_files, AutoRun}; +use cargo_metadata::Message; +use std::ffi::OsStr; +use std::fs; +use std::io::BufReader; +use std::path::{Path, PathBuf}; +use std::process::{Child, Command, Stdio}; + +macro_rules! path_buf { + // The arguments are expressions that can be pushed to the PathBuf. + ($base_path:expr, $($extra_path:expr),+) => {{ + let mut path_buf = PathBuf::from($base_path); + $(path_buf.push($extra_path);)+ + path_buf + }}; +} + +#[cfg(target_os = "linux")] +fn lib_extension() -> &'static str { + ".so" +} + +#[cfg(target_os = "macos")] +fn lib_extension() -> &'static str { + ".dylib" +} + +/// Returns the path to Kani sysroot. I.e.: folder where we store pre-compiled binaries and +/// libraries. +pub fn kani_sysroot() -> PathBuf { + PathBuf::from(env!("KANI_SYSROOT")) +} + +/// Returns the path to where Kani and std pre-compiled libraries are stored. +pub fn kani_sysroot_lib() -> PathBuf { + path_buf!(kani_sysroot(), "lib") +} + +/// Returns the path to where Kani pre-compiled library are stored. +/// +/// The legacy libraries are compiled on the top of rustup sysroot. Using it results in missing +/// symbols. This is still needed though because when we use the rust monomorphizer as our +/// reachability algorithm, the resulting boundaries are different than the new sysroot. +pub fn kani_sysroot_legacy_lib() -> PathBuf { + path_buf!(kani_sysroot(), "legacy-lib") +} + +/// Returns the path to where Kani's pre-compiled binaries are stored. +pub fn kani_sysroot_bin() -> PathBuf { + path_buf!(kani_sysroot(), "bin") +} + +/// Build the `lib/` folder for the new sysroot. +/// This will include Kani's libraries as well as the standard libraries compiled with --emit-mir. +/// TODO: Don't copy Kani's libstd. +pub fn build_lib() { + // Run cargo build with -Z build-std + let target = env!("TARGET"); + let target_dir = env!("KANI_BUILD_LIBS"); + let args = [ + "build", + "-p", + "std", + "-p", + "kani", + "-p", + "kani_macros", + "-Z", + "unstable-options", + "--target-dir", + target_dir, + "-Z", + "target-applies-to-host", + "-Z", + "host-config", + "-Z", + "build-std=panic_abort,std,test", + "--profile", + "dev", + "--config", + "profile.dev.panic=\"abort\"", + "--config", + "host.rustflags=[\"--cfg=kani\"]", + "--target", + target, + "--message-format", + "json-diagnostic-rendered-ansi", + ]; + let mut cmd = Command::new("cargo") + .env("CARGO_ENCODED_RUSTFLAGS", ["--cfg=kani", "-Z", "always-encode-mir"].join("\x1f")) + .args(args) + .stdout(Stdio::piped()) + .spawn() + .expect("Failed to run `cargo build`."); + + // Remove kani "std" library leftover. + filter_kani_std(&mut cmd); + let _ = cmd.wait().expect("Couldn't get cargo's exit status"); + + // Create sysroot folder. + let sysroot_lib = kani_sysroot_lib(); + sysroot_lib.exists().then(|| fs::remove_dir_all(&sysroot_lib)); + fs::create_dir_all(&sysroot_lib).expect(&format!("Failed to create {:?}", sysroot_lib)); + + // Copy Kani libraries to inside sysroot folder. + let target_folder = Path::new(target_dir); + let macro_lib = format!("libkani_macros{}", lib_extension()); + let kani_macros = path_buf!(target_folder, "debug", macro_lib); + cp(&kani_macros, &sysroot_lib).unwrap(); + + let kani_rlib_folder = path_buf!(target_folder, target, "debug"); + cp_files(&kani_rlib_folder, &sysroot_lib, &is_rlib).unwrap(); + + // Copy `std` libraries and dependencies to sysroot folder following expected path format. + // TODO: Create a macro for all these push. + let src_path = path_buf!(target_folder, target, "debug", "deps"); + + let dst_path = path_buf!(sysroot_lib, "rustlib", target, "lib"); + fs::create_dir_all(&dst_path).unwrap(); + cp_files(&src_path, &dst_path, &is_rlib).unwrap(); +} + +/// Kani's "std" library may cause a name conflict with the rust standard library. We remove it +/// from the `deps/` folder, since we already store it outside of the `deps/` folder. +/// For that, we retrieve its location from `cargo build` output. +fn filter_kani_std(cargo_cmd: &mut Child) { + let reader = BufReader::new(cargo_cmd.stdout.take().unwrap()); + for message in Message::parse_stream(reader) { + match message.unwrap() { + Message::CompilerMessage(msg) => { + // Print message as cargo would. + println!("{:?}", msg) + } + Message::CompilerArtifact(artifact) => { + // Remove the `rlib` and `rmeta` files for our `std` library from the deps folder. + if artifact.target.name == "std" + && artifact.target.src_path.starts_with(env!("KANI_REPO_ROOT")) + { + let rmeta = artifact.filenames.iter().find(|p| p.extension() == Some("rmeta")); + let mut glob = PathBuf::from(rmeta.unwrap()); + glob.set_extension("*"); + Command::new("rm").arg("-f").arg(glob.as_os_str()).run().unwrap(); + } + } + Message::BuildScriptExecuted(_script) => { + // do nothing + } + Message::BuildFinished(_finished) => { + // do nothing + } + // Non-exhaustive enum. + _ => (), + } + } +} + +/// Build Kani libraries using the regular rust toolchain standard libraries. +/// We should be able to remove this once the MIR linker is stable. +pub fn build_lib_legacy() { + // Run cargo build with -Z build-std + let target_dir = env!("KANI_LEGACY_LIBS"); + let args = + ["build", "-p", "std", "-p", "kani", "-p", "kani_macros", "--target-dir", target_dir]; + Command::new("cargo") + .env("CARGO_ENCODED_RUSTFLAGS", ["--cfg=kani"].join("\x1f")) + .args(args) + .run() + .expect("Failed to build Kani libraries."); + + // Create sysroot folder. + let legacy_lib = kani_sysroot_legacy_lib(); + legacy_lib.exists().then(|| fs::remove_dir_all(&legacy_lib)); + fs::create_dir_all(&legacy_lib).expect(&format!("Failed to create {:?}", legacy_lib)); + + // Copy Kani libraries to inside the lib folder. + let target_folder = Path::new(target_dir); + let macro_lib = format!("libkani_macros{}", lib_extension()); + let kani_macros = path_buf!(target_folder, "debug", macro_lib); + cp(&kani_macros, &legacy_lib).unwrap(); + + let kani_rlib_folder = path_buf!(target_folder, "debug"); + cp_files(&kani_rlib_folder, &legacy_lib, &is_rlib).unwrap(); +} + +fn is_rlib(path: &Path) -> bool { + path.is_file() && String::from(path.file_name().unwrap().to_string_lossy()).ends_with(".rlib") +} + +/// Extra arguments to be given to `cargo build` while building Kani's binaries. +/// Note that the following arguments are always provided: +/// ```bash +/// cargo build --bins -Z unstable-options --out-dir $KANI_SYSROOT/bin/ +/// ``` +pub fn build_bin>(extra_args: &[T]) { + let out_dir = kani_sysroot_bin(); + let args = ["--bins", "-Z", "unstable-options", "--out-dir", out_dir.to_str().unwrap()]; + Command::new("cargo") + .arg("build") + .args(args) + .args(extra_args) + .run() + .expect("Failed to build binaries."); +}