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

ostd/mm/frame/
frame_ref.rs
