Struct VmState 

pub struct VmState<'ctx, 'tcx> {

    pub(crate) ctx: &'ctx Context,
    pub(crate) tcx: TyCtxt<'tcx>,
    pub(crate) caller_def_id: DefId,
    pub(crate) body: &'ctx Body<'tcx>,
    pub(crate) locals: FxHashMap<Local, VmValue<'ctx, 'tcx>>,
    pub(crate) local_addresses: FxHashMap<Local, Int<'ctx>>,
    pub(crate) local_alloc_ids: FxHashMap<Local, AllocId>,
    pub(crate) allocations: Vec<Allocation<'ctx, 'tcx>>,
    pub(crate) path_conditions: Vec<Bool<'ctx>>,
    pub(crate) definition_count: usize,
    pub(crate) next_alloc_id: usize,
    pub(crate) block_occurrences: FxHashMap<BasicBlock, usize>,
    pub(crate) binary_op_sources: FxHashMap<PlaceKey, (Option<PlaceKey>, Option<PlaceKey>)>,
    pub(crate) comparison_conds: FxHashMap<PlaceKey, Bool<'ctx>>,
    pub(crate) discriminant_terms: FxHashMap<Local, Int<'ctx>>,
    pub(crate) other_op_sources: FxHashMap<PlaceKey, (Option<PlaceKey>, Option<PlaceKey>)>,
    pub(crate) contract_flags: ContractFlags,
    pub(crate) field_values: FxHashMap<(Local, Vec<usize>), VmValue<'ctx, 'tcx>>,
    pub(crate) is_empty_len: FxHashMap<Local, Int<'ctx>>,
    pub(crate) iter_ptr_offset: FxHashMap<Local, Int<'ctx>>,
    pub(crate) bytes: FxHashMap<(AllocId, usize), ByteInfo<'ctx>>,
    pub(crate) notes: Vec<String>,
    pub(crate) path: Option<Path>,
    pub(crate) last_call_name: String,
    pub(crate) inline_depth: usize,
    pub(crate) inline_frames: Vec<InlineFrame<'ctx, 'tcx>>,
    pub(crate) not_mask_terms: FxHashSet<Int<'ctx>>,
}

The full symbolic execution state at a program point.

Accumulates locals, allocations, path conditions, and definitions as the VM steps through retained MIR items. The Z3 context is borrowed so a single context can be reused across property checks.

Fields

ctx: &'ctx Context

Shared Z3 context.

tcx: TyCtxt<'tcx>

Compiler type context.

caller_def_id: DefId

The DefId of the function whose body we are executing.

body: &'ctx Body<'tcx>

The MIR body being executed.

locals: FxHashMap<Local, VmValue<'ctx, 'tcx>>

Current value bound to each MIR local.

local_addresses: FxHashMap<Local, Int<'ctx>>

Known address for each stack-allocated local.

local_alloc_ids: FxHashMap<Local, AllocId>

Allocation ID for each stack-allocated local.

allocations: Vec<Allocation<'ctx, 'tcx>>

All known allocations.

path_conditions: Vec<Bool<'ctx>>

Accumulated path conditions (SwitchInt branches, Assert).

definition_count: usize

Monotonic counter used to uniquify fresh symbolic constant names.

next_alloc_id: usize

The next allocation ID.

block_occurrences: FxHashMap<BasicBlock, usize>

Track block occurrence counts for loop-carried value indexing.

binary_op_sources: FxHashMap<PlaceKey, (Option<PlaceKey>, Option<PlaceKey>)>

Binary op sources for guard inference: destination → (lhs, rhs) place keys.

comparison_conds: FxHashMap<PlaceKey, Bool<'ctx>>

Direct boolean condition for a comparison result place (Le/Lt/Ge/Gt/Eq/Ne), used to record precise switch-guard path conditions.

discriminant_terms: FxHashMap<Local, Int<'ctx>>

Enum discriminant term for a local holding an Option-like value whose variant is known symbolically (e.g. Iterator::next returns Some(x) iff !is_empty). Used by Rvalue::Discriminant so switchInt branches stay tied to the actual emptiness condition.

other_op_sources: FxHashMap<PlaceKey, (Option<PlaceKey>, Option<PlaceKey>)>

Non-binary-op sources (select_unpredictable, etc.): destination → (lhs, rhs) place keys. Kept separately from binary_op_sources so guard inference (infer_guard_non_null) does not treat these as pointer comparisons.

contract_flags: ContractFlags

One-shot execution/contract flags accumulated while stepping a path.

field_values: FxHashMap<(Local, Vec<usize>), VmValue<'ctx, 'tcx>>

Field-level value tracking for aggregates: (local, field_indices) → value. Example: (local_3, [0]) is local_3.0, (local_3, [0, 1]) is local_3.0.1.

is_empty_len: FxHashMap<Local, Int<'ctx>>

Locals set by iterpreter_iter_is_empty for Iter/IterMut, along with the field-based len expression. When a switchint on such local takes the false (!is_empty) branch, we inject len >= 1 as a path condition to help Z3.

iter_ptr_offset: FxHashMap<Local, Int<'ctx>>

Cumulative ptr offset for Iter/IterMut field [0] (ptr). Key: (struct_local). When post_inc_start advances the ptr by n elements, we increment this offset instead of nesting symbolic additions. This keeps Z3 expressions compact.

bytes: FxHashMap<(AllocId, usize), ByteInfo<'ctx>>

Per-byte symbolic state: (alloc_id, concrete_byte_offset) → ByteInfo. Populated by aggregate initialisation, pointer stores, and write call effects. Enables byte-level reasoning for properties like ValidCStr.

notes: Vec<String>

Notes from unsupported operations.

path: Option<Path>

The path being executed (for branch target resolution).

last_call_name: String

Name of the most recent call (for context-aware effects like Vec push).

inline_depth: usize

Current depth of the recursive exec_inline_call stack. exec_call re-enters inline execution with depth = 0 on every nested call, so a separate counter (instead of the depth argument) is needed to actually bound nested inlining and avoid unbounded recursion / stack overflow.

inline_frames: Vec<InlineFrame<'ctx, 'tcx>>

Stack of saved caller contexts for cross-function inline. The top of the stack is the frame of the function currently being inlined; each entry carries the caller’s body, def-id, and locals so the caller can be restored on exit.

not_mask_terms: FxHashSet<Int<'ctx>>

Terms that are the result of a bitwise Not (two’s-complement mask). Used to recognize x & !(align-1) alignment patterns in BitAnd so we can derive align = -mask and emit linear bounds for the result.

Implementations

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub fn resolve_origin(&self, value: &VmValue<'ctx, 'tcx>) -> Option<VmOrigin>

Trace the origin of a pointer value through VM provenance.

Given a VmValue (extracted from a checkpoint argument), follows its provenance back to determine where the allocation came from.

fn classify_local(&self, local: &Local) -> VmOriginKind

Classify a local by its type.

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub fn exec_call( &mut self, func: &Operand<'tcx>, args: &[Spanned<Operand<'tcx>>], destination: Local, _target: Option<BasicBlock>, _cleanup: Option<BasicBlock>, caller_def_id: DefId, )

Execute a call terminator.

Dispatch priority: hand-specialized handlers first, then fn_simulator summaries (whose hand-crafted invariants are more precise than inline), then inline execution of the callee’s MIR (including dependency crates), then interprocedural/effect summaries, and finally an unconstrained “unsupported call” result.

fn try_select_unpredictable( &mut self, name: &str, arg_values: &[VmValue<'ctx, 'tcx>], args: &[Spanned<Operand<'tcx>>], destination: Local, ) -> bool

select_unpredictable: result ∈ {x, y}.

fn try_slice_index( &mut self, name: &str, arg_values: &[VmValue<'ctx, 'tcx>], args: &[Spanned<Operand<'tcx>>], destination: Local, ) -> bool

Slice range indexing <[T]>::index(range) / ::index_mut(range): returns a sub-slice whose length is the range’s extent. Model it as a sub-allocation of the array so downstream into_iter/next() see the correct element count (empty for ..0). Single-element indexing (index(usize)) has a non-slice destination and keeps the plain alias behaviour from the summary table.

fn try_iter_len_is_empty( &mut self, name: &str, arg_values: &[VmValue<'ctx, 'tcx>], args: &[Spanned<Operand<'tcx>>], destination: Local, ) -> bool

Iter::len() / Iter::is_empty(): compute from struct fields (ptr + end_or_len share the same allocation with per-field offsets). The generic fn_simulator would return sizeof(Iter)/sizeof(T), which is wrong for generic T.

fn try_iter_next( &mut self, name: &str, arg_values: &[VmValue<'ctx, 'tcx>], _args: &[Spanned<Operand<'tcx>>], destination: Local, ) -> bool

Iter::next() / IterMut::next(): advance ptr by 1 and return old. The MIR calls the Iterator::next trait method, so also match the trait path (std::iter::Iterator::next) in addition to the concrete Iter/IterMut method names.

fn materialize_const_bytes_after_call( &mut self, args: &[Spanned<Operand<'tcx>>], destination: Local, )

fn exec_inline_call( &mut self, callee_def_id: DefId, arg_values: &[VmValue<'ctx, 'tcx>], caller_arg_locals: &[Option<Local>], dest: Local, ) -> bool

Recursively execute a callee’s MIR body inline.

Binds the caller’s argument values to the callee’s parameters, executes the callee’s MIR, and writes the return value to the caller’s destination local. Returns false if inline is not possible (e.g., recursion limit reached, callee has branches, or the callee is too large).

fn switch_targets_unreachable( tcx: TyCtxt<'tcx>, body: &Body<'tcx>, targets: &SwitchTargets, ) -> bool

Whether a SwitchInt’s non-otherwise targets all lead straight to panic/unreachable (a debug_assert!/assert! dispatch). Such a switch is dead on the normal path and can be inlined by following only the otherwise edge.

fn switch_is_debug_assert( tcx: TyCtxt<'tcx>, body: &Body<'tcx>, bb: BasicBlock, ) -> bool

Whether a block’s SwitchInt is a debug_assert!-style dispatch (all non-otherwise targets are panic/unreachable).

fn inline_execute_body(&mut self)

BFS-execute the callee’s MIR body.

fn apply_call_effect( &mut self, effect: &CallEffect, args: &[VmValue<'ctx, 'tcx>], caller_arg_locals: &[Option<Local>], dest: Local, )

Apply a single call effect to the VM state.

fn compute_pointer_add_align( &self, base: &VmValue<'ctx, 'tcx>, _offset: &VmValue<'ctx, 'tcx>, stride_bytes: u64, ) -> Option<u64>

Compute the preserved alignment when doing base + offset * stride. Pointer arithmetic only ever preserves the base’s alignment; it never creates it. When the base’s alignment is unknown, we cannot conclude anything about the result (a wrapping_add over misaligned storage does not become aligned just because the stride is a power of two).

pub(crate) fn propagate_const_bytes_to_tracked( &mut self, args: &[Spanned<Operand<'tcx>>], )

pub(crate) fn iter_elem_size(&self, ptr: &VmValue<'ctx, 'tcx>) -> u64

Element size (bytes) of the type iterated by an Iter/IterMut pointer.

fn iter_remaining_len(&self, local: Local) -> Option<Int<'ctx>>

Remaining element count of the Iter/IterMut backed by local (fields [0] = ptr, [1] = end_or_len). When a tracked pointer offset exists (iter_ptr_offset), prefers the compact base_len - offset form; otherwise falls back to (end.offset - ptr.offset) / elem_size.

fn interpreter_iter_len( &mut self, arg_val: &VmValue<'ctx, 'tcx>, dest: Local, ) -> bool

For Iter/IterMut types, compute len from struct fields directly instead of the generic allocation-size heuristic. Returns true if handled (value set to dest).

fn interpreter_iter_is_empty( &mut self, arg_val: &VmValue<'ctx, 'tcx>, dest: Local, ) -> bool

For Iter/IterMut types, compute is_empty from struct fields. Returns true if handled (value set to dest).

fn apply_iter_ptr_update( &mut self, _callee: DefId, cname: &str, arg_values: &[VmValue<'ctx, 'tcx>], _caller_arg_locals: &[Option<Local>], )

Apply the side effect of post_inc_start / pre_dec_end on Iter/IterMut. Only updates the tracked offset (not field values), so that the precondition check (which runs before the call executes) sees the pre-update state, while subsequent len()/is_empty() calls use base_len - offset via interpreter_iter_len.

fn find_iter_self_local(&self, arg_val: &VmValue<'ctx, 'tcx>) -> Option<Local>

If arg_val is a reference to an Iter or IterMut struct, return the local index of the referent (so field values can be looked up). Since len()/is_empty() always take &self, local 1 is the receiver.

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub fn describe(&self) -> String

Produce a compact diagnostic summary of the VM state.

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub fn execute_items(&mut self, items: &[RelevantItem<'tcx>])

Execute all retained MIR items in path order.

fn handle_callee_entry(&mut self, callee_def_id: DefId, arg_locals: &[Local])

Enter a callee’s function context during sliced inline execution. Saves the caller’s locals state, pushes the callee body onto the context stack, and binds caller args to callee parameters.

fn handle_callee_exit(&mut self, dest: Local)

Exit a callee’s function context. Captures the return value from callee’s local_0, restores the caller’s locals and body, and writes the return value to the caller’s dest local.

fn init_parameters(&mut self)

fn init_ptr_field( &mut self, local: Local, path: Vec<usize>, field_ty: Ty<'tcx>, pointee: Ty<'tcx>, local_idx: usize, idx: usize, elem_alloc: &mut FxHashMap<Ty<'tcx>, (AllocId, Int<'ctx>)>, is_raw_ptr: bool, nn_fresh_prefix: &str, )

Initialize one pointer-like field (raw pointer or NonNull<T>) of a decomposed struct/ref parameter. The first field with a given pointee type creates a shared external allocation; later fields with the same pointee reuse it with a symbolic offset, preserving relationships like ptr = start, end_or_len = start + len.

fn decompose_adt_fields( &mut self, local: Local, prefix: Vec<usize>, ty: Ty<'tcx>, local_idx: usize, elem_alloc: &mut FxHashMap<Ty<'tcx>, (AllocId, Int<'ctx>)>, depth: usize, )

Recursively decompose a (possibly nested) struct parameter into per-field symbolic values. Nested ADT fields (e.g. Handle { node: NodeRef { node: NonNull<LeafNode>, .. }, .. }) are descended into so their NonNull / raw-pointer leaves get external-allocation provenance — otherwise a NonNull buried two levels deep loses its provenance and downstream Allocated/Init checks (e.g. descend’s edges.get_unchecked) fail.

pub(crate) fn propagate_from_checkpoint(&mut self, checkpoint_block: BasicBlock)

Replay same-block assignment chains that the backward slicer may omit. Walks backwards through the CFG from the checkpoint block, propagating provenance and invariants through Use/Cast/RawPtr/CopyForDeref chains. Uses the current path to avoid cross-branch contamination.

fn propagate_pass( &mut self, checkpoint_block: BasicBlock, path_blocks: Option<&FxHashSet<BasicBlock>>, use_only: bool, )

fn is_propagate_use_kind(rvalue: &Rvalue<'tcx>) -> bool

Check if an rvalue kind should be re-propagated in the use-only pass (Use/Cast/CopyForDeref — forward-propagate existing provenance).

fn propagate_single_assign(&mut self, dest_local: Local, rvalue: &Rvalue<'tcx>)

Propagate a single MIR assignment to fill in provenance for previously uninitialised locals.

pub(crate) fn exec_statement( &mut self, block: BasicBlock, statement_index: usize, statement: &Statement<'tcx>, )

fn exec_assign(&mut self, place: &Place<'tcx>, rvalue: &Rvalue<'tcx>)

fn record_projected_store( &mut self, place: &Place<'tcx>, value: &VmValue<'ctx, 'tcx>, )

Record byte-level values when assigning to a place with projections. This handles patterns like buf[i] = 0u8 (nul-store) and arr[i] = val.

fn record_indexed_store_for_vm( &mut self, place: &Place<'tcx>, value: &VmValue<'ctx, 'tcx>, )

Track byte-level values for index-based stores (e.g. buf[i] = 0u8) that record_projected_store skips due to Index projections.

fn inject_layout_constraints( &mut self, operand: &Operand<'tcx>, val: &VmValue<'ctx, 'tcx>, )

Inject layout constraints (>= 1) for generic AlignOf/SizeOf constants.

fn eval_rvalue( &mut self, dest_place: &Place<'tcx>, rvalue: &Rvalue<'tcx>, ) -> VmValue<'ctx, 'tcx>

Evaluate an Rvalue into a VmValue.

fn eval_binary_op( &mut self, op: BinOp, lhs: &Int<'ctx>, rhs: &Int<'ctx>, ) -> Int<'ctx>

fn eval_unary_op( &mut self, op: UnOp, val: &Int<'ctx>, is_bool: bool, ) -> Int<'ctx>

fn slice_len_from_value(&self, val: &VmValue<'ctx, 'tcx>) -> Option<Int<'ctx>>

Compute the slice length for a &[T] / &mut [T] value: the allocation size divided by the element size. Reuses the allocation’s size term so it agrees with InBound/alloc.size checks.

fn provenance_for_binary_op( &self, op: BinOp, lhs: &VmValue<'ctx, 'tcx>, rhs: &VmValue<'ctx, 'tcx>, ) -> Option<Provenance<'ctx>>

Compute provenance for a binary operation on pointer values. Propagates provenance with adjusted offset for pointer arithmetic (ptr + offset, ptr - offset, Offset).

fn invariants_for_binary_op( &self, op: BinOp, lhs: &VmValue<'ctx, 'tcx>, rhs: &VmValue<'ctx, 'tcx>, provenance: &Option<Provenance<'ctx>>, ) -> ValueInvariants

Compute invariants for a binary operation. Propagates non_null from pointer arithmetic and align_n from compatible ops.

fn rhs_is_aligned_multiple(&self, val: &VmValue<'ctx, 'tcx>, align: u64) -> bool

Check if a value is known to be a multiple of align (e.g. the result of a Mul by a constant factor of align).

fn exec_storage_live(&mut self, local: Local)

fn exec_storage_dead(&mut self, local: Local)

pub(crate) fn exec_drop(&mut self, place: &Place<'tcx>)

fn exec_terminator( &mut self, block: BasicBlock, terminator: &Terminator<'tcx>, occurrence: usize, )

fn exec_switchint( &mut self, block: BasicBlock, discr: &Operand<'tcx>, targets: &SwitchTargets, occurrence: usize, )

Execute a SwitchInt terminator.

Uses the path to determine which branch is taken, then adds a path condition asserting the discriminant equals that value.

fn exec_assert( &mut self, cond: &Operand<'tcx>, expected: bool, _block: BasicBlock, _occurrence: usize, )

Execute an Assert terminator.

pub(crate) fn infer_guard_align(&mut self, cond: &Operand<'tcx>, expected: bool)

Infer alignment constraints from guards of the form (x % n) == 0.

pub(crate) fn infer_guard_non_null( &mut self, cond: &Operand<'tcx>, expected: bool, )

Infer non_null invariants from branch guards.

fn infer_switch_guard(&mut self, discr: &Operand<'tcx>)

Infer non_null from SwitchInt discriminant.

fn mark_guard_pointer(&mut self, lhs: &Option<PlaceKey>, rhs: &Option<PlaceKey>)

fn check_place_alignment(&self, place: &Place<'tcx>) -> bool

Check if a MIR place’s type alignment is statically known.

fn assert_contract_fact(&mut self, property: &Property<'tcx>)

Assert a contract fact as VM state invariants.

fn contract_target_local(&self, property: &Property<'tcx>) -> Option<Local>

Get the local referenced by a contract property’s target.

fn materialize_external_alloc( &mut self, elem_ty: Ty<'tcx>, count_term: Option<Int<'ctx>>, val_ty: Ty<'tcx>, huge: bool, ) -> VmValue<'ctx, 'tcx>

Materialize a fresh external allocation for an Allocated contract fact, returning a value carrying the allocation’s provenance.

fn assert_allocated_fact(&mut self, property: &Property<'tcx>)

Assert an Allocated(p, T, n) contract fact by materializing a fresh external allocation for the pointer-typed target.

• For a whole pointer parameter (src), the allocation is sized n * sizeof(T) so downstream pointer arithmetic stays in bounds.
• For a plain pointer field (e.g. RawVecInner::ptr), the allocation is written back to the field via set_contract_target_value, and is unbounded so field-subrange InBound checks auto-pass.
• For IterElements/Downcast targets (e.g. buckets.iter()), the container itself is not a pointer — keep the legacy whole-local behaviour.

fn contract_field_path( &self, property: &Property<'tcx>, ) -> Option<(Local, Vec<usize>)>

Resolve a contract place to (local, field_path). Field projections are accumulated into field_path; Downcast/IterElements terminate the path (they unwrap the value in place).

fn contract_target_value( &mut self, property: &Property<'tcx>, ) -> Option<VmValue<'ctx, 'tcx>>

Get the VmValue for a contract property’s target, following field projections so that Align(self.heap, T) resolves to the heap field value rather than the whole self reference.

fn set_contract_target_value( &mut self, property: &Property<'tcx>, val: VmValue<'ctx, 'tcx>, )

Write a contract target value back to its (possibly field) location.

fn contract_alloc_id_field_aware( &mut self, property: &Property<'tcx>, ) -> Option<AllocId>

Resolve the alloc_id for a contract property target, following field projections to locate the actual field value’s provenance.

fn resolve_contract_count(&self, arg: &PropertyArg<'tcx>) -> Option<Int<'ctx>>

Resolve a contract count argument to a Z3 term by looking up the corresponding function parameter in the VM state.

fn eval_predicate_as_bool( &self, pred: &NumericPredicate<'tcx>, ) -> Option<Bool<'ctx>>

Evaluate a numeric predicate to a Z3 Bool for path-condition assertion.

fn eval_contract_expr_simple( &self, expr: &ContractExpr<'tcx>, ) -> Option<Int<'ctx>>

fn eval_contract_expr_simple_value( &self, expr: &ContractExpr<'tcx>, ) -> Option<VmValue<'ctx, 'tcx>>

fn try_simple_iter_len( &self, arg_val: &VmValue<'ctx, 'tcx>, ) -> Option<Int<'ctx>>

Try field-based len for Iter/IterMut references (same logic as interpreter_iter_len in call.rs). Used by eval_contract_expr_simple so that ContractFact assertions use the same symbolic term as the VM execution path.

fn try_simple_iter_len_from_pred( &self, pred: &NumericPredicate<'tcx>, ) -> Option<Int<'ctx>>

For a predicate of the form self.len() != 0 (i.e. !self.is_empty()), if the self is an Iter/IterMut reference, return the field-based len term so that a len >= 1 constraint can be added.

fn inject_is_empty_len(&mut self, discr: &Operand<'tcx>)

If discr is a local that was set by iterpreter_iter_is_empty for an Iter/IterMut struct, push len >= 1 as a path condition.

fn track_iter_ptr_update(&mut self, local: Local)

If local is a reference to Iter/IterMut and field 0 (ptr) is updated, increment the cumulative ptr offset so that interpreter_iter_len can express len = initial_len - offset instead of nested (end - (ptr + sz + sz + ...)) / sz.

fn track_iter_ptr_after_inline(&mut self)

After inlining post_inc_start/pre_dec_end for Iter/IterMut, increment the tracked ptr offset so that interpreter_iter_len can compute base_len - offset compactly.

fn set_non_null_for_value( &mut self, property: &Property<'tcx>, val: VmValue<'ctx, 'tcx>, )

Set non_null invariant on the target value.

fn set_in_bounds_for_value( &mut self, property: &Property<'tcx>, val: VmValue<'ctx, 'tcx>, )

fn assert_in_bound_for_each( &mut self, property: &Property<'tcx>, fe_place: &ContractPlace<'tcx>, )

fn set_align_for_value( &mut self, property: &Property<'tcx>, val: VmValue<'ctx, 'tcx>, )

Set align invariant on the target value.

fn set_init_for_value( &mut self, property: &Property<'tcx>, val: VmValue<'ctx, 'tcx>, )

Set init invariant on the target value and its allocation.

fn set_owning_for_value(&mut self, val: VmValue<'ctx, 'tcx>)

Set owning invariant on the target value.

fn find_nn_pointee(&self, ty: Ty<'tcx>) -> Option<Ty<'tcx>>

Extract the pointee type if ty is NonNull<P> or wrapped in Option<NonNull<P>>. Returns Some(P).

fn try_as_ptr_fallback( &mut self, dest: Local, func: &Operand<'tcx>, first_arg_val: VmValue<'ctx, 'tcx>, first_arg_op: &Operand<'tcx>, ) -> bool

Try to propagate provenance from pointer-extracting calls (e.g. as_ptr, as_mut_ptr). Returns true if applied. Try to propagate provenance from pointer-extracting calls (e.g. as_ptr, as_mut_ptr). Returns true if applied.

pub(crate) fn try_materialize_const_bytes( &mut self, val: &mut VmValue<'ctx, 'tcx>, operand: &Operand<'tcx>, )

If operand is a constant reference to a byte array (e.g. b"hello\0"), extract the raw bytes and create a tracked allocation. Updates val in-place with the proper provenance and invariants.

pub(crate) fn trace_to_const_bytes( &self, operand: &Operand<'tcx>, ) -> Option<Vec<u8>>

fn propagate_field_values_to_ref( &mut self, source_place: &Place<'tcx>, dest: Local, )

Propagate byte values from a source place’s allocation to the provenance allocation of a reference. This ensures that when we create &bytes from an aggregate, the byte-level tracking follows. Propagate a source place’s per-field values to a reference destination, shifting the field path by the source place’s Field projection prefix. E.g. for _3 = &(_1.0) where _1 is a Handle { node: NodeRef { node: NonNull<..>, .. }, .. }, the nested NonNull’s field value stored at path [0, 1] becomes available at _3’s path [1], so an inlined callee that dereferences _3 and reads its node field sees the provenance of the underlying allocation.

fn propagate_byte_values_to_ref( &mut self, source_place: &Place<'tcx>, ref_val: &VmValue<'ctx, 'tcx>, )

fn aggregate_field_tys(&self, ty: Ty<'tcx>) -> Vec<Ty<'tcx>>

Return the per-field types for an aggregate’s operands.

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub fn address_of_place( &mut self, place: &Place<'tcx>, ) -> Option<VmValue<'ctx, 'tcx>>

pub(crate) fn ensure_local_allocation(&mut self, local: Local)

Lazily create a stack allocation for a MIR local if one doesn’t exist.

pub(crate) fn field_offset_in_bytes( &self, ty: Ty<'tcx>, field_idx: usize, ) -> u64

pub fn size_of_ty(&self, ty: Ty<'tcx>) -> u64

pub fn align_of_ty(&self, ty: Ty<'tcx>) -> u64

pub fn alloc_for_local(&self, local: Local) -> Option<AllocId>

pub fn allocation_size(&self, alloc_id: AllocId) -> Option<&Int<'ctx>>

pub fn allocation_base(&self, alloc_id: AllocId) -> Option<&Int<'ctx>>

pub fn pointee_elem_size(&self, ty: Ty<'tcx>) -> u64

Get the element size (in bytes) for a pointer type, peeling through *const T, *mut T, &T, and &[T] to find size_of(T).

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub fn new( ctx: &'ctx Context, tcx: TyCtxt<'tcx>, body: &'ctx Body<'tcx>, caller_def_id: DefId, ) -> Self

Create a fresh VM state for executing a path.

pub fn local_value(&self, local: Local) -> Option<&VmValue<'ctx, 'tcx>>

Look up the value bound to a MIR local.

pub fn set_local(&mut self, local: Local, value: VmValue<'ctx, 'tcx>)

Bind a value to a MIR local.

pub fn local_address(&mut self, local: Local) -> Int<'ctx>

Get or create the symbolic address of a MIR local.

pub fn allocate( &mut self, size: Int<'ctx>, align: u64, element_ty: Option<Ty<'tcx>>, ) -> (AllocId, Int<'ctx>)

Allocate a fresh symbolic object and return its ID and base address.

pub fn allocate_external( &mut self, size: Int<'ctx>, align: u64, element_ty: Option<Ty<'tcx>>, ) -> (AllocId, Int<'ctx>)

Allocate a fresh external allocation (for raw-pointer parameters). External allocations may be null and have unlimited size.

pub(crate) fn alloc(&self, id: AllocId) -> &Allocation<'ctx, 'tcx>

Indexed access to an allocation by its AllocId (the id is the index).

pub(crate) fn alloc_mut(&mut self, id: AllocId) -> &mut Allocation<'ctx, 'tcx>

Mutable indexed access to an allocation by its AllocId.

pub fn fresh_int(&self, prefix: &str) -> Int<'ctx>

Create a symbolic Z3 int constant.

pub fn record_definition(&mut self)

Bump the symbolic-name uniquifier (called once per executed assignment).

pub fn field_value( &self, local: Local, path: &[usize], ) -> Option<&VmValue<'ctx, 'tcx>>

Get the value of a specific field within an aggregate local.

pub fn set_field_value( &mut self, local: Local, path: Vec<usize>, value: VmValue<'ctx, 'tcx>, )

Set the value of a specific field within an aggregate local.

pub fn record_byte_value( &mut self, alloc_id: AllocId, offset: usize, term: Int<'ctx>, )

Record a per-byte symbolic value at a concrete offset in an allocation.

pub fn mark_byte_init(&mut self, alloc_id: AllocId, offset: usize)

Mark a byte as initialized without changing its value.

pub fn mark_byte_nul(&mut self, alloc_id: AllocId, offset: usize)

Mark a byte as known NUL (0x00).

pub fn mark_byte_non_nul(&mut self, alloc_id: AllocId, offset: usize)

Mark a byte as known non-NUL (!= 0x00).

pub fn get_byte_value( &self, alloc_id: AllocId, offset: usize, ) -> Option<&Int<'ctx>>

Look up a per-byte Z3 term for a concrete offset in an allocation.

pub fn is_byte_init(&self, alloc_id: AllocId, offset: usize) -> bool

Check whether a byte at a concrete offset is known to be initialized.

pub fn is_byte_nul(&self, alloc_id: AllocId, offset: usize) -> bool

Check whether a byte at a concrete offset is known to be NUL.

pub fn is_byte_non_nul(&self, alloc_id: AllocId, offset: usize) -> bool

Check whether a byte at a concrete offset is known to be non-NUL.

pub fn alloc_byte_values(&self, alloc_id: AllocId) -> Vec<(usize, &Int<'ctx>)>

Return all known (offset, term) pairs for an allocation, sorted by offset.

pub fn alloc_nul_offsets(&self, alloc_id: AllocId) -> Vec<usize>

Collect all offsets known to be NUL in an allocation.

pub fn alloc_non_nul_offsets(&self, alloc_id: AllocId) -> Vec<usize>

Collect all offsets known to be non-NUL in an allocation.

pub(crate) fn copy_byte_tracking(&mut self, src: AllocId, dst: AllocId)

Copy all per-byte tracking (value, init, NUL knowledge) from one allocation to another.

pub fn assert_all(&self, solver: &Solver<'ctx>)

Assert path conditions and invariant constraints into a solver.

impl<'ctx, 'tcx> VmState<'ctx, 'tcx>

pub(crate) fn value_of_operand( &self, operand: &Operand<'tcx>, ) -> VmValue<'ctx, 'tcx>

Extract a VmValue from a MIR operand.

pub(crate) fn value_of_place( &self, place: &Place<'tcx>, ) -> Option<VmValue<'ctx, 'tcx>>

Look up the value stored at a MIR place.

pub(crate) fn unknown_value_for_place( &self, place: &Place<'tcx>, ) -> VmValue<'ctx, 'tcx>

Create an unknown value for a place.

Trait Implementations

impl Debug for VmState<'_, '_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.