From 0456f2bf3c687ef136821ddb285f8032bc26e3b7 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Tue, 12 Mar 2024 12:06:19 -0400 Subject: [PATCH 1/2] Don't attempt to parse a range as a float --- CHANGELOG.md | 2 ++ src/verus.pest | 2 +- tests/verus-consistency.rs | 24 ++++++++++++++++++++++++ 3 files changed, 27 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3bc3c68..4f0158d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ # Unreleased +* Improve parsing of range expressions (e.g., `0..(1 + 2)`) that start "float-like" + # v0.2.7 * Improve `verus!{ ... }` macro collapsing inside indented contexts (#39) diff --git a/src/verus.pest b/src/verus.pest index bc7a460..2b295be 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -132,7 +132,7 @@ int_number = @{ float_decimal = @{ (ASCII_DIGIT | "_")+ ~ - "." ~ + !".." ~ "." ~ (ASCII_DIGIT | "_")* ~ ("f32" | "f64")? } diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 270653a..3678f86 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1675,3 +1675,27 @@ proof fn uses_arrow_matches_1(t: ThisOrThat) { assert(t matches ThisOrThat::This } // verus! "###); } + +#[test] +fn verus_range_operator() { + let file = r#" +verus! { + +fn foo() { for i in 0..(10 + 5) { + +} } + +} + +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + fn foo() { + for i in 0..(10 + 5) { + } + } + + } // verus! + "###); +} From 501575f29cdc255e7291f6b03a0a84d388898f77 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Tue, 12 Mar 2024 12:19:31 -0400 Subject: [PATCH 2/2] Add for-loop support, new in Verus --- CHANGELOG.md | 1 + src/lib.rs | 11 ++++---- src/verus.pest | 1 + tests/verus-consistency.rs | 55 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 63 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4f0158d..18af539 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,6 @@ # Unreleased +* Add support for `for` loops with invariants, recently added to Verus * Improve parsing of range expressions (e.g., `0..(1 + 2)`) that start "float-like" # v0.2.7 diff --git a/src/lib.rs b/src/lib.rs index f1e3cff..3497df5 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -476,6 +476,11 @@ fn loop_to_doc<'a>( arena.concat(pair.into_inner().map(|p| { if p.as_rule() == Rule::condition { to_doc(ctx, p, arena).append(arena.space()) + } else if p.as_rule() == Rule::in_str { + // Used for for-loops + arena.space().append(to_doc(ctx, p, arena)) + } else if p.as_rule() == Rule::expr_no_struct { + to_doc(ctx, p, arena).append(arena.space()) } else if let Some(c) = last_clause { if p.as_rule() == c { to_doc(ctx, p, arena).append(arena.line()) @@ -1138,11 +1143,7 @@ fn to_doc<'a>( Rule::condition => map_to_doc(ctx, arena, pair), Rule::if_expr => if_expr_to_doc(ctx, arena, pair), Rule::loop_expr => loop_to_doc(ctx, arena, pair), - Rule::for_expr => arena.concat(pair.into_inner().map(|p| match p.as_rule() { - Rule::in_str => arena.space().append(to_doc(ctx, p, arena)), - Rule::expr_no_struct => to_doc(ctx, p, arena).append(arena.space()), - _ => to_doc(ctx, p, arena), - })), + Rule::for_expr => loop_to_doc(ctx, arena, pair), Rule::while_expr => loop_to_doc(ctx, arena, pair), Rule::label => unsupported(pair), Rule::break_expr => map_to_doc(ctx, arena, pair), diff --git a/src/verus.pest b/src/verus.pest index 2b295be..e4d7ca8 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -1285,6 +1285,7 @@ loop_expr = { for_expr = { attr* ~ label? ~ for_str ~ pat ~ in_str ~ expr_no_struct ~ + invariant_clause? ~ invariant_ensures_clause? ~ ensures_clause? ~ decreases_clause? ~ fn_block_expr } diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index 3678f86..3c812f9 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -1699,3 +1699,58 @@ fn foo() { for i in 0..(10 + 5) { } // verus! "###); } + +#[test] +fn verus_for_loops() { + let file = r#" +verus!{ +fn reverse(v: &mut Vec) + ensures + v.len() == old(v).len(), + forall|i: int| 0 <= i < old(v).len() ==> v[i] == old(v)[old(v).len() - i - 1], +{ + let length = v.len(); + let ghost v1 = v@; + for n in 0..(length / 2) + invariant + length == v.len(), + forall|i: int| 0 <= i < n ==> v[i] == v1[length - i - 1], + forall|i: int| 0 <= i < n ==> v1[i] == v[length - i - 1], + forall|i: int| n <= i && i + n < length ==> #[trigger] v[i] == v1[i], + { + let x = v[n]; + let y = v[length - 1 - n]; + v.set(n, y); + v.set(length - 1 - n, x); + } +} + +} +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + fn reverse(v: &mut Vec) + ensures + v.len() == old(v).len(), + forall|i: int| 0 <= i < old(v).len() ==> v[i] == old(v)[old(v).len() - i - 1], + { + let length = v.len(); + let ghost v1 = v@; + for n in 0..(length / 2) + invariant + length == v.len(), + forall|i: int| 0 <= i < n ==> v[i] == v1[length - i - 1], + forall|i: int| 0 <= i < n ==> v1[i] == v[length - i - 1], + forall|i: int| n <= i && i + n < length ==> #[trigger] v[i] == v1[i], + { + let x = v[n]; + let y = v[length - 1 - n]; + v.set(n, y); + v.set(length - 1 - n, x); + } + } + + } // verus! + "###); +}