Expand description
Shared alias hazard analysis for both legacy and VM backends.
This module extracts the MIR-level hazard scanning logic from
smt_check/alias.rs and makes it independent of the old forward
verifier (ForwardVisitResult, PtsGraph, SmtChecker).
The VM backend provides its own origin resolution via
vm/alias.rs and calls into this module for hazard scanning.
Structs§
Enums§
Functions§
- alias_
from_ 🔒rvalue - alias_
producer - alias_
proved_ for_ param_ local - alias_
proved_ for_ param_ local_ from_ origin - any_
struct_ field_ origin - as_
ptr_ provenance_ origins - blocks_
reachable_ after_ call - Collect all basic blocks reachable after (and including) a call block.
- call_
destination - Return the destination local for a checkpoint’s call or deref.
- call_
target_ 🔒def_ id - callsite_
arg_ origins - collect_
place_ aliases - Build a mapping from MIR locals to their resolved PlaceKey origins.
- deep_
resolve_ place - Follow local-origin associations transitively to resolve to the ultimate source (parameter or root local) and accumulated field path.
- destination_
flows_ to_ return - escaped_
self_ field_ violation - expand_
hazard_ 🔒alias_ locals - expand_
origin_ 🔒aliases - find_
as_ 🔒ptr_ receivers - hazard_
used_ 🔒after_ block - hazard_
used_ 🔒after_ statement - impls_
for_ 🔒struct - is_
origin_ a_ reference - is_
ownership_ 🔒return_ api - is_
ownership_ 🔒transfer_ terminator - is_
ptr_ 🔒add_ offset_ eq - is_
ptr_ 🔒from_ ptr_ add - is_
vec_ 🔒invalidating_ method - kill_
strongly_ 🔒updated_ origins - local_
callsites - local_
hazard_ violation - local_
hazard_ violation_ with - local_
traces_ 🔒to_ self_ field - method_
exposes_ 🔒self_ field - method_
writes_ 🔒self_ field - operand_
mir_ place - Extract the MIR Place from an operand.
- operand_
place - Extract a PlaceKey from a MIR operand.
- ownership_
transfer_ violation - param_
index_ of_ origin - place_
is_ 🔒raw_ access_ to_ any_ origin - place_
is_ 🔒raw_ access_ to_ live_ origin - place_
is_ 🔒raw_ access_ to_ origin - place_
key_ 🔒is_ prefix_ of - place_
raw_ 🔒accesses_ self_ field - places_
holding_ 🔒transferred_ pointer - pre_
existing_ 🔒view_ on_ origin - private_
fn_ callsite_ delegation - public_
raw_ 🔒field - raw_
access_ conflicts - resolve_
mir_ place - Resolve a MIR place through alias mapping to get a canonical PlaceKey.
- resolve_
param_ origin - resolve_
place_ 🔒for_ key - reverse_
postorder_ 🔒blocks - rvalue_
any_ place_ matching - Check whether any MIR place used in an rvalue matches a predicate.
- rvalue_
copies_ 🔒live_ origin_ value - rvalue_
has_ 🔒hazard_ local_ base - rvalue_
mentions_ 🔒any_ local - rvalue_
mentions_ 🔒local - rvalue_
mentions_ 🔒origin - rvalue_
reads_ 🔒any_ origin - rvalue_
reads_ 🔒like_ view - rvalue_
reads_ 🔒live_ origin - self_
borrow_ 🔒mutability - self_
field_ 🔒key - self_
field_ origin - splice_
holder_ 🔒fields - statement_
uses_ 🔒any_ local - terminator_
invalidates_ 🔒vec_ owner - terminator_
is_ 🔒benign_ origin_ use - terminator_
returns_ 🔒ownership - terminator_
uses_ 🔒any_ local - terminator_
uses_ 🔒live_ origin - terminator_
uses_ 🔒origin - terminator_
writes_ 🔒origin - trace_
place_ root - Trace a place back to its root local via local origin map.
- trace_
raw_ ptr_ through_ call - Trace a raw pointer local back through call terminators to find the
originating place (e.g. slice from
get_unchecked). - type_
contains_ 🔒ref_ or_ ptr - vec_
owners_ 🔒for_ origins