diff --git a/anneal/v2/src/charon.rs b/anneal/v2/src/charon.rs index 2b360eebb5..e2c0575487 100644 --- a/anneal/v2/src/charon.rs +++ b/anneal/v2/src/charon.rs @@ -101,58 +101,6 @@ pub fn run_charon( // 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 { - if let crate::parse::ParsedItem::Function(func) = &item.item { - // Check if the function body is an Axiom (unsafe). - if let crate::parse::attr::FunctionBlockInner::Axiom { .. } = func.anneal.inner { - // Mark `unsafe(axiom)` functions as opaque in Charon. This - // instructs Aeneas to treat the function as external and - // generate a template file (`FunsExternal_Template.lean`) - // containing the type signature as an axiom, rather than - // attempting to translate the body. This allows users to - // mechanically verify the composition of safe code while - // manually vouching for the correctness of unsafe leaf - // functions. - let mut opaque_name = item.module_path.join("::"); - opaque_name.push_str("::"); - opaque_name.push_str(func.item.name()); - - log::trace!("Marking item as opaque in Charon: {}", opaque_name); - cmd.args(["--opaque", &opaque_name]); - } - } - } - - // Start translation from specific entry points. Sort to ensure - // deterministic ordering for testing. Determinism is important for - // production too, because the order of arguments can affect the order - // of generated definitions in Lean, which we want to be stable to - // minimize churn. - let mut start_from = artifact.start_from.iter().map(String::as_ref).collect::>(); - start_from.sort_unstable(); // Slightly faster than `sort`, and equivalent for strings. - - if log::log_enabled!(log::Level::Trace) { - for entry in &start_from { - log::trace!("Translation entry point: {}", entry); - } - } - - 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. 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.", - artifact.name.package_name, - start_from_str.len() - ); - } - - cmd.arg("--start-from").arg(start_from_str); - // Separator for the underlying cargo command. cmd.arg("--"); @@ -322,10 +270,9 @@ mod tests { // 5. Resolve roots. let roots = resolve_roots(&args).unwrap(); - // 6. Scan workspace (our simplified scanner will find `add` function). + // 6. Scan workspace. let packages = scan_workspace(&roots).unwrap(); assert_eq!(packages.len(), 1); - assert!(packages[0].start_from.contains("crate::add")); // 7. Lock run root. let locked_roots = roots.lock_run_root().unwrap(); @@ -346,4 +293,174 @@ mod tests { let llbc_path = packages[0].llbc_path(&locked_roots); assert!(llbc_path.exists(), "llbc file not found at {:?}", llbc_path); } + + #[cfg(feature = "exocrate_tests")] + #[test] + fn test_run_charon_multiple_modules() { + let _ = env_logger::builder().is_test(true).try_init(); + + // 1. Create a temporary workspace with multiple modules. + let temp_dir = tempfile::tempdir().unwrap(); + crate::workspace_fixture!(&temp_dir, { + "Cargo.toml" => r#" + [package] + name = "test_proj" + version = "0.1.0" + edition = "2021" + + [lib] + path = "src/lib.rs" + "#, + "src/lib.rs" => r#" + pub mod foo; + pub mod bar; + "#, + "src/foo.rs" => r#" + pub fn foo_fn() {} + "#, + "src/bar.rs" => r#" + pub fn bar_fn() {} + "#, + }); + + // 2. Construct Args pointing to this temp project. + let args = Args::try_parse_from(&[ + "cargo-anneal", + "--manifest-path", + temp_dir.path().join("Cargo.toml").to_str().unwrap(), + ]) + .unwrap(); + + // 3. Resolve roots and scan workspace. + let roots = resolve_roots(&args).unwrap(); + let packages = scan_workspace(&roots).unwrap(); + assert_eq!(packages.len(), 1); + + // 4. Lock run root. + let locked_roots = roots.lock_run_root().unwrap(); + + // 5. Resolve 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, // show_progress + ); + assert!(res.is_ok(), "charon failed: {:?}", res.err()); + + // 6. Verify .llbc file exists and contains BOTH functions. + let llbc_path = packages[0].llbc_path(&locked_roots); + assert!(llbc_path.exists(), "llbc file not found at {:?}", llbc_path); + + log::debug!("llbc path: {:?}", llbc_path); + + let llbc_content = std::fs::read_to_string(&llbc_path).expect("failed to read llbc file"); + + log::debug!("llbc content:\n'''\n{}\n'''", llbc_content); + + // Assert that the serialized AST contains the names of both functions + // defined in separate, independent modules. + assert!(llbc_content.contains("foo_fn"), "Function 'foo_fn' was not translated!"); + assert!(llbc_content.contains("bar_fn"), "Function 'bar_fn' was not translated!"); + } + + #[cfg(feature = "exocrate_tests")] + #[test] + fn test_run_charon_multiple_packages() { + let _ = env_logger::builder().is_test(true).try_init(); + + // 1. Create a temporary workspace containing multiple packages. + let temp_dir = tempfile::tempdir().unwrap(); + crate::workspace_fixture!(&temp_dir, { + "Cargo.toml" => r#" + [workspace] + resolver = "2" + members = [ + "package_a", + "package_b", + ] + "#, + "package_a/Cargo.toml" => r#" + [package] + name = "package_a" + version = "0.1.0" + edition = "2021" + + [lib] + path = "src/lib.rs" + "#, + "package_a/src/lib.rs" => r#" + pub fn func_a() {} + "#, + "package_b/Cargo.toml" => r#" + [package] + name = "package_b" + version = "0.1.0" + edition = "2021" + + [lib] + path = "src/lib.rs" + "#, + "package_b/src/lib.rs" => r#" + pub fn func_b() {} + "#, + }); + + // 2. Construct Args pointing to this temp project. + let args = Args::try_parse_from(&[ + "cargo-anneal", + "--manifest-path", + temp_dir.path().join("Cargo.toml").to_str().unwrap(), + ]) + .unwrap(); + + // 3. Resolve roots and scan workspace. + let roots = resolve_roots(&args).unwrap(); + let packages = scan_workspace(&roots).unwrap(); + assert_eq!(packages.len(), 2, "Expected exactly two packages resolved in workspace"); + + // 4. Lock run root. + let locked_roots = roots.lock_run_root().unwrap(); + + // 5. Resolve toolchain and run charon on both packages. + let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain"); + let res = run_charon( + &args, + &toolchain, + &locked_roots, + &packages, + false, // show_progress + ); + assert!(res.is_ok(), "charon failed: {:?}", res.err()); + + // 6. Verify .llbc file exists and contains correct code for Package A. + let llbc_path_a = packages[0].llbc_path(&locked_roots); + assert!(llbc_path_a.exists(), "llbc file for Package A not found at {:?}", llbc_path_a); + let llbc_content_a = + std::fs::read_to_string(&llbc_path_a).expect("failed to read llbc file A"); + assert!( + llbc_content_a.contains("func_a"), + "Function 'func_a' was not translated in Package A!" + ); + assert!( + !llbc_content_a.contains("func_b"), + "Function 'func_b' was incorrectly translated in Package A!" + ); + + // 7. Verify .llbc file exists and contains correct code for Package B. + let llbc_path_b = packages[1].llbc_path(&locked_roots); + assert!(llbc_path_b.exists(), "llbc file for Package B not found at {:?}", llbc_path_b); + let llbc_content_b = + std::fs::read_to_string(&llbc_path_b).expect("failed to read llbc file B"); + assert!( + llbc_content_b.contains("func_b"), + "Function 'func_b' was not translated in Package B!" + ); + assert!( + !llbc_content_b.contains("func_a"), + "Function 'func_a' was incorrectly translated in Package B!" + ); + } } diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs index 42f8d2735e..b57c109471 100644 --- a/anneal/v2/src/main.rs +++ b/anneal/v2/src/main.rs @@ -12,7 +12,6 @@ use clap::Parser as _; mod charon; mod diagnostics; -mod parse; mod resolve; mod scanner; mod setup; diff --git a/anneal/v2/src/parse.rs b/anneal/v2/src/parse.rs deleted file mode 100644 index 2507fa8e28..0000000000 --- a/anneal/v2/src/parse.rs +++ /dev/null @@ -1,62 +0,0 @@ -// Copyright 2026 The Fuchsia Authors -// -// Licensed under the 2-Clause BSD License , Apache License, Version 2.0 -// , or the MIT -// license , at your option. -// This file may not be copied, modified, or distributed except according to -// those terms. - -pub mod hkd { - pub struct Safe; - pub trait ThreadSafety {} - impl ThreadSafety for Safe {} - pub struct Local; - impl ThreadSafety for Local {} -} - -#[derive(Clone, Debug)] -pub struct AnnealDecorated { - pub item: T, - pub anneal: B, -} - -#[derive(Clone, Debug)] -pub enum FunctionItem { - Free(std::marker::PhantomData), -} - -impl FunctionItem { - pub fn name(&self) -> &str { - "" - } -} - -#[derive(Clone, Debug)] -pub enum FunctionBlockInner { - Axiom { sorry: bool }, - Other, -} - -#[derive(Clone, Debug)] -pub struct FunctionAnnealBlock { - pub inner: FunctionBlockInner, - _phantom: std::marker::PhantomData, -} - -#[derive(Clone, Debug)] -pub enum ParsedItem { - Function(AnnealDecorated, FunctionAnnealBlock>), - Dummy, -} - -#[derive(Debug)] -pub struct ParsedLeanItem { - pub item: ParsedItem, - pub module_path: Vec, - pub source_file: std::path::PathBuf, -} - -pub mod attr { - pub use super::FunctionBlockInner; -} diff --git a/anneal/v2/src/resolve.rs b/anneal/v2/src/resolve.rs index 0fc99abf86..45d0959a21 100644 --- a/anneal/v2/src/resolve.rs +++ b/anneal/v2/src/resolve.rs @@ -141,8 +141,7 @@ pub struct AnnealTargetName { pub struct AnnealTarget { pub name: AnnealTargetName, pub kind: AnnealTargetKind, - /// Path to the main source file for this target. - pub src_path: std::path::PathBuf, + /// Path to the `Cargo.toml` for this target. pub manifest_path: std::path::PathBuf, } @@ -268,7 +267,6 @@ pub fn resolve_roots(args: &Args) -> anyhow::Result { // reference for the rest of the pipeline. This avoids ambiguity // if the CWD changes or if we're working with complex workspace // structures. - src_path: target.src_path.as_std_path().to_owned(), manifest_path: package.manifest_path.as_std_path().to_owned(), })); } diff --git a/anneal/v2/src/scanner.rs b/anneal/v2/src/scanner.rs index 730d9b1e68..1209894e85 100644 --- a/anneal/v2/src/scanner.rs +++ b/anneal/v2/src/scanner.rs @@ -9,19 +9,16 @@ use sha2::Digest as _; +/// Represents a compilation target (artifact) that needs to be processed. +/// +/// In this rewrite, we no longer directly parse Rust files to extract annotations +/// or entry points. Instead, Charon compiles the entire target to generate LLBC +/// files, and annotations will be processed from LLBC directly at a later stage. pub struct AnnealArtifact { pub name: crate::resolve::AnnealTargetName, pub target_kind: crate::resolve::AnnealTargetKind, /// The path to the crate's `Cargo.toml`. pub manifest_path: std::path::PathBuf, - pub items: Vec>, - // NOTE: We store `start_from` as a `HashSet` rather than a `Vec` as an - // optimization: when we encounter items which we can't name (which carry - // Anneal annotations), we add their parent module to the list of - // entrypoints. If there are multiple items in the same module, this can - // lead to duplication in the list of entrypoints. Storing them in a - // `HashSet` avoids us having to de-dup later. - pub start_from: std::collections::HashSet, } impl AnnealArtifact { @@ -107,39 +104,15 @@ impl AnnealArtifact { } } +/// Scans the resolved workspace roots to identify the targets that need to be passed +/// to Charon. No Rust source code parsing is performed during this step. pub fn scan_workspace(roots: &crate::resolve::Roots) -> anyhow::Result> { let mut artifacts = Vec::new(); for target in &roots.roots { - let mut start_from = std::collections::HashSet::new(); - if let Ok(content) = std::fs::read_to_string(&target.src_path) { - for line in content.lines() { - let trimmed = line.trim(); - let mut func_name = None; - if let Some(rest) = trimmed.strip_prefix("fn ") { - func_name = rest.split('(').next(); - } else if let Some(rest) = trimmed.strip_prefix("pub fn ") { - func_name = rest.split('(').next(); - } - if let Some(name) = func_name { - let name = name.trim(); - if !name.is_empty() && name.chars().all(|c| c.is_alphanumeric() || c == '_') { - start_from.insert(format!("crate::{}", name)); - } - } - } - } - - // If we found nothing, but it's a bin, assume `main`. - if start_from.is_empty() && target.kind == crate::resolve::AnnealTargetKind::Bin { - start_from.insert("crate::main".to_string()); - } - artifacts.push(AnnealArtifact { name: target.name.clone(), target_kind: target.kind, manifest_path: target.manifest_path.clone(), - items: vec![], // Empty for now. - start_from, }); } Ok(artifacts) diff --git a/anneal/v2/src/util.rs b/anneal/v2/src/util.rs index fd35f313d2..e3533277f5 100644 --- a/anneal/v2/src/util.rs +++ b/anneal/v2/src/util.rs @@ -128,10 +128,6 @@ pub(crate) fn prepend_to_env_var(var_name: &str, new_path: &std::path::Path) -> 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; - pub(crate) struct ProcessOutput { pub status: std::process::ExitStatus, pub stderr_lines: Vec, @@ -251,6 +247,21 @@ pub(crate) fn run_test_lock_helper( Ok(()) } +#[cfg(test)] +#[macro_export] +macro_rules! workspace_fixture { + ($dir:expr, { $($path:expr => $content:expr),* $(,)? }) => {{ + let root = $dir.path(); + $( + let file_path = root.join($path); + if let Some(parent) = file_path.parent() { + std::fs::create_dir_all(parent).unwrap(); + } + std::fs::write(&file_path, $content).unwrap(); + )* + }}; +} + #[cfg(test)] mod tests { use super::*;