From ea2cf1a3b6a7b8343d40fcb96a6ff0ed6c8d5d4b Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Sun, 24 Dec 2023 19:11:54 -0500
Subject: [PATCH] Add more nuance for prefix_expr w.r.t. when it can/cannot
 have structs

---
 examples/wip.rs            | 9 ++-------
 src/lib.rs                 | 3 ++-
 src/verus.pest             | 7 ++++++-
 tests/verus-consistency.rs | 7 +++++++
 4 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index 1d7d2ed..98b70f9 100644
--- a/examples/wip.rs
+++ b/examples/wip.rs
@@ -1,12 +1,7 @@
 verus! {
 
-fn has_new_pointsto() {
-    (forall |addr: int| mem_protect == MemProtect { read: true })
-}
-
-fn foo()
-    ensures forall|x:int| x == x
-{
+fn local_direct_update(loc1: Local, loc2: Local, i: int, j: int, pq: int) -> bool {
+    &&& loc2 == Local { heap: loc2.heap, ..loc1 }
 }
 
 } // verus!
diff --git a/src/lib.rs b/src/lib.rs
index b1be61a..3c37872 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -388,7 +388,7 @@ fn is_prefix_triple(pair: Pair<Rule>) -> bool {
     match pair.into_inner().find(|p| matches!(p.as_rule(), Rule::expr_inner)) {
         None => false,
         Some(pair) => 
-            match pair.into_inner().find(|p| matches!(p.as_rule(), Rule::prefix_expr)) {
+            match pair.into_inner().find(|p| matches!(p.as_rule(), Rule::prefix_expr) || matches!(p.as_rule(), Rule::prefix_expr_no_struct)) {
                 None => false,
                 Some(pair) => 
                     pair.into_inner().find(|p| matches!(p.as_rule(), Rule::triple_and) || matches!(p.as_rule(), Rule::triple_or)).is_some(),
@@ -841,6 +841,7 @@ fn to_doc<'a>(
             block_braces(arena, mapped, terminal_expr(&pairs))
         }
         Rule::prefix_expr => map_to_doc(ctx, arena, pair),
+        Rule::prefix_expr_no_struct => map_to_doc(ctx, arena, pair),
         Rule::assignment_ops => docs![arena, arena.space(), s, arena.line()],
         Rule::bin_expr_ops_special => arena.hardline().append(map_to_doc(ctx, arena, pair)),
         Rule::bin_expr_ops_normal => docs![arena, arena.line(), s, arena.space()]
diff --git a/src/verus.pest b/src/verus.pest
index c328934..1577de5 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -873,7 +873,7 @@ expr_inner_no_struct = _{
   | block_expr
   | box_expr
   | break_expr
-  | prefix_expr
+  | prefix_expr_no_struct
   | closure_expr
   | quantifier_expr_no_struct
   | continue_expr
@@ -969,6 +969,7 @@ expr_inner = {
     if_expr  // Must precede struct_expr or struct_expr thinks `if {}` is a struct
   | struct_expr // Must precede expr_inner_no_struct or `my_struct { }` will be `my_struct`: path_expr
   | quantifier_expr
+  | prefix_expr
   | expr_inner_no_struct
 }
 
@@ -1036,6 +1037,10 @@ fn_block_expr = {
 }
 
 prefix_expr = {
+    attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr
+}
+
+prefix_expr_no_struct = {
     attr* ~ (dash_str | bang_str | star_str | triple_or | triple_and) ~ expr_no_struct
 }
 
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index 459b5d5..87bea53 100644
--- a/tests/verus-consistency.rs
+++ b/tests/verus-consistency.rs
@@ -471,6 +471,9 @@ spec fn host_ignoring_unparseable(pre: AbstractHostState, post: AbstractHostStat
     post == AbstractHostState { received_packet: None, ..pre }
 }
 
+fn local_direct_update(loc1: Local, pq: int) -> bool {
+    &&& loc2 == Local { heap: loc2.heap, ..loc1 }
+}
 
 } // verus!
 "#;
@@ -482,6 +485,10 @@ spec fn host_ignoring_unparseable(pre: AbstractHostState, post: AbstractHostStat
         post == AbstractHostState { received_packet: None, ..pre }
     }
 
+    fn local_direct_update(loc1: Local, pq: int) -> bool {
+        &&& loc2 == Local { heap: loc2.heap, ..loc1 }
+    }
+
     } // verus!
     "###);
 }