From 0b41623249552ee7640704ff3a543b48553c70e9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 1 Oct 2024 09:22:17 +0200 Subject: [PATCH] Use the beginning of the line to recover comments --- charon/src/ast/gast.rs | 11 +++++------ .../translate/translate_functions_to_ullbc.rs | 16 ++++++++++++---- charon/src/transform/recover_body_comments.rs | 5 ++--- charon/tests/ui/arrays.out | 14 +++++++------- charon/tests/ui/comments.out | 14 ++++---------- charon/tests/ui/no_nested_borrows.out | 2 +- .../tests/ui/predicates-on-late-bound-vars.out | 1 - charon/tests/ui/rvalues.out | 2 -- charon/tests/ui/traits.out | 5 ----- 9 files changed, 31 insertions(+), 39 deletions(-) diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 7812c4ff6..a630badfb 100644 --- a/charon/src/ast/gast.rs +++ b/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 { /// - the input arguments /// - the remaining locals, used for the intermediate computations pub locals: Vector, - /// 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)>, + pub comments: Vec<(Loc, Vec)>, pub body: T, } diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index eb33526dd..37eed13fc 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/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)> { + fn translate_body_comments(&mut self, charon_span: Span) -> Vec<(Loc, Vec)> { 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(); diff --git a/charon/src/transform/recover_body_comments.rs b/charon/src/transform/recover_body_comments.rs index b34d3870e..f4395a98f 100644 --- a/charon/src/transform/recover_body_comments.rs +++ b/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)> = b.comments.clone(); + let mut comments: Vec<(Loc, Vec)> = 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(); })); diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 3f185272e..2f2aea267 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -688,8 +688,8 @@ 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 @@ -697,28 +697,28 @@ fn test_crate::take_all() @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,7 +1005,6 @@ 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 for Array}#16, 4 : usize>[core::slice::index::{impl core::ops::index::IndexMut for Slice}#1>[core::slice::index::{impl core::slice::index::SliceIndex> for core::ops::range::Range}#4]]::index_mut(move (@6), move (@7)) @@ -1013,6 +1012,7 @@ fn test_crate::range_all() drop @6 @4 := &mut *(@5) @3 := &two-phase-mut *(@4) + // CONFIRM: there is no way to shrink [T;N] into [T;M] with M(@1: &'_0 (Slice)) -> u32 let @25: &'_ (Slice); // 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 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 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 @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) diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out index 2a4bc0df9..4c8148df0 100644 --- a/charon/tests/ui/no_nested_borrows.out +++ b/charon/tests/ui/no_nested_borrows.out @@ -597,9 +597,9 @@ fn test_crate::new_pair1() -> test_crate::StructWithPair let @0: test_crate::StructWithPair; // return let @1: test_crate::Pair; // 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 diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index 3c1e7111d..e333447d2 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/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}#21::new(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}#22::try_borrow(move (@3)) drop @3 diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index 4f4cd897b..2b70355b8 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -255,7 +255,6 @@ fn test_crate::transmute(@1: Array) -> u64 let @0: u64; // return let x@1: Array; // arg #1 - // When optimized, this becomes a built-in cast. Otherwise this is just a call to `transmute`. @0 := transmute, u64>(copy (x@1)) return } @@ -284,7 +283,6 @@ fn test_crate::nullary_ops() -> usize let offset@3: usize; // local let @4: usize; // anonymous local - // This one seems to be optimized out. size@1 := size_of align@2 := align_of offset@3 := offset_of(?)> diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 1154783a6..c48c52b5d 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -392,11 +392,6 @@ where let @7: u64; // anonymous local let @8: &'_ (test_crate::{test_crate::TestType}#6::test::TestType1); // anonymous local - // Remark: we can't write: impl TestTrait for TestType, - // 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