ostd/mm/
mod.rs

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

ostd/mm/
mod.rs
