diff --git a/anneal/v2/src/charon.rs b/anneal/v2/src/charon.rs index 5bde6d6a76..a95ffb4725 100644 --- a/anneal/v2/src/charon.rs +++ b/anneal/v2/src/charon.rs @@ -50,14 +50,29 @@ pub fn run_charon( // 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 = show_progress && packages.len() == 1; + // Initialize MultiProgress if progress is enabled. + let mp = if show_progress { + Some(std::sync::Arc::new(indicatif::MultiProgress::new())) + } else { + None + }; packages.par_iter().try_for_each(|artifact| { if artifact.start_from.is_empty() { return Ok(()); } + let pb = mp.as_ref().map(|m| { + let pb = m.add(indicatif::ProgressBar::new_spinner()); + pb.set_style( + indicatif::ProgressStyle::default_spinner() + .template("{spinner:.green} {msg}") + .unwrap(), + ); + pb.set_message("Compiling..."); + pb + }); + log::info!("Invoking Charon on package '{}'...", artifact.name.package_name); let mut cmd = toolchain.command(crate::setup::Tool::Charon); @@ -185,9 +200,8 @@ pub fn run_charon( let mut mapper = crate::diagnostics::DiagnosticMapper::new(roots.workspace().clone()); - let progress_msg = if show_progress { Some("Compiling...") } else { None }; - - let res = crate::util::run_command_with_progress(cmd, progress_msg, move |line, pb| { + let pb_clone = pb.clone(); + let res = crate::util::run_command_with_progress(cmd, pb_clone, move |line, pb| { if let Ok(msg) = serde_json::from_str::(line) { match msg { cargo_metadata::Message::CompilerArtifact(a) => { @@ -203,7 +217,8 @@ pub fn run_charon( } if matches!( msg.message.level, - cargo_metadata::diagnostic::DiagnosticLevel::Error | cargo_metadata::diagnostic::DiagnosticLevel::Ice + cargo_metadata::diagnostic::DiagnosticLevel::Error + | cargo_metadata::diagnostic::DiagnosticLevel::Ice ) { output_error_clone.store(true, std::sync::atomic::Ordering::Relaxed); } @@ -257,15 +272,14 @@ pub fn run_charon( #[cfg(test)] mod tests { use super::*; - use std::fs; use crate::resolve::{Args, resolve_roots}; use crate::scanner::scan_workspace; use clap::Parser as _; + use std::fs; + #[cfg(feature = "exocrate_tests")] #[test] fn test_run_charon_simple() { - // The test environment disables progress bar via configuration injection. - // 1. Create a temporary directory. let temp_dir = tempfile::tempdir().unwrap(); let proj_dir = temp_dir.path().join("test_proj"); @@ -297,7 +311,8 @@ mod tests { "cargo-anneal", "--manifest-path", proj_dir.join("Cargo.toml").to_str().unwrap(), - ]).unwrap(); + ]) + .unwrap(); // 5. Resolve roots. let roots = resolve_roots(&args).unwrap(); @@ -310,20 +325,20 @@ mod tests { // 7. Lock run root. let locked_roots = roots.lock_run_root().unwrap(); - // 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); + // 8. Resolve standard developer toolchain and run charon. + let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain"); - let res = run_charon(&args, &toolchain, &locked_roots, &packages, false); + let res = run_charon( + &args, + &toolchain, + &locked_roots, + &packages, + false, // show_progress + ); assert!(res.is_ok(), "charon failed: {:?}", res.err()); // 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); - - } } diff --git a/anneal/v2/src/diagnostics.rs b/anneal/v2/src/diagnostics.rs index 31b71eb118..fa65c6d0c6 100644 --- a/anneal/v2/src/diagnostics.rs +++ b/anneal/v2/src/diagnostics.rs @@ -48,7 +48,9 @@ impl miette::Diagnostic for MappedError { self.help.as_ref().map(|h| Box::new(h.clone()) as Box) } - fn related<'a>(&'a self) -> Option + 'a>> { + fn related<'a>( + &'a self, + ) -> Option + 'a>> { if self.related.is_empty() { None } else { @@ -120,7 +122,10 @@ impl DiagnosticMapper { where F: FnMut(String), { - let mut mapped_paths_and_spans: std::collections::HashMap> = std::collections::HashMap::new(); + let mut mapped_paths_and_spans: std::collections::HashMap< + std::path::PathBuf, + Vec<&DiagnosticSpan>, + > = std::collections::HashMap::new(); // 1) Group spans by mapped path. for s in &diag.spans { @@ -151,7 +156,8 @@ impl DiagnosticMapper { let mut all_errors = Vec::new(); // Sort the paths to have the primary path first. - let mut paths: Vec = mapped_paths_and_spans.keys().cloned().collect(); + let mut paths: Vec = + mapped_paths_and_spans.keys().cloned().collect(); paths.sort_by_key(|p| p != &main_path); for p in paths { diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs index 08af491a6b..b29b79f5ec 100644 --- a/anneal/v2/src/main.rs +++ b/anneal/v2/src/main.rs @@ -9,13 +9,13 @@ use clap::Parser as _; -mod util; +mod charon; mod diagnostics; -mod resolve; mod parse; +mod resolve; mod scanner; -mod charon; mod setup; +mod util; /// Anneal: A Literate Verification Toolchain #[derive(clap::Parser, Debug)] @@ -31,12 +31,19 @@ enum Commands { Setup(SetupArgs), /// Expand a crate (runs Charon) Expand(ExpandArgs), - /// Setup test-only stripped toolchain (dev only) - /// - /// FIXME: Add GitHub actions that will block changes that would update - /// tests/toolchains/ files if TestSetup were invoked without committing them. + + /// Helper to acquire shared or exclusive locks for multi-process integration testing (dev only) #[cfg(feature = "exocrate_tests")] - TestSetup, + TestLockHelper { + #[arg(long)] + role: String, + #[arg(long)] + lock_dir: std::path::PathBuf, + #[arg(long)] + log_file: std::path::PathBuf, + #[arg(long)] + sig_file: std::path::PathBuf, + }, } #[derive(clap::Parser, Debug)] @@ -54,13 +61,15 @@ pub struct ExpandArgs { /// Controls where LLBC output is placed on the filesystem #[arg(long, value_name = "output-dir")] pub output_dir: Option, + + /// Do not show compilation progress bars + #[arg(long)] + pub no_progress: bool, } fn setup(args: SetupArgs) { - crate::setup::run_setup(crate::setup::SetupArgs { - local_archive: args.local_archive, - }) - .expect("failed to setup toolchain"); + crate::setup::run_setup(crate::setup::SetupArgs { local_archive: args.local_archive }) + .expect("failed to setup toolchain"); } fn expand(args: ExpandArgs) -> anyhow::Result<()> { @@ -75,8 +84,14 @@ fn expand(args: ExpandArgs) -> anyhow::Result<()> { locked_roots.llbc_override = Some(output_dir); } let toolchain = crate::setup::Toolchain::resolve()?; - let show_progress = std::env::var("ANNEAL_NO_PROGRESS").is_err(); - crate::charon::run_charon(&args.resolve_args, &toolchain, &locked_roots, &packages, show_progress)?; + let show_progress = !args.no_progress; + crate::charon::run_charon( + &args.resolve_args, + &toolchain, + &locked_roots, + &packages, + show_progress, + )?; Ok(()) } @@ -101,10 +116,13 @@ fn main() { std::process::exit(1); } } + #[cfg(feature = "exocrate_tests")] - Commands::TestSetup => { - if let Err(e) = crate::setup::run_test_setup() { - eprintln!("TestSetup failed: {:?}", e); + Commands::TestLockHelper { role, lock_dir, log_file, sig_file } => { + if let Err(e) = + crate::util::run_test_lock_helper(&role, &lock_dir, &log_file, &sig_file) + { + eprintln!("TestLockHelper failed: {:?}", e); std::process::exit(1); } } @@ -116,8 +134,7 @@ mod tests { #[cfg(feature = "exocrate_tests")] #[test] fn test_setup_and_toolchain_paths() { - // 1. Run setup (this compiles dependencies and installs them locally to target/.anneal - // because __ANNEAL_LOCAL_DEV=1 is defined in our .cargo/config.toml!). + // 1. Run setup. super::setup(super::SetupArgs { // ASSUMPTION: Dependency builder installs archive at // `target/anneal-exocrate.tar.zst`. @@ -128,10 +145,29 @@ mod tests { let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain"); // 3. Verify that all returned paths exist as directories. + // Note: these assertions would be more appropriate in the setup.rs module, + // but including them here avoids introducing multiple tests that attempt to + // extract the (large) anneal exocrate archive. assert!(toolchain.root().is_dir(), "root is not a directory: {:?}", toolchain.root()); - assert!(toolchain.aeneas_bin_dir().is_dir(), "aeneas_bin_dir is not a directory: {:?}", toolchain.aeneas_bin_dir()); - assert!(toolchain.rust_sysroot().is_dir(), "rust_sysroot is not a directory: {:?}", toolchain.rust_sysroot()); - assert!(toolchain.rust_bin().is_dir(), "rust_bin is not a directory: {:?}", toolchain.rust_bin()); - assert!(toolchain.rust_lib().is_dir(), "rust_lib is not a directory: {:?}", toolchain.rust_lib()); + assert!( + toolchain.aeneas_bin_dir().is_dir(), + "aeneas_bin_dir is not a directory: {:?}", + toolchain.aeneas_bin_dir() + ); + assert!( + toolchain.rust_sysroot().is_dir(), + "rust_sysroot is not a directory: {:?}", + toolchain.rust_sysroot() + ); + assert!( + toolchain.rust_bin().is_dir(), + "rust_bin is not a directory: {:?}", + toolchain.rust_bin() + ); + assert!( + toolchain.rust_lib().is_dir(), + "rust_lib is not a directory: {:?}", + toolchain.rust_lib() + ); } } diff --git a/anneal/v2/src/resolve.rs b/anneal/v2/src/resolve.rs index 1f302b58b3..e60d363e5a 100644 --- a/anneal/v2/src/resolve.rs +++ b/anneal/v2/src/resolve.rs @@ -267,7 +267,9 @@ pub fn resolve_roots(args: &Args) -> anyhow::Result { Ok(roots) } -fn resolve_run_roots(metadata: &cargo_metadata::Metadata) -> (std::path::PathBuf, std::path::PathBuf) { +fn resolve_run_roots( + metadata: &cargo_metadata::Metadata, +) -> (std::path::PathBuf, std::path::PathBuf) { log::trace!("resolve_run_root"); log::debug!("workspace_root: {:?}", metadata.workspace_root.as_std_path()); // NOTE: Automatically handles `CARGO_TARGET_DIR` env var. diff --git a/anneal/v2/src/setup.rs b/anneal/v2/src/setup.rs index 1c290d169d..2906d102cd 100644 --- a/anneal/v2/src/setup.rs +++ b/anneal/v2/src/setup.rs @@ -84,11 +84,6 @@ impl Toolchain { pub fn command(&self, tool: Tool) -> std::process::Command { std::process::Command::new(tool.path(self)) } - - #[cfg(test)] - pub fn new_test(root: std::path::PathBuf) -> Self { - Self { root } - } } pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> { @@ -108,69 +103,3 @@ pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> { log::info!("anneal toolchain is installed at {:?}", installation_dir); Ok(()) } - -#[cfg(feature = "exocrate_tests")] -pub fn run_test_setup() -> anyhow::Result<()> { - log::debug!("Running standard setup..."); - run_setup(SetupArgs { - local_archive: Some("target/anneal-exocrate.tar.zst".into()), - })?; - - let toolchain = Toolchain::resolve()?; - let dest_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) - .join("tests") - .join("toolchains") - .join("charon-only"); - - if dest_dir.exists() { - log::debug!("Cleaning existing test toolchain at {:?}", dest_dir); - std::fs::remove_dir_all(&dest_dir).context("Failed to clean test toolchain dir")?; - } - std::fs::create_dir_all(&dest_dir)?; - - let copy_file = |src: &std::path::Path, dest: &std::path::Path| -> anyhow::Result<()> { - if let Some(parent) = dest.parent() { - std::fs::create_dir_all(parent)?; - } - std::fs::copy(src, dest)?; - let meta = std::fs::metadata(src)?; - std::fs::set_permissions(dest, meta.permissions())?; - Ok(()) - }; - - log::debug!("Copying Charon binaries..."); - copy_file( - &toolchain.aeneas_bin_dir().join("charon"), - &dest_dir.join("aeneas").join("bin").join("charon"), - )?; - copy_file( - &toolchain.aeneas_bin_dir().join("charon-driver"), - &dest_dir.join("aeneas").join("bin").join("charon-driver"), - )?; - - log::debug!("Copying rustc binary..."); - copy_file( - &toolchain.rust_bin().join("rustc"), - &dest_dir.join("rust").join("bin").join("rustc"), - )?; - - log::debug!("Copying rust libraries (this may take a while)..."); - let src_lib = toolchain.rust_lib(); - let dest_lib = dest_dir.join("rust").join("lib"); - - for entry in walkdir::WalkDir::new(&src_lib) { - let entry = entry?; - let rel_path = entry.path().strip_prefix(&src_lib)?; - let dest_path = dest_lib.join(rel_path); - if entry.file_type().is_dir() { - std::fs::create_dir_all(&dest_path)?; - } else { - copy_file(entry.path(), &dest_path)?; - } - } - - log::debug!("Test toolchain successfully set up at {:?}", dest_dir); - Ok(()) -} - - diff --git a/anneal/v2/src/util.rs b/anneal/v2/src/util.rs index 829a9a7420..22d9c2be88 100644 --- a/anneal/v2/src/util.rs +++ b/anneal/v2/src/util.rs @@ -70,7 +70,10 @@ impl DirLock { /// Walks a directory recursively and replaces string patterns inside `.trace` /// files. This is used to patch non-portable paths generated by Lake. -pub(crate) fn patch_trace_files(dir: &std::path::Path, replacements: &[(&str, &str)]) -> anyhow::Result<()> { +pub(crate) fn patch_trace_files( + dir: &std::path::Path, + replacements: &[(&str, &str)], +) -> anyhow::Result<()> { if dir.exists() { let walker = walkdir::WalkDir::new(dir).into_iter(); for entry in walker { @@ -96,7 +99,7 @@ pub(crate) fn patch_trace_files(dir: &std::path::Path, replacements: &[(&str, &s /// Prepends a path to an existing environment variable, /// separating them with a colon if the variable is not empty. This contains the /// pure string formatting logic. -pub(crate) fn prepend_to_env_var_impl( +fn prepend_to_env_var_impl( current_val: std::ffi::OsString, new_path: &std::path::Path, ) -> std::ffi::OsString { @@ -129,7 +132,7 @@ pub(crate) struct ProcessOutput { /// its stdout line-by-line in the main thread while showing a progress spinner. pub(crate) fn run_command_with_progress( mut cmd: std::process::Command, - progress_msg: Option<&str>, + pb: Option, mut process_stdout_line: F, ) -> anyhow::Result where @@ -153,17 +156,9 @@ where })); } - let pb = progress_msg.map(|msg| { - let pb = indicatif::ProgressBar::new_spinner(); - pb.set_style( - indicatif::ProgressStyle::default_spinner() - .template("{spinner:.green} {msg}") - .unwrap(), - ); - pb.enable_steady_tick(std::time::Duration::from_millis(100)); - pb.set_message(msg.to_string()); - pb - }); + if let Some(ref p) = pb { + p.enable_steady_tick(std::time::Duration::from_millis(100)); + } if let Some(stdout) = child.stdout.take() { let reader = std::io::BufReader::new(stdout); @@ -185,14 +180,68 @@ where let _ = thread.join(); } - let stderr_lines = std::sync::Arc::try_unwrap(stderr_buffer) - .unwrap() - .into_inner() - .unwrap(); + let stderr_lines = std::sync::Arc::try_unwrap(stderr_buffer).unwrap().into_inner().unwrap(); Ok(ProcessOutput { status, stderr_lines }) } +#[cfg(feature = "exocrate_tests")] +pub(crate) fn run_test_lock_helper( + role: &str, + lock_dir: &std::path::Path, + log_file: &std::path::Path, + sig_file: &std::path::Path, +) -> anyhow::Result<()> { + use std::io::Write as _; + + let append_log = |msg: &str| -> anyhow::Result<()> { + let mut file = std::fs::OpenOptions::new().create(true).append(true).open(log_file)?; + writeln!(file, "{}", msg)?; + Ok(()) + }; + + let wait_for_sig = || -> anyhow::Result<()> { + let start = std::time::Instant::now(); + while !sig_file.exists() { + if start.elapsed() > std::time::Duration::from_secs(3) { + anyhow::bail!("Timeout waiting for signal file {:?}", sig_file); + } + std::thread::sleep(std::time::Duration::from_millis(50)); + } + Ok(()) + }; + + match role { + "reader-a" => { + let _lock = DirLock::lock_shared(lock_dir.to_path_buf())?; + append_log("SHARED_START_A")?; + wait_for_sig()?; + append_log("SHARED_END_A")?; + } + "reader-b" => { + let _lock = DirLock::lock_shared(lock_dir.to_path_buf())?; + append_log("SHARED_START_B")?; + std::fs::write(sig_file, "")?; + append_log("SHARED_END_B")?; + } + "writer-a" => { + let _lock = DirLock::lock_exclusive(lock_dir.to_path_buf())?; + append_log("EXCLUSIVE_START_A")?; + wait_for_sig()?; + append_log("EXCLUSIVE_END_A")?; + } + "reader-exclusion" => { + std::fs::write(sig_file, "")?; + let _lock = DirLock::lock_shared(lock_dir.to_path_buf())?; + append_log("SHARED_START_B")?; + append_log("SHARED_END_B")?; + } + _ => anyhow::bail!("Unknown test-lock-helper role: {}", role), + } + + Ok(()) +} + #[cfg(test)] mod tests { use super::*; @@ -226,7 +275,7 @@ mod tests { let thread_a = std::thread::spawn(move || { let _lock = DirLock::lock_exclusive(lock_path_clone).expect("Failed to lock exclusive"); barrier_clone.wait(); // Signal Thread B that A holds the lock. - + // Simulate brief work holding the lock. std::thread::sleep(std::time::Duration::from_millis(100)); lock_released_clone.store(true, std::sync::atomic::Ordering::Relaxed); @@ -236,12 +285,15 @@ mod tests { // Thread B waits for Thread A to acquire the lock, then tries to acquire it itself. let thread_b = std::thread::spawn(move || { barrier.wait(); // Wait for Thread A to acquire lock. - + // Attempt to acquire lock. This should block until Thread A releases it. let _lock = DirLock::lock_exclusive(lock_path).expect("Failed to lock exclusive in B"); - + // Assert that B only successfully locked the directory AFTER A released it. - assert!(lock_released.load(std::sync::atomic::Ordering::Relaxed), "Thread B acquired lock before Thread A released it!"); + assert!( + lock_released.load(std::sync::atomic::Ordering::Relaxed), + "Thread B acquired lock before Thread A released it!" + ); }); thread_a.join().unwrap(); diff --git a/anneal/v2/tests/integration.rs b/anneal/v2/tests/integration.rs index 46eafc9aa7..9ffa413b4a 100644 --- a/anneal/v2/tests/integration.rs +++ b/anneal/v2/tests/integration.rs @@ -1,32 +1,29 @@ -use std::process::Command; use std::fs; +use std::process::Command; +#[cfg(feature = "exocrate_tests")] #[test] fn test_expand_subcommand_simple() { let temp_dir = tempfile::tempdir().unwrap(); let output_dir = temp_dir.path().join("llbc_out"); - + let bin_path = std::env::var("CARGO_BIN_EXE_cargo-anneal") .or_else(|_| std::env::var("CARGO_BIN_EXE_cargo_anneal")) .expect("CARGO_BIN_EXE_* not set"); - + let mut cmd = Command::new(bin_path); - cmd.arg("expand") - .arg("--example") - .arg("simple") - .arg("--output-dir") - .arg(&output_dir); - + cmd.arg("expand").arg("--example").arg("simple").arg("--output-dir").arg(&output_dir); + cmd.arg("--no-progress"); + cmd.env("__ANNEAL_LOCAL_DEV", "1"); - cmd.env("ANNEAL_NO_PROGRESS", "1"); - + let output = cmd.output().expect("failed to execute cargo-anneal"); - + println!("stdout: {}", String::from_utf8_lossy(&output.stdout)); println!("stderr: {}", String::from_utf8_lossy(&output.stderr)); - + assert!(output.status.success(), "cargo-anneal failed"); - + let mut found_llbc = false; if output_dir.exists() { for entry in fs::read_dir(&output_dir).unwrap() { @@ -38,6 +35,6 @@ fn test_expand_subcommand_simple() { } } } - + assert!(found_llbc, "No .llbc file found in output directory {:?}", output_dir); }