From 6129947341c47116e2ae065afb9f92cd996a2f81 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Tue, 28 May 2024 18:33:14 -0700 Subject: [PATCH 1/3] Support automatic formatting of the `seq!` macro --- CHANGELOG.md | 2 ++ src/lib.rs | 5 ++-- src/verus.pest | 7 ++++++ tests/verus-consistency.rs | 47 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 59 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 136233f..f841457 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,7 @@ # Unreleased +* Support automatic formatting of the `seq!` macro + # v0.3.4 * Support const generic arguments diff --git a/src/lib.rs b/src/lib.rs index e60d8eb..4e8e0c5 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -646,7 +646,7 @@ fn to_doc<'a>( | Rule::underscore_str | Rule::arrow_expr_str => s, Rule::fn_traits | Rule::impl_str => s, - Rule::calc_str => s, + Rule::calc_str | Rule::seq_str => s, Rule::pipe_str => docs!(arena, arena.line(), s, arena.space()), // Rule::triple_and | // Rule::triple_or => @@ -838,11 +838,12 @@ fn to_doc<'a>( )) } Rule::calc_macro_call => map_to_doc(ctx, arena, pair), + Rule::seq_macro_call => map_to_doc(ctx, arena, pair), Rule::macro_call | Rule::macro_call_stmt => { if pair .clone() .into_inner() - .any(|x| matches!(x.as_rule(), Rule::calc_macro_call)) + .any(|x| matches!(x.as_rule(), Rule::calc_macro_call | Rule::seq_macro_call)) { map_to_doc(ctx, arena, pair) } else { diff --git a/src/verus.pest b/src/verus.pest index 1eca11c..2f4ce1c 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -312,6 +312,7 @@ return_str = ${ "return" ~ !("_" | ASCII_ALPHANUMERIC) } r_str = ${ "r" ~ !("_" | ASCII_ALPHANUMERIC) } Self_str = ${ "Self" ~ !("_" | ASCII_ALPHANUMERIC) } self_str = ${ "self" ~ !("_" | ASCII_ALPHANUMERIC) } +seq_str = ${ "seq" ~ !("_" | ASCII_ALPHANUMERIC) } sizeof_str = ${ "size_of" ~ !("_" | ASCII_ALPHANUMERIC) } spec_fn_str = ${ "spec_fn" ~ !("_" | ASCII_ALPHANUMERIC) } spec_str = ${ "spec" ~ !("_" | ASCII_ALPHANUMERIC) } @@ -501,9 +502,15 @@ calc_macro_call = { calc_macro_body } +seq_macro_call = { + attr* ~ seq_str ~ bang_str ~ !"=" ~ + lbracket_str ~ comma_delimited_exprs? ~ rbracket_str +} + // TODO: Special handling for the state_machine! macros? macro_call = { calc_macro_call + | seq_macro_call | attr* ~ path ~ bang_str ~ !"=" ~ token_tree } diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs index f6b3b03..35932df 100644 --- a/tests/verus-consistency.rs +++ b/tests/verus-consistency.rs @@ -2263,3 +2263,50 @@ fn foo(arg: ConstBytes<2>) -> (res: ConstBytes<4>) { } // verus! "###); } + +#[test] +fn verus_seq_macro() { + let file = r#" +verus! { +proof fn f() { + let s = seq![ + 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, + 0x00, 0x00, 0x00, + ]; + let s = seq![ + 0x00, 0x00, + 0x00, 0x00, + ]; +} +} +"#; + assert_snapshot!(parse_and_format(file).unwrap(), @r###" + verus! { + + proof fn f() { + let s = seq![ + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + 0x00, + ]; + let s = seq![0x00, 0x00, 0x00, 0x00]; + } + + } // verus! + "###); +} From a41841c2c8f09929ca5917af5acd2492ee0a048c Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Tue, 28 May 2024 18:34:00 -0700 Subject: [PATCH 2/3] Update snapshots with `seq!` formatting --- examples/ironfleet.rs | 75 +++++++++++++++++++++++++++---------------- examples/pagetable.rs | 26 +++++++-------- 2 files changed, 59 insertions(+), 42 deletions(-) diff --git a/examples/ironfleet.rs b/examples/ironfleet.rs index 3113349..a89a6a9 100644 --- a/examples/ironfleet.rs +++ b/examples/ironfleet.rs @@ -3939,9 +3939,9 @@ impl HostState { let iop: NetEvent = LIoOp::TimeoutReceive { }; let ghost res = EventResults { recvs: seq![], - clocks: seq![ iop ], + clocks: seq![iop], sends: seq![], - ios: seq![ iop ], + ios: seq![iop], }; proof { old_self.delegation_map.valid_implies_complete(); @@ -3958,10 +3958,10 @@ impl HostState { match cpacket.msg { CSingleMessage::InvalidMessage { } => { let ghost res = EventResults { - recvs: seq![ net_event@ ], + recvs: seq![net_event@], clocks: seq![], sends: seq![], - ios: seq![ net_event@ ], + ios: seq![net_event@], }; proof { old_self.delegation_map.valid_implies_complete(); @@ -4835,9 +4835,11 @@ impl HostState { ) == extract_packets_from_lsht_packets( seq![abstractify_cpacket_to_lsht_packet(p)], )); - assert(seq![abstractify_cpacket_to_lsht_packet(p)].map_values( - |lp: LSHTPacket| extract_packet_from_lsht_packet(lp))[0] - == Packet { + assert(seq![ + abstractify_cpacket_to_lsht_packet(p), + ].map_values( + |lp: LSHTPacket| extract_packet_from_lsht_packet(lp), + )[0] == Packet { dst: pkt.src, src: self.constants.me@, msg: sm@, @@ -5162,8 +5164,11 @@ impl HostState { sent_packets@, ).map_values( |lp: LSHTPacket| extract_packet_from_lsht_packet(lp), - ) - =~= seq![extract_packet_from_lsht_packet(abstractify_cpacket_to_lsht_packet(p))]); // twiddle + ) =~= seq![ + extract_packet_from_lsht_packet( + abstractify_cpacket_to_lsht_packet(p), + ), + ]); // twiddle assert(next_shard( old(self)@, self@, @@ -6599,13 +6604,15 @@ impl NetClient { ensures ({ &&& self.state().is_Sending() - &&& self.history() == old(self).history() + seq![LIoOp::ReadClock{t: time as int}] + &&& self.history() == old(self).history() + seq![ + LIoOp::ReadClock { t: time as int }, + ] }), { let time: u64 = self.get_time_internal(); self.state = Ghost(State::Sending); self.history = Ghost( - self.history@ + seq![LIoOp::>::ReadClock{t: time as int}], + self.history@ + seq![LIoOp::>::ReadClock { t: time as int }], ); time } @@ -6668,19 +6675,18 @@ impl NetClient { NetcReceiveResult::Received { sender, message } => { &&& self.state().is_Receiving() &&& sender.abstractable() - &&& self.history() == old(self).history() - + seq![ - LIoOp::Receive{ - r: LPacket{ - dst: self.my_end_point(), - src: sender@, - msg: message@} - }] + &&& self.history() == old(self).history() + seq![ + LIoOp::Receive { + r: LPacket { dst: self.my_end_point(), src: sender@, msg: message@ }, + }, + ] }, NetcReceiveResult::TimedOut { } => { &&& self.state().is_Sending() - &&& self.history() == old(self).history() - + seq![LIoOp/*TODO(verus) fix name when qpath fix*/::TimeoutReceive{}] + &&& self.history() == old(self).history() + seq![ + LIoOp /*TODO(verus) fix name when qpath fix*/ + ::TimeoutReceive { }, + ] }, NetcReceiveResult::Error { } => { self.state().is_Error() }, }, @@ -6689,12 +6695,19 @@ impl NetClient { match result { NetcReceiveResult::Received { ref sender, ref message } => { self.history = Ghost( - self.history@ - + seq![LIoOp::Receive { r: LPacket::> { dst: self.my_end_point(), src: sender@, msg: message@ } } ], + self.history@ + seq![ + LIoOp::Receive { + r: LPacket::> { + dst: self.my_end_point(), + src: sender@, + msg: message@, + }, + }, + ], ); }, NetcReceiveResult::TimedOut { } => { - self.history = Ghost(self.history@ + seq![LIoOp::TimeoutReceive{}]); + self.history = Ghost(self.history@ + seq![LIoOp::TimeoutReceive { }]); }, NetcReceiveResult::Error { } => { self.state = Ghost(State::Error { }); @@ -6746,16 +6759,22 @@ impl NetClient { self.my_end_point() == old(self).my_end_point(), self.state().is_Error() <==> result.is_Err(), result.is_Ok() ==> self.state().is_Sending(), - result.is_Ok() ==> self.history() == old(self).history() - + seq![LIoOp::Send{s: LPacket{dst: recipient@, src: self.my_end_point(), msg: message@}}], + result.is_Ok() ==> self.history() == old(self).history() + seq![ + LIoOp::Send { + s: LPacket { dst: recipient@, src: self.my_end_point(), msg: message@ }, + }, + ], { let result: Result<(), IronfleetIOError> = self.send_internal_wrapper(recipient, message); match result { Ok(_) => { self.state = Ghost(State::Sending { }); self.history = Ghost( - self.history@ - + seq![LIoOp::Send{s: LPacket{dst: recipient@, src: self.my_end_point(), msg: message@}}], + self.history@ + seq![ + LIoOp::Send { + s: LPacket { dst: recipient@, src: self.my_end_point(), msg: message@ }, + }, + ], ); }, Err(_) => { diff --git a/examples/pagetable.rs b/examples/pagetable.rs index 2e602b1..3425ea0 100644 --- a/examples/pagetable.rs +++ b/examples/pagetable.rs @@ -9348,13 +9348,12 @@ pub proof fn axiom_x86_arch_exec_spec() pub exec fn x86_arch_exec() -> (res: ArchExec) ensures - res.layers@ - == seq![ - ArchLayerExec { entry_size: L0_ENTRY_SIZE, num_entries: 512 }, - ArchLayerExec { entry_size: L1_ENTRY_SIZE, num_entries: 512 }, - ArchLayerExec { entry_size: L2_ENTRY_SIZE, num_entries: 512 }, - ArchLayerExec { entry_size: L3_ENTRY_SIZE, num_entries: 512 }, - ], + res.layers@ == seq![ + ArchLayerExec { entry_size: L0_ENTRY_SIZE, num_entries: 512 }, + ArchLayerExec { entry_size: L1_ENTRY_SIZE, num_entries: 512 }, + ArchLayerExec { entry_size: L2_ENTRY_SIZE, num_entries: 512 }, + ArchLayerExec { entry_size: L3_ENTRY_SIZE, num_entries: 512 }, + ], res@ === x86_arch_spec, res === x86_arch_exec_spec(), { @@ -9376,13 +9375,12 @@ pub exec fn x86_arch_exec() -> (res: ArchExec) } pub spec const x86_arch_spec: Arch = Arch { - layers: - seq![ - ArchLayer { entry_size: L0_ENTRY_SIZE as nat, num_entries: 512 }, - ArchLayer { entry_size: L1_ENTRY_SIZE as nat, num_entries: 512 }, - ArchLayer { entry_size: L2_ENTRY_SIZE as nat, num_entries: 512 }, - ArchLayer { entry_size: L3_ENTRY_SIZE as nat, num_entries: 512 }, - ], + layers: seq![ + ArchLayer { entry_size: L0_ENTRY_SIZE as nat, num_entries: 512 }, + ArchLayer { entry_size: L1_ENTRY_SIZE as nat, num_entries: 512 }, + ArchLayer { entry_size: L2_ENTRY_SIZE as nat, num_entries: 512 }, + ArchLayer { entry_size: L3_ENTRY_SIZE as nat, num_entries: 512 }, + ], }; } // verus! From fd245176cbcbd618da21c21da8009f3d66093777 Mon Sep 17 00:00:00 2001 From: Jay Bosamiya Date: Wed, 29 May 2024 15:11:45 -0700 Subject: [PATCH 3/3] Remove unnecessary parser complexity This `!"="` is necessary for general macro calls, to prevent accidentally considering `foo != bar` as if it were a macro call going `foo! =` and then getting confused. However, both the `calc` and `seq` macros explicitly check for the curly braces, so don't actually need the negative forward lookahead. --- src/verus.pest | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/verus.pest b/src/verus.pest index 2f4ce1c..ee28f09 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -498,12 +498,12 @@ calc_macro_body = { } calc_macro_call = { - attr* ~ calc_str ~ bang_str ~ !"=" ~ + attr* ~ calc_str ~ bang_str ~ calc_macro_body } seq_macro_call = { - attr* ~ seq_str ~ bang_str ~ !"=" ~ + attr* ~ seq_str ~ bang_str ~ lbracket_str ~ comma_delimited_exprs? ~ rbracket_str }