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