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

ostd/mm/
mod.rs
