ostd/sync/rcu/non_null/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2//! This module provides a trait and some auxiliary types to help abstract and
3//! work with non-null pointers.
4use alloc::{boxed::Box, sync::Arc};
5use vstd::prelude::*;
6use vstd::raw_ptr::*;
7use vstd_extra::prelude::*;
8
9mod either;
10
11use core::{marker::PhantomData, mem::ManuallyDrop, ops::Deref, ptr::NonNull};
12
13use crate::prelude::*;
14
15verus! {
16
17broadcast use {group_nonull_axioms, group_raw_ptr_axioms};
18
19/// A trait that abstracts non-null pointers.
20///
21/// All common smart pointer types such as `Box<T>`,  `Arc<T>`, and `Weak<T>`
22/// implement this trait as they can be converted to and from the raw pointer
23/// type of `*const T`.
24///
25/// # Safety
26///
27/// This trait must be implemented correctly (according to the doc comments for
28/// each method). Types like [`Rcu`] rely on this assumption to safely use the
29/// raw pointers.
30///
31/// [`Rcu`]: super::Rcu
32#[verus_verify]
33pub unsafe trait NonNullPtr: Sized + 'static {
34    /// The target type that this pointer refers to.
35    // TODO: Support `Target: ?Sized`.
36    type Target;
37
38    // VERUS LIMITATION: Verus does not support generic associated type with lifetime yet,
39    // so we put all methods related to the Ref associated type in the `NonNullPtrRef` trait.
40    /*/// A type that behaves just like a shared reference to the `NonNullPtr`.
41    type Ref<'a>
42    where
43        Self: 'a;*/
44    /// A verification-only permission type that represents the ownership of the memory managed by the pointer.
45    type Permission: Inv;
46
47    /// The power of two of the pointer alignment.
48    const ALIGN_BITS: u32;
49
50    /// Converts to a raw pointer.
51    ///
52    /// Each call to `into_raw` must be paired with a call to `from_raw`
53    /// in order to avoid memory leakage.
54    ///
55    /// The lower [`Self::ALIGN_BITS`] of the raw pointer is guaranteed to
56    /// be zero. In other words, the pointer is guaranteed to be aligned to
57    /// `1 << Self::ALIGN_BITS`.
58    /// VERUS LIMITATION: the #[verus_spec] attribute does not support `with` in trait yet.
59    fn into_raw(self) -> ((res_ptr, perm): (NonNull<Self::Target>, Tracked<Self::Permission>))
60        ensures
61            Self::ptr_perm_match(res_ptr.view_ptr_mut(), perm@),
62            self.rel_perm(perm@),
63            perm@.inv(),
64            res_ptr.view_ptr_mut().addr() % (1usize << Self::ALIGN_BITS) == 0,
65    ;
66
67    /// Converts back from a raw pointer.
68    ///
69    /// # Safety
70    ///
71    /// 1. The raw pointer must have been previously returned by a call to
72    ///    `into_raw`.
73    /// 2. The raw pointer must not be used after calling `from_raw`.
74    ///
75    /// Note that the second point is a hard requirement: Even if the
76    /// resulting value has not (yet) been dropped, the pointer cannot be
77    /// used because it may break Rust aliasing rules (e.g., `Box<T>`
78    /// requires the pointer to be unique and thus _never_ aliased).
79    /// VERIFICATION DESIGN: It's easy to verify the second point by consuming the permission produced by `into_raw`,
80    /// so we can do nothing with the raw pointer because of the absence of permission.
81    /// VERUS LIMITATION: the #[verus_spec] attribute does not support `with` in trait yet.
82    unsafe fn from_raw(ptr: NonNull<Self::Target>, perm: Tracked<Self::Permission>) -> (ret: Self)
83        requires
84            Self::ptr_perm_match(ptr.view_ptr_mut(), perm@),
85            perm@.inv(),
86        ensures
87            ret.rel_perm(perm@),
88    ;
89
90    /*/// Obtains a shared reference to the original pointer.
91    ///
92    /// # Safety
93    ///
94    /// The original pointer must outlive the lifetime parameter `'a`, and during `'a`
95    /// no mutable references to the pointer will exist.
96    //unsafe fn raw_as_ref<'a>(raw: NonNull<Self::Target>) -> Self::Ref<'a>;*/
97    /*/// Converts a shared reference to a raw pointer.
98    fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> NonNull<Self::Target>;*/
99    /// A specification function that constraints the nonnull pointer and the permission returned by `into_raw`.
100    /// This design is to support the tagged pointer trick used in `Either`.
101    spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool;
102
103    /// A specification function that relates the original smart pointer and the permission.
104    spec fn rel_perm(self, perm: Self::Permission) -> bool;
105
106    /// The ALIGN_BITS must be less than usize::BITS.
107    proof fn lemma_align_bits_range()
108        ensures
109            Self::ALIGN_BITS < usize::BITS,
110    ;
111}
112
113/// The trait for the associated Ref type of `NonNullPtr`, which is separated from the `NonNullPtr` trait.
114/// FIXME: This is a workaround for the lack of GAT with lifetime in Verus. We can merge this trait back to `NonNullPtr`
115/// once it is supported.
116pub unsafe trait NonNullPtrRef<'a>: NonNullPtr {
117    type Ref: 'a;
118
119    /// A verification-only permission type that represents the reading permission of the memory managed by the pointer.
120    type RefPermission: Inv;
121
122    /// The RefPermission must be able to be viewed as the owned Permission.
123    spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission;
124
125    /// A specification function that relates the `Ref` type and the `RefPermission`.
126    spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool;
127
128    /// The `RefPermission` must present the invariant of the `Permission`.
129    proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission)
130        requires
131            perm.inv(),
132        ensures
133            Self::ref_perm_view_permission(perm).inv(),
134    ;
135
136    /// Borrows a reusable reading permission from an existing reading permission.
137    proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> (tracked ret:
138        Self::RefPermission)
139        requires
140            perm.inv(),
141        ensures
142            ret.inv(),
143            Self::ref_perm_view_permission(ret) == Self::ref_perm_view_permission(*perm),
144    ;
145
146    /// Borrows a reusable reading permission from the owned permission.
147    proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> (tracked ret:
148        Self::RefPermission)
149        requires
150            perm.inv(),
151        ensures
152            ret.inv(),
153            Self::ref_perm_view_permission(ret) == *perm,
154    ;
155
156    /// Obtains a shared reference to the original pointer.
157    ///
158    /// # Safety
159    ///
160    /// The original pointer must outlive the lifetime parameter `'a`, and during `'a`
161    /// no mutable references to the pointer will exist.
162    unsafe fn raw_as_ref(raw: NonNull<Self::Target>, perm: Tracked<Self::RefPermission>) -> (ret:
163        Self::Ref)
164        requires
165            Self::ptr_perm_match(raw.view_ptr_mut(), Self::ref_perm_view_permission(perm@)),
166            perm@.inv(),
167        ensures
168            Self::ref_rel_perm(ret, perm@),
169    ;
170
171    /// Converts a shared reference to a raw pointer.
172    fn ref_as_raw(ptr_ref: Self::Ref) -> ((res_ptr, perm): (
173        NonNull<Self::Target>,
174        Tracked<Self::RefPermission>,
175    ))
176        ensures
177            Self::ref_rel_perm(ptr_ref, perm@),
178            Self::ptr_perm_match(res_ptr.view_ptr_mut(), Self::ref_perm_view_permission(perm@)),
179            perm@.inv(),
180            res_ptr.view_ptr_mut().addr() % (1usize << Self::ALIGN_BITS) == 0,
181    ;
182}
183
184/// A type that represents `&'a Box<T>`.
185#[verus_verify]
186#[derive(Debug)]
187pub struct BoxRef<'a, T> {
188    inner: *mut T,
189    _marker: PhantomData<&'a T>,
190    tracked_perm: Tracked<BoxPointsToRef<'a, T>>,
191}
192
193impl<'a, T> BoxRef<'a, T> {
194    #[verifier::type_invariant]
195    spec fn type_inv(self) -> bool {
196        &&& self.inner@.addr != 0
197        &&& self.inner@.addr as int % vstd::layout::align_of::<T>() as int == 0
198        &&& self.tracked_perm@@.ptr() == self.inner
199        &&& self.tracked_perm@.inv()
200    }
201
202    pub closed spec fn ptr(self) -> *mut T {
203        self.inner
204    }
205
206    pub closed spec fn value(self) -> T {
207        self.tracked_perm@@.value()
208    }
209}
210
211/*
212impl<T> Deref for BoxRef<'_, T> {
213    type Target = Box<T>;
214
215    fn deref(&self) -> &Self::Target {
216        // SAFETY: A `Box<T>` is guaranteed to be represented by a single pointer [1] and a shared
217        // reference to the `Box<T>` during the lifetime `'a` can be created according to the
218        // safety requirements of `NonNullPtr::raw_as_ref`.
219        //
220        // [1]: https://doc.rust-lang.org/std/boxed/#memory-layout
221        unsafe { core::mem::transmute(&self.inner) }
222    }
223}
224*/
225
226#[verus_verify]
227impl<'a, T> BoxRef<'a, T> {
228    /// Dereferences `self` to get a reference to `T` with the lifetime `'a`.
229    #[verus_spec(ret => ensures *ret == self.value())]
230    pub fn deref_target(&self) -> &'a T {
231        proof!{
232            use_type_invariant(self);
233        }
234        // [VERIFIED] SAFETY: The reference is created through `NonNullPtr::raw_as_ref`, hence
235        // the original owned pointer and target must outlive the lifetime parameter `'a`,
236        // and during `'a` no mutable references to the pointer will exist.
237
238        // The function body of ptr_ref is exactly the same as `unsafe { &*(self.inner) }`
239        //unsafe { &*(self.inner) }
240        vstd::raw_ptr::ptr_ref(
241            self.inner,
242            Tracked(self.tracked_perm.borrow().tracked_borrow_points_to()),
243        )
244    }
245}
246
247unsafe impl<T: 'static> NonNullPtr for Box<T> {
248    type Target = T;
249
250    type Permission = BoxPointsTo<T>;
251
252    /*type Ref<'a>
253        = BoxRef<'a, T>
254    where
255        Self: 'a;*/
256    #[verifier::external_body]
257    const ALIGN_BITS: u32 = core::mem::align_of::<T>().trailing_zeros();
258
259    #[verus_spec]
260    fn into_raw(self) -> (NonNull<Self::Target>, Tracked<Self::Permission>) {
261        proof_decl! {
262            let tracked perm: (PointsTo<T>, Option<Dealloc>);
263        }
264
265        //let ptr = Box::into_raw(self);
266        proof_with!(=> Tracked(perm));
267        let ptr = box_into_raw(self);
268
269        proof_decl!{
270            let tracked box_points_to = BoxPointsTo {
271                perm: PointsTowithDealloc::new(perm.0, perm.1),
272            };
273        }
274        assume(ptr.addr() % (1usize << Self::ALIGN_BITS) == 0);
275
276        // [VERIFIED] SAFETY: The pointer representing a `Box` can never be NULL.
277        (unsafe { NonNull::new_unchecked(ptr) }, Tracked(box_points_to))
278    }
279
280    #[verus_spec]
281    unsafe fn from_raw(
282        ptr: NonNull<Self::Target>,
283        Tracked(perm): Tracked<Self::Permission>,
284    ) -> Self {
285        proof_decl!{
286            let tracked perm = perm.tracked_get_points_to_with_dealloc();
287        }
288
289        let ptr = ptr.as_ptr();
290
291        // [VERIFIED] SAFETY: The safety is upheld by the caller.
292        // unsafe { Box::from_raw(ptr) }
293        unsafe {
294            proof_with!(Tracked(perm.points_to), Tracked(perm.dealloc));
295            box_from_raw(ptr)
296        }
297    }
298
299    open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool {
300        ptr == perm.ptr()
301    }
302
303    open spec fn rel_perm(self, perm: Self::Permission) -> bool {
304        perm.view_target() == *self
305    }
306
307    axiom fn lemma_align_bits_range();
308}
309
310unsafe impl<'a, T: 'static> NonNullPtrRef<'a> for Box<T> {
311    type Ref = BoxRef<'a, T>;
312
313    type RefPermission = BoxPointsToRef<'a, T>;
314
315    open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission {
316        perm@
317    }
318
319    open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool {
320        &&& r.value() == perm@.value()
321        &&& r.ptr() == perm@.ptr()
322    }
323
324    proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission) {
325    }
326
327    proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> (tracked ret:
328        Self::RefPermission) {
329        BoxPointsToRef(perm.0)
330    }
331
332    proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> (tracked ret:
333        Self::RefPermission) {
334        BoxPointsToRef(perm)
335    }
336
337    unsafe fn raw_as_ref(
338        raw: NonNull<Self::Target>,
339        perm: Tracked<Self::RefPermission>,
340    ) -> Self::Ref {
341        BoxRef { inner: raw.as_ptr(), _marker: PhantomData, tracked_perm: perm }
342    }
343
344    fn ref_as_raw(ptr_ref: Self::Ref) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>) {
345        proof!{
346            use_type_invariant(&ptr_ref);
347            assume(ptr_ref.ptr().addr() % (1usize << Self::ALIGN_BITS) == 0);
348        }
349        // [VERIFIED] SAFETY: The pointer representing a `Box` can never be NULL.
350        (unsafe { NonNull::new_unchecked(ptr_ref.inner) }, ptr_ref.tracked_perm)
351    }
352}
353
354/// A type that represents `&'a Arc<T>`.
355///
356/// Note there is no verification-only permission field, because `ArcRef` uses `Arc` instead of a raw pointer internally.
357#[verus_verify]
358#[derive(Debug)]
359pub struct ArcRef<'a, T: 'static> {
360    inner: ManuallyDrop<Arc<T>>,
361    _marker: PhantomData<&'a Arc<T>>,
362}
363
364impl<T> View for ArcRef<'_, T> {
365    type V = Arc<T>;
366
367    closed spec fn view(&self) -> Arc<T> {
368        self.inner@
369    }
370}
371
372#[verus_verify]
373impl<T> Deref for ArcRef<'_, T> {
374    type Target = Arc<T>;
375
376    #[verus_spec(ret =>
377        ensures *ret == self@
378    )]
379    fn deref(&self) -> &Self::Target {
380        &self.inner
381    }
382}
383
384#[verus_verify]
385impl<'a, T> ArcRef<'a, T> {
386    /// Dereferences `self` to get a reference to `T` with the lifetime `'a`.
387    /// VERUS LIMITATION: The code includes a cast from `&T` to `*const T`, which is not specified yet in Verus.
388    /// This is also a nontrivial use case that extends the lifetime of the reference.
389    #[verus_verify(external_body)]
390    #[verus_spec(ret => ensures *ret == *self@)]
391    pub fn deref_target(&self) -> &'a T {
392        // SAFETY: The reference is created through `NonNullPtr::raw_as_ref`, hence
393        // the original owned pointer and target must outlive the lifetime parameter `'a`,
394        // and during `'a` no mutable references to the pointer will exist.
395        unsafe { &*(self.deref().deref() as *const T) }
396    }
397}
398
399unsafe impl<T: 'static> NonNullPtr for Arc<T> {
400    type Target = T;
401
402    type Permission = ArcPointsTo<T>;
403
404    /*
405    type Ref<'a>
406        = ArcRef<'a, T>
407    where
408        Self: 'a;*/
409    #[verifier::external_body]
410    const ALIGN_BITS: u32 = core::mem::align_of::<T>().trailing_zeros();
411
412    #[verus_spec]
413    fn into_raw(self) -> (NonNull<Self::Target>, Tracked<Self::Permission>) {
414        proof_decl!{
415            let tracked perm: ArcPointsTo<T>;
416        }
417        // let ptr = Arc::into_raw(self).cast_mut();
418        let ptr = (#[verus_spec(with => Tracked(perm))]
419        arc_into_raw(self)).cast_mut();
420        assume(ptr.addr() % (1usize << Self::ALIGN_BITS) == 0);
421
422        // [VERIFIED] SAFETY: The pointer representing an `Arc` can never be NULL.
423        (unsafe { NonNull::new_unchecked(ptr) }, Tracked(perm))
424    }
425
426    unsafe fn from_raw(
427        ptr: NonNull<Self::Target>,
428        Tracked(perm): Tracked<Self::Permission>,
429    ) -> Self {
430        let ptr = ptr.as_ptr().cast_const();
431
432        // [VERIFIED] SAFETY: The safety is upheld by the caller.
433        // unsafe { Arc::from_raw(ptr) }
434        unsafe {
435            #[verus_spec(with Tracked(perm))]
436            arc_from_raw(ptr)
437        }
438    }
439
440    open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool {
441        ptr == perm.ptr()
442    }
443
444    open spec fn rel_perm(self, perm: Self::Permission) -> bool {
445        perm.view_target() == *self
446    }
447
448    axiom fn lemma_align_bits_range();
449}
450
451unsafe impl<'a, T: 'static> NonNullPtrRef<'a> for Arc<T> {
452    type Ref = ArcRef<'a, T>;
453
454    type RefPermission = ArcPointsTo<T>;
455
456    open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission {
457        perm
458    }
459
460    open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool {
461        perm.view_target() == *r@
462    }
463
464    proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission) {
465    }
466
467    proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> (tracked ret:
468        Self::RefPermission) {
469        ArcPointsTo { perm: perm.perm }
470    }
471
472    proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> (tracked ret:
473        Self::RefPermission) {
474        ArcPointsTo { perm: perm.perm }
475    }
476
477    unsafe fn raw_as_ref(
478        raw: NonNull<Self::Target>,
479        perm: Tracked<Self::RefPermission>,
480    ) -> Self::Ref {
481        unsafe {
482            ArcRef {
483                inner: ManuallyDrop::new(
484                    #[verus_spec(with perm)]
485                    arc_from_raw(raw.as_ptr()),
486                ),
487                _marker: PhantomData,
488            }
489        }
490    }
491
492    fn ref_as_raw(ptr_ref: Self::Ref) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>) {
493        NonNullPtr::into_raw(ManuallyDrop::into_inner(ptr_ref.inner))
494    }
495}
496
497} // verus!
ostd/sync/rcu/non_null/mod.rs

ostd/sync/rcu/non_null/
mod.rs
