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

ostd/mm/frame/
frame_ref.rs
