|
| 1 | +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. |
| 2 | +// SPDX-License-Identifier: Apache-2.0 OR MIT |
| 3 | + |
| 4 | +//! This crate includes two "proxy binaries": `kani` and `cargo-kani`. |
| 5 | +//! These are conveniences to make it easy to: |
| 6 | +//! |
| 7 | +//! ```bash |
| 8 | +//! cargo install --locked kani-verifer |
| 9 | +//! ``` |
| 10 | +//! |
| 11 | +//! Upon first run, or upon running `cargo-kani setup`, these proxy |
| 12 | +//! binaries will download the appropriate Kani release bundle and invoke |
| 13 | +//! the "real" `kani` and `cargo-kani` binaries. |
| 14 | +
|
| 15 | +#![warn(clippy::all, clippy::cargo)] |
| 16 | + |
| 17 | +use std::env; |
| 18 | +use std::ffi::OsString; |
| 19 | +use std::os::unix::prelude::CommandExt; |
| 20 | +use std::path::{Path, PathBuf}; |
| 21 | +use std::process::Command; |
| 22 | + |
| 23 | +use anyhow::{bail, Context, Result}; |
| 24 | + |
| 25 | +/// Comes from our Cargo.toml manifest file. Must correspond to our release verion. |
| 26 | +const VERSION: &str = env!("CARGO_PKG_VERSION"); |
| 27 | +/// Set by our `build.rs`, reflects the Rust target triple we're building for |
| 28 | +const TARGET: &str = env!("TARGET"); |
| 29 | + |
| 30 | +/// Typically `~/.kani/kani-1.x/` |
| 31 | +fn kani_dir() -> PathBuf { |
| 32 | + home::home_dir() |
| 33 | + .expect("Couldn't find home dir?") |
| 34 | + .join(".kani") |
| 35 | + .join(format!("kani-{}", VERSION)) |
| 36 | +} |
| 37 | + |
| 38 | +/// The filename of the release bundle |
| 39 | +fn download_filename() -> String { |
| 40 | + format!("kani-{}-{}.tar.gz", VERSION, TARGET) |
| 41 | +} |
| 42 | + |
| 43 | +/// Helper to find the download URL for this version of Kani |
| 44 | +fn download_url() -> String { |
| 45 | + let tag: &str = &format!("kani-{}", VERSION); |
| 46 | + let file: &str = &download_filename(); |
| 47 | + format!("https://github.com/model-checking/kani/releases/download/{}/{}", tag, file) |
| 48 | +} |
| 49 | + |
| 50 | +/// Effectively the entry point (i.e. `main` function) for both our proxy binaries. |
| 51 | +pub fn proxy(bin: &str) -> Result<()> { |
| 52 | + // In an effort to keep our dependencies minimal, we do the bare minimum argument parsing |
| 53 | + let args: Vec<_> = std::env::args_os().collect(); |
| 54 | + if args.len() >= 2 && args[1] == "setup" { |
| 55 | + if args.len() >= 4 && args[2] == "--use-local-bundle" { |
| 56 | + setup(Some(args[3].clone())) |
| 57 | + } else { |
| 58 | + setup(None) |
| 59 | + } |
| 60 | + } else { |
| 61 | + if !appears_setup() { |
| 62 | + setup(None)?; |
| 63 | + } |
| 64 | + exec(bin) |
| 65 | + } |
| 66 | +} |
| 67 | + |
| 68 | +/// Fast check to see if we look setup already |
| 69 | +fn appears_setup() -> bool { |
| 70 | + kani_dir().exists() |
| 71 | +} |
| 72 | + |
| 73 | +/// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION` |
| 74 | +fn setup(use_local_bundle: Option<OsString>) -> Result<()> { |
| 75 | + let kani_dir = kani_dir(); |
| 76 | + // e.g. `~/.kani/` |
| 77 | + let base_dir = kani_dir.parent().expect("No base directory?"); |
| 78 | + |
| 79 | + println!("[0/6] Running Kani first-time setup..."); |
| 80 | + |
| 81 | + println!("[1/6] Ensuring the existence of: {}", base_dir.display()); |
| 82 | + std::fs::create_dir_all(&base_dir)?; |
| 83 | + |
| 84 | + if let Some(pathstr) = use_local_bundle { |
| 85 | + let path = Path::new(&pathstr).canonicalize()?; |
| 86 | + println!("[2/6] Installing local Kani bundle: {}", path.display()); |
| 87 | + Command::new("tar").arg("zxf").arg(&path).current_dir(base_dir).run()?; |
| 88 | + |
| 89 | + // when given a local bundle, it's often "-latest" but we expect "-1.0" or something. Hack it up. |
| 90 | + let file = path.file_name().expect("has filename").to_string_lossy(); |
| 91 | + let components: Vec<_> = file.split('-').collect(); |
| 92 | + let expected_dir = format!("{}-{}", components[0], components[1]); |
| 93 | + |
| 94 | + std::fs::rename(base_dir.join(expected_dir), &kani_dir)?; |
| 95 | + } else { |
| 96 | + let filename = download_filename(); |
| 97 | + println!("[2/6] Downloading Kani release bundle: {}", &filename); |
| 98 | + let bundle = base_dir.join(filename); |
| 99 | + Command::new("curl") |
| 100 | + .args(&["-sSLf", "-o"]) |
| 101 | + .arg(&bundle) |
| 102 | + .arg(download_url()) |
| 103 | + .run() |
| 104 | + .context("Failed to download Kani release bundle")?; |
| 105 | + |
| 106 | + Command::new("tar").arg("zxf").arg(&bundle).current_dir(base_dir).run()?; |
| 107 | + |
| 108 | + std::fs::remove_file(bundle)?; |
| 109 | + } |
| 110 | + |
| 111 | + let toolchain_version = std::fs::read_to_string(kani_dir.join("rust-toolchain-version")) |
| 112 | + .context("Reading release bundle rust-toolchain-version")?; |
| 113 | + println!("[3/6] Installing rust toolchain version: {}", &toolchain_version); |
| 114 | + Command::new("rustup").args(&["toolchain", "install", &toolchain_version]).run()?; |
| 115 | + |
| 116 | + let toolchain = home::rustup_home()?.join("toolchains").join(&toolchain_version); |
| 117 | + |
| 118 | + Command::new("ln").arg("-s").arg(toolchain).arg(kani_dir.join("toolchain")).run()?; |
| 119 | + |
| 120 | + println!("[4/6] Installing Kani python dependencies..."); |
| 121 | + let pyroot = kani_dir.join("pyroot"); |
| 122 | + |
| 123 | + // TODO: this is a repetition of versions from elsewhere |
| 124 | + Command::new("python3") |
| 125 | + .args(&["-m", "pip", "install", "cbmc-viewer==2.11", "--target"]) |
| 126 | + .arg(&pyroot) |
| 127 | + .run()?; |
| 128 | + Command::new("python3") |
| 129 | + .args(&["-m", "pip", "install", "colorama==0.4.3", "--target"]) |
| 130 | + .arg(&pyroot) |
| 131 | + .run()?; |
| 132 | + |
| 133 | + println!("[5/6] Building Kani library prelude..."); |
| 134 | + // We need a workspace to build them in, otherwise repeated builds generate different hashes and `kani` can't find `kani_macros` |
| 135 | + let contents = "[workspace]\nmembers = [\"kani\",\"kani_macros\",\"std\"]"; |
| 136 | + std::fs::write(kani_dir.join("library").join("Cargo.toml"), contents)?; |
| 137 | + |
| 138 | + // A little helper for invoking Cargo repeatedly here |
| 139 | + let cargo = |crate_name: &str| -> Result<()> { |
| 140 | + let manifest = format!("library/{}/Cargo.toml", crate_name); |
| 141 | + Command::new("cargo") |
| 142 | + .args(&[ |
| 143 | + &format!("+{}", toolchain_version), |
| 144 | + "build", |
| 145 | + "-Z", |
| 146 | + "unstable-options", |
| 147 | + "--manifest-path", |
| 148 | + &manifest, |
| 149 | + "--out-dir", |
| 150 | + "lib", |
| 151 | + "--target-dir", |
| 152 | + "target", |
| 153 | + ]) |
| 154 | + .current_dir(&kani_dir) |
| 155 | + // https://doc.rust-lang.org/cargo/reference/environment-variables.html |
| 156 | + .env("CARGO_ENCODED_RUSTFLAGS", "--cfg=kani") |
| 157 | + .run() |
| 158 | + .with_context(|| format!("Failed to build Kani prelude library {}", crate_name)) |
| 159 | + }; |
| 160 | + |
| 161 | + // We seem to need 3 invocations because of the behavior of the `--out-dir` flag. |
| 162 | + // It only seems to produce the requested artifact, not its dependencies. |
| 163 | + cargo("kani")?; |
| 164 | + cargo("kani_macros")?; |
| 165 | + cargo("std")?; |
| 166 | + |
| 167 | + std::fs::remove_dir_all(kani_dir.join("target"))?; |
| 168 | + |
| 169 | + println!("[6/6] Successfully completed Kani first-time setup."); |
| 170 | + |
| 171 | + Ok(()) |
| 172 | +} |
| 173 | + |
| 174 | +/// Executes `cargo-kani` in `bin` mode, augmenting environment variables to accomodate our release environment |
| 175 | +fn exec(bin: &str) -> Result<()> { |
| 176 | + let kani_dir = kani_dir(); |
| 177 | + let program = kani_dir.join("bin").join("cargo-kani"); |
| 178 | + let pyroot = kani_dir.join("pyroot"); |
| 179 | + let bin_kani = kani_dir.join("bin"); |
| 180 | + let bin_pyroot = pyroot.join("bin"); |
| 181 | + let bin_toolchain = kani_dir.join("toolchain").join("bin"); |
| 182 | + |
| 183 | + // Allow python scripts to find dependencies under our pyroot |
| 184 | + let pythonpath = augment_search(&[pyroot], env::var_os("PYTHONPATH"))?; |
| 185 | + // Add: kani, cbmc, viewer (pyroot), and our rust toolchain directly to our PATH |
| 186 | + let path = augment_search(&[bin_kani, bin_pyroot, bin_toolchain], env::var_os("PATH"))?; |
| 187 | + |
| 188 | + let mut cmd = Command::new(program); |
| 189 | + cmd.args(std::env::args_os().skip(1)).env("PYTHONPATH", pythonpath).env("PATH", path).arg0(bin); |
| 190 | + |
| 191 | + std::process::exit(cmd.status()?.code().expect("No exit code?")); |
| 192 | +} |
| 193 | + |
| 194 | +/// Prepend paths to an environment variable |
| 195 | +fn augment_search(paths: &[PathBuf], original: Option<OsString>) -> Result<OsString> { |
| 196 | + match original { |
| 197 | + None => Ok(env::join_paths(paths)?), |
| 198 | + Some(original) => { |
| 199 | + let orig = env::split_paths(&original); |
| 200 | + let new_iter = paths.iter().cloned().chain(orig); |
| 201 | + Ok(env::join_paths(new_iter)?) |
| 202 | + } |
| 203 | + } |
| 204 | +} |
| 205 | + |
| 206 | +/// Helper trait to fallibly run commands |
| 207 | +trait AutoRun { |
| 208 | + fn run(&mut self) -> Result<()>; |
| 209 | +} |
| 210 | +impl AutoRun for Command { |
| 211 | + fn run(&mut self) -> Result<()> { |
| 212 | + // This can sometimes fail during the set-up of the forked process before exec, |
| 213 | + // for example by setting `current_dir` to a directory that does not exist. |
| 214 | + let status = self.status().with_context(|| { |
| 215 | + format!( |
| 216 | + "Internal failure before invoking command: {}", |
| 217 | + render_command(self).to_string_lossy() |
| 218 | + ) |
| 219 | + })?; |
| 220 | + if !status.success() { |
| 221 | + bail!("Failed command: {}", render_command(self).to_string_lossy()); |
| 222 | + } |
| 223 | + Ok(()) |
| 224 | + } |
| 225 | +} |
| 226 | + |
| 227 | +/// Render a Command as a string, to log it |
| 228 | +pub fn render_command(cmd: &Command) -> OsString { |
| 229 | + let mut str = OsString::new(); |
| 230 | + |
| 231 | + for (k, v) in cmd.get_envs() { |
| 232 | + if let Some(v) = v { |
| 233 | + str.push(k); |
| 234 | + str.push("=\""); |
| 235 | + str.push(v); |
| 236 | + str.push("\" "); |
| 237 | + } |
| 238 | + } |
| 239 | + |
| 240 | + str.push(cmd.get_program()); |
| 241 | + |
| 242 | + for a in cmd.get_args() { |
| 243 | + str.push(" "); |
| 244 | + if a.to_string_lossy().contains(' ') { |
| 245 | + str.push("\""); |
| 246 | + str.push(a); |
| 247 | + str.push("\""); |
| 248 | + } else { |
| 249 | + str.push(a); |
| 250 | + } |
| 251 | + } |
| 252 | + |
| 253 | + str |
| 254 | +} |
0 commit comments