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

ostd/specs/arch/x86_64/
mm.rs
