Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move all rustc arguments to kani-driver #2174

Merged
merged 6 commits into from
Feb 3, 2023
Merged

Move all rustc arguments to kani-driver #2174

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0ae2357
Move all rustc arguments to kani-driver
celinval Feb 2, 2023
dd2d668
Adjust std build regression script
celinval Feb 2, 2023
7bed136
Fix unsound experiments
celinval Feb 2, 2023
7db5b7f
Merge branch 'main' into issue-2137-move-args
celinval Feb 2, 2023
1b7247f
Remove details about std override
celinval Feb 2, 2023
fee8c5c
Update call_cargo.rs
celinval Feb 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Cargo.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -523,6 +523,8 @@ dependencies = [
"rustc-demangle",
"serde",
"serde_json",
"strum",
"strum_macros",
"toml",
"tracing",
"tracing-subscriber",
Expand Down
136 changes: 1 addition & 135 deletions kani-compiler/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,48 +47,9 @@ use rustc_hir::definitions::DefPathHash;
use rustc_interface::Config;
use rustc_session::config::ErrorOutputType;
use session::json_panic_hook;
use std::env;
use std::ffi::OsStr;
use std::path::PathBuf;
use std::rc::Rc;
use std::{env, fs};

/// This function generates all rustc configurations required by our goto-c codegen.
fn rustc_gotoc_flags(lib_path: &str) -> Vec<String> {
// The option below provides a mechanism by which definitions in the
// standard library can be overriden. See
// https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Globally.20override.20an.20std.20macro/near/268873354
// for more details.
let kani_std_rlib = PathBuf::from(lib_path).join("libstd.rlib");
let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
let args = vec![
"-C",
"overflow-checks=on",
"-C",
"panic=abort",
"-Z",
"unstable-options",
"-Z",
"panic_abort_tests=yes",
"-Z",
"trim-diagnostic-paths=no",
"-Z",
"human_readable_cgu_names",
"-Z",
"always-encode-mir",
"--cfg=kani",
"-Z",
"crate-attr=feature(register_tool)",
"-Z",
"crate-attr=register_tool(kanitool)",
"-L",
lib_path,
"--extern",
"kani",
"--extern",
kani_std_wrapper.as_str(),
];
args.iter().map(|s| s.to_string()).collect()
}

/// Main function. Configure arguments and run the compiler.
fn main() -> Result<(), &'static str> {
Expand Down Expand Up @@ -152,35 +113,9 @@ impl Callbacks for KaniCallbacks {
}
}

/// The Kani root folder has all binaries inside bin/ and libraries inside lib/.
/// This folder can also be used as a rustc sysroot.
fn kani_root() -> PathBuf {
match env::current_exe() {
Ok(exe_path) => {
let mut path = fs::canonicalize(&exe_path).unwrap_or(exe_path);
// Current folder (bin/)
path.pop();
// Top folder
path.pop();
path
}
Err(e) => panic!("Failed to get current exe path: {e}"),
}
}

/// Generate the arguments to pass to rustc_driver.
fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
let mut rustc_args = vec![String::from("rustc")];
if args.get_flag(parser::GOTO_C) {
let mut default_path = kani_root();
default_path.push("lib");
let gotoc_args = rustc_gotoc_flags(
args.get_one::<String>(parser::KANI_LIB)
.unwrap_or(&default_path.to_str().unwrap().to_string()),
);
rustc_args.extend_from_slice(&gotoc_args);
}

if args.get_flag(parser::RUSTC_VERSION) {
rustc_args.push(String::from("--version"))
}
Expand All @@ -192,9 +127,6 @@ fn generate_rustc_args(args: &ArgMatches) -> Vec<String> {
if let Some(extra_flags) = args.get_raw(parser::RUSTC_OPTIONS) {
extra_flags.for_each(|arg| rustc_args.push(convert_arg(arg)));
}
let sysroot = sysroot_path(args);
rustc_args.push(String::from("--sysroot"));
rustc_args.push(convert_arg(sysroot.as_os_str()));
tracing::debug!(?rustc_args, "Compile");
rustc_args
}
Expand All @@ -205,72 +137,6 @@ fn convert_arg(arg: &OsStr) -> String {
arg.to_str().expect(format!("[Error] Cannot parse argument \"{arg:?}\".").as_str()).to_string()
}

/// Get the sysroot, for our specific version of Rust nightly.
///
/// Rust normally finds its sysroot by looking at where itself (the `rustc`
/// executable) is located. This will fail for us because we're `kani-compiler`
/// and not located under the rust sysroot.
///
/// We do know the actual name of the toolchain we need, however.
/// We look for our toolchain in the usual place for rustup.
///
/// We previously used to pass `--sysroot` in `KANIFLAGS` from `kani-driver`,
/// but this failed to have effect when building a `build.rs` file.
/// This wasn't used anywhere but passing down here, so we've just migrated
/// the code to find the sysroot path directly into this function.
///
/// This function will soon be removed.
#[deprecated]
fn toolchain_sysroot_path() -> PathBuf {
// If we're installed normally, we'll find `$KANI/toolchain` as a symlink to our desired toolchain
{
let kani_root = kani_root();
let toolchain_path = kani_root.join("toolchain");
if toolchain_path.exists() {
return toolchain_path;
}
}

// rustup sets some environment variables during build, but this is not clearly documented.
// https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
// We're using RUSTUP_TOOLCHAIN here, which is going to be set by our `rust-toolchain.toml` file.
// This is a *compile-time* constant, not a dynamic lookup at runtime, so this is reliable.
let toolchain = env!("RUSTUP_TOOLCHAIN");

// We use the home crate to do a *runtime* determination of where rustup toolchains live
let rustup = home::rustup_home().expect("Couldn't find RUSTUP_HOME");
let path = rustup.join("toolchains").join(toolchain);

if !path.exists() {
panic!("Couldn't find Kani Rust toolchain {toolchain}. Tried: {}", path.display());
}
path
}

/// Get the sysroot relative to the binary location.
///
/// Kani uses a custom sysroot. The `std` library and dependencies are compiled in debug mode and
/// include the entire MIR definitions needed by Kani.
///
/// We do provide a `--sysroot` option that users may want to use instead.
#[allow(deprecated)]
fn sysroot_path(args: &ArgMatches) -> PathBuf {
let sysroot_arg = args.get_one::<String>(parser::SYSROOT);
let path = if let Some(s) = sysroot_arg {
PathBuf::from(s)
} else if !args.get_flag(parser::GOTO_C) {
toolchain_sysroot_path()
} else {
kani_root()
};

if !path.exists() {
panic!("Couldn't find Kani Rust toolchain {:?}.", path.display());
}
tracing::debug!(?path, ?sysroot_arg, "Sysroot path.");
path
}

/// Find the stub mapping for the given harness.
///
/// This function is necessary because Kani currently allows a harness to be
Expand Down
2 changes: 2 additions & 0 deletions kani-driver/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@ rustc-demangle = "0.1.21"
pathdiff = "0.2.1"
rayon = "1.5.3"
comfy-table = "6.0.0"
strum = {version = "0.24.0"}
strum_macros = {version = "0.24.0"}
tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
tracing-tree = "0.2.2"
Expand Down
32 changes: 11 additions & 21 deletions kani-driver/src/call_cargo.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

use crate::args::KaniArgs;
use crate::session::{KaniSession, ReachabilityMode};
use crate::session::KaniSession;
use anyhow::{bail, Context, Result};
use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
use cargo_metadata::{Message, Metadata, MetadataCommand, Package};
use std::ffi::OsString;
use std::ffi::{OsStr, OsString};
use std::fs;
use std::io::BufReader;
use std::path::{Path, PathBuf};
Expand Down Expand Up @@ -58,8 +58,9 @@ impl KaniSession {
fs::remove_dir_all(&target_dir)?;
}

let mut kani_args = self.kani_specific_flags();
let rustc_args = self.kani_rustc_flags();
let kani_args = self.kani_compiler_flags();
let mut rustc_args = self.kani_rustc_flags();
rustc_args.push("--kani-flags".into());

let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
if let Some(path) = &self.args.cargo.manifest_path {
Expand Down Expand Up @@ -99,21 +100,8 @@ impl KaniSession {
}

// Arguments that will only be passed to the target package.
let mut pkg_args: Vec<OsString> = vec![];
match self.reachability_mode() {
ReachabilityMode::ProofHarnesses => {
pkg_args.extend(["--".into(), "--reachability=harnesses".into()]);
}
ReachabilityMode::AllPubFns => {
pkg_args.extend(["--".into(), "--reachability=pub_fns".into()]);
}
ReachabilityMode::Tests => {
pkg_args.extend(["--".into(), "--reachability=tests".into()]);
}
}

// Only joing them at the end. All kani flags must come first.
kani_args.extend_from_slice(&rustc_args);
let mut pkg_args: Vec<String> = vec![];
pkg_args.extend(["--".to_string(), format!("--reachability={}", self.reachability_mode())]);

let mut found_target = false;
let packages = packages_to_verify(&self.args, &metadata);
Expand All @@ -125,8 +113,10 @@ impl KaniSession {
.args(&target.to_args())
.args(&pkg_args)
.env("RUSTC", &self.kani_compiler)
.env("RUSTFLAGS", "--kani-flags")
.env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "))
.env("KANIFLAGS", kani_args.join(" "))
// Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
celinval marked this conversation as resolved.
Show resolved Hide resolved
.env("CARGO_TERM_PROGRESS_WHEN", "never");

self.run_cargo(cmd)?;
Expand Down
69 changes: 48 additions & 21 deletions kani-driver/src/call_single_file.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use std::ffi::OsString;
use std::path::Path;
use std::process::Command;

use crate::session::{KaniSession, ReachabilityMode};
use crate::session::{base_folder, lib_folder, KaniSession};

impl KaniSession {
/// Used by `kani` and not `cargo-kani` to process a single Rust file into a `.symtab.json`
Expand All @@ -17,15 +17,8 @@ impl KaniSession {
crate_name: &String,
outdir: &Path,
) -> Result<()> {
let mut kani_args = self.kani_specific_flags();
kani_args.push(
match self.reachability_mode() {
ReachabilityMode::ProofHarnesses => "--reachability=harnesses",
ReachabilityMode::AllPubFns => "--reachability=pub_fns",
ReachabilityMode::Tests => "--reachability=tests",
}
.into(),
);
let mut kani_args = self.kani_compiler_flags();
kani_args.push(format!("--reachability={}", self.reachability_mode()));

let mut rustc_args = self.kani_rustc_flags();
rustc_args.push(file.into());
Expand Down Expand Up @@ -65,10 +58,9 @@ impl KaniSession {
Ok(())
}

/// These arguments are arguments passed to kani-compiler that are `kani` specific.
/// These are also used by call_cargo to pass as the env var KANIFLAGS.
pub fn kani_specific_flags(&self) -> Vec<OsString> {
let mut flags = vec![OsString::from("--goto-c")];
/// These arguments are arguments passed to kani-compiler that are `kani` compiler specific.
pub fn kani_compiler_flags(&self) -> Vec<String> {
let mut flags = vec![];

if self.args.debug {
flags.push("--log-level=debug".into());
Expand All @@ -93,19 +85,57 @@ impl KaniSession {
flags.push("--enable-stubbing".into());
}
if let Some(harness) = &self.args.harness {
flags.push(format!("--harness={harness}").into());
flags.push(format!("--harness={harness}"));
}

// This argument will select the Kani flavour of the compiler. It will be removed before
// rustc driver is invoked.
flags.push("--goto-c".into());

#[cfg(feature = "unsound_experiments")]
flags.extend(self.args.unsound_experiments.process_args());

flags
}

/// These arguments are arguments passed to kani-compiler that are `rustc` specific.
/// These are also used by call_cargo to pass as the env var KANIFLAGS.
/// This function generates all rustc configurations required by our goto-c codegen.
pub fn kani_rustc_flags(&self) -> Vec<OsString> {
let mut flags = Vec::<OsString>::new();
let lib_path = lib_folder().unwrap();
let kani_std_rlib = lib_path.join("libstd.rlib");
let kani_std_wrapper = format!("noprelude:std={}", kani_std_rlib.to_str().unwrap());
let sysroot = base_folder().unwrap();
let args = vec![
"-C",
"overflow-checks=on",
"-C",
"panic=abort",
"-C",
"symbol-mangling-version=v0",
"-Z",
"unstable-options",
"-Z",
"panic_abort_tests=yes",
"-Z",
"trim-diagnostic-paths=no",
"-Z",
"human_readable_cgu_names",
"-Z",
"always-encode-mir",
"--cfg=kani",
"-Z",
"crate-attr=feature(register_tool)",
"-Z",
"crate-attr=register_tool(kanitool)",
"--sysroot",
sysroot.to_str().unwrap(),
"-L",
lib_path.to_str().unwrap(),
"--extern",
"kani",
"--extern",
kani_std_wrapper.as_str(),
];
let mut flags: Vec<_> = args.iter().map(OsString::from).collect();
if self.args.use_abs {
flags.push("-Z".into());
flags.push("force-unstable-if-unmarked=yes".into()); // ??
Expand All @@ -124,9 +154,6 @@ impl KaniSession {
}
}

flags.push("-C".into());
flags.push("symbol-mangling-version=v0".into());

// e.g. compiletest will set 'compile-flags' here and we should pass those down to rustc
// and we fail in `tests/kani/Match/match_bool.rs`
if let Ok(str) = std::env::var("RUSTFLAGS") {
Expand Down
Loading