Merge pull request #359 from Nadrieril/fix-spans

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

@@ -688,18 +688,18 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         source_info: &hax::SourceInfo,
     ) -> Span {
         // Translate the span
-        let mut scope_data = source_scopes.get(source_info.scope).unwrap();
-        let span = self.translate_raw_span(scope_data.span.clone());
+        let span = self.translate_raw_span(source_info.span.clone());
 
         // Lookup the top-most inlined parent scope.
-        if scope_data.inlined_parent_scope.is_some() {
-            while scope_data.inlined_parent_scope.is_some() {
-                let parent_scope = scope_data.inlined_parent_scope.unwrap();
-                scope_data = source_scopes.get(parent_scope).unwrap();
-            }
-
-            let parent_span = self.translate_raw_span(scope_data.span.clone());
+        let mut parent_span = None;
+        let mut scope_data = &source_scopes[source_info.scope];
+        while let Some(parent_scope) = scope_data.inlined_parent_scope {
+            scope_data = &source_scopes[parent_scope];
+            parent_span = Some(&scope_data.span);
+        }
 
+        if let Some(parent_span) = parent_span {
+            let parent_span = self.translate_raw_span(parent_span.clone());
             Span {
                 span: parent_span,
                 generated_from_span: Some(span),

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

@@ -906,10 +906,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         let t_statement: Option<RawStatement> = match &*statement.kind {
             StatementKind::Assign((place, rvalue)) => {
                 let t_place = self.translate_place(span, place)?;
-                let t_rvalue = self.translate_rvalue(
-                    statement.source_info.span.rust_span_data.unwrap().span(),
-                    rvalue,
-                )?;
+                let t_rvalue = self.translate_rvalue(span, rvalue)?;
 
                 Some(RawStatement::Assign(t_place, t_rvalue))
             }

charon/src/transform/recover_body_comments.rs

@@ -14,9 +14,8 @@ impl LlbcPass for Transform {
         // - each comment should be assigned to exactly one statement;
         // - the order of comments in the source should refine the partial order of control flow;
         // - a comment should come before the statement it was applied to.
-        // Statement spans are way too imprecise for that.
 
-        // This is a pretty terrible heuristic but the spans are really terrible.
+        // This is a pretty simple heuristic which is good enough for now.
         let mut comments: Vec<(usize, Vec<String>)> = b.comments.clone();
         b.body
             .drive_mut(&mut visitor_enter_fn_mut(|st: &mut Statement| {

charon/tests/cargo/workspace.out

@@ -13,6 +13,7 @@ fn crate2::extra_random_number() -> u32
     let @0: u32; // return
     let @1: u32; // anonymous local
 
+    // Even more random.
     @1 := crate1::random_number()
     @0 := move (@1) + const (1 : u32)
     drop @1

charon/tests/crate_data.rs

@@ -1,9 +1,6 @@
 use charon_lib::ast::{AnyTransItem, TranslatedCrate};
-use derive_visitor::{visitor_enter_fn, Drive};
-use indoc::indoc;
 use itertools::Itertools;
-use llbc_ast::Statement;
-use std::collections::{HashMap, HashSet};
+use std::collections::HashMap;
 
 use charon_lib::ast::*;
 
@@ -133,84 +130,19 @@ fn spans() -> anyhow::Result<()> {
     let function = &crate_data.fun_decls[0];
     // Span of the whole function.
     assert_eq!(repr_span(function.item_meta.span), "2:8-10:9");
+
     let body_id = function.body.unwrap();
     let body = &crate_data.bodies[body_id].as_structured().unwrap().body;
-    // The whole function declaration.
-    assert_eq!(repr_span(body.span), "2:8-10:9");
+    // Span of the function body
+    assert_eq!(repr_span(body.span), "3:16-10:9");
+
     let the_loop = body
         .statements
         .iter()
         .find(|st| st.content.is_loop())
         .unwrap();
-    // That's not a very precise span :/
-    assert_eq!(repr_span(the_loop.span), "4:12-10:9");
-    Ok(())
-}
-
-#[test]
-fn comments() -> anyhow::Result<()> {
-    let crate_data = translate(
-        "
-        pub fn sum(s: &[u32]) -> u32 {
-            // Comment1
-            let mut sum = 0;
-            // Comment2
-            let mut i = 0;
-            // Comment3
-            while i < s.len() {
-                // Comment4
-                sum += s[i];
-                // Comment5
-                i += 1;
-            }
-            // Comment6
-            sum = if sum > 10 {
-                // Comment7
-                sum + 100
-            } else {
-                // Comment8
-                sum
-            };
-            // Comment9
-            sum
-        }
-        ",
-    )?;
-    let function = &crate_data.fun_decls[0];
-    let body_id = function.body.unwrap();
-    let body = &crate_data.bodies[body_id].as_structured().unwrap();
-    assert_eq!(function.item_meta.span.span.beg.line, 2);
-
-    let mut statement_lines = HashSet::new();
-    body.body.drive(&mut visitor_enter_fn(|st: &Statement| {
-        statement_lines.insert(st.span.span.beg.line);
-    }));
-    // This is terrible, we only distinguish three lines out of so many.
-    assert_eq!(
-        statement_lines.into_iter().sorted().collect_vec(),
-        vec![2, 4, 6]
-    );
+    assert_eq!(repr_span(the_loop.span), "5:12-8:13");
 
-    let comments = body
-        .comments
-        .iter()
-        .map(|(i, comments)| format!("{i}: {comments:?}"))
-        .join("\n");
-    assert_eq!(
-        comments,
-        indoc!(
-            r#"
-            4: ["Comment1"]
-            6: ["Comment2"]
-            8: ["Comment3"]
-            10: ["Comment4"]
-            12: ["Comment5"]
-            15: ["Comment6"]
-            17: ["Comment7"]
-            20: ["Comment8"]
-            23: ["Comment9"]"#
-        )
-    );
     Ok(())
 }
 

charon/tests/ui/arrays.out

@@ -688,6 +688,7 @@ 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)
     @2 := test_crate::take_array(move (@3))
     drop @3
@@ -696,12 +697,14 @@ 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)
     @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))
@@ -710,6 +713,8 @@ fn test_crate::take_all()
     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))
@@ -1000,6 +1005,7 @@ 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))
@@ -1087,12 +1093,16 @@ fn test_crate::non_copyable_array()
     drop @3
     drop @2
     @fake_read(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
     @6 := ()
     @0 := move (@6)
+    // this fails, naturally:
+    // take_array_t(x);
     drop x@1
     @0 := ()
     return

charon/tests/ui/comments.out

@@ -26,12 +26,13 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     let @19: &'_ (Slice<u32>); // anonymous local
     let @20: &'_ (u32); // anonymous local
 
+    // Comment1
     sum@2 := const (0 : u32)
     @fake_read(sum@2)
-    // Comment1
+    // Comment2
     i@3 := const (0 : usize)
     @fake_read(i@3)
-    // Comment2
+    // Comment3
     loop {
         @7 := copy (i@3)
         @9 := &*(s@1)
@@ -41,13 +42,15 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
         if move (@6) {
             drop @8
             drop @7
+            // Comment4
             @11 := copy (i@3)
             @19 := &*(s@1)
             @20 := @SliceIndexShared<'_, u32>(move (@19), copy (@11))
             @10 := copy (*(@20))
             sum@2 := copy (sum@2) + move (@10)
             drop @10
             drop @11
+            // Comment5
             i@3 := copy (i@3) + const (1 : usize)
             @17 := ()
             @5 := move (@17)
@@ -65,21 +68,25 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     drop @12
     drop @6
     drop @4
+    // Comment6
     @15 := copy (sum@2)
     @14 := move (@15) > const (10 : u32)
     if move (@14) {
         drop @15
+        // Comment7
         @16 := copy (sum@2)
         @13 := move (@16) + const (100 : u32)
         drop @16
     }
     else {
         drop @15
+        // Comment8
         @13 := copy (sum@2)
     }
     drop @14
     sum@2 := move (@13)
     drop @13
+    // Comment9
     @0 := copy (sum@2)
     drop i@3
     drop sum@2

charon/tests/ui/loops.out

@@ -528,6 +528,7 @@ fn test_crate::test_loop6(@1: u32) -> u32
     }
     drop @6
     drop @4
+    // All the below nodes are exit candidates (each of them is referenced twice)
     s@3 := copy (s@3) + const (1 : u32)
     @0 := copy (s@3)
     drop s@3

charon/tests/ui/no_nested_borrows.out

@@ -597,6 +597,8 @@ 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
 
+    // 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

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

@@ -64,6 +64,7 @@ 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,6 +255,7 @@ 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
 }

charon/tests/ui/traits.out

@@ -392,15 +392,15 @@ where
     let @7: u64; // anonymous local
     let @8: &'_ (test_crate::{test_crate::TestType<T>}#6::test::TestType1); // anonymous local
 
-    @4 := move (x@2)
-    x@3 := @TraitClause1::to_u64(move (@4))
-    drop @4
-    @fake_read(x@3)
     // 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
+    @fake_read(x@3)
     y@5 := test_crate::{test_crate::TestType<T>}#6::test::TestType1 { 0: const (0 : u64) }
     @fake_read(y@5)
     @7 := copy (x@3)