From f1646acda59bfa43d4ddacb01910d0f2ff3aaed6 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Thu, 12 Feb 2026 14:56:03 +0000 Subject: [PATCH] [hermes] Harden against weird symlink layout gherrit-pr-id: Gtu5rhuk5rjkrhhqpfwbmniejgf57ogzn --- tools/hermes/src/parse.rs | 2 +- tools/hermes/src/resolve.rs | 12 ++++-- tools/hermes/src/scanner.rs | 37 ++++++++++++++++--- .../expected_status.txt | 1 + .../canonicalized_workspace/hermes.toml | 0 .../canonicalized_workspace/source/Cargo.toml | 3 ++ .../source/crates/app/Cargo.toml | 10 +++++ .../source/crates/app/src/lib.rs | 4 ++ .../source/crates/lib/Cargo.toml | 6 +++ .../source/crates/lib/src/lib.rs | 1 + .../fixtures/cyclic_paths/expected_status.txt | 1 + .../tests/fixtures/cyclic_paths/hermes.toml | 0 .../fixtures/cyclic_paths/source/Cargo.toml | 6 +++ .../fixtures/cyclic_paths/source/src/lib.rs | 9 +++++ .../missing_cfg_file/expected_status.txt | 1 + .../fixtures/missing_cfg_file/hermes.toml | 0 .../missing_cfg_file/source/Cargo.toml | 6 +++ .../missing_cfg_file/source/src/lib.rs | 7 ++++ .../nested_file_mod/expected_config.toml | 3 ++ .../nested_file_mod/expected_status.txt | 1 + .../fixtures/nested_file_mod/hermes.toml | 0 .../nested_file_mod/source/Cargo.toml | 6 +++ .../nested_file_mod/source/src/foo.rs | 1 + .../nested_file_mod/source/src/foo/bar.rs | 4 ++ .../nested_file_mod/source/src/lib.rs | 1 + 25 files changed, 113 insertions(+), 9 deletions(-) create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/expected_status.txt create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/hermes.toml create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/source/Cargo.toml create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/Cargo.toml create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/Cargo.toml create mode 100644 tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/src/lib.rs create mode 100644 tools/hermes/tests/fixtures/cyclic_paths/expected_status.txt create mode 100644 tools/hermes/tests/fixtures/cyclic_paths/hermes.toml create mode 100644 tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml create mode 100644 tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs create mode 100644 tools/hermes/tests/fixtures/missing_cfg_file/expected_status.txt create mode 100644 tools/hermes/tests/fixtures/missing_cfg_file/hermes.toml create mode 100644 tools/hermes/tests/fixtures/missing_cfg_file/source/Cargo.toml create mode 100644 tools/hermes/tests/fixtures/missing_cfg_file/source/src/lib.rs create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/expected_config.toml create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/expected_status.txt create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/hermes.toml create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/source/Cargo.toml create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/source/src/foo.rs create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/source/src/foo/bar.rs create mode 100644 tools/hermes/tests/fixtures/nested_file_mod/source/src/lib.rs diff --git a/tools/hermes/src/parse.rs b/tools/hermes/src/parse.rs index 07c1b7d586..1fa0d5257f 100644 --- a/tools/hermes/src/parse.rs +++ b/tools/hermes/src/parse.rs @@ -118,7 +118,7 @@ where F: FnMut(&str, Result), { log::trace!("read_file_and_scan_compilation_unit({:?})", path); - let source = fs::read_to_string(path).expect("Failed to read file"); + let source = fs::read_to_string(path)?; let unloaded_modules = scan_compilation_unit(&source, f); Ok((source, unloaded_modules)) } diff --git a/tools/hermes/src/resolve.rs b/tools/hermes/src/resolve.rs index 28d6aede28..49a0004b7d 100644 --- a/tools/hermes/src/resolve.rs +++ b/tools/hermes/src/resolve.rs @@ -1,5 +1,5 @@ use std::{ - env, + env, fs, hash::{Hash as _, Hasher as _}, path::PathBuf, }; @@ -341,7 +341,9 @@ fn resolve_targets<'a>( /// is found. pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> { log::trace!("check_for_external_deps"); - let workspace_root = metadata.workspace_root.as_std_path(); + // Canonicalize workspace root to handle symlinks correctly + let workspace_root = fs::canonicalize(&metadata.workspace_root) + .context("Failed to canonicalize workspace root")?; for pkg in &metadata.packages { // We only care about packages that are "local" (source is None). @@ -350,8 +352,12 @@ pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> { if pkg.source.is_none() { let pkg_path = pkg.manifest_path.as_std_path(); + // Canonicalize the package path for comparison + let canonical_pkg_path = fs::canonicalize(pkg_path) + .with_context(|| format!("Failed to canonicalize path for package {}", pkg.name))?; + // Check if the package lives outside the workspace tree - if !pkg_path.starts_with(workspace_root) { + if !canonical_pkg_path.starts_with(&workspace_root) { anyhow::bail!( "Unsupported external dependency: '{}' at {:?}.\n\ Hermes currently only supports verifying workspaces where all local \ diff --git a/tools/hermes/src/scanner.rs b/tools/hermes/src/scanner.rs index 2696d651e2..9e1c130891 100644 --- a/tools/hermes/src/scanner.rs +++ b/tools/hermes/src/scanner.rs @@ -1,5 +1,6 @@ use std::{ collections::HashMap, + ffi::OsStr, hash::{Hash, Hasher as _}, path::{Path, PathBuf}, sync::mpsc::{self, Sender}, @@ -141,14 +142,28 @@ fn process_file_recursive<'a>( name: HermesTargetName, ) { log::trace!("process_file_recursive(src_path: {:?})", src_path); - if !visited.insert(src_path.to_path_buf()) { + + // Canonicalize the path to ensure we don't process the same file multiple + // times (e.g. via symlinks or different relative paths). + let src_path = match std::fs::canonicalize(src_path) { + Ok(p) => p, + Err(e) => { + // It is valid for a module to be declared but not exist (e.g., if + // it is cfg-gated for another platform). In strict Rust, we would + // check the cfg attributes, but since we are just scanning, it is + // safe to warn and return. + log::debug!("Skipping unreachable or missing file {:?}: {}", src_path, e); + return; + } + }; + + if !visited.insert(src_path.clone()) { return; } - // Walking the AST is enough to collect new modules. // 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 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() { @@ -177,11 +192,23 @@ fn process_file_recursive<'a>( } }; + // Determine the directory to search for child modules in. + // - For `mod.rs`, `lib.rs`, `main.rs`, children are in the parent directory. + // e.g. `src/lib.rs` -> `mod foo` -> `src/foo.rs` + // - For `my_mod.rs`, children are in a sibling directory of the same name. + // e.g. `src/my_mod.rs` -> `mod sub` -> `src/my_mod/sub.rs` + let file_stem = src_path.file_stem().and_then(OsStr::to_str).unwrap_or(""); + let base_dir = if matches!(file_stem, "mod" | "lib" | "main") { + src_path.parent().unwrap_or(&src_path).to_path_buf() + } else { + // e.g. src/foo.rs -> src/foo/ + src_path.with_extension("") + }; + // 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()) + resolve_module_path(&base_dir, &module.name, module.path_attr.as_deref()) { // Spawn new tasks for discovered modules. let (err_tx, path_tx) = (err_tx.clone(), path_tx.clone()); diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/expected_status.txt b/tools/hermes/tests/fixtures/canonicalized_workspace/expected_status.txt new file mode 100644 index 0000000000..2e9ba477f8 --- /dev/null +++ b/tools/hermes/tests/fixtures/canonicalized_workspace/expected_status.txt @@ -0,0 +1 @@ +success diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/hermes.toml b/tools/hermes/tests/fixtures/canonicalized_workspace/hermes.toml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/source/Cargo.toml b/tools/hermes/tests/fixtures/canonicalized_workspace/source/Cargo.toml new file mode 100644 index 0000000000..293e64e9bc --- /dev/null +++ b/tools/hermes/tests/fixtures/canonicalized_workspace/source/Cargo.toml @@ -0,0 +1,3 @@ +[workspace] +members = ["crates/app", "crates/lib"] +resolver = "2" diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/Cargo.toml b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/Cargo.toml new file mode 100644 index 0000000000..3ff246c8f3 --- /dev/null +++ b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "app" +version = "0.1.0" +edition = "2021" + +[dependencies] +# Intentionally messy relative path that traverses up and down +# ../../crates/lib is inside the workspace, but we structure it to ensure +# canonicalization is required to match it correctly. +my_lib = { path = "../../crates/lib" } diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs new file mode 100644 index 0000000000..54406dd2f7 --- /dev/null +++ b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs @@ -0,0 +1,4 @@ +/// ```lean +/// theorem main_proof : True := trivial +/// ``` +pub fn main_proof() {} diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/Cargo.toml b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/Cargo.toml new file mode 100644 index 0000000000..7a4919fb2d --- /dev/null +++ b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "my_lib" +version = "0.1.0" +edition = "2021" + +[dependencies] diff --git a/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/src/lib.rs b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/src/lib.rs new file mode 100644 index 0000000000..b1d5c4b8ed --- /dev/null +++ b/tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/src/lib.rs @@ -0,0 +1 @@ +pub fn shared() {} diff --git a/tools/hermes/tests/fixtures/cyclic_paths/expected_status.txt b/tools/hermes/tests/fixtures/cyclic_paths/expected_status.txt new file mode 100644 index 0000000000..7a4059ef83 --- /dev/null +++ b/tools/hermes/tests/fixtures/cyclic_paths/expected_status.txt @@ -0,0 +1 @@ +failure diff --git a/tools/hermes/tests/fixtures/cyclic_paths/hermes.toml b/tools/hermes/tests/fixtures/cyclic_paths/hermes.toml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml b/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml new file mode 100644 index 0000000000..c9d084f63a --- /dev/null +++ b/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "cyclic_paths" +version = "0.1.0" +edition = "2021" + +[dependencies] diff --git a/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs b/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs new file mode 100644 index 0000000000..03f8974b07 --- /dev/null +++ b/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs @@ -0,0 +1,9 @@ +// This simulates a symlink loop by pointing a module declaration back at itself. +// Without canonicalization, this causes a stack overflow. +#[path = "lib.rs"] +mod self_loop; + +/// ```lean +/// theorem valid : True := trivial +/// ``` +pub fn valid() {} diff --git a/tools/hermes/tests/fixtures/missing_cfg_file/expected_status.txt b/tools/hermes/tests/fixtures/missing_cfg_file/expected_status.txt new file mode 100644 index 0000000000..2e9ba477f8 --- /dev/null +++ b/tools/hermes/tests/fixtures/missing_cfg_file/expected_status.txt @@ -0,0 +1 @@ +success diff --git a/tools/hermes/tests/fixtures/missing_cfg_file/hermes.toml b/tools/hermes/tests/fixtures/missing_cfg_file/hermes.toml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tools/hermes/tests/fixtures/missing_cfg_file/source/Cargo.toml b/tools/hermes/tests/fixtures/missing_cfg_file/source/Cargo.toml new file mode 100644 index 0000000000..390b40c24b --- /dev/null +++ b/tools/hermes/tests/fixtures/missing_cfg_file/source/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "missing_cfg_file" +version = "0.1.0" +edition = "2021" + +[dependencies] diff --git a/tools/hermes/tests/fixtures/missing_cfg_file/source/src/lib.rs b/tools/hermes/tests/fixtures/missing_cfg_file/source/src/lib.rs new file mode 100644 index 0000000000..19b192970f --- /dev/null +++ b/tools/hermes/tests/fixtures/missing_cfg_file/source/src/lib.rs @@ -0,0 +1,7 @@ +#[cfg(target_os = "windows")] +mod windows_sys; // This file will intentionally not exist + +/// ```lean +/// theorem demo : True := trivial +/// ``` +pub fn demo() {} diff --git a/tools/hermes/tests/fixtures/nested_file_mod/expected_config.toml b/tools/hermes/tests/fixtures/nested_file_mod/expected_config.toml new file mode 100644 index 0000000000..dd1eb20ee2 --- /dev/null +++ b/tools/hermes/tests/fixtures/nested_file_mod/expected_config.toml @@ -0,0 +1,3 @@ +[[command]] +args = ["--start-from", "crate::foo::bar::deep_proof"] +should_not_exist = false diff --git a/tools/hermes/tests/fixtures/nested_file_mod/expected_status.txt b/tools/hermes/tests/fixtures/nested_file_mod/expected_status.txt new file mode 100644 index 0000000000..2e9ba477f8 --- /dev/null +++ b/tools/hermes/tests/fixtures/nested_file_mod/expected_status.txt @@ -0,0 +1 @@ +success diff --git a/tools/hermes/tests/fixtures/nested_file_mod/hermes.toml b/tools/hermes/tests/fixtures/nested_file_mod/hermes.toml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/tools/hermes/tests/fixtures/nested_file_mod/source/Cargo.toml b/tools/hermes/tests/fixtures/nested_file_mod/source/Cargo.toml new file mode 100644 index 0000000000..3d37c4f3fe --- /dev/null +++ b/tools/hermes/tests/fixtures/nested_file_mod/source/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "nested_file_mod" +version = "0.1.0" +edition = "2021" + +[dependencies] diff --git a/tools/hermes/tests/fixtures/nested_file_mod/source/src/foo.rs b/tools/hermes/tests/fixtures/nested_file_mod/source/src/foo.rs new file mode 100644 index 0000000000..8f95ce316a --- /dev/null +++ b/tools/hermes/tests/fixtures/nested_file_mod/source/src/foo.rs @@ -0,0 +1 @@ +mod bar; diff --git a/tools/hermes/tests/fixtures/nested_file_mod/source/src/foo/bar.rs b/tools/hermes/tests/fixtures/nested_file_mod/source/src/foo/bar.rs new file mode 100644 index 0000000000..556ebd2241 --- /dev/null +++ b/tools/hermes/tests/fixtures/nested_file_mod/source/src/foo/bar.rs @@ -0,0 +1,4 @@ +/// ```lean +/// theorem deep_proof : True := trivial +/// ``` +pub fn deep_proof() {} diff --git a/tools/hermes/tests/fixtures/nested_file_mod/source/src/lib.rs b/tools/hermes/tests/fixtures/nested_file_mod/source/src/lib.rs new file mode 100644 index 0000000000..f4ad3bff5c --- /dev/null +++ b/tools/hermes/tests/fixtures/nested_file_mod/source/src/lib.rs @@ -0,0 +1 @@ +mod foo;