vstd_extra/external/
smart_ptr.rs

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

vstd_extra/external/
smart_ptr.rs
