Merge branch 'main' into issue-xxxx-reverse-postorder

.gitignore

@@ -16,6 +16,7 @@ desktop.ini
 Session.vim
 .cproject
 .idea
+toolchains/
 *.iml
 .vscode
 .project

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"

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]]

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"]);

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?)

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)

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

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)
+}