vstd_extra/external/
smart_ptr.rs

1use crate::ownership::*;
2use crate::raw_ptr_extra::*;
3use alloc::sync::Arc;
4use vstd::layout::valid_layout;
5use vstd::prelude::*;
6use vstd::raw_ptr::*;
7
8// A unified interface for the raw ptr permission returned by `into_raw` methods of smart pointers like `Box` and `Arc`.
9verus! {
10
11/// A verification-only trait that abstracts the permission that tracks both the pointer and the value it points to.
12pub trait PtrPointsToTrait {
13    /// The type of the pointer.
14    type Ptr;
15
16    /// The type of the value that the pointer points to.
17    type Target;
18
19    spec fn ptr(self) -> *mut Self::Target;
20
21    spec fn view_target(self) -> Self::Target;
22}
23
24impl<T> PtrPointsToTrait for BoxPointsTo<T> {
25    type Ptr = Box<T>;
26
27    type Target = T;
28
29    open spec fn ptr(self) -> *mut T {
30        self.perm.ptr()
31    }
32
33    open spec fn view_target(self) -> T {
34        self.perm.value()
35    }
36}
37
38impl<T> PtrPointsToTrait for ArcPointsTo<T> {
39    type Ptr = Arc<T>;
40
41    type Target = T;
42
43    open spec fn ptr(self) -> *mut T {
44        self.perm.ptr()
45    }
46
47    open spec fn view_target(self) -> T {
48        self.perm.value()
49    }
50}
51
52// The permission to access memory given by the `into_raw` methods of smart pointers like `Box` and `Arc`.
53/// For `Box<T>`, the `into_raw` method gives you the ownership of the memory
54pub tracked struct BoxPointsTo<T> {
55    pub perm: PointsTowithDealloc<T>,
56}
57
58/// For `Arc<T>`, the `into_raw` method gives shared access to the memory, and the reference count is not decreased,
59/// so the value will not be deallocated until we convert back to `Arc<T>` and drop it.
60/// See <https://doc.rust-lang.org/src/alloc/sync.rs.html#1480>.
61pub tracked struct ArcPointsTo<T: 'static> {
62    pub perm: &'static PointsTo<T>,
63}
64
65impl<T> BoxPointsTo<T> {
66    pub open spec fn perm(self) -> PointsTowithDealloc<T> {
67        self.perm
68    }
69
70    pub open spec fn ptr(self) -> *mut T {
71        self.perm.ptr()
72    }
73
74    pub open spec fn addr(self) -> usize {
75        self.ptr().addr()
76    }
77
78    pub open spec fn is_init(self) -> bool {
79        self.perm.is_init()
80    }
81
82    pub open spec fn value(self) -> T {
83        self.perm.value()
84    }
85
86    pub proof fn tracked_get_points_to_with_dealloc(tracked self) -> (tracked ret:
87        PointsTowithDealloc<T>)
88        returns
89            self.perm,
90    {
91        self.perm
92    }
93
94    pub proof fn tracked_borrow_points_to_with_dealloc(tracked &self) -> (tracked ret:
95        &PointsTowithDealloc<T>)
96        returns
97            &self.perm,
98    {
99        &self.perm
100    }
101
102    pub proof fn tracked_get_points_to(tracked self) -> (tracked ret: PointsTo<T>)
103        returns
104            self.perm.points_to,
105    {
106        self.tracked_get_points_to_with_dealloc().tracked_get_points_to()
107    }
108
109    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &PointsTo<T>)
110        returns
111            &self.perm.points_to,
112    {
113        &self.tracked_borrow_points_to_with_dealloc().tracked_borrow_points_to()
114    }
115}
116
117impl<T> ArcPointsTo<T> {
118    pub open spec fn perm(self) -> &'static PointsTo<T> {
119        self.perm
120    }
121
122    pub open spec fn ptr(self) -> *mut T {
123        self.perm.ptr()
124    }
125
126    pub open spec fn addr(self) -> usize {
127        self.ptr().addr()
128    }
129
130    pub open spec fn is_init(self) -> bool {
131        self.perm.is_init()
132    }
133
134    pub open spec fn value(self) -> T {
135        self.perm.value()
136    }
137
138    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &'static PointsTo<T>)
139        returns
140            self.perm,
141    {
142        self.perm
143    }
144}
145
146impl<T> Inv for BoxPointsTo<T> {
147    open spec fn inv(self) -> bool {
148        &&& self.perm.inv()
149        &&& self.perm.dealloc_aligned()
150        &&& self.perm.is_init()
151    }
152}
153
154impl<T> Inv for ArcPointsTo<T> {
155    open spec fn inv(self) -> bool {
156        &&& self.addr() != 0
157        &&& self.addr() as int % vstd::layout::align_of::<T>() as int == 0
158        &&& self.perm.is_init()
159    }
160}
161
162/// A wrapper around `Box::into_raw` that also returns the permission to access the memory.
163///
164/// Soundness: it is unsound to create a `ptr` method for `Box<T>` that returns the raw pointer without the permission.
165/// As Verus only compares the value of the `Box<T>` for equality, so the following code will be wrongly verified:
166/// ```rust
167/// let b1 = Box::new(1);
168/// let b2 = Box::new(1);
169/// assert(b1.ptr() == b2.ptr()); // this will be verified but is actually not true, as b1 and b2 are different allocations with different pointers.
170/// ```
171// VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an external_body function
172// The memory layout ensures that Box<T> has the following properties:
173//  1. The pointer is aligned.
174//  2. The pointer is non-null even for zero-sized types.
175//  3. The pointer points to a valid value, whose layout is determined by Layout::for_value (exactly size_of::<T>() and align_of::<T>()).
176// See https://doc.rust-lang.org/stable/std/boxed/index.html
177// Its guarantee is actually much stronger than PointsTowithDealloc.inv().
178#[verifier::external_body]
179#[verus_spec(ret =>
180    with
181        -> perm: Tracked<(PointsTo<T>, Option<Dealloc>)>,
182    ensures
183        ret == perm@.0.ptr(),
184        perm@.0.ptr().addr() != 0,
185        perm@.0.is_init(),
186        perm@.0.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
187        perm@.0.value() == *b,
188        match perm@.1 {
189            Some(dealloc) => {
190                &&& vstd::layout::size_of::<T>() > 0
191                &&& dealloc.addr() == perm@.0.ptr().addr()
192                &&& dealloc.size() == vstd::layout::size_of::<T>()
193                &&& dealloc.align() == vstd::layout::align_of::<T>()
194                &&& dealloc.provenance() == perm@.0.ptr()@.provenance
195                &&& valid_layout(size_of::<T>(), align_of::<T>())
196            },
197            None => { &&& vstd::layout::size_of::<T>() == 0 },
198        }
199)]
200pub fn box_into_raw<T>(b: Box<T>) -> *mut T {
201    proof_with!(|= Tracked::assume_new());
202    Box::into_raw(b)
203}
204
205#[verifier::external_body]
206#[verus_spec(ret =>
207    with
208        Tracked(points_to): Tracked<PointsTo<T>>,
209        Tracked(dealloc): Tracked<Option<Dealloc>>,
210    requires
211        ptr@.addr != 0,
212        points_to.ptr() == ptr,
213        points_to.is_init(),
214        points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
215        match dealloc@ {
216            Some(dealloc) => {
217                &&& vstd::layout::size_of::<T>() > 0
218                &&& dealloc.addr() == ptr@.addr
219                &&& dealloc.size() == vstd::layout::size_of::<T>()
220                &&& dealloc.align() == vstd::layout::align_of::<T>()
221                &&& dealloc.provenance() == ptr@.provenance
222                &&& valid_layout(size_of::<T>(), align_of::<T>())
223            },
224            None => { &&& vstd::layout::size_of::<T>() == 0 },
225        },
226    ensures
227        *ret == points_to.value(),
228    )]
229pub unsafe fn box_from_raw<T>(ptr: *mut T) -> Box<T> {
230    unsafe { Box::from_raw(ptr) }
231}
232
233/// A wrapper around `Arc::into_raw` that also returns the permission to access the memory.
234///
235/// Soundness: the soundness concern is similar to `box_into_raw`.
236// VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an external_body function
237// `Arc::into_raw` will not decrease the reference count, so the memory will keep valid until we convert back to Arc<T> and drop it.
238#[verifier::external_body]
239#[verus_spec(ret =>
240    with
241        -> perm: Tracked<ArcPointsTo<T>>,
242    ensures
243        ret == perm@.ptr(),
244        perm@.ptr().addr() != 0,
245        perm@.is_init(),
246        perm@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
247        perm@.value() == *p,
248)]
249pub fn arc_into_raw<T>(p: Arc<T>) -> *const T {
250    proof_with!(|= Tracked::assume_new());
251    Arc::into_raw(p)
252}
253
254/// According to the documentation, [`Arc::from_raw`](<https://doc.rust-lang.org/std/sync/struct.Arc.html#method.from_raw>) allows transmuting between different types as long as the pointer has the same size and alignment.
255/// In verification this responsibility is dispatched to casting the `PointsTo<T>` appropriately, which is not handled here.
256#[verifier::external_body]
257#[verus_spec(ret =>
258    with
259        Tracked(points_to): Tracked<ArcPointsTo<T>>,
260    requires
261        ptr.addr() != 0,
262        points_to.ptr() == ptr,
263        points_to.is_init(),
264        points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
265    ensures
266        *ret == points_to.value(),
267)]
268pub unsafe fn arc_from_raw<T>(ptr: *const T) -> Arc<T> {
269    unsafe { Arc::from_raw(ptr) }
270}
271
272/// A permission that is equivalent to `&BoxPointsTo<T>`.
273pub tracked struct BoxPointsToRef<'a, T>(pub &'a BoxPointsTo<T>);
274
275impl<'a, T> View for BoxPointsToRef<'a, T> {
276    type V = BoxPointsTo<T>;
277
278    open spec fn view(&self) -> BoxPointsTo<T> {
279        *self.0
280    }
281}
282
283impl<'a, T> Inv for BoxPointsToRef<'a, T> {
284    open spec fn inv(self) -> bool {
285        self@.inv()
286    }
287}
288
289impl<'a, T> BoxPointsToRef<'a, T> {
290    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &'a PointsTo<T>)
291        returns
292            self@.perm.points_to,
293    {
294        self.0.tracked_borrow_points_to()
295    }
296}
297
298} // verus!
vstd_extra/external/smart_ptr.rs

vstd_extra/external/
smart_ptr.rs
