Skip to content

Commit

Permalink
Fix minor min-parsing issues (#87)
Browse files Browse the repository at this point in the history
Hit some issues when attempting to run verusfmt on
https://github.com/secure-foundations/human-eval-verus/blob/main/tasks/human_eval_001.rs
; specifically, our minimal parser would consider the parenthesis in
`'('` to be syntactically-relevant, rather than ignore it, thereby
causing a:
```
thread 'main' panicked at src/rustfmt.rs:51:10:
Minimal parsing should never fail. If it did, please report this as an error.: Error { variant: ParsingError { positives: [COMMENT, tt], negatives: [] }, location: Pos(5984), line_col: Pos((155, 9)), path: None, line: "        } else if c == ')' {", continued_line: None }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
```

This PR fixes the issues.

Automatically-minimized example that triggers the issue before this PR:
```rs
verus! {

fn a()
    ensures
{
    {
        if '(' {
            if 0 {
            }
        }
    }
}

} // verus!
```
  • Loading branch information
jaybosamiya-ms authored Aug 21, 2024
2 parents 57b07a5 + 5e101e3 commit 1d3ff7b
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 5 deletions.
10 changes: 7 additions & 3 deletions src/verus-minimal.pest
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,10 @@ raw_byte_string = @{
"b" ~ raw_string
}

char = @{
"'" ~ ("\\'" | !"'" ~ ANY) ~ "'"
}

multiline_comment = @{
"/*" ~ (multiline_comment | (!"*/" ~ ANY))* ~ "*/"
}
Expand All @@ -59,12 +63,12 @@ file = {

/// Region of code that doesn't contain any Verus macro use whatsoever
non_verus = @{
(!("verus!" ~ WHITESPACE* ~ "{") ~ (string | raw_string | byte_string | raw_byte_string | ANY))*
(!("verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE* ~ "{") ~ (string | raw_string | byte_string | raw_byte_string | char | ANY))*
}

/// An actual use of the `verus! { ... }` macro
verus_macro_use = ${
"verus!" ~ WHITESPACE* ~ "{" ~ (WHITESPACE | COMMENT)* ~ verus_macro_body ~ (WHITESPACE | COMMENT)* ~ "}" ~ WHITESPACE* ~ ("//" ~ WHITESPACE* ~ "verus!" ~ WHITESPACE*)?
"verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE* ~ "{" ~ (WHITESPACE | COMMENT)* ~ verus_macro_body ~ (WHITESPACE | COMMENT)* ~ "}" ~ WHITESPACE* ~ ("//" ~ WHITESPACE* ~ "verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE*)?
}

/// Anything inside the `verus! { ... }` macro
Expand All @@ -90,5 +94,5 @@ paren_tree = {

/// _Technically_ not a Rust token, but we're trying to do a minimal parser _anyways_
token = {
!("{" | "}" | "[" | "]" | "(" | ")") ~ ANY
!("{" | "}" | "[" | "]" | "(" | ")") ~ (string | raw_string | byte_string | raw_byte_string | char | ANY)
}
4 changes: 2 additions & 2 deletions src/verus.pest
Original file line number Diff line number Diff line change
Expand Up @@ -82,12 +82,12 @@ file = {
/// happens, then we need to make sure that we aren't accidentally starting
/// parsing in the middle of the macro_rules macro body itself. Similarly, strings.
non_verus = @{
(!("verus!" ~ WHITESPACE* ~ "{") ~ (macro_rules | string | raw_string | byte_string | raw_byte_string | ANY))*
(!("verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE* ~ "{") ~ (macro_rules | string | raw_string | byte_string | raw_byte_string | ANY))*
}

/// An actual use of the `verus! { ... }` macro
verus_macro_use = ${
"verus!" ~ WHITESPACE* ~ "{" ~ (WHITESPACE | COMMENT)* ~ verus_macro_body ~ (WHITESPACE | COMMENT)* ~ "}" ~ WHITESPACE* ~ ("//" ~ WHITESPACE* ~ "verus!")?
"verus" ~ WHITESPACE* ~ "!" ~ WHITESPACE* ~ "{" ~ (WHITESPACE | COMMENT)* ~ verus_macro_body ~ (WHITESPACE | COMMENT)* ~ "}" ~ WHITESPACE* ~ ("//" ~ WHITESPACE* ~ "verus" ~ WHITESPACE* ~ "!")?
}

/// Anything inside the `verus! { ... }` macro
Expand Down

0 comments on commit 1d3ff7b

Please sign in to comment.