ChildRef

ostd::mm::page_table

Enum ChildRef

pub enum ChildRef<'a, C: PageTableConfig> {
    PageTable(PageTableNodeRef<'a, C>),
    Frame(Paddr, PagingLevel, PageProperty),
    None,
}

Expand description

A reference to the child of a page table node.

Variants§

PageTable(PageTableNodeRef<'a, C>)

A child page table node.

Frame(Paddr, PagingLevel, PageProperty)

Physical address of a mapped physical frame.

It is associated with the virtual page property and the level of the mapping node, which decides the size of the frame.

None

Implementations§

impl<'a, C: PageTableConfig> ChildRef<'a, C>

pub fn arrow_1(self) -> PagingLevel

pub fn arrow_2(self) -> PageProperty

pub fn arrow_PageTable_0(self) -> PageTableNodeRef<'a, C>

pub fn arrow_Frame_0(self) -> Paddr

pub fn arrow_Frame_1(self) -> PagingLevel

pub fn arrow_Frame_2(self) -> PageProperty

impl<C: PageTableConfig> ChildRef<'_, C>

pub exec fn from_pte(pte: &C::E, level: PagingLevel) -> res : Self

with

Tracked(regions): Tracked <& mut MetaRegionOwners>,
Tracked(entry_owner): Tracked <& EntryOwner <C>>,

requires

entry_owner.match_pte(*pte, level),

entry_owner.inv(),

pte.paddr() % PAGE_SIZE() == 0,

pte.paddr() < MAX_PADDR(),

old(regions).inv(),

entry_owner.is_node() ==> entry_owner.node.unwrap().relate_region(*old(regions)),

ensures

regions.inv(),

res.wf(*entry_owner),

Converts a PTE to a child.

§Safety

The PTE must be the output of a Child::into_pte, where the child outlives the reference created by this function.

The provided level must be the same with the level of the page table node that contains this PTE.

Trait Implementations§

impl<'a, C: PageTableConfig> Inv for ChildRef<'a, C>

open spec fn inv(self) -> bool

{ true }

impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C>

open spec fn wf(self, owner: Self::Owner) -> bool

{
    match self {
        Self::PageTable(node) => (
            &&& owner.is_node()
            &&& manually_drop_deref_spec(&node.inner.0).ptr.addr()
                == owner.node.unwrap().meta_perm.addr()

        ),
        Self::Frame(paddr, level, prop) => (
            &&& owner.is_frame()
            &&& owner.frame.unwrap().mapped_pa == paddr
            &&& owner.frame.unwrap().prop == prop

        ),
        Self::None => owner.is_absent(),
    }
}

type Owner = EntryOwner<C>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Auto Trait Implementations§

impl<'a, C> Freeze for ChildRef<'a, C>

impl<'a, C> !RefUnwindSafe for ChildRef<'a, C>

impl<'a, C> Send for ChildRef<'a, C>

impl<'a, C> Sync for ChildRef<'a, C>

impl<'a, C> Unpin for ChildRef<'a, C>
where C: Unpin,

impl<'a, C> !UnwindSafe for ChildRef<'a, C>

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>