vstd/
raw_ptr.rs

1#![allow(unused_imports)]
2
3/*!
4Tools and reasoning principles for [raw pointers](https://doc.rust-lang.org/std/primitive.pointer.html).
5The tools here are meant to address "real Rust pointers, including all their subtleties on the Rust Abstract Machine,
6to the largest extent that is reasonable."
7
8For a gentler introduction to some of the concepts here, see [`PPtr`](crate::simple_pptr), which uses a much-simplified pointer model.
9
10### Pointer model
11
12A pointer consists of an address (`ptr.addr()` or `ptr as usize`), a provenance `ptr@.provenance`,
13and metadata `ptr@.metadata` (which is trivial except for pointers to non-sized types).
14Note that in spec code, pointer equality requires *all 3* to be equal, whereas runtime equality (eq)
15only compares addresses and metadata.
16
17`*mut T` vs. `*const T` do not have any semantic difference and Verus treats them as the same;
18they can be seamlessly cast to and fro.
19*/
20
21use super::layout::*;
22use super::prelude::*;
23
24verus! {
25
26//////////////////////////////////////
27// Define a model of Ptrs and PointsTo
28// Notes on mutability:
29//
30//  - Unique vs shared ownership in Verus is always determined
31//    via the PointsTo ghost tracked object.
32//
33//  - Thus, there is effectively no difference between *mut T and *const T,
34//    so we encode both of these in the same way.
35//    (In VIR, we distinguish these via a decoration.)
36//    Thus we can cast freely between them both in spec and exec code.
37//
38//  - This is consistent with Rust's operational semantics;
39//    casting between *mut T and *const T has no operational meaning.
40//
41//  - When creating a pointer from a reference, the mutability
42//    of the pointer *does* have an effect because it determines
43//    what kind of "tag" the pointer gets, i.e., whether that
44//    tag is readonly or not. In our model here, this tag is folded
45//    into the provenance.
46//
47/// Provenance
48///
49/// A full model of provenance is given by formalisms such as "Stacked Borrows"
50/// or "Tree Borrows."
51///
52/// None of these models are finalized, nor has Rust committed to them.
53/// Rust's recent [RFC on provenance](https://rust-lang.github.io/rfcs/3559-rust-has-provenance.html)
54/// simply details that there *is* some concept of provenance.
55///
56/// Our model here, likewise, simply declares `Provenance` as an
57/// abstract type.
58///
59/// MiniRust currently declares a pointer has an `Option<Provenance>`;
60/// the model here gives provenance a special "null" value instead
61/// of using an option.
62///
63/// More reading for reference:
64/// * [https://doc.rust-lang.org/std/ptr/](https://doc.rust-lang.org/std/ptr/)
65/// * [https://github.com/minirust/minirust/tree/master](https://github.com/minirust/minirust/tree/master)
66#[verifier::external_body]
67pub ghost struct Provenance {}
68
69impl Provenance {
70    /// The provenance of the null ptr (or really, "no provenance")
71    pub uninterp spec fn null() -> Self;
72}
73
74/// Metadata
75///
76/// For thin pointers (i.e., when T: Sized), the metadata is `()`.
77/// For slices (`[T]`) and `str`, the metadata is `usize`.
78/// For `dyn` types (not supported by Verus at the time of writing), this type is also nontrivial.
79///
80/// See: <https://doc.rust-lang.org/std/ptr/trait.Pointee.html>
81#[cfg(verus_keep_ghost)]
82pub type Metadata<T> = <T as core::ptr::Pointee>::Metadata;
83
84#[cfg(not(verus_keep_ghost))]
85pub struct FakeMetadata<T: ?Sized> {
86    t: *mut T,
87}
88
89#[cfg(not(verus_keep_ghost))]
90pub type Metadata<T> = FakeMetadata<T>;
91
92/// Model of a pointer `*mut T` or `*const T` in Rust's abstract machine.
93/// In addition to the address, each pointer has its corresponding provenance and metadata.
94pub ghost struct PtrData<T: ?Sized> {
95    pub addr: usize,
96    pub provenance: Provenance,
97    pub metadata: Metadata<T>,
98}
99
100/// Permission to access possibly-initialized, _typed_ memory.
101// ptr |--> Init(v) means:
102//   bytes in this memory are consistent with value v
103//   and we have all the ghost state associated with type V
104//
105// ptr |--> Uninit means:
106//   no knowledge about what's in memory
107//   (to be pedantic, the bytes might be initialized in rust's abstract machine,
108//   but we don't know so we have to pretend they're uninitialized)
109#[verifier::external_body]
110#[verifier::accept_recursive_types(T)]
111pub tracked struct PointsTo<T> {
112    phantom: core::marker::PhantomData<T>,
113    no_copy: NoCopy,
114}
115
116//#[verifier::external_body]
117//#[verifier::accept_recursive_types(T)]
118//pub tracked struct PointsToBytes<T> {
119//    phantom: core::marker::PhantomData<T>,
120//    no_copy: NoCopy,
121//}
122/// Represents (typed) contents of memory.
123// Don't use std Option here in order to avoid circular dependency issues
124// with verifying the standard library.
125// (Also, using our own enum here lets us have more meaningful
126// variant names like Uninit/Init.)
127#[verifier::accept_recursive_types(T)]
128pub ghost enum MemContents<T> {
129    /// Represents uninitialized memory.
130    Uninit,
131    /// Represents initialized memory with the given value of type `T`.
132    Init(T),
133}
134
135/// Data associated with a `PointsTo` permission.
136/// We keep track of both the pointer and the (potentially uninitialized) value
137/// it points to.
138///
139/// If `opt_value` is `Init(T)`, this signifies that `ptr` points to initialized memory,
140/// and the value of `opt_value` is consistent with the bytes `ptr` points to,
141/// We also have all the ghost state associated with type `T`.
142///
143/// If `opt_value` is `Uninit`, then we have no knowledge about what's in memory,
144/// and we assume `ptr` points to uninitialized memory.
145/// (To be pedantic, the bytes might be initialized in Rust's abstract machine,
146///  but we don't know, so we have to pretend they're uninitialized.)
147pub ghost struct PointsToData<T> {
148    pub ptr: *mut T,
149    pub opt_value: MemContents<T>,
150}
151
152impl<T: ?Sized> View for *mut T {
153    type V = PtrData<T>;
154
155    uninterp spec fn view(&self) -> Self::V;
156}
157
158/// Compares the address and metadata of two pointers.
159///
160/// Note that this DOES not compare provenance, which does not exist in the runtime
161/// pointer representation (i.e., it only exists in the Rust abstract machine).
162pub assume_specification<T: ?Sized>[ <*mut T as PartialEq<*mut T>>::eq ](
163    x: &*mut T,
164    y: &*mut T,
165) -> (res: bool)
166    ensures
167        res <==> (x@.addr == y@.addr) && (x@.metadata == y@.metadata),
168;
169
170impl<T: ?Sized> View for *const T {
171    type V = PtrData<T>;
172
173    #[verifier::inline]
174    open spec fn view(&self) -> Self::V {
175        (*self as *mut T).view()
176    }
177}
178
179/// Compares the address and metadata of two pointers.
180///
181/// Note that this DOES not compare provenance, which does not exist in the runtime
182/// pointer representation (i.e., it only exists in the Rust abstract machine).
183pub assume_specification<T: ?Sized>[ <*const T as PartialEq<*const T>>::eq ](
184    x: &*const T,
185    y: &*const T,
186) -> (res: bool)
187    ensures
188        res <==> (x@.addr == y@.addr) && (x@.metadata == y@.metadata),
189;
190
191impl<T> View for PointsTo<T> {
192    type V = PointsToData<T>;
193
194    uninterp spec fn view(&self) -> Self::V;
195}
196
197impl<T> PointsTo<T> {
198    /// The pointer that this permission is associated with.
199    #[verifier::inline]
200    pub open spec fn ptr(&self) -> *mut T {
201        self.view().ptr
202    }
203
204    /// The (possibly uninitialized) memory that this permission gives access to.
205    #[verifier::inline]
206    pub open spec fn opt_value(&self) -> MemContents<T> {
207        self.view().opt_value
208    }
209
210    /// Returns `true` if the permission's associated memory is initialized.
211    #[verifier::inline]
212    pub open spec fn is_init(&self) -> bool {
213        self.opt_value().is_init()
214    }
215
216    /// Returns `true` if the permission's associated memory is uninitialized.
217    #[verifier::inline]
218    pub open spec fn is_uninit(&self) -> bool {
219        self.opt_value().is_uninit()
220    }
221
222    /// If the permission's associated memory is initialized,
223    /// returns the value that the pointer points to.
224    /// Otherwise, the result is meaningless.
225    #[verifier::inline]
226    pub open spec fn value(&self) -> T
227        recommends
228            self.is_init(),
229    {
230        self.opt_value().value()
231    }
232
233    /// Guarantee that the `PointsTo` for any non-zero-sized type points to a non-null address.
234    ///
235    // ZST pointers *are* allowed to be null, so we need a precondition that size != 0.
236    // See https://doc.rust-lang.org/std/ptr/#safety
237    pub axiom fn is_nonnull(tracked &self)
238        requires
239            size_of::<T>() != 0,
240        ensures
241            self@.ptr@.addr != 0,
242    ;
243
244    /// Guarantee that the `PointsTo` points to an aligned address.
245    ///
246    // Note that even for ZSTs, pointers need to be aligned.
247    pub axiom fn is_aligned(tracked &self)
248        ensures
249            self@.ptr@.addr as nat % align_of::<T>() == 0,
250    ;
251
252    /// "Forgets" about the value stored behind the pointer.
253    /// Updates the `PointsTo` value to [`MemContents::Uninit`](MemContents::Uninit).
254    /// Note that this is a `proof` function, i.e.,
255    /// it is operationally a no-op in executable code, even on the Rust Abstract Machine.
256    /// Only the proof-code representation changes.
257    pub axiom fn leak_contents(tracked &mut self)
258        ensures
259            self.ptr() == old(self).ptr(),
260            self.is_uninit(),
261    ;
262
263    /// Guarantees that the memory ranges associated with two permissions will not overlap,
264    /// since you cannot have two permissions to the same memory.
265    ///
266    /// Note: If both S and T are non-zero-sized, then this implies the pointers
267    /// have distinct addresses.
268    pub axiom fn is_disjoint<S>(tracked &mut self, tracked other: &PointsTo<S>)
269        ensures
270            *old(self) == *self,
271            self.ptr() as int + size_of::<T>() <= other.ptr() as int || other.ptr() as int
272                + size_of::<S>() <= self.ptr() as int,
273    ;
274}
275
276impl<T> MemContents<T> {
277    /// Returns `true` if it is a [`MemContents::Init`] value.
278    #[verifier::inline]
279    pub open spec fn is_init(&self) -> bool {
280        self is Init
281    }
282
283    /// Returns `true` if it is a [`MemContents::Uninit`] value.
284    #[verifier::inline]
285    pub open spec fn is_uninit(&self) -> bool {
286        self is Uninit
287    }
288
289    /// If it is a [`MemContents::Init`] value, returns the value.
290    /// Otherwise, the return value is meaningless.
291    #[verifier::inline]
292    pub open spec fn value(&self) -> T
293        recommends
294            self is Init,
295    {
296        self->0
297    }
298}
299
300//////////////////////////////////////
301// Inverse functions:
302// Pointers are equivalent to their model
303/// Constructs a pointer from its underlying model.
304pub uninterp spec fn ptr_mut_from_data<T: ?Sized>(data: PtrData<T>) -> *mut T;
305
306/// Constructs a pointer from its underlying model.
307/// Since `*mut T` and `*const T` are [semantically the same](https://verus-lang.github.io/verus/verusdoc/vstd/raw_ptr/index.html#pointer-model),
308/// we can define this operation in terms of the operation on `*mut T`.
309#[verifier::inline]
310pub open spec fn ptr_from_data<T: ?Sized>(data: PtrData<T>) -> *const T {
311    ptr_mut_from_data(data) as *const T
312}
313
314/// The view of a pointer constructed from `data: PtrData` should be exactly that data.
315pub broadcast axiom fn axiom_ptr_mut_from_data<T: ?Sized>(data: PtrData<T>)
316    ensures
317        (#[trigger] ptr_mut_from_data::<T>(data))@ == data,
318;
319
320// Equiv to ptr_mut_from_data, but named differently to avoid trigger issues
321// Only use for ptrs_mut_eq
322#[doc(hidden)]
323pub uninterp spec fn view_reverse_for_eq<T: ?Sized>(data: PtrData<T>) -> *mut T;
324
325/// Implies that `a@ == b@ ==> a == b`.
326pub broadcast axiom fn ptrs_mut_eq<T: ?Sized>(a: *mut T)
327    ensures
328        view_reverse_for_eq::<T>(#[trigger] a@) == a,
329;
330
331// We do the same trick again, but specialized for Sized types. This improves automation.
332// Specifically, this makes it easier to prove `a == b` without having to explicitly write
333// `a@.metadata == b@.metadata`, since this condition is trivial; both values are always unit.
334// (See the test_extensionality_sized test case.)
335#[doc(hidden)]
336pub closed spec fn view_reverse_for_eq_sized<T>(addr: usize, provenance: Provenance) -> *mut T {
337    view_reverse_for_eq(PtrData { addr: addr, provenance: provenance, metadata: () })
338}
339
340pub broadcast proof fn ptrs_mut_eq_sized<T>(a: *mut T)
341    ensures
342        view_reverse_for_eq_sized::<T>((#[trigger] a@).addr, a@.provenance) == a,
343{
344    assert(a@.metadata == ());
345    ptrs_mut_eq(a);
346}
347
348//////////////////////////////////////
349/// Constructs a null pointer.
350/// NOTE: Trait aliases are not yet supported,
351/// so we use `Pointee<Metadata = ()>` instead of `core::ptr::Thin` here
352#[verifier::inline]
353pub open spec fn ptr_null<T: ?Sized + core::ptr::Pointee<Metadata = ()>>() -> *const T {
354    ptr_from_data(PtrData::<T> { addr: 0, provenance: Provenance::null(), metadata: () })
355}
356
357#[cfg(verus_keep_ghost)]
358#[verifier::when_used_as_spec(ptr_null)]
359pub assume_specification<
360    T: ?Sized + core::ptr::Pointee<Metadata = ()>,
361>[ core::ptr::null ]() -> (res: *const T)
362    ensures
363        res == ptr_null::<T>(),
364    opens_invariants none
365    no_unwind
366;
367
368/// Constructs a mutable null pointer.
369/// NOTE: Trait aliases are not yet supported,
370/// so we use `Pointee<Metadata = ()>` instead of `core::ptr::Thin` here
371#[verifier::inline]
372pub open spec fn ptr_null_mut<T: ?Sized + core::ptr::Pointee<Metadata = ()>>() -> *mut T {
373    ptr_mut_from_data(PtrData::<T> { addr: 0, provenance: Provenance::null(), metadata: () })
374}
375
376#[cfg(verus_keep_ghost)]
377#[verifier::when_used_as_spec(ptr_null_mut)]
378pub assume_specification<
379    T: ?Sized + core::ptr::Pointee<Metadata = ()>,
380>[ core::ptr::null_mut ]() -> (res: *mut T)
381    ensures
382        res == ptr_null_mut::<T>(),
383    opens_invariants none
384    no_unwind
385;
386
387//////////////////////////////////////
388// Casting
389// as-casts and implicit casts are translated internally to these functions
390// (including casts that involve *const ptrs)
391/// Cast a pointer to a thin pointer. Address and provenance are preserved; metadata is now thin.
392pub open spec fn spec_cast_ptr_to_thin_ptr<T: ?Sized, U: Sized>(ptr: *mut T) -> *mut U {
393    ptr_mut_from_data(PtrData::<U> { addr: ptr@.addr, provenance: ptr@.provenance, metadata: () })
394}
395
396/// Cast a pointer to a thin pointer. Address and provenance are preserved; metadata is now thin.
397///
398/// Don't call this directly; use an `as`-cast instead.
399#[verifier::external_body]
400#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::raw_ptr::cast_ptr_to_thin_ptr")]
401#[verifier::when_used_as_spec(spec_cast_ptr_to_thin_ptr)]
402pub fn cast_ptr_to_thin_ptr<T: ?Sized, U: Sized>(ptr: *mut T) -> (result: *mut U)
403    ensures
404        result == spec_cast_ptr_to_thin_ptr::<T, U>(ptr),
405    opens_invariants none
406    no_unwind
407{
408    ptr as *mut U
409}
410
411/// Cast a pointer to an array of length `N` to a slice pointer.
412/// Address and provenance are preserved; metadata has length `N`.
413pub open spec fn spec_cast_array_ptr_to_slice_ptr<T, const N: usize>(ptr: *mut [T; N]) -> *mut [T] {
414    ptr_mut_from_data(PtrData::<[T]> { addr: ptr@.addr, provenance: ptr@.provenance, metadata: N })
415}
416
417/// Cast a pointer to an array of length `N` to a slice pointer.
418/// Address and provenance are preserved; metadata has length `N`.
419///
420/// Don't call this directly; use an `as`-cast instead.
421#[verifier::external_body]
422#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::raw_ptr::cast_array_ptr_to_slice_ptr")]
423#[verifier::when_used_as_spec(spec_cast_array_ptr_to_slice_ptr)]
424pub fn cast_array_ptr_to_slice_ptr<T, const N: usize>(ptr: *mut [T; N]) -> (result: *mut [T])
425    ensures
426        result == spec_cast_array_ptr_to_slice_ptr(ptr),
427    opens_invariants none
428    no_unwind
429{
430    ptr as *mut [T]
431}
432
433/// Cast a pointer to a `usize` by extracting just the address.
434pub open spec fn spec_cast_ptr_to_usize<T: Sized>(ptr: *mut T) -> usize {
435    ptr@.addr
436}
437
438/// Cast the address of a pointer to a `usize`.
439///
440/// Don't call this directly; use an `as`-cast instead.
441#[verifier::external_body]
442#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::raw_ptr::cast_ptr_to_usize")]
443#[verifier::when_used_as_spec(spec_cast_ptr_to_usize)]
444pub fn cast_ptr_to_usize<T: Sized>(ptr: *mut T) -> (result: usize)
445    ensures
446        result == spec_cast_ptr_to_usize(ptr),
447    opens_invariants none
448    no_unwind
449{
450    ptr as usize
451}
452
453//////////////////////////////////////
454// Reading and writing
455/// Calls [`core::ptr::write`] to write the value `v` to the memory location pointed to by `ptr`,
456/// using the permission `perm`.
457///
458/// This does _not_ drop the contents. If the memory is already initialized,
459/// this could leak allocations or resources, so care should be taken to not overwrite an object that should be dropped.
460/// This is appropriate for initializing uninitialized memory, or overwriting memory that has previously been [read](ptr_mut_read) from.
461#[inline(always)]
462#[verifier::external_body]
463pub fn ptr_mut_write<T>(ptr: *mut T, Tracked(perm): Tracked<&mut PointsTo<T>>, v: T)
464    requires
465        old(perm).ptr() == ptr,
466    ensures
467        perm.ptr() == ptr,
468        perm.opt_value() == MemContents::Init(v),
469    opens_invariants none
470    no_unwind
471{
472    unsafe {
473        core::ptr::write(ptr, v);
474    }
475}
476
477/// Calls [`core::ptr::read`] to read from the memory pointed to by `ptr`,
478/// using the permission `perm`.
479///
480/// This leaves the data as "unitialized", i.e., performs a move.
481///
482/// TODO: This needs to be made more general (i.e., should be able to read a Copy type
483/// without destroying it; should be able to leave the bytes intact without uninitializing them).
484#[inline(always)]
485#[verifier::external_body]
486pub fn ptr_mut_read<T>(ptr: *const T, Tracked(perm): Tracked<&mut PointsTo<T>>) -> (v: T)
487    requires
488        old(perm).ptr() == ptr,
489        old(perm).is_init(),
490    ensures
491        perm.ptr() == ptr,
492        perm.is_uninit(),
493        v == old(perm).value(),
494    opens_invariants none
495    no_unwind
496{
497    unsafe { core::ptr::read(ptr) }
498}
499
500/// Equivalent to `&*ptr`, passing in a permission `perm` to ensure safety.
501/// The memory pointed to by `ptr` must be initialized.
502#[inline(always)]
503#[verifier::external_body]
504pub fn ptr_ref<T>(ptr: *const T, Tracked(perm): Tracked<&PointsTo<T>>) -> (v: &T)
505    requires
506        perm.ptr() == ptr,
507        perm.is_init(),
508    ensures
509        v == perm.value(),
510    opens_invariants none
511    no_unwind
512{
513    unsafe { &*ptr }
514}
515
516/* coming soon
517/// Equivalent to &mut *X, passing in a permission `perm` to ensure safety.
518/// The memory pointed to by `ptr` must be initialized.
519#[inline(always)]
520#[verifier::external_body]
521pub fn ptr_mut_ref<T>(ptr: *mut T, Tracked(perm): Tracked<&mut PointsTo<T>>) -> (v: &mut T)
522    requires
523        old(perm).ptr() == ptr,
524        old(perm).is_init()
525    ensures
526        perm.ptr() == ptr,
527        perm.is_init(),
528
529        old(perm).value() == *old(v),
530        new(perm).value() == *new(v),
531    unsafe { &*ptr }
532}
533*/
534
535macro_rules! pointer_specs {
536    ($mod_ident:ident, $ptr_from_data:ident, $mu:tt) => {
537        #[cfg(verus_keep_ghost)]
538        mod $mod_ident {
539            use super::*;
540
541            verus!{
542
543            #[verifier::inline]
544            pub open spec fn spec_addr<T: ?Sized>(p: *$mu T) -> usize { p@.addr }
545
546            #[verifier::when_used_as_spec(spec_addr)]
547            pub assume_specification<T: ?Sized>[<*$mu T>::addr](p: *$mu T) -> (addr: usize)
548                ensures addr == spec_addr(p)
549                opens_invariants none
550                no_unwind;
551
552            pub open spec fn spec_with_addr<T: ?Sized>(p: *$mu T, addr: usize) -> *$mu T {
553                $ptr_from_data(PtrData::<T> { addr: addr, .. p@ })
554            }
555
556            #[verifier::when_used_as_spec(spec_with_addr)]
557            pub assume_specification<T: ?Sized>[<*$mu T>::with_addr](p: *$mu T, addr: usize) -> (q: *$mu T)
558                ensures q == spec_with_addr(p, addr)
559                opens_invariants none
560                no_unwind;
561
562            }
563        }
564    };
565}
566
567pointer_specs!(ptr_mut_specs, ptr_mut_from_data, mut);
568
569pointer_specs!(ptr_const_specs, ptr_from_data, const);
570
571pub broadcast group group_raw_ptr_axioms {
572    axiom_ptr_mut_from_data,
573    ptrs_mut_eq,
574    ptrs_mut_eq_sized,
575}
576
577/// Tracked object that indicates a given provenance has been exposed.
578#[verifier::external_body]
579pub tracked struct IsExposed {}
580
581impl Clone for IsExposed {
582    #[verifier::external_body]
583    fn clone(&self) -> (s: Self)
584        ensures
585            s == self,
586    {
587        IsExposed {  }
588    }
589}
590
591impl Copy for IsExposed {
592
593}
594
595impl IsExposed {
596    /// The view of `IsExposed` is simply its provenance.
597    pub open spec fn view(self) -> Provenance {
598        self.provenance()
599    }
600
601    /// Provenance we are exposing.
602    pub uninterp spec fn provenance(self) -> Provenance;
603
604    /// It is always possible to expose/construct the null provenance.
605    pub axiom fn null() -> (tracked exp: IsExposed)
606        ensures
607            exp.provenance() == Provenance::null(),
608    ;
609}
610
611/// Perform a provenance expose operation.
612#[verifier::external_body]
613pub fn expose_provenance<T: Sized>(m: *mut T) -> (provenance: Tracked<IsExposed>)
614    ensures
615        provenance@@ == m@.provenance,
616    opens_invariants none
617    no_unwind
618{
619    let _ = m as usize;
620    Tracked::assume_new()
621}
622
623/// Construct a pointer with the given provenance from a _usize_ address.
624/// The provenance must have previously been exposed.
625#[verifier::external_body]
626pub fn with_exposed_provenance<T: Sized>(
627    addr: usize,
628    Tracked(provenance): Tracked<IsExposed>,
629) -> (p: *mut T)
630    ensures
631        p == ptr_mut_from_data::<T>(
632            PtrData::<T> { addr: addr, provenance: provenance@, metadata: () },
633        ),
634    opens_invariants none
635    no_unwind
636{
637    addr as *mut T
638}
639
640/// Variable-sized uninitialized memory.
641///
642/// Permission is for an arbitrary set of addresses, not necessarily contiguous,
643/// and with a given provenance.
644// Note reading from uninitialized memory is UB, so we shouldn't give any
645// reading capabilities to PointsToRaw. Turning a PointsToRaw into a PointsTo
646// should always leave it as 'uninitialized'.
647#[verifier::external_body]
648pub tracked struct PointsToRaw {
649    // TODO implement this as Map<usize, PointsTo<u8>> or something
650    no_copy: NoCopy,
651}
652
653impl PointsToRaw {
654    /// Provenance of the `PointsToRaw` permission;
655    /// this corresponds to the original allocation and does not change.
656    pub uninterp spec fn provenance(self) -> Provenance;
657
658    /// Memory addresses (domain) that the `PointsToRaw` permission gives access to.
659    /// This set may be split apart and/or recombined, in order to create permissions to smaller pieces of the allocation.
660    pub uninterp spec fn dom(self) -> Set<int>;
661
662    /// Returns `true` if the domain of this permission is exactly the range `[start, start + len)`.
663    pub open spec fn is_range(self, start: int, len: int) -> bool {
664        super::set_lib::set_int_range(start, start + len) =~= self.dom()
665    }
666
667    /// Returns `true` if the domain of this permission contains the range `[start, start + len)`.
668    pub open spec fn contains_range(self, start: int, len: int) -> bool {
669        super::set_lib::set_int_range(start, start + len) <= self.dom()
670    }
671
672    /// Constructs a `PointsToRaw` permission over an empty domain with the given provenance.
673    pub axiom fn empty(provenance: Provenance) -> (tracked points_to_raw: Self)
674        ensures
675            points_to_raw.dom() == Set::<int>::empty(),
676            points_to_raw.provenance() == provenance,
677    ;
678
679    /// Splits the current `PointsToRaw` permission into a permission with domain `range`
680    /// and a permission containing the rest of the domain,
681    /// provided that `range` is contained in the domain of the current permission.
682    pub axiom fn split(tracked self, range: Set<int>) -> (tracked res: (Self, Self))
683        requires
684            range.subset_of(self.dom()),
685        ensures
686            res.0.provenance() == self.provenance(),
687            res.1.provenance() == self.provenance(),
688            res.0.dom() == range,
689            res.1.dom() == self.dom().difference(range),
690    ;
691
692    /// Joins two `PointsToRaw` permissions into one,
693    /// provided that they have the same provenance.
694    /// The memory addresses of the new permission is the union of the domains of `self` and `other`.
695    pub axiom fn join(tracked self, tracked other: Self) -> (tracked joined: Self)
696        requires
697            self.provenance() == other.provenance(),
698        ensures
699            joined.provenance() == self.provenance(),
700            joined.dom() == self.dom() + other.dom(),
701    ;
702
703    /// Creates a `PointsTo<V>` permission from a `PointsToRaw` permission
704    /// with address `start` and the same provanance as the `PointsToRaw` permission,
705    /// provided that `start` is aligned to `V` and
706    /// that the domain of the `PointsToRaw` permission matches the size of `V`.
707    ///
708    /// In combination with PointsToRaw::empty(),
709    /// this lets us create a PointsTo for a ZST for _any_ aligned pointer (any address and provenance, even null).
710    pub axiom fn into_typed<V>(tracked self, start: usize) -> (tracked points_to: PointsTo<V>)
711        requires
712            start as int % align_of::<V>() as int == 0,
713            self.is_range(start as int, size_of::<V>() as int),
714        ensures
715            points_to.ptr() == ptr_mut_from_data::<V>(
716                PtrData { addr: start, provenance: self.provenance(), metadata: () },
717            ),
718            points_to.is_uninit(),
719    ;
720}
721
722impl<V> PointsTo<V> {
723    /// Creates a `PointsToRaw` from a `PointsTo<V>` with the same provenance
724    /// and a range corresponding to the address of the `PointsTo<V>` and size of `V`,
725    /// provided that the memory tracked by the `PointsTo<V>`is uninitialized.
726    pub axiom fn into_raw(tracked self) -> (tracked points_to_raw: PointsToRaw)
727        requires
728            self.is_uninit(),
729        ensures
730            points_to_raw.is_range(self.ptr().addr() as int, size_of::<V>() as int),
731            points_to_raw.provenance() == self.ptr()@.provenance,
732    ;
733}
734
735// Allocation and deallocation via the global allocator
736/// Permission to perform a deallocation with the global allocator.
737#[verifier::external_body]
738pub tracked struct Dealloc {
739    no_copy: NoCopy,
740}
741
742/// Data associated with a `Dealloc` permission.
743pub ghost struct DeallocData {
744    pub addr: usize,
745    pub size: nat,
746    pub align: nat,
747    /// This should probably be some kind of "allocation ID" (with "allocation ID" being
748    /// only one part of a full Provenance definition).
749    pub provenance: Provenance,
750}
751
752impl Dealloc {
753    pub uninterp spec fn view(self) -> DeallocData;
754
755    /// Start address of the allocation you are allowed to deallocate.
756    #[verifier::inline]
757    pub open spec fn addr(self) -> usize {
758        self.view().addr
759    }
760
761    /// Size of the allocation you are allowed to deallocate.
762    #[verifier::inline]
763    pub open spec fn size(self) -> nat {
764        self.view().size
765    }
766
767    /// Alignment of the allocation you are allowed to deallocate.
768    #[verifier::inline]
769    pub open spec fn align(self) -> nat {
770        self.view().align
771    }
772
773    /// Provenance of the allocation you are allowed to deallocate.
774    #[verifier::inline]
775    pub open spec fn provenance(self) -> Provenance {
776        self.view().provenance
777    }
778}
779
780/// Allocate with the global allocator.
781/// The precondition should be consistent with the [documented safety conditions on `alloc`](https://doc.rust-lang.org/alloc/alloc/trait.GlobalAlloc.html#tymethod.alloc).
782/// Returns a pointer with a corresponding [`PointsToRaw`] and [`Dealloc`] permissions.
783#[cfg(feature = "std")]
784#[verifier::external_body]
785pub fn allocate(size: usize, align: usize) -> (pt: (
786    *mut u8,
787    Tracked<PointsToRaw>,
788    Tracked<Dealloc>,
789))
790    requires
791        valid_layout(size, align),
792        size != 0,
793    ensures
794        pt.1@.is_range(pt.0.addr() as int, size as int),
795        pt.0.addr() + size <= usize::MAX + 1,
796        pt.2@@ == (DeallocData {
797            addr: pt.0.addr(),
798            size: size as nat,
799            align: align as nat,
800            provenance: pt.1@.provenance(),
801        }),
802        pt.0.addr() as int % align as int == 0,
803        pt.0@.provenance == pt.1@.provenance(),
804    opens_invariants none
805{
806    // SAFETY: valid_layout is a precondition
807    let layout = unsafe { alloc::alloc::Layout::from_size_align_unchecked(size, align) };
808    // SAFETY: size != 0
809    let p = unsafe { ::alloc::alloc::alloc(layout) };
810    if p == core::ptr::null_mut() {
811        std::process::abort();
812    }
813    (p, Tracked::assume_new(), Tracked::assume_new())
814}
815
816/// Deallocate with the global allocator.
817///
818/// The [`Dealloc`] permission ensures that the
819/// [documented safety conditions on `dealloc`](https://doc.rust-lang.org/1.82.0/core/alloc/trait.GlobalAlloc.html#tymethod.dealloc)
820/// are satisfied; by also giving up permission of the [`PointsToRaw`] permission,
821/// we ensure there can be no use-after-free bug as a result of this deallocation.
822/// In order to do so, the parameters of the [`PointsToRaw`] and [`Dealloc`] permissions must match the parameters of the deallocation.
823#[cfg(feature = "alloc")]
824#[verifier::external_body]
825pub fn deallocate(
826    p: *mut u8,
827    size: usize,
828    align: usize,
829    Tracked(pt): Tracked<PointsToRaw>,
830    Tracked(dealloc): Tracked<Dealloc>,
831)
832    requires
833        dealloc.addr() == p.addr(),
834        dealloc.size() == size,
835        dealloc.align() == align,
836        dealloc.provenance() == pt.provenance(),
837        pt.is_range(dealloc.addr() as int, dealloc.size() as int),
838        p@.provenance == dealloc.provenance(),
839    opens_invariants none
840{
841    // SAFETY: ensured by dealloc token
842    let layout = unsafe { alloc::alloc::Layout::from_size_align_unchecked(size, align) };
843    unsafe {
844        ::alloc::alloc::dealloc(p, layout);
845    }
846}
847
848/// This is meant to be a replacement for `&'a T` that allows Verus to keep track of
849/// not just the `T` value but the pointer as well.
850/// It would be better to get rid of this and use normal reference types `&'a T`,
851/// but there are a lot of unsolved implementation questions.
852/// The existence of `SharedReference<'a, T>` is a stop-gap.
853#[verifier::external_body]
854#[verifier::accept_recursive_types(T)]
855pub struct SharedReference<'a, T>(&'a T);
856
857impl<'a, T> Clone for SharedReference<'a, T> {
858    #[verifier::external_body]
859    fn clone(&self) -> (ret: Self)
860        ensures
861            ret == *self,
862    {
863        SharedReference(self.0)
864    }
865}
866
867impl<'a, T> Copy for SharedReference<'a, T> {
868
869}
870
871impl<'a, T> SharedReference<'a, T> {
872    pub uninterp spec fn value(self) -> T;
873
874    pub uninterp spec fn ptr(self) -> *const T;
875
876    #[verifier::external_body]
877    fn new(t: &'a T) -> (s: Self)
878        ensures
879            s.value() == t,
880    {
881        SharedReference(t)
882    }
883
884    #[verifier::external_body]
885    fn as_ref(self) -> (t: &'a T)
886        ensures
887            t == self.value(),
888    {
889        self.0
890    }
891
892    #[verifier::external_body]
893    fn as_ptr(self) -> (ptr: *const T)
894        ensures
895            ptr == self.ptr(),
896    {
897        &*self.0
898    }
899
900    pub axiom fn points_to(tracked self) -> (tracked pt: &'a PointsTo<T>)
901        ensures
902            pt.ptr() == self.ptr(),
903            pt.is_init(),
904            pt.value() == self.value(),
905    ;
906}
907
908/// Like [`ptr_ref`] but returns a `SharedReference` so it keeps track of the relationship
909/// between the pointers.
910/// Note the resulting reference's pointers does NOT have the same provenance.
911/// This is because in Rust models like Stacked Borrows / Tree Borrows, the pointer
912/// gets a new tag.
913#[inline(always)]
914#[verifier::external_body]
915pub fn ptr_ref2<'a, T>(ptr: *const T, Tracked(perm): Tracked<&PointsTo<T>>) -> (v: SharedReference<
916    'a,
917    T,
918>)
919    requires
920        perm.ptr() == ptr,
921        perm.is_init(),
922    ensures
923        v.value() == perm.value(),
924        v.ptr().addr() == ptr.addr(),
925        v.ptr()@.metadata == ptr@.metadata,
926    opens_invariants none
927    no_unwind
928{
929    SharedReference(unsafe { &*ptr })
930}
931
932} // verus!