diff --git a/tools/hermes/src/resolve.rs b/tools/hermes/src/resolve.rs index bcff354367..28d6aede28 100644 --- a/tools/hermes/src/resolve.rs +++ b/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 { }, kind, src_path: target.src_path.as_std_path().to_owned(), + manifest_path: package.manifest_path.as_std_path().to_owned(), }); } } @@ -187,7 +190,7 @@ 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); } @@ -195,7 +198,7 @@ fn resolve_run_root(metadata: &Metadata) -> PathBuf { // 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 diff --git a/tools/hermes/src/scanner.rs b/tools/hermes/src/scanner.rs index 629dce0900..2696d651e2 100644 --- a/tools/hermes/src/scanner.rs +++ b/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> { log::trace!("scan_workspace({:?})", roots); @@ -117,7 +117,7 @@ pub fn scan_workspace(roots: &Roots) -> Result> { .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> { .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 { - 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> { - // 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); } } } diff --git a/tools/hermes/tests/fixtures/env_interleaved_stdout/mock_charon_output.json b/tools/hermes/tests/fixtures/env_interleaved_stdout/mock_charon_output.json index 61b528a00d..9123e36220 100644 --- a/tools/hermes/tests/fixtures/env_interleaved_stdout/mock_charon_output.json +++ b/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 diff --git a/tools/hermes/tests/fixtures/fs_missing_source/mock_charon_output.json b/tools/hermes/tests/fixtures/fs_missing_source/mock_charon_output.json index 366092dc02..3326c561fa 100644 --- a/tools/hermes/tests/fixtures/fs_missing_source/mock_charon_output.json +++ b/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}]}} \ No newline at end of file +{"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}]}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/json_code_suggestions/mock_charon_output.json b/tools/hermes/tests/fixtures/json_code_suggestions/mock_charon_output.json index 3aa84b53fb..5367c64d56 100644 --- a/tools/hermes/tests/fixtures/json_code_suggestions/mock_charon_output.json +++ b/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": []}]}} \ No newline at end of file +{"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": []}]}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/json_nested_children/mock_charon_output.json b/tools/hermes/tests/fixtures/json_nested_children/mock_charon_output.json index ff19b723f4..e5f7ee92b6 100644 --- a/tools/hermes/tests/fixtures/json_nested_children/mock_charon_output.json +++ b/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": []}]}} \ No newline at end of file +{"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": []}]}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/map_mixed_diagnostics/mock_charon_output.json b/tools/hermes/tests/fixtures/map_mixed_diagnostics/mock_charon_output.json index 2aa0eac805..caa7ba78c9 100644 --- a/tools/hermes/tests/fixtures/map_mixed_diagnostics/mock_charon_output.json +++ b/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"}} diff --git a/tools/hermes/tests/fixtures/map_rewritten_file/mock_charon_output.json b/tools/hermes/tests/fixtures/map_rewritten_file/mock_charon_output.json deleted file mode 100644 index caf9404f76..0000000000 --- a/tools/hermes/tests/fixtures/map_rewritten_file/mock_charon_output.json +++ /dev/null @@ -1 +0,0 @@ -{"reason": "compiler-message", "package_id": "map_rewritten_file 0.1.0 (path+file://[SHADOW_ROOT])", "manifest_path": "[SHADOW_ROOT]/Cargo.toml", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "map_rewritten_file", "src_path": "[SHADOW_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: my test error\n", "spans": [{"file_name": "[SHADOW_ROOT]/src/lib.rs", "byte_start": 36, "byte_end": 52, "line_start": 4, "line_end": 4, "column_start": 1, "column_end": 17, "is_primary": true, "text": [{"text": "pub fn demo() {}", "highlight_start": 1, "highlight_end": 17}], "label": "my span label"}], "message": "my test error", "level": "error", "code": null, "children": []}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/map_symlinked_file/mock_charon_output.json b/tools/hermes/tests/fixtures/map_symlinked_file/mock_charon_output.json index cd488ed2d5..0a3bf4c7e6 100644 --- a/tools/hermes/tests/fixtures/map_symlinked_file/mock_charon_output.json +++ b/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() {}"}]}]}} \ No newline at end of file +{"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() {}"}]}]}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/span_empty_unsafe_block/mock_charon_output.json b/tools/hermes/tests/fixtures/span_empty_unsafe_block/mock_charon_output.json index 1454214dc2..174d30d9e4 100644 --- a/tools/hermes/tests/fixtures/span_empty_unsafe_block/mock_charon_output.json +++ b/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": []}]}} \ No newline at end of file +{"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": []}]}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/span_macro_expansion/mock_charon_output.json b/tools/hermes/tests/fixtures/span_macro_expansion/mock_charon_output.json index 37cdb51ad9..e605512927 100644 --- a/tools/hermes/tests/fixtures/span_macro_expansion/mock_charon_output.json +++ b/tools/hermes/tests/fixtures/span_macro_expansion/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: macro fail\n", "children": [], "code": null, "level": "error", "message": "macro fail", "spans": [{"byte_end": 42, "byte_start": 38, "column_end": 43, "column_start": 39, "expansion": {"span": {"byte_end": 42, "byte_start": 38, "column_end": 43, "column_start": 39, "line_end": 1, "line_start": 1, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "bang", "text": [], "expansion": null}, "macro_decl_name": "f!", "def_site_span": {"byte_end": 29, "byte_start": 0, "column_end": 30, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": null, "text": [], "expansion": null}}, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "bang", "line_end": 1, "line_start": 1, "text": []}]}} \ No newline at end of file +{"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: macro fail\n", "children": [], "code": null, "level": "error", "message": "macro fail", "spans": [{"byte_end": 42, "byte_start": 38, "column_end": 43, "column_start": 39, "expansion": {"span": {"byte_end": 42, "byte_start": 38, "column_end": 43, "column_start": 39, "line_end": 1, "line_start": 1, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "bang", "text": [], "expansion": null}, "macro_decl_name": "f!", "def_site_span": {"byte_end": 29, "byte_start": 0, "column_end": 30, "column_start": 1, "line_end": 1, "line_start": 1, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": null, "text": [], "expansion": null}}, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "bang", "line_end": 1, "line_start": 1, "text": []}]}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/map_rewritten_file/expected_status.txt b/tools/hermes/tests/fixtures/span_mapping_basic/expected_status.txt similarity index 100% rename from tools/hermes/tests/fixtures/map_rewritten_file/expected_status.txt rename to tools/hermes/tests/fixtures/span_mapping_basic/expected_status.txt diff --git a/tools/hermes/tests/fixtures/map_rewritten_file/expected_stderr.txt b/tools/hermes/tests/fixtures/span_mapping_basic/expected_stderr.txt similarity index 100% rename from tools/hermes/tests/fixtures/map_rewritten_file/expected_stderr.txt rename to tools/hermes/tests/fixtures/span_mapping_basic/expected_stderr.txt diff --git a/tools/hermes/tests/fixtures/map_rewritten_file/hermes.toml b/tools/hermes/tests/fixtures/span_mapping_basic/hermes.toml similarity index 100% rename from tools/hermes/tests/fixtures/map_rewritten_file/hermes.toml rename to tools/hermes/tests/fixtures/span_mapping_basic/hermes.toml diff --git a/tools/hermes/tests/fixtures/span_mapping_basic/mock_charon_output.json b/tools/hermes/tests/fixtures/span_mapping_basic/mock_charon_output.json new file mode 100644 index 0000000000..867fcd7af9 --- /dev/null +++ b/tools/hermes/tests/fixtures/span_mapping_basic/mock_charon_output.json @@ -0,0 +1 @@ +{"reason": "compiler-message", "package_id": "span_mapping_basic 0.1.0 (path+file://[PROJECT_ROOT])", "manifest_path": "[PROJECT_ROOT]/Cargo.toml", "target": {"kind": ["lib"], "crate_types": ["lib"], "name": "span_mapping_basic", "src_path": "[PROJECT_ROOT]/src/lib.rs", "edition": "2021", "doc": true, "doctest": true, "test": true}, "message": {"rendered": "error: my test error\n", "spans": [{"file_name": "[PROJECT_ROOT]/src/lib.rs", "byte_start": 36, "byte_end": 52, "line_start": 4, "line_end": 4, "column_start": 1, "column_end": 17, "is_primary": true, "text": [{"text": "pub fn demo() {}", "highlight_start": 1, "highlight_end": 17}], "label": "my span label"}], "message": "my test error", "level": "error", "code": null, "children": []}} \ No newline at end of file diff --git a/tools/hermes/tests/fixtures/map_rewritten_file/source/Cargo.toml b/tools/hermes/tests/fixtures/span_mapping_basic/source/Cargo.toml similarity index 68% rename from tools/hermes/tests/fixtures/map_rewritten_file/source/Cargo.toml rename to tools/hermes/tests/fixtures/span_mapping_basic/source/Cargo.toml index 6f38a5210f..f4efaf35c0 100644 --- a/tools/hermes/tests/fixtures/map_rewritten_file/source/Cargo.toml +++ b/tools/hermes/tests/fixtures/span_mapping_basic/source/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "map_rewritten_file" +name = "span_mapping_basic" version = "0.1.0" edition = "2021" diff --git a/tools/hermes/tests/fixtures/map_rewritten_file/source/src/lib.rs b/tools/hermes/tests/fixtures/span_mapping_basic/source/src/lib.rs similarity index 100% rename from tools/hermes/tests/fixtures/map_rewritten_file/source/src/lib.rs rename to tools/hermes/tests/fixtures/span_mapping_basic/source/src/lib.rs diff --git a/tools/hermes/tests/fixtures/span_multibyte_offsets/mock_charon_output.json b/tools/hermes/tests/fixtures/span_multibyte_offsets/mock_charon_output.json index 189f5ce490..52f8e3939e 100644 --- a/tools/hermes/tests/fixtures/span_multibyte_offsets/mock_charon_output.json +++ b/tools/hermes/tests/fixtures/span_multibyte_offsets/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: fire\n", "children": [], "code": null, "level": "error", "message": "fire", "spans": [{"byte_end": 12, "byte_start": 7, "column_end": 9, "column_start": 8, "expansion": null, "file_name": "[SHADOW_ROOT]/src/lib.rs", "is_primary": true, "label": "hot", "line_end": 1, "line_start": 1, "text": []}]}} \ No newline at end of file +{"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: fire\n", "children": [], "code": null, "level": "error", "message": "fire", "spans": [{"byte_end": 12, "byte_start": 7, "column_end": 9, "column_start": 8, "expansion": null, "file_name": "[PROJECT_ROOT]/src/lib.rs", "is_primary": true, "label": "hot", "line_end": 1, "line_start": 1, "text": []}]}} \ No newline at end of file diff --git a/tools/hermes/tests/integration.rs b/tools/hermes/tests/integration.rs index 337f438bf7..ede0e474db 100644 --- a/tools/hermes/tests/integration.rs +++ b/tools/hermes/tests/integration.rs @@ -2,7 +2,6 @@ use std::{fs, os::unix::fs::PermissionsExt, path::Path}; use serde::Deserialize; use tempfile::tempdir; -use walkdir::WalkDir; datatest_stable::harness! { { test = run_integration_test, root = "tests/fixtures", pattern = "hermes.toml$" } } @@ -89,22 +88,13 @@ exec "{1}" "$@" .env_remove("RUSTFLAGS") // Forces deterministic output path: target/hermes/hermes_test_target // (normally, the path includes a hash of the crate's path). - .env("HERMES_TEST_SHADOW_NAME", "hermes_test_target"); + .env("HERMES_TEST_DIR_NAME", "hermes_test_target"); // Mock JSON integration let mock_json_file = test_case_root.join("mock_charon_output.json"); if mock_json_file.exists() { - // Instead of writing the mock json to the shadow root (which gets cleared by build_shadow_crate), write it to the test workspace root! - // We still need the path for mapping `[SHADOW_ROOT]` correctly! - // But we construct it manually since it might not be created yet: - let abs_shadow_root = std::env::current_dir().unwrap().join(&sandbox_root); - let abs_test_case_root = - test_case_root.canonicalize().unwrap_or_else(|_| test_case_root.to_path_buf()); - let mock_src = fs::read_to_string(&mock_json_file).unwrap(); - let processed_mock = mock_src - .replace("[PROJECT_ROOT]", sandbox_root.to_str().unwrap()) - .replace("[SHADOW_ROOT]", abs_shadow_root.to_str().unwrap()); + let processed_mock = mock_src.replace("[PROJECT_ROOT]", sandbox_root.to_str().unwrap()); let processed_mock_file = sandbox_root.join("mock_charon_output.json"); fs::write(&processed_mock_file, &processed_mock).unwrap();