Skip to content

Commit 991f380

Browse files
mdittmerjoshlf
authored andcommitted
[anneal][v2] Add charon execution engine, expand command CLI, and integration tests
gherrit-pr-id: Gnafivbpqcaatsvsxamgsjcudchscvaae
1 parent 3b23aff commit 991f380

10 files changed

Lines changed: 1073 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: 665 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
@@ -42,6 +42,7 @@ impl DirLock {
4242
///
4343
/// Multiple processes can hold shared locks simultaneously, but an
4444
/// exclusive lock will block until all shared locks are released.
45+
#[allow(dead_code)]
4546
pub(crate) fn lock_shared(path: std::path::PathBuf) -> anyhow::Result<Self> {
4647
let file = Self::open_lock_file(&path)?;
4748
file.lock_shared()
@@ -80,6 +81,7 @@ impl DirLock {
8081

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

anneal/v2/tests/integration.rs

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

0 commit comments

Comments
 (0)