Enum miri::Provenance
source · pub enum Provenance {
Concrete {
alloc_id: AllocId,
tag: BorTag,
},
Wildcard,
}
Expand description
Pointer provenance.
Variants§
Concrete
For pointers with concrete provenance. we exactly know which allocation they are attached to and what their borrow tag is.
Wildcard
Pointers with wildcard provenance are created on int-to-ptr casts. According to the specification, we should at that point angelically “guess” a provenance that will make all future uses of this pointer work, if at all possible. Of course such a semantics cannot be actually implemented in Miri. So instead, we approximate this, erroring on the side of accepting too much code rather than rejecting correct code: a pointer with wildcard provenance “acts like” any previously exposed pointer. Each time it is used, we check whether some exposed pointer could have done what we want to do, and if the answer is yes then we allow the access. This allows too much code in two ways:
- The same wildcard pointer can “take the role” of multiple different exposed pointers on subsequent memory accesses.
- In the aliasing model, we don’t just have to know the borrow tag of the pointer used for the access, we also have to update the aliasing state – and that update can be very different depending on which borrow tag we pick! Stacked Borrows has support for this by switching to a stack that is only approximately known, i.e. we over-approximate the effect of using any exposed pointer for this access, and only keep information about the borrow stack that would be true with all possible choices.
Trait Implementations§
source§impl Clone for Provenance
impl Clone for Provenance
source§fn clone(&self) -> Provenance
fn clone(&self) -> Provenance
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source
. Read moresource§impl Debug for Provenance
impl Debug for Provenance
source§impl Hash for Provenance
impl Hash for Provenance
source§impl PartialEq for Provenance
impl PartialEq for Provenance
source§impl Provenance for Provenance
impl Provenance for Provenance
source§const OFFSET_IS_ADDR: bool = true
const OFFSET_IS_ADDR: bool = true
We use absolute addresses in the offset
of a Pointer<Provenance>
.
source§fn get_alloc_id(self) -> Option<AllocId>
fn get_alloc_id(self) -> Option<AllocId>
OFFSET_IS_ADDR == false
, provenance must always be able to
identify the allocation this ptr points to (i.e., this must return Some
).
Otherwise this function is best-effort (but must agree with Machine::ptr_get_alloc
).
(Identifying the offset in that allocation, however, is harder – use Memory::ptr_get_alloc
for that.)