diff --git a/tools/hermes/src/main.rs b/tools/hermes/src/main.rs index 88240d5b91..30b5e03d5f 100644 --- a/tools/hermes/src/main.rs +++ b/tools/hermes/src/main.rs @@ -4,7 +4,7 @@ mod errors; mod parse; mod resolve; mod shadow; -mod transform; + mod ui_test_shim; use clap::Parser; diff --git a/tools/hermes/src/shadow.rs b/tools/hermes/src/shadow.rs index c87f8695a8..1e2eeba142 100644 --- a/tools/hermes/src/shadow.rs +++ b/tools/hermes/src/shadow.rs @@ -14,7 +14,6 @@ use walkdir::WalkDir; use crate::{ parse, resolve::{HermesTargetKind, HermesTargetName, Roots}, - transform, }; pub struct HermesArtifact { @@ -207,13 +206,11 @@ fn process_file_recursive<'a>( fs::create_dir_all(parent)?; } - // Walk the AST, collecting edits and new modules to process. - let mut edits = Vec::new(); + // 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) => { - transform::append_edits(&parsed_item, &mut edits); if let Some(item_name) = parsed_item.item.name() { // Calculate the full path to this item. let mut full_path = module_prefix.clone(); @@ -234,9 +231,7 @@ fn process_file_recursive<'a>( }) .context(format!("Failed to parse {:?}", src_path))?; - // Apply edits in-place before writing to disk. - let mut buffer = source_code.into_bytes(); - transform::apply_edits(&mut buffer, &edits); + let buffer = source_code.into_bytes(); fs::write(&dest_path, &buffer) .context(format!("Failed to write shadow file {:?}", dest_path))?; diff --git a/tools/hermes/src/transform.rs b/tools/hermes/src/transform.rs deleted file mode 100644 index 8ec897249c..0000000000 --- a/tools/hermes/src/transform.rs +++ /dev/null @@ -1,178 +0,0 @@ -use std::ops::Range; - -use syn::spanned::Spanned; - -use crate::parse::{ParsedItem, ParsedLeanItem}; - -/// Appends the byte ranges that should be blanked out in the shadow crate. -/// -/// For `unsafe` functions with Hermes annotations, this targets: -/// 1. The `unsafe` keyword (to make the function signature "safe" for Aeneas). -/// 2. The *contents* of the function block (preserving the braces `{}`). -pub fn append_edits(item: &ParsedLeanItem, edits: &mut Vec>) { - if let ParsedItem::Fn(func) = &item.item { - if let Some(unsafety) = &func.sig.unsafety { - // 1. Mark the `unsafe` keyword for blanking. - // Result: `unsafe fn` -> ` fn` - edits.push(unsafety.span().byte_range()); - - // TODO: - // - Only blank bodies for functions which are modeled. - // - Figure out what to replace these bodies with. - - // 2. Mark the *inside* of the block for blanking. - // We use start+1 and end-1 to preserve the curly braces. - let block_range = func.block.span().byte_range(); - if block_range.len() >= 2 { - edits.push(block_range.start + 1..block_range.end - 1); - } - } - } -} - -/// Applies a set of redaction edits to the source buffer in-place. -/// -/// For each span in `edits`, this function replaces all characters with spaces -/// (`0x20`), except for newline characters (`0x0A` and `0x0D`), which are -/// preserved to maintain line numbering and Windows compatibility. This allows -/// the shadow crate to report errors on spans that align with the user's -/// original file. -/// -/// # Panics -/// -/// Panics if any span in `edits` is not in-bounds of `buffer`. -pub fn apply_edits(buffer: &mut [u8], edits: &[Range]) { - for range in edits { - for byte in &mut buffer[range.clone()] { - if !matches!(*byte, b'\n' | b'\r') { - *byte = b' '; - } - } - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_apply_edits_preserves_newlines() { - let source = b"unsafe fn test() {\r\n let a = 1;\n let b = 2;\r\n}"; - let mut buffer = source.to_vec(); - - let file = syn::parse_file(std::str::from_utf8(source).unwrap()).unwrap(); - let func = match &file.items[0] { - syn::Item::Fn(f) => f, - _ => panic!("Expected function"), - }; - - let edits = - vec![func.sig.unsafety.unwrap().span().byte_range(), func.block.span().byte_range()]; - - apply_edits(&mut buffer, &edits); - - let expected = b" fn test() \r\n \n \r\n ".to_vec(); - assert_eq!(std::str::from_utf8(&buffer).unwrap(), std::str::from_utf8(&expected).unwrap()); - } - - #[test] - fn test_apply_edits_with_parsed_item() { - let source = " - /// ```lean - /// theorem foo : True := by trivial - /// ``` - unsafe fn foo() { - let x = 1; - } - "; - let mut items = Vec::new(); - crate::parse::scan_compilation_unit(source, |_src, res| items.push(res)); - - let item = items.into_iter().next().unwrap().unwrap(); - let mut edits = Vec::new(); - append_edits(&item, &mut edits); - - let mut buffer = source.as_bytes().to_vec(); - apply_edits(&mut buffer, &edits); - - let expected = " - /// ```lean - /// theorem foo : True := by trivial - /// ``` - fn foo() { - - } - "; - assert_eq!(std::str::from_utf8(&buffer).unwrap(), expected); - } - - #[test] - fn test_apply_edits_multibyte_utf8() { - // Source contains multi-byte characters: - // - Immediately preceding `unsafe`: `/*前*/` - // - Immediately following `{`: `/*后*/` - // - Immediately before `}`: `/*前*/` - let source = " - fn safe() {} - /// ```lean - /// ``` - /*前*/unsafe fn foo() {/*后*/ - let x = '中'; - /*前*/} - "; - let mut items = Vec::new(); - crate::parse::scan_compilation_unit(source, |_src, res| items.push(res)); - - // Find the unsafe function (should be the first item, as safe() is skipped) - let item = items - .into_iter() - .find(|i| { - if let Ok(ParsedLeanItem { item: ParsedItem::Fn(f), .. }) = i { - f.sig.ident == "foo" - } else { - false - } - }) - .unwrap() - .unwrap(); - - let mut edits = Vec::new(); - append_edits(&item, &mut edits); - - let mut buffer = source.as_bytes().to_vec(); - apply_edits(&mut buffer, &edits); - - // Expected whitespace lengths: - // Line 1: ` /*前*/unsafe fn foo() {/*后*/` - // - Indent: 12 spaces - // - `/*前*/`: 7 bytes (preserved) - // - `unsafe`: 6 bytes -> 6 spaces - // - ` fn foo() {`: 9 bytes (preserved) - // - `/*后*/`: 7 bytes -> 7 spaces - // - // Line 2: ` let x = '中';` - // - Indent: 16 spaces -> 16 spaces - // - `let x = '中';`: 14 bytes -> 14 spaces - // `let` (3) + ` ` (1) + `x` (1) + ` ` (1) + `=` (1) + ` ` (1) + `'` (1) + `中` (3) + `'` (1) + `;` (1) = 14 - // Total: 30 spaces - // - // Line 3: ` /*前*/}` - // - Indent 12 spaces -> 12 spaces - // - `/*前*/`: 7 bytes -> 7 spaces - // - `}`: 1 byte (preserved) - // Total: 19 spaces + `}` - - let line_with_unsafe = " /*前*/ fn foo() { "; - let line_body = " ".repeat(30); - let line_end = format!("{}}}", " ".repeat(19)); - - let expected = format!( - "\n fn safe() {{}}\n /// ```lean\n /// ```\n{}\n{}\n{}\n ", - line_with_unsafe, - line_body, - line_end - ); - - assert_eq!(std::str::from_utf8(&buffer).unwrap(), expected); - } -} diff --git a/tools/hermes/tests/fixtures/unsafe_redaction/expected/src/lib.rs b/tools/hermes/tests/fixtures/unsafe_redaction/expected/src/lib.rs index 1798de0a0a..31e1f13b80 100644 --- a/tools/hermes/tests/fixtures/unsafe_redaction/expected/src/lib.rs +++ b/tools/hermes/tests/fixtures/unsafe_redaction/expected/src/lib.rs @@ -1,6 +1,6 @@ /// ```lean /// model foo /// ``` - fn foo() -> i32 { - +unsafe fn foo() -> i32 { + 1 + 1 } diff --git a/tools/hermes/tests/fixtures/unsafe_redaction/expected_status.txt b/tools/hermes/tests/fixtures/unsafe_redaction/expected_status.txt index 7a4059ef83..2e9ba477f8 100644 --- a/tools/hermes/tests/fixtures/unsafe_redaction/expected_status.txt +++ b/tools/hermes/tests/fixtures/unsafe_redaction/expected_status.txt @@ -1 +1 @@ -failure +success diff --git a/tools/hermes/tests/fixtures/unsafe_redaction/expected_stderr.txt b/tools/hermes/tests/fixtures/unsafe_redaction/expected_stderr.txt index 2406573f31..8b13789179 100644 --- a/tools/hermes/tests/fixtures/unsafe_redaction/expected_stderr.txt +++ b/tools/hermes/tests/fixtures/unsafe_redaction/expected_stderr.txt @@ -1,11 +1 @@ -× mismatched types - ╭─[[PROJECT_ROOT]/src/lib.rs:4:11] - 3 │ /// ``` - 4 │ unsafe fn foo() -> i32 { - · ─┬─ ─┬─ - · │ ╰── expected `i32`, found `()` - · ╰── implicitly returns `()` as its body has no tail or `return` expression - 5 │ 1 + 1 - ╰──── -[External Info] For more information about this error, try `rustc --explain E0308`. diff --git a/tools/hermes/tests/fixtures/weird_functions/expected/src/lib.rs b/tools/hermes/tests/fixtures/weird_functions/expected/src/lib.rs index 57818aa977..15c7da8851 100644 --- a/tools/hermes/tests/fixtures/weird_functions/expected/src/lib.rs +++ b/tools/hermes/tests/fixtures/weird_functions/expected/src/lib.rs @@ -1,14 +1,14 @@ /// ```lean /// model async_foo /// ``` -async fn async_foo() -> i32 { } +async unsafe fn async_foo() -> i32 { 0 } /// ```lean /// model const_foo /// ``` -const fn const_foo() -> i32 { } +const unsafe fn const_foo() -> i32 { 0 } /// ```lean /// model extern_foo /// ``` - extern "C" fn extern_foo() -> i32 { } +unsafe extern "C" fn extern_foo() -> i32 { 0 } diff --git a/tools/hermes/tests/fixtures/workspace_path_dep/expected/app/src/lib.rs b/tools/hermes/tests/fixtures/workspace_path_dep/expected/app/src/lib.rs index 3f340b3cab..035b0948a1 100644 --- a/tools/hermes/tests/fixtures/workspace_path_dep/expected/app/src/lib.rs +++ b/tools/hermes/tests/fixtures/workspace_path_dep/expected/app/src/lib.rs @@ -1,4 +1,4 @@ /// ```lean /// model main /// ``` - fn main() +unsafe fn main() {}