From 69f79105fedceafd2f422872575830570b452799 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 23 Sep 2024 15:38:31 -0700 Subject: [PATCH 1/4] Support parsing for const generic literals --- CHANGELOG.md | 2 ++ src/verus.pest | 8 +++++++- tests/verus-consistency.rs | 30 ++++++++++++++++++++++++++++++ 3 files changed, 39 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8dae773..3813aef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ # Unreleased +* Support parsing for const generic literals + # v0.4.1 * Minor fix to prevent panic on formatting files containing unbalanced parentheses in strings/chars/... diff --git a/src/verus.pest b/src/verus.pest index 04e3284..7a13d7c 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -485,7 +485,13 @@ lifetime_arg = { } const_arg = { - expr + // Currently stable Rust only support literals as const args inside generic + // args. In general, it could be arbitrary expressions, but that causes + // headaches for parsing (in particular, we need to parse an `expr` that + // does _not_ have a `>` sign in it, but our `expr` parsing greedily eats + // any `>` that exists within it. Thus, for now, we simply restrict to + // literals. + literal } generic_args_binding = { diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index a82ad24..809baf0 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -2473,3 +2473,33 @@ fn fff() { } // verus! "###); } + +#[test] +fn verus_const_generics() { + // Regression test for https://github.com/verus-lang/verusfmt/issues/90 + let file = r#" +verus! { + pub fn f() -> u64 { N } + pub fn g() -> u64 { N } + fn main() { f::<123>(); g::<123, 456>(); } +} +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + pub fn f() -> u64 { + N + } + + pub fn g() -> u64 { + N + } + + fn main() { + f::<123>(); + g::<123, 456>(); + } + + } // verus! + "###); +} From 0ef7f8debab0244232146ac3dc19c988df241c4b Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Mon, 23 Sep 2024 16:06:46 -0700 Subject: [PATCH 2/4] Support `opens_invariants` with concrete sets --- CHANGELOG.md | 2 ++ src/verus.pest | 1 + tests/verus-consistency.rs | 38 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 41 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8dae773..caba544 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ # Unreleased +* Support parsing `opens_invariants` with specific concrete sets + # v0.4.1 * Minor fix to prevent panic on formatting files containing unbalanced parentheses in strings/chars/... diff --git a/src/verus.pest b/src/verus.pest index 04e3284..24b5fe0 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -1750,6 +1750,7 @@ unwind_clause = { opens_invariants_mode = { any_str | none_str + | lbracket_str ~ comma_delimited_exprs? ~ rbracket_str } opens_invariants_clause = { diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index a82ad24..eaedf1c 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -2473,3 +2473,41 @@ fn fff() { } // verus! "###); } + +#[test] +fn verus_support_opens_invariants() { + // Regression test for https://github.com/verus-lang/verusfmt/issues/91 + let file = r#" +verus! { + proof fn a() opens_invariants none {} + proof fn f() opens_invariants [ 123u8 ] {} + proof fn g() opens_invariants [ 123u8, 456u8 ] {} + proof fn z() opens_invariants any {} +} +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + proof fn a() + opens_invariants none + { + } + + proof fn f() + opens_invariants [123u8] + { + } + + proof fn g() + opens_invariants [123u8, 456u8] + { + } + + proof fn z() + opens_invariants any + { + } + + } // verus! + "###) +} From 56668599fb70fe8d6c335d5d5084b5e849733ce5 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Fri, 20 Sep 2024 15:06:43 -0700 Subject: [PATCH 3/4] Improve debugging experience --- src/lib.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 7f5e9b7..5ea07e1 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -562,8 +562,18 @@ fn terminal_expr(pairs: &Pairs) -> bool { } fn debug_print(pair: Pair, indent: usize) { - print!("{:indent$}{:?} {{", "", pair.as_rule(), indent = indent); - let pairs = pair.into_inner(); + if pair.as_rule() == Rule::COMMENT { + print!( + "{:indent$}{:?} {{ {comment:?} ", + "", + pair.as_rule(), + indent = indent, + comment = pair.as_str() + ); + } else { + print!("{:indent$}{:?} {{", "", pair.as_rule(), indent = indent); + } + let pairs = pair.clone().into_inner(); if pairs.peek().is_some() { println!(); pairs.for_each(|p| debug_print(p, indent + 2)); From dec44e7f6c6867c06eff192147071fbb12909bee Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Fri, 20 Sep 2024 15:07:25 -0700 Subject: [PATCH 4/4] Improve handling of separated clauses Specifically, in the presence of comments around `expr_with_block` cases (such as `assert ... by { ... }` blocks) that don't necessarily have a semicolon, the previous version would end up reorganizing the affinity of the comments across the clauses, preferring the previous clause. With this commit, each comments stays loyal to its own clause. --- CHANGELOG.md | 3 ++ src/verus.pest | 6 +++- tests/verus-consistency.rs | 60 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 68 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8dae773..a5f9fe9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Unreleased +* Improved handling of comments around clauses/stanzas + - Each comment now maintains loyalty to the clause the user picked it to stay with, rather than automatically migrating to the previous clause in the presence of `assert ... by { ... }`-style constructs + # v0.4.1 * Minor fix to prevent panic on formatting files containing unbalanced parentheses in strings/chars/... diff --git a/src/verus.pest b/src/verus.pest index 04e3284..6a223b8 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -988,7 +988,11 @@ stmt = !{ | proof_block | let_stmt | assignment_stmt - | expr_with_block ~ semi_str? + // We can't use `expr_with_block ~ semi_str?` here, and instead need to do it + // as the two separate ordered alternatives (`ewb ~ semi_str | ewb`) to + // prevent munching of multi-newlines that happens otherwise + | expr_with_block ~ semi_str + | expr_with_block | expr ~ semi_str | item_no_macro_call | macro_call_stmt diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index a82ad24..8cc1585 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -2453,6 +2453,36 @@ fn fff() { baz; } +pub fn foo() { + // this should stay stuck to the `a` + assert(a) by { + // whatever + } + // this should also stay stuck to the `a` + // and so should this line + + // but this line + // and this line should stick to the `b` + b; + // and this comment should also stick to the `b` + + // similarly `c` + c; + // `c` again + + // and an empty comment stands alone + + // similarly `d` + d; + // `d` again + + // and finally, `d` + assert(d) by { + // whatever + } + // well, now done with `d` +} + } // verus! "#; @@ -2470,6 +2500,36 @@ fn fff() { baz; } + pub fn foo() { + // this should stay stuck to the `a` + assert(a) by { + // whatever + } + // this should also stay stuck to the `a` + // and so should this line + + // but this line + // and this line should stick to the `b` + b; + // and this comment should also stick to the `b` + + // similarly `c` + c; + // `c` again + + // and an empty comment stands alone + + // similarly `d` + d; + // `d` again + + // and finally, `d` + assert(d) by { + // whatever + } + // well, now done with `d` + } + } // verus! "###); }