ostd/mm/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Virtual memory (VM).
3use crate::specs::arch::PAGE_SIZE;
4use core::fmt::Debug;
5use vstd::arithmetic::div_mod::group_div_basics;
6use vstd::arithmetic::div_mod::lemma_div_non_zero;
7use vstd::arithmetic::power2::*;
8use vstd::prelude::*;
9
10/// Virtual addresses.
11pub type Vaddr = usize;
12
13/// Physical addresses.
14pub type Paddr = usize;
15
16/// The level of a page table node or a frame.
17pub type PagingLevel = u8;
18
19/// The maximum value of `PagingConstsTrait::NR_LEVELS`.
20pub const MAX_NR_LEVELS: usize = 4;
21
22//pub(crate) mod dma;
23pub mod frame;
24//pub mod heap;
25pub mod io;
26pub mod kspace;
27pub(crate) mod page_prop;
28pub mod page_table;
29pub mod pod;
30pub mod tlb;
31pub mod vm_space;
32
33#[cfg(ktest)]
34mod test;
35
36use core::ops::Range;
37
38// Import types and constants from arch
39pub use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, NR_ENTRIES, NR_LEVELS};
40
41#[doc(hidden)]
42pub use crate::specs::arch::paging_consts::PagingConsts;
43
44// Re-export paddr_to_vaddr from kspace
45#[doc(hidden)]
46pub use kspace::paddr_to_vaddr;
47
48// Re-export largest_pages from page_table
49#[doc(hidden)]
50pub use page_table::largest_pages;
51
52verus! {
53
54/// The maximum virtual address of user space (non inclusive).
55///
56/// Typical 64-bit systems have at least 48-bit virtual address space.
57/// A typical way to reserve half of the address space for the kernel is
58/// to use the highest 48-bit virtual address space.
59///
60/// Also, the top page is not regarded as usable since it's a workaround
61/// for some x86_64 CPUs' bugs. See
62/// <https://github.com/torvalds/linux/blob/480e035fc4c714fb5536e64ab9db04fedc89e910/arch/x86/include/asm/page_64.h#L68-L78>
63/// for the rationale.
64/// Page size.
65pub const MAX_USERSPACE_VADDR: usize = 0x0000_8000_0000_0000 - PAGE_SIZE;
66
67/// The kernel address space.
68///
69/// There are the high canonical addresses defined in most 48-bit width
70/// architectures.
71pub const KERNEL_VADDR_RANGE: Range<Vaddr> = 0xffff_8000_0000_0000..0xffff_ffff_ffff_0000;
72
73/// Gets physical address trait
74pub trait HasPaddr {
75    /// Returns the physical address.
76    fn paddr(&self) -> Paddr;
77}
78
79/// Checks if the given address is page-aligned.
80pub const fn is_page_aligned(p: usize) -> bool {
81    (p & (PAGE_SIZE - 1)) == 0
82}
83
84#[allow(non_snake_case)]
85pub trait PagingConstsTrait: Debug + Sync {
86    spec fn BASE_PAGE_SIZE_spec() -> usize;
87
88    proof fn lemma_BASE_PAGE_SIZE_properties()
89        ensures
90            0 < Self::BASE_PAGE_SIZE_spec(),
91            is_pow2(Self::BASE_PAGE_SIZE_spec() as int),
92    ;
93
94    /// The smallest page size.
95    /// This is also the page size at level 1 page tables.
96    #[verifier::when_used_as_spec(BASE_PAGE_SIZE_spec)]
97    fn BASE_PAGE_SIZE() -> (res: usize)
98        ensures
99            res == Self::BASE_PAGE_SIZE_spec(),
100            0 < res,
101            is_pow2(res as int),
102    ;
103
104    spec fn NR_LEVELS_spec() -> PagingLevel;
105
106    /// The number of levels in the page table.
107    /// The numbering of levels goes from deepest node to the root node. For example,
108    /// the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables,
109    /// Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5
110    /// Table, respectively.
111    #[verifier::when_used_as_spec(NR_LEVELS_spec)]
112    fn NR_LEVELS() -> (res: PagingLevel)
113        ensures
114            res == Self::NR_LEVELS_spec(),
115            res > 0,
116    ;
117
118    spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel;
119
120    /// The highest level that a PTE can be directly used to translate a VA.
121    /// This affects the the largest page size supported by the page table.
122    #[verifier::when_used_as_spec(HIGHEST_TRANSLATION_LEVEL_spec)]
123    fn HIGHEST_TRANSLATION_LEVEL() -> (res: PagingLevel)
124        ensures
125            res == Self::HIGHEST_TRANSLATION_LEVEL_spec(),
126    ;
127
128    spec fn PTE_SIZE_spec() -> usize;
129
130    /// The size of a PTE.
131    #[verifier::when_used_as_spec(PTE_SIZE_spec)]
132    fn PTE_SIZE() -> (res: usize)
133        ensures
134            res == Self::PTE_SIZE_spec(),
135            is_pow2(res as int),
136            0 < res <= Self::BASE_PAGE_SIZE(),
137    ;
138
139    proof fn lemma_PTE_SIZE_properties()
140        ensures
141            0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE(),
142            is_pow2(Self::PTE_SIZE_spec() as int),
143    ;
144
145    spec fn ADDRESS_WIDTH_spec() -> usize;
146
147    /// The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS.
148    /// If it is shorter than that, the higher bits in the highest level are ignored.
149    #[verifier::when_used_as_spec(ADDRESS_WIDTH_spec)]
150    fn ADDRESS_WIDTH() -> (res: usize)
151        ensures
152            res == Self::ADDRESS_WIDTH_spec(),
153    ;
154
155    /// Whether virtual addresses are sign-extended.
156    ///
157    /// The sign bit of a [`Vaddr`] is the bit at index [`PagingConstsTrait::ADDRESS_WIDTH`] - 1.
158    /// If this constant is `true`, bits in [`Vaddr`] that are higher than the sign bit must be
159    /// equal to the sign bit. If an address violates this rule, both the hardware and OSTD
160    /// should reject it.
161    ///
162    /// Otherwise, if this constant is `false`, higher bits must be zero.
163    ///
164    /// Regardless of sign extension, [`Vaddr`] is always not signed upon calculation.
165    /// That means, `0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001` is `true`.
166    spec fn VA_SIGN_EXT_spec() -> bool;
167
168    #[verifier::when_used_as_spec(VA_SIGN_EXT_spec)]
169    fn VA_SIGN_EXT() -> bool;
170}
171
172#[verifier::inline]
173pub open spec fn nr_subpage_per_huge_spec<C: PagingConstsTrait>() -> usize {
174    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
175}
176
177/// The number of sub pages in a huge page.
178#[inline(always)]
179#[verifier::when_used_as_spec(nr_subpage_per_huge_spec)]
180pub fn nr_subpage_per_huge<C: PagingConstsTrait>() -> (res: usize)
181    ensures
182        res == nr_subpage_per_huge_spec::<C>(),
183{
184    C::BASE_PAGE_SIZE() / C::PTE_SIZE()
185}
186
187pub proof fn lemma_nr_subpage_per_huge_bounded<C: PagingConstsTrait>()
188    ensures
189        0 < nr_subpage_per_huge::<C>() <= C::BASE_PAGE_SIZE(),
190{
191    C::lemma_PTE_SIZE_properties();
192    broadcast use group_div_basics;
193
194    assert(C::PTE_SIZE() <= C::BASE_PAGE_SIZE());
195    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() <= C::BASE_PAGE_SIZE());
196    assert(C::BASE_PAGE_SIZE() / C::PTE_SIZE() > 0) by {
197        lemma_div_non_zero(C::BASE_PAGE_SIZE() as int, C::PTE_SIZE() as int);
198    };
199}
200
201} // verus!
ostd/mm/mod.rs

ostd/mm/
mod.rs
