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

vstd_extra/external/
smart_ptr.rs
