Skip to content

SQUASH ME: More minor fix-ups and a parallel strategy for invoking charon #3391

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

Closed
mdittmer wants to merge 1 commit into from
Closed

SQUASH ME: More minor fix-ups and a parallel strategy for invoking charon #3391

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
52 changes: 52 additions & 0 deletions anneal/v2/Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions anneal/v2/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ fs2 = "0.4"
walkdir = "2.5.0"
sha2 = "0.10"
tempfile = "3.27.0"
rayon = "1.11.0"

# FIXME: Drop patch if forked change gets merged.
[patch.crates-io]
Expand Down
138 changes: 79 additions & 59 deletions anneal/v2/src/charon.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,13 @@
//! - Validating the extraction result.

use anyhow::Context as _;
use rayon::prelude::IntoParallelRefIterator as _;
use rayon::prelude::ParallelIterator as _;

/// Runs Charon on the specified packages to generate LLBC artifacts.
///
/// This function requires `LockedRoots` to ensure that it has exclusive access
/// to the `llbc` output directory. It iterates over each `AnnealArtifact`,
/// This function requires [`crate::resolve::LockedRoots`] to ensure that it has exclusive access
/// to the `llbc` output directory. It iterates over each [`crate::scanner::AnnealArtifact`],
/// constructs the appropriate `charon` command, and executes it.
///
/// It handles:
Expand All @@ -23,45 +25,43 @@ use anyhow::Context as _;
/// - **Entry Points**: passing the computed `start_from` roots to Charon to
/// minimize extraction scope.
/// - **Output Handling**: capturing stdout/stderr, parsing JSON compiler
/// messages, and rendering them using `DiagnosticMapper`.
/// messages, and rendering them using [`crate::diagnostics::DiagnosticMapper`].
pub fn run_charon(
args: &crate::resolve::Args,
toolchain: &crate::setup::Toolchain,
roots: &crate::resolve::LockedRoots,
packages: &[crate::scanner::AnnealArtifact],
toolchain: &crate::setup::Toolchain,
) -> anyhow::Result<()> {
let llbc_root = roots.llbc_root();
std::fs::create_dir_all(&llbc_root).context("Failed to create LLBC output directory")?;

let rust_bin = toolchain.rust_bin();
let rust_lib = toolchain.rust_lib();

// We prepend the managed Rust toolchain's `bin` directory to `PATH`. This is
// necessary because Charon is a compiler frontend that invokes `cargo` and
// `rustc` under the hood. To ensure hermeticity and correctness, we must force
// Charon to use our pinned nightly compiler version rather than falling back
// to whatever version happens to be installed in the system `PATH`.
let new_path = crate::util::prepend_to_env_var("PATH", rust_bin);
// Prepend to `PATH` to ensure that when `charon` delegates to tools such as
// `cargo` and `rustc` it invokes the correct rust toolchain.
let new_path = crate::util::prepend_to_env_var("PATH", &toolchain.rust_bin());

let lib_env_var =
if cfg!(target_os = "macos") { "DYLD_LIBRARY_PATH" } else { "LD_LIBRARY_PATH" };
// We set `LD_LIBRARY_PATH` (or `DYLD_LIBRARY_PATH` on macOS) to point to the
// managed Rust toolchain's `lib` directory. This is strictly required because
// `charon-driver` is a dynamic executable that links against `rustc` compiler
// dynamic libraries (like `librustc_driver-*.so`). Without this, the dynamic
// linker will fail to load the libraries when `charon-driver` is executed.
let new_lib_path = crate::util::prepend_to_env_var(lib_env_var, rust_lib);

for artifact in packages {
// Set `LD_LIBRARY_PATH` (or `DYLD_LIBRARY_PATH` on macOS) to point to the
// managed Rust toolchain's `lib` directory so that dynamic executables (like
// `charon-driver` which links against `rustc` dynamic libraries) can find them.
let new_lib_path = crate::util::prepend_to_env_var(lib_env_var, &toolchain.rust_lib());

// Global print mutex to prevent interleaved printing of consolidated artifact buffers.
let print_mutex = std::sync::Arc::new(std::sync::Mutex::new(()));

// Determine if we should show progress bar.
let show_progress = std::env::var("ANNEAL_NO_PROGRESS").is_err() && packages.len() == 1;

packages.par_iter().try_for_each(|artifact| {
if artifact.start_from.is_empty() {
continue;
return Ok(());
}

log::info!("Invoking Charon on package '{}'...", artifact.name.package_name);

let mut cmd = toolchain.command(crate::setup::Tool::Charon);

// We set `CHARON_TOOLCHAIN_IS_IN_PATH=1` to instruct Charon to bypass its
// Set `CHARON_TOOLCHAIN_IS_IN_PATH=1` to instruct Charon to bypass its
// standard toolchain resolution logic (which expects the compiler to be
// managed via `rustup`). Instead, it will directly use the `rustc` and
// `cargo` binaries we prepended to the `PATH` environment variable.
Expand All @@ -72,15 +72,10 @@ pub fn run_charon(
cmd.arg("cargo");
cmd.arg("--preset=aeneas");

// Output artifacts to target/anneal/<hash>/llbc.
let llbc_path = artifact.llbc_path(roots);
log::debug!("Writing .llbc file to {:?}", llbc_path);
cmd.arg("--dest-file").arg(llbc_path);

// We use `--abort-on-error` to fail fast. If Charon (or `rustc`)
// encounters a compilation error or translation failure (e.g., an
// unsupported Rust feature), it will terminate the process immediately
// rather than attempting to proceed and translate other parts of the crate.
// Fail fast on errors.
cmd.arg("--abort-on-error");

for item in &artifact.items {
Expand Down Expand Up @@ -141,11 +136,12 @@ pub fn run_charon(

cmd.arg("--manifest-path").arg(&artifact.manifest_path);

use crate::resolve::AnnealTargetKind::*;
match artifact.target_kind {
crate::resolve::AnnealTargetKind::Lib | crate::resolve::AnnealTargetKind::RLib | crate::resolve::AnnealTargetKind::ProcMacro | crate::resolve::AnnealTargetKind::CDyLib | crate::resolve::AnnealTargetKind::DyLib | crate::resolve::AnnealTargetKind::StaticLib => cmd.arg("--lib"),
crate::resolve::AnnealTargetKind::Bin => cmd.args(["--bin", &artifact.name.target_name]),
crate::resolve::AnnealTargetKind::Example => cmd.args(["--example", &artifact.name.target_name]),
crate::resolve::AnnealTargetKind::Test => cmd.args(["--test", &artifact.name.target_name]),
Lib | RLib | ProcMacro | CDyLib | DyLib | StaticLib => cmd.arg("--lib"),
Bin => cmd.args(["--bin", &artifact.name.target_name]),
Example => cmd.args(["--example", &artifact.name.target_name]),
Test => cmd.args(["--test", &artifact.name.target_name]),
};

// Forward all feature-related flags.
Expand All @@ -159,10 +155,9 @@ pub fn run_charon(
cmd.arg("--features").arg(feature);
}

// We share `CARGO_TARGET_DIR` (`target/anneal/cargo_target`) across all
// Charon invocations to enable Cargo's incremental build cache. This
// prevents Cargo from recompiling identical workspace dependencies from
// scratch for each individual target, saving significant compilation time.
// Reuse the main target directory for dependencies to save time: share
// `CARGO_TARGET_DIR` (`target/anneal/cargo_target`) across all Charon
// invocations to enable Cargo's incremental build cache.
cmd.env("CARGO_TARGET_DIR", roots.cargo_target_dir());

log::debug!("Executing charon command: {:?}", cmd);
Expand All @@ -179,18 +174,28 @@ pub fn run_charon(
let safety_buffer = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
let safety_buffer_clone = std::sync::Arc::clone(&safety_buffer);

// Local buffer to collect all output (diagnostics) for this artifact.
let artifact_diagnostics = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
let artifact_diagnostics_clone = std::sync::Arc::clone(&artifact_diagnostics);

let mut mapper = crate::diagnostics::DiagnosticMapper::new(roots.workspace().clone());

let res = crate::util::run_command_with_progress(cmd, "Compiling...", move |line, pb| {
let progress_msg = if show_progress { Some("Compiling...") } else { None };

let res = crate::util::run_command_with_progress(cmd, progress_msg, move |line, pb| {
if let Ok(msg) = serde_json::from_str::<cargo_metadata::Message>(line) {
match msg {
cargo_metadata::Message::CompilerArtifact(a) => {
pb.set_message(format!("Compiling {}", a.target.name));
if let Some(p) = pb {
p.set_message(format!("Compiling {}", a.target.name));
}
}
cargo_metadata::Message::CompilerMessage(msg) => {
pb.suspend(|| {
mapper.render_miette(&msg.message, |s| eprintln!("{}", s));
});
let mut rendered = String::new();
mapper.render_miette(&msg.message, |s| rendered.push_str(&s));
if !rendered.is_empty() {
artifact_diagnostics_clone.lock().unwrap().push(rendered);
}
if matches!(
msg.message.level,
cargo_metadata::diagnostic::DiagnosticLevel::Error | cargo_metadata::diagnostic::DiagnosticLevel::Ice
Expand All @@ -211,15 +216,23 @@ pub fn run_charon(

log::trace!("Charon for '{}' took {:.2?}", artifact.name.package_name, start.elapsed());

// FIXME: There's a subtle edge case here – if we get error output AND
// Rustc ICE's, there's a good chance that the JSON error messages we
// print won't include all relevant information – some will be printed
// via stderr. In this case, `output_error = true` and so we bail and
// discard stderr, which will swallow information from the user.
// Lock the print mutex to print this artifact's consolidated output atomically.
let _lock = print_mutex.lock().unwrap();

// Print all collected diagnostics for this artifact.
let diags = artifact_diagnostics.lock().unwrap();
if !diags.is_empty() {
eprintln!("=== Diagnostics for '{}' ===", artifact.name.package_name);
for diag in diags.iter() {
eprintln!("{}", diag);
}
}

if output_error.load(std::sync::atomic::Ordering::Relaxed) {
anyhow::bail!("Diagnostic error in charon");
} else if !res.status.success() {
// "Silent Death" dump.
// Print safety buffer on failure (also atomically since we hold print_mutex).
eprintln!("=== Failure output for '{}' ===", artifact.name.package_name);
for line in safety_buffer.lock().unwrap().iter() {
eprintln!("{}", line);
}
Expand All @@ -229,7 +242,9 @@ pub fn run_charon(
}
anyhow::bail!("Charon failed with status: {}", res.status);
}
}

Ok(())
})?;

Ok(())
}
Expand All @@ -244,12 +259,15 @@ mod tests {

#[test]
fn test_run_charon_simple() {
// 1. Create a temporary directory
// Disable progress bar for test.
unsafe { std::env::set_var("ANNEAL_NO_PROGRESS", "1"); }

// 1. Create a temporary directory.
let temp_dir = tempfile::tempdir().unwrap();
let proj_dir = temp_dir.path().join("test_proj");
fs::create_dir_all(&proj_dir).unwrap();

// 2. Create a simple Cargo.toml
// 2. Create a simple Cargo.toml.
let cargo_toml = r#"
[package]
name = "test_proj"
Expand All @@ -261,7 +279,7 @@ mod tests {
"#;
fs::write(proj_dir.join("Cargo.toml"), cargo_toml).unwrap();

// 3. Create a simple src/lib.rs
// 3. Create a simple src/lib.rs.
fs::create_dir_all(proj_dir.join("src")).unwrap();
let lib_rs = r#"
pub fn add(left: usize, right: usize) -> usize {
Expand All @@ -270,36 +288,38 @@ mod tests {
"#;
fs::write(proj_dir.join("src").join("lib.rs"), lib_rs).unwrap();

// 4. Construct Args pointing to this temp project
// 4. Construct Args pointing to this temp project.
let args = Args::try_parse_from(&[
"cargo-anneal",
"--manifest-path",
proj_dir.join("Cargo.toml").to_str().unwrap(),
]).unwrap();

// 5. Resolve roots
// 5. Resolve roots.
let roots = resolve_roots(&args).unwrap();

// 6. Scan workspace (our simplified scanner will find `add` function)
// 6. Scan workspace (our simplified scanner will find `add` function).
let packages = scan_workspace(&roots).unwrap();
assert_eq!(packages.len(), 1);
assert!(packages[0].start_from.contains("crate::add"));

// 7. Lock run root
// 7. Lock run root.
let locked_roots = roots.lock_run_root().unwrap();

// 8. Resolve test-only stripped toolchain and run charon
// 8. Resolve test-only stripped toolchain and run charon.
let toolchain_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
.join("tests")
.join("toolchains")
.join("charon-only");
let toolchain = crate::setup::Toolchain::new_test(toolchain_root);

let res = run_charon(&args, &locked_roots, &packages, &toolchain);
let res = run_charon(&args, &toolchain, &locked_roots, &packages);
assert!(res.is_ok(), "charon failed: {:?}", res.err());

// 9. Verify .llbc file exists
// 9. Verify .llbc file exists.
let llbc_path = packages[0].llbc_path(&locked_roots);
assert!(llbc_path.exists(), "llbc file not found at {:?}", llbc_path);

unsafe { std::env::remove_var("ANNEAL_NO_PROGRESS"); }
}
}
Loading
Loading