Struct VmState 

pub(crate) struct VmState<'z3, 'tcx> {
    pub(crate) z3_ctx: &'z3 Context,
    pub(crate) tcx: TyCtxt<'tcx>,
    pub(crate) current_frame: FrameState,
    pub(crate) caller_frames: Vec<FrameState>,
    pub(crate) units: Vec<MemoryUnit<'z3, 'tcx>>,
    pub(crate) constraints: Constraints<'z3, 'tcx>,
    pub(crate) inline: InlineCtx<'z3, 'tcx>,
    pub(crate) path_facts: PathFacts,
}

The full symbolic execution state at a program point.

Accumulates the name → allocation bindings, allocations, and solver constraints as the VM steps through retained MIR items. The Z3 context is borrowed so a single context can be reused across property checks.

Fields

z3_ctx: &'z3 Context

Shared Z3 context.

tcx: TyCtxt<'tcx>

Compiler type context.

current_frame: FrameState

caller_frames: Vec<FrameState>

Stack of saved caller frames for path-replay inlining (CalleeEntry/CalleeExit items). Together with Self::current_frame (the current frame) it forms the call stack: entering an inlined callee moves the current frame here, exiting restores it.

units: Vec<MemoryUnit<'z3, 'tcx>>

The object space: one MemoryUnit per allocation, indexed by AllocId. Each unit carries its shape (Allocation) and its contents (per-byte state + per-allocation typed values).

constraints: Constraints<'z3, 'tcx>

Solver constraints and term caches accumulated along the current path.

inline: InlineCtx<'z3, 'tcx>

Recursive-inlining scratch state (depth and per-call temporary bindings pushed/popped on inline entry/exit).

path_facts: PathFacts

Per-path facts (latched while stepping, or derived in Self::new), read by the property checker.

Implementations

impl<'z3, 'tcx> VmState<'z3, 'tcx>

pub(crate) fn resolve_origin( &self, value: &VmValue<'z3, '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<'z3, 'tcx> VmState<'z3, 'tcx>

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

Execute a call terminator.

Dispatch priority: hand-specialized handlers first, then builtin_models 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_slice_index( &mut self, callee: Option<DefId>, arg_values: &[VmValue<'z3, '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_slice_get( &mut self, callee: Option<DefId>, arg_values: &[VmValue<'z3, 'tcx>], args: &[Spanned<Operand<'tcx>>], destination: Local, ) -> bool

Slice range get <[T]>::get(range) / ::get_mut(range): returns Option<&[T]> whose Some payload is a sub-slice with the range’s extent. Mirrors try_slice_index, but stores the sub-slice under field 0 (the Some payload) so a downstream slice.len() / memchr(x, subslice) sees the correct element count and provenance.

fn try_iter_len_is_empty( &mut self, name: &str, arg_values: &[VmValue<'z3, '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 builtin_models would return sizeof(Iter)/sizeof(T), which is wrong for generic T.

fn try_nonnull_new( &mut self, callee: Option<DefId>, arg_values: &[VmValue<'z3, 'tcx>], destination: Local, ) -> bool

NonNull::<T>::new(ptr) -> Option<NonNull<T>>: the safe constructor returns Some iff ptr is non-null. Its body branches on ptr.is_null(), so exec_inline_call (branch-free only) cannot inline it. Model the null-check directly from provenance, mirroring check_non_null: internal provenance or a set non_null/in_bounds invariant means the pointer is definitely non-null (Some(ptr)), and otherwise the Option is left symbolic (it may be None).

fn try_iter_next( &mut self, name: &str, arg_values: &[VmValue<'z3, '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<'z3, '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_discr_const(body: &Body<'tcx>, discr: &Operand<'tcx>) -> Option<u64>

Resolve a SwitchInt discriminant to a constant u64, following a single local-assignment chain (a cfg!-style runtime-check flag).

fn inline_execute_body(&mut self)

BFS-execute the callee’s MIR body.

fn set_dest_as_heap_ptr(&mut self, arg_val: &VmValue<'z3, 'tcx>, dest: Local)

Clone arg_val, retype it to dest’s type, mark it as a non-null, aligned, initialized pointer, and bind it to dest.

fn try_size_align_effect( &mut self, func: &Operand<'tcx>, destination: Local, ) -> bool

For a size_of::<T>() / align_of::<T>() call whose T is generic (no concrete layout), bind the destination to the shared symbolic sizeof_T / align_T so it agrees with size_sym/align_sym. Returns true when handled. Concrete layouts are left to eff_layout_const.

fn apply_binary_num( &mut self, dest: Local, args: &[VmValue<'z3, 'tcx>], lhs_arg: usize, rhs_arg: usize, f: impl Fn(&Int<'z3>, &Int<'z3>) -> Int<'z3>, )

Apply a binary numeric effect: compute f(lhs.z3_term, rhs.z3_term) and store it as the destination’s fresh scalar value.

fn apply_unary_num( &mut self, dest: Local, args: &[VmValue<'z3, 'tcx>], arg: usize, f: impl Fn(&Int<'z3>) -> Int<'z3>, )

Apply a unary numeric effect: compute f(a.z3_term) and store it as the destination’s fresh scalar value.

pub(crate) fn apply_call_effect( &mut self, effect: &CallEffect, args: &[VmValue<'z3, 'tcx>], caller_arg_locals: &[Option<Local>], dest: Local, callee: Option<DefId>, )

Apply a single call effect to the VM state.

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

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).

fn pointer_stride_term(&mut self, dest: Local, stride: Option<u64>) -> Int<'z3>

The byte stride for a pointer add/sub: the fixed stride, or the pointee’s symbolic size when the stride is element-sized (a generic T).

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

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

Element size of the type iterated by an Iter/IterMut pointer, symbolic (sizeof_T) for a generic element type so size / elem_size cancels.

pub(crate) fn iter_len_from_ptrs( &self, ptr: &VmValue<'z3, 'tcx>, end: &VmValue<'z3, 'tcx>, ) -> Option<Int<'z3>>

Element count from two pointer fields sharing the same allocation: (end.offset - ptr.offset) / elem_size. When both pointers carry an element-structured offset (OffsetKind::Element, or the base), the count is computed element-wise (end_elem - ptr_elem) so the (end·S - ptr·S)/S division is avoided for a generic element size S.

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

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<'z3, '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 apply_iter_ptr_update( &mut self, callee: DefId, arg_values: &[VmValue<'z3, 'tcx>], )

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.

pub(crate) fn find_local_by_address(&self, term: &Int<'z3>) -> Option<Local>

Find the local whose symbolic address matches term (the address a reference value points at). Used to resolve a &self/&mut self receiver (often a reborrow temp) back to the referent local that carries the materialized field values.

pub(crate) fn find_whole_reborrow_referent(&self, local: Local) -> Option<Local>

Resolve a whole-place reborrow (_7 = &mut (*_1) / _7 = &(*_1), projection exactly [Deref]) back to its referent local. Used to propagate the referent’s materialized field values into an inlined callee when the reborrow temp’s own forward assignment was pruned from the slice (so its value is still the stack-address default and find_local_by_address can only self-match). Deliberately excludes field reborrows (&mut (*_x).field) — those address a subfield, whose value is tracked separately, so propagating the whole struct’s fields would be wrong (BTreeMap’s NodeRef handles).

pub(crate) fn find_field_reborrow_referent( &self, local: Local, ) -> Option<(Local, Vec<usize>)>

Resolve a field reborrow (_7 = &mut (*_x).field, projection [Deref, Field(..)*]) back to its referent local plus the field path.

pub(crate) fn find_copy_root(&self, local: Local) -> Option<Local>

Resolve a whole-place copy root: _x = copy _y / _x = move _y (no projection) traces _x back to _y. Used to recover a value parameter’s materialized fields when the optimizer inserted a copy temporary between the caller’s argument and the inlined callee’s parameter (e.g. get_ext’s _2 = copy _1 before NonZero::get(move _2)), so that handle_callee_entry’s field collection can follow the copy chain to the local that actually carries the fields.

fn find_iter_self_local(&self, arg_val: &VmValue<'z3, '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.

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

Derive an element count from the backing allocation (size / elem_size). Used by ReturnLengthOfArg and the fallback in ReturnFieldOfArg (slices, &str, and Vec values whose {buf{ptr,cap}, len} field was not materialized). Returns true when a value was produced.

fn apply_field_of_arg_effect( &mut self, arg: usize, field: usize, sub_offset: Option<u64>, args: &[VmValue<'z3, 'tcx>], caller_arg_locals: &[Option<Local>], dest: Local, )

Apply a ReturnFieldOfArg/ReturnFieldOfArgSub effect: read the materialized field field of the receiver’s pointee and return it, preserving the field’s own type/provenance. For ReturnFieldOfArgSub, subtract sub_offset elements from the field pointer (next_back_unchecked after pre_dec_end).

The receiver of a &self getter is a reborrow temp (_t = &data) whose local carries no field values, while the fields were materialized on the referent (data). Resolve the referent by matching the receiver value’s address term against the known local addresses; fall back to the direct arg local.

fn apply_range_effect( &mut self, bounds_arg: usize, args: &[VmValue<'z3, 'tcx>], caller_arg_locals: &[Option<Local>], dest: Local, )

Apply a ReturnRange effect: model slice::range(range, bounds) returning Range { start, end } with 0 <= start <= end <= bounds.end. The bounds argument is a RangeTo<usize> whose field 0 carries the slice length; the returned Range<usize> fields are fresh symbols bound by the range invariant.

pub(crate) fn materialize_vec_fields( &mut self, local: Local, ptr: VmValue<'z3, 'tcx>, cap: Int<'z3>, len: Int<'z3>, )

Compute the (ptr, cap, len) field paths of a Vec-shaped local, handling both the std Vec<T> layout { buf: RawVec { ptr, cap }, len } and the flat local re-implementation { ptr: NonNull, len, cap } used by the std-challenge suites. Materialize the {ptr, cap, len} field values of a Vec<T> aggregate at local. The backing-buffer pointer is written to the owning raw pointer field (located generically via Self::container_ptr_field); the len/cap are no longer materialized as fields — they are asserted as path conditions and tracked by the backing allocation’s slice length.

The symbolic invariant 0 <= len <= cap and cap * elem_size <= isize::MAX is asserted as a path condition so downstream len() / capacity() / InBound / ValidNum queries agree.

pub(crate) fn materialize_vec_len_cap( &mut self, cap: Int<'z3>, len: Int<'z3>, elem_size: u64, )

Assert the Vec length/capacity invariants 0 <= len <= cap and cap * elem_size <= isize::MAX as path conditions.

impl<'z3, 'tcx> VmState<'z3, 'tcx>

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

Execute all retained MIR items in path order.

fn handle_callee_entry(&mut self, callee: DefId, arg_locals: &[usize])

Enter an inlined callee during path execution: save the caller context, switch to the callee body, and bind the caller’s argument locals to the callee’s parameters.

fn handle_callee_exit(&mut self, dest: usize)

Exit an inlined callee: capture the callee’s return value, restore the caller context, and write the return value to the caller’s destination.

fn init_parameters(&mut self)

fn materialize_external_field( &mut self, local: Local, idx: usize, field_ty: Ty<'tcx>, elem_ty: Ty<'tcx>, alive_region: Option<Region<'tcx>>, )

Materialize a struct field holding a reference (&T / &[T]), a DST slice ([T]), or a heap-backed smart pointer (Box/Vec) as an external allocation, so field access (e.g. self.buckets.iter(), as_ptr()) resolves to the data rather than the whole struct. The caller pre-computes elem_ty (the pointee / slice element). alive_region carries the lifetime of a reference field (&'a T), marking its referent alive for 'a (a reference guarantees its referent is alive); a raw slice / Box / Vec field carries no such guarantee and passes None.

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<'z3>)>, 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<'z3>)>, 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.

fn field_term_from_bytes( &self, alloc_id: AllocId, offset: usize, size: usize, ) -> Option<Int<'z3>>

Read a scalar field’s value back out of the byte layer over [offset, offset + size) (little-endian). Returns None when the byte layer does not cover the whole field (a hole, or no byte written), so the caller falls back to a fresh symbol.

This is the byte→field direction of the cast cross-view materialization: when bytes are written first (*buf = 3) and the buffer is then reinterpreted as a repr(C) struct, the field value is those bytes, not an unrelated fresh symbol.

fn decompose_pointee_fields( &mut self, alloc_id: AllocId, prefix: Vec<usize>, ty: Ty<'tcx>, root_ty: Ty<'tcx>, local_idx: usize, depth: usize, byte_offset: usize, )

Recursively decompose a pointee ADT’s fields into per-allocation field tracking, mirroring decompose_adt_fields but keyed by allocation instead of local. This is what lets a &*NonNull<LeafNode> dereference resolve (*leaf).len to the actual len field value rather than the raw pointer term.

byte_offset is the running byte offset of the field being decomposed, used for the byte→field cross-view materialization (see Self::field_term_from_bytes).

pub(crate) fn exec_statement(&mut self, 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<'z3, '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<'z3, '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<'z3, 'tcx>, )

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

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

HACK: slice::align_to_offsets computes its element split via const { gcd(size_of::<T>(), size_of::<U>()) }. The recursive gcd const fn cannot be inlined, so the VM would otherwise model the result as a fresh, unconstrained constant and lose the one fact that makes the proof go through: the gcd divides both sizes. That divisibility is what turns us = sizeof_T / gcd / ts = sizeof_U / gcd into exact divisions, giving us * sizeof_U == ts * sizeof_T (both the lcm) and hence us_len * sizeof_U <= len * sizeof_T. Detect the gcd const block and re-establish gcd’s key consequences as path conditions. This is a targeted workaround for a missing general property of recursive const fns, not an align_to-specific effect.

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

The provenance allocation’s alignment, when it is non-trivial (≠ 1).

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

Evaluate an Rvalue into a VmValue.

fn bool_as_int(&self, cond: &Bool<'z3>) -> Int<'z3>

Encode a boolean condition as the integer 1/0.

fn negate(&self, val: &Int<'z3>) -> Int<'z3>

Negate a Z3 integer (0 - val).

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

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

pub(crate) fn slice_len_of_alloc(&self, alloc_id: AllocId) -> Option<Int<'z3>>

The slice/array element count for an allocation: the materialized slice_len, or size / elem_size as a fallback for allocations created before materialization (e.g. some call effects). Uses the symbolic element size (size_sym_read) so len = (len·S) / S cancels to len for a generic element type — mirroring set_len_from_alloc. Returns None when the element type is unknown.

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

The slice length of a &[T] / &mut [T] value, resolved through its provenance allocation (see Self::slice_len_of_alloc).

pub(crate) fn try_adt_len_field( &self, val: &VmValue<'z3, 'tcx>, ) -> Option<Int<'z3>>

Resolve x.len() for a pointer whose pointee ADT carries a len field (e.g. NodeRef<LeafNode>: len() reads (*ptr).len). Returns the pointee’s len field term, or None when the pointee has no such field.

fn try_adt_len_field_at( &self, alloc_id: AllocId, ty: Ty<'tcx>, root_ty: Ty<'tcx>, prefix: &[usize], ) -> Option<Int<'z3>>

Resolve a len field on ty, recursing into ADT sub-fields when there is no direct len (e.g. String { vec: Vec { ptr, len, cap } } resolves String.len() to vec.len). root_ty stays fixed as the allocation’s element type, which is how decompose_pointee_fields keys MemoryContent::values.

pub(crate) fn try_index_range_len( &self, val: &VmValue<'z3, 'tcx>, ) -> Option<Int<'z3>>

Resolve len() for core::ops::IndexRange (a private { start, end } struct): len() = end - start. The len field lookup above misses it because IndexRange has no len field — its len() computes the difference of its two private fields.

pub(crate) fn len_from_value( &self, val: &VmValue<'z3, 'tcx>, ) -> Option<Int<'z3>>

Resolve len() of a slice/ADT value: the pointee ADT’s len field, then the materialized slice length, then size / elem_size. Shared by the exec- and checker-side Len evaluators so the fallback chain is defined once.

pub(crate) fn try_struct_nn_len_field( &self, local: Local, field_path: &[usize], ty: Ty<'tcx>, ) -> Option<Int<'z3>>

Resolve x.len() for a struct x (e.g. NodeRef) whose len() method reads (*x.field).len through a NonNull/raw-pointer field. Follows that field to its pointee allocation and reads the pointee’s len field.

pub(crate) fn field_type_at( &self, local: Local, field_path: &[usize], ) -> Option<Ty<'tcx>>

Resolve the type of a place (local + field path) by walking the ADT field definitions.

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

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

fn facts_for_binary_op( &self, op: BinOp, lhs: &VmValue<'z3, 'tcx>, rhs: &VmValue<'z3, 'tcx>, provenance: &Option<Provenance<'z3>>, ) -> ValueFacts<'z3>

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

fn rhs_is_aligned_multiple( &self, val: &VmValue<'z3, 'tcx>, align: &Int<'z3>, ) -> 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, terminator: &Terminator<'tcx>, switch_succ: Option<BasicBlock>, )

fn exec_switchint( &mut self, discr: &Operand<'tcx>, targets: &SwitchTargets, switch_succ: Option<BasicBlock>, )

Execute a SwitchInt terminator.

Uses the successor resolved by the slicer (switch_succ) 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)

Execute an Assert terminator.

fn op_source_of( &self, pk: &PlaceKey, ) -> Option<(Option<PlaceKey>, Option<PlaceKey>, BinOp)>

The (lhs, rhs, op) of the binary-op/comparison source recorded on the value bound to pk’s local, if any.

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

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

fn mark_align_n(&mut self, src_pk: &Option<PlaceKey>, align: Int<'z3>)

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 assert_contract_fact(&mut self, property: &Property<'tcx>)

Assert a contract fact as VM state invariants.

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

Apply a single atom’s direct effect (its match kind arm), without recursing into its subsumption consequences.

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

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

fn mark_alloc_live_keep( &mut self, val: &VmValue<'z3, 'tcx>, elem_ty: Ty<'tcx>, ) -> bool

Materialize a fresh external allocation for an Allocated contract fact, returning a value carrying the allocation’s provenance. Mark the target pointer’s existing allocation as live (and record its element type for downstream Typed checks). Returns true when the pointer already carried an allocation, so a fresh external allocation should not be materialized (which would loosen bound checks).

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

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 ForEach/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/ForEach terminate the path (they unwrap the value in place).

fn contract_target_value( &mut self, property: &Property<'tcx>, ) -> Option<VmValue<'z3, '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<'z3, '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<'z3>>

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

fn relop_to_bool(&self, op: RelOp, lhs: &Int<'z3>, rhs: &Int<'z3>) -> Bool<'z3>

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

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

fn eval_numeric_binary( &self, l: &Int<'z3>, r: &Int<'z3>, op: NumericBinOp, ) -> Option<Int<'z3>>

Evaluate a numeric binary operation over two symbolic terms.

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

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

fn is_iter_ref(&self, val: &VmValue<'z3, 'tcx>) -> bool

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 iter_ptr_comparison( &self, op: BinOp, lhs: &VmValue<'z3, 'tcx>, rhs: &VmValue<'z3, 'tcx>, ) -> Option<Bool<'z3>>

When lhs op rhs compares an iterator’s ptr and end_or_len pointers (the inlined form of is_empty: ptr == end), express the comparison element-wise as iter_ptr_offset == base_len. The operands may be plain temporaries (from the as_ptr/cast/field-read lowering), so the iterator is located via the shared buffer allocation (the end field’s provenance alloc id). Returns None when this is not an iterator emptiness comparison.

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

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

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 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 set_non_null_for_value( &mut self, property: &Property<'tcx>, val: VmValue<'z3, 'tcx>, )

Set non_null invariant on the target value.

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

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

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

Record the numeric index < len bound for a single-index InBound(slice, index), so a derived index (e.g. index - 1 guarded by index >= 1) can be discharged by SMT rather than only via the coarse in_bounds flag. Range indices (start..end) are left to the checker’s extract_range_end (end <= len).

fn assert_pointee_struct_invariants( &mut self, dest_ty: Ty<'tcx>, dest_local: Local, )

When a &T/&mut T reference is created (e.g. via &*NonNull<T>), assume T’s #[rapx::invariant]s on the new reference local, rebinding the invariant’s self place to that reference. This is what lets a struct’s invariants flow through pointer dereferences into the caller’s state.

fn assert_alloc_pointee_invariants( &mut self, alloc_id: AllocId, pointee_ty: Ty<'tcx>, )

Assert a pointee ADT’s #[rapx::invariant] struct invariants directly against its materialized per-allocation field values. This is the pointer-field analogue of [assert_pointee_struct_invariants](Self:: assert_pointee_struct_invariants): that helper covers &T references, while this one covers NonNull<T> / Box<T> pointer fields whose pointee is decomposed by init_ptr_field (e.g. NodeRef.node: NonNull<LeafNode> must satisfy LeafNode’s len <= CAPACITY).

fn eval_pointee_predicate_as_bool( &self, alloc_id: AllocId, view_ty: Ty<'tcx>, pred: &NumericPredicate<'tcx>, ) -> Option<Bool<'z3>>

Evaluate a ValidNum predicate against a pointee allocation (not a MIR local): field places resolve through MemoryContent::values keyed by the pointee type.

fn eval_pointee_expr( &self, alloc_id: AllocId, view_ty: Ty<'tcx>, expr: &ContractExpr<'tcx>, ) -> Option<Int<'z3>>

Evaluate a numeric ContractExpr against a pointee allocation.

fn eval_pointee_expr_value( &self, alloc_id: AllocId, view_ty: Ty<'tcx>, expr: &ContractExpr<'tcx>, ) -> Option<VmValue<'z3, 'tcx>>

Resolve a Place (or Len inner) against a pointee allocation, returning the materialized VmValue so slice-length fallbacks can read provenance.

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

Set align invariant on the target value.

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

Set init invariant on the target value and its allocation.

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

Set owning invariant on the target value.

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

Record the Align(container.iter(), T) for_each fact: every element pointer is aligned to align_of(T). Anchored to the container allocation so a pointer loaded from it can discharge Align(cur, T).

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

Record the Allocated(container.iter(), T, n) for_each fact: every element pointer backs >= n T elements (n may be symbolic).

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

Record the Owning(container.iter()) for_each fact: every element pointer is the sole owner of its pointee. Anchored to the container allocation so a pointer loaded from it can discharge Owning(cur).

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

Extract the pointee type if ty is a #[repr(transparent)] single-field raw-pointer wrapper (NonNull<P>) or wrapped in Option<NonNull<P>>. Returns Some(P).

Detected structurally (via #[repr(transparent)] + a raw-pointer field) rather than by name, so re-implemented std types in the challenge suites are modelled identically to their std counterparts.

fn transparent_ptr_pointee( &self, adt_def: &AdtDef<'_>, substs: GenericArgsRef<'tcx>, ) -> Option<Ty<'tcx>>

Pointee type of a #[repr(transparent)] single-field raw-pointer wrapper such as NonNull<T> (struct NonNull<T> { pointer: *const T }).

pub(crate) fn container_ptr_field( &self, ty: Ty<'tcx>, ) -> Option<(Vec<usize>, Ty<'tcx>)>

fn container_ptr_field_inner( &self, ty: Ty<'tcx>, prefix: Vec<usize>, depth: usize, ) -> Option<(Vec<usize>, Ty<'tcx>)>

pub(crate) fn container_data_alloc( &self, header: AllocId, ty: Ty<'tcx>, ) -> Option<AllocId>

pub(crate) fn data_alloc_of( &self, header: AllocId, ty: Ty<'tcx>, ) -> Option<AllocId>

The data allocation behind a container header or a slice view’s header. Tries the type-driven owning field first, then falls back to scanning the header’s materialized fields for the first owning pointer (covers slice views whose header AllocId no longer carries a type key).

fn header_data_alloc(&self, header: AllocId) -> Option<AllocId>

Scan a header allocation’s materialized fields for the owning pointer (its provenance names the data allocation). This is the header → data fallback for slice views (whose provenance names the container header, not the data), replacing the old slice_data edge.

Returns the provenance only when the header has exactly one owning pointer field. A multi-owning-pointer header (e.g. a linked list’s head/tail) is ambiguous, so fall back to None rather than guess.

pub(crate) fn set_container_data_field( &mut self, header: AllocId, ty: Ty<'tcx>, data_alloc: AllocId, base: Int<'z3>, elem_ty: Ty<'tcx>, ) -> bool

pub(crate) fn try_materialize_const_bytes( &mut self, val: &mut VmValue<'z3, '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<'z3, 'tcx>, )

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

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

impl<'z3, 'tcx> VmState<'z3, 'tcx>

pub(crate) fn address_of_place( &mut self, place: &Place<'tcx>, ) -> Option<VmValue<'z3, '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(crate) fn size_of_ty(&self, ty: Ty<'tcx>) -> u64

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

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

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

pub(crate) 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).

pub(crate) fn size_sym(&mut self, ty: Ty<'tcx>) -> Int<'z3>

Element size of ty as a symbolic Z3 term. For concrete types this is the constant byte size; for a generic type whose size_of is unknown (an unconstrained T) it is a single reusable symbolic constant with >= 0 (so T may be a ZST). Using the same constant everywhere (ptr strides, access counts, allocation sizes) lets SMT cancel the factor in InBound.

fn const_len_term(&self, const_len: &Const<'tcx>) -> Int<'z3>

The array length N as a Z3 term (concrete value or symbolic const generic). The symbolic name mirrors value_of_operand’s formatting so it is identical to the const N term appearing in path conditions.

pub(crate) fn size_sym_read(&self, ty: Ty<'tcx>) -> Int<'z3>

Read-only sibling of size_sym: returns the symbolic size for ty, falling back to 1 when the symbolic constant has not been created yet (e.g. a checker invoked before the exec phase created it). Non-ZST concrete types return their constant byte size; a concrete ZST or a not-yet-created generic constant falls back to 1 — a non-zero element size keeps size / elem_size derivations from dividing by zero.

pub(crate) fn generic_elem_size(&self, alloc_id: AllocId) -> Option<Int<'z3>>

The symbolic element-size term of alloc_id’s element type, when it is a generic type parameter (so it may be 0 for a ZST or ≥ 1 for a non-ZST). Returns None for concrete element types, where the size is a known constant and no case split is needed.

pub(crate) fn align_sym(&mut self, ty: Ty<'tcx>) -> Int<'z3>

Alignment of ty as a symbolic Z3 term. For a concrete type this is the constant byte alignment; for a generic type it is a reusable symbolic constant align_T with >= 1, lower-bounded by the trait bounds’ minimum alignment, and linked to the element size by the layout constraint sizeof_T % align_T == 0 (a type’s size is always a multiple of its alignment). For a generic struct, its alignment is additionally constrained to be a multiple of each field’s alignment, so a field pointer ((*node).value) inherits the container’s alignment.

pub(crate) fn align_sym_read(&self, ty: Ty<'tcx>) -> Int<'z3>

Read-only sibling of align_sym: returns the symbolic alignment for ty, falling back to the trait bounds’ minimum alignment when the constant has not been created yet (e.g. a generic U that only appears in a cast/contract, never as an allocation element type). Concrete types return their constant alignment.

pub(crate) fn struct_size_sym(&mut self, ty: Ty<'tcx>) -> Option<Int<'z3>>

Size of a struct/ADT as the sum of its fields’ sizes (each via size_sym). This lower-bounds the real layout so a field reference (Allocated(&alloc)) can be discharged against the struct allocation (sizeof_A <= 8 + 8 + sizeof_A). Returns None for non-ADT or enum types.

fn uninit_byte(&self) -> Int<'z3>

The shared UNINIT sentinel (≥ 256, outside the u8 range).

fn fresh_byte_array(&self) -> Array<'z3>

A fresh Array<Int, Int> whose every offset reads UNINIT.

pub(crate) fn byte_read(&self, alloc_id: AllocId, i: &Int<'z3>) -> Int<'z3>

Read byte[i] at a (possibly symbolic) offset; unwritten offsets read UNINIT.

The result is simplified so a select(store(…), i) chain (built up by repeated byte_write / copy_byte_tracking) collapses to its constant byte value when i is concrete, rather than leaking the nested select/store expression into downstream SMT obligations.

pub(crate) fn byte_write( &mut self, alloc_id: AllocId, i: &Int<'z3>, v: &Int<'z3>, )

Write byte[i] = v.

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

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

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

Mark a byte as initialized (written) with an unknown value.

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

Whether a byte at a concrete offset was written (select != UNINIT).

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

Whether a byte at a concrete offset is known NUL.

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

Whether a byte at a concrete offset is known non-NUL.

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

Enumerate (offset, term) pairs for the written bytes of an allocation, in ascending offset order.

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

Offsets known to be NUL.

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

Offsets known to be non-NUL.

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

Copy the per-byte state (values + written-offset bound) of one allocation to another, shifting by src_offset so dst[i] = src[i + src_offset].

pub(crate) fn load_value( &self, alloc_id: AllocId, view_ty: Ty<'tcx>, path: &[usize], ) -> Option<&VmValue<'z3, 'tcx>>

The value at a field offset within an allocation viewed as view_ty.

This is the memory-contents (typed-value) layer (MemoryContent::values): the single source of truth for field values. Self::field_value is the local-facing wrapper that resolves a MIR local’s backing allocation and declared type, then reads this same layer. The viewed type is part of the key so reinterpret casts (LeafNode ↔ InternalNode) resolve to the right field view.

pub(crate) fn store_value( &mut self, alloc_id: AllocId, view_ty: Ty<'tcx>, path: Vec<usize>, value: VmValue<'z3, 'tcx>, )

Store a value at a field offset within an allocation viewed as view_ty.

This is the write counterpart to Self::load_value on the same memory-contents layer (MemoryContent::values); the viewed type is part of the key so reinterpret casts resolve to the right field view.

pub(crate) fn utf8_validity(&self, alloc_id: AllocId) -> Option<Bool<'z3>>

Encode the UTF-8 validity DFA over this allocation’s tracked bytes. Returns None when no bytes are tracked (validity is trivially satisfied), so callers can short-circuit to “proved”.

impl<'z3, 'tcx> VmState<'z3, 'tcx>

pub(crate) fn new( z3_ctx: &'z3 Context, tcx: TyCtxt<'tcx>, path: &Path, caller_def_id: DefId, ) -> Self

Create a fresh VM state for executing a path.

pub(crate) fn body(&self) -> &'tcx Body<'tcx>

The MIR body of the current function, derived from current_def_id.

pub(crate) fn save_frame(&mut self) -> FrameState

Capture the frame-scoped state before switching to an inlined callee.

This is the single source of truth for what is frame-scoped: the whole FrameState (function identity, local bindings, and operand sources). Both inline mechanisms (handle_callee_entry in path replay and exec_inline_call) call this, so they can no longer drift apart.

pub(crate) fn restore_frame(&mut self, frame: FrameState)

Restore the frame-scoped state after an inlined callee returns.

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

Look up the whole value bound to a MIR local (its path == [] slot in the allocation backing the local).

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

Bind a whole value to a MIR local (store it at path == [] in the allocation backing the local, allocating that stack slot on demand).

pub(crate) fn mark_initialized(&mut self, value: &mut VmValue<'z3, 'tcx>)

Mark a value as initialized (written), and sync its backing allocation’s ContentFacts::initialized fact.

This is the single entry point that keeps the value-level ValueFacts::init and the allocation-level ContentFacts::initialized in sync; callers must set the pair through here rather than by hand so the two facts cannot drift apart.

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

Get the symbolic address of a MIR local (its stack allocation’s base).

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

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

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

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

pub(crate) fn allocate_slice( &mut self, len: Int<'z3>, elem_size: Int<'z3>, align: Int<'z3>, element_ty: Option<Ty<'tcx>>, ) -> (AllocId, Int<'z3>)

Allocate a slice/array data allocation with a known (possibly symbolic) element count. Computes size = len * elem_size and materializes len in one step, so size and the slice length can never diverge (the size == len * elem_size invariant is established here instead of being re-derived by every caller).

fn allocate_internal( &mut self, size: Int<'z3>, align: Int<'z3>, element_ty: Option<Ty<'tcx>>, kind: AllocKind<'z3>, ) -> (AllocId, Int<'z3>)

pub(crate) fn alloc(&self, id: AllocId) -> &Allocation<'z3, '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<'z3, 'tcx>

Mutable indexed access to an allocation by its AllocId.

pub(crate) fn content(&self, id: AllocId) -> &MemoryContent<'z3, 'tcx>

Indexed access to an allocation’s contents by its AllocId.

pub(crate) fn content_mut( &mut self, id: AllocId, ) -> &mut MemoryContent<'z3, 'tcx>

Mutable indexed access to an allocation’s contents by its AllocId.

pub(crate) fn is_cstr_trusted(&self, id: AllocId) -> bool

Whether id was asserted a valid C string via a ValidCStr contract fact / struct invariant.

pub(crate) fn is_utf8_trusted(&self, id: AllocId) -> bool

Whether id was asserted valid UTF-8 via a ValidString contract fact.

pub(crate) fn root_alloc(&self, id: AllocId) -> AllocId

The ultimate root allocation, following parent chains (sub-allocations created by from_raw_parts / split_at / as_chunks, whose parent points at the allocation they were split from).

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

Create a fresh symbolic Z3 int constant (globally unique, even across calls with the same prefix — Z3_mk_fresh_const auto-suffixes the name).

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

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

Field values live in the allocation backing the local (the memory-contents layer MemoryContent::values), keyed by the local’s declared type as the view type. Returns None if the local has no allocation (the field was never materialized).

pub(crate) fn field_paths(&self, local: Local) -> Vec<Vec<usize>>

Enumerate the field paths materialized for a local: every non-empty path for which Self::field_value currently returns a value (the local’s allocation’s fields under its declared view type). The whole value (path == []) is deliberately excluded — it is read via Self::local_value, not as a “field”, so callers iterating fields do not accidentally treat the whole value as a field projection.

fn frame_local_ty(&self, frame: &FrameState, local: Local) -> Ty<'tcx>

The declared type of local in frame’s body.

pub(crate) fn frame_field_paths( &self, frame: &FrameState, local: Local, ) -> Vec<Vec<usize>>

Enumerate the field paths materialized for local in a saved caller frame. Field values live in the path-scoped MemoryContent::values, so they are read via frame’s local_alloc and declared type.

pub(crate) fn frame_field_value( &self, frame: &FrameState, local: Local, path: &[usize], ) -> Option<&VmValue<'z3, 'tcx>>

Read a field of local in a saved caller frame.

pub(crate) fn frame_local_value( &self, frame: &FrameState, local: Local, ) -> Option<&VmValue<'z3, 'tcx>>

Read the whole value of local in a saved caller frame (its path == [] slot). The value lives in the path-scoped MemoryContent::values, while the name → allocation binding lives in the saved frame.

pub(crate) fn all_local_values(&self) -> Vec<(Local, &VmValue<'z3, 'tcx>)>

Enumerate (local, whole value) for every local with a materialized whole value (its path == [] slot). This is the whole-value counterpart to Self::field_paths, used where code used to iterate locals.

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

The buffer an Iter/IterMut at local walks: the provenance of its end field. This is frame-independent (the buffer allocation is path-scoped), unlike the local itself, so it keys the per-iterator element index in TermCaches::iter_ptr_offset.

pub(crate) fn iter_utf8_buffer( &self, local: Local, ) -> Option<(AllocId, Int<'z3>)>

The byte buffer walked by an iterator at local, possibly wrapped in adapter types (Cloned/Rev/…). Rvalue::Aggregate flattens nested adapters, so the innermost Iter/IterMut end pointer is any tracked field whose path ends in [1]. Return its allocation and end offset (the end offset doubles as the byte length when the element is u8).

pub(crate) fn owner_ptr_field( &self, local: Local, ) -> Option<&VmValue<'z3, 'tcx>>

The field carrying an owned value’s heap pointer (Box/Vec/String’s owning pointer field), located generically via Self::container_ptr_field (e.g. Box → [0, 0], Vec → [0, 0, 0]). Falls back to the first materialized field with heap provenance for owners whose deep NonNull leaf was not explicitly materialized (e.g. a Box produced by into_boxed_slice, which only records the whole value).

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

Invalidate local’s owner-field provenance (mark it moved-out after a whole-place move), so a later Owning check does not treat it as a second owner of the heap allocation it no longer owns.

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

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

Ensures the local has a backing allocation, then stores into the memory-contents layer (MemoryContent::values) keyed by the local’s declared type as the view type.

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

Assert path conditions and invariant constraints into a solver.

fn assert_value_constraints( &self, solver: &Solver<'z3>, value: &VmValue<'z3, 'tcx>, )

Assert a single symbolic value’s known invariant constraints.

impl<'z3, 'tcx> VmState<'z3, 'tcx>

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

Extract a VmValue from a MIR operand.

fn byte_from_field( &self, alloc_id: AllocId, ty: Ty<'tcx>, offset: usize, ) -> Option<Int<'z3>>

Read the byte at offset within a repr(C)-style ADT from its materialized scalar field values — the field→byte direction of the cast cross-view materialization. Returns None when offset does not land inside a concrete scalar field (so the caller falls back to the base).

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

Look up the value stored at a MIR place.

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

Create an unknown value for a place.

The value carries no non_null (or any other) assumption: a raw pointer whose provenance was lost may still be null, so assuming non-null here would let NonNull/null-guard checks pass unsoundly.

Trait Implementations

impl Debug for VmState<'_, '_>

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

Formats the value using the given formatter.