vstd/cell/
pcell_maybe_uninit.rs

1#![allow(unused_imports)]
2
3use super::super::prelude::*;
4use super::super::raw_ptr::MemContents;
5use super::CellId;
6use super::pcell as pc;
7use core::cell::UnsafeCell;
8use core::marker::PhantomData;
9use core::mem::ManuallyDrop;
10use core::mem::MaybeUninit;
11
12use verus as verus_;
13verus_! {
14
15/**
16Variant of [`pcell::PCell<V>`](super::pcell::PCell) for potentially uninitialized data.
17
18See the [`pcell::PCell<V>`](super::pcell::PCell) docs for a high-level overview.
19
20### Example
21
22```rust,ignore
23use vstd::prelude::*;
24use vstd::cell::pcell_maybe_uninit as un;
25use vstd::raw_ptr::MemContents;
26
27verus! {
28
29fn example_pcell_maybe_uninit() {
30    let (cell, Tracked(mut points_to)) = un::PCell::new(5);
31
32    assert(points_to.id() == cell.id());
33    assert(points_to.mem_contents() == MemContents::Init(5));
34
35    let x = cell.take(Tracked(&mut points_to));
36    assert(x == 5);
37
38    assert(points_to.id() == cell.id());
39    assert(points_to.mem_contents() == MemContents::Uninit);
40
41    cell.put(Tracked(&mut points_to), 17);
42
43    assert(points_to.id() == cell.id());
44    assert(points_to.mem_contents() == MemContents::Init(17));
45}
46
47} // verus!
48*/
49
50pub struct PCell<V>(pc::PCell<MaybeUninit<V>>);
51
52/// Permission object associated with a [`PCell<V>`].
53///
54/// See the documentation of [`PCell<V>`] for more information.
55pub tracked struct PointsTo<V>(pc::PointsTo<MaybeUninit<V>>);
56
57impl<V> PointsTo<V> {
58    /// The [`CellId`] of the [`PCell`] this permission is associated with.
59    pub closed spec fn id(&self) -> CellId {
60        self.0.id()
61    }
62
63    /// The contents of the cell.
64    pub closed spec fn mem_contents(&self) -> MemContents<V> {
65        self.0.value().mem_contents()
66    }
67
68    /// Is this cell initialized?
69    #[verifier::inline]
70    pub open spec fn is_init(&self) -> bool {
71        self.mem_contents().is_init()
72    }
73
74    /// Is this cell uninitialized?
75    #[verifier::inline]
76    pub open spec fn is_uninit(&self) -> bool {
77        self.mem_contents().is_uninit()
78    }
79
80    /// Value of the cell (if initialized)
81    #[verifier::inline]
82    pub open spec fn value(&self) -> V
83        recommends
84            self.is_init(),
85    {
86        self.mem_contents().value()
87    }
88
89    /// Guarantees that two permissions can not be associated with the same `CellId`.
90    pub proof fn is_exclusive(tracked &mut self, tracked other: &PointsTo<V>)
91    ensures
92        *final(self) == *old(self),
93        final(self).id() != other.id(),
94    {
95        self.0.is_exclusive(&other.0);
96    }
97}
98
99impl<V> PCell<V> {
100    /// A unique ID for the cell.
101    pub closed spec fn id(&self) -> CellId {
102        self.0.id()
103    }
104
105    /// Return an empty ("uninitialized") cell.
106    #[inline(always)]
107    pub const fn empty() -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
108        ensures
109            pt.1@.id() == pt.0.id(),
110            pt.1@.mem_contents() == MemContents::Uninit,
111    {
112        let (pcell, Tracked(pt)) = pc::PCell::new(MaybeUninit::uninit());
113        (PCell(pcell), Tracked(PointsTo(pt)))
114    }
115
116    #[inline(always)]
117    pub const fn new(v: V) -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
118        ensures
119            pt.1@.id() == pt.0.id(),
120            pt.1@.mem_contents() == MemContents::Init(v),
121    {
122        let (pcell, Tracked(pt)) = pc::PCell::new(MaybeUninit::new(v));
123        (PCell(pcell), Tracked(PointsTo(pt)))
124    }
125
126    #[inline(always)]
127    pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
128        requires
129            old(perm).id() == self.id(),
130            old(perm).mem_contents() == MemContents::Uninit,
131        ensures
132            final(perm).id() == self.id(),
133            final(perm).mem_contents() == MemContents::Init(in_v),
134        opens_invariants none
135        no_unwind
136    {
137        self.0.replace(Tracked(&mut perm.0), MaybeUninit::new(in_v));
138    }
139
140    #[inline(always)]
141    pub fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (out_v: V)
142        requires
143            self.id() == old(perm).id(),
144            old(perm).is_init(),
145        ensures
146            final(perm).id() == old(perm).id(),
147            final(perm).mem_contents() == MemContents::Uninit,
148            out_v == old(perm).value(),
149        opens_invariants none
150        no_unwind
151    {
152        unsafe {
153            self.0.replace(Tracked(&mut perm.0), MaybeUninit::uninit()).assume_init()
154        }
155    }
156
157    #[inline(always)]
158    pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V)
159        requires
160            self.id() == old(perm).id(),
161            old(perm).is_init(),
162        ensures
163            final(perm).id() == old(perm).id(),
164            final(perm).mem_contents() == MemContents::Init(in_v),
165            out_v == old(perm).value(),
166        opens_invariants none
167        no_unwind
168    {
169        unsafe {
170            self.0.replace(Tracked(&mut perm.0), MaybeUninit::new(in_v)).assume_init()
171        }
172    }
173
174    #[inline(always)]
175    pub fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V)
176        requires
177            self.id() == perm.id(),
178            perm.is_init(),
179        ensures
180            *v == perm.value(),
181        opens_invariants none
182        no_unwind
183    {
184        unsafe {
185            self.0.borrow(Tracked(&perm.0)).assume_init_ref()
186        }
187    }
188
189    #[inline(always)]
190    pub fn borrow_mut<'a>(&'a self, Tracked(perm): Tracked<&'a mut PointsTo<V>>) -> (v: &'a mut V)
191        requires
192            self.id() == perm.id(),
193            perm.is_init(),
194        ensures
195            *v == old(perm).value(),
196            final(perm).is_init(),
197            final(perm).value() == *final(v),
198        opens_invariants none
199        no_unwind
200    {
201        unsafe {
202            self.0.borrow_mut(Tracked(&mut perm.0)).assume_init_mut()
203        }
204    }
205
206    #[inline(always)]
207    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
208        requires
209            self.id() == perm.id(),
210            perm.is_init(),
211        ensures
212            v == perm.value(),
213        opens_invariants none
214        no_unwind
215    {
216        let tracked mut perm = perm;
217        self.take(Tracked(&mut perm))
218    }
219
220    #[inline(always)]
221    pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
222        requires
223            self.id() == old(perm).id(),
224        ensures
225            final(perm).id() == old(perm).id(),
226            final(perm).mem_contents() == MemContents::Init(in_v),
227        opens_invariants none
228        no_unwind
229    {
230        self.0.replace(Tracked(&mut perm.0), MaybeUninit::new(in_v));
231    }
232
233    #[inline(always)]
234    pub fn read(&self, Tracked(perm): Tracked<&PointsTo<V>>) -> (out_v: V)
235        where V: Copy
236        requires
237            self.id() == perm.id(),
238            perm.is_init(),
239        returns
240            perm.value()
241        opens_invariants none
242        no_unwind
243    {
244        *self.borrow(Tracked(perm))
245    }
246}
247
248}
vstd/cell/pcell_maybe_uninit.rs

vstd/cell/
pcell_maybe_uninit.rs
