From f0d6aae282345bc38080d2897a136d86ec72dccf Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Wed, 15 Nov 2023 10:38:34 -0500 Subject: [PATCH 1/2] Add support for while loops with invariants. --- examples/wip.rs | 15 ++++++++++++- src/lib.rs | 41 ++++++++++++++++++++++++++++++------ tests/rustfmt-tests.rs | 2 -- tests/snap-tests.rs | 48 +++++++++++++++++++++++++++++++++++++++++- 4 files changed, 95 insertions(+), 11 deletions(-) diff --git a/examples/wip.rs b/examples/wip.rs index fadcf8e..6f9f6e8 100644 --- a/examples/wip.rs +++ b/examples/wip.rs @@ -1,6 +1,19 @@ verus! { -fn syntactic_eq(&self, other: &Self) { +pub fn clone_vec_u8() { + let i = 0; + while i < v.len() + invariant + i <= v.len(), + i == out.len(), + forall |j| #![auto] 0 <= j < i ==> out@[j] == v@[j], + ensures + i > 0, + decreases + 72, + { + i = i + 1; + } } } // verus! diff --git a/src/lib.rs b/src/lib.rs index b9ef63c..c8d1adc 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -441,7 +441,6 @@ fn to_doc<'a>( | Rule::impl_str | Rule::in_str | Rule::int_str - | Rule::invariant_str | Rule::isize_str | Rule::let_str | Rule::loop_str @@ -497,9 +496,11 @@ fn to_doc<'a>( .append(arena.space()) .nest(INDENT_SPACES), - Rule::decreases_str | Rule::ensures_str | Rule::recommends_str | Rule::requires_str => { - arena.hardline().append(s).nest(INDENT_SPACES) - } + Rule::decreases_str + | Rule::ensures_str + | Rule::invariant_str + | Rule::recommends_str + | Rule::requires_str => arena.hardline().append(s).nest(INDENT_SPACES), Rule::assert_str | Rule::assume_str @@ -585,7 +586,12 @@ fn to_doc<'a>( saw_comment_after_param_list = true; }; // Special case where we don't want an extra newline after the possibly inline comment - comment_to_doc(ctx, arena, p, !has_qualifier || !saw_comment_after_param_list) + comment_to_doc( + ctx, + arena, + p, + !has_qualifier || !saw_comment_after_param_list, + ) } Rule::param_list => { saw_param_list = true; @@ -742,7 +748,28 @@ fn to_doc<'a>( Rule::if_expr => map_to_doc(ctx, arena, pair), Rule::loop_expr => unsupported(pair), Rule::for_expr => unsupported(pair), - Rule::while_expr => map_to_doc(ctx, arena, pair), + Rule::while_expr => { + // We need to add a newline after the very last clause, + // so that the opening brace of the loop body is on a fresh line + let mut last_clause = None; + pair.clone().into_inner().for_each(|p| match p.as_rule() { + Rule::invariant_clause => last_clause = Some(Rule::invariant_clause), + Rule::ensures_clause => last_clause = Some(Rule::ensures_clause), + Rule::decreases_clause => last_clause = Some(Rule::decreases_clause), + _ => (), + }); + arena.concat(pair.into_inner().map(|p| { + if let Some(c) = last_clause { + if p.as_rule() == c { + to_doc(ctx, p, arena).append(arena.line()) + } else { + to_doc(ctx, p, arena) + } + } else { + to_doc(ctx, p, arena) + } + })) + } Rule::label => unsupported(pair), Rule::break_expr => map_to_doc(ctx, arena, pair), Rule::continue_expr => map_to_doc(ctx, arena, pair), @@ -839,7 +866,7 @@ fn to_doc<'a>( Rule::verus_clause_non_expr => map_to_doc(ctx, arena, pair), Rule::requires_clause => map_to_doc(ctx, arena, pair), Rule::ensures_clause => map_to_doc(ctx, arena, pair), - Rule::invariant_clause => unsupported(pair), + Rule::invariant_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::assert_requires => map_to_doc(ctx, arena, pair).append(arena.line()), diff --git a/tests/rustfmt-tests.rs b/tests/rustfmt-tests.rs index 0978a92..871add2 100644 --- a/tests/rustfmt-tests.rs +++ b/tests/rustfmt-tests.rs @@ -368,6 +368,4 @@ let (temp_owl__x607, Tracked(itree)): ( _ } "#; compare(file); - } - diff --git a/tests/snap-tests.rs b/tests/snap-tests.rs index 05fae25..8130469 100644 --- a/tests/snap-tests.rs +++ b/tests/snap-tests.rs @@ -696,7 +696,7 @@ pub exec fn foo() } #[test] -fn keyword_prefixed_identifier_parsing() { +fn verus_keyword_prefixed_identifier_parsing() { let file = r#" verus! { pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) { @@ -717,3 +717,49 @@ pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) { } // verus! "###); } + +#[test] +fn verus_loops() { + let file = r#" +verus! { + +pub fn clone_vec_u8() { + let i = 0; + while i < v.len() + invariant + i <= v.len(), + i == out.len(), + forall |j| #![auto] 0 <= j < i ==> out@[j] == v@[j], + ensures + i > 0, + decreases + 72, + { + i = i + 1; + } +} + +} // verus! +"#; + + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + pub fn clone_vec_u8() { + let i = 0; + while i < v.len() + invariant + i <= v.len(), + i == out.len(), + forall|j| #![auto] 0 <= j < i ==> out@[j] == v@[j], + ensures + i > 0, + decreases 72, + { + i = i + 1; + } + } + + } // verus! + "###); +} From e947b8b67c566838fc81a3e4187f34673650b750 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Wed, 15 Nov 2023 11:45:28 -0500 Subject: [PATCH 2/2] Add support for type_bound_list --- examples/wip.rs | 27 +++++++++++++------------ src/lib.rs | 32 ++++++++++++++++++++++++------ src/verus.pest | 10 ++++++++-- tests/rustfmt-tests.rs | 2 +- tests/snap-tests.rs | 45 ++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 94 insertions(+), 22 deletions(-) diff --git a/examples/wip.rs b/examples/wip.rs index 6f9f6e8..abf7b73 100644 --- a/examples/wip.rs +++ b/examples/wip.rs @@ -1,18 +1,19 @@ verus! { -pub fn clone_vec_u8() { - let i = 0; - while i < v.len() - invariant - i <= v.len(), - i == out.len(), - forall |j| #![auto] 0 <= j < i ==> out@[j] == v@[j], - ensures - i > 0, - decreases - 72, - { - i = i + 1; +struct StrictlyOrderedVec { + a: int, +} + +struct DelegationMap< + #[verifier(maybe_negative)] + K: KeyTrait + VerusClone, +> { + b: int, +} + +impl DelegationMap { + fn view() -> Map { + c } } diff --git a/src/lib.rs b/src/lib.rs index c8d1adc..d67e168 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -400,9 +400,8 @@ fn to_doc<'a>( | Rule::star_str | Rule::tilde_str | Rule::underscore_str => s, - Rule::fn_traits => s, + Rule::fn_traits | Rule::impl_str => s, Rule::pipe_str => docs!(arena, arena.line(), s, arena.space()), - Rule::rarrow_str => docs!(arena, arena.space(), s, arena.space()), // Rule::triple_and | // Rule::triple_or => // docs![arena, arena.hardline(), s, arena.space()].nest(INDENT_SPACES), @@ -412,7 +411,9 @@ fn to_doc<'a>( Rule::eq_str => docs![arena, arena.space(), s, arena.line_(), arena.space()] .nest(INDENT_SPACES - 1) .group(), - Rule::else_str => docs![arena, arena.space(), s, arena.space()], + Rule::plus_str | Rule::rarrow_str | Rule::else_str => { + docs![arena, arena.space(), s, arena.space()] + } Rule::assert_space_str | Rule::async_str | Rule::auto_str @@ -438,7 +439,6 @@ fn to_doc<'a>( | Rule::i64_str | Rule::i8_str | Rule::if_str - | Rule::impl_str | Rule::in_str | Rule::int_str | Rule::isize_str @@ -638,11 +638,31 @@ fn to_doc<'a>( .append(block_braces(arena, map_to_doc(ctx, arena, pair), true)) } Rule::assoc_item => map_to_doc(ctx, arena, pair), - Rule::r#impl => map_to_doc(ctx, arena, pair), + Rule::r#impl => { + let has_generic_params = pair + .clone() + .into_inner() + .find(|p| matches!(p.as_rule(), Rule::spaced_generic_param_list)); + arena.concat(pair.into_inner().map(|p| { + let r = p.as_rule(); + let d = to_doc(ctx, p, arena); + match r { + Rule::impl_str => { + if has_generic_params.is_none() { + d.append(arena.space()) + } else { + d + } + } + _ => d, + } + })) + } Rule::extern_block => unsupported(pair), Rule::extern_item_list => unsupported(pair), Rule::extern_item => unsupported(pair), Rule::generic_param_list => comma_delimited(ctx, arena, pair).angles().group(), + Rule::spaced_generic_param_list => map_to_doc(ctx, arena, pair).append(arena.space()), Rule::generic_param => map_to_doc(ctx, arena, pair), Rule::type_param => map_to_doc(ctx, arena, pair), Rule::const_param => unsupported(pair), @@ -821,7 +841,7 @@ fn to_doc<'a>( Rule::for_type => map_to_doc(ctx, arena, pair), Rule::impl_trait_type => map_to_doc(ctx, arena, pair), Rule::dyn_trait_type => map_to_doc(ctx, arena, pair), - Rule::type_bound_list => unsupported(pair), + Rule::type_bound_list => map_to_doc(ctx, arena, pair), Rule::type_bound => map_to_doc(ctx, arena, pair), //************************// diff --git a/src/verus.pest b/src/verus.pest index 9e2ad61..49ba5db 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -187,6 +187,7 @@ lbrace_str = { "{" } lbracket_str = { "[" } lparen_str = { "(" } pipe_str = { "|" } +plus_str = { "+" } pound_str = { "#" } question_str = { "?" } rangle_str = { ">" } @@ -693,7 +694,7 @@ assoc_item = { impl = { attr* ~ visibility? ~ default_str? ~ unsafe_str? ~ - impl_str ~ generic_param_list? ~ (const_str? ~ bang_str? ~ type ~ for_str)? ~ type ~ where_clause? ~ + impl_str ~ spaced_generic_param_list? ~ (const_str? ~ bang_str? ~ type ~ for_str)? ~ type ~ where_clause? ~ assoc_item_list } @@ -716,6 +717,11 @@ generic_param_list = { "<" ~ (generic_param ~ ("," ~ generic_param)* ~ ","?)? ~ ">" } +// A generic_param_list that should be followed by a space +spaced_generic_param_list = { + generic_param_list +} + generic_param = { const_param | lifetime_param @@ -1244,7 +1250,7 @@ dyn_trait_type = { } type_bound_list = { - type_bound ~ ("+" ~ type_bound)* ~ "+"? + type_bound ~ (plus_str ~ type_bound)* ~ plus_str? } type_bound = { diff --git a/tests/rustfmt-tests.rs b/tests/rustfmt-tests.rs index 871add2..ace6673 100644 --- a/tests/rustfmt-tests.rs +++ b/tests/rustfmt-tests.rs @@ -19,7 +19,7 @@ fn compare(file: &str) { 3, Some(("rust", "verus")), ); - assert_eq!(rust_fmt, verus_inner, "{diff}"); + assert_eq!(rust_fmt, verus_inner, "\n{diff}"); } #[test] diff --git a/tests/snap-tests.rs b/tests/snap-tests.rs index 8130469..1b346ed 100644 --- a/tests/snap-tests.rs +++ b/tests/snap-tests.rs @@ -718,6 +718,51 @@ pub exec fn foo(mut_state: &mut Blah, selfie_stick: SelfieStick) { "###); } +#[test] +fn verus_impl_bounds() { + let file = r#" +verus! { +struct StrictlyOrderedVec { + a: int +} + +struct DelegationMap<#[verifier(maybe_negative)] K: KeyTrait + VerusClone> { + b: int +} + +impl DelegationMap { + fn view() -> Map { + c + } +} + +} // verus! +"#; + + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + struct StrictlyOrderedVec { + a: int, + } + + struct DelegationMap< + #[verifier(maybe_negative)] + K: KeyTrait + VerusClone, + > { + b: int, + } + + impl DelegationMap { + fn view() -> Map { + c + } + } + + } // verus! + "###); +} + #[test] fn verus_loops() { let file = r#"