pub unsafe trait NonNullPtr: Sized + 'static {
type Target;
// Required methods
exec fn ALIGN_BITS() -> u32;
exec fn into_raw(
self,
) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>);
unsafe fn from_raw(
ptr: NonNull<Self::Target>,
perm: Tracked<SmartPtrPointsTo<Self::Target>>,
) -> Self;
spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool;
spec fn ptr_mut_spec(self) -> *mut Self::Target;
}Expand description
A trait that abstracts non-null pointers.
All common smart pointer types such as Box<T>, Arc<T>, and Weak<T>
implement this trait as they can be converted to and from the raw pointer
type of *const T.
§Safety
This trait must be implemented correctly (according to the doc comments for
each method). Types like Rcu rely on this assumption to safely use the
raw pointers.
Required Associated Types§
Required Methods§
Sourceexec fn ALIGN_BITS() -> u32
exec fn ALIGN_BITS() -> u32
The power of two of the pointer alignment.
Sourceexec fn into_raw(
self,
) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>)
exec fn into_raw( self, ) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>)
ptr_mut_from_nonnull(ret) == self.ptr_mut_spec(),ptr_mut_from_nonnull(ret) == perm@.ptr(),perm@.inv(),Self::match_points_to_type(perm@),Converts to a raw pointer.
Each call to into_raw must be paired with a call to from_raw
in order to avoid memory leakage.
The lower Self::ALIGN_BITS of the raw pointer is guaranteed to
be zero. In other words, the pointer is guaranteed to be aligned to
1 << Self::ALIGN_BITS.
VERUS LIMITATION: the #[verus_spec] attribute does not support with in trait yet.
SOUNDNESS: Considering also returning the Dealloc permission to ensure no memory leak.
Sourceunsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
perm: Tracked<SmartPtrPointsTo<Self::Target>>,
) -> ret : Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, perm: Tracked<SmartPtrPointsTo<Self::Target>>, ) -> ret : Self
Self::match_points_to_type(perm@),ptr_mut_from_nonnull(ptr) == perm@.ptr(),perm@.inv(),ptr_mut_from_nonnull(ptr) == ret.ptr_mut_spec(),Converts back from a raw pointer.
§Safety
- The raw pointer must have been previously returned by a call to
into_raw. - The raw pointer must not be used after calling
from_raw.
Note that the second point is a hard requirement: Even if the
resulting value has not (yet) been dropped, the pointer cannot be
used because it may break Rust aliasing rules (e.g., Box<T>
requires the pointer to be unique and thus never aliased).
VERIFICATION DESIGN: It’s easy to verify the second point by consuming the permission produced by into_raw,
so we can do nothing with the raw pointer because of the absence of permission.
VERUS LIMITATION: the #[verus_spec] attribute does not support with in trait yet.
SOUNDNESS: Considering consuming the Dealloc permission to ensure no double free.
Sourcespec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool
spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool
Sourcespec fn ptr_mut_spec(self) -> *mut Self::Target
spec fn ptr_mut_spec(self) -> *mut Self::Target
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<T: 'static> NonNullPtr for Box<T>
impl<T: 'static> NonNullPtr for Box<T>
Source§exec fn ALIGN_BITS() -> u32
exec fn ALIGN_BITS() -> u32
Source§exec fn into_raw(
self,
) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>)
exec fn into_raw( self, ) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>)
Source§unsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
verus_tmp_perm: Tracked<SmartPtrPointsTo<Self::Target>>,
) -> Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, verus_tmp_perm: Tracked<SmartPtrPointsTo<Self::Target>>, ) -> Self
Source§open spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool
open spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool
{ perm is Box }Source§open spec fn ptr_mut_spec(self) -> *mut Self::Target
open spec fn ptr_mut_spec(self) -> *mut Self::Target
{ box_pointer_spec(self) }type Target = T
Source§impl<T: 'static> NonNullPtr for Arc<T>
impl<T: 'static> NonNullPtr for Arc<T>
Source§exec fn ALIGN_BITS() -> u32
exec fn ALIGN_BITS() -> u32
Source§exec fn into_raw(
self,
) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>)
exec fn into_raw( self, ) -> (NonNull<Self::Target>, Tracked<SmartPtrPointsTo<Self::Target>>)
Source§unsafe exec fn from_raw(
ptr: NonNull<Self::Target>,
verus_tmp_perm: Tracked<SmartPtrPointsTo<Self::Target>>,
) -> Self
unsafe exec fn from_raw( ptr: NonNull<Self::Target>, verus_tmp_perm: Tracked<SmartPtrPointsTo<Self::Target>>, ) -> Self
Source§open spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool
open spec fn match_points_to_type(perm: SmartPtrPointsTo<Self::Target>) -> bool
{ perm is Arc }Source§open spec fn ptr_mut_spec(self) -> *mut Self::Target
open spec fn ptr_mut_spec(self) -> *mut Self::Target
{ arc_pointer_spec(self) as *mut Self::Target }