SQUASH ME: More fix-ups on things the agent got wrong, and some initial lock tests

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"); }
+
     }
 }

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());
     }
 }

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,19 +66,19 @@ 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 {
         self.root.join(RUST_SYSROOT)
     }
 
     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());
-    }
-}
+

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);
     }
 }