Skip to content

Commit 0f6e5b2

Browse files
Xungan2Xungan2
committed
fmt
1 parent 59ca8a1 commit 0f6e5b2

9 files changed

Lines changed: 33 additions & 80 deletions

File tree

‎lock-protocol/src/exec/mod.rs‎

Lines changed: 0 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -135,24 +135,19 @@ pub fn alloc_page_table<C: PageTableConfig>(
135135
// fn is_present(&self) -> bool {
136136
// self.frame_pa != 0
137137
// }
138-
139138
// open spec fn is_present_spec(&self) -> bool {
140139
// self.frame_pa != 0
141140
// }
142-
143141
// fn frame_paddr(&self) -> (res: usize) {
144142
// self.frame_pa as usize
145143
// }
146-
147144
// open spec fn frame_paddr_spec(&self) -> Paddr {
148145
// self.frame_pa as Paddr
149146
// }
150-
151147
// #[verifier::external_body]
152148
// fn is_last(&self, level: u8) -> bool {
153149
// level == 1
154150
// }
155-
156151
// fn new_page(
157152
// paddr: crate::mm::Paddr,
158153
// level: crate::mm::PagingLevel,
@@ -166,7 +161,6 @@ pub fn alloc_page_table<C: PageTableConfig>(
166161
// prop,
167162
// }
168163
// }
169-
170164
// #[verifier::external_body]
171165
// fn new_pt(paddr: crate::mm::Paddr) -> Self {
172166
// MockPageTableEntry {
@@ -181,45 +175,36 @@ pub fn alloc_page_table<C: PageTableConfig>(
181175
// },
182176
// }
183177
// }
184-
185178
// #[verifier::external_body]
186179
// fn new_token(token: crate::mm::vm_space::Token) -> Self {
187180
// todo!()
188181
// }
189-
190182
// #[verifier::external_body]
191183
// fn prop(&self) -> crate::mm::page_prop::PageProperty {
192184
// self.prop.clone()
193185
// }
194-
195186
// open spec fn prop_spec(&self) -> PageProperty {
196187
// self.prop
197188
// }
198-
199189
// #[verifier::external_body]
200190
// fn set_prop(&mut self, prop: crate::mm::page_prop::PageProperty) {
201191
// todo!()
202192
// }
203-
204193
// #[verifier::external_body]
205194
// fn set_paddr(&mut self, paddr: crate::mm::Paddr) {
206195
// todo!()
207196
// }
208-
209197
// #[verifier::external_body]
210198
// fn new_absent() -> Self {
211199
// // Self::default()
212200
// std::unimplemented!()
213201
// }
214-
215202
// fn pte_paddr(&self) -> (res: Paddr) {
216203
// self.pte_addr as Paddr
217204
// }
218-
219205
// open spec fn pte_paddr_spec(&self) -> Paddr {
220206
// self.pte_addr as Paddr
221207
// }
222-
223208
// fn clone_pte(&self) -> (res: Self) {
224209
// MockPageTableEntry {
225210
// pte_addr: self.pte_addr,
@@ -229,7 +214,6 @@ pub fn alloc_page_table<C: PageTableConfig>(
229214
// }
230215
// }
231216
// }
232-
233217
// #[verifier::external_body]
234218
// pub fn main_test() {
235219
// test_map::test(
@@ -242,7 +226,6 @@ pub fn alloc_page_table<C: PageTableConfig>(
242226
// },
243227
// )
244228
// }
245-
246229
pub open spec fn get_pte_addr_from_va_frame_addr_and_level_spec<C: PagingConstsTrait>(
247230
va: usize,
248231
frame_va: usize,

‎lock-protocol/src/exec/rcu/cursor/mod.rs‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
pub mod locking;
22

3-
use std::{
4-
marker::PhantomData,
5-
ops::Range,
6-
};
3+
use std::{marker::PhantomData, ops::Range};
74

85
use vstd::prelude::*;
96

@@ -32,7 +29,7 @@ impl<'a, C: PageTableConfig> Cursor<'a, C> {
3229
pub open spec fn wf(&self) -> bool {
3330
&&& self.path.len() == 4
3431
&&& 1 <= self.level <= self.guard_level <= 4
35-
&&& forall |level: PagingLevel|
32+
&&& forall|level: PagingLevel|
3633
#![trigger self.path[level - 1]]
3734
1 <= level <= 4 ==> {
3835
if level > self.guard_level {

‎lock-protocol/src/exec/rcu/node/child.rs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,9 @@ impl<C: PageTableConfig> Child<C> {
8787
Child::PageTable(node) => {
8888
let paddr = node.start_paddr();
8989
let tracked_node = node.deref();
90-
proof { tracked_node.axiom_from_raw_sound(); }
90+
proof {
91+
tracked_node.axiom_from_raw_sound();
92+
}
9193
let tracked_inst = tracked_node.inst;
9294
let tracked inst = tracked_inst.borrow().clone();
9395
let ghost nid = node.nid@;

‎lock-protocol/src/exec/rcu/node/mod.rs‎

Lines changed: 5 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,8 @@ impl<C: PageTableConfig> PageTableNode<C> {
104104
self.wf(),
105105
ensures
106106
Self::from_raw_spec(self.start_paddr()) =~= *self,
107-
{}
107+
{
108+
}
108109
}
109110

110111
// Functions defined in struct 'PageTableNode'.
@@ -284,11 +285,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
284285
res.guard->Some_0.in_protocol@ == false,
285286
{
286287
let guard = self.deref().meta().lock.normal_lock();
287-
PageTableGuard {
288-
inner: self,
289-
guard: Some(guard),
290-
_phantom: PhantomData,
291-
}
288+
PageTableGuard { inner: self, guard: Some(guard), _phantom: PhantomData }
292289
}
293290

294291
pub fn normal_lock_new_allocated_node<'rcu>(
@@ -311,11 +308,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
311308
res.guard->Some_0.in_protocol@ == false,
312309
{
313310
let guard = self.deref().meta().lock.normal_lock_new_allocated_node(pa_pte_array_token);
314-
PageTableGuard {
315-
inner: self,
316-
guard: Some(guard),
317-
_phantom: PhantomData,
318-
}
311+
PageTableGuard { inner: self, guard: Some(guard), _phantom: PhantomData }
319312
}
320313

321314
pub fn lock<'rcu>(
@@ -353,11 +346,7 @@ impl<'a, C: PageTableConfig> PageTableNodeRef<'a, C> {
353346
proof {
354347
m = res.1.get();
355348
}
356-
let guard = PageTableGuard {
357-
inner: self,
358-
guard: Some(res.0),
359-
_phantom: PhantomData,
360-
};
349+
let guard = PageTableGuard { inner: self, guard: Some(res.0), _phantom: PhantomData };
361350
(guard, Tracked(m))
362351
}
363352

‎lock-protocol/src/exec/rcu/node/spinlock/mod.rs‎

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -156,11 +156,7 @@ impl<C: PageTableConfig> PageTableEntryPerms<C> {
156156
}
157157
}
158158

159-
pub open spec fn relate_pte(
160-
&self,
161-
pte: Pte<C>,
162-
idx: nat
163-
) -> bool {
159+
pub open spec fn relate_pte(&self, pte: Pte<C>, idx: nat) -> bool {
164160
pte =~= self.inner.value()[idx as int]
165161
}
166162
}
@@ -807,11 +803,9 @@ impl<C: PageTableConfig> PageTablePageSpinLock<C> {
807803
(guard, Tracked(m))
808804
}
809805

810-
pub fn unlock(
811-
&self,
812-
guard: SpinGuard<C>,
813-
m: Tracked<LockProtocolModel>
814-
) -> (res: Tracked<LockProtocolModel>)
806+
pub fn unlock(&self, guard: SpinGuard<C>, m: Tracked<LockProtocolModel>) -> (res: Tracked<
807+
LockProtocolModel,
808+
>)
815809
requires
816810
self.wf(),
817811
guard.wf(self),

‎lock-protocol/src/exec/rcu/pte/mod.rs‎

Lines changed: 3 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
// pub mod page_table_entry;
33
// pub mod page_table_entry_trait;
44
// pub mod page_table_flags;
5-
65
use std::marker::PhantomData;
76

87
use vstd::prelude::*;
@@ -144,11 +143,7 @@ impl<C: PageTableConfig> Pte<C> {
144143
res.wf_new_page(paddr, level, prop),
145144
res.is_frame(level) || res.is_marked(),
146145
{
147-
Self {
148-
inner: C::E::new_page(paddr, level, prop),
149-
nid: Ghost(None),
150-
inst: Tracked(None),
151-
}
146+
Self { inner: C::E::new_page(paddr, level, prop), nid: Ghost(None), inst: Tracked(None) }
152147
}
153148

154149
pub open spec fn wf_new_pt(&self, paddr: Paddr, inst: SpecInstance, nid: NodeId) -> bool {
@@ -170,11 +165,7 @@ impl<C: PageTableConfig> Pte<C> {
170165
res.is_pt((PageTableNode::<C>::from_raw_spec(paddr).level_spec() + 1) as PagingLevel),
171166
res.inner.paddr() == paddr,
172167
{
173-
Self {
174-
inner: C::E::new_pt(paddr),
175-
nid: Ghost(Some(nid@)),
176-
inst: Tracked(Some(inst.get())),
177-
}
168+
Self { inner: C::E::new_pt(paddr), nid: Ghost(Some(nid@)), inst: Tracked(Some(inst.get())) }
178169
}
179170
}
180171

@@ -192,7 +183,7 @@ impl<C: PageTableConfig> Clone for Pte<C> {
192183
}
193184

194185
impl<C: PageTableConfig> Copy for Pte<C> {
195-
186+
196187
}
197188

198189
} // verus!

‎lock-protocol/src/mm/page_table/mod.rs‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -208,8 +208,7 @@ impl<C: PageTableConfig> PagingConstsTrait for C {
208208
}
209209
}
210210

211-
pub trait PageTableEntryTrait: Clone +
212-
Copy +
211+
pub trait PageTableEntryTrait: Clone + Copy +
213212
// Default +
214213
// Sized + Send + Sync + 'static
215214
// Debug // TODO: Implement Debug for PageTableEntryTrait
@@ -232,7 +231,7 @@ Sized {
232231
returns
233232
self.as_value_spec(),
234233
;
235-
234+
236235
open spec fn new_absent_spec() -> Self {
237236
Self::default_spec()
238237
}
@@ -268,7 +267,8 @@ Sized {
268267
#[verifier::when_used_as_spec(new_page_spec)]
269268
fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> (res: Self)
270269
requires
271-
// valid_paddr(paddr),
270+
// valid_paddr(paddr),
271+
272272
level == 1,
273273
ensures
274274
res.is_present(),
@@ -284,10 +284,12 @@ Sized {
284284
#[verifier::when_used_as_spec(new_pt_spec)]
285285
fn new_pt(paddr: Paddr) -> (res: Self)
286286
requires
287-
// valid_paddr(paddr),
287+
// valid_paddr(paddr),
288+
288289
ensures
289290
res.is_present(),
290-
// valid_paddr(res.paddr()),
291+
// valid_paddr(res.paddr()),
292+
291293
returns
292294
Self::new_pt_spec(paddr),
293295
;
@@ -343,7 +345,8 @@ Sized {
343345
!Self::default().is_present(),
344346
forall|p: Paddr, level: PagingLevel, prop: PageProperty|
345347
#![trigger Self::new_page(p, level, prop)]
346-
// valid_paddr(p) &&
348+
// valid_paddr(p) &&
349+
347350
level == 1 ==> {
348351
let page = Self::new_page(p, level, prop);
349352
&&& page.is_present()
@@ -352,13 +355,15 @@ Sized {
352355
},
353356
forall|p: Paddr|
354357
#![trigger Self::new_pt(p)]
355-
// valid_paddr(p) ==>
358+
// valid_paddr(p) ==>
359+
356360
{
357361
let pt = Self::new_pt(p);
358362
&&& pt.is_present()
359363
&&& pt.paddr_spec() == p
360364
// TODO
361365
// &&& !pt.is_last(PageTableNode::from_raw_spec(p).level_spec())
366+
362367
},
363368
;
364369

‎lock-protocol/src/mm/page_table/node/child.rs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,9 @@ impl<C: PageTableConfig> Child<C> {
6363
C::E::new_pt(paddr)
6464
},
6565
Child::Frame(paddr, level, prop) => {
66-
assert(level == 1) by { admit(); };
66+
assert(level == 1) by {
67+
admit();
68+
};
6769
C::E::new_page(paddr, level, prop)
6870
},
6971
Child::None => C::E::new_absent(),

‎lock-protocol/src/mm/vm_space.rs‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -166,25 +166,18 @@ pub(crate) struct UserPtConfig {}
166166
// fn TOP_LEVEL_INDEX_RANGE() -> Range<usize> {
167167
// 0..256
168168
// }
169-
170169
// open spec fn TOP_LEVEL_INDEX_RANGE_spec() -> Range<usize> {
171170
// 0..256
172171
// }
173-
174172
// fn TOP_LEVEL_CAN_UNMAP() -> bool {
175173
// true
176174
// }
177-
178175
// open spec fn TOP_LEVEL_CAN_UNMAP_spec() -> bool {
179176
// true
180177
// }
181-
182178
// type E = MockPageTableEntry;
183-
184179
// type C = PagingConsts;
185-
186180
// type Item = VmItem;
187-
188181
// fn item_into_raw(item: Self::Item) -> (res: (Paddr, PagingLevel, PageProperty))
189182
// ensures
190183
// res == Self::item_into_raw_spec(item),
@@ -201,7 +194,6 @@ pub(crate) struct UserPtConfig {}
201194
// },
202195
// }
203196
// }
204-
205197
// open spec fn item_into_raw_spec(item: Self::Item) -> (Paddr, PagingLevel, PageProperty) {
206198
// match item {
207199
// VmItem::Frame(frame, prop) => {
@@ -215,7 +207,6 @@ pub(crate) struct UserPtConfig {}
215207
// },
216208
// }
217209
// }
218-
219210
// unsafe fn item_from_raw(
220211
// paddr: Paddr,
221212
// level: PagingLevel,
@@ -235,6 +226,5 @@ pub(crate) struct UserPtConfig {}
235226
// }
236227
// }
237228
// }
238-
239229
// TODO: TryFrom<PageTableItem> for VmItem
240230
} // verus!

0 commit comments

Comments
 (0)