Skip to main content

vaddr_range_spec

ostd::specs::mm::page_table

Function vaddr_range_spec 

Source 
pub open spec fn vaddr_range_spec<C: PageTableConfig>() -> RangeInclusive<Vaddr>
Expand description
{
    let off = pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat;
    let lb = C::LEADING_BITS_spec() as int;
    let base = lb * 0x1_0000_0000_0000int;
    let start = (base + (C::TOP_LEVEL_INDEX_RANGE().start) * pow2(off)) as usize;
    let end = (base + (C::TOP_LEVEL_INDEX_RANGE().end) * pow2(off) - 1) as usize;
    start..=end
}

Canonical bounds of the VA range managed by a page-table config,

Derived from LEADING_BITS_spec and TOP_LEVEL_INDEX_RANGE. For UserPtConfig (LEADING_BITS=0, idx=0..256) this is (0, 2^47 - 1); for KernelPtConfig (LEADING_BITS=0xffff, idx=256..512) this is (0xffff_8000_0000_0000, 0xffff_ffff_ffff_ffff).