ostd/specs/mm/page_table/cursor/
page_table_cursor_specs.rs

1use vstd::prelude::*;
2
3use vstd::set_lib::*;
4
5use vstd_extra::ownership::*;
6use vstd_extra::prelude::TreePath;
7
8use crate::mm::page_table::*;
9use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
10use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
11use crate::specs::arch::paging_consts::PagingConsts;
12use crate::specs::mm::page_table::cursor::owners::*;
13use crate::specs::mm::page_table::*;
14use crate::mm::page_prop::PageProperty;
15
16use core::ops::Range;
17
18verus! {
19
20impl<C: PageTableConfig> PageTableOwner<C> {
21    pub uninterp spec fn new_cursor_owner_spec<'rcu>(self) -> (Self, CursorOwner<'rcu, C>);
22}
23
24/// A `CursorView` is not aware that the underlying structure of the page table is a tree.
25/// It treats the page table as an array of mappings of various sizes, and the cursor itself as the
26/// current virtual address, moving from low to high addresses. These functions specify its behavior
27/// and provide a simple interface for reasoning about its behavior.
28impl<C: PageTableConfig> CursorView<C> {
29
30    /// This function checks if the current virtual address is mapped. It does not correspond
31    /// to a cursor method itself, but defines what it means for an entry to present:
32    /// there is a mapping whose virtual address range contains the current virtual address.
33    pub open spec fn present(self) -> bool {
34        self.mappings.filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end).len() > 0
35    }
36
37    /// This function specifies the behavior of the `query` method. It returns the mapping containing
38    /// the current virtual address.
39    pub open spec fn query_item_spec(self) -> Mapping
40        recommends
41            self.present(),
42    {
43        self.mappings.filter(|m: Mapping| m.va_range.start <= self.cur_va < m.va_range.end).choose()
44    }
45
46    /// The specification for the internal function, `find_next_impl`. It finds the next mapped virtual address
47    /// that is at most `len` bytes away from the current virtual address. TODO: add the specifications for
48    /// `find_unmap_subtree` and `split_huge`, which are used by other functions that call thie one.
49    /// This returns a mapping rather than the address because that is useful when it's called as a subroutine.
50    pub open spec fn find_next_impl_spec(self, len: usize, find_unmap_subtree: bool, split_huge: bool) -> (Self, Option<Mapping>) {
51        let mappings_in_range = self.mappings.filter(|m: Mapping| self.cur_va <= m.va_range.start < self.cur_va + len);
52
53        if mappings_in_range.len() > 0 {
54            let mapping = mappings_in_range.find_unique_minimal(|m: Mapping, n: Mapping| m.va_range.start < n.va_range.start);
55            let view = CursorView {
56                cur_va: mapping.va_range.end,
57                ..self
58            };
59            (view, Some(mapping))
60        } else {
61            let view = CursorView {
62                cur_va: (self.cur_va + len) as Vaddr,
63                ..self
64            };
65            (view, None)
66        }
67    }
68
69    /// Actual specification for `find_next`. The cursor finds the next mapped virtual address
70    /// that is at most `len` bytes away from the current virtual address, returns it, and then
71    /// moves the cursor forward to the next end of its range.
72    pub open spec fn find_next_spec(self, len: usize) -> (Self, Option<Vaddr>) {
73        let (cursor, mapping) = self.find_next_impl_spec(len, false, false);
74        if mapping is Some {
75            (cursor, Some(mapping.unwrap().va_range.start))
76        } else {
77            (cursor, None)
78        }
79    }
80
81    /// Jump just sets the current virtual address to the given address.
82    pub open spec fn jump_spec(self, va: usize) -> Self {
83        CursorView {
84            cur_va: va as Vaddr,
85            ..self
86        }
87    }
88
89    /// Inserts a mapping into the cursor. If there were previously mappings there,
90    /// they are removed. Note that multiple mappings might be removed if they overlap with
91    /// a new large mapping.
92    pub open spec fn map_spec(self, paddr: Paddr, size: usize, prop: PageProperty) -> Self {
93        let existing = self.mappings.filter(|m: Mapping|
94            m.va_range.start <= self.cur_va < m.va_range.end || m.va_range.start <= self.cur_va + size < m.va_range.end);
95        let new = Mapping {
96            va_range: self.cur_va..(self.cur_va + size) as usize,
97            pa_range: paddr..(paddr + size) as usize,
98            page_size: size,
99            property: prop,
100        };
101        CursorView {
102            cur_va: (self.cur_va + size) as Vaddr,
103            mappings: self.mappings.difference(existing).insert(new),
104            ..self
105        }
106    }
107
108    /// Unmaps a range of virtual addresses from the current address up to `len` bytes.
109    /// It returns the number of mappings that were removed.
110    pub open spec fn unmap_spec(self, len: usize) -> (Self, usize) {
111        let taken = self.mappings.filter(|m: Mapping|
112            self.cur_va <= m.va_range.start < self.cur_va + len);
113        (CursorView {
114            cur_va: (self.cur_va + len) as Vaddr,
115            mappings: self.mappings.difference(taken),
116            ..self
117        }, taken.len() as usize)
118    }
119
120    pub open spec fn protect_spec(self, len: usize, op: impl Fn(PageProperty) -> PageProperty) -> (Self, Option<Range<Vaddr>>) {
121        let (cursor, next) = self.find_next_impl_spec(len, false, true);
122        if next is Some {
123            // TODO: Model props in here
124            (cursor, Some(next.unwrap().va_range))
125        } else {
126            (cursor, None)
127        }
128    }
129}
130
131} // verus!
ostd/specs/mm/page_table/cursor/page_table_cursor_specs.rs

ostd/specs/mm/page_table/cursor/
page_table_cursor_specs.rs
