rapx 0.7.39

//! Symbolic VM state types.
//!
//! Core data structures that represent the symbolic execution state:
//! `VmValue` (symbolic value with invariants), `Allocation` (memory object),
//! and `VmState` (the full execution state at a program point).

use rustc_hir::def_id::DefId;
use rustc_middle::{
    mir::{BasicBlock, Body, Local, Operand, Place, ProjectionElem},
    ty::{Ty, TyCtxt},
};
use z3::{
    Context,
    ast::{Ast, Bool, Int},
};

use crate::compat::{FxHashMap, FxHashSet};
use crate::verify::{def_use::PlaceKey, path_extractor::Path};

/// Unique identifier for a heap or stack allocation.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub(crate) struct AllocId(pub usize);

/// Pointer provenance: which allocation and at what byte offset.
#[derive(Clone, Debug)]
pub(crate) struct Provenance<'ctx> {
    /// The allocation this pointer derives from.
    pub alloc_id: AllocId,
    /// Byte offset from the allocation base. A freshly created
    /// pointer to the base of an allocation has `offset = 0`.
    pub offset: Int<'ctx>,
    /// Whether `offset` is a compile-time field offset (`offset_of!`).  Such an
    /// offset always satisfies `0 <= offset` and `offset + size_of(field) <=
    /// size_of(container)`, which the verifier uses to discharge in-bounds
    /// checks for patterns like `Option::as_slice`.
    pub is_field_offset: bool,
}

/// Known invariants about a symbolic value.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub(crate) struct ValueInvariants<'ctx> {
    pub non_null: bool,
    pub aligned: bool,
    pub init: bool,
    pub in_bounds: bool,
    /// If Some(n), the value's term is known to satisfy `term % n == 0`.
    /// Set by alignment guards, Mul by power-of-two, and type alignment.
    /// `n` is a Z3 term so that a generic type's alignment (a symbolic
    /// `align_T`) can be carried the same way as a concrete alignment.
    pub align_n: Option<Int<'ctx>>,
    /// Whether this scalar value is a compile-time field offset (`offset_of!`).
    /// Propagated to a pointer's provenance when used as an `add`/`byte_add`
    /// offset.
    pub is_field_offset: bool,
}

/// A symbolic value tracked by the VM.
///
/// # Semantics of `term`
///
/// - For pointer/reference types (`&T`, `*const T`, `*mut T`, `Box<T>`, etc.):
///   `term` represents the **address** in the VM's logical address space.
/// - For scalar types (integers, `bool`, `char`): `term` represents the **value**.
/// - For aggregate types (struct, tuple, enum): `term` is the base address of
///   the stack allocation backing the aggregate.
///
/// When `provenance` is `Some`, the following relationship holds and is
/// asserted into the solver at check time:
///   `term == alloc[provenance.alloc_id].base + provenance.offset`
#[derive(Clone, Debug)]
pub(crate) struct VmValue<'ctx, 'tcx> {
    /// The Z3 integer term (address or scalar value, see struct docs).
    pub term: Int<'ctx>,
    /// Rust type, for layout queries.
    pub ty: Ty<'tcx>,
    /// Which allocation this pointer derives from and at what offset.
    pub provenance: Option<Provenance<'ctx>>,
    /// Known constraints on this value.
    pub invariants: ValueInvariants<'ctx>,
}

impl<'ctx, 'tcx> VmValue<'ctx, 'tcx> {
    pub(crate) fn new(term: Int<'ctx>, ty: Ty<'tcx>) -> Self {
        VmValue {
            term,
            ty,
            provenance: None,
            invariants: ValueInvariants::default(),
        }
    }

    /// Convenience: extract the `AllocId` from provenance, if any.
    pub(crate) fn provenance_alloc_id(&self) -> Option<AllocId> {
        self.provenance.as_ref().map(|p| p.alloc_id)
    }
}

/// A memory allocation (stack or heap).
///
/// The allocation is stored in `VmState::allocations` at index `AllocId.0`
/// (an `AllocId` is a monotonic counter that doubles as the vector index).
#[derive(Clone, Debug)]
pub(crate) struct Allocation<'ctx, 'tcx> {
    /// Base address (fresh Z3 constant).
    pub base: Int<'ctx>,

    /// Size in bytes (Z3 term, may be symbolic).
    pub size: Int<'ctx>,

    /// Alignment in bytes (Z3 term, may be symbolic for a generic element
    /// type).
    pub align: Int<'ctx>,

    /// Element type for bounds checking.
    pub element_ty: Option<Ty<'tcx>>,

    /// Element count (the slice/array length), materialized like the fat
    /// pointer's metadata word.  `size` is derived from it as
    /// `slice_len * size_of(element_ty)`.  `None` for allocations that are not
    /// slice/array data (e.g. a single object or a Vec's external buffer).
    pub slice_len: Option<Int<'ctx>>,

    /// True if this allocation models an external raw-pointer parameter
    /// whose exact size and nullability are unknown.
    pub is_external: bool,

    /// Allocations that have been freed (StorageDead, Drop).
    pub dead: bool,

    /// Allocations that have been written to (initialized via write/MaybeUninit).
    pub initialized: bool,

    /// Allocations assumed alive via contract (e.g. `#[rapx::requires(Alive(ptr))]`).
    pub alive_assumed: bool,

    /// Allocations known to be a null-terminated byte buffer (a valid C
    /// string), asserted via a `ValidCStr` contract fact or struct invariant.
    pub nul_terminated: bool,

    /// Parent allocation for sub-allocations created by split_at / from_raw_parts.
    pub parent: Option<AllocId>,

    /// Slice data allocation: for a `&[T]` reference's stack allocation, the
    /// symbolic data allocation created for the slice contents.
    pub slice_data: Option<AllocId>,
}

impl<'ctx, 'tcx> Allocation<'ctx, 'tcx> {
    /// Construct a fresh allocation with all live/dead/invariant flags in
    /// their initial state.
    pub(crate) fn new(
        base: Int<'ctx>,
        size: Int<'ctx>,
        align: Int<'ctx>,
        element_ty: Option<Ty<'tcx>>,
        is_external: bool,
    ) -> Self {
        Allocation {
            base,
            size,
            align,
            element_ty,
            slice_len: None,
            is_external,
            dead: false,
            initialized: false,
            alive_assumed: false,
            nul_terminated: false,
            parent: None,
            slice_data: None,
        }
    }
}

/// One-shot execution/contract flags accumulated while stepping a path.
#[derive(Clone, Copy, Debug, Default)]
pub(crate) struct ContractFlags {
    /// Whether a SplitTransmute contract was asserted by the caller.
    pub split_transmute_asserted: bool,
    /// Whether an `Alias` hazard was accepted via the caller's contract.
    pub alias_hazard_accepted: bool,
    /// Whether a ChecksIndexBoundsDisjoint call was processed in any
    /// checkpoint of this function (accumulated across checkpoints).
    pub has_checked_bounds: bool,
    /// Set once the path evaluated an `Iterator::next` discriminant whose
    /// variant was known symbolically.
    pub saw_next_discriminant: bool,
}

/// Per-byte symbolic state at a concrete offset in an allocation.
#[derive(Clone, Debug, Default)]
pub(crate) struct ByteInfo<'ctx> {
    /// Symbolic value, if tracked.
    pub value: Option<Int<'ctx>>,
    /// Whether the byte has been explicitly written.
    pub init: bool,
    /// NUL knowledge: `Some(true)` known NUL, `Some(false)` known non-NUL.
    pub nul: Option<bool>,
}

/// A saved caller context pushed when entering an inlined callee during path
/// execution.
pub(crate) struct InlineFrame<'ctx, 'tcx> {
    pub body: &'ctx Body<'tcx>,
    pub def_id: DefId,
    pub saved_locals: FxHashMap<Local, VmValue<'ctx, 'tcx>>,
    pub saved_field_values: FxHashMap<(Local, Vec<usize>), VmValue<'ctx, 'tcx>>,
}

/// 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.
pub(crate) struct VmState<'ctx, 'tcx> {
    /// Shared Z3 context.
    pub(crate) ctx: &'ctx Context,

    /// Compiler type context.
    pub(crate) tcx: TyCtxt<'tcx>,

    /// The DefId of the function whose body we are executing.
    pub(crate) caller_def_id: DefId,

    /// The MIR body being executed.
    pub(crate) body: &'ctx Body<'tcx>,

    /// Current value bound to each MIR local.
    pub(crate) locals: FxHashMap<Local, VmValue<'ctx, 'tcx>>,

    /// Known address for each stack-allocated local.
    pub(crate) local_addresses: FxHashMap<Local, Int<'ctx>>,

    /// Allocation ID for each stack-allocated local.
    pub(crate) local_alloc_ids: FxHashMap<Local, AllocId>,

    /// All known allocations.
    pub(crate) allocations: Vec<Allocation<'ctx, 'tcx>>,

    /// Accumulated path conditions (SwitchInt branches, Assert).
    pub(crate) path_conditions: Vec<Bool<'ctx>>,

    /// The next allocation ID.
    pub(crate) next_alloc_id: usize,

    /// Track block occurrence counts for loop-carried value indexing.
    pub(crate) block_occurrences: FxHashMap<BasicBlock, usize>,

    /// Binary op sources for guard inference: destination → (lhs, rhs) place keys.
    pub(crate) binary_op_sources: FxHashMap<PlaceKey, (Option<PlaceKey>, Option<PlaceKey>)>,

    /// Direct boolean condition for a comparison result place (Le/Lt/Ge/Gt/Eq/Ne),
    /// used to record precise switch-guard path conditions.
    pub(crate) comparison_conds: FxHashMap<PlaceKey, Bool<'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.
    pub(crate) discriminant_terms: FxHashMap<Local, Int<'ctx>>,

    /// 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.
    pub(crate) other_op_sources: FxHashMap<PlaceKey, (Option<PlaceKey>, Option<PlaceKey>)>,

    /// One-shot execution/contract flags accumulated while stepping a path.
    pub(crate) contract_flags: ContractFlags,

    /// 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`.
    pub(crate) field_values: FxHashMap<(Local, Vec<usize>), VmValue<'ctx, 'tcx>>,

    /// Per-allocation field tracking: (alloc_id, field_indices) → value.  This
    /// mirrors `field_values` but is keyed by allocation instead of local, so a
    /// `&*NonNull<ADT>` dereference can resolve the pointee's fields (e.g.
    /// `(*leaf).len`) regardless of which local holds the pointer.
    pub(crate) alloc_field_values: FxHashMap<(AllocId, Vec<usize>), VmValue<'ctx, 'tcx>>,

    /// 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.
    pub(crate) iter_ptr_offset: FxHashMap<Local, Int<'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.
    pub(crate) bytes: FxHashMap<(AllocId, usize), ByteInfo<'ctx>>,

    /// Notes from unsupported operations.
    pub(crate) notes: Vec<String>,

    /// The path being executed (for branch target resolution).
    pub(crate) path: Option<Path>,

    /// Name of the most recent call (for context-aware effects like Vec push).
    pub(crate) last_call_name: String,

    /// `DefId` of the most recent call (for `DefId`-based API classification).
    pub(crate) last_call_callee: Option<DefId>,

    /// 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.
    pub(crate) inline_depth: usize,

    /// Stack of saved caller contexts for inlined-callee path execution.
    pub(crate) inline_frames: Vec<InlineFrame<'ctx, 'tcx>>,

    /// 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.
    pub(crate) not_mask_terms: FxHashSet<Int<'ctx>>,

    /// During `exec_inline_call`, maps each callee argument index to the
    /// *caller* local its value points at (resolved from the reference's
    /// address term before the caller's address map is saved away). Used by
    /// `exec_assign` to resolve `(*self).field = val` writes through a `&mut
    /// self` reborrow temp back to the caller's referent.
    pub(crate) inline_arg_referents: Vec<Option<Local>>,

    /// Field writes collected during `exec_inline_call` that must be applied to
    /// the caller's `field_values` *after* the inline frame is popped (the
    /// caller's field map is not live while the callee executes). Each entry is
    /// `(caller_referent_local, field_path, value)`.
    pub(crate) deferred_field_writes: Vec<(Local, Vec<usize>, VmValue<'ctx, 'tcx>)>,

    /// Symbolic element size for generic types whose concrete `size_of` is
    /// unknown at verification time (e.g. an unconstrained `T`).  A single
    /// symbolic constant per type keeps `ptr.add` strides, `access_bytes`
    /// element sizes, and allocation sizes consistent so that SMT can cancel the
    /// factor in `InBound` (e.g. `(mid+n)·S <= len·S  ⟺  mid+n <= len`).
    pub(crate) sym_sizes: FxHashMap<Ty<'tcx>, Int<'ctx>>,

    /// Symbolic element alignment for generic types whose concrete `align_of`
    /// is unknown at verification time (an unconstrained `T`).  One constant
    /// per type, linked to `sym_sizes` by the layout constraint
    /// `sizeof_T % align_T == 0`.
    pub(crate) sym_aligns: FxHashMap<Ty<'tcx>, Int<'ctx>>,
}

impl<'ctx, 'tcx> VmState<'ctx, 'tcx> {
    /// Create a fresh VM state for executing a path.
    pub(crate) fn new(
        ctx: &'ctx Context,
        tcx: TyCtxt<'tcx>,
        body: &'ctx Body<'tcx>,
        caller_def_id: DefId,
    ) -> Self {
        Self {
            ctx,
            tcx,
            body,
            caller_def_id,
            locals: FxHashMap::default(),
            local_addresses: FxHashMap::default(),
            local_alloc_ids: FxHashMap::default(),
            allocations: Vec::new(),
            path_conditions: Vec::new(),
            next_alloc_id: 0,
            block_occurrences: FxHashMap::default(),
            binary_op_sources: FxHashMap::default(),
            comparison_conds: FxHashMap::default(),
            discriminant_terms: FxHashMap::default(),
            other_op_sources: FxHashMap::default(),
            contract_flags: ContractFlags::default(),
            field_values: FxHashMap::default(),
            alloc_field_values: FxHashMap::default(),
            iter_ptr_offset: FxHashMap::default(),
            bytes: FxHashMap::default(),
            notes: Vec::new(),
            path: None,
            last_call_name: String::new(),
            last_call_callee: None,
            inline_depth: 0,
            inline_frames: Vec::new(),
            not_mask_terms: FxHashSet::default(),
            inline_arg_referents: Vec::new(),
            deferred_field_writes: Vec::new(),
            sym_sizes: FxHashMap::default(),
            sym_aligns: FxHashMap::default(),
        }
    }

    /// Look up the value bound to a MIR local.
    pub(crate) fn local_value(&self, local: Local) -> Option<&VmValue<'ctx, 'tcx>> {
        self.locals.get(&local)
    }

    /// Bind a value to a MIR local.
    pub(crate) fn set_local(&mut self, local: Local, value: VmValue<'ctx, 'tcx>) {
        self.locals.insert(local, value);
    }

    /// Get or create the symbolic address of a MIR local.
    pub(crate) fn local_address(&mut self, local: Local) -> Int<'ctx> {
        if let Some(addr) = self.local_addresses.get(&local) {
            return addr.clone();
        }
        let name = format!("addr__{}", local.as_usize());
        let addr = Int::new_const(self.ctx, name.as_str());
        self.local_addresses.insert(local, addr.clone());
        addr
    }

    /// Allocate a fresh symbolic object and return its ID and base address.
    pub(crate) fn allocate(
        &mut self,
        size: Int<'ctx>,
        align: Int<'ctx>,
        element_ty: Option<Ty<'tcx>>,
    ) -> (AllocId, Int<'ctx>) {
        self.allocate_internal(size, align, element_ty, false)
    }

    /// Allocate a fresh external allocation (for raw-pointer parameters).
    /// External allocations may be null and have unlimited size.
    pub(crate) fn allocate_external(
        &mut self,
        size: Int<'ctx>,
        align: Int<'ctx>,
        element_ty: Option<Ty<'tcx>>,
    ) -> (AllocId, Int<'ctx>) {
        self.allocate_internal(size, align, element_ty, true)
    }

    fn allocate_internal(
        &mut self,
        size: Int<'ctx>,
        align: Int<'ctx>,
        element_ty: Option<Ty<'tcx>>,
        is_external: bool,
    ) -> (AllocId, Int<'ctx>) {
        let id = AllocId(self.next_alloc_id);
        self.next_alloc_id += 1;
        let base = {
            let name = format!("{}_{}", if is_external { "ext" } else { "heap" }, id.0);
            Int::new_const(self.ctx, name.as_str())
        };
        let alloc = Allocation::new(base.clone(), size, align, element_ty, is_external);
        self.allocations.push(alloc);
        (id, base)
    }

    /// Indexed access to an allocation by its `AllocId` (the id is the index).
    pub(crate) fn alloc(&self, id: AllocId) -> &Allocation<'ctx, 'tcx> {
        &self.allocations[id.0]
    }

    /// Mutable indexed access to an allocation by its `AllocId`.
    pub(crate) fn alloc_mut(&mut self, id: AllocId) -> &mut Allocation<'ctx, 'tcx> {
        &mut self.allocations[id.0]
    }

    /// 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 fresh_int(&self, prefix: &str) -> Int<'ctx> {
        Int::fresh_const(self.ctx, prefix)
    }

    /// Get the value of a specific field within an aggregate local.
    pub(crate) fn field_value(&self, local: Local, path: &[usize]) -> Option<&VmValue<'ctx, 'tcx>> {
        self.field_values.get(&(local, path.to_vec()))
    }

    /// Set the value of a specific field within an aggregate local.
    pub(crate) fn set_field_value(
        &mut self,
        local: Local,
        path: Vec<usize>,
        value: VmValue<'ctx, 'tcx>,
    ) {
        self.field_values.insert((local, path), value);
    }

    /// Record a per-byte symbolic value at a concrete offset in an allocation.
    pub(crate) fn record_byte_value(&mut self, alloc_id: AllocId, offset: usize, term: Int<'ctx>) {
        let byte = self.bytes.entry((alloc_id, offset)).or_default();
        byte.value = Some(term);
        byte.init = true;
    }

    /// Mark a byte as initialized without changing its value.
    pub(crate) fn mark_byte_init(&mut self, alloc_id: AllocId, offset: usize) {
        self.bytes.entry((alloc_id, offset)).or_default().init = true;
    }

    /// Mark a byte as known NUL (0x00).
    pub(crate) fn mark_byte_nul(&mut self, alloc_id: AllocId, offset: usize) {
        self.bytes.entry((alloc_id, offset)).or_default().nul = Some(true);
    }

    /// Mark a byte as known non-NUL (!= 0x00).
    pub(crate) fn mark_byte_non_nul(&mut self, alloc_id: AllocId, offset: usize) {
        self.bytes.entry((alloc_id, offset)).or_default().nul = Some(false);
    }

    /// Look up a per-byte Z3 term for a concrete offset in an allocation.
    pub(crate) fn get_byte_value(&self, alloc_id: AllocId, offset: usize) -> Option<&Int<'ctx>> {
        self.bytes
            .get(&(alloc_id, offset))
            .and_then(|b| b.value.as_ref())
    }

    /// Check whether a byte at a concrete offset is known to be initialized.
    pub(crate) fn is_byte_init(&self, alloc_id: AllocId, offset: usize) -> bool {
        self.bytes.get(&(alloc_id, offset)).is_some_and(|b| b.init)
    }

    /// Check whether a byte at a concrete offset is known to be NUL.
    pub(crate) fn is_byte_nul(&self, alloc_id: AllocId, offset: usize) -> bool {
        self.bytes
            .get(&(alloc_id, offset))
            .is_some_and(|b| b.nul == Some(true))
    }

    /// Check whether a byte at a concrete offset is known to be non-NUL.
    pub(crate) fn is_byte_non_nul(&self, alloc_id: AllocId, offset: usize) -> bool {
        self.bytes
            .get(&(alloc_id, offset))
            .is_some_and(|b| b.nul == Some(false))
    }

    /// Return all known (offset, term) pairs for an allocation, sorted by offset.
    pub(crate) fn alloc_byte_values(&self, alloc_id: AllocId) -> Vec<(usize, &Int<'ctx>)> {
        let mut pairs: Vec<_> = self
            .bytes
            .iter()
            .filter_map(|((aid, off), byte)| {
                if *aid == alloc_id {
                    byte.value.as_ref().map(|term| (*off, term))
                } else {
                    None
                }
            })
            .collect();
        pairs.sort_by_key(|(off, _)| *off);
        pairs
    }

    /// Collect all offsets known to be NUL in an allocation.
    pub(crate) fn alloc_nul_offsets(&self, alloc_id: AllocId) -> Vec<usize> {
        self.bytes
            .iter()
            .filter_map(|((aid, off), byte)| {
                if *aid == alloc_id && byte.nul == Some(true) {
                    Some(*off)
                } else {
                    None
                }
            })
            .collect()
    }

    /// Collect all offsets known to be non-NUL in an allocation.
    pub(crate) fn alloc_non_nul_offsets(&self, alloc_id: AllocId) -> Vec<usize> {
        self.bytes
            .iter()
            .filter_map(|((aid, off), byte)| {
                if *aid == alloc_id && byte.nul == Some(false) {
                    Some(*off)
                } else {
                    None
                }
            })
            .collect()
    }

    /// Copy all per-byte tracking (value, init, NUL knowledge) from one
    /// allocation to another.
    pub(crate) fn copy_byte_tracking(&mut self, src: AllocId, dst: AllocId) {
        let infos: Vec<(usize, ByteInfo<'ctx>)> = self
            .bytes
            .iter()
            .filter(|((aid, _), _)| *aid == src)
            .map(|((_, off), byte)| (*off, byte.clone()))
            .collect();
        for (off, byte) in infos {
            self.bytes.insert((dst, off), byte);
        }
    }

    /// Assert path conditions and invariant constraints into a solver.
    pub(crate) fn assert_all(&self, solver: &z3::Solver<'ctx>) {
        for cond in &self.path_conditions {
            solver.assert(cond);
        }
        let zero = Int::from_u64(self.ctx, 0);
        for alloc in &self.allocations {
            if !alloc.is_external {
                solver.assert(&alloc.base._eq(&zero).not());
            }
            solver.assert(&alloc.size.ge(&zero));
            if alloc.align.simplify().as_u64() != Some(1) {
                solver.assert(&alloc.base.rem(&alloc.align)._eq(&zero));
            }
        }

        for (_local, value) in self.locals.iter() {
            self.assert_value_constraints(solver, value);
        }
        for value in self.field_values.values() {
            self.assert_value_constraints(solver, value);
        }
    }

    /// Assert a single symbolic value's known invariant constraints.
    fn assert_value_constraints(&self, solver: &z3::Solver<'ctx>, value: &VmValue<'ctx, 'tcx>) {
        let zero = Int::from_u64(self.ctx, 0);
        if value.invariants.non_null {
            solver.assert(&value.term._eq(&zero).not());
        }
        if let Some(ref prov) = value.provenance {
            let alloc = self.alloc(prov.alloc_id);
            let expected = Int::add(self.ctx, &[&alloc.base, &prov.offset]);
            solver.assert(&value.term._eq(&expected));
        }
        if matches!(
            value.ty.kind(),
            rustc_middle::ty::TyKind::Uint(_)
                | rustc_middle::ty::TyKind::Bool
                | rustc_middle::ty::TyKind::Char
        ) {
            solver.assert(&value.term.ge(&zero));
        }
        if matches!(value.ty.kind(), rustc_middle::ty::TyKind::Bool) {
            let one = Int::from_u64(self.ctx, 1);
            solver.assert(&value.term.le(&one));
        }
        if matches!(value.ty.kind(), rustc_middle::ty::TyKind::Char) {
            let max = Int::from_u64(self.ctx, 0x10FFFF);
            solver.assert(&value.term.le(&max));
        }
    }
}

impl std::fmt::Debug for VmState<'_, '_> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.debug_struct("VmState")
            .field("locals_count", &self.locals.len())
            .field("allocations_count", &self.allocations.len())
            .field("path_conditions", &self.path_conditions.len())
            .field("notes", &self.notes)
            .finish()
    }
}

// ── Shared value extraction ──────────────────────────────────────

impl<'ctx, 'tcx> VmState<'ctx, 'tcx> {
    /// Extract a VmValue from a MIR operand.
    pub(crate) fn value_of_operand(&self, operand: &Operand<'tcx>) -> VmValue<'ctx, 'tcx> {
        match operand {
            Operand::Copy(place) | Operand::Move(place) => self
                .value_of_place(place)
                .unwrap_or_else(|| self.unknown_value_for_place(place)),
            Operand::Constant(constant) => {
                let text = format!("{:?}", constant.const_);
                let int_val = crate::helpers::mir_utils::eval_const_scalar_int(
                    self.tcx,
                    &constant.const_,
                    &text,
                );
                let is_field_offset = int_val.is_none()
                    && crate::helpers::mir_utils::offset_of_container(self.tcx, &constant.const_)
                        .is_some();
                let term = if let Some(v) = int_val {
                    if v < 0 {
                        Int::from_i64(self.ctx, v as i64)
                    } else {
                        Int::from_u64(self.ctx, v as u64)
                    }
                } else {
                    // Create a deterministic name for const generics so
                    // multiple uses of the same parameter share one term.
                    let name = format!("const_{}", text.replace([':', '#', ' '], "_"));
                    Int::new_const(self.ctx, name.as_str())
                };
                let ty = constant.const_.ty();
                VmValue {
                    term,
                    ty,
                    provenance: None,
                    invariants: ValueInvariants {
                        is_field_offset,
                        ..ValueInvariants::default()
                    },
                }
            }
            #[cfg(rapx_ge_99)]
            Operand::RuntimeChecks(_) => VmValue::new(
                self.fresh_int("runtime_checks"),
                self.body.local_decls[Local::from_usize(0)].ty,
            ),
        }
    }

    /// Look up the value stored at a MIR place.
    pub(crate) fn value_of_place(&self, place: &Place<'tcx>) -> Option<VmValue<'ctx, 'tcx>> {
        if place.projection.is_empty() {
            return self.locals.get(&place.local).cloned();
        }

        // Collect field indices from projections
        let field_path: Vec<usize> = place
            .projection
            .iter()
            .filter_map(|proj| match proj.kind() {
                ProjectionElem::Field(field_idx, _) => Some(field_idx.as_usize()),
                _ => None,
            })
            .collect();

        // If we have a pure field path (only Field / Downcast projections),
        // look up in the per-field value map first.  For `Option`/`ControlFlow`,
        // the variant's data is stored under the same field index as the enum
        // field (the discriminant is tracked separately, not in field_values),
        // so `(x as Some).0` resolves to `field_values[x][0]`.
        let is_pure_field = place.projection.iter().all(|p| {
            matches!(
                p.kind(),
                ProjectionElem::Field(..) | ProjectionElem::Downcast(..)
            )
        });
        let has_downcast = place
            .projection
            .iter()
            .any(|p| matches!(p.kind(), ProjectionElem::Downcast(..)));
        if !field_path.is_empty() && is_pure_field {
            if let Some(val) = self
                .field_values
                .get(&(place.local, field_path.clone()))
                .cloned()
            {
                return Some(val);
            }
            if !has_downcast {
                // Fallback: when the base local has provenance, propagate it
                // to field accesses. This handles pointer-wrapper types (Box,
                // Unique, NonNull) where accessing inner pointer fields yields
                // the same provenance as the container.
                if let Some(base_val) = self.locals.get(&place.local) {
                    if let Some(ref prov) = base_val.provenance {
                        return Some(VmValue {
                            term: base_val.term.clone(),
                            ty: place.ty(self.body, self.tcx).ty,
                            provenance: Some(prov.clone()),
                            invariants: base_val.invariants.clone(),
                        });
                    }
                }
                return None;
            }
            // A Downcast without a materialized field falls through to the
            // Deref+Field / multi-element fallback below, which returns the
            // base local (preserving the pre-Downcast behavior instead of
            // forcing a fresh value).
        }

        // For Deref+Field chains (e.g. (*self).ptr), strip the leading Deref
        // projection(s) and look up field_values with the remaining field path.
        if !field_path.is_empty()
            && field_path.len() < place.projection.len()
            && place
                .projection
                .iter()
                .any(|p| matches!(p.kind(), ProjectionElem::Deref))
        {
            // Only Deref and Field projections — all non-Field must be Deref.
            let non_field_deref = place
                .projection
                .iter()
                .all(|p| matches!(p.kind(), ProjectionElem::Field(..) | ProjectionElem::Deref));
            if non_field_deref {
                if let Some(val) = self
                    .field_values
                    .get(&(place.local, field_path.clone()))
                    .cloned()
                {
                    return Some(val);
                }
                // Resolve a Deref+Field access through the pointee allocation's
                // per-allocation field tracking (e.g. `(*leaf).len` → the
                // `LeafNode.len` field value materialized by
                // `decompose_pointee_fields`).
                if let Some(base_val) = self.locals.get(&place.local) {
                    if let Some(alloc_id) = base_val.provenance_alloc_id() {
                        if let Some(val) = self
                            .alloc_field_values
                            .get(&(alloc_id, field_path.clone()))
                            .cloned()
                        {
                            return Some(val);
                        }
                    }
                }
            }
        }

        // Handle Deref + Field projections: follow the dereference chain to
        // get the pointee base, then apply field offsets.
        // E.g. `(*self).ptr` → Deref then Field(0).
        let mut base = self.locals.get(&place.local)?.clone();
        for proj in place.projection.iter() {
            match proj.kind() {
                ProjectionElem::Deref => {
                    base.ty = place.ty(self.body, self.tcx).ty;
                }
                ProjectionElem::Field(_field_idx, _) => {
                    // Try to get the field value from the VM's field tracking
                    if !field_path.is_empty() {
                        if let Some(val) = self
                            .field_values
                            .get(&(place.local, field_path.clone()))
                            .cloned()
                        {
                            return Some(val);
                        }
                    }
                    // Fallback: return the base with updated type info
                    base.ty = place.ty(self.body, self.tcx).ty;
                }
                _ => {}
            }
        }

        // Fall back to type-level resolution with single-element projections
        if place.projection.len() == 1 {
            if let Some(proj) = place.projection.first() {
                match proj {
                    ProjectionElem::Index(local) => {
                        if let Some(ref prov) = base.provenance {
                            let alloc_id = prov.alloc_id;
                            let byte_vals: Vec<_> = self.alloc_byte_values(alloc_id);
                            if !byte_vals.is_empty() {
                                let inner_ty = match base.ty.kind() {
                                    rustc_middle::ty::TyKind::Array(inner, _) => *inner,
                                    _ => return Some(base.clone()),
                                };
                                let elem_sz = self.size_of_ty(inner_ty) as usize;
                                let step = elem_sz.max(1);
                                if let Some(index_val) = self.locals.get(local) {
                                    if let Some(concrete_idx) = index_val.term.as_u64() {
                                        let offset = concrete_idx as usize * step;
                                        let term = self
                                            .get_byte_value(alloc_id, offset)
                                            .cloned()
                                            .unwrap_or_else(|| self.fresh_int("arr_elem"));
                                        return Some(VmValue {
                                            term,
                                            ty: place.ty(self.body, self.tcx).ty,
                                            provenance: None,
                                            invariants: ValueInvariants::default(),
                                        });
                                    } else {
                                        let mut chain = self.fresh_int("arr_elem");
                                        for (offset, term) in byte_vals.iter().rev() {
                                            let vidx = offset / step;
                                            let idx_term = Int::from_u64(self.ctx, vidx as u64);
                                            let cond = index_val.term._eq(&idx_term);
                                            chain = Bool::ite(&cond, term, &chain);
                                        }
                                        return Some(VmValue {
                                            term: chain,
                                            ty: place.ty(self.body, self.tcx).ty,
                                            provenance: None,
                                            invariants: ValueInvariants::default(),
                                        });
                                    }
                                }
                            }
                        }
                        return Some(base.clone());
                    }
                    _ => {}
                }
                match proj.kind() {
                    ProjectionElem::Deref => {
                        // A `*dest` load of a reference created from a field
                        // (`let r = &mut self.v`) should yield the field's
                        // *value* (materialized by `propagate_field_values_to_ref`
                        // at the empty field path), not the field's address.
                        if let Some(v) = self.field_values.get(&(place.local, Vec::new())).cloned()
                        {
                            return Some(v);
                        }
                        let mut val = base.clone();
                        val.ty = place.ty(self.body, self.tcx).ty;
                        return Some(val);
                    }
                    ProjectionElem::Field(_field_idx, _field_ty) => {
                        let val = base.clone();
                        return Some(val);
                    }
                    _ => {
                        // Downcast or other unsupported projection: still return
                        // the base with updated type so provenance propagates.
                        let mut val = base.clone();
                        val.ty = place.ty(self.body, self.tcx).ty;
                        return Some(val);
                    }
                }
            }
        }

        // For multi-element projections with Deref+Field or Downcast, return
        // the base value since we already traced through Deref above.
        if place.projection.len() > 1
            && place.projection.iter().any(|p| {
                matches!(
                    p.kind(),
                    ProjectionElem::Deref | ProjectionElem::Downcast(..)
                )
            })
        {
            let mut val = base;
            val.ty = place.ty(self.body, self.tcx).ty;
            return Some(val);
        }

        None
    }

    /// 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.
    pub(crate) fn unknown_value_for_place(&self, place: &Place<'tcx>) -> VmValue<'ctx, 'tcx> {
        let ty = place.ty(self.body, self.tcx).ty;
        VmValue {
            term: self.fresh_int("unknown"),
            ty,
            provenance: None,
            invariants: ValueInvariants::default(),
        }
    }
}