Skip to content

Commit

Permalink
Fix incorrect parsing of strings containing verus!{ (#72)
Browse files Browse the repository at this point in the history
  • Loading branch information
XuhengLi authored Jun 1, 2024
1 parent 53c0590 commit 4a450c5
Show file tree
Hide file tree
Showing 4 changed files with 39 additions and 3 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
# Unreleased

* Fix incorrect parsing of string literals containing "verus!{"
* Support automatic formatting of the `seq!` macro

# v0.3.4
Expand Down
27 changes: 26 additions & 1 deletion src/verus-minimal.pest
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,31 @@ COMMENT = @{
| ("//" ~ (!NEWLINE ~ ANY)* ~ NEWLINE)
}

string = @{
"\"" ~ ("\\\"" | !"\"" ~ ANY)* ~ "\""
}

raw_string = @{
"r" ~ PUSH("#"*) ~ "\"" // push the number signs onto the stack
~ raw_string_interior
~ "\"" ~ POP // match a quotation mark and the number signs
}
raw_string_interior = {
(
!("\"" ~ PEEK) // unless the next character is a quotation mark
// followed by the correct amount of number signs,
~ ANY // consume one character
)*
}

byte_string = @{
"b" ~ string
}

raw_byte_string = @{
"b" ~ raw_string
}

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

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

/// An actual use of the `verus! { ... }` macro
Expand Down
4 changes: 2 additions & 2 deletions src/verus.pest
Original file line number Diff line number Diff line change
Expand Up @@ -72,9 +72,9 @@ file = {
/// someone might define a macro-rules macro _outside_ the verus! macro, but use
/// a verus! inside of the macro body itself, to generate Verus code; if that
/// happens, then we need to make sure that we aren't accidentally starting
/// parsing in the middle of the macro_rules macro body itself.
/// parsing in the middle of the macro_rules macro body itself. Similarly, strings.
non_verus = @{
(!("verus!" ~ WHITESPACE* ~ "{") ~ (macro_rules | ANY))*
(!("verus!" ~ WHITESPACE* ~ "{") ~ (macro_rules | string | raw_string | byte_string | raw_byte_string | ANY))*
}

/// An actual use of the `verus! { ... }` macro
Expand Down
10 changes: 10 additions & 0 deletions tests/rustfmt-matching.rs
Original file line number Diff line number Diff line change
Expand Up @@ -430,3 +430,13 @@ fn test() {
"#;
compare(file);
}

#[test]
fn rust_verus_bang_in_string() {
let file = r#"
fn test() {
println!("verus!{{{}}}", "Hello");
}
"#;
compare(file);
}

0 comments on commit 4a450c5

Please sign in to comment.