support no_unwind clause

verus-lang · Apr 9, 2024 · bd492fd · bd492fd
1 parent 90f21b0
commit bd492fd
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 1 deletion.
diff --git a/src/lib.rs b/src/lib.rs
@@ -771,8 +771,11 @@ fn to_doc<'a>(
         | Rule::invariant_ensures_str
         | Rule::opens_invariants_str
         | Rule::recommends_str
+        | Rule::no_unwind_str
         | Rule::requires_str => arena.hardline().append(s).nest(INDENT_SPACES),
 
+        Rule::no_unwind_when_str => arena.space().append(s).append(arena.space()),
+
         Rule::any_str
         | Rule::assert_str
         | Rule::assume_str
@@ -1275,6 +1278,7 @@ fn to_doc<'a>(
         Rule::invariant_ensures_clause => map_to_doc(ctx, arena, pair),
         Rule::recommends_clause => map_to_doc(ctx, arena, pair),
         Rule::decreases_clause => map_to_doc(ctx, arena, pair),
+        Rule::unwind_clause => map_to_doc(ctx, arena, pair),
         Rule::opens_invariants_mode => arena.space().append(map_to_doc(ctx, arena, pair)),
         Rule::opens_invariants_clause => map_to_doc(ctx, arena, pair),
         Rule::assert_requires => map_to_doc(ctx, arena, pair).append(arena.line()),

diff --git a/src/verus.pest b/src/verus.pest
@@ -296,6 +296,8 @@ move_str = ${ "move" ~ !("_" | ASCII_ALPHANUMERIC) }
 mut_str = ${ "mut" ~ !("_" | ASCII_ALPHANUMERIC) }
 nat_str = ${ "nat" ~ !("_" | ASCII_ALPHANUMERIC) }
 none_str = ${ "none" ~ !("_" | ASCII_ALPHANUMERIC) }
+no_unwind_str = ${ "no_unwind" ~ !("_" | ASCII_ALPHANUMERIC) }
+no_unwind_when_str = ${ "when" ~ !("_" | ASCII_ALPHANUMERIC) }
 opens_invariants_str = ${ "opens_invariants" ~ !("_" | ASCII_ALPHANUMERIC) }
 open_str = ${ "open" ~ !("_" | ASCII_ALPHANUMERIC) }
 proof_space_str = ${ "proof" ~ !("_" | ASCII_ALPHANUMERIC) }
@@ -652,7 +654,7 @@ use_tree_list = {
 }
 
 fn_qualifier = {
-    (requires_clause | recommends_clause | ensures_clause | decreases_clause | opens_invariants_clause)*
+    (requires_clause | recommends_clause | ensures_clause | decreases_clause | opens_invariants_clause | unwind_clause)*
 }
 
 fn_terminator = {
@@ -1691,6 +1693,10 @@ decreases_clause = {
     decreases_str ~ groupable_comma_delimited_exprs_for_verus_clauses ~ (when_str ~ expr_no_struct)? ~ (via_str ~ expr_no_struct)?
 }
 
+unwind_clause = {
+    no_unwind_str ~ (no_unwind_when_str ~ expr_no_struct)?
+}
+
 opens_invariants_mode = {
     any_str
   | none_str

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -2062,3 +2062,35 @@ proof fn to_multiset_build<A>(s: Seq<A>, a: A)
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_unwind() {
+    let file = r###"
+verus! {
+proof fn a()
+    no_unwind
+{
+}
+
+proof fn b()
+    no_unwind when x >= 0
+{
+}
+} // verus!
+"###;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    proof fn a()
+        no_unwind
+    {
+    }
+
+    proof fn b()
+        no_unwind when x >= 0
+    {
+    }
+
+    } // verus!
+    "###);
+}