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
90impl<V> PCell<V> {
91    /// A unique ID for the cell.
92    pub closed spec fn id(&self) -> CellId {
93        self.0.id()
94    }
95
96    /// Return an empty ("uninitialized") cell.
97    #[inline(always)]
98    pub const fn empty() -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
99        ensures
100            pt.1@.id() == pt.0.id(),
101            pt.1@.mem_contents() === MemContents::Uninit,
102    {
103        let (pcell, Tracked(pt)) = pc::PCell::new(MaybeUninit::uninit());
104        (PCell(pcell), Tracked(PointsTo(pt)))
105    }
106
107    #[inline(always)]
108    pub const fn new(v: V) -> (pt: (PCell<V>, Tracked<PointsTo<V>>))
109        ensures
110            pt.1@.id() == pt.0.id(),
111            pt.1@.mem_contents() == MemContents::Init(v),
112    {
113        let (pcell, Tracked(pt)) = pc::PCell::new(MaybeUninit::new(v));
114        (PCell(pcell), Tracked(PointsTo(pt)))
115    }
116
117    #[inline(always)]
118    pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
119        requires
120            old(perm).id() == self.id(),
121            old(perm).mem_contents() === MemContents::Uninit,
122        ensures
123            perm.id() == self.id(),
124            perm.mem_contents() === MemContents::Init(in_v),
125        opens_invariants none
126        no_unwind
127    {
128        self.0.replace(Tracked(&mut perm.0), MaybeUninit::new(in_v));
129    }
130
131    #[inline(always)]
132    pub fn take(&self, Tracked(perm): Tracked<&mut PointsTo<V>>) -> (out_v: V)
133        requires
134            self.id() === old(perm).id(),
135            old(perm).is_init(),
136        ensures
137            perm.id() === old(perm).id(),
138            perm.mem_contents() === MemContents::Uninit,
139            out_v === old(perm).value(),
140        opens_invariants none
141        no_unwind
142    {
143        unsafe {
144            self.0.replace(Tracked(&mut perm.0), MaybeUninit::uninit()).assume_init()
145        }
146    }
147
148    #[inline(always)]
149    pub fn replace(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V) -> (out_v: V)
150        requires
151            self.id() === old(perm).id(),
152            old(perm).is_init(),
153        ensures
154            perm.id() === old(perm).id(),
155            perm.mem_contents() === MemContents::Init(in_v),
156            out_v === old(perm).value(),
157        opens_invariants none
158        no_unwind
159    {
160        unsafe {
161            self.0.replace(Tracked(&mut perm.0), MaybeUninit::new(in_v)).assume_init()
162        }
163    }
164
165    #[inline(always)]
166    pub fn borrow<'a>(&'a self, Tracked(perm): Tracked<&'a PointsTo<V>>) -> (v: &'a V)
167        requires
168            self.id() === perm.id(),
169            perm.is_init(),
170        ensures
171            *v === perm.value(),
172        opens_invariants none
173        no_unwind
174    {
175        unsafe {
176            self.0.borrow(Tracked(&perm.0)).assume_init_ref()
177        }
178    }
179
180    #[inline(always)]
181    pub fn into_inner(self, Tracked(perm): Tracked<PointsTo<V>>) -> (v: V)
182        requires
183            self.id() === perm.id(),
184            perm.is_init(),
185        ensures
186            v === perm.value(),
187        opens_invariants none
188        no_unwind
189    {
190        let tracked mut perm = perm;
191        self.take(Tracked(&mut perm))
192    }
193
194    #[inline(always)]
195    pub fn write(&self, Tracked(perm): Tracked<&mut PointsTo<V>>, in_v: V)
196        requires
197            self.id() === old(perm).id(),
198        ensures
199            perm.id() === old(perm).id(),
200            perm.mem_contents() === MemContents::Init(in_v),
201        opens_invariants none
202        no_unwind
203    {
204        self.0.replace(Tracked(&mut perm.0), MaybeUninit::new(in_v));
205    }
206
207    #[inline(always)]
208    pub fn read(&self, Tracked(perm): Tracked<&PointsTo<V>>) -> (out_v: V)
209        where V: Copy
210        requires
211            self.id() === perm.id(),
212            perm.is_init(),
213        returns
214            perm.value()
215        opens_invariants none
216        no_unwind
217    {
218        *self.borrow(Tracked(perm))
219    }
220}
221
222}
vstd/cell/pcell_maybe_uninit.rs

vstd/cell/
pcell_maybe_uninit.rs
