Skip to content

Commit 964666d

Browse files
committed
[anneal][v2] Add charon execution engine, expand command CLI, and integration tests
gherrit-pr-id: Gnafivbpqcaatsvsxamgsjcudchscvaae
1 parent 10684db commit 964666d

10 files changed

Lines changed: 1065 additions & 31 deletions

File tree

anneal/v2/examples/simple.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
pub fn add(left: usize, right: usize) -> usize {
2+
left + right
3+
}
4+
5+
fn main() {
6+
println!("Hello, world! {}", add(1, 2));
7+
}

anneal/v2/src/charon.rs

Lines changed: 659 additions & 0 deletions
Large diffs are not rendered by default.

anneal/v2/src/diagnostics.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,7 @@ impl DiagnosticMapper {
242242
/// bytes.
243243
/// 3. Anneal calls this method to print the error onto the Rust file
244244
/// canvas.
245+
#[allow(dead_code)]
245246
pub fn render_raw<F>(
246247
&mut self,
247248
file_name: &str,

anneal/v2/src/main.rs

Lines changed: 103 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,16 @@
77
// This file may not be copied, modified, or distributed except according to
88
// those terms.
99

10+
use anyhow::Context as _;
1011
use clap::Parser as _;
1112

13+
mod charon;
14+
mod diagnostics;
15+
mod resolve;
16+
mod scanner;
17+
mod setup;
18+
mod util;
19+
1220
/// Anneal
1321
#[derive(clap::Parser, Debug)]
1422
#[command(name = "cargo-anneal", version, about, long_about = None)]
@@ -21,50 +29,77 @@ struct Cli {
2129
enum Commands {
2230
/// Setup Anneal dependencies
2331
Setup(SetupArgs),
32+
/// Expand a crate (runs Charon)
33+
Expand(ExpandArgs),
34+
35+
/// Helper to acquire shared or exclusive locks for multi-process integration testing (dev only)
36+
#[cfg(feature = "exocrate_tests")]
37+
TestLockHelper {
38+
/// The role to run as: 'reader-a', 'reader-b', 'writer-a', or 'reader-exclusion'
39+
#[arg(long)]
40+
role: String,
41+
/// Path to the directory to lock
42+
#[arg(long)]
43+
lock_dir: std::path::PathBuf,
44+
/// Path to the shared log file where lock transitions are appended
45+
#[arg(long)]
46+
log_file: std::path::PathBuf,
47+
/// Path to the temporary synchronization signal file
48+
#[arg(long)]
49+
sig_file: std::path::PathBuf,
50+
},
2451
}
2552

2653
#[derive(clap::Parser, Debug)]
2754
pub struct SetupArgs {
28-
/// Path to a local dependency archive to use instead of downloading.
55+
/// Path to a local dependency archive to use instead of downloading
2956
#[arg(long, value_name = "path-to-local-archive")]
3057
pub local_archive: Option<std::path::PathBuf>,
3158
}
3259

33-
exocrate::config! {
34-
const CONFIG: Config = Config {
35-
rel_dir_path: [".anneal", "toolchain"],
36-
versioned_files: &["../Cargo.toml", "../Cargo.lock"],
37-
};
60+
#[derive(clap::Parser, Debug)]
61+
pub struct ExpandArgs {
62+
#[command(flatten)]
63+
pub resolve_args: crate::resolve::Args,
64+
65+
/// Controls where LLBC output is placed on the filesystem
66+
#[arg(long, value_name = "output-dir")]
67+
pub output_dir: Option<std::path::PathBuf>,
68+
69+
/// Do not show compilation progress bars
70+
#[arg(long)]
71+
pub no_progress: bool,
3872
}
3973

40-
exocrate::parse_remote_archive! {
41-
const REMOTE: RemoteArchive = "Cargo.toml" [
42-
(linux, x86_64),
43-
(macos, x86_64),
44-
(linux, aarch64),
45-
(macos, aarch64),
46-
];
74+
fn setup(args: SetupArgs) -> anyhow::Result<()> {
75+
crate::setup::run_setup(crate::setup::SetupArgs { local_archive: args.local_archive })
76+
.context("Failed to setup toolchain")
4777
}
4878

49-
fn setup(args: SetupArgs) {
50-
let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
51-
exocrate::Location::LocalDev
52-
} else {
53-
exocrate::Location::UserGlobal
54-
};
55-
let source = match args.local_archive {
56-
Some(local_archive) => exocrate::Source::Local(local_archive),
57-
None => exocrate::Source::Remote(REMOTE),
58-
};
59-
60-
let installation_dir = CONFIG
61-
.resolve_installation_dir_or_install(location, source)
62-
// FIXME: Implement unified error reporting (e.g., via `anyhow`).
63-
.expect("failed to resolve-or-install dependencies");
64-
log::info!("anneal toolchain is installed at {:?}", installation_dir);
79+
fn expand(args: ExpandArgs) -> anyhow::Result<()> {
80+
let roots = crate::resolve::resolve_roots(&args.resolve_args)?;
81+
let packages = crate::scanner::scan_workspace(&roots)?;
82+
if packages.is_empty() {
83+
log::warn!("No targets found to expand.");
84+
return Ok(());
85+
}
86+
let mut locked_roots = roots.lock_run_root()?;
87+
if let Some(output_dir) = args.output_dir {
88+
locked_roots.llbc_override = Some(output_dir);
89+
}
90+
let toolchain = crate::setup::Toolchain::resolve()?;
91+
let show_progress = !args.no_progress;
92+
crate::charon::run_charon(
93+
&args.resolve_args,
94+
&toolchain,
95+
&locked_roots,
96+
&packages,
97+
show_progress,
98+
)?;
99+
Ok(())
65100
}
66101

67-
fn main() {
102+
fn main() -> anyhow::Result<()> {
68103
// Suppressing timestamps removes a source of nondeterminism that is
69104
// difficult to work around in integration tests.
70105
env_logger::builder().format_timestamp(None).init();
@@ -79,18 +114,55 @@ fn main() {
79114

80115
match args.command {
81116
Commands::Setup(args) => setup(args),
117+
Commands::Expand(args) => expand(args),
118+
119+
#[cfg(feature = "exocrate_tests")]
120+
Commands::TestLockHelper { role, lock_dir, log_file, sig_file } => {
121+
crate::util::run_test_lock_helper(&role, &lock_dir, &log_file, &sig_file)
122+
}
82123
}
83124
}
84125

85126
#[cfg(test)]
86127
mod tests {
87128
#[cfg(feature = "exocrate_tests")]
88129
#[test]
89-
fn test_setup() {
130+
fn test_setup_and_toolchain_paths() {
131+
// 1. Run setup.
90132
super::setup(super::SetupArgs {
91133
// ASSUMPTION: Dependency builder installs archive at
92134
// `target/anneal-exocrate.tar.zst`.
93135
local_archive: Some("target/anneal-exocrate.tar.zst".into()),
94136
})
137+
.expect("Failed to run setup");
138+
139+
// 2. Once setup completes successfully, resolve the toolchain.
140+
let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
141+
142+
// 3. Verify that all returned paths exist as directories.
143+
// Note: these assertions would be more appropriate in the setup.rs module,
144+
// but including them here avoids introducing multiple tests that attempt to
145+
// extract the (large) anneal exocrate archive.
146+
assert!(toolchain.root().is_dir(), "root is not a directory: {:?}", toolchain.root());
147+
assert!(
148+
toolchain.aeneas_bin_dir().is_dir(),
149+
"aeneas_bin_dir is not a directory: {:?}",
150+
toolchain.aeneas_bin_dir()
151+
);
152+
assert!(
153+
toolchain.rust_sysroot().is_dir(),
154+
"rust_sysroot is not a directory: {:?}",
155+
toolchain.rust_sysroot()
156+
);
157+
assert!(
158+
toolchain.rust_bin().is_dir(),
159+
"rust_bin is not a directory: {:?}",
160+
toolchain.rust_bin()
161+
);
162+
assert!(
163+
toolchain.rust_lib().is_dir(),
164+
"rust_lib is not a directory: {:?}",
165+
toolchain.rust_lib()
166+
);
95167
}
96168
}

anneal/v2/src/resolve.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -187,10 +187,12 @@ impl<'a> LockedRoots<'a> {
187187
}
188188
}
189189

190+
#[allow(dead_code)]
190191
pub fn lean_root(&self) -> std::path::PathBuf {
191192
self.anneal_run_root.path.join("lean")
192193
}
193194

195+
#[allow(dead_code)]
194196
pub fn lean_generated_root(&self) -> std::path::PathBuf {
195197
self.lean_root().join("generated")
196198
}

anneal/v2/src/scanner.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,7 @@ impl AnnealArtifact {
9191
}
9292

9393
/// Returns the name of the `.lean` spec file to use for this artifact.
94+
#[allow(dead_code)]
9495
pub fn lean_spec_file_name(&self) -> String {
9596
format!("{}.lean", self.artifact_slug())
9697
}

anneal/v2/src/setup.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,7 @@ impl Toolchain {
7070
Ok(Self { root })
7171
}
7272

73+
#[allow(dead_code)]
7374
pub fn root(&self) -> &std::path::Path {
7475
&self.root
7576
}

anneal/v2/src/util.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ impl DirLock {
4141
///
4242
/// Multiple processes can hold shared locks simultaneously, but an
4343
/// exclusive lock will block until all shared locks are released.
44+
#[allow(dead_code)]
4445
pub(crate) fn lock_shared(path: std::path::PathBuf) -> anyhow::Result<Self> {
4546
let file = Self::open_lock_file(&path)?;
4647
file.lock_shared()
@@ -79,6 +80,7 @@ impl DirLock {
7980

8081
/// Walks a directory recursively and replaces string patterns inside `.trace`
8182
/// files. This is used to patch non-portable paths generated by Lake.
83+
#[allow(dead_code)]
8284
pub(crate) fn patch_trace_files(
8385
dir: &std::path::Path,
8486
replacements: &[(&str, &str)],

anneal/v2/tests/integration.rs

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
// Copyright 2026 The Fuchsia Authors
2+
//
3+
// Licensed under the 2-Clause BSD License <LICENSE-BSD or
4+
// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
5+
// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
6+
// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
7+
// This file may not be copied, modified, or distributed except according to
8+
// those terms.
9+
10+
use std::fs;
11+
use std::path::{Path, PathBuf};
12+
use std::process::Command;
13+
use std::sync::OnceLock;
14+
15+
#[cfg(feature = "exocrate_tests")]
16+
fn cargo_anneal_bin_path() -> PathBuf {
17+
std::env::var("CARGO_BIN_EXE_cargo-anneal")
18+
.or_else(|_| std::env::var("CARGO_BIN_EXE_cargo_anneal"))
19+
.expect("CARGO_BIN_EXE_* not set")
20+
.into()
21+
}
22+
23+
#[cfg(feature = "exocrate_tests")]
24+
fn ensure_test_toolchain(bin_path: &Path) {
25+
static SETUP_RESULT: OnceLock<Result<(), String>> = OnceLock::new();
26+
27+
let result = SETUP_RESULT.get_or_init(|| {
28+
let manifest_dir = Path::new(env!("CARGO_MANIFEST_DIR"));
29+
let output = Command::new(bin_path)
30+
.arg("setup")
31+
.arg("--local-archive")
32+
.arg(manifest_dir.join("target/anneal-exocrate.tar.zst"))
33+
.env("__ANNEAL_LOCAL_DEV", "1")
34+
.env("CARGO_MANIFEST_DIR", manifest_dir)
35+
.output()
36+
.map_err(|err| format!("failed to execute cargo-anneal setup: {err}"))?;
37+
38+
if output.status.success() {
39+
return Ok(());
40+
}
41+
42+
Err(format!(
43+
"cargo-anneal setup failed\nstdout: {}\nstderr: {}",
44+
String::from_utf8_lossy(&output.stdout),
45+
String::from_utf8_lossy(&output.stderr)
46+
))
47+
});
48+
49+
if let Err(err) = result {
50+
panic!("{err}");
51+
}
52+
}
53+
54+
#[cfg(feature = "exocrate_tests")]
55+
#[test]
56+
fn test_expand_subcommand_simple() {
57+
let temp_dir = tempfile::tempdir().unwrap();
58+
let project_dir = temp_dir.path().join("project");
59+
let output_dir = temp_dir.path().join("llbc_out");
60+
fs::create_dir_all(project_dir.join("examples")).unwrap();
61+
fs::write(
62+
project_dir.join("Cargo.toml"),
63+
r#"
64+
[package]
65+
name = "test_proj"
66+
version = "0.1.0"
67+
edition = "2021"
68+
69+
[[example]]
70+
name = "simple"
71+
path = "examples/simple.rs"
72+
"#,
73+
)
74+
.unwrap();
75+
fs::write(
76+
project_dir.join("examples").join("simple.rs"),
77+
r#"
78+
pub fn add(left: usize, right: usize) -> usize {
79+
left + right
80+
}
81+
82+
fn main() {
83+
println!("Hello, world! {}", add(1, 2));
84+
}
85+
"#,
86+
)
87+
.unwrap();
88+
89+
let bin_path = cargo_anneal_bin_path();
90+
ensure_test_toolchain(&bin_path);
91+
92+
let mut cmd = Command::new(bin_path);
93+
cmd.arg("expand")
94+
.arg("--manifest-path")
95+
.arg(project_dir.join("Cargo.toml"))
96+
.arg("--example")
97+
.arg("simple")
98+
.arg("--output-dir")
99+
.arg(&output_dir);
100+
cmd.arg("--no-progress");
101+
102+
cmd.env("__ANNEAL_LOCAL_DEV", "1");
103+
cmd.env("CARGO_MANIFEST_DIR", env!("CARGO_MANIFEST_DIR"));
104+
105+
let output = cmd.output().expect("failed to execute cargo-anneal");
106+
107+
println!("stdout: {}", String::from_utf8_lossy(&output.stdout));
108+
println!("stderr: {}", String::from_utf8_lossy(&output.stderr));
109+
110+
assert!(output.status.success(), "cargo-anneal failed");
111+
112+
let mut found_llbc = false;
113+
if output_dir.exists() {
114+
for entry in fs::read_dir(&output_dir).unwrap() {
115+
let entry = entry.unwrap();
116+
let path = entry.path();
117+
if path.is_file() && path.extension().map_or(false, |ext| ext == "llbc") {
118+
found_llbc = true;
119+
break;
120+
}
121+
}
122+
}
123+
124+
assert!(found_llbc, "No .llbc file found in output directory {:?}", output_dir);
125+
}

0 commit comments

Comments
 (0)