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

vstd_extra/external/
smart_ptr.rs
