ostd/mm/frame/
frame_ref.rs

1// SPDX-License-Identifier: MPL-2.0
2use core::{marker::PhantomData, ops::Deref, ptr::NonNull};
3
4use vstd::prelude::*;
5use vstd::simple_pptr::PPtr;
6use vstd_extra::cast_ptr::Repr;
7use vstd_extra::drop_tracking::*;
8use vstd_extra::prelude::*;
9
10use crate::mm::frame::MetaPerm;
11use crate::mm::frame::meta::mapping::{frame_to_index, frame_to_meta, meta_to_frame};
12use crate::mm::frame::meta::{AnyFrameMeta, MetaSlot, has_safe_slot};
13use crate::mm::{Paddr, PagingLevel, Vaddr};
14use crate::specs::arch::mm::{MAX_PADDR, PAGE_SIZE};
15use crate::specs::mm::frame::meta_owners::MetaSlotStorage;
16use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
17
18use super::Frame;
19
20verus! {
21
22/// A struct that can work as `&'a Frame<M>`.
23pub struct FrameRef<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>> {
24    pub inner: ManuallyDrop<Frame<M>>,
25    pub _marker: PhantomData<&'a Frame<M>>,
26}
27
28impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Deref for FrameRef<'_, M> {
29    type Target = Frame<M>;
30
31    #[verus_spec(ensures returns &self.inner.0)]
32    fn deref(&self) -> &Self::Target {
33        &self.inner
34    }
35}
36
37#[verus_verify]
38impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> FrameRef<'_, M> {
39    /// Borrows the [`Frame`] at the physical address as a [`FrameRef`].
40    ///
41    /// Under the borrow-protocol redesign, `from_raw` mints one
42    /// `frame_obligations` entry at the slot index and `MD::new`
43    /// immediately consumes it — net-zero on the ledger across this
44    /// borrow. The slot's `ref_count` is unchanged (the existing live
45    /// reference covers the borrow's lifetime via the `'a` lifetime).
46    ///
47    /// # Safety
48    /// By providing a borrowed `MetaPerm` of the appropriate type, the
49    /// caller ensures that the frame has that type and that the
50    /// `FrameRef` will be useless if it outlives the frame.
51    #[verus_spec(r =>
52        with
53            Tracked(regions): Tracked<&mut MetaRegionOwners>,
54        requires
55            Frame::<M>::from_raw_requires_safety(*old(regions), raw),
56            old(regions).slots.contains_key(frame_to_index(raw)),
57        ensures
58            final(regions).inv(),
59            r.inner.0.ptr.addr() == frame_to_meta(raw),
60            final(regions).slot_owners =~= old(regions).slot_owners,
61            final(regions).slots == old(regions).slots,
62            final(regions).frame_obligations =~= old(regions).frame_obligations,
63    )]
64    pub(in crate::mm) unsafe fn borrow_paddr(raw: Paddr) -> Self {
65        proof {
66            broadcast use crate::mm::frame::meta::mapping::group_page_meta;
67
68            old(regions).inv_implies_correct_addr(raw);
69        }
70
71        let ghost idx = frame_to_index(raw);
72        let ghost regions0 = *regions;
73
74        proof_decl! {
75            let tracked from_raw_obl: vstd_extra::drop_tracking::DropObligation<usize>;
76        }
77        // `from_raw` mints one `frame_obligations` entry at the slot and
78        // hands back the token; the token is dropped affinely (the ledger
79        // entry is what matters). `MD::new` then consumes that entry. Net
80        // effect on the ledger: zero.
81        let frame = unsafe {
82            #[verus_spec(with Tracked(regions) => Tracked(from_raw_obl))]
83            Frame::from_raw(raw)
84        };
85
86        let inner = ManuallyDrop::new(frame, Tracked(regions));
87
88        proof {
89            // `from_raw` did `insert(idx)`; `MD::new` did `remove(idx)`.
90            // The pair is identity on the multiset.
91            assert(regions.frame_obligations =~= regions0.frame_obligations);
92        }
93
94        Self { inner, _marker: PhantomData }
95    }
96}
97
98// TODO: I moved this here to avoid having to pull the rest of `sync` into the verification.
99// Once it is pulled in, we should delete this one.
100/// A trait that abstracts non-null pointers.
101///
102/// All common smart pointer types such as `Box<T>`,  `Arc<T>`, and `Weak<T>`
103/// implement this trait as they can be converted to and from the raw pointer
104/// type of `*const T`.
105///
106/// # Safety
107///
108/// This trait must be implemented correctly (according to the doc comments for
109/// each method). Types like [`Rcu`] rely on this assumption to safely use the
110/// raw pointers.
111///
112/// [`Rcu`]: super::Rcu
113pub unsafe trait NonNullPtr: 'static + Sized + TrackDrop<State = MetaRegionOwners> {
114    /// The target type that this pointer refers to.
115    // TODO: Support `Target: ?Sized`.
116    type Target;
117
118    /// A type that behaves just like a shared reference to the `NonNullPtr`.
119    type Ref<'a>;
120
121    /// The power of two of the pointer alignment.
122    fn ALIGN_BITS() -> u32;
123
124    /// Converts to a raw pointer.
125    ///
126    /// Each call to `into_raw` must be paired with a call to `from_raw`
127    /// in order to avoid memory leakage.
128    ///
129    /// The lower [`Self::ALIGN_BITS`] of the raw pointer is guaranteed to
130    /// be zero. In other words, the pointer is guaranteed to be aligned to
131    /// `1 << Self::ALIGN_BITS`.
132    fn into_raw(self, Tracked(regions): Tracked<&mut MetaRegionOwners>) -> PPtr<Self::Target>
133        requires
134            self.constructor_requires(*old(regions)),
135    ;
136
137    /// Converts back from a raw pointer.
138    ///
139    /// # Safety
140    ///
141    /// 1. The raw pointer must have been previously returned by a call to
142    ///    `into_raw`.
143    /// 2. The raw pointer must not be used after calling `from_raw`.
144    ///
145    /// Note that the second point is a hard requirement: Even if the
146    /// resulting value has not (yet) been dropped, the pointer cannot be
147    /// used because it may break Rust aliasing rules (e.g., `Box<T>`
148    /// requires the pointer to be unique and thus _never_ aliased).
149    unsafe fn from_raw(ptr: PPtr<Self::Target>) -> Self;
150
151    /// Obtains a shared reference to the original pointer.
152    ///
153    /// # Safety
154    ///
155    /// The original pointer must outlive the lifetime parameter `'a`, and during `'a`
156    /// no mutable references to the pointer will exist.
157    unsafe fn raw_as_ref<'a>(
158        raw: PPtr<Self::Target>,
159        Tracked(regions): Tracked<&mut MetaRegionOwners>,
160    ) -> Self::Ref<'a>
161        requires
162            old(regions).inv(),
163            old(regions).slot_owners.contains_key(frame_to_index(meta_to_frame(raw.addr()))),
164    ;
165
166    /// Converts a shared reference to a raw pointer.
167    fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> PPtr<Self::Target>;
168}
169
170pub assume_specification[ usize::trailing_zeros ](_0: usize) -> u32
171;
172
173// SAFETY: `Frame` is essentially a `*const MetaSlot` that could be used as a non-null
174// `*const` pointer.
175unsafe impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + 'static> NonNullPtr for Frame<M> {
176    type Target = PhantomData<Self>;
177
178    type Ref<'a> = FrameRef<'a, M>;
179
180    fn ALIGN_BITS() -> u32 {
181        core::mem::align_of::<MetaSlot>().trailing_zeros()
182    }
183
184    fn into_raw(self, Tracked(regions): Tracked<&mut MetaRegionOwners>) -> PPtr<Self::Target> {
185        let ptr = self.ptr;
186        proof {
187            // Mint the obligation that `MD::new` will immediately
188            // consume — net-zero on the ledger; the Frame value is
189            // forgotten inside the wrapper, and `ref_count` (set by the
190            // original producer) stays elevated to balance the eventual
191            // `from_raw + drop`.
192            let tracked _ = regions.tracked_mint_frame_obligation(self.index());
193        }
194        let _ = ManuallyDrop::new(self, Tracked(regions));
195        PPtr::<Self::Target>::from_addr(ptr.addr())
196    }
197
198    unsafe fn from_raw(raw: PPtr<Self::Target>) -> Self {
199        Self { ptr: PPtr::<MetaSlot>::from_addr(raw.addr()), _marker: PhantomData }
200    }
201
202    unsafe fn raw_as_ref<'a>(
203        raw: PPtr<Self::Target>,
204        Tracked(regions): Tracked<&mut MetaRegionOwners>,
205    ) -> Self::Ref<'a> {
206        let frame = Frame::<M> {
207            ptr: PPtr::<MetaSlot>::from_addr(raw.addr()),
208            _marker: PhantomData,
209        };
210        proof {
211            let tracked _ = regions.tracked_mint_frame_obligation(frame.index());
212        }
213        let dropped = ManuallyDrop::<Frame<M>>::new(frame, Tracked(regions));
214        Self::Ref { inner: dropped, _marker: PhantomData }
215    }
216
217    fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> PPtr<Self::Target> {
218        PPtr::from_addr(ptr_ref.inner.ptr.addr())
219    }
220}
221
222} // verus!
ostd/mm/frame/frame_ref.rs

ostd/mm/frame/
frame_ref.rs
