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 can be obtained from a raw pointer.
12pub trait RawPtrPerm {
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 addr(self) -> usize;
22}
23
24impl<T> RawPtrPerm 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 addr(self) -> usize {
34        self.ptr().addr()
35    }
36}
37
38impl<T> RawPtrPerm 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 addr(self) -> usize {
48        self.ptr().addr()
49    }
50}
51
52
53
54// The permission to access memory given by the `into_raw` methods of smart pointers like `Box` and `Arc`.
55/// For `Box<T>`, the `into_raw` method gives you the ownership of the memory
56pub tracked struct BoxPointsTo<T> {
57    pub perm: PointsTowithDealloc<T>,
58}
59
60/// For `Arc<T>`, the `into_raw` method gives shared access to the memory, and the reference count is not decreased,
61/// so the value will not be deallocated until we convert back to `Arc<T>` and drop it.
62/// See <https://doc.rust-lang.org/src/alloc/sync.rs.html#1480>.
63pub tracked struct ArcPointsTo<T: 'static> {
64    pub perm: &'static PointsTo<T>,
65}
66
67impl<T> BoxPointsTo<T> {
68    pub open spec fn perm(self) -> PointsTowithDealloc<T> {
69        self.perm
70    }
71
72    pub open spec fn ptr(self) -> *mut T {
73        self.perm.ptr()
74    }
75
76    pub open spec fn addr(self) -> usize {
77        self.ptr().addr()
78    }
79
80    pub open spec fn is_uninit(self) -> bool {
81        self.perm.is_uninit()
82    }
83
84    pub open spec fn is_init(self) -> bool {
85        self.perm.is_init()
86    }
87
88    pub open spec fn value(self) -> T {
89        self.perm.value()
90    }
91
92    pub proof fn tracked_get_points_to_with_dealloc(tracked self) -> (tracked ret:
93        PointsTowithDealloc<T>)
94        returns
95            self.perm,
96    {
97        self.perm
98    }
99
100    pub proof fn tracked_borrow_points_to_with_dealloc(tracked &self) -> (tracked ret:
101        &PointsTowithDealloc<T>)
102        returns
103            &self.perm,
104    {
105        &self.perm
106    }
107
108    pub proof fn tracked_get_points_to(tracked self) -> (tracked ret: PointsTo<T>)
109        returns
110            self.perm.points_to,
111    {
112        self.tracked_get_points_to_with_dealloc().tracked_get_points_to()
113    }
114
115    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &PointsTo<T>)
116        returns
117            &self.perm.points_to,
118    {
119        &self.tracked_borrow_points_to_with_dealloc().tracked_borrow_points_to()
120    }
121}
122
123impl<T> ArcPointsTo<T> {
124    pub open spec fn perm(self) -> &'static PointsTo<T> {
125        self.perm
126    }
127
128    pub open spec fn ptr(self) -> *mut T {
129        self.perm.ptr()
130    }
131
132    pub open spec fn addr(self) -> usize {
133        self.ptr().addr()
134    }
135
136    pub open spec fn is_uninit(self) -> bool {
137        self.perm.is_uninit()
138    }
139
140    pub open spec fn is_init(self) -> bool {
141        self.perm.is_init()
142    }
143
144    pub open spec fn value(self) -> T {
145        self.perm.value()
146    }
147
148    pub proof fn tracked_borrow_points_to(tracked &self) -> (tracked ret: &'static PointsTo<T>)
149        returns
150            self.perm,
151    {
152        self.perm
153    }
154}
155
156impl<T> Inv for BoxPointsTo<T> {
157    open spec fn inv(self) -> bool {
158        &&& self.perm.inv()
159        &&& self.perm.dealloc_aligned()
160        &&& self.is_init()
161    }
162}
163
164impl<T> Inv for ArcPointsTo<T> {
165    open spec fn inv(self) -> bool {
166        &&& self.addr() != 0
167        &&& self.addr() as int % vstd::layout::align_of::<T>() as int == 0
168        &&& self.is_init()
169    }
170}
171
172pub uninterp spec fn box_pointer_spec<T>(b: Box<T>) -> *mut T;
173
174// VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an external_body function
175// The memory layout ensures that Box<T> has the following properties:
176//  1. The pointer is aligned.
177//  2. The pointer is non-null even for zero-sized types.
178//  3. The pointer points to a valid value, whose layout is determined by Layout::for_value (exactly size_of::<T>() and align_of::<T>()).
179// See https://doc.rust-lang.org/stable/std/boxed/index.html
180// Its guarantee is actually much stronger than PointsTowithDealloc.inv().
181#[verifier::external_body]
182pub fn box_into_raw<T>(b: Box<T>) -> ((ret, perm, dealloc): (*mut T, Tracked<PointsTo<T>>, Tracked<Option<Dealloc>>))
183    ensures
184        ret == box_pointer_spec(b),
185        ret == perm@.ptr(),
186        perm@.ptr().addr() != 0,
187        perm@.is_init(),
188        perm@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
189        match dealloc@ {
190            Some(dealloc) => {
191                &&& vstd::layout::size_of::<T>() > 0
192                &&& dealloc.addr() == perm@.ptr().addr()
193                &&& dealloc.size() == vstd::layout::size_of::<T>()
194                &&& dealloc.align() == vstd::layout::align_of::<T>()
195                &&& dealloc.provenance() == perm@.ptr()@.provenance
196                &&& valid_layout(size_of::<T>(), align_of::<T>())
197            },
198            None => { &&& vstd::layout::size_of::<T>() == 0 },
199        },
200{
201    (Box::into_raw(b), Tracked::assume_new(), Tracked::assume_new())
202}
203
204#[verifier::external_body]
205pub unsafe fn box_from_raw<T>(
206    ptr: *mut T,
207    tracked points_to: Tracked<PointsTo<T>>,
208    tracked dealloc: Tracked<Option<Dealloc>>,
209) -> (ret: Box<T>)
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        box_pointer_spec(ret) == ptr,
228{
229    unsafe { Box::from_raw(ptr) }
230}
231
232pub uninterp spec fn arc_pointer_spec<T>(a: Arc<T>) -> *const T;
233
234// VERUS LIMITATION: can not add ghost parameter in external specification yet, sp we wrap it in an external_body function
235// `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.
236#[verifier::external_body]
237pub fn arc_into_raw<T>(p: Arc<T>) -> ((ret, perm): (*const T, Tracked<ArcPointsTo<T>>))
238    ensures
239        ret == arc_pointer_spec(p),
240        ret == perm@.ptr(),
241        perm@.ptr().addr() != 0,
242        perm@.is_init(),
243        perm@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
244{
245    (Arc::into_raw(p), Tracked::assume_new())
246}
247
248#[verifier::external_body]
249/// 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.
250/// In verification this responsibility is dispatched to casting the `PointsTo<T>` appropriately, which is not handled here.
251pub unsafe fn arc_from_raw<T>(ptr: *const T, tracked points_to: Tracked<ArcPointsTo<T>>) -> (ret:
252    Arc<T>)
253    requires
254        ptr@.addr != 0,
255        points_to@.ptr() == ptr,
256        points_to@.is_init(),
257        points_to@.ptr().addr() as int % vstd::layout::align_of::<T>() as int == 0,
258    ensures
259        arc_pointer_spec(ret) == ptr,
260{
261    unsafe { Arc::from_raw(ptr) }
262}
263
264} // verus!
vstd_extra/external/smart_ptr.rs

vstd_extra/external/
smart_ptr.rs
