Merge branch 'main' into issue-2690-ptr-access

.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-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -2,7 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use stable_mir::mir::{BasicBlock, BasicBlockIdx};
+use stable_mir::mir::{BasicBlock, BasicBlockIdx, Body};
+use std::collections::HashSet;
 use tracing::debug;
 
 pub fn bb_label(bb: BasicBlockIdx) -> String {
@@ -72,3 +73,32 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  }
 }
+
+/// Iterate over the basic blocks in reverse post-order.
+///
+/// The `reverse_postorder` function used before was internal to the compiler and reflected the
+/// internal body representation.
+///
+/// As we introduce transformations on the top of SMIR body, there will be not guarantee of a
+/// 1:1 relationship between basic blocks from internal body and monomorphic body from StableMIR.
+pub fn reverse_postorder(body: &Body) -> impl Iterator<Item = BasicBlockIdx> {
+ postorder(body, 0, &mut HashSet::with_capacity(body.blocks.len())).into_iter().rev()
+}
+
+fn postorder(
+ body: &Body,
+ bb: BasicBlockIdx,
+ visited: &mut HashSet<BasicBlockIdx>,
+) -> Vec<BasicBlockIdx> {
+ if visited.contains(&bb) {
+ return vec![];
+ }
+ visited.insert(bb);
+
+ let mut result = vec![];
+ for succ in body.blocks[bb].terminator.successors() {
+ result.append(&mut postorder(body, succ, visited));
+ }
+ result.push(bb);
+ result
+}

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -3,10 +3,10 @@
 
 //! This file contains functions related to codegenning MIR functions into gotoc
 
+use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
-use rustc_middle::mir::traversal::reverse_postorder;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Local};
 use stable_mir::ty::{RigidTy, TyKind};
@@ -67,9 +67,7 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_declare_variables(&body);
 
  // Get the order from internal body for now.
- let internal_body = self.current_fn().body_internal();
- reverse_postorder(internal_body)
- .for_each(|(bb, _)| self.codegen_block(bb.index(), &body.blocks[bb.index()]));
+ reverse_postorder(&body).for_each(|bb| self.codegen_block(bb, &body.blocks[bb]));
 
  let loc = self.codegen_span_stable(instance.def.span());
  let stmts = self.current_fn_mut().extract_block();

kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs

@@ -4,7 +4,6 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Stmt;
 use cbmc::InternedString;
-use rustc_middle::mir::Body as BodyInternal;
 use rustc_middle::ty::Instance as InstanceInternal;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
@@ -21,8 +20,6 @@ pub struct CurrentFnCtx<'tcx> {
  instance: Instance,
  /// The crate this function is from
  krate: String,
- /// The MIR for the current instance. This is using the internal representation.
- mir: &'tcx BodyInternal<'tcx>,
  /// The current instance. This is using the internal representation.
  instance_internal: InstanceInternal<'tcx>,
  /// A list of local declarations used to retrieve MIR component types.
@@ -53,7 +50,6 @@ impl<'tcx> CurrentFnCtx<'tcx> {
  Self {
  block: vec![],
  instance,
- mir: gcx.tcx.instance_mir(instance_internal.def),
  instance_internal,
  krate: instance.def.krate().name,
  locals,
@@ -94,11 +90,6 @@ impl<'tcx> CurrentFnCtx<'tcx> {
  self.instance
  }
 
- /// The internal MIR for the function we are currently compiling using internal APIs.
- pub fn body_internal(&self) -> &'tcx BodyInternal<'tcx> {
- self.mir
- }
-
  /// The name of the function we are currently compiling
  pub fn name(&self) -> String {
  self.name.clone()

kani-driver/src/args/mod.rs

@@ -79,6 +79,9 @@ pub struct StandaloneArgs {
 
  #[command(subcommand)]
  pub command: Option<StandaloneSubcommand>,
+
+ #[arg(long, hide = true)]
+ pub crate_name: Option<String>,
 }
 
 /// Kani takes optional subcommands to request specialized behavior.

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