Struct Page Table Entry &nbsp; Copy item path

impl PageTableEntry

pub const exec fn PROP_MASK() -> res : usize

pub open spec fn prop_assign_spec(self, flags: usize) -> Self

{ Self((self.0 & !Self::PROP_MASK()) | flags as usize) }

pub exec fn prop_assign(&mut self, flags: usize)

ensures

self.0 == old(self).prop_assign_spec(flags).0,

pub exec fn encode_cache(cache: CachePolicy) -> res : usize

pub open spec fn format_flags_spec(prop: PageProperty) -> usize

{
    let flags: u8 = prop.flags.value();
    let priv_flags: u8 = prop.priv_flags.value();
    PageTableFlags::PRESENT() | flags.map_forward(&PAGE_FLAG_MAPPING)
        | flags.map_invert_forward(&PAGE_INVERTED_FLAG_MAPPING)
        | priv_flags.map_forward(&PAGE_PRIV_MAPPING) | Self::encode_cache(prop.cache)
}

pub exec fn format_flags(prop: PageProperty) -> res : usize

ensures

res == Self::format_flags_spec(prop),

pub exec fn format_cache(flags: usize) -> res : CachePolicy

pub open spec fn format_property_spec(entry: usize) -> PageProperty

{
    let flags: u8 = entry.map_backward(&PAGE_FLAG_MAPPING)
        | entry.map_invert_backward(&PAGE_INVERTED_FLAG_MAPPING);
    let priv_flags: u8 = entry.map_backward(&PAGE_PRIV_MAPPING);
    let cache = Self::format_cache(entry);
    PageProperty {
        flags: PageFlags::from_bits(flags),
        cache,
        priv_flags: PrivilegedPageFlags::from_bits(priv_flags),
    }
}

pub exec fn format_property(entry: usize) -> res : PageProperty

ensures

res == Self::format_property_spec(entry),

pub exec fn format_huge_page(level: PagingLevel) -> res : u64

Trait Implementations§

impl Clone for PageTableEntry

exec fn clone(&self) -> Self

1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more

impl Debug for PageTableEntry

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

impl PageTableEntryTrait for PageTableEntry

open spec fn default_spec() -> Self

{ Self { 0: 0 } }

exec fn default() -> res : Self

ensures

res == Self::default_spec(),

open spec fn new_absent_spec() -> Self

{ Self::default_spec() }

exec fn new_absent() -> res : Self

open spec fn as_usize_spec(self) -> usize

{ self.0 as usize }

exec fn as_usize(self) -> res : usize

ensures

res == self.as_usize_spec(),

open spec fn is_present_spec(&self) -> bool

{ self.0 & PageTableFlags::PRESENT() != 0 }

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

ensures

res == self.is_present_spec(),

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

{
    let flags = Self::format_flags(prop);
    self.prop_assign_spec(flags)
}

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

ensures

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

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

{
    let addr = paddr & PHYS_ADDR_MASK();
    let hp = Self::format_huge_page(level) as usize;
    let flags = Self::format_flags(prop) as usize;
    Self(addr | hp | flags)
}

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

open spec fn new_pt_spec(paddr: Paddr) -> Self

{
    let addr = paddr & PHYS_ADDR_MASK();
    Self(
        addr | PageTableFlags::PRESENT() | PageTableFlags::WRITABLE()
            | PageTableFlags::USER(),
    )
}

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

open spec fn paddr_spec(&self) -> Paddr

{ self.0 & PHYS_ADDR_MASK() }

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

ensures

res == self.paddr_spec(),

open spec fn prop_spec(&self) -> PageProperty

{ Self::format_property(self.0) }

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

ensures

res == self.prop_spec(),

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

{ level == 1 || (self.0 & PageTableFlags::HUGE() != 0) }

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

ensures

res == self.is_last_spec(level),

proof fn set_prop_properties(self, prop: PageProperty)

proof fn new_properties()

fn from_usize(pte_raw: usize) -> Self

impl PartialEq for PageTableEntry

fn eq(&self, other: &PageTableEntry) -> bool

Tests for self and other values to be equal, and is used by ==.

1.0.0 · Source§

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for PageTableEntry

impl StructuralPartialEq for PageTableEntry

Auto Trait Implementations§

impl UnwindSafe for PageTableEntry

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> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. 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 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 for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<A, Rhs> PartialEqIs<Rhs> for A
where A: PartialEq<Rhs> + ?Sized, Rhs: ?Sized,

fn is_eq(&self, other: &Rhs) -> bool

fn is_ne(&self, other: &Rhs) -> bool

impl<Rhs, VERUS_SPEC__A> PartialEqSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: PartialEq<Rhs> + ?Sized, Rhs: ?Sized,

fn obeys_eq_spec() -> bool

fn eq_spec(&self, other: &Rhs) -> bool

impl<T> ToOwned for T
where T: Clone,

type Owned = T

The resulting type after obtaining ownership.

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more

impl<T, U> TryFrom 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>::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 for T
where U: TryFrom<T>,

type Error = >::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, >::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 for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool