ostd/specs/arch/x86_64/
mm.rs

1use vstd::prelude::*;
2
3use vstd_extra::prelude::*;
4
5use core::ops::Range;
6
7use super::*;
8use crate::mm::{Paddr, Vaddr, page_prop::CachePolicy};
9
10verus! {
11
12/// Page size.
13pub const PAGE_SIZE: usize = 4096;
14
15/// The maximum number of entries in a page table node
16pub const NR_ENTRIES: usize = 512;
17
18/// The maximum level of a page table node.
19pub const NR_LEVELS: usize = 4;
20
21/// Parameterized maximum physical address.
22pub const MAX_PADDR: usize = 0x8000_0000;
23
24pub const MAX_NR_PAGES: u64 = (MAX_PADDR / PAGE_SIZE) as u64;
25
26/// The maximum virtual address of user space (non inclusive).
27pub const MAX_USERSPACE_VADDR: Vaddr = 0x0000_8000_0000_0000_usize - PAGE_SIZE;
28
29/// The kernel address space.
30/// There are the high canonical addresses defined in most 48-bit width
31/// architectures.
32pub const KERNEL_VADDR_RANGE: Range<Vaddr> =
33    0xffff_8000_0000_0000_usize..0xffff_ffff_ffff_0000_usize;
34
35pub uninterp spec fn current_page_table_paddr_spec() -> Paddr;
36
37/// Activates the given level 4 page table.
38/// The cache policy of the root page table node is controlled by `root_pt_cache`.
39///
40/// # Safety
41///
42/// Changing the level 4 page table is unsafe, because it's possible to violate memory safety by
43/// changing the page mapping.
44#[verifier::external_body]
45pub unsafe fn activate_page_table(root_paddr: Paddr, root_pt_cache: CachePolicy) {
46    unimplemented!()
47}
48
49#[verifier::external_body]
50#[verifier::when_used_as_spec(current_page_table_paddr_spec)]
51#[verus_spec(
52    returns
53        current_page_table_paddr_spec(),
54)]
55pub fn current_page_table_paddr() -> Paddr {
56    unimplemented!()
57}
58
59} // verus!
60verus! {
61
62/// Flush any TLB entry that contains the map of the given virtual address.
63///
64/// This flush performs regardless of the global-page bit. So it can flush both global
65/// and non-global entries.
66#[verifier::external_body]
67pub fn tlb_flush_addr(vaddr: Vaddr) {
68    // tlb::flush(VirtAddr::new(vaddr as u64));
69    unimplemented!()
70}
71
72/// Flush any TLB entry that intersects with the given address range.
73#[verifier::external_body]
74pub fn tlb_flush_addr_range(range: &Range<Vaddr>) {
75    for vaddr in range.clone().step_by(PAGE_SIZE) {
76        tlb_flush_addr(vaddr);
77    }
78}
79
80/// Flush all TLB entries except for the global-page entries.
81#[verifier::external_body]
82pub fn tlb_flush_all_excluding_global() {
83    // tlb::flush_all();
84    unimplemented!()
85}
86
87/// Flush all TLB entries, including global-page entries.
88#[verifier::external_body]
89pub fn tlb_flush_all_including_global() {
90    // SAFETY: updates to CR4 here only change the global-page bit, the side effect
91    // is only to invalidate the TLB, which doesn't affect the memory safety.
92    // unsafe {
93    //     // To invalidate all entries, including global-page
94    //     // entries, disable global-page extensions (CR4.PGE=0).
95    //     x86_64::registers::control::Cr4::update(|cr4| {
96    //         *cr4 -= x86_64::registers::control::Cr4Flags::PAGE_GLOBAL;
97    //     });
98    //     x86_64::registers::control::Cr4::update(|cr4| {
99    //         *cr4 |= x86_64::registers::control::Cr4Flags::PAGE_GLOBAL;
100    //     });
101    // }
102    unimplemented!()
103}
104
105} // verus!
ostd/specs/arch/x86_64/mm.rs

ostd/specs/arch/x86_64/
mm.rs
