mod cmd;
mod os_hacks;
mod setup;
use std::env;
use std::ffi::OsString;
use std::os::unix::prelude::CommandExt;
use std::path::{Path, PathBuf};
use std::process::Command;
use anyhow::{bail, Context, Result};
pub fn proxy(bin: &str) -> Result<()> {
match parse_args(env::args_os().collect()) {
ArgsResult::ExplicitSetup { use_local_bundle } => setup::setup(use_local_bundle),
ArgsResult::Default => {
fail_if_in_dev_environment()?;
if !setup::appears_setup() {
setup::setup(None)?;
}
exec(bin)
}
}
}
#[derive(PartialEq, Eq, Debug)]
enum ArgsResult {
ExplicitSetup { use_local_bundle: Option<OsString> },
Default,
}
fn parse_args(args: Vec<OsString>) -> ArgsResult {
let args_ez: Vec<Option<&str>> = args.iter().map(|x| x.to_str()).collect();
match &args_ez[..] {
&[_, Some("setup"), Some("--use-local-bundle"), _] => {
ArgsResult::ExplicitSetup { use_local_bundle: Some(args[3].clone()) }
}
&[_, Some("kani"), Some("setup"), Some("--use-local-bundle"), _] => {
ArgsResult::ExplicitSetup { use_local_bundle: Some(args[4].clone()) }
}
&[_, Some("setup")] | &[_, Some("kani"), Some("setup")] => {
ArgsResult::ExplicitSetup { use_local_bundle: None }
}
_ => ArgsResult::Default,
}
}
fn fail_if_in_dev_environment() -> Result<()> {
if let Ok(exe) = std::env::current_exe() {
if let Some(path) = exe.parent() {
if path.ends_with("target/debug") || path.ends_with("target/release") {
bail!(
"Running a release-only executable, {}, from a development environment. This is usually caused by PATH including 'target/release' erroneously.",
exe.file_name().unwrap().to_string_lossy()
)
}
}
}
Ok(())
}
fn exec(bin: &str) -> Result<()> {
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 pythonpath = prepend_search_path(&[pyroot], env::var_os("PYTHONPATH"))?;
let path = prepend_search_path(&[bin_kani, bin_pyroot], env::var_os("PATH"))?;
fixup_dynamic_linking_environment();
set_kani_rust_toolchain(&kani_dir)?;
let mut cmd = Command::new(program);
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?"));
}
fn prepend_search_path(paths: &[PathBuf], original: Option<OsString>) -> Result<OsString> {
match original {
None => Ok(env::join_paths(paths)?),
Some(original) => {
let orig = env::split_paths(&original);
let new_iter = paths.iter().cloned().chain(orig);
Ok(env::join_paths(new_iter)?)
}
}
}
fn fixup_dynamic_linking_environment() {
#[cfg(not(target_os = "macos"))]
const LOADER_PATH: &str = "LD_LIBRARY_PATH";
#[cfg(target_os = "macos")]
const LOADER_PATH: &str = "DYLD_FALLBACK_LIBRARY_PATH";
if let Some(paths) = env::var_os(LOADER_PATH) {
let new_val =
env::join_paths(env::split_paths(&paths).filter(unlike_toolchain_path)).unwrap();
env::set_var(LOADER_PATH, new_val);
}
}
#[allow(clippy::ptr_arg)]
fn unlike_toolchain_path(path: &PathBuf) -> bool {
let mut components = path.iter().rev();
!(components.next() == Some(std::ffi::OsStr::new("lib"))
&& components.next().is_some()
&& components.next() == Some(std::ffi::OsStr::new("toolchains")))
}
fn set_kani_rust_toolchain(kani_dir: &Path) -> Result<()> {
let toolchain_verison = setup::get_rust_toolchain_version(kani_dir)?;
env::set_var("RUSTUP_TOOLCHAIN", toolchain_verison);
Ok(())
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn check_unlike_toolchain_path() {
fn trial(s: &str) -> bool {
unlike_toolchain_path(&PathBuf::from(s))
}
assert!(!trial("/home/user/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib"));
assert!(!trial("/home/user/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/"));
assert!(!trial("/home/user/.rustup/toolchains/nightly/lib"));
assert!(!trial("/home/user/.rustup/toolchains/stable/lib"));
assert!(!trial("toolchains/nightly/lib"));
assert!(trial("/home/user/.rustup/toolchains"));
assert!(trial("/usr/lib"));
assert!(trial("/home/user/lib/toolchains"));
assert!(trial(""));
assert!(trial("/"));
}
#[test]
fn check_arg_parsing() {
fn trial(args: &[&str]) -> ArgsResult {
parse_args(args.iter().map(OsString::from).collect())
}
{
let e = ArgsResult::Default;
assert_eq!(e, trial(&["cargo-kani", "kani"]));
assert_eq!(e, trial(&[]));
}
{
let e = ArgsResult::ExplicitSetup { use_local_bundle: None };
assert_eq!(e, trial(&["cargo-kani", "kani", "setup"]));
assert_eq!(e, trial(&["cargo", "kani", "setup"]));
assert_eq!(e, trial(&["cargo-kani", "setup"]));
}
{
let e = ArgsResult::ExplicitSetup { use_local_bundle: Some(OsString::from("FILE")) };
assert_eq!(e, trial(&["cargo-kani", "kani", "setup", "--use-local-bundle", "FILE"]));
assert_eq!(e, trial(&["cargo", "kani", "setup", "--use-local-bundle", "FILE"]));
assert_eq!(e, trial(&["cargo-kani", "setup", "--use-local-bundle", "FILE"]));
}
}
}