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

ostd/mm/frame/
frame_ref.rs
