Module alias_hazard 

MIR-level alias hazard scanning for the symbolic VM backend.

This module holds the pure MIR hazard analysis (origin-based parameter safety, escape analysis, local hazard scanning, and ownership-transfer violation scanning) independent of VM state and Z3 terms. It was extracted from the old forward verifier’s smt_check/alias.rs.

vm/alias.rs provides the VM-specific provenance→origin resolution and orchestrates the overall alias check, calling into this module for the underlying MIR scanning.

Structs

LocalCallsite 🔒

Enums

AliasProducer 🔒

HazardCheck 🔒

HazardKind 🔒

RawAccessKind 🔒

Functions

alias_producer 🔒

alias_proved_for_param_local 🔒

alias_proved_for_param_local_from_origin 🔒

any_struct_field_origin 🔒

callsite_arg_origins 🔒

check_fn_against_field 🔒

Check whether item (a struct method or a same-module free function) writes or exposes the raw field origin through the borrow carried by self_local. A shared current borrow (&self) is not invalidated by a mutable item borrow (&mut self), and a mutable/mutable pair is likewise fine; any other combination is a violation. Returns the violation description, or None.

destination_flows_to_return 🔒

escaped_self_field_violation 🔒

expand_hazard_alias_locals 🔒

expand_origin_aliases 🔒

find_as_ptr_receivers 🔒

free_fns_for_struct 🔒

Collect the free functions in the struct’s own module that take a &Struct / &mut Struct parameter. Rust privacy is module-scoped, so only those can reach a private raw field. Each entry pairs the function with the parameter locals that carry the struct reference.

hazard_used_after_block 🔒

hazard_used_after_statement 🔒

impls_for_struct 🔒

is_origin_a_reference 🔒

is_ptr_add_offset_eq 🔒

is_ptr_from_ptr_add 🔒

kill_strongly_updated_origins 🔒

live_locals_at 🔒

Compute the set of locals that are live (between StorageLive and StorageDead) at the deref point (call_block, statement_index), scanning the function in execution order up to that point. Used by the callsite shared-XOR-mutable check to ignore temporaries that have already gone dead (e.g. a method call’s &self receiver).

local_callsites 🔒

local_hazard_violation 🔒

local_hazard_violation_with 🔒

local_traces_to_self_field 🔒

Backward-traces local through MIR assignments to check whether its value is derived from (*self_local).field_index.

method_exposes_self_field 🔒

Whether method returns a raw-pointer-bearing value derived from the field field_index of the struct borrowed via self_local, i.e. it leaks the raw field to the caller.

method_writes_self_field 🔒

Whether method writes through the raw field field_index of the struct borrowed via self_local (_1 for a method, any parameter for a free fn).

ownership_transfer_violation 🔒

param_index_of_origin 🔒

Return the 0-based argument index for origin when it is a direct, whole raw-pointer parameter (no field projections, no local-copy tracing).

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 🔒

Whether place is a raw-pointer deref whose operand traces back to the field field_index of the struct borrowed via self_local.

places_holding_transferred_pointer 🔒

pre_existing_view_on_origin 🔒

private_fn_callsite_delegation 🔒

public_raw_field 🔒

raw_access_conflicts 🔒

resolve_mir_place_tree 🔒

Resolve a MIR place through the alias tree: a field-projected place resolves to itself; a whole-local place resolves to its ultimate origin.

resolve_param_origin 🔒

Resolve origin to a parameter MIR local, tracing through local-copy origins when the base is not itself a parameter.

resolve_place_key_tree 🔒

Resolve a place’s local through the alias tree (ignoring the place’s own field projections), falling back to the MIR place itself when unmapped.

resolve_via_tree 🔒

Resolve (local, fields) through the alias tree: a place that already names a field path resolves to itself; a whole-local place resolves to its ultimate (root, fields) origin.

reverse_postorder_blocks 🔒

rvalue_copies_live_origin_value 🔒

rvalue_mentions_any_local 🔒

rvalue_mentions_local 🔒

rvalue_mentions_origin 🔒

rvalue_reads_any_origin 🔒

rvalue_reads_like_view 🔒

self_borrow_mutability 🔒

The mutability (Not / Mut) of the borrow carried by self_local’s type (a &T / &mut T), or None if it is not a reference. self_local is _1 for a method receiver, and any parameter for a free function.

self_field_key 🔒

The PlaceKey for (*self_local).field_index.

self_field_origin 🔒

splice_holder_fields 🔒

statement_uses_any_local 🔒

struct_ref_param_locals 🔒

Return the parameter locals of def_id whose type is a &Struct / &mut Struct reference to struct_def_id.

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 🔒