From 51b476c776372b5185f5d855053e1c3e9a00798c Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Fri, 27 Sep 2024 19:07:22 -0400 Subject: [PATCH] vstd: add SharedRef to raw_ptr --- source/vstd/raw_ptr.rs | 87 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/source/vstd/raw_ptr.rs b/source/vstd/raw_ptr.rs index 3dd190e90..bd0a6e638 100644 --- a/source/vstd/raw_ptr.rs +++ b/source/vstd/raw_ptr.rs @@ -757,4 +757,91 @@ pub fn deallocate( } } +/// This is meant to be a replacement for `&'a T` that allows Verus to keep track of +/// not just the `T` value but the pointer as well. +/// It would be better to get rid of this and use normal reference types `&'a T`, +/// but there are a lot of unsolved implementation questions. +/// The existence of `SharedReference<'a, T>` is a stop-gap. +#[verifier::external_body] +#[verifier::accept_recursive_types(T)] +pub struct SharedReference<'a, T>(&'a T); + +impl<'a, T> Clone for SharedReference<'a, T> { + #[verifier::external_body] + fn clone(&self) -> (ret: Self) + ensures + ret == *self, + { + SharedReference(self.0) + } +} + +impl<'a, T> Copy for SharedReference<'a, T> { + +} + +impl<'a, T> SharedReference<'a, T> { + pub spec fn value(self) -> T; + + pub spec fn ptr(self) -> *const T; + + #[verifier::external_body] + fn new(t: &'a T) -> (s: Self) + ensures + s.value() == t, + { + SharedReference(t) + } + + #[verifier::external_body] + fn as_ref(self) -> (t: &'a T) + ensures + t == self.value(), + { + self.0 + } + + #[verifier::external_body] + fn as_ptr(self) -> (ptr: *const T) + ensures + ptr == self.ptr(), + { + &*self.0 + } + + #[verifier::external_body] + proof fn points_to(tracked self) -> (tracked pt: &'a PointsTo) + ensures + pt.ptr() == self.ptr(), + pt.is_init(), + pt.value() == self.value(), + { + unimplemented!(); + } +} + +/// Like [`ptr_ref`] but returns a `SharedReference` so it keeps track of the relationship +/// between the pointers. +/// Note the resulting reference's pointers does NOT have the same provenance. +/// This is because in Rust models like Stacked Borrows / Tree Borrows, the pointer +/// gets a new tag. +#[inline(always)] +#[verifier::external_body] +pub fn ptr_ref2<'a, T>(ptr: *const T, Tracked(perm): Tracked<&PointsTo>) -> (v: SharedReference< + 'a, + T, +>) + requires + perm.ptr() == ptr, + perm.is_init(), + ensures + v.value() == perm.value(), + v.ptr().addr() == ptr.addr(), + v.ptr()@.metadata == ptr@.metadata, + opens_invariants none + no_unwind +{ + SharedReference(unsafe { &*ptr }) +} + } // verus!