Use the beginning of the line to recover comments

charon/src/ast/gast.rs

@@ -1,14 +1,12 @@
 //! Definitions common to [crate::ullbc_ast] and [crate::llbc_ast]
 pub use super::gast_utils::*;
-use crate::expressions::*;
+use crate::ast::*;
 use crate::generate_index_type;
 use crate::ids::Vector;
 use crate::llbc_ast;
 use crate::meta::{ItemMeta, Span};
 use crate::names::Name;
-use crate::types::*;
 use crate::ullbc_ast;
-use crate::values::*;
 use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut};
 use macros::EnumIsA;
 use macros::EnumToGetters;
@@ -59,10 +57,11 @@ pub struct GExprBody<T> {
     /// - the input arguments
     /// - the remaining locals, used for the intermediate computations
     pub locals: Vector<VarId, Var>,
-    /// For each line inside the body, we record any whole-line `//` comments found before it. They
-    /// are added to statements in the late `recover_body_comments` pass.
+    /// For each line inside the body, we record any whole-line `//` comments found before it. The
+    /// `Loc` is the location of the start of the (non-comment) line. They are added to statements
+    /// in the late `recover_body_comments` pass.
     #[charon::opaque]
-    pub comments: Vec<(usize, Vec<String>)>,
+    pub comments: Vec<(Loc, Vec<String>)>,
     pub body: T,
 }
 

charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs

@@ -1255,7 +1255,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     }
 
     /// Gather all the lines that start with `//` inside the given span.
-    fn translate_body_comments(&mut self, charon_span: Span) -> Vec<(usize, Vec<String>)> {
+    fn translate_body_comments(&mut self, charon_span: Span) -> Vec<(Loc, Vec<String>)> {
         let rust_span = charon_span.rust_span();
         let source_map = self.t_ctx.tcx.sess.source_map();
         if rust_span.ctxt().is_root()
@@ -1269,12 +1269,20 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 // Compute the absolute line number
                 .map(|(i, line)| (charon_span.span.end.line - i, line))
                 // Extract the comment if this line starts with `//`
-                .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
+                .map(|(line_nbr, line)| {
+                    let trimmed = line.trim_start();
+                    // The location of the start of the line
+                    let loc = Loc {
+                        line: line_nbr,
+                        col: line.len() - trimmed.len(),
+                    };
+                    (loc, trimmed.strip_prefix("//"))
+                })
                 .peekable()
                 .batching(|iter| {
                     // Get the next line. This is not a comment: it's either the last line of the
                     // body or a line that wasn't consumed by `peeking_take_while`.
-                    let (line_nbr, _first) = iter.next()?;
+                    let (loc, _first) = iter.next()?;
                     // Collect all the comments before this line.
                     let mut comments = iter
                         // `peeking_take_while` ensures we don't consume a line that returns
@@ -1285,7 +1293,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         .map(str::to_owned)
                         .collect_vec();
                     comments.reverse();
-                    Some((line_nbr, comments))
+                    Some((loc, comments))
                 })
                 .filter(|(_, comments)| !comments.is_empty())
                 .collect_vec();

charon/src/transform/recover_body_comments.rs

@@ -16,12 +16,11 @@ impl LlbcPass for Transform {
         // - a comment should come before the statement it was applied to.
 
         // This is a pretty simple heuristic which is good enough for now.
-        let mut comments: Vec<(usize, Vec<String>)> = b.comments.clone();
+        let mut comments: Vec<(Loc, Vec<String>)> = b.comments.clone();
         b.body
             .drive_mut(&mut visitor_enter_fn_mut(|st: &mut Statement| {
-                let st_line = st.span.span.beg.line;
                 st.comments_before = comments
-                    .extract_if(|(i, _)| *i <= st_line)
+                    .extract_if(|(loc, _)| *loc == st.span.span.beg)
                     .flat_map(|(_, comments)| comments)
                     .collect();
             }));

charon/tests/ui/arrays.out

@@ -688,37 +688,37 @@ fn test_crate::take_all()
 
     x@1 := [const (0 : u32), const (0 : u32); 2 : usize]
     @fake_read(x@1)
-    // x is deep copied (copy node appears in Charon, followed by a move)
     @3 := copy (x@1)
+    // x is deep copied (copy node appears in Charon, followed by a move)
     @2 := test_crate::take_array(move (@3))
     drop @3
     drop @2
     @5 := copy (x@1)
     @4 := test_crate::take_array(move (@5))
     drop @5
     drop @4
-    // x passed by address, there is a reborrow here
     @8 := &x@1
     @7 := &*(@8)
+    // x passed by address, there is a reborrow here
     @6 := test_crate::take_array_borrow(move (@7))
     drop @7
     drop @8
     drop @6
-    // automatic cast from array to slice (spanning entire array)
     @12 := &x@1
     @11 := &*(@12)
     @10 := @ArrayToSliceShared<'_, u32, 2 : usize>(move (@11))
     drop @11
+    // automatic cast from array to slice (spanning entire array)
     @9 := test_crate::take_slice(move (@10))
     drop @10
     drop @12
     drop @9
-    // note that both appear as SliceNew expressions, meaning the SliceNew UnOp is overloaded for
-    // mut and non-mut cases
     @16 := &mut x@1
     @15 := &mut *(@16)
     @14 := @ArrayToSliceMut<'_, u32, 2 : usize>(move (@15))
     drop @15
+    // note that both appear as SliceNew expressions, meaning the SliceNew UnOp is overloaded for
+    // mut and non-mut cases
     @13 := test_crate::take_mut_slice(move (@14))
     drop @14
     drop @16
@@ -1005,14 +1005,14 @@ fn test_crate::range_all()
 
     x@1 := [const (0 : u32), const (0 : u32), const (0 : u32), const (0 : u32); 4 : usize]
     @fake_read(x@1)
-    // CONFIRM: there is no way to shrink [T;N] into [T;M] with M<N?
     @6 := &mut x@1
     @7 := core::ops::range::Range { start: const (1 : usize), end: const (3 : usize) }
     @5 := core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>}#16<u32, core::ops::range::Range<usize>, 4 : usize>[core::slice::index::{impl core::ops::index::IndexMut<I> for Slice<T>}#1<u32, core::ops::range::Range<usize>>[core::slice::index::{impl core::slice::index::SliceIndex<Slice<T>> for core::ops::range::Range<usize>}#4<u32>]]::index_mut(move (@6), move (@7))
     drop @7
     drop @6
     @4 := &mut *(@5)
     @3 := &two-phase-mut *(@4)
+    // CONFIRM: there is no way to shrink [T;N] into [T;M] with M<N?
     @2 := test_crate::update_mut_slice(move (@3))
     drop @3
     drop @5
@@ -1093,9 +1093,9 @@ fn test_crate::non_copyable_array()
     drop @3
     drop @2
     @fake_read(x@1)
+    @5 := move (x@1)
     // x is moved (not deep copied!)
     // TODO: determine whether the translation needs to be aware of that and pass by ref instead of by copy
-    @5 := move (x@1)
     @4 := test_crate::take_array_t(move (@5))
     drop @5
     drop @4

charon/tests/ui/comments.out

@@ -44,18 +44,14 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     let @25: &'_ (Slice<u32>); // anonymous local
     let @26: &'_ (u32); // anonymous local
 
-    // Comment1
     sum@2 := const (0 : u32)
     @fake_read(sum@2)
-    // Comment2
-    //  Comment2.1
-    // Comment2.2
     i@3 := const (0 : usize)
     @fake_read(i@3)
-    // Comment3
     @6 := copy (sum@2)
     @5 := move (@6) + const (2 : u32)
     drop @6
+    // Comment3
     @4 := test_crate::function_call(move (@5))
     drop @5
     drop @4
@@ -69,11 +65,11 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
         if move (@9) {
             drop @11
             drop @10
-            // Comment5
             @14 := copy (i@3)
             @25 := &*(s@1)
             @26 := @SliceIndexShared<'_, u32>(move (@25), copy (@14))
             @13 := copy (*(@26))
+            // Comment5
             sum@2 := copy (sum@2) + move (@13)
             drop @13
             drop @14
@@ -96,7 +92,6 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     drop @15
     drop @9
     drop @7
-    // Comment8
     @18 := copy (sum@2)
     @17 := move (@18) > const (10 : u32)
     if move (@17) {
@@ -112,12 +107,13 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
         @16 := copy (sum@2)
     }
     drop @17
+    // Comment8
     sum@2 := move (@16)
     drop @16
-    // Comment11
     @22 := copy (sum@2)
     @21 := move (@22) + const (2 : u32)
     drop @22
+    // Comment11
     @20 := test_crate::function_call(move (@21))
     drop @21
     drop @20
@@ -145,7 +141,6 @@ fn test_crate::thing()
     let @5: u32; // anonymous local
     let @6: (); // anonymous local
 
-    // This comment belongs above the assignment to `x` and not above intermediate computations.
     @5 := test_crate::CONSTANT
     @2 := move (@5) >> const (3 : i32)
     x@1 := move (@2) + const (12 : u32)
@@ -168,7 +163,6 @@ fn test_crate::fake_read(@1: u32)
     let x@1: u32; // arg #1
     let @2: (); // anonymous local
 
-    // This statement is translated to a `fake_read`.
     @fake_read(x@1)
     @2 := ()
     @0 := move (@2)

charon/tests/ui/no_nested_borrows.out

@@ -597,9 +597,9 @@ fn test_crate::new_pair1() -> test_crate::StructWithPair<u32, u32>
     let @0: test_crate::StructWithPair<u32, u32>; // return
     let @1: test_crate::Pair<u32, u32>; // anonymous local
 
+    @1 := test_crate::Pair { x: const (1 : u32), y: const (2 : u32) }
     // This actually doesn't make rustc generate a constant...
     // I guess it only happens for tuples.
-    @1 := test_crate::Pair { x: const (1 : u32), y: const (2 : u32) }
     @0 := test_crate::StructWithPair { p: move (@1) }
     drop @1
     return

charon/tests/ui/predicates-on-late-bound-vars.out

@@ -64,7 +64,6 @@ fn test_crate::foo()
 
     ref_b@1 := core::cell::{core::cell::RefCell<T>}#21::new<bool>(const (false))
     @fake_read(ref_b@1)
-    // `try_borrow` has a type that includes predicates on late bound regions.
     @3 := &ref_b@1
     @2 := core::cell::{core::cell::RefCell<T>}#22::try_borrow<bool>(move (@3))
     drop @3

charon/tests/ui/rvalues.out

@@ -255,7 +255,6 @@ fn test_crate::transmute(@1: Array<u32, 2 : usize>) -> u64
     let @0: u64; // return
     let x@1: Array<u32, 2 : usize>; // arg #1
 
-    // When optimized, this becomes a built-in cast. Otherwise this is just a call to `transmute`.
     @0 := transmute<Array<u32, 2 : usize>, u64>(copy (x@1))
     return
 }
@@ -284,7 +283,6 @@ fn test_crate::nullary_ops<T>() -> usize
     let offset@3: usize; // local
     let @4: usize; // anonymous local
 
-    // This one seems to be optimized out.
     size@1 := size_of<T>
     align@2 := align_of<T>
     offset@3 := offset_of(?)<test_crate::nullary_ops::Struct<T>>

charon/tests/ui/traits.out

@@ -392,11 +392,6 @@ where
     let @7: u64; // anonymous local
     let @8: &'_ (test_crate::{test_crate::TestType<T>}#6::test::TestType1); // anonymous local
 
-    // Remark: we can't write: impl TestTrait for TestType<T>,
-    // we have to use a *local* parameter (can't use the outer T).
-    // In other words: the parameters used in the items inside
-    // an impl must be bound by the impl block (can't come from outer
-    // blocks).
     @4 := move (x@2)
     x@3 := @TraitClause1::to_u64(move (@4))
     drop @4