[hermes] Clean up after removing shadow crate support

tools/hermes/src/resolve.rs

@@ -110,6 +110,8 @@ pub struct HermesTarget {
     pub kind: HermesTargetKind,
     /// Path to the main source file for this target.
     pub src_path: PathBuf,
+    /// Path to the `Cargo.toml` for this target.
+    pub manifest_path: PathBuf,
 }
 
 #[derive(Debug)]
@@ -172,6 +174,7 @@ pub fn resolve_roots(args: &Args) -> Result<Roots> {
                 },
                 kind,
                 src_path: target.src_path.as_std_path().to_owned(),
+                manifest_path: package.manifest_path.as_std_path().to_owned(),
             });
         }
     }
@@ -187,15 +190,15 @@ fn resolve_run_root(metadata: &Metadata) -> PathBuf {
     let hermes_global = target_dir.join("hermes");
 
     // Used by integration tests to ensure deterministic shadow dir names.
-    if let Ok(name) = std::env::var("HERMES_TEST_SHADOW_NAME") {
+    if let Ok(name) = std::env::var("HERMES_TEST_DIR_NAME") {
         return hermes_global.join(name);
     }
 
     // Hash the path to the workspace root to avoid collisions between different
     // workspaces using the same target directory.
     let workspace_root_hash = {
         let mut hasher = std::hash::DefaultHasher::new();
-        hasher.write(b"hermes_shadow_salt");
+        hasher.write(b"hermes_build_salt");
         metadata.workspace_root.hash(&mut hasher);
         hasher.finish()
     };
@@ -331,7 +334,7 @@ fn resolve_targets<'a>(
 }
 
 // TODO: Eventually, we'll want to support external path dependencies by
-// rewriting the path in the `Cargo.toml` in the shadow copy.
+// analyzing them in-place or ensuring they are accessible to Charon.
 
 /// Scans the package graph to ensure all local dependencies are contained
 /// within the workspace root. Returns an error if an external path dependency

tools/hermes/src/scanner.rs

@@ -5,7 +5,7 @@ use std::{
     sync::mpsc::{self, Sender},
 };
 
-use anyhow::{Context, Result};
+use anyhow::Result;
 use dashmap::DashSet;
 
 use crate::{
@@ -43,8 +43,8 @@ impl HermesArtifact {
     }
 }
 
-/// 1. Scans and rules all reachable source files, printing any errors
-///    encountered. Collects all items with Hermes annotations.
+/// Scans the workspace to identify Hermes entry points (`/// ```lean` blocks)
+/// and collects targets for verification.
 pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
     log::trace!("scan_workspace({:?})", roots);
 
@@ -117,7 +117,7 @@ pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
         .roots
         .iter()
         .filter_map(|target| {
-            let manifest_path = find_package_root(&target.src_path).ok()?.join("Cargo.toml");
+            let manifest_path = target.manifest_path.clone();
             let start_from = entry_points.remove(&target.name)?;
 
             Some(HermesArtifact {
@@ -130,20 +130,6 @@ pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
         .collect())
 }
 
-/// Walks up the directory tree from the source file to find the directory
-/// containing Cargo.toml.
-fn find_package_root(src_path: &Path) -> Result<PathBuf> {
-    let mut current = src_path;
-    while let Some(parent) = current.parent() {
-        if parent.join("Cargo.toml").exists() {
-            return Ok(parent.to_path_buf());
-        }
-        current = parent;
-    }
-    // This is highly unlikely if the path came from cargo metadata.
-    anyhow::bail!("Could not find Cargo.toml in any parent of {:?}", src_path)
-}
-
 fn process_file_recursive<'a>(
     scope: &rayon::Scope<'a>,
     src_path: &Path,
@@ -160,78 +146,61 @@ fn process_file_recursive<'a>(
     }
 
     // Walking the AST is enough to collect new modules.
-    let result = (|| -> Result<Vec<(PathBuf, String)>> {
-        // Walk the AST, collecting new modules to process.
-        let (_source_code, unloaded_modules) =
-            parse::read_file_and_scan_compilation_unit(src_path, |_src, item_result| {
-                match item_result {
-                    Ok(parsed_item) => {
-                        if let Some(item_name) = parsed_item.item.name() {
-                            // Calculate the full path to this item.
-                            let mut full_path = module_prefix.clone();
-                            full_path.extend(parsed_item.module_path);
-                            full_path.push(item_name);
-
-                            let _ = path_tx.send((name.clone(), full_path.join("::")));
-                        }
-                    }
-                    Err(e) => {
-                        // A parsing error means we either:
-                        // 1. Lost the module graph, causing missing files later.
-                        // 2. Lost a specification, causing unsound verification.
-                        // We must abort the build.
-                        let _ = err_tx.send(anyhow::anyhow!(e));
+    // Walk the AST, collecting new modules to process.
+    let (_source_code, unloaded_modules) =
+        match parse::read_file_and_scan_compilation_unit(src_path, |_src, item_result| {
+            match item_result {
+                Ok(parsed_item) => {
+                    if let Some(item_name) = parsed_item.item.name() {
+                        // Calculate the full path to this item.
+                        let mut full_path = module_prefix.clone();
+                        full_path.extend(parsed_item.module_path);
+                        full_path.push(item_name);
+
+                        let _ = path_tx.send((name.clone(), full_path.join("::")));
                     }
                 }
-            })
-            .context(format!("Failed to parse {:?}", src_path))?;
-
-        // Resolve and queue child modules for processing.
-        let base_dir = src_path.parent().unwrap();
-        let mut next_paths = Vec::new();
-        for module in unloaded_modules {
-            if let Some(mod_path) =
-                resolve_module_path(base_dir, &module.name, module.path_attr.as_deref())
-            {
-                next_paths.push((mod_path, module.name));
-            } else {
-                // This is an expected condition – it shows up when modules are
-                // conditionally compiled. Instead of implementing conditional
-                // compilation ourselves, we can just let rustc error later if
-                // this is actually an error.
-                log::debug!("Could not resolve module '{}' in {:?}", module.name, src_path);
+                Err(e) => {
+                    // A parsing error means we either:
+                    // 1. Lost the module graph, causing missing files later.
+                    // 2. Lost a specification, causing unsound verification.
+                    // We must abort the build.
+                    let _ = err_tx.send(anyhow::anyhow!(e));
+                }
             }
-        }
-
-        Ok(next_paths)
-    })();
-
-    match result {
-        Ok(children) => {
+        }) {
+            Ok(res) => res,
+            Err(e) => {
+                let _ = err_tx
+                    .send(anyhow::anyhow!(e).context(format!("Failed to parse {:?}", src_path)));
+                return;
+            }
+        };
+
+    // Resolve and queue child modules for processing.
+    let base_dir = src_path.parent().unwrap();
+    for module in unloaded_modules {
+        if let Some(mod_path) =
+            resolve_module_path(base_dir, &module.name, module.path_attr.as_deref())
+        {
             // Spawn new tasks for discovered modules.
-            for (child_path, mod_name) in children {
-                let (err_tx, path_tx) = (err_tx.clone(), path_tx.clone());
+            let (err_tx, path_tx) = (err_tx.clone(), path_tx.clone());
 
-                let mut new_prefix = module_prefix.clone();
-                new_prefix.push(mod_name);
+            let mut new_prefix = module_prefix.clone();
+            new_prefix.push(module.name);
 
-                let name = name.clone();
-                scope.spawn(move |s| {
-                    process_file_recursive(
-                        s,
-                        &child_path,
-                        config,
-                        visited,
-                        err_tx,
-                        path_tx,
-                        new_prefix,
-                        name,
-                    )
-                })
-            }
-        }
-        Err(e) => {
-            let _ = err_tx.send(e);
+            let name = name.clone();
+            scope.spawn(move |s| {
+                process_file_recursive(
+                    s, &mod_path, config, visited, err_tx, path_tx, new_prefix, name,
+                )
+            })
+        } else {
+            // This is an expected condition – it shows up when modules are
+            // conditionally compiled. Instead of implementing conditional
+            // compilation ourselves, we can just let rustc error later if
+            // this is actually an error.
+            log::debug!("Could not resolve module '{}' in {:?}", module.name, src_path);
         }
     }
 }

tools/hermes/tests/fixtures/env_interleaved_stdout/mock_charon_output.json

@@ -1,3 +1,3 @@
 Line 1 from charon
-{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: interleaved\n", "children": [], "code": null, "level": "error", "message": "interleaved error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "label", "text": [], "expansion": null}]}}
+{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: interleaved\n", "children": [], "code": null, "level": "error", "message": "interleaved error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "label", "text": [], "expansion": null}]}}
 Line 2 from charon

tools/hermes/tests/fixtures/fs_missing_source/mock_charon_output.json

@@ -1 +1 @@
-{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: missing source\n", "children": [], "code": null, "level": "error", "message": "missing source", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[SHADOW_ROOT]/src/missing.rs", "is_primary": true, "label": "label", "text": [], "expansion": null}]}}
+{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: missing source\n", "children": [], "code": null, "level": "error", "message": "missing source", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[PROJECT_ROOT]/src/missing.rs", "is_primary": true, "label": "label", "text": [], "expansion": null}]}}

tools/hermes/tests/fixtures/json_code_suggestions/mock_charon_output.json

@@ -1 +1 @@
-{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "crate_types": ["lib"], "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: ignore this rendered text\n", "children": [], "code": null, "level": "error", "message": "real error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "expansion": null, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "real label", "line_end": 1, "line_start": 1, "text": []}]}}
+{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "crate_types": ["lib"], "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: ignore this rendered text\n", "children": [], "code": null, "level": "error", "message": "real error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "expansion": null, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "real label", "line_end": 1, "line_start": 1, "text": []}]}}

tools/hermes/tests/fixtures/json_nested_children/mock_charon_output.json

@@ -1 +1 @@
-{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "crate_types": ["lib"], "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: parent error\n", "children": [{"children": [], "code": null, "level": "help", "message": "help me", "rendered": null, "spans": []}], "code": null, "level": "error", "message": "parent error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "expansion": null, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "oops", "line_end": 1, "line_start": 1, "text": []}]}}
+{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "crate_types": ["lib"], "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: parent error\n", "children": [{"children": [], "code": null, "level": "help", "message": "help me", "rendered": null, "spans": []}], "code": null, "level": "error", "message": "parent error", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "expansion": null, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "oops", "line_end": 1, "line_start": 1, "text": []}]}}

tools/hermes/tests/fixtures/map_mixed_diagnostics/mock_charon_output.json

@@ -1 +1 @@
-{"reason": "compiler-message", "message": {"message": "mixed span error", "level": "error", "code": null, "spans": [{"file_name": "[SHADOW_ROOT]/src/rewritten.rs", "byte_start": 10, "byte_end": 20, "line_start": 1, "line_end": 1, "column_start": 11, "column_end": 21, "is_primary": true, "text": [], "label": "called here"}, {"file_name": "[PROJECT_ROOT]/src/symlinked.rs", "byte_start": 50, "byte_end": 60, "line_start": 2, "line_end": 2, "column_start": 1, "column_end": 11, "is_primary": false, "text": [], "label": "defined here"}], "children": [], "rendered": "Rendered mixed error"}}
+{"reason": "compiler-message", "message": {"message": "mixed span error", "level": "error", "code": null, "spans": [{"file_name": "[PROJECT_ROOT]/src/rewritten.rs", "byte_start": 10, "byte_end": 20, "line_start": 1, "line_end": 1, "column_start": 11, "column_end": 21, "is_primary": true, "text": [], "label": "called here"}, {"file_name": "[PROJECT_ROOT]/src/symlinked.rs", "byte_start": 50, "byte_end": 60, "line_start": 2, "line_end": 2, "column_start": 1, "column_end": 11, "is_primary": false, "text": [], "label": "defined here"}], "children": [], "rendered": "Rendered mixed error"}}

tools/hermes/tests/fixtures/map_symlinked_file/mock_charon_output.json

@@ -1 +1 @@
-{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: something bad\n --> src/untransformed.rs:1:1\n", "children": [], "code": null, "level": "error", "message": "something bad", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "expansion": null, "file_name": "[SHADOW_ROOT]/src/untransformed.rs", "is_primary": true, "label": "oops", "line_end": 1, "line_start": 1, "suggested_replacement": null, "suggestion_applicability": null, "text": [{"highlight_end": 11, "highlight_start": 1, "text": "pub fn untouched() {}"}]}]}}
+{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: something bad\n --> src/untransformed.rs:1:1\n", "children": [], "code": null, "level": "error", "message": "something bad", "spans": [{"byte_end": 10, "byte_start": 0, "column_end": 11, "column_start": 1, "expansion": null, "file_name": "[PROJECT_ROOT]/src/untransformed.rs", "is_primary": true, "label": "oops", "line_end": 1, "line_start": 1, "suggested_replacement": null, "suggestion_applicability": null, "text": [{"highlight_end": 11, "highlight_start": 1, "text": "pub fn untouched() {}"}]}]}}

tools/hermes/tests/fixtures/span_empty_unsafe_block/mock_charon_output.json

@@ -1 +1 @@
-{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "crate_types": ["lib"], "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: unsafe\n", "children": [], "code": null, "level": "error", "message": "unsafe", "spans": [{"byte_end": 18, "byte_start": 9, "column_end": 19, "column_start": 10, "expansion": null, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "danger", "line_end": 1, "line_start": 1, "text": []}]}}
+{"reason": "compiler-message", "package_id": "test 0.1.0 (path+file://[PROJECT_ROOT])", "target": {"kind": ["lib"], "name": "test", "src_path": "[PROJECT_ROOT]/src/lib.rs", "crate_types": ["lib"], "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: unsafe\n", "children": [], "code": null, "level": "error", "message": "unsafe", "spans": [{"byte_end": 18, "byte_start": 9, "column_end": 19, "column_start": 10, "expansion": null, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "danger", "line_end": 1, "line_start": 1, "text": []}]}}