From 2b43dbbda57117d3c00058f4c296c15f3f4904cd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 15 Jun 2023 13:00:11 -0700 Subject: [PATCH 1/2] Build the verification libraries using Kani compiler This will ensure we run Kani extra validation checks in our libraries. --- tools/build-kani/src/main.rs | 7 +++--- tools/build-kani/src/sysroot.rs | 43 ++++++++++++++++++++------------- 2 files changed, 29 insertions(+), 21 deletions(-) diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 5c1200e63180..e781f3ceb942 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -19,7 +19,7 @@ fn main() -> Result<()> { let args = parser::ArgParser::parse(); match args.subcommand { - parser::Commands::BuildDev(build_parser) => build_lib().and(build_bin(&build_parser.args)), + parser::Commands::BuildDev(build_parser) => build_lib(&build_bin(&build_parser.args)?), parser::Commands::Bundle(bundle_parser) => { let version_string = bundle_parser.version; let kani_string = format!("kani-{version_string}"); @@ -67,9 +67,8 @@ fn prebundle(dir: &Path) -> Result<()> { } // Before we begin, ensure Kani is built successfully in release mode. - build_bin(&["--release"]) - // And that libraries have been built too. - .and(build_lib()) + // And that libraries have been built too. + build_lib(&build_bin(&["--release"])?) } /// Copy Kani files into `dir` diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index dc508b8f62ee..eefeac45a243 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -56,35 +56,42 @@ pub fn kani_playback_lib() -> PathBuf { } /// Returns the path to where Kani's pre-compiled binaries are stored. -pub fn kani_sysroot_bin() -> PathBuf { +fn kani_sysroot_bin() -> PathBuf { path_buf!(kani_sysroot(), "bin") } /// 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() -> Result<()> { - build_verification_lib()?; - build_playback_lib() +pub fn build_lib(bin_folder: &Path) -> Result<()> { + let compiler = bin_folder.join("kani-compiler"); + build_verification_lib(&compiler)?; + build_playback_lib(&compiler) } /// Build the `lib/` folder for the new sysroot used during verification. /// This will include Kani's libraries as well as the standard libraries compiled with --emit-mir. -fn build_verification_lib() -> Result<()> { +fn build_verification_lib(compiler: &Path) -> Result<()> { let extra_args = ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""]; - build_kani_lib(&kani_sysroot_lib(), &extra_args) + let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm"]; + build_kani_lib(compiler, &kani_sysroot_lib(), &extra_args, &compiler_args) } /// 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() -> Result<()> { +fn build_playback_lib(compiler: &Path) -> Result<()> { let extra_args = ["--features=std/concrete_playback,kani/concrete_playback", "-Z", "build-std=std,test"]; - build_kani_lib(&kani_playback_lib(), &extra_args) + build_kani_lib(compiler, &kani_playback_lib(), &extra_args, &[]) } -fn build_kani_lib(path: &Path, extra_args: &[&str]) -> Result<()> { +fn build_kani_lib( + compiler: &Path, + path: &Path, + extra_cargo_args: &[&str], + extra_rustc_args: &[&str], +) -> Result<()> { // Run cargo build with -Z build-std let target = env!("TARGET"); let target_dir = env!("KANI_BUILD_LIBS"); @@ -117,13 +124,13 @@ fn build_kani_lib(path: &Path, extra_args: &[&str]) -> Result<()> { "--message-format", "json-diagnostic-rendered-ansi", ]; + let mut rustc_args = vec!["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"]; + rustc_args.extend_from_slice(extra_rustc_args); let mut cmd = Command::new("cargo") - .env( - "CARGO_ENCODED_RUSTFLAGS", - ["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"].join("\x1f"), - ) + .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f")) + .env("RUSTC", compiler) .args(args) - .args(extra_args) + .args(extra_cargo_args) .stdout(Stdio::piped()) .spawn() .expect("Failed to run `cargo build`."); @@ -225,18 +232,20 @@ fn build_artifacts(cargo_cmd: &mut Child) -> Vec { .collect() } +/// Build Kani binaries with the extra arguments provided and return path to the binaries folder. /// 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]) -> Result<()> { +pub fn build_bin>(extra_args: &[T]) -> Result { 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) + .args(args) .run() - .or(Err(format_err!("Failed to build binaries."))) + .or(Err(format_err!("Failed to build binaries.")))?; + Ok(out_dir) } From f521cee2923dbd86d4a08da2e977539eefef506c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 16 Jun 2023 10:09:42 -0700 Subject: [PATCH 2/2] Address PR feedback --- tools/build-kani/src/sysroot.rs | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index eefeac45a243..3d7e2d1dd5dd 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -64,31 +64,31 @@ fn kani_sysroot_bin() -> PathBuf { /// - 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 = bin_folder.join("kani-compiler"); - build_verification_lib(&compiler)?; - build_playback_lib(&compiler) + let compiler_path = bin_folder.join("kani-compiler"); + build_verification_lib(&compiler_path)?; + build_playback_lib(&compiler_path) } /// Build the `lib/` folder for the new sysroot used during verification. /// This will include Kani's libraries as well as the standard libraries compiled with --emit-mir. -fn build_verification_lib(compiler: &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"]; - build_kani_lib(compiler, &kani_sysroot_lib(), &extra_args, &compiler_args) + build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args) } /// 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) -> Result<()> { +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, &kani_playback_lib(), &extra_args, &[]) + build_kani_lib(compiler_path, &kani_playback_lib(), &extra_args, &[]) } fn build_kani_lib( - compiler: &Path, - path: &Path, + compiler_path: &Path, + output_path: &Path, extra_cargo_args: &[&str], extra_rustc_args: &[&str], ) -> Result<()> { @@ -128,7 +128,7 @@ fn build_kani_lib( rustc_args.extend_from_slice(extra_rustc_args); let mut cmd = Command::new("cargo") .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f")) - .env("RUSTC", compiler) + .env("RUSTC", compiler_path) .args(args) .args(extra_cargo_args) .stdout(Stdio::piped()) @@ -145,7 +145,7 @@ fn build_kani_lib( } // Create sysroot folder hierarchy. - copy_artifacts(&artifacts, path, target) + copy_artifacts(&artifacts, output_path, target) } /// Copy all the artifacts to their correct place to generate a valid sysroot. @@ -232,7 +232,7 @@ fn build_artifacts(cargo_cmd: &mut Child) -> Vec { .collect() } -/// Build Kani binaries with the extra arguments provided and return path to the binaries folder. +/// Build Kani binaries with the extra arguments provided and return the path to the binaries folder. /// Extra arguments to be given to `cargo build` while building Kani's binaries. /// Note that the following arguments are always provided: /// ```bash