Skip to content

Commit

Permalink
Automatic formatting for the seq! macro (#71)
Browse files Browse the repository at this point in the history
  • Loading branch information
@jaybosamiya
jaybosamiya authored May 30, 2024
2 parents c001b55 + fd24517 commit 53c0590
Show file tree
Hide file tree
Showing 6 changed files with 119 additions and 45 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
# Unreleased

* Support automatic formatting of the `seq!` macro

# v0.3.4

* Support const generic arguments
Expand Down
75 changes: 47 additions & 28 deletions examples/ironfleet.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand All @@ -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();
Expand Down Expand Up @@ -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@,
Expand Down Expand Up @@ -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@,
Expand Down Expand Up @@ -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::<AbstractEndPoint, Seq<u8>>::ReadClock{t: time as int}],
self.history@ + seq![LIoOp::<AbstractEndPoint, Seq<u8>>::ReadClock { t: time as int }],
);
time
}
Expand Down Expand Up @@ -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() },
},
Expand All @@ -6689,12 +6695,19 @@ impl NetClient {
match result {
NetcReceiveResult::Received { ref sender, ref message } => {
self.history = Ghost(
self.history@
+ seq![LIoOp::Receive { r: LPacket::<AbstractEndPoint, Seq<u8>> { dst: self.my_end_point(), src: sender@, msg: message@ } } ],
self.history@ + seq![
LIoOp::Receive {
r: LPacket::<AbstractEndPoint, Seq<u8>> {
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 { });
Expand Down Expand Up @@ -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(_) => {
Expand Down
26 changes: 12 additions & 14 deletions examples/pagetable.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
{
Expand All @@ -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!
Expand Down
5 changes: 3 additions & 2 deletions src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down Expand Up @@ -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 {
Expand Down
9 changes: 8 additions & 1 deletion src/verus.pest
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) }
Expand Down Expand Up @@ -497,13 +498,19 @@ 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 ~
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
}

Expand Down
47 changes: 47 additions & 0 deletions tests/verus-consistency.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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!
"###);
}

0 comments on commit 53c0590

Please sign in to comment.