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!