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} // verus!
163/// A wrapper around `Box::into_raw` that also returns the permission to access the memory.
164///
165/// Soundness: it is unsound to create a `ptr` method for `Box<T>` that returns the raw pointer without the permission.
166/// As Verus only compares the value of the `Box<T>` for equality, so the following code will be wrongly verified:
167/// ```rust
168/// let b1 = Box::new(1);
169/// let b2 = Box::new(1);
170/// assert(b1.ptr() == b2.ptr()); // this will be verified but is actually not true, as b1 and b2 are different allocations with different pointers.
171/// ```
172// VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an external_body function
173// The memory layout ensures that Box<T> has the following properties:
174//  1. The pointer is aligned.
175//  2. The pointer is non-null even for zero-sized types.
176//  3. The pointer points to a valid value, whose layout is determined by Layout::for_value (exactly size_of::<T>() and align_of::<T>()).
177// See https://doc.rust-lang.org/stable/std/boxed/index.html
178// Its guarantee is actually much stronger than PointsTowithDealloc.inv().
179#[verifier::external_body]
180#[verus_spec(ret =>
181    with
182        -> perm: Tracked<(PointsTo<T>, Option<Dealloc>)>,
183    ensures
184        ret == perm@.0.ptr(),
185        perm@.0.ptr().addr() != 0,
186        perm@.0.is_init(),
187        perm@.0.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
188        perm@.0.value() == *b,
189        match perm@.1 {
190            Some(dealloc) => {
191                &&& vstd::layout::size_of::<T>() > 0
192                &&& dealloc.addr() == perm@.0.ptr().addr()
193                &&& dealloc.size() == vstd::layout::size_of::<T>()
194                &&& dealloc.align() == vstd::layout::align_of::<T>()
195                &&& dealloc.provenance() == perm@.0.ptr()@.provenance
196                &&& valid_layout(size_of::<T>(), align_of::<T>())
197            },
198            None => { &&& vstd::layout::size_of::<T>() == 0 },
199        }
200)]
201pub fn box_into_raw<T>(b: Box<T>) -> *mut T {
202    proof_with!(|= Tracked::assume_new());
203    Box::into_raw(b)
204}
205
206#[verifier::external_body]
207#[verus_spec(ret =>
208    with
209        Tracked(points_to): Tracked<PointsTo<T>>,
210        Tracked(dealloc): Tracked<Option<Dealloc>>,
211    requires
212        ptr@.addr != 0,
213        points_to.ptr() == ptr,
214        points_to.is_init(),
215        points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
216        match dealloc@ {
217            Some(dealloc) => {
218                &&& vstd::layout::size_of::<T>() > 0
219                &&& dealloc.addr() == ptr@.addr
220                &&& dealloc.size() == vstd::layout::size_of::<T>()
221                &&& dealloc.align() == vstd::layout::align_of::<T>()
222                &&& dealloc.provenance() == ptr@.provenance
223                &&& valid_layout(size_of::<T>(), align_of::<T>())
224            },
225            None => { &&& vstd::layout::size_of::<T>() == 0 },
226        },
227    ensures
228        *ret == points_to.value(),
229    )]
230pub unsafe fn box_from_raw<T>(ptr: *mut T) -> Box<T> {
231    unsafe { Box::from_raw(ptr) }
232}
233
234/// A wrapper around `Arc::into_raw` that also returns the permission to access the memory.
235///
236/// Soundness: the soundness concern is similar to `box_into_raw`.
237// VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an external_body function
238// `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.
239#[verifier::external_body]
240#[verus_spec(ret =>
241    with
242        -> perm: Tracked<ArcPointsTo<T>>,
243    ensures
244        ret == perm@.ptr(),
245        perm@.ptr().addr() != 0,
246        perm@.is_init(),
247        perm@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
248        perm@.value() == *p,
249)]
250pub fn arc_into_raw<T>(p: Arc<T>) -> *const T {
251    proof_with!(|= Tracked::assume_new());
252    Arc::into_raw(p)
253}
254
255/// 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.
256/// In verification this responsibility is dispatched to casting the `PointsTo<T>` appropriately, which is not handled here.
257#[verifier::external_body]
258#[verus_spec(ret =>
259    with
260        Tracked(points_to): Tracked<ArcPointsTo<T>>,
261    requires
262        ptr.addr() != 0,
263        points_to.ptr() == ptr,
264        points_to.is_init(),
265        points_to.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
266    ensures
267        *ret == points_to.value(),
268)]
269pub unsafe fn arc_from_raw<T>(ptr: *const T) -> Arc<T> {
270    unsafe { Arc::from_raw(ptr) }
271}
272
273verus! {
274
275/// A permission that is equivalent to `&BoxPointsTo<T>`.
276pub tracked struct BoxPointsToRef<'a, T>(pub &'a BoxPointsTo<T>);
277
278impl<'a, T> View for BoxPointsToRef<'a, T> {
279    type V = BoxPointsTo<T>;
280
281    open spec fn view(&self) -> BoxPointsTo<T> {
282        *self.0
283    }
284}
285
286impl<'a, T> Inv for BoxPointsToRef<'a, T> {
287    open spec fn inv(self) -> bool {
288        self@.inv()
289    }
290}
291
292impl<'a, T> BoxPointsToRef<'a, T> {
293    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &'a PointsTo<T>)
294        returns
295            self@.perm.points_to,
296    {
297        self.0.tracked_borrow_points_to()
298    }
299}
300
301} // verus!
vstd_extra/external/smart_ptr.rs

vstd_extra/external/
smart_ptr.rs
