From 722d82fc782f492fae901812589761e691834f9a Mon Sep 17 00:00:00 2001 From: Mark Dittmer Date: Thu, 21 May 2026 18:38:22 +0000 Subject: [PATCH] SQUASH ME: More fix-ups on things the agent got wrong, and some initial lock tests gherrit-pr-id: Gmgbefq4ee32sehnr4tj4q7b7okgf4rtl --- anneal/v2/src/charon.rs | 18 +++++---- anneal/v2/src/main.rs | 19 ++++++++-- anneal/v2/src/setup.rs | 31 ++++----------- anneal/v2/src/util.rs | 84 ++++++++++++++++++++++++++++++++++------- 4 files changed, 104 insertions(+), 48 deletions(-) diff --git a/anneal/v2/src/charon.rs b/anneal/v2/src/charon.rs index ddcb7e3c0a..5bde6d6a76 100644 --- a/anneal/v2/src/charon.rs +++ b/anneal/v2/src/charon.rs @@ -31,6 +31,7 @@ pub fn run_charon( toolchain: &crate::setup::Toolchain, roots: &crate::resolve::LockedRoots, packages: &[crate::scanner::AnnealArtifact], + show_progress: bool, ) -> anyhow::Result<()> { let llbc_root = roots.llbc_root(); std::fs::create_dir_all(&llbc_root).context("Failed to create LLBC output directory")?; @@ -50,7 +51,7 @@ pub fn run_charon( 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; + let show_progress = show_progress && packages.len() == 1; packages.par_iter().try_for_each(|artifact| { if artifact.start_from.is_empty() { @@ -75,7 +76,9 @@ pub fn run_charon( let llbc_path = artifact.llbc_path(roots); cmd.arg("--dest-file").arg(llbc_path); - // Fail fast on errors. + // Fail fast on errors: 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. cmd.arg("--abort-on-error"); for item in &artifact.items { @@ -117,7 +120,9 @@ pub fn run_charon( let start_from_str = start_from.join(","); if start_from_str.len() > crate::util::ARG_CHAR_LIMIT { // FIXME: Pass the list of entry points to Charon via a file instead - // of the command line. + // of the command line. This is currently blocked on upstream Charon + // supporting response files or file-based entry points: + // https://github.com/AeneasVerif/charon/issues/1020 anyhow::bail!( "The list of Anneal entry points for package '{}' is too large ({} bytes). \n\ This exceeds safe OS command-line limits.", @@ -259,8 +264,7 @@ mod tests { #[test] fn test_run_charon_simple() { - // Disable progress bar for test. - unsafe { std::env::set_var("ANNEAL_NO_PROGRESS", "1"); } + // The test environment disables progress bar via configuration injection. // 1. Create a temporary directory. let temp_dir = tempfile::tempdir().unwrap(); @@ -313,13 +317,13 @@ mod tests { .join("charon-only"); let toolchain = crate::setup::Toolchain::new_test(toolchain_root); - let res = run_charon(&args, &toolchain, &locked_roots, &packages); + let res = run_charon(&args, &toolchain, &locked_roots, &packages, false); 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); - unsafe { std::env::remove_var("ANNEAL_NO_PROGRESS"); } + } } diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs index b4ab5a6ca6..08af491a6b 100644 --- a/anneal/v2/src/main.rs +++ b/anneal/v2/src/main.rs @@ -75,7 +75,8 @@ fn expand(args: ExpandArgs) -> anyhow::Result<()> { locked_roots.llbc_override = Some(output_dir); } let toolchain = crate::setup::Toolchain::resolve()?; - crate::charon::run_charon(&args.resolve_args, &toolchain, &locked_roots, &packages)?; + let show_progress = std::env::var("ANNEAL_NO_PROGRESS").is_err(); + crate::charon::run_charon(&args.resolve_args, &toolchain, &locked_roots, &packages, show_progress)?; Ok(()) } @@ -114,13 +115,23 @@ fn main() { mod tests { #[cfg(feature = "exocrate_tests")] #[test] - fn test_setup() { - unsafe { std::env::set_var("__ANNEAL_LOCAL_DEV", "1"); } + 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!). super::setup(super::SetupArgs { // ASSUMPTION: Dependency builder installs archive at // `target/anneal-exocrate.tar.zst`. local_archive: Some("target/anneal-exocrate.tar.zst".into()), }); - unsafe { std::env::remove_var("__ANNEAL_LOCAL_DEV"); } + + // 2. Once setup completes successfully, resolve the toolchain. + let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain"); + + // 3. Verify that all returned paths exist as directories. + 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()); } } diff --git a/anneal/v2/src/setup.rs b/anneal/v2/src/setup.rs index d3800ae4f0..1c290d169d 100644 --- a/anneal/v2/src/setup.rs +++ b/anneal/v2/src/setup.rs @@ -40,8 +40,9 @@ impl Tool { const AENEAS_DIR: &str = "aeneas"; const RUST_SYSROOT: &str = "rust"; -const BIN_DIR: &str = "bin"; -const LIB_DIR: &str = "lib"; +const AENEAS_BIN_DIR: &str = "bin"; +const RUST_BIN_DIR: &str = "bin"; +const RUST_LIB_DIR: &str = "lib"; pub struct Toolchain { root: std::path::PathBuf, @@ -65,7 +66,7 @@ impl Toolchain { } pub fn aeneas_bin_dir(&self) -> std::path::PathBuf { - self.root.join(AENEAS_DIR).join(BIN_DIR) + self.root.join(AENEAS_DIR).join(AENEAS_BIN_DIR) } pub fn rust_sysroot(&self) -> std::path::PathBuf { @@ -73,11 +74,11 @@ impl Toolchain { } pub fn rust_bin(&self) -> std::path::PathBuf { - self.rust_sysroot().join(BIN_DIR) + self.rust_sysroot().join(RUST_BIN_DIR) } pub fn rust_lib(&self) -> std::path::PathBuf { - self.rust_sysroot().join(LIB_DIR) + self.rust_sysroot().join(RUST_LIB_DIR) } pub fn command(&self, tool: Tool) -> std::process::Command { @@ -172,22 +173,4 @@ pub fn run_test_setup() -> anyhow::Result<()> { Ok(()) } -#[cfg(test)] -mod tests { - use super::*; - - #[cfg(feature = "exocrate_tests")] - #[test] - fn test_toolchain_paths() { - // Ensure toolchain is installed locally for test. - unsafe { std::env::set_var("__ANNEAL_LOCAL_DEV", "1"); } - - let toolchain = Toolchain::resolve().expect("Failed to resolve toolchain"); - - 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()); - } -} + diff --git a/anneal/v2/src/util.rs b/anneal/v2/src/util.rs index ceda2961dd..829a9a7420 100644 --- a/anneal/v2/src/util.rs +++ b/anneal/v2/src/util.rs @@ -94,10 +94,12 @@ 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 is used -/// to inject our managed Rust toolchain paths before the system paths. -pub(crate) fn prepend_to_env_var(var_name: &str, new_path: &std::path::Path) -> std::ffi::OsString { - let current_val = std::env::var_os(var_name).unwrap_or_default(); +/// 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( + current_val: std::ffi::OsString, + new_path: &std::path::Path, +) -> std::ffi::OsString { let mut combined = new_path.to_path_buf().into_os_string(); if !current_val.is_empty() { combined.push(":"); @@ -106,6 +108,14 @@ pub(crate) fn prepend_to_env_var(var_name: &str, new_path: &std::path::Path) -> combined } +/// Prepends a path to an existing environment variable in the active process +/// environment, separating them with a colon if the variable is not empty. +/// This is used to inject our managed Rust toolchain paths before the system paths. +pub(crate) fn prepend_to_env_var(var_name: &str, new_path: &std::path::Path) -> std::ffi::OsString { + let current_val = std::env::var_os(var_name).unwrap_or_default(); + prepend_to_env_var_impl(current_val, new_path) +} + /// OS command-line length limits (Windows is ~32k; Linux `ARG_MAX` is /// usually larger, but variable). pub(crate) const ARG_CHAR_LIMIT: usize = 32_768; @@ -189,20 +199,68 @@ mod tests { #[test] fn test_prepend_to_env_var() { - let var_name = "ANNEAL_TEST_VAR"; - unsafe { std::env::remove_var(var_name); } - - // Test when var is empty. + // Test when current value is empty. let path1 = std::path::Path::new("/path/one"); - let res1 = prepend_to_env_var(var_name, path1); + let res1 = prepend_to_env_var_impl(std::ffi::OsString::new(), path1); assert_eq!(res1, "/path/one"); - // Test when var is not empty. - unsafe { std::env::set_var(var_name, &res1); } + // Test when current value is not empty. let path2 = std::path::Path::new("/path/two"); - let res2 = prepend_to_env_var(var_name, path2); + let res2 = prepend_to_env_var_impl(res1, path2); assert_eq!(res2, "/path/two:/path/one"); + } + + #[test] + fn test_dir_lock_exclusive_mutual_exclusion() { + let temp_dir = tempfile::tempdir().unwrap(); + let lock_path = temp_dir.path().to_path_buf(); + + let barrier = std::sync::Arc::new(std::sync::Barrier::new(2)); + let barrier_clone = std::sync::Arc::clone(&barrier); + let lock_path_clone = lock_path.clone(); + + let lock_released = std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false)); + let lock_released_clone = std::sync::Arc::clone(&lock_released); + + // Thread A acquires the lock. + 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); + // _lock drops here, releasing the lock. + }); + + // 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!"); + }); + + thread_a.join().unwrap(); + thread_b.join().unwrap(); + } + + #[test] + fn test_dir_lock_shared_coexistence() { + let temp_dir = tempfile::tempdir().unwrap(); + let lock_path = temp_dir.path().to_path_buf(); + + // Thread A acquires shared lock. + let lock_a = DirLock::lock_shared(lock_path.clone()).expect("Failed to lock shared"); + + // Thread B should be able to acquire shared lock immediately without blocking. + let lock_b = DirLock::lock_shared(lock_path).expect("Failed to lock shared concurrently"); - unsafe { std::env::remove_var(var_name); } + // Both locks are held. + drop(lock_a); + drop(lock_b); } }