Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
42 changes: 7 additions & 35 deletions charon/src/bin/charon-driver/driver.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,16 @@
//! Run the rustc compiler with our custom options and hooks.
use crate::CharonFailure;
use crate::translate::translate_crate;
use charon_lib::common::arg_value;
use charon_lib::options::CliOpts;
use charon_lib::transform::TransformCtx;
use itertools::Itertools;
use rustc_driver::{Callbacks, Compilation};
use rustc_interface::Config;
use rustc_interface::interface::Compiler;
use rustc_middle::ty::TyCtxt;
use rustc_middle::util::Providers;
use rustc_session::config::{OutputType, OutputTypes};
use std::ops::Deref;
use std::sync::atomic::{AtomicBool, Ordering};
use std::{env, fmt};

Expand Down Expand Up @@ -91,6 +92,10 @@ pub fn run_rustc_driver(options: &CliOpts) -> Result<Option<TransformCtx>, Charo
// Retreive the command-line arguments pased to `charon_driver`. The first arg is the path to
// the current executable, we skip it.
let mut compiler_args: Vec<String> = env::args().skip(1).collect();
trace!(
"charon-driver called with args: {}",
compiler_args.iter().format(" ")
);

// When called using cargo, we tell cargo to use `charon-driver` by setting the `RUSTC_WRAPPER`
// env var. This uses `charon-driver` for all the crates being compiled.
Expand All @@ -105,7 +110,7 @@ pub fn run_rustc_driver(options: &CliOpts) -> Result<Option<TransformCtx>, Charo
// Currently, we detect this by checking for "--target=", which is never set for host crates.
// This matches what Miri does, which hopefully makes it reliable enough. This relies on us
// always invoking cargo itself with `--target`, which `charon` ensures.
let is_target = arg_values(&compiler_args, "--target").next().is_some();
let is_target = arg_value(&compiler_args, "--target").is_some();
// Whether this is the crate we want to translate.
let is_selected_crate = !is_workspace_dependency && is_target;

Expand Down Expand Up @@ -176,39 +181,6 @@ impl<'a> Callbacks for RunCompilerNormallyCallbacks<'a> {
}
}

/// Returns the values of the command-line options that match `find_arg`. The options are built-in
/// to be of the form `--arg=value` or `--arg value`.
fn arg_values<'a, T: Deref<Target = str>>(
args: &'a [T],
needle: &'a str,
) -> impl Iterator<Item = &'a str> {
struct ArgFilter<'a, T> {
args: std::slice::Iter<'a, T>,
needle: &'a str,
}
impl<'a, T: Deref<Target = str>> Iterator for ArgFilter<'a, T> {
type Item = &'a str;
fn next(&mut self) -> Option<Self::Item> {
while let Some(arg) = self.args.next() {
let mut split_arg = arg.splitn(2, '=');
if split_arg.next() == Some(self.needle) {
return match split_arg.next() {
// `--arg=value` form
arg @ Some(_) => arg,
// `--arg value` form
None => self.args.next().map(|x| x.deref()),
};
}
}
None
}
}
ArgFilter {
args: args.iter(),
needle,
}
}

/// Custom `DefId` debug routine that doesn't print unstable values like ids and hashes.
fn def_id_debug(def_id: rustc_hir::def_id::DefId, f: &mut fmt::Formatter<'_>) -> fmt::Result {
rustc_middle::ty::tls::with_opt(|opt_tcx| {
Expand Down
8 changes: 3 additions & 5 deletions charon/src/bin/charon/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@
//! callbacks.
use anyhow::Result;
use charon_lib::{
common::arg_value,
logger,
options::{CHARON_ARGS, CliOpts},
};
Expand Down Expand Up @@ -93,17 +94,14 @@ fn translate_with_cargo(
cmd.env_remove("CARGO_PRIMARY_PACKAGE");
cmd.env(CHARON_ARGS, serde_json::to_string(&options).unwrap());
cmd.arg("build");
let is_specified = |arg| {
let mut iter = cargo_args.iter();
iter.any(|input| input.starts_with(arg))
};
if !is_specified("--target") {
if arg_value(&cargo_args, "--target").is_none() {
// Make sure the build target is explicitly set. This is needed to detect which crates are
// proc-macro/build-script in `charon-driver`.
cmd.arg("--target");
cmd.arg(&get_rustc_version()?.host);
}
cmd.args(cargo_args);
trace!("running {cmd:?}");
Ok(cmd
.spawn()
.expect("could not run cargo")
Expand Down
37 changes: 37 additions & 0 deletions charon/src/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -301,3 +301,40 @@ const STACK_PER_RECURSION: usize = 1024 * 1024; // 1MB
pub fn ensure_sufficient_stack<R>(f: impl FnOnce() -> R) -> R {
stacker::maybe_grow(RED_ZONE, STACK_PER_RECURSION, f)
}

/// Returns the values of the command-line options that match `find_arg`. The options are built-in
/// to be of the form `--arg=value` or `--arg value`.
pub fn arg_values<'a, T: AsRef<str>>(
args: &'a [T],
needle: &'a str,
) -> impl Iterator<Item = &'a str> {
struct ArgFilter<'a, T> {
args: std::slice::Iter<'a, T>,
needle: &'a str,
}
impl<'a, T: AsRef<str>> Iterator for ArgFilter<'a, T> {
type Item = &'a str;
fn next(&mut self) -> Option<Self::Item> {
while let Some(arg) = self.args.next() {
let mut split_arg = arg.as_ref().splitn(2, '=');
if split_arg.next() == Some(self.needle) {
return match split_arg.next() {
// `--arg=value` form
arg @ Some(_) => arg,
// `--arg value` form
None => self.args.next().map(|x| x.as_ref()),
};
}
}
None
}
}
ArgFilter {
args: args.iter(),
needle,
}
}

pub fn arg_value<'a, T: AsRef<str>>(args: &'a [T], needle: &'a str) -> Option<&'a str> {
arg_values(args, needle).next()
}
24 changes: 24 additions & 0 deletions charon/tests/cli.rs
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,30 @@ fn charon_cargo_target() -> Result<()> {
})
}

#[test]
fn charon_cargo_target_dir() -> Result<()> {
// Regression test for #938.
charon(
&[
"cargo",
"--print-llbc",
"--",
"-p",
"crate2",
"--target-dir=target/foo",
],
"tests/cargo/workspace",
|stdout, cmd| {
let search = "pub fn extra_random_number";
ensure!(
stdout.contains(search),
"Output of `{cmd}` is:\n{stdout:?}\nIt doesn't contain {search:?}."
);
Ok(())
},
)
}

#[test]
fn charon_rustc() -> Result<()> {
let path = "tests/cargo/workspace/crate1/src/lib.rs";
Expand Down