pub struct CursorView<C: PageTableConfig> {
pub cur_va: Vaddr,
pub mappings: Set<Mapping>,
pub phantom: PhantomData<C>,
}Fields§
§cur_va: Vaddr§mappings: Set<Mapping>§phantom: PhantomData<C>Implementations§
Source§impl<C: PageTableConfig> CursorView<C>
A CursorView is not aware that the underlying structure of the page table is a tree.
It treats the page table as an array of mappings of various sizes, and the cursor itself as the
current virtual address, moving from low to high addresses. These functions specify its behavior
and provide a simple interface for reasoning about its behavior.
impl<C: PageTableConfig> CursorView<C>
A CursorView is not aware that the underlying structure of the page table is a tree.
It treats the page table as an array of mappings of various sizes, and the cursor itself as the
current virtual address, moving from low to high addresses. These functions specify its behavior
and provide a simple interface for reasoning about its behavior.
Sourcepub open spec fn item_into_mapping(va: Vaddr, item: C::Item) -> Mapping
pub open spec fn item_into_mapping(va: Vaddr, item: C::Item) -> Mapping
{
let (paddr, level, prop) = C::item_into_raw_spec(item);
let size = page_size(level);
Mapping {
va_range: va..(va + size) as usize,
pa_range: paddr..(paddr + size) as Paddr,
page_size: size,
property: prop,
}
}Sourcepub open spec fn present(self) -> bool
pub open spec fn present(self) -> bool
{
self
.mappings
.filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end)
.len() > 0
}This function checks if the current virtual address is mapped. It does not correspond to a cursor method itself, but defines what it means for an entry to present: there is a mapping whose virtual address range contains the current virtual address.
Sourcepub open spec fn query_mapping(self) -> Mapping
pub open spec fn query_mapping(self) -> Mapping
self.present(),{
self.mappings
.filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end)
.choose()
}Sourcepub open spec fn query(self, paddr: Paddr, size: usize, prop: PageProperty) -> bool
pub open spec fn query(self, paddr: Paddr, size: usize, prop: PageProperty) -> bool
{
let m = self.query_mapping();
m.pa_range.start == paddr && m.page_size == size && m.property == prop
}Sourcepub open spec fn query_range(self) -> Range<Vaddr>
pub open spec fn query_range(self) -> Range<Vaddr>
{ self.query_mapping().va_range }Sourcepub open spec fn cur_slot_range(self, size: usize) -> Range<Vaddr>
pub open spec fn cur_slot_range(self, size: usize) -> Range<Vaddr>
{
let start = nat_align_down(self.cur_va as nat, size as nat) as Vaddr;
start..(start as nat + size as nat) as Vaddr
}The VA range of the current slot when mapping a page of the given size. Works for both present and absent mappings: when present, equals query_range() for a mapping of that size; when absent, returns the aligned range that would be mapped.
Sourcepub open spec fn query_item_spec(self, item: C::Item) -> Option<Range<Vaddr>>
pub open spec fn query_item_spec(self, item: C::Item) -> Option<Range<Vaddr>>
self.present(),{
let (paddr, level, prop) = C::item_into_raw_spec(item);
let size = page_size(level);
if self.query(paddr, size, prop) { Some(self.query_range()) } else { None }
}This predicate specifies the behavior of the query method. It states that the current item
in the page table matches the given item, mapped at the resulting virtual address range.
Sourcepub open spec fn find_next_impl_spec(
self,
len: usize,
find_unmap_subtree: bool,
split_huge: bool,
) -> (Self, Option<Mapping>)
pub open spec fn find_next_impl_spec( self, len: usize, find_unmap_subtree: bool, split_huge: bool, ) -> (Self, Option<Mapping>)
{
let mappings_in_range = self
.mappings
.filter(|m: Mapping| self.cur_va <= m.va_range.start < self.cur_va + len);
if mappings_in_range.len() > 0 {
let mapping = mappings_in_range
.find_unique_minimal(|m: Mapping, n: Mapping| {
m.va_range.start < n.va_range.start
});
let view = CursorView {
cur_va: mapping.va_range.end,
..self
};
(view, Some(mapping))
} else {
let view = CursorView {
cur_va: (self.cur_va + len) as Vaddr,
..self
};
(view, None)
}
}The specification for the internal function, find_next_impl. It finds the next mapped virtual address
that is at most len bytes away from the current virtual address. TODO: add the specifications for
find_unmap_subtree and split_huge, which are used by other functions that call this one.
This returns a mapping rather than the address because that is useful when it’s called as a subroutine.
Sourcepub open spec fn find_next_spec(self, len: usize) -> (Self, Option<Vaddr>)
pub open spec fn find_next_spec(self, len: usize) -> (Self, Option<Vaddr>)
{
let (cursor, mapping) = self.find_next_impl_spec(len, false, false);
if mapping is Some {
(cursor, Some(mapping.unwrap().va_range.start))
} else {
(cursor, None)
}
}Actual specification for find_next. The cursor finds the next mapped virtual address
that is at most len bytes away from the current virtual address, returns it, and then
moves the cursor forward to the next end of its range.
Sourcepub open spec fn jump_spec(self, va: usize) -> Self
pub open spec fn jump_spec(self, va: usize) -> Self
{
CursorView {
cur_va: va as Vaddr,
..self
}
}Jump just sets the current virtual address to the given address.
Sourcepub open spec fn align_up_spec(self, size: usize) -> Vaddr
pub open spec fn align_up_spec(self, size: usize) -> Vaddr
{ nat_align_up(self.cur_va as nat, size as nat) as Vaddr }Sourcepub open spec fn split_index(m: Mapping, new_size: usize, n: usize) -> Mapping
pub open spec fn split_index(m: Mapping, new_size: usize, n: usize) -> Mapping
{
Mapping {
va_range: (m.va_range.start + n * new_size)
as usize..(m.va_range.start + (n + 1) * new_size) as usize,
pa_range: (m.pa_range.start + n * new_size)
as usize..(m.pa_range.start + (n + 1) * new_size) as usize,
page_size: new_size,
property: m.property,
}
}Sourcepub open spec fn split_if_mapped_huge_spec(self, new_size: usize) -> Self
pub open spec fn split_if_mapped_huge_spec(self, new_size: usize) -> Self
{
let m = self.query_mapping();
let size = m.page_size;
let new_mappings = Set::<int>::new(|n: int| 0 <= n < size / new_size)
.map(|n: int| Self::split_index(m, new_size, n as usize));
CursorView {
cur_va: self.cur_va,
mappings: self.mappings - set![m] + new_mappings,
..self
}
}Sourcepub open spec fn split_while_huge(self, size: usize) -> Self
pub open spec fn split_while_huge(self, size: usize) -> Self
{
if self.present() {
let m = self.query_mapping();
if m.page_size > size {
let new_size = m.page_size.ilog2() as usize;
let new_self = self.split_if_mapped_huge_spec(new_size);
new_self.split_while_huge(size)
} else {
self
}
} else {
self
}
}Sourcepub open spec fn remove_subtree(self, size: usize) -> Set<Mapping>
pub open spec fn remove_subtree(self, size: usize) -> Set<Mapping>
{
let subtree = self
.mappings
.filter(|m: Mapping| self.cur_va <= m.va_range.start < self.cur_va + size);
self.mappings - subtree
}Sourcepub open spec fn map_spec(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self
pub open spec fn map_spec(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self
{
let new = Mapping {
va_range: self.cur_slot_range(size),
pa_range: paddr..(paddr + size) as usize,
page_size: size,
property: prop,
};
let split_self = self.split_while_huge(size);
CursorView {
cur_va: split_self.align_up_spec(size),
mappings: split_self.remove_subtree(size) + set![new],
..split_self
}
}Inserts a mapping into the cursor. If there were previously mappings there, they are removed. Note that multiple mappings might be removed if they overlap with a new large mapping.
Sourcepub open spec fn map_simple(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self
pub open spec fn map_simple(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self
{
let new = Mapping {
va_range: self.cur_slot_range(size),
pa_range: paddr..(paddr + size) as usize,
page_size: size,
property: prop,
};
CursorView {
cur_va: self.cur_va,
mappings: self.mappings + set![new],
..self
}
}Sourcepub open spec fn unmap_spec(self, len: usize, new_view: Self, num_unmapped: usize) -> bool
pub open spec fn unmap_spec(self, len: usize, new_view: Self, num_unmapped: usize) -> bool
{
let taken = self
.mappings
.filter(|m: Mapping| self.cur_va <= m.va_range.start < self.cur_va + len);
&&& new_view.cur_va >= (self.cur_va + len) as Vaddr
&&& new_view.mappings == self.mappings - taken
&&& num_unmapped == taken.len() as usize
}Unmaps a range of virtual addresses from the current address up to len bytes.
It returns the number of mappings that were removed.
Trait Implementations§
Source§impl<C: PageTableConfig> Inv for CursorView<C>
impl<C: PageTableConfig> Inv for CursorView<C>
Source§open spec fn inv(self) -> bool
open spec fn inv(self) -> bool
{
&&& self.cur_va < MAX_USERSPACE_VADDR
&&& forall |m: Mapping| self.mappings.contains(m) ==> m.inv()
&&& forall |m: Mapping, n: Mapping| {
self.mappings.contains(m)
==> (self.mappings.contains(n)
==> (m != n
==> m.va_range.end <= n.va_range.start
|| n.va_range.end <= m.va_range.start))
}
}