Skip to content

Commit

Permalink
Refactor kani-verifier (rust-lang#1218)
Browse files Browse the repository at this point in the history
  • Loading branch information
@tedinski
tedinski authored May 24, 2022
1 parent 885546c commit 96c6b3b
Show file tree
Hide file tree
Showing 3 changed files with 269 additions and 218 deletions.
60 changes: 60 additions & 0 deletions src/cmd.rs
View file
Original file line number Diff line number Diff line change
@@ -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
}
234 changes: 16 additions & 218 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -90,157 +64,31 @@ 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<OsString>) -> 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");
let bin_pyroot = pyroot.join("bin");
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<OsString>) -> Result<OsString> {
/// Prepend paths to an environment variable search string like PATH
fn prepend_search_path(paths: &[PathBuf], original: Option<OsString>) -> Result<OsString> {
match original {
None => Ok(env::join_paths(paths)?),
Some(original) => {
Expand All @@ -250,53 +98,3 @@ fn augment_search(paths: &[PathBuf], original: Option<OsString>) -> Result<OsStr
}
}
}

/// Helper trait to fallibly run commands
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
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
}
Loading

0 comments on commit 96c6b3b

Please sign in to comment.