[hermes] Add Charon step

gherrit-pr-id: Ge1bd84b5d857e18e3668e809844c6d73b808a020

Author: joshlf

tools/Cargo.lock

@@ -12,6 +12,7 @@ cargo_metadata = "0.23.1"
 clap = { version = "4.5.57", features = ["derive"] }
 clap-cargo = { version = "0.18.3", features = ["cargo_metadata"] }
 dashmap = "6.1.0"
+env_logger = "0.11.8"
 log = "0.4.29"
 miette = { version = "7.6.0", features = ["derive", "fancy"] }
 proc-macro2 = { version = "1.0.105", features = ["span-locations"] }

tools/hermes/Cargo.toml

@@ -0,0 +1,89 @@
+use std::process::Command;
+
+use anyhow::{bail, Context as _, Result};
+
+use crate::{
+    resolve::{Args, Roots},
+    shadow::HermesTargetPackage,
+};
+
+pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesTargetPackage]) -> Result<()> {
+    let charon_root = roots.charon_root();
+
+    std::fs::create_dir_all(&charon_root).context("Failed to create charon output directory")?;
+
+    for pkg in packages {
+        if pkg.start_from.is_empty() {
+            continue;
+        }
+
+        log::info!("Invoking Charon on package '{}'...", pkg.name);
+
+        let mut cmd = Command::new("charon");
+        cmd.arg("cargo");
+
+        // Output artifacts to target/hermes/<hash>/charon
+        let llbc_path = charon_root.join(pkg.llbc_file_name());
+        log::debug!("Writing .llbc file to {}", llbc_path.display());
+        cmd.arg("--dest-file").arg(llbc_path);
+
+        // Fail fast on errors
+        cmd.arg("--abort-on-error");
+
+        // Start translation from specific entry points
+        cmd.arg("--start-from").arg(pkg.start_from.join(","));
+
+        // Separator for the underlying cargo command
+        cmd.arg("--");
+
+        cmd.arg("--manifest-path").arg(&pkg.shadow_manifest_path);
+
+        // NOTE: We do not forward --workspace, -p, or --exclude, as we are
+        // manually iterating over the selected packages.
+        if args.lib {
+            cmd.arg("--lib");
+        }
+        if args.bins {
+            cmd.arg("--bins");
+        }
+        for bin in &args.bin {
+            cmd.arg("--bin").arg(bin);
+        }
+        if args.examples {
+            cmd.arg("--examples");
+        }
+        for example in &args.example {
+            cmd.arg("--example").arg(example);
+        }
+        if args.tests {
+            cmd.arg("--tests");
+        }
+        for test in &args.test {
+            cmd.arg("--test").arg(test);
+        }
+
+        // Forward all feature-related flags.
+        if args.features.all_features {
+            cmd.arg("--all-features");
+        }
+        if args.features.no_default_features {
+            cmd.arg("--no-default-features");
+        }
+        for feature in &args.features.features {
+            cmd.arg("--features").arg(feature);
+        }
+
+        // Reuse the main target directory for dependencies to save time.
+        cmd.env("CARGO_TARGET_DIR", &roots.cargo_target_dir);
+
+        log::debug!("Command: {:?}", cmd);
+
+        let status = cmd.status().context("Failed to execute charon")?;
+
+        if !status.success() {
+            bail!("Charon failed with status: {}", status);
+        }
+    }
+
+    Ok(())
+}

tools/hermes/src/charon.rs

@@ -1,3 +1,4 @@
+mod charon;
 mod errors;
 mod parse;
 mod resolve;
@@ -22,6 +23,8 @@ enum Commands {
 }
 
 fn main() -> anyhow::Result<()> {
+    env_logger::init();
+
     if std::env::var("HERMES_UI_TEST_MODE").is_ok() {
         ui_test_shim::run();
         return Ok(());
@@ -31,7 +34,17 @@ fn main() -> anyhow::Result<()> {
     match args.command {
         Commands::Verify(resolve_args) => {
             let roots = resolve::resolve_roots(&resolve_args)?;
-            shadow::build_shadow_crate(&roots)
+            let entry_points = shadow::build_shadow_crate(&roots)?;
+            if entry_points.is_empty() {
+                anyhow::bail!("No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.");
+            }
+            charon::run_charon(&resolve_args, &roots, &entry_points)
         }
     }
 }
+
+/// A no-op function with a Hermes annotation so we can test Hermes on itself.
+///
+/// ```lean
+/// ```
+fn _foo() {}

tools/hermes/src/main.rs

@@ -45,6 +45,17 @@ pub enum ParsedItem {
 }
 
 impl ParsedItem {
+    pub fn name(&self) -> Option<String> {
+        match self {
+            Self::Fn(item) => Some(item.sig.ident.to_string()),
+            Self::Struct(item) => Some(item.ident.to_string()),
+            Self::Enum(item) => Some(item.ident.to_string()),
+            Self::Union(item) => Some(item.ident.to_string()),
+            Self::Trait(item) => Some(item.ident.to_string()),
+            Self::Impl(_) => None,
+        }
+    }
+
     /// Returns the attributes on this item.
     fn attrs(&self) -> &[Attribute] {
         match self {
@@ -62,7 +73,7 @@ impl ParsedItem {
 #[derive(Debug)]
 pub struct ParsedLeanItem {
     pub item: ParsedItem,
-    module_path: Vec<String>,
+    pub module_path: Vec<String>,
     lean_block: String,
     source_file: Option<PathBuf>,
 }

tools/hermes/src/parse.rs

@@ -11,41 +11,41 @@ use clap::Parser;
 #[derive(Parser, Debug)]
 pub struct Args {
     #[command(flatten)]
-    manifest: clap_cargo::Manifest,
+    pub manifest: clap_cargo::Manifest,
 
     #[command(flatten)]
-    workspace: clap_cargo::Workspace,
+    pub workspace: clap_cargo::Workspace,
 
     #[command(flatten)]
-    features: clap_cargo::Features,
+    pub features: clap_cargo::Features,
 
     /// Verify the library target
     #[arg(long)]
-    lib: bool,
+    pub lib: bool,
 
     /// Verify specific binary targets
     #[arg(long)]
-    bin: Vec<String>,
+    pub bin: Vec<String>,
 
     /// Verify all binary targets
     #[arg(long)]
-    bins: bool,
+    pub bins: bool,
 
     /// Verify specific example targets
     #[arg(long)]
-    example: Vec<String>,
+    pub example: Vec<String>,
 
     /// Verify all example targets
     #[arg(long)]
-    examples: bool,
+    pub examples: bool,
 
     /// Verify specific test targets
     #[arg(long)]
-    test: Vec<String>,
+    pub test: Vec<String>,
 
     /// Verify all test targets
     #[arg(long)]
-    tests: bool,
+    pub tests: bool,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
@@ -111,6 +111,10 @@ impl Roots {
     pub fn shadow_root(&self) -> PathBuf {
         self.hermes_run_root.join("shadow")
     }
+
+    pub fn charon_root(&self) -> PathBuf {
+        self.hermes_run_root.join("charon")
+    }
 }
 
 /// Resolves all verification roots.