Struct Page Table Entry &nbsp; Copy item path

impl PageTableEntry

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

returns

({ !PHYS_ADDR_MASK & !(PageTableFlags::HUGE()) }),

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

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

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

returns

({
    match cache {
        CachePolicy::Uncacheable => PageTableFlags::NO_CACHE(),
        CachePolicy::Writethrough => PageTableFlags::WRITE_THROUGH(),
        _ => 0,
    }
}),

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

{
    let flags: u8 = prop.flags.bits();
    let priv_flags: u8 = prop.priv_flags.bits();
    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) -> usize

returns

Self::format_flags_spec(prop),

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

returns

({
    if flags & PageTableFlags::NO_CACHE() != 0 {
        CachePolicy::Uncacheable
    } else if flags & PageTableFlags::WRITE_THROUGH() != 0 {
        CachePolicy::Writethrough
    } else {
        CachePolicy::Writeback
    }
}),

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).unwrap(),
        cache,
        priv_flags: PrivilegedPageFlags::from_bits(priv_flags).unwrap(),
    }
}

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

returns

Self::format_property_spec(entry),

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

returns

({ if level == 1 { 0 } else { PageTableFlags::HUGE() as u64 } }),

impl PageTableEntry

pub proof fn absent_pte_paddr_ok()

ensures

Self::new_absent_spec().paddr_spec() % crate::specs::arch::mm::PAGE_SIZE == 0,

Self::new_absent_spec().paddr_spec() < crate::specs::arch::mm::MAX_PADDR,

Absent (zero) PTE has well-formed paddr for match_pte.

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() -> Self

returns

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) -> usize

returns

self.as_usize_spec(),

open spec fn is_present_spec(&self) -> bool

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

exec fn is_present(&self) -> bool

returns

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

*final(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) -> Paddr

returns

self.paddr_spec(),

open spec fn prop_spec(&self) -> PageProperty

{ Self::format_property(self.0) }

exec fn prop(&self) -> PageProperty

returns

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) -> bool

returns

self.is_last_spec(level),

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 Pod for PageTableEntry

fn new_zeroed() -> Self

Creates a new instance of Pod type that is filled with zeroes.

fn new_uninit() -> Self

Creates a new instance of Pod type with uninitialized content.

fn as_bytes(&self) -> &[u8] ⓘ

As an immutable slice of bytes.

fn as_bytes_mut(&mut self) -> &mut [u8] ⓘ

As a mutable slice of bytes.

fn as_array_ptr_bytes<const N: usize>( &self, ) -> (ArrayPtr<u8, N>, Tracked<&PointsTo<u8, N>>)

As a slice of bytes via an [ArrayPtr] (with a tracked permission). Read more

impl Copy for PageTableEntry

impl PodOnce for PageTableEntry

impl StructuralPartialEq for PageTableEntry

Auto Trait Implementations§

impl Freeze for PageTableEntry

impl RefUnwindSafe for PageTableEntry

impl Send for PageTableEntry

impl Sync for PageTableEntry

impl Unpin for PageTableEntry

impl UnsafeUnpin for PageTableEntry

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

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

impl<A> SpecEq<&A> for A
where A: ?Sized,

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

impl<A> SpecEq<A> for A
where A: ?Sized,

impl<A> SpecEq<Ghost<A>> for A