[hermes] Get tests passing again

gherrit-pr-id: G3db3762006cf6333a7112b668f747072f8bb477b

Author: joshlf

tools/hermes/src/parse.rs

@@ -325,17 +325,14 @@ where
 
         // If this is a trait impl, we use UFCS syntax (`<Type as Trait>`). If
         // this is an inherent impl, we use the `Type: Type` syntax.
+        let self_ty = &node.self_ty;
         let segment = if let Some((_, path, _)) = &node.trait_ {
-            let self_ty = &node.self_ty;
-            let tokens = quote! { <#self_ty as #path> };
-            tokens.to_string().replace(" ", "") // Remove spaces for cleaner paths
+            quote! { <#self_ty as #path> }
         } else {
-            let self_ty = &node.self_ty;
-            let tokens = quote! { #self_ty };
-            tokens.to_string().replace(" ", "")
+            quote! { #self_ty }
         };
 
-        self.current_path.push(segment);
+        self.current_path.push(segment.to_string());
         syn::visit::visit_item_impl(self, node);
         self.current_path.pop();
     }

tools/hermes/src/transform.rs

@@ -1,24 +1,31 @@
-use proc_macro2::Span;
+use std::ops::Range;
+
 use syn::spanned::Spanned;
 
 use crate::parse::{ParsedItem, ParsedLeanItem};
 
-/// Appends the spans of text that should be blanked out in the shadow crate.
+/// 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 entire function block (to remove the unverified implementation).
-pub fn append_edits(item: &ParsedLeanItem, edits: &mut Vec<Span>) {
+/// 2. The *contents* of the function block (preserving the braces `{}`).
+pub fn append_edits(item: &ParsedLeanItem, edits: &mut Vec<Range<usize>>) {
     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());
+            edits.push(unsafety.span().byte_range());
 
             // TODO:
             // - Only blank bodies for functions which are modeled.
             // - Figure out what to replace these bodies with.
-            edits.push(func.block.span());
+
+            // 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);
+            }
         }
     }
 }
@@ -34,9 +41,9 @@ pub fn append_edits(item: &ParsedLeanItem, edits: &mut Vec<Span>) {
 /// # Panics
 ///
 /// Panics if any span in `edits` is not in-bounds of `buffer`.
-pub fn apply_edits(buffer: &mut [u8], edits: &[Span]) {
-    for span in edits {
-        for byte in &mut buffer[span.byte_range()] {
+pub fn apply_edits(buffer: &mut [u8], edits: &[Range<usize>]) {
+    for range in edits {
+        for byte in &mut buffer[range.clone()] {
             if *byte != b'\n' && *byte != b'\r' {
                 *byte = b' ';
             }
@@ -59,7 +66,8 @@ mod tests {
             _ => panic!("Expected function"),
         };
 
-        let edits = vec![func.sig.unsafety.unwrap().span(), func.block.span()];
+        let edits =
+            vec![func.sig.unsafety.unwrap().span().byte_range(), func.block.span().byte_range()];
 
         apply_edits(&mut buffer, &edits);
 
@@ -91,9 +99,9 @@ mod tests {
             /// ```lean
             /// theorem foo : True := by trivial
             /// ```
-                   fn foo()  
+                   fn foo() {
                           
-             
+            }
         ";
         assert_eq!(std::str::from_utf8(&buffer).unwrap(), expected);
     }

tools/hermes/tests/fixtures/complex_impl/expected_config.toml

@@ -1,4 +1,3 @@
 [[command]]
-# Expected: crate::<*constFooasT1>::m1, crate::<[Foo;5]asT3>::m3, crate::<[Foo]asT2>::m2
-args = ["--start-from", "crate::<*constFooasT1>::m1,crate::<[Foo;5]asT3>::m3,crate::<[Foo]asT2>::m2"]
+args = ["--start-from", "crate::< * const Foo as T1 >::m1,crate::< [Foo ; 5] as T3 >::m3,crate::< [Foo] as T2 >::m2"]
 should_not_exist = false

tools/hermes/tests/fixtures/complex_impl/expected_status.txt

@@ -0,0 +1 @@
+failure

tools/hermes/tests/fixtures/crlf_endings/expected/src/lib.rs

@@ -1 +1,5 @@
 fn windows() {}
+
+/// ```lean
+/// ```
+fn _hermes_dummy() {}

tools/hermes/tests/fixtures/crlf_endings/source/src/lib.rs

@@ -1 +1,5 @@
 fn windows() {}
+
+/// ```lean
+/// ```
+fn _hermes_dummy() {}

tools/hermes/tests/fixtures/custom_path_mod/source/src/lib.rs

@@ -1,3 +1,7 @@
 #[path = "sys/unix.rs"]
 mod sys;
 
+
+/// ```lean
+/// ```
+fn _hermes_dummy() {}

tools/hermes/tests/fixtures/deep_invocation/source/src/lib.rs

@@ -1,2 +1,6 @@
 pub mod nested;
 
+
+/// ```lean
+/// ```
+fn _hermes_dummy() {}

tools/hermes/tests/fixtures/dir_mod/source/src/lib.rs

@@ -1,2 +1,6 @@
 mod bar;
 
+
+/// ```lean
+/// ```
+fn _hermes_dummy() {}

tools/hermes/tests/fixtures/dirty_target_dir/expected/src/lib.rs

@@ -1,2 +1,6 @@
 fn clean() {}
 
+
+/// ```lean
+/// ```
+fn _hermes_dummy() {}