fix spans for binary ops

while preserving the safety of parenthesizing incoming LHS/RHS
viperproject · Jan 7, 2023 · b0db31e · b0db31e
1 parent 0916b01
commit b0db31e
Show file tree

Hide file tree

Showing 12 changed files with 116 additions and 92 deletions.
diff --git a/prusti-contracts/prusti-specs/src/specifications/preparser.rs b/prusti-contracts/prusti-specs/src/specifications/preparser.rs
@@ -878,20 +878,25 @@ impl PrustiBinaryOp {
         }
     }
 
-    fn translate(&self, span: Span, lhs: TokenStream, rhs: TokenStream) -> TokenStream {
+    fn translate(&self, span: Span, raw_lhs: TokenStream, raw_rhs: TokenStream) -> TokenStream {
+        let lhs = quote_spanned! { raw_lhs.span() => (#raw_lhs) };
+        let rhs = quote_spanned! { raw_rhs.span() => (#raw_rhs) };
         match self {
-            Self::Rust(op) => op.translate(span, lhs, rhs),
+            Self::Rust(op) => op.translate(span, raw_lhs, raw_rhs),
             // implication is desugared into this form to avoid evaluation
             // order issues: `f(a, b)` makes Rust evaluate both `a` and `b`
             // before the `f` call
             Self::Implies => {
                 // preserve span of LHS
-                let not_lhs = quote_spanned! { lhs.span() => !(#lhs) };
-                quote_spanned! { span => (#not_lhs || (#rhs)) }
+                let not_lhs = quote_spanned! { lhs.span() => !#lhs };
+                quote_spanned! { span => #not_lhs || #rhs }
+            }
+            Self::Or => quote_spanned! { span => #lhs || #rhs },
+            Self::And => quote_spanned! { span => #lhs && #rhs },
+            Self::SnapEq => {
+                let joined_span = join_spans(lhs.span(), rhs.span());
+                quote_spanned! { joined_span => snapshot_equality(&#lhs, &#rhs) }
             }
-            Self::Or => quote_spanned! { span => (#lhs) || (#rhs) },
-            Self::And => quote_spanned! { span => (#lhs) && (#rhs) },
-            Self::SnapEq => quote_spanned! { span => snapshot_equality(&(#lhs), &(#rhs)) },
         }
     }
 }

diff --git a/prusti-tests/tests/parse/ui/composite.stdout b/prusti-tests/tests/parse/ui/composite.stdout
@@ -42,7 +42,7 @@ use prusti_contracts::*;
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test1_$(NUM_UUID)() -> bool {
-    !!(((!((true) && (true)) || ((true) && (true)))): bool)
+    !!((!((true) && (true)) || ((true) && (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -51,7 +51,7 @@ fn test1() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
-    !!(((((true) && (((!(true) || (true))))) && (((true) || (true)))) &&
+    !!(((((true) && ((!(true) || (true)))) && (((true) || (true)))) &&
                             (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
@@ -61,7 +61,7 @@ fn test2() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
-    !!(((!(((true) && (true))) || (true))): bool)
+    !!((!(((true) && (true))) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -70,7 +70,7 @@ fn test3() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test4_$(NUM_UUID)() -> bool {
-    !!(((!((((!(true) || (true)))) && (true)) || (true))): bool)
+    !!((!(((!(true) || (true))) && (true)) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -79,8 +79,8 @@ fn test4() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
-    !!(((((!(true) || (true)))) &&
-                            (((!(true) || ((true) && (((true) || (true)))))))): bool)
+    !!((((!(true) || (true))) &&
+                            ((!(true) || ((true) && (((true) || (true))))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -89,8 +89,8 @@ fn test5() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test6_$(NUM_UUID)() -> bool {
-    !!(((!(((true) && (true))) ||
-                                ((!(true) || ((!(true) || ((!(true) || (true))))))))): bool)
+    !!((!(((true) && (true))) ||
+                            (!(true) || (!(true) || (!(true) || (true))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -99,8 +99,8 @@ fn test6() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test7_$(NUM_UUID)() -> bool {
-    !!(((!(((true) && (true))) ||
-                                ((!(((true) && (true))) || (((true) && (true))))))): bool)
+    !!((!(((true) && (true))) ||
+                            (!(((true) && (true))) || (((true) && (true))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -109,7 +109,7 @@ fn test7() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test8_$(NUM_UUID)() -> bool {
-    !!(((!(((true) || (true))) || (((true) || (true))))): bool)
+    !!((!(((true) || (true))) || (((true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -118,8 +118,8 @@ fn test8() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test9_$(NUM_UUID)() -> bool {
-    !!(((!(((true) || (true))) ||
-                                (((true) || (((true) && (((true) || (true))))))))): bool)
+    !!((!(((true) || (true))) ||
+                            (((true) || (((true) && (((true) || (true)))))))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -151,10 +151,10 @@ fn test12() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test13_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                ((!(forall((),
-                                                        #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                                            { ((a == 5): bool) })) || (true))))): bool)
+    !!((!(true) ||
+                            (!(forall((),
+                                                #[prusti::spec_only] |a: i32, b: i32| -> bool
+                                                    { ((a == 5): bool) })) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -163,10 +163,10 @@ fn test13() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test14_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                (forall((),
-                                        #[prusti::spec_only] |a: i32| -> bool
-                                            { ((a == 5): bool) })))): bool)
+    !!((!(true) ||
+                            (forall((),
+                                    #[prusti::spec_only] |a: i32| -> bool
+                                        { ((a == 5): bool) }))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -175,9 +175,9 @@ fn test14() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test15_$(NUM_UUID)() -> bool {
-    !!(((!(forall((),
-                                            #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
-                                || (true))): bool)
+    !!((!(forall((),
+                                        #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
+                            || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -186,13 +186,13 @@ fn test15() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test16_$(NUM_UUID)() -> bool {
-    !!(((!(forall((),
-                                            #[prusti::spec_only] |b: i32| -> bool
-                                                { ((b == 10): bool) })) ||
-                                ((!(true) ||
-                                            (forall((),
-                                                    #[prusti::spec_only] |a: u32, b: u32| -> bool
-                                                        { ((a == 5): bool) })))))): bool)
+    !!((!(forall((),
+                                        #[prusti::spec_only] |b: i32| -> bool
+                                            { ((b == 10): bool) })) ||
+                            (!(true) ||
+                                    (forall((),
+                                            #[prusti::spec_only] |a: u32, b: u32| -> bool
+                                                { ((a == 5): bool) })))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -224,10 +224,10 @@ fn test19() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test20_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                ((!(exists((),
-                                                        #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                                            { ((a == 5): bool) })) || (true))))): bool)
+    !!((!(true) ||
+                            (!(exists((),
+                                                #[prusti::spec_only] |a: i32, b: i32| -> bool
+                                                    { ((a == 5): bool) })) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -236,10 +236,10 @@ fn test20() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test21_$(NUM_UUID)() -> bool {
-    !!(((!(true) ||
-                                (exists((),
-                                        #[prusti::spec_only] |a: i32| -> bool
-                                            { ((a == 5): bool) })))): bool)
+    !!((!(true) ||
+                            (exists((),
+                                    #[prusti::spec_only] |a: i32| -> bool
+                                        { ((a == 5): bool) }))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -248,9 +248,9 @@ fn test21() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test22_$(NUM_UUID)() -> bool {
-    !!(((!(exists((),
-                                            #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
-                                || (true))): bool)
+    !!((!(exists((),
+                                        #[prusti::spec_only] |a: i32| -> bool { ((a == 5): bool) }))
+                            || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -259,13 +259,13 @@ fn test22() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test23_$(NUM_UUID)() -> bool {
-    !!(((!(exists((),
-                                            #[prusti::spec_only] |b: i32| -> bool
-                                                { ((b == 10): bool) })) ||
-                                ((!(true) ||
-                                            (exists((),
-                                                    #[prusti::spec_only] |a: u32, b: u32| -> bool
-                                                        { ((a == 5): bool) })))))): bool)
+    !!((!(exists((),
+                                        #[prusti::spec_only] |b: i32| -> bool
+                                            { ((b == 10): bool) })) ||
+                            (!(true) ||
+                                    (exists((),
+                                            #[prusti::spec_only] |a: u32, b: u32| -> bool
+                                                { ((a == 5): bool) })))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]

diff --git a/prusti-tests/tests/parse/ui/exists.stdout b/prusti-tests/tests/parse/ui/exists.stdout
@@ -50,8 +50,7 @@ fn test2() {}
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
     !!((exists((),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -92,8 +91,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool {
                                     #[prusti::spec_only] |a: i32, b: i32| (2)),
                                 (#[prusti::spec_only] |a: i32, b: i32| (1),)),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]

diff --git a/prusti-tests/tests/parse/ui/forall.stdout b/prusti-tests/tests/parse/ui/forall.stdout
@@ -50,8 +50,7 @@ fn test2() {}
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
     !!((forall((),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -92,8 +91,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool {
                                     #[prusti::spec_only] |a: i32, b: i32| (2)),
                                 (#[prusti::spec_only] |a: i32, b: i32| (1),)),
                             #[prusti::spec_only] |a: i32, b: i32| -> bool
-                                { (((!(a + b == a + b) || (a + b == a + b))): bool) })):
-                    bool)
+                                { ((!(a + b == a + b) || (a + b == a + b)): bool) })): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]

diff --git a/prusti-tests/tests/parse/ui/implies.stdout b/prusti-tests/tests/parse/ui/implies.stdout
@@ -28,7 +28,7 @@ use prusti_contracts::*;
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test1_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (true))): bool)
+    !!((!(true) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -37,7 +37,7 @@ fn test1() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test2_$(NUM_UUID)() -> bool {
-    !!(((!(true) || ((!(true) || (true))))): bool)
+    !!((!(true) || (!(true) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -46,7 +46,7 @@ fn test2() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test3_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (((!(true) || (true)))))): bool)
+    !!((!(true) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -55,7 +55,7 @@ fn test3() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test4_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (true))): bool)
+    !!((!((!(true) || (true))) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -64,7 +64,7 @@ fn test4() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (((!(true) || (true)))))): bool)
+    !!((!((!(true) || (true))) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -73,7 +73,7 @@ fn test5() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test21_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (true))): bool)
+    !!((!(true) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -82,7 +82,7 @@ fn test21() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test22_$(NUM_UUID)() -> bool {
-    !!(((!(true) || ((!(true) || (true))))): bool)
+    !!((!(true) || (!(true) || (true))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -91,7 +91,7 @@ fn test22() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test23_$(NUM_UUID)() -> bool {
-    !!(((!(true) || (((!(true) || (true)))))): bool)
+    !!((!(true) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -100,7 +100,7 @@ fn test23() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test24_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (true))): bool)
+    !!((!((!(true) || (true))) || (true)): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]
@@ -109,7 +109,7 @@ fn test24() {}
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 fn prusti_pre_item_test25_$(NUM_UUID)() -> bool {
-    !!(((!(((!(true) || (true)))) || (((!(true) || (true)))))): bool)
+    !!((!((!(true) || (true))) || ((!(true) || (true)))): bool)
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 #[prusti::specs_version = $(SPECS_VERSION)]

diff --git a/prusti-tests/tests/parse/ui/predicates.stdout b/prusti-tests/tests/parse/ui/predicates.stdout
@@ -79,7 +79,7 @@ fn prusti_pred_item_forall_implication_$(NUM_UUID)()
     -> bool {
     !!((forall((),
                             #[prusti::spec_only] |x: usize| -> bool
-                                { (((!((x != 0)) || (x * 2 != 0))): bool) })): bool)
+                                { ((!((x != 0)) || (x * 2 != 0)): bool) })): bool)
 }
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]
@@ -96,7 +96,7 @@ fn prusti_pred_item_exists_implication_$(NUM_UUID)()
     -> bool {
     !!((exists((),
                             #[prusti::spec_only] |x: usize| -> bool
-                                { (((!((x != 0)) || (x * 2 != 0))): bool) })): bool)
+                                { ((!((x != 0)) || (x * 2 != 0)): bool) })): bool)
 }
 #[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::pred_spec_id_ref = "$(NUM_UUID)"]