ostd/mm/frame/
frame_ref.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::{
3    prelude::*,
4    simple_pptr::{PPtr, PointsTo},
5};
6use vstd_extra::{cast_ptr::Repr, prelude::*};
7
8use crate::specs::{
9    arch::valid_frame_paddr,
10    mm::frame::{
11        frame_specs::FrameRawPerms,
12        mapping::meta_to_index,
13        meta_owners::{FracMetadataPerm, MetaSlotStorage},
14        meta_region_owners::MetaRegionOwners,
15    },
16};
17
18use super::{
19    Frame,
20    meta::{AnyFrameMeta, MetaSlot},
21};
22use crate::mm::Paddr;
23use crate::mm::frame::meta::mapping::frame_to_meta;
24use core::{marker::PhantomData, mem::ManuallyDrop, ops::Deref, ptr::NonNull};
25
26verus! {
27
28/// A struct that can work as `&'a Frame<M>`.
29// FIXME: field visibility
30pub struct FrameRef<'a, M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage>> {
31    pub inner: ManuallyDrop<Frame<M>>,
32    pub _marker: PhantomData<&'a Frame<M>>,
33}
34
35#[verus_verify]
36impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> FrameRef<'_, M> {
37    /// Borrows the [`Frame`] at the physical address as a [`FrameRef`].
38    ///
39    /// # Safety
40    /// The caller's typed frame handle supplies the metadata type; the borrow
41    /// remains tied to the lifetime of that handle.
42    #[verus_spec(r =>
43        with
44            Tracked(slot_perm): Tracked<&'static PointsTo<MetaSlot>>,
45            Tracked(metadata_perm): Tracked<&FracMetadataPerm>
46        requires
47            valid_frame_paddr(raw),
48            MetaSlot::perms_related(*slot_perm,metadata_perm.resource()),
49            slot_perm.pptr().addr() == frame_to_meta(raw),
50            slot_perm.is_init(),
51        ensures
52            r.inner@.ptr.addr() == frame_to_meta(raw),
53            r.inner@.ptr_inv(),
54            r.inner@.tracked_slot_perm@ == slot_perm,
55            r.inner@.tracked_metadata_perm@ is None,
56            MetaSlot::perms_related(r.inner@.slot_perm(), metadata_perm.resource()),
57    )]
58    pub(in crate::mm) unsafe fn borrow_paddr(raw: Paddr) -> Self {
59        proof_with!{ tracked_slot_perm: Tracked(slot_perm), tracked_metadata_perm: Tracked(None)}
60        let frame = Frame::<M> {
61            ptr: PPtr::<MetaSlot>::from_addr(frame_to_meta(raw)),
62            _marker: PhantomData,
63        };
64
65        let inner = ManuallyDrop::new(frame);
66
67        Self { inner, _marker: PhantomData }
68    }
69}
70
71impl<M: AnyFrameMeta + ?Sized + Repr<MetaSlotStorage>> Deref for FrameRef<'_, M> {
72    type Target = Frame<M>;
73
74    #[verus_spec(r => ensures *r == self.inner@)]
75    fn deref(&self) -> &Self::Target {
76        &self.inner
77    }
78}
79
80// TODO: Use NonNullPtr in `sync`.
81/// A trait that abstracts non-null pointers.
82///
83/// All common smart pointer types such as `Box<T>`,  `Arc<T>`, and `Weak<T>`
84/// implement this trait as they can be converted to and from the raw pointer
85/// type of `*const T`.
86///
87/// # Safety
88///
89/// This trait must be implemented correctly (according to the doc comments for
90/// each method). Types like [`Rcu`] rely on this assumption to safely use the
91/// raw pointers.
92///
93/// [`Rcu`]: super::Rcu
94pub unsafe trait NonNullPtr: 'static + Sized {
95    /// The target type that this pointer refers to.
96    // TODO: Support `Target: ?Sized`.
97    type Target;
98
99    #[cfg(not(feature = "irc11"))]
100    type Permission: Inv;
101
102    #[cfg(feature = "irc11")]
103    type Permission: Inv + vstd::thread_view::Objective;
104
105    /// A type that behaves just like a shared reference to the `NonNullPtr`.
106    type Ref<'a>;
107
108    /// The power of two of the pointer alignment.
109    const ALIGN_BITS: u32;
110
111    /// Converts to a raw pointer.
112    ///
113    /// Each call to `into_raw` must be paired with a call to `from_raw`
114    /// in order to avoid memory leakage.
115    ///
116    /// The lower [`Self::ALIGN_BITS`] of the raw pointer is guaranteed to
117    /// be zero. In other words, the pointer is guaranteed to be aligned to
118    /// `1 << Self::ALIGN_BITS`.
119    fn into_raw(self) -> ((res_ptr, perm): (PPtr<Self::Target>, Tracked<Self::Permission>))
120        ensures
121            Self::ptr_perm_match(res_ptr, perm@),
122            self.rel_perm(perm@),
123            perm@.inv(),
124            res_ptr.addr() % (1usize << Self::ALIGN_BITS) == 0,
125    ;
126
127    /// Converts back from a raw pointer.
128    ///
129    /// # Safety
130    ///
131    /// 1. The raw pointer must have been previously returned by a call to
132    ///    `into_raw`.
133    /// 2. The raw pointer must not be used after calling `from_raw`.
134    ///
135    /// Note that the second point is a hard requirement: Even if the
136    /// resulting value has not (yet) been dropped, the pointer cannot be
137    /// used because it may break Rust aliasing rules (e.g., `Box<T>`
138    /// requires the pointer to be unique and thus _never_ aliased).
139    unsafe fn from_raw(ptr: PPtr<Self::Target>, perm: Tracked<Self::Permission>) -> (ret: Self)
140        requires
141            Self::ptr_perm_match(ptr, perm@),
142            perm@.inv(),
143        ensures
144            ret.rel_perm(perm@),
145    ;
146
147    /// Obtains a shared reference to the original pointer.
148    ///
149    /// # Safety
150    ///
151    /// The original pointer must outlive the lifetime parameter `'a`, and during `'a`
152    /// no mutable references to the pointer will exist.
153    unsafe fn raw_as_ref<'a>(raw: PPtr<Self::Target>) -> Self::Ref<'a>;
154
155    /// Converts a shared reference to a raw pointer.
156    fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> PPtr<Self::Target>;
157
158    /// A specification function that constraints the nonnull pointer and the permission returned by `into_raw`.
159    /// This design is to support the tagged pointer trick used in `Either`.
160    spec fn ptr_perm_match(ptr: PPtr<Self::Target>, perm: Self::Permission) -> bool;
161
162    /// A specification function that relates the original smart pointer and the permission.
163    spec fn rel_perm(self, perm: Self::Permission) -> bool;
164}
165
166// SAFETY: `Frame` is essentially a `*const MetaSlot` that could be used as a non-null
167// `*const` pointer.
168unsafe impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + 'static> NonNullPtr for Frame<M> {
169    type Target = PhantomData<Self>;
170
171    type Permission = FrameRawPerms;
172
173    type Ref<'a> = FrameRef<'a, M>;
174
175    #[verifier::external_body]
176    const ALIGN_BITS: u32 = core::mem::align_of::<MetaSlot>().trailing_zeros();
177
178    fn into_raw(mut self) -> (PPtr<Self::Target>, Tracked<Self::Permission>) {
179        assume(self.inv());
180        proof_decl! {
181            let tracked perm = FrameRawPerms {
182                slot_perm: *self.tracked_slot_perm.borrow(),
183                metadata_perm: self.tracked_metadata_perm.tracked_take(),
184            };
185        }
186        let ptr = self.ptr;
187        let _ = ManuallyDrop::new(self);
188        assume(ptr.addr() % (1usize << Self::ALIGN_BITS) == 0);
189        (PPtr::<Self::Target>::from_addr(ptr.addr()), Tracked(perm))
190    }
191
192    unsafe fn from_raw(raw: PPtr<Self::Target>, Tracked(perm): Tracked<Self::Permission>) -> Self {
193        Self {
194            ptr: PPtr::<MetaSlot>::from_addr(raw.addr()),
195            _marker: PhantomData,
196            #[cfg(verus_keep_ghost_body)]
197            tracked_slot_perm: Tracked(perm.slot_perm),
198            #[cfg(verus_keep_ghost_body)]
199            tracked_metadata_perm: Tracked(Some(perm.metadata_perm)),
200        }
201    }
202
203    #[verifier::external_body]
204    unsafe fn raw_as_ref<'a>(raw: PPtr<Self::Target>) -> Self::Ref<'a> {
205        let frame = Frame::<M> {
206            ptr: PPtr::<MetaSlot>::from_addr(raw.addr()),
207            _marker: PhantomData,
208            #[cfg(verus_keep_ghost_body)]
209            tracked_slot_perm: Tracked::assume_new(),
210            #[cfg(verus_keep_ghost_body)]
211            tracked_metadata_perm: Tracked(None),
212        };
213        let dropped = ManuallyDrop::<Frame<M>>::new(frame);
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    open spec fn ptr_perm_match(ptr: PPtr<Self::Target>, perm: Self::Permission) -> bool {
222        ptr.addr() == perm.slot_perm.addr()
223    }
224
225    open spec fn rel_perm(self, perm: Self::Permission) -> bool {
226        &&& perm.slot_perm == self.slot_perm()
227        &&& perm.metadata_perm == self.frac_metadata_perm()
228    }
229}
230
231} // verus!
ostd/mm/frame/frame_ref.rs

ostd/mm/frame/
frame_ref.rs
