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

ostd/mm/frame/
frame_ref.rs
