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!