ostd/mm/page_table/node/
child.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module specifies the type of the children of a page table node.
3use vstd::prelude::*;
4use vstd_extra::external::manually_drop_deref_spec;
5
6use crate::mm::frame::meta::mapping::{frame_to_index, meta_to_frame};
7use crate::mm::frame::Frame;
8use crate::mm::page_table::*;
9use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
10use crate::specs::arch::paging_consts::PagingConsts;
11use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
12
13use vstd_extra::cast_ptr::*;
14use vstd_extra::ownership::*;
15use vstd_extra::undroppable::*;
16
17use crate::specs::*;
18
19use crate::{
20    mm::{page_prop::PageProperty, Paddr, PagingConstsTrait, PagingLevel, Vaddr},
21    //    sync::RcuDrop,
22};
23use vstd_extra::undroppable::NeverDrop;
24
25use super::*;
26
27verus! {
28
29/// A page table entry that owns the child of a page table node if present.
30#[rustc_has_incoherent_inherent_impls]
31pub enum Child<C: PageTableConfig> {
32    /// A child page table node.
33    pub PageTable(PageTableNode<C>),
34    /// Physical address of a mapped physical frame.
35    ///
36    /// It is associated with the virtual page property and the level of the
37    /// mapping node, which decides the size of the frame.
38    pub Frame(Paddr, PagingLevel, PageProperty),
39    pub None,
40}
41
42impl<C: PageTableConfig> Child<C> {
43    pub open spec fn get_node(self) -> Option<PageTableNode<C>> {
44        match self {
45            Self::PageTable(node) => Some(node),
46            _ => None,
47        }
48    }
49
50    pub open spec fn get_frame_tuple(self) -> Option<(Paddr, PagingLevel, PageProperty)> {
51        match self {
52            Self::Frame(paddr, level, prop) => Some((paddr, level, prop)),
53            _ => None,
54        }
55    }
56
57    /// Returns whether the child is not present.
58    #[vstd::contrib::auto_spec]
59    pub fn is_none(&self) -> (b: bool) {
60        matches!(self, Child::None)
61    }
62}
63
64/// A reference to the child of a page table node.
65#[rustc_has_incoherent_inherent_impls]
66pub enum ChildRef<'a, C: PageTableConfig> {
67    /// A child page table node.
68    PageTable(PageTableNodeRef<'a, C>),
69    /// Physical address of a mapped physical frame.
70    ///
71    /// It is associated with the virtual page property and the level of the
72    /// mapping node, which decides the size of the frame.
73    Frame(Paddr, PagingLevel, PageProperty),
74    None,
75}
76
77impl<'a, C: PageTableConfig> Inv for ChildRef<'a, C> {
78    open spec fn inv(self) -> bool {
79        true
80    }
81}
82
83impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
84    type Owner = EntryOwner<C>;
85
86    open spec fn wf(self, owner: Self::Owner) -> bool {
87        match self {
88            Self::PageTable(node) => {
89                &&& owner.is_node()
90                &&& manually_drop_deref_spec(&node.inner.0).ptr.addr()
91                    == owner.node.unwrap().meta_perm.addr()
92            },
93            Self::Frame(paddr, level, prop) => {
94                &&& owner.is_frame()
95                &&& owner.frame.unwrap().mapped_pa == paddr
96                &&& owner.frame.unwrap().prop == prop
97            },
98            Self::None => owner.is_absent(),
99        }
100    }
101}
102
103impl<'a, C: PageTableConfig> Inv for Child<C> {
104    open spec fn inv(self) -> bool {
105        true
106    }
107}
108
109impl<C: PageTableConfig> OwnerOf for Child<C> {
110    type Owner = EntryOwner<C>;
111
112    open spec fn wf(self, owner: Self::Owner) -> bool {
113        match self {
114            Self::PageTable(node) => {
115                &&& owner.is_node()
116                &&& node.ptr.addr() == owner.node.unwrap().meta_perm.addr()
117            },
118            Self::Frame(paddr, level, prop) => {
119                &&& owner.is_frame()
120                &&& owner.frame.unwrap().mapped_pa == paddr
121                &&& owner.frame.unwrap().prop == prop
122                &&& level == owner.parent_level
123            },
124            Self::None => owner.is_absent(),
125        }
126    }
127}
128
129impl<C: PageTableConfig> Child<C> {
130    #[rustc_allow_incoherent_impl]
131    #[verus_spec(
132        with Tracked(owner): Tracked<&EntryOwner<C>>,
133            Tracked(regions): Tracked<&mut MetaRegionOwners>
134    )]
135    pub fn into_pte(self) -> (res: C::E)
136        requires
137            owner.inv(),
138            old(regions).inv(),
139            self.wf(*owner),
140        ensures
141            regions.inv(),
142            res.paddr() % PAGE_SIZE() == 0,
143            res.paddr() < MAX_PADDR(),
144            owner.match_pte(res, owner.parent_level),
145    {
146        proof {
147            C::E::new_properties();
148        }
149
150        match self {
151            Child::PageTable(node) => {
152                let ghost node_owner = owner.node.unwrap();
153
154                #[verus_spec(with Tracked(&owner.node.tracked_borrow().meta_perm.points_to))]
155                let paddr = node.start_paddr();
156
157                assert(node.constructor_requires(*old(regions))) by { admit() };
158                let _ = NeverDrop::new(node, Tracked(regions));
159                C::E::new_pt(paddr)
160            },
161            Child::Frame(paddr, level, prop) => C::E::new_page(paddr, level, prop),
162            Child::None => C::E::new_absent(),
163        }
164    }
165
166    /// # Safety
167    ///
168    /// The provided PTE must be the output of [`Self::into_pte`], and the PTE:
169    ///  - must not be used to created a [`Child`] twice;
170    ///  - must not be referenced by a living [`ChildRef`].
171    ///
172    /// The level must match the original level of the child.
173    #[verifier::external_body]
174    #[verus_spec(
175        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
176            Tracked(entry_own): Tracked<&EntryOwner<C>>,
177    )]
178    pub fn from_pte(pte: C::E, level: PagingLevel) -> (res: Self)
179        requires
180            pte.paddr() % PAGE_SIZE() == 0,
181            pte.paddr() < MAX_PADDR(),
182            old(regions).inv(),
183            entry_own.inv(),
184            entry_own.is_node() ==> entry_own.node.unwrap().relate_region(*old(regions)),
185        ensures
186            regions.inv(),
187            res.wf(*entry_own),
188            !pte.is_present() ==> res == Child::<C>::None,
189            pte.is_present() && pte.is_last(level) ==> res == Child::<C>::from_pte_frame_spec(
190                pte,
191                level,
192            ),
193            pte.is_present() && !pte.is_last(level) ==> res == Child::<C>::from_pte_pt_spec(
194                pte.paddr(),
195                *regions,
196            ),
197            entry_own.is_node() ==> entry_own.node.unwrap().relate_region(*regions),
198    {
199        if !pte.is_present() {
200            return Child::None;
201        }
202        let paddr = pte.paddr();
203
204        if !pte.is_last(level) {
205
206            // SAFETY: The caller ensures that this node was created by
207            // `into_pte`, so that restoring the forgotten reference is safe.
208            #[verus_spec(with Tracked(regions), Tracked(&entry_own.node.tracked_borrow().meta_perm))]
209            let node = PageTableNode::from_raw(paddr);
210            //            debug_assert_eq!(node.level(), level - 1);
211
212            return Child::PageTable(node);
213        }
214        Child::Frame(paddr, level, pte.prop())
215    }
216}
217
218impl<C: PageTableConfig> ChildRef<'_, C> {
219    /// Converts a PTE to a child.
220    ///
221    /// # Safety
222    ///
223    /// The PTE must be the output of a [`Child::into_pte`], where the child
224    /// outlives the reference created by this function.
225    ///
226    /// The provided level must be the same with the level of the page table
227    /// node that contains this PTE.
228    #[rustc_allow_incoherent_impl]
229    #[verus_spec(
230        with Tracked(regions): Tracked<&mut MetaRegionOwners>,
231            Tracked(entry_owner): Tracked<&EntryOwner<C>>
232    )]
233    pub fn from_pte(pte: &C::E, level: PagingLevel) -> (res: Self)
234        requires
235            entry_owner.match_pte(*pte, level),
236            entry_owner.inv(),
237            pte.paddr() % PAGE_SIZE() == 0,
238            pte.paddr() < MAX_PADDR(),
239//            !old(regions).slots.contains_key(frame_to_index(pte.paddr())),
240//            old(regions).dropped_slots.contains_key(frame_to_index(pte.paddr())),
241            old(regions).inv(),
242            entry_owner.is_node() ==> entry_owner.node.unwrap().relate_region(*old(regions)),
243        ensures
244            regions.inv(),
245            res.wf(*entry_owner),
246    {
247        if !pte.is_present() {
248            assert(entry_owner.is_absent()) by { admit() };
249            return ChildRef::None;
250        }
251        let paddr = pte.paddr();
252
253        if !pte.is_last(level) {
254
255            // SAFETY: The caller ensures that the lifetime of the child is
256            // contained by the residing node, and the physical address is
257            // valid since the entry is present.
258            #[verus_spec(with Tracked(regions), Tracked(&entry_owner.node.tracked_borrow().meta_perm))]
259            let node = PageTableNodeRef::borrow_paddr(paddr);
260
261            assert(manually_drop_deref_spec(&node.inner.0).ptr.addr()
262                == entry_owner.node.unwrap().meta_perm.addr());
263
264            // debug_assert_eq!(node.level(), level - 1);
265            return ChildRef::PageTable(node);
266        }
267
268        ChildRef::Frame(paddr, level, pte.prop())
269    }
270}
271
272} // verus!
ostd/mm/page_table/node/child.rs

ostd/mm/page_table/node/
child.rs
