Skip to content

Commit 4ed2707

Browse files
zaklogicianzaklogician
committed
tool: reformat viper output-related code
Signed-off-by: Zoltan A. Kocsis <11808286+zaklogician@users.noreply.github.com>
1 parent 322b54c commit 4ed2707

2 files changed

Lines changed: 44 additions & 126 deletions

File tree

‎tool/microkit/src/main.rs‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ use microkit_tool::viper;
3333
use microkit_tool::{DisjointMemoryRegion, MemoryRegion};
3434
use std::collections::HashMap;
3535
use std::fs::{self, metadata};
36-
use std::path::{Path};
36+
use std::path::Path;
3737

3838
const MAX_BUILD_ITERATION: usize = 3;
3939

@@ -705,14 +705,11 @@ fn main() -> Result<(), String> {
705705
std::process::exit(1);
706706
});
707707
for view in viper::get_combined_views(&spec_container, &system) {
708-
let mut output =
709-
String::from(
710-
format!(
711-
"// exported invariants for PD {} in {}\n",
712-
view.pd_name,
713-
&args.sdf_path.display(),
714-
)
715-
);
708+
let mut output = String::from(format!(
709+
"// exported invariants for PD {} in {}\n",
710+
view.pd_name,
711+
&args.sdf_path.display(),
712+
));
716713
view.export(&mut output);
717714
let path = viper_output_dir.join(format!("{}.vpr", view.pd_name));
718715
fs::write(&path, output).unwrap_or_else(|source| {
@@ -723,7 +720,6 @@ fn main() -> Result<(), String> {
723720
std::process::exit(1);
724721
});
725722
}
726-
727723
}
728724

729725
write_report(&spec_container, &kernel_config, &args.report_path);

‎tool/microkit/src/viper.rs‎

Lines changed: 38 additions & 116 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,8 @@ use crate::sdf::SystemDescription;
1111

1212
fn export_define_set(name: &'static str, vector: &Vec<u64>, target: &mut String) {
1313
if vector.is_empty() {
14-
target.push_str(&format!(
15-
"define {name}(x) (false)\n"
16-
));
17-
target.push_str(&format!(
18-
"define f_{name}(heap,gv,x) ({name}(x))\n"
19-
));
14+
target.push_str(&format!("define {name}(x) (false)\n"));
15+
target.push_str(&format!("define f_{name}(heap,gv,x) ({name}(x))\n"));
2016
return;
2117
}
2218

@@ -26,15 +22,10 @@ fn export_define_set(name: &'static str, vector: &Vec<u64>, target: &mut String)
2622
.collect::<Vec<_>>()
2723
.join(",");
2824

29-
target.push_str(&format!(
30-
"define {name}(x) (x in Set({items}))\n"
31-
));
32-
target.push_str(&format!(
33-
"define f_{name}(heap,gv,x) ({name}(x))\n"
34-
));
25+
target.push_str(&format!("define {name}(x) (x in Set({items}))\n"));
26+
target.push_str(&format!("define f_{name}(heap,gv,x) ({name}(x))\n"));
3527
}
3628

37-
3829
#[derive(Debug, Clone, Default, PartialEq, Eq)]
3930
pub struct CapView {
4031
pub occupied_slots: Vec<u64>,
@@ -52,56 +43,24 @@ pub struct CapView {
5243

5344
impl CapView {
5445
pub fn export(&self, target: &mut String) {
55-
export_define_set(
56-
"pansel4_has_cap",
57-
&self.occupied_slots,
58-
target
59-
);
60-
export_define_set(
61-
"pansel4_has_endpoint_cap",
62-
&self.endpoint_caps,
63-
target
64-
);
46+
export_define_set("pansel4_has_cap", &self.occupied_slots, target);
47+
export_define_set("pansel4_has_endpoint_cap", &self.endpoint_caps, target);
6548
export_define_set(
6649
"pansel4_has_notification_cap",
6750
&self.notification_caps,
68-
target
69-
);
70-
export_define_set(
71-
"pansel4_has_reply_cap",
72-
&self.reply_caps,
73-
target
74-
);
75-
export_define_set(
76-
"pansel4_has_page_table_cap",
77-
&self.page_table_caps,
78-
target
51+
target,
7952
);
53+
export_define_set("pansel4_has_reply_cap", &self.reply_caps, target);
54+
export_define_set("pansel4_has_page_table_cap", &self.page_table_caps, target);
8055
export_define_set(
8156
"pansel4_has_irq_handler_cap",
8257
&self.irq_handler_caps,
83-
target
84-
);
85-
export_define_set(
86-
"pansel4_has_tcb_cap",
87-
&self.tcb_caps,
88-
target
89-
);
90-
export_define_set(
91-
"pansel4_has_vcpu_cap",
92-
&self.vcpu_caps,
93-
target
94-
);
95-
export_define_set(
96-
"pansel4_has_ioport_cap",
97-
&self.ioport_caps,
98-
target
99-
);
100-
export_define_set(
101-
"pansel4_has_arm_smc_cap",
102-
&self.arm_smc_caps,
103-
target
58+
target,
10459
);
60+
export_define_set("pansel4_has_tcb_cap", &self.tcb_caps, target);
61+
export_define_set("pansel4_has_vcpu_cap", &self.vcpu_caps, target);
62+
export_define_set("pansel4_has_ioport_cap", &self.ioport_caps, target);
63+
export_define_set("pansel4_has_arm_smc_cap", &self.arm_smc_caps, target);
10564
}
10665

10766
fn sort_and_dedup(&mut self) {
@@ -159,11 +118,11 @@ pub fn get_cap_view(
159118
Cap::PageTable(_) => {
160119
view.page_table_caps.push(slot);
161120
}
162-
Cap::ArmIrqHandler(_) |
163-
Cap::IrqHandler(_) |
164-
Cap::IrqIOApicHandler(_) |
165-
Cap::IrqMsiHandler(_) |
166-
Cap::RiscvIrqHandler(_) => {
121+
Cap::ArmIrqHandler(_)
122+
| Cap::IrqHandler(_)
123+
| Cap::IrqIOApicHandler(_)
124+
| Cap::IrqMsiHandler(_)
125+
| Cap::RiscvIrqHandler(_) => {
167126
view.irq_handler_caps.push(slot);
168127
}
169128
Cap::Tcb(_) => {
@@ -179,12 +138,12 @@ pub fn get_cap_view(
179138
view.arm_smc_caps.push(slot);
180139
}
181140

182-
Cap::AsidPool(_) |
183-
Cap::CNode(_) |
184-
Cap::DomainSet(_) |
185-
Cap::Frame(_) |
186-
Cap::SchedContext(_) |
187-
Cap::Untyped(_) => {
141+
Cap::AsidPool(_)
142+
| Cap::CNode(_)
143+
| Cap::DomainSet(_)
144+
| Cap::Frame(_)
145+
| Cap::SchedContext(_)
146+
| Cap::Untyped(_) => {
188147
/* ^ The caps above can occupy CSpace slots, but Viper
189148
* verification currently has no use for them, so we
190149
* intentionally do not emit anything here.
@@ -197,7 +156,6 @@ pub fn get_cap_view(
197156
Some(view)
198157
}
199158

200-
201159
#[derive(Debug, Clone, Default, PartialEq, Eq)]
202160
pub struct SdfView {
203161
// the world, from the perspective of a single PD
@@ -211,43 +169,18 @@ pub struct SdfView {
211169
}
212170

213171
impl SdfView {
214-
215172
pub fn export(&self, target: &mut String) -> () {
216-
export_define_set(
217-
"mk_is_protected_source",
218-
&self.protected_sources,
219-
target,
220-
);
173+
export_define_set("mk_is_protected_source", &self.protected_sources, target);
221174

222-
export_define_set(
223-
"mk_is_ppcall_target",
224-
&self.ppcall_targets,
225-
target,
226-
);
175+
export_define_set("mk_is_ppcall_target", &self.ppcall_targets, target);
227176

228-
export_define_set(
229-
"mk_is_notified_source",
230-
&self.notified_sources,
231-
target,
232-
);
177+
export_define_set("mk_is_notified_source", &self.notified_sources, target);
233178

234-
export_define_set(
235-
"mk_is_notify_target",
236-
&self.notify_targets,
237-
target,
238-
);
179+
export_define_set("mk_is_notify_target", &self.notify_targets, target);
239180

240-
export_define_set(
241-
"mk_is_irq_channel",
242-
&self.irqs,
243-
target,
244-
);
181+
export_define_set("mk_is_irq_channel", &self.irqs, target);
245182

246-
export_define_set(
247-
"mk_is_child",
248-
&self.children,
249-
target,
250-
);
183+
export_define_set("mk_is_child", &self.children, target);
251184
}
252185
}
253186

@@ -297,7 +230,7 @@ pub fn get_sdf_view(system: &SystemDescription, current_pd: usize) -> Option<Sdf
297230
for pd in &system.protection_domains {
298231
if pd.parent == Some(current_pd) {
299232
match pd.id {
300-
Some(id) => { view.children.push(id) }
233+
Some(id) => view.children.push(id),
301234
None => {}
302235
}
303236
}
@@ -306,7 +239,6 @@ pub fn get_sdf_view(system: &SystemDescription, current_pd: usize) -> Option<Sdf
306239
Some(view)
307240
}
308241

309-
310242
#[derive(Debug, Clone, Default, PartialEq, Eq)]
311243
pub struct Mem {
312244
pub name: String,
@@ -327,29 +259,20 @@ impl Mem {
327259

328260
fn export_define_mem_set(perm: &'static str, vector: &Vec<Mem>, target: &mut String) {
329261
if vector.is_empty() {
330-
target.push_str(&format!(
331-
"define mem_{perm}(x) (false)\n"
332-
));
333-
target.push_str(&format!(
334-
"define f_mem_{perm}(heap,gv,x) (mem_{perm}(x))\n"
335-
));
262+
target.push_str(&format!("define mem_{perm}(x) (false)\n"));
263+
target.push_str(&format!("define f_mem_{perm}(heap,gv,x) (mem_{perm}(x))\n"));
336264
return;
337265
}
338266
let items = vector
339267
.iter()
340-
.map(|x| format!("mem_{}_contains(x)",x.name))
268+
.map(|x| format!("mem_{}_contains(x)", x.name))
341269
.collect::<Vec<_>>()
342270
.join(" || ");
343271

344-
target.push_str(&format!(
345-
"define mem_{perm}(x) ({items})\n"
346-
));
347-
target.push_str(&format!(
348-
"define f_mem_{perm}(heap,gv,x) (mem_{perm}(x))\n"
349-
));
272+
target.push_str(&format!("define mem_{perm}(x) ({items})\n"));
273+
target.push_str(&format!("define f_mem_{perm}(heap,gv,x) (mem_{perm}(x))\n"));
350274
}
351275

352-
353276
#[derive(Debug, Clone, Default, PartialEq, Eq)]
354277
pub struct MemView {
355278
pub read: Vec<Mem>,
@@ -375,8 +298,7 @@ pub fn get_mem_view(system: &SystemDescription, current_pd: usize) -> Option<Mem
375298
};
376299

377300
for mr in &system.memory_regions {
378-
let mmaps_into_current_pd =
379-
current.maps.iter().filter(|map| map.mr == mr.name);
301+
let mmaps_into_current_pd = current.maps.iter().filter(|map| map.mr == mr.name);
380302

381303
for mmap in mmaps_into_current_pd {
382304
let start = mmap.vaddr;

0 commit comments

Comments
 (0)