Add --use-local-toolchain to Kani setup (#3056)

Adds `--use-local-toolchain` to Kani's setup flow, which accepts a local toolchain and then uses that to finish the Kani setup. Some notes: 1. Why? This is mainly for installing GPG verified toolchains. 2. This is missing some cleanup and refactoring work, like ensuring that the user defined toolchain matches the one that Kani was built against etc. Marked as Todo, for later. Resolves [#3058](#3058) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
model-checking · Mar 7, 2024 · 45caad4 · 45caad4
1 parent 12768f2
commit 45caad4
Show file tree

Hide file tree

Showing 10 changed files with 236 additions and 47 deletions.
diff --git a/.gitignore b/.gitignore
@@ -16,6 +16,7 @@ desktop.ini
 Session.vim
 .cproject
 .idea
+toolchains/
 *.iml
 .vscode
 .project

diff --git a/Cargo.lock b/Cargo.lock
@@ -33,6 +33,15 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "ansi_term"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2"
+dependencies = [
+ "winapi",
+]
+
 [[package]]
 name = "anstream"
 version = "0.6.13"
@@ -87,6 +96,17 @@ version = "1.0.80"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5ad32ce52e4161730f7098c077cd2ed6229b5804ccf99e5366be1ab72a98b4e1"
 
+[[package]]
+name = "atty"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
+dependencies = [
+ "hermit-abi",
+ "libc",
+ "winapi",
+]
+
 [[package]]
 name = "autocfg"
 version = "1.1.0"
@@ -125,7 +145,7 @@ version = "0.47.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
- "clap",
+ "clap 4.5.1",
  "which",
 ]
 
@@ -167,6 +187,21 @@ version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
+[[package]]
+name = "clap"
+version = "2.34.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c"
+dependencies = [
+ "ansi_term",
+ "atty",
+ "bitflags 1.3.2",
+ "strsim 0.8.0",
+ "textwrap",
+ "unicode-width",
+ "vec_map",
+]
+
 [[package]]
 name = "clap"
 version = "4.5.1"
@@ -186,7 +221,7 @@ dependencies = [
  "anstream",
  "anstyle",
  "clap_lex",
- "strsim",
+ "strsim 0.11.0",
 ]
 
 [[package]]
@@ -392,6 +427,15 @@ version = "0.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
 
+[[package]]
+name = "hermit-abi"
+version = "0.1.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "home"
 version = "0.5.9"
@@ -437,7 +481,7 @@ dependencies = [
 name = "kani-compiler"
 version = "0.47.0"
 dependencies = [
- "clap",
+ "clap 4.5.1",
  "cprover_bindings",
  "home",
  "itertools",
@@ -460,7 +504,7 @@ version = "0.47.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
- "clap",
+ "clap 4.5.1",
  "comfy-table",
  "console",
  "glob",
@@ -487,6 +531,7 @@ name = "kani-verifier"
 version = "0.47.0"
 dependencies = [
  "anyhow",
+ "clap 2.34.0",
  "home",
  "os_info",
 ]
@@ -505,7 +550,7 @@ dependencies = [
 name = "kani_metadata"
 version = "0.47.0"
 dependencies = [
- "clap",
+ "clap 4.5.1",
  "cprover_bindings",
  "serde",
  "strum 0.26.1",
@@ -1050,6 +1095,12 @@ dependencies = [
  "serde",
 ]
 
+[[package]]
+name = "strsim"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
+
 [[package]]
 name = "strsim"
 version = "0.11.0"
@@ -1127,6 +1178,15 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "textwrap"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060"
+dependencies = [
+ "unicode-width",
+]
+
 [[package]]
 name = "thiserror"
 version = "1.0.57"
@@ -1305,6 +1365,12 @@ version = "0.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d"
 
+[[package]]
+name = "vec_map"
+version = "0.8.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
+
 [[package]]
 name = "version_check"
 version = "0.9.4"

diff --git a/Cargo.toml b/Cargo.toml
@@ -19,6 +19,7 @@ include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.m
 [dependencies]
 anyhow = "1"
 home = "0.5"
+clap = "2.33.3"
 os_info = { version = "3", default-features = false }
 
 [[bin]]

diff --git a/kani-compiler/build.rs b/kani-compiler/build.rs
@@ -20,6 +20,8 @@ macro_rules! path_str {
 /// kani-compiler with nightly only. We also link to the rustup rustc_driver library for now.
 pub fn main() {
     // Add rustup to the rpath in order to properly link with the correct rustc version.
+
+    // This is for dev purposes only, if dev point/search toolchain in .rustup/toolchains/
     let rustup_home = env::var("RUSTUP_HOME").unwrap();
     let rustup_tc = env::var("RUSTUP_TOOLCHAIN").unwrap();
     let rustup_lib = path_str!([&rustup_home, "toolchains", &rustup_tc, "lib"]);

diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs
@@ -4,12 +4,12 @@
 use std::collections::HashSet;
 use std::path::Path;
 use std::path::PathBuf;
-use std::process::Command;
 use std::time::Instant;
 
 use anyhow::Result;
 use cargo_metadata::Package;
 
+use crate::session::setup_cargo_command;
 use crate::session::KaniSession;
 
 use super::metadata::AssessMetadata;
@@ -168,7 +168,8 @@ fn invoke_assess(
 ) -> Result<()> {
     let dir = manifest.parent().expect("file not in a directory?");
     let log = std::fs::File::create(logfile)?;
-    let mut cmd = Command::new("cargo");
+
+    let mut cmd = setup_cargo_command()?;
     cmd.arg("kani");
     // Use of options before 'assess' subcommand is a hack, these should be factored out.
     // TODO: --only-codegen should be outright an option to assess. (perhaps tests too?)

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
@@ -4,8 +4,8 @@
 use crate::args::VerificationArgs;
 use crate::call_single_file::to_rustc_arg;
 use crate::project::Artifact;
-use crate::session::KaniSession;
-use crate::{session, util};
+use crate::session::{setup_cargo_command, KaniSession};
+use crate::util;
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target};
@@ -109,9 +109,8 @@ impl KaniSession {
         let mut failed_targets = vec![];
         for package in packages {
             for verification_target in package_targets(&self.args, package) {
-                let mut cmd = Command::new("cargo");
-                cmd.arg(session::toolchain_shorthand())
-                    .args(&cargo_args)
+                let mut cmd = setup_cargo_command()?;
+                cmd.args(&cargo_args)
                     .args(vec!["-p", &package.name])
                     .args(&verification_target.to_args())
                     .args(&pkg_args)

diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs
@@ -7,7 +7,7 @@ use crate::args::common::Verbosity;
 use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat};
 use crate::call_cargo::cargo_config_args;
 use crate::call_single_file::base_rustc_flags;
-use crate::session::{lib_playback_folder, InstallType};
+use crate::session::{lib_playback_folder, setup_cargo_command, InstallType};
 use crate::{session, util};
 use anyhow::Result;
 use std::ffi::OsString;
@@ -17,8 +17,7 @@ use std::process::Command;
 use tracing::debug;
 
 pub fn playback_cargo(args: CargoPlaybackArgs) -> Result<()> {
-    let install = InstallType::new()?;
-    cargo_test(&install, args)
+    cargo_test(args)
 }
 
 pub fn playback_standalone(args: KaniPlaybackArgs) -> Result<()> {
@@ -93,9 +92,10 @@ fn build_test(install: &InstallType, args: &KaniPlaybackArgs) -> Result<PathBuf>
 }
 
 /// Invokes cargo test using Kani compiler and the provided arguments.
-/// TODO: This should likely be inside KaniSession, but KaniSession requires `VerificationArgs` today.
-/// For now, we just use InstallType directly.
-fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
+fn cargo_test(args: CargoPlaybackArgs) -> Result<()> {
+    let install = InstallType::new()?;
+    let mut cmd = setup_cargo_command()?;
+
     let rustc_args = base_rustc_flags(lib_playback_folder()?);
     let mut cargo_args: Vec<OsString> = vec!["test".into()];
 
@@ -123,9 +123,7 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> {
     }
 
     // Arguments that will only be passed to the target package.
-    let mut cmd = Command::new("cargo");
-    cmd.arg(session::toolchain_shorthand())
-        .args(&cargo_args)
+    cmd.args(&cargo_args)
         .env("RUSTC", &install.kani_compiler()?)
         // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
         // https://doc.rust-lang.org/cargo/reference/environment-variables.html

diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
@@ -379,3 +379,25 @@ fn init_logger(args: &VerificationArgs) {
     );
     tracing::subscriber::set_global_default(subscriber).unwrap();
 }
+
+// Setup the default version of cargo being run, based on the type/mode of installation for kani
+// If kani is being run in developer mode, then we use the one provided by rustup as we can assume that the developer will have rustup installed
+// For release versions of Kani, we use a version of cargo that's in the toolchain that's been symlinked during `cargo-kani` setup. This will allow
+// Kani to remove the runtime dependency on rustup later on.
+pub fn setup_cargo_command() -> Result<Command> {
+    let install_type = InstallType::new()?;
+
+    let cmd = match install_type {
+        InstallType::DevRepo(_) => {
+            let mut cmd = Command::new("cargo");
+            cmd.arg(self::toolchain_shorthand());
+            cmd
+        }
+        InstallType::Release(kani_dir) => {
+            let cargo_path = kani_dir.join("toolchain").join("bin").join("cargo");
+            Command::new(cargo_path)
+        }
+    };
+
+    Ok(cmd)
+}