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

ostd/sync/rcu/non_null/
mod.rs
