From 96c6b3b1037045167dcc5e7498d6b828980f6f84 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Tue, 24 May 2022 15:16:35 -0500 Subject: [PATCH] Refactor kani-verifier (#1218) --- src/cmd.rs | 60 +++++++++++++ src/lib.rs | 234 ++++----------------------------------------------- src/setup.rs | 193 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 269 insertions(+), 218 deletions(-) create mode 100644 src/cmd.rs create mode 100644 src/setup.rs diff --git a/src/cmd.rs b/src/cmd.rs new file mode 100644 index 0000000000000..77204f092e74b --- /dev/null +++ b/src/cmd.rs @@ -0,0 +1,60 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains small helper functions for running Commands. +//! We could possibly eliminate this if we find a small-enough dependency. + +use std::ffi::OsString; +use std::process::Command; + +use anyhow::{bail, Context, Result}; + +/// Helper trait to fallibly run commands +pub trait AutoRun { + fn run(&mut self) -> Result<()>; +} +impl AutoRun for Command { + fn run(&mut self) -> Result<()> { + // This can sometimes fail during the set-up of the forked process before exec, + // for example by setting `current_dir` to a directory that does not exist. + let status = self.status().with_context(|| { + format!( + "Internal failure before invoking command: {}", + render_command(self).to_string_lossy() + ) + })?; + if !status.success() { + bail!("Failed command: {}", render_command(self).to_string_lossy()); + } + Ok(()) + } +} + +/// Render a Command as a string, to log it +fn render_command(cmd: &Command) -> OsString { + let mut str = OsString::new(); + + for (k, v) in cmd.get_envs() { + if let Some(v) = v { + str.push(k); + str.push("=\""); + str.push(v); + str.push("\" "); + } + } + + str.push(cmd.get_program()); + + for a in cmd.get_args() { + str.push(" "); + if a.to_string_lossy().contains(' ') { + str.push("\""); + str.push(a); + str.push("\""); + } else { + str.push(a); + } + } + + str +} diff --git a/src/lib.rs b/src/lib.rs index 875c18ce28e89..ed33c8f7723b2 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -14,63 +14,37 @@ #![warn(clippy::all, clippy::cargo)] +mod cmd; +mod setup; + use std::env; use std::ffi::OsString; use std::os::unix::prelude::CommandExt; -use std::path::{Path, PathBuf}; +use std::path::PathBuf; use std::process::Command; use anyhow::{bail, Context, Result}; -/// Comes from our Cargo.toml manifest file. Must correspond to our release verion. -const VERSION: &str = env!("CARGO_PKG_VERSION"); -/// Set by our `build.rs`, reflects the Rust target triple we're building for -const TARGET: &str = env!("TARGET"); - -/// Typically `~/.kani/kani-1.x/` -fn kani_dir() -> PathBuf { - home::home_dir() - .expect("Couldn't find home dir?") - .join(".kani") - .join(format!("kani-{}", VERSION)) -} - -/// The filename of the release bundle -fn download_filename() -> String { - format!("kani-{}-{}.tar.gz", VERSION, TARGET) -} - -/// Helper to find the download URL for this version of Kani -fn download_url() -> String { - let tag: &str = &format!("kani-{}", VERSION); - let file: &str = &download_filename(); - format!("https://github.com/model-checking/kani/releases/download/{}/{}", tag, file) -} - /// Effectively the entry point (i.e. `main` function) for both our proxy binaries. +/// `bin` should be either `kani` or `cargo-kani` pub fn proxy(bin: &str) -> Result<()> { // In an effort to keep our dependencies minimal, we do the bare minimum argument parsing - let args: Vec<_> = std::env::args_os().collect(); + let args: Vec<_> = env::args_os().collect(); if args.len() >= 2 && args[1] == "setup" { if args.len() >= 4 && args[2] == "--use-local-bundle" { - setup(Some(args[3].clone())) + setup::setup(Some(args[3].clone())) } else { - setup(None) + setup::setup(None) } } else { fail_if_in_dev_environment()?; - if !appears_setup() { - setup(None)?; + if !setup::appears_setup() { + setup::setup(None)?; } exec(bin) } } -/// Fast check to see if we look setup already -fn appears_setup() -> bool { - kani_dir().exists() -} - /// In dev environments, this proxy shouldn't be used. /// But accidentally using it (with the test suite) can fire off /// hundreds of HTTP requests trying to download a non-existent release bundle. @@ -90,136 +64,10 @@ fn fail_if_in_dev_environment() -> Result<()> { Ok(()) } -/// Give users a better error message than "404" if we're on an unsupported platform. -fn fail_if_unsupported_target() -> Result<()> { - // This is basically going to be reduced to a compile-time constant - match TARGET { - "x86_64-unknown-linux-gnu" | "x86_64-apple-darwin" => Ok(()), - _ => bail!("Kani does not support this platform (Rust target {})", TARGET), - } -} - -/// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION` -fn setup(use_local_bundle: Option) -> Result<()> { - let kani_dir = kani_dir(); - // e.g. `~/.kani/` - let base_dir = kani_dir.parent().expect("No base directory?"); - - println!("[0/6] Running Kani first-time setup..."); - - println!("[1/6] Ensuring the existence of: {}", base_dir.display()); - std::fs::create_dir_all(&base_dir)?; - - if let Some(pathstr) = use_local_bundle { - println!("[2/6] 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 - // extract it directly into the expected (kani_dir) directory (instead of base_dir). - if !kani_dir.exists() { - std::fs::create_dir(&kani_dir)?; - } - Command::new("tar") - .arg("--strip-components=1") - .arg("-zxf") - .arg(&path) - .current_dir(&kani_dir) - .run()?; - } else { - let filename = download_filename(); - println!("[2/6] Downloading Kani release bundle: {}", &filename); - fail_if_unsupported_target()?; - let bundle = base_dir.join(filename); - Command::new("curl") - .args(&["-sSLf", "-o"]) - .arg(&bundle) - .arg(download_url()) - .run() - .context("Failed to download Kani release bundle")?; - - Command::new("tar").arg("zxf").arg(&bundle).current_dir(base_dir).run()?; - - std::fs::remove_file(bundle)?; - } - - 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); - Command::new("rustup").args(&["toolchain", "install", &toolchain_version]).run()?; - - let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); - - symlink_rust_toolchain(&toolchain, &kani_dir)?; - - println!("[4/6] Installing Kani python dependencies..."); - let pyroot = kani_dir.join("pyroot"); - - // TODO: this is a repetition of versions from elsewhere - Command::new("python3") - .args(&["-m", "pip", "install", "cbmc-viewer==3.2", "--target"]) - .arg(&pyroot) - .run()?; - Command::new("python3") - .args(&["-m", "pip", "install", "colorama==0.4.3", "--target"]) - .arg(&pyroot) - .run()?; - - 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"))?; - - println!("[6/6] Successfully completed Kani first-time setup."); - - Ok(()) -} - -/// Creates a `kani_dir/toolchain` symlink pointing to `toolchain`. -fn symlink_rust_toolchain(toolchain: &Path, kani_dir: &Path) -> Result<()> { - let path = kani_dir.join("toolchain"); - // We want to be idempotent, so if the symlink already exists, delete it first - if path.exists() && path.is_symlink() { - std::fs::remove_file(&path)?; - } - std::os::unix::fs::symlink(toolchain, path)?; - Ok(()) -} - /// Executes `kani-driver` in `bin` mode (kani or cargo-kani) /// augmenting environment variables to accomodate our release environment fn exec(bin: &str) -> Result<()> { - let kani_dir = kani_dir(); + let kani_dir = setup::kani_dir(); let program = kani_dir.join("bin").join("kani-driver"); let pyroot = kani_dir.join("pyroot"); let bin_kani = kani_dir.join("bin"); @@ -227,20 +75,20 @@ fn exec(bin: &str) -> Result<()> { let bin_toolchain = kani_dir.join("toolchain").join("bin"); // Allow python scripts to find dependencies under our pyroot - let pythonpath = augment_search(&[pyroot], env::var_os("PYTHONPATH"))?; + let pythonpath = prepend_search_path(&[pyroot], env::var_os("PYTHONPATH"))?; // Add: kani, cbmc, viewer (pyroot), and our rust toolchain directly to our PATH - let path = augment_search(&[bin_kani, bin_pyroot, bin_toolchain], env::var_os("PATH"))?; + let path = prepend_search_path(&[bin_kani, bin_pyroot, bin_toolchain], env::var_os("PATH"))?; let mut cmd = Command::new(program); - cmd.args(std::env::args_os().skip(1)).env("PYTHONPATH", pythonpath).env("PATH", path).arg0(bin); + cmd.args(env::args_os().skip(1)).env("PYTHONPATH", pythonpath).env("PATH", path).arg0(bin); let result = cmd.status().context("Failed to invoke kani-driver")?; std::process::exit(result.code().expect("No exit code?")); } -/// Prepend paths to an environment variable -fn augment_search(paths: &[PathBuf], original: Option) -> Result { +/// Prepend paths to an environment variable search string like PATH +fn prepend_search_path(paths: &[PathBuf], original: Option) -> Result { match original { None => Ok(env::join_paths(paths)?), Some(original) => { @@ -250,53 +98,3 @@ fn augment_search(paths: &[PathBuf], original: Option) -> Result Result<()>; -} -impl AutoRun for Command { - fn run(&mut self) -> Result<()> { - // This can sometimes fail during the set-up of the forked process before exec, - // for example by setting `current_dir` to a directory that does not exist. - let status = self.status().with_context(|| { - format!( - "Internal failure before invoking command: {}", - render_command(self).to_string_lossy() - ) - })?; - if !status.success() { - bail!("Failed command: {}", render_command(self).to_string_lossy()); - } - Ok(()) - } -} - -/// Render a Command as a string, to log it -pub fn render_command(cmd: &Command) -> OsString { - let mut str = OsString::new(); - - for (k, v) in cmd.get_envs() { - if let Some(v) = v { - str.push(k); - str.push("=\""); - str.push(v); - str.push("\" "); - } - } - - str.push(cmd.get_program()); - - for a in cmd.get_args() { - str.push(" "); - if a.to_string_lossy().contains(' ') { - str.push("\""); - str.push(a); - str.push("\""); - } else { - str.push(a); - } - } - - str -} diff --git a/src/setup.rs b/src/setup.rs new file mode 100644 index 0000000000000..b9c76b0dade3d --- /dev/null +++ b/src/setup.rs @@ -0,0 +1,193 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains all first-time setup code done as part of `cargo kani setup`. + +use std::env; +use std::ffi::OsString; +use std::path::{Path, PathBuf}; +use std::process::Command; + +use anyhow::{bail, Context, Result}; + +use crate::cmd::AutoRun; + +/// Comes from our Cargo.toml manifest file. Must correspond to our release verion. +const VERSION: &str = env!("CARGO_PKG_VERSION"); +/// Set by our `build.rs`, reflects the Rust target triple we're building for +const TARGET: &str = env!("TARGET"); + +/// Where Kani has been installed. Typically `~/.kani/kani-1.x/` +pub fn kani_dir() -> PathBuf { + home::home_dir() + .expect("Couldn't find home dir?") + .join(".kani") + .join(format!("kani-{}", VERSION)) +} + +/// Fast check to see if we look setup already +pub fn appears_setup() -> bool { + kani_dir().exists() +} + +/// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION` +pub fn setup(use_local_bundle: Option) -> Result<()> { + let kani_dir = kani_dir(); + + println!("[0/6] Running Kani first-time setup..."); + + println!("[1/6] 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_python_deps(&kani_dir)?; + + setup_build_kani_prelude(&kani_dir, toolchain_version)?; + + println!("[6/6] Successfully completed Kani first-time setup."); + + Ok(()) +} + +/// Download and unpack the Kani release bundle +fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option) -> Result<()> { + // e.g. `~/.kani/` + 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()); + 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 + // extract it directly into the expected (kani_dir) directory (instead of base_dir). + Command::new("tar") + .arg("--strip-components=1") + .arg("-zxf") + .arg(&path) + .current_dir(&kani_dir) + .run()?; + } else { + let filename = download_filename(); + println!("[2/6] Downloading Kani release bundle: {}", &filename); + fail_if_unsupported_target()?; + let bundle = base_dir.join(filename); + Command::new("curl") + .args(&["-sSLf", "-o"]) + .arg(&bundle) + .arg(download_url()) + .run() + .context("Failed to download Kani release bundle")?; + + Command::new("tar").arg("zxf").arg(&bundle).current_dir(base_dir).run()?; + + std::fs::remove_file(bundle)?; + } + Ok(()) +} + +/// Install the Rust toolchain version we require +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); + Command::new("rustup").args(&["toolchain", "install", &toolchain_version]).run()?; + + let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); + + symlink_rust_toolchain(&toolchain, kani_dir)?; + Ok(toolchain_version) +} + +/// Install into the pyroot the python dependencies we need +fn setup_python_deps(kani_dir: &Path) -> Result<()> { + println!("[4/6] Installing Kani python dependencies..."); + let pyroot = kani_dir.join("pyroot"); + + // TODO: this is a repetition of versions from kani/scripts/setup/$OS/install_deps.sh + Command::new("python3") + .args(&["-m", "pip", "install", "cbmc-viewer==3.2", "colorama==0.4.3", "--target"]) + .arg(&pyroot) + .run()?; + 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. + +/// The filename of the release bundle +fn download_filename() -> String { + format!("kani-{}-{}.tar.gz", VERSION, TARGET) +} + +/// The download URL for this version of Kani +fn download_url() -> String { + let tag: &str = &format!("kani-{}", VERSION); + let file: &str = &download_filename(); + format!("https://github.com/model-checking/kani/releases/download/{}/{}", tag, file) +} + +/// Give users a better error message than "404" if we're on an unsupported platform. +/// This is called just before we try to download the release bundle. +fn fail_if_unsupported_target() -> Result<()> { + // This is basically going to be reduced to a compile-time constant + match TARGET { + "x86_64-unknown-linux-gnu" | "x86_64-apple-darwin" => Ok(()), + _ => bail!("Kani does not support this platform (Rust target {})", TARGET), + } +} + +/// Creates a `kani_dir/toolchain` symlink pointing to `toolchain`. +fn symlink_rust_toolchain(toolchain: &Path, kani_dir: &Path) -> Result<()> { + let path = kani_dir.join("toolchain"); + // We want setup to be idempotent, so if the symlink already exists, delete instead of failing + if path.exists() && path.is_symlink() { + std::fs::remove_file(&path)?; + } + std::os::unix::fs::symlink(toolchain, path)?; + Ok(()) +}