PageTableEntryTrait

ostd::mm::page_table

Trait PageTableEntryTrait 

Source 
pub trait PageTableEntryTrait:
    Clone
    + Copy
    + Debug
    + Sized
    + Send
    + Sync
    + 'static {

Show 23 methods    // Required methods
    spec fn default_spec() -> Self;
    exec fn default() -> res : Self;
    spec fn new_absent_spec() -> Self;
    exec fn new_absent() -> res : Self;
    spec fn is_present_spec(&self) -> bool;
    exec fn is_present(&self) -> res : bool;
    spec fn new_page_spec(
        paddr: Paddr,
        level: PagingLevel,
        prop: PageProperty,
    ) -> Self;
    exec fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> res : Self;
    spec fn new_pt_spec(paddr: Paddr) -> Self;
    exec fn new_pt(paddr: Paddr) -> res : Self;
    proof fn new_properties();
    spec fn paddr_spec(&self) -> Paddr;
    exec fn paddr(&self) -> res : Paddr;
    spec fn prop_spec(&self) -> PageProperty;
    exec fn prop(&self) -> res : PageProperty;
    spec fn set_prop_spec(&self, prop: PageProperty) -> Self;
    exec fn set_prop(&mut self, prop: PageProperty);
    proof fn set_prop_properties(self, prop: PageProperty);
    spec fn is_last_spec(&self, level: PagingLevel) -> bool;
    exec fn is_last(&self, level: PagingLevel) -> b : bool;
    spec fn as_usize_spec(self) -> usize;

    // Provided methods
    exec fn as_usize(self) -> res : usize { ... }
    fn from_usize(pte_raw: usize) -> Self { ... }

}
Expand description

The interface for defining architecture-specific page table entries.

Note that a default PTE should be a PTE that points to nothing.

Required Methods§

Source

spec fn default_spec() -> Self

Source

exec fn default() -> res : Self

ensures
res == Self::default_spec(),

For implement Default trait.

Source

spec fn new_absent_spec() -> Self

Create a set of new invalid page table flags that indicates an absent page.

Note that currently the implementation requires an all zero PTE to be an absent PTE.

Source

exec fn new_absent() -> res : Self

ensures
res == Self::new_absent_spec(),
res.paddr() % PAGE_SIZE() == 0,
res.paddr() < MAX_PADDR(),
Source

spec fn is_present_spec(&self) -> bool

If the flags are present with valid mappings.

Source

exec fn is_present(&self) -> res : bool

ensures
res == self.is_present_spec(),
Source

spec fn new_page_spec(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self

Create a new PTE with the given physical address and flags that map to a page.

Source

exec fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> res : Self

requires
paddr % PAGE_SIZE() == 0,
paddr < MAX_PADDR(),
ensures
res == Self::new_page_spec(paddr, level, prop),
res.paddr() == paddr,
res.paddr() % PAGE_SIZE() == 0,
res.paddr() < MAX_PADDR(),
Source

spec fn new_pt_spec(paddr: Paddr) -> Self

Create a new PTE that map to a child page table.

Source

exec fn new_pt(paddr: Paddr) -> res : Self

requires
paddr % PAGE_SIZE() == 0,
paddr < MAX_PADDR(),
ensures
res == Self::new_pt_spec(paddr),
res.paddr() == paddr,
res.paddr() % PAGE_SIZE() == 0,
res.paddr() < MAX_PADDR(),
Source

proof fn new_properties()

ensures
!Self::new_absent_spec().is_present(),
forall |paddr: Paddr, level: PagingLevel, prop: PageProperty| {
    &&& Self::new_page_spec(paddr, level, prop).is_present()
    &&& Self::new_page_spec(paddr, level, prop).paddr() == paddr
    &&& Self::new_page_spec(paddr, level, prop).prop() == prop
    &&& Self::new_page_spec(paddr, level, prop).is_last(level)

},
forall |paddr: Paddr| {
    &&& Self::new_pt_spec(paddr).is_present()
    &&& Self::new_pt_spec(paddr).paddr() == paddr
    &&& forall |level: PagingLevel| !Self::new_pt_spec(paddr).is_last(level)

},
Source

spec fn paddr_spec(&self) -> Paddr

Get the physical address from the PTE. The physical address recorded in the PTE is either:

  • the physical address of the next level page table;
  • or the physical address of the page it maps to.
Source

exec fn paddr(&self) -> res : Paddr

ensures
res == self.paddr_spec(),
Source

spec fn prop_spec(&self) -> PageProperty

Source

exec fn prop(&self) -> res : PageProperty

ensures
res == self.prop_spec(),
Source

spec fn set_prop_spec(&self, prop: PageProperty) -> Self

Set the page property of the PTE.

This will be only done if the PTE is present. If not, this method will do nothing.

Source

exec fn set_prop(&mut self, prop: PageProperty)

ensures
old(self).set_prop_spec(prop) == *self,
Source

proof fn set_prop_properties(self, prop: PageProperty)

ensures
self.set_prop_spec(prop).prop() == prop,
self.set_prop_spec(prop).paddr() == self.paddr(),
self.is_present() ==> self.set_prop_spec(prop).is_present(),
forall |level: PagingLevel| {
    self.is_last(level) ==> self.set_prop_spec(prop).is_last(level)
},
Source

spec fn is_last_spec(&self, level: PagingLevel) -> bool

If the PTE maps a page rather than a child page table.

The level of the page table the entry resides is given since architectures like amd64 only uses a huge bit in intermediate levels.

Source

exec fn is_last(&self, level: PagingLevel) -> b : bool

ensures
b == self.is_last_spec(level),
Source

spec fn as_usize_spec(self) -> usize

Converts the PTE into its corresponding usize value.

Provided Methods§

Source

exec fn as_usize(self) -> res : usize

ensures
res == self.as_usize_spec(),
Source

exec fn from_usize(pte_raw: usize) -> Self

Converts a usize pte_raw into a PTE.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§