rapx/analysis/path/

graph.rs

use super::PathTree;
use crate::compat::{FxHashMap, FxHashSet};
use crate::graphs::{
    cfg::{CfgBlock, ControlFlowGraph},
    scc::{Scc, SccInfo},
};
use rustc_middle::{
    mir::{
        AggregateKind, BasicBlock, BinOp, Local, Operand, ProjectionElem, Rvalue, StatementKind,
        SwitchTargets, Terminator, TerminatorKind, UnOp, UnwindAction,
    },
    ty::{TyCtxt, TyKind, TypingEnv},
};
use rustc_span::def_id::DefId;
use std::collections::hash_map::DefaultHasher;
use std::hash::{Hash, Hasher};

use crate::limit::{
    LOCAL_INLINE_BLOCK_LIMIT, SCC_MAX_DEPTH, SCC_MAX_PATH_LEN, SCC_MAX_SEEN_PATHS,
    SCC_PATH_CACHE_LIMIT, WHOLE_CFG_PATH_DEPTH_LIMIT,
};

/// Check whether the current entry→entry sub-path introduces a new block
/// *sequence* (not just new blocks).  Different branch choices inside the SCC
/// produce different sequences even when all block IDs have already been seen,
/// e.g. `if i % 2 == 0 { A } else { B }` alternates between two paths through
/// the same set of blocks on successive loop iterations.
fn check_postfix_segment(
    path: &[usize],
    enter: usize,
    segment_counts: &mut FxHashMap<Vec<usize>, usize>,
    max_repeats: usize,
) -> bool {
    let segment = extract_segment(path, enter);
    let count = segment_counts.entry(segment).or_insert(0);
    *count += 1;
    *count == 1 || *count - 1 <= max_repeats
}

fn extract_segment(path: &[usize], enter: usize) -> Vec<usize> {
    let prev_pos = path[..path.len() - 1]
        .iter()
        .rposition(|&node| node == enter)
        .unwrap_or(0);
    path[prev_pos + 1..path.len() - 1].to_vec()
}

#[derive(Clone, Debug)]
/// A single enumerated acyclic path through an SCC region.
///
/// `blocks` is the ordered sequence of MIR block indices from the SCC entry
/// to the last block before exiting. The last block may have multiple CFG
/// successors outside the SCC (e.g. a `SwitchInt` branching to different
/// out-of-SCC targets), which are stored in `exit_successors`.
///
/// For example, in a loop with `switch x { A => loop_body, B => done1, C => done2 }`,
/// the corresponding `SccPath` would have `exit_successors = [done1, done2]`
/// — the DFS forks recursively into each of these when constructing whole-CFG paths.
pub struct SccPath {
    pub blocks: Vec<usize>,
    pub exit_successors: Vec<usize>,
}

/// Per-block info collected during construction for path reachability
/// analysis.  Each block's assignments, constants, and copy chains are
/// stored together so they can be read with a single index lookup.
#[derive(Clone, Debug, Default)]
pub struct BlockConstantInfo {
    pub assigned_locals: FxHashSet<usize>,
    pub constants: FxHashMap<usize, usize>,
    pub constraint_copies: FxHashMap<usize, usize>,
    /// Maps a local assigned by `AddWithOverflow(src, const)` to `(src, const)`.
    pub increments: FxHashMap<usize, (usize, usize)>,
    /// Maps a local assigned by `Rem(src, const)` to `(src, divisor)`.
    pub remainders: FxHashMap<usize, (usize, usize)>,
    /// Maps a boolean local (e.g., a guard result) to the binary comparison
    /// that produced it: `(op, lhs_local, rhs_kind)`.
    pub comparison_sources: FxHashMap<usize, ComparisonSource>,
    /// Set of locals that are provably non-null (e.g. assigned from
    /// `Box::into_raw`).  Used for path reachability pruning.
    pub known_nonnull_locals: FxHashSet<usize>,
    pub negation_sources: FxHashMap<usize, usize>,
    pub and_sources: FxHashMap<usize, (usize, usize)>,
}
/// Records the origin of a boolean temporary produced by a binary
/// comparison during guard-clause evaluation.
#[derive(Clone, Debug)]
pub struct ComparisonSource {
    pub op: rustc_middle::mir::BinOp,
    pub lhs_local: usize,
    pub rhs_local: usize,
    pub rhs_is_constant: bool,
}

/// Encode a `(local, field_index)` pair into a single `usize`.
const AGGREGATE_FIELD_MULT: usize = 256;
const AGGREGATE_FIELD_SENTINEL: usize = 1 << (usize::BITS as usize - 1);

fn encode_aggregate_field(local: usize, field: usize) -> usize {
    debug_assert!(field < AGGREGATE_FIELD_MULT);
    AGGREGATE_FIELD_SENTINEL | (local * AGGREGATE_FIELD_MULT + field)
}

fn decode_aggregate_field(encoded: usize) -> Option<(usize, usize)> {
    if encoded & AGGREGATE_FIELD_SENTINEL == 0 {
        return None;
    }
    let raw = encoded & !AGGREGATE_FIELD_SENTINEL;
    Some((raw / AGGREGATE_FIELD_MULT, raw % AGGREGATE_FIELD_MULT))
}

fn first_field_projection(place: &rustc_middle::mir::Place<'_>) -> Option<usize> {
    for proj in place.projection.iter() {
        if let rustc_middle::mir::ProjectionElem::Field(field, _) = proj {
            return Some(field.as_usize());
        }
    }
    None
}

/// Enum discriminant metadata used by [`check_switch_transition`].
///
/// `source_of` maps a discriminant local to the ADT local it was read from
/// (via `Rvalue::Discriminant`).  `variant_count_of` tracks the number of
/// variants for each ADT local, used to determine whether a `SwitchInt`
/// otherwise-target is uniquely determined.
#[derive(Clone, Debug, Default)]
pub struct DiscriminantInfo {
    pub source_of: FxHashMap<usize, usize>,
    pub variant_count_of: FxHashMap<usize, usize>,
}

/// CFG augmented with per-block constant info and discriminant metadata
/// for path reachability analysis.
///
/// `PathGraph` wraps a `ControlFlowGraph` and adds block-indexed data
/// that track assignments, constants, and copy chains.  These are used by
/// [`check_transition`](PathGraph::check_transition) to update a set of
/// discriminant constraints while traversing the CFG, enabling early
/// pruning of infeasible `SwitchInt` branches during path enumeration.
#[derive(Clone)]
pub struct PathGraph<'tcx> {
    pub cfg: ControlFlowGraph<'tcx>,
    pub block_info: Vec<BlockConstantInfo>,
    pub disc_info: DiscriminantInfo,
    /// Global store: maps encoded `(local, field_idx)` to source local from Aggregates.
    pub aggregate_field_sources: FxHashMap<usize, usize>,
    /// Global store: maps `dest` to `src` for pointer-cast chains.
    pub cast_chains: FxHashMap<usize, usize>,
    /// Global store: maps `_dest` to encoded `(base, field_idx)` from field-projection copies.
    pub field_projection_source: FxHashMap<usize, usize>,
    /// Per-inlined-callee argument binding: maps the callee's entry block
    /// (global index) to the caller's argument locals and destination local.
    pub inline_bindings: FxHashMap<usize, InlineBinding>,
    /// Per-inlined-callee parent: entry block (global index) → the `DefId` of
    /// the caller whose `Call` was inlined at that entry.
    pub inline_parents: FxHashMap<usize, DefId>,
    /// Caller blocks whose `Call` terminator was inlined (their successor edge
    /// now leads into a callee). The slicer skips these calls.
    pub inlined_call_blocks: FxHashSet<usize>,
    /// Per-function local-index namespace: `def_id` → base offset. The root
    /// caller uses base `0`; every inlined callee gets a fresh base so its MIR
    /// locals do not clash with the caller's in the flat constraint maps
    /// (`block_info`, `disc_info`, `cast_chains`, …). A constraint key `k` in
    /// the namespace of `def_id` denotes MIR local `k - base`.
    local_bases: FxHashMap<DefId, usize>,
    /// Next unused local-namespace base (monotonic counter).
    next_local_base: usize,
}

/// Argument/return binding recorded when a callee CFG is inlined.
#[derive(Clone, Debug)]
pub struct InlineBinding {
    /// Caller argument locals (callee param `_i+1` ← `arg_locals[i]`).
    pub arg_locals: Vec<usize>,
    /// Caller destination local (receives the callee's `_0`).
    pub dest_local: usize,
}

/// Scan a function's MIR and collect its per-block constant/discriminant
/// metadata and global source maps, remapping every MIR local `l` to
/// `local_base + l`. The root caller uses base `0`; inlined callees use a
/// fresh base so their locals never collide with the caller's in the flat
/// constraint maps (see [`PathGraph::local_bases`]).
#[allow(clippy::type_complexity)]
fn build_function_info(
    tcx: TyCtxt<'_>,
    def_id: DefId,
    local_base: usize,
) -> (
    Vec<BlockConstantInfo>,
    DiscriminantInfo,
    FxHashMap<usize, usize>,
    FxHashMap<usize, usize>,
    FxHashMap<usize, usize>,
) {
    let body = tcx.optimized_mir(def_id);
    let basicblocks = &body.basic_blocks;
    let mut block_info = Vec::new();
    let mut disc_info = DiscriminantInfo::default();
    let mut aggregate_field_sources: FxHashMap<usize, usize> = FxHashMap::default();
    let mut field_projection_source: FxHashMap<usize, usize> = FxHashMap::default();
    let mut cast_chains: FxHashMap<usize, usize> = FxHashMap::default();

    for i in 0..basicblocks.len() {
        let bb = &basicblocks[BasicBlock::from(i)];
        let mut info = BlockConstantInfo::default();

        for stmt in &bb.statements {
            if let StatementKind::Assign(assign) = &stmt.kind {
                let (place, rvalue) = &**assign;
                let dest = local_base + place.local.as_usize();
                // Writing through (*ptr).field doesn't reassign ptr itself,
                // so ptr's constraint should not be cleared.
                let is_deref = place
                    .projection
                    .iter()
                    .any(|p| matches!(p, ProjectionElem::Deref));
                if !is_deref {
                    info.assigned_locals.insert(dest);
                }
                match rvalue {
                    Rvalue::Use(Operand::Constant(c), ..) => {
                        let typing_env = TypingEnv::post_analysis(tcx, def_id);
                        let val = match c.const_.ty().kind() {
                            TyKind::Bool => c
                                .const_
                                .try_eval_bool(tcx, typing_env)
                                .map(|b| if b { 1 } else { 0 }),
                            TyKind::Int(_) | TyKind::Uint(_) => {
                                c.const_.try_eval_bits(tcx, typing_env).map(|v| v as usize)
                            }
                            _ => None,
                        };
                        if let Some(val) = val {
                            info.constants.insert(dest, val);
                        }
                    }
                    Rvalue::Use(Operand::Copy(src) | Operand::Move(src), ..) => {
                        let src_local = local_base + src.local.as_usize();
                        if let Some(field_proj) = first_field_projection(src) {
                            let encoded = encode_aggregate_field(src_local, field_proj);
                            field_projection_source.insert(dest, encoded);
                        }
                        info.constraint_copies.insert(dest, src_local);
                    }
                    Rvalue::Discriminant(rv_place) => {
                        let src_local = local_base + rv_place.local.as_usize();
                        disc_info.source_of.insert(dest, src_local);
                        if !disc_info.variant_count_of.contains_key(&src_local) {
                            let src_ty = body.local_decls[rv_place.local].ty;
                            if let TyKind::Adt(adt_def, _) = src_ty.kind() {
                                let num = adt_def.variants().len();
                                if num > 0 {
                                    disc_info.variant_count_of.insert(src_local, num);
                                }
                            }
                        }
                    }
                    Rvalue::Aggregate(kind, operands) => {
                        if let AggregateKind::Adt(_, _, _, _, _) = kind.as_ref() {
                            let agg_local = local_base + place.local.as_usize();
                            for (field_idx, operand) in operands.iter().enumerate() {
                                if let Operand::Copy(src) | Operand::Move(src) = operand {
                                    let key = encode_aggregate_field(agg_local, field_idx);
                                    let src_local = local_base + src.local.as_usize();
                                    aggregate_field_sources.insert(key, src_local);
                                }
                            }
                        }
                        let discr = match kind.as_ref() {
                            AggregateKind::Adt(_, variant_idx, _, _, _) => Some(variant_idx.as_usize()),
                            _ => None,
                        };
                        if let Some(discr) = discr {
                            info.constants.insert(dest, discr);
                            if !disc_info.variant_count_of.contains_key(&dest) {
                                let dest_ty = body.local_decls[place.local].ty;
                                if let TyKind::Adt(adt_def, _) = dest_ty.kind() {
                                    let num = adt_def.variants().len();
                                    if num > 0 {
                                        disc_info.variant_count_of.insert(dest, num);
                                    }
                                }
                            }
                        }
                    }
                    Rvalue::BinaryOp(op, operands) if matches!(op, BinOp::AddWithOverflow) => {
                        let (lhs, rhs): (&Operand<'_>, &Operand<'_>) =
                            (&operands.0, &operands.1);
                        if let Some(lhs_local) = match lhs {
                            Operand::Copy(l) | Operand::Move(l) if l.projection.is_empty() => {
                                Some(local_base + l.local.as_usize())
                            }
                            _ => None,
                        } {
                            let incr = match rhs {
                                Operand::Constant(c) => {
                                    let typing_env = TypingEnv::post_analysis(tcx, def_id);
                                    c.const_.try_eval_bits(tcx, typing_env).map(|v| v as usize)
                                }
                                _ => None,
                            };
                            if let Some(incr) = incr {
                                info.increments.insert(dest, (lhs_local, incr));
                            }
                        }
                    }
                    Rvalue::BinaryOp(op, operands)
                        if matches!(
                            op,
                            BinOp::Lt
                                | BinOp::Le
                                | BinOp::Gt
                                | BinOp::Ge
                                | BinOp::Eq
                                | BinOp::Ne
                                | BinOp::BitAnd
                        ) =>
                    {
                        let (lhs, rhs): (&Operand<'_>, &Operand<'_>) =
                            (&operands.0, &operands.1);
                        let lhs_local = match lhs {
                            Operand::Copy(l) | Operand::Move(l) if l.projection.is_empty() => {
                                Some(local_base + l.local.as_usize())
                            }
                            _ => None,
                        };
                        if let Some(lhs_local) = lhs_local {
                            let rhs_eval = match rhs {
                                Operand::Constant(c) => {
                                    let typing_env = TypingEnv::post_analysis(tcx, def_id);
                                    c.const_
                                        .try_eval_bits(tcx, typing_env)
                                        .map(|v| (v as usize, true))
                                }
                                Operand::Copy(r) | Operand::Move(r)
                                    if r.projection.is_empty() =>
                                {
                                    Some((local_base + r.local.as_usize(), false))
                                }
                                _ => None,
                            };
                            let Some((rhs_local, rhs_is_constant)) = rhs_eval else {
                                continue;
                            };
                            info.comparison_sources.insert(
                                dest,
                                ComparisonSource {
                                    op: *op,
                                    lhs_local,
                                    rhs_local,
                                    rhs_is_constant,
                                },
                            );
                            if matches!(op, BinOp::BitAnd)
                                && matches!(body.local_decls[place.local].ty.kind(), TyKind::Bool)
                            {
                                info.and_sources.insert(dest, (lhs_local, rhs_local));
                            }
                        }
                    }
                    Rvalue::BinaryOp(op, operands) if matches!(op, BinOp::Rem) => {
                        let (lhs, rhs): (&Operand<'_>, &Operand<'_>) =
                            (&operands.0, &operands.1);
                        if let Some(lhs_local) = match lhs {
                            Operand::Copy(l) | Operand::Move(l) if l.projection.is_empty() => {
                                Some(local_base + l.local.as_usize())
                            }
                            _ => None,
                        } {
                            let divisor = match rhs {
                                Operand::Constant(c) => {
                                    let typing_env = TypingEnv::post_analysis(tcx, def_id);
                                    c.const_.try_eval_bits(tcx, typing_env).map(|v| v as usize)
                                }
                                _ => None,
                            };
                            if let Some(divisor) = divisor {
                                if divisor != 0 {
                                    info.remainders.insert(dest, (lhs_local, divisor));
                                }
                            }
                        }
                    }
                    Rvalue::UnaryOp(unop, operand) => {
                        if matches!(unop, UnOp::Not)
                            && let Operand::Copy(src) | Operand::Move(src) = operand
                        {
                            info.negation_sources
                                .insert(dest, local_base + src.local.as_usize());
                        }
                    }
                    Rvalue::Cast(_, operand, _) => {
                        if let Operand::Copy(src) | Operand::Move(src) = operand
                            && matches!(
                                body.local_decls[place.local].ty.kind(),
                                TyKind::RawPtr(..) | TyKind::Int(..) | TyKind::Uint(..)
                            )
                        {
                            cast_chains.insert(dest, local_base + src.local.as_usize());
                        }
                    }
                    _ => {} // close match rvalue
                }
            }
        }

        if let Some(terminator) = &bb.terminator {
            if let TerminatorKind::Call {
                destination,
                ref func,
                ..
            } = terminator.kind
            {
                let name = crate::helpers::mir_utils::call_name(tcx, func);
                if name.contains("::into_raw")
                    || (name.contains("::new") && name.contains("Box"))
                    || name.contains("::as_mut_ptr")
                    || name.contains("::as_ptr")
                {
                    info.known_nonnull_locals
                        .insert(local_base + destination.local.as_usize());
                }
                if name.contains("null_mut") || (name.contains("null") && name.contains("ptr::")) {
                    info.constants
                        .insert(local_base + destination.local.as_usize(), 0);
                }
            }
        }

        block_info.push(info);
    }

    (
        block_info,
        disc_info,
        aggregate_field_sources,
        field_projection_source,
        cast_chains,
    )
}

impl<'tcx> PathGraph<'tcx> {
    pub fn new(tcx: TyCtxt<'tcx>, def_id: DefId) -> PathGraph<'tcx> {
        let body = tcx.optimized_mir(def_id);
        let basicblocks = &body.basic_blocks;
        let mut cfg_blocks = Vec::<CfgBlock>::new();

        for i in 0..basicblocks.len() {
            let bb = &basicblocks[BasicBlock::from(i)];
            let mut cfg_block = CfgBlock::new(def_id, i, bb.is_cleanup);

            let Some(terminator) = &bb.terminator else {
                cfg_blocks.push(cfg_block);
                continue;
            };

            match terminator.kind.clone() {
                TerminatorKind::Goto { ref target } => {
                    cfg_block.add_next(target.as_usize());
                }
                TerminatorKind::SwitchInt {
                    discr: _,
                    ref targets,
                } => {
                    for (_, ref target) in targets.iter() {
                        cfg_block.add_next(target.as_usize());
                    }
                    cfg_block.add_next(targets.otherwise().as_usize());
                }
                TerminatorKind::Drop {
                    place: _,
                    target,
                    unwind,
                    replace: _,
                    drop: _,
                    #[cfg(not(rapx_ge_99))]
                        async_fut: _,
                } => {
                    cfg_block.add_next(target.as_usize());
                    if let UnwindAction::Cleanup(target) = unwind {
                        cfg_block.add_next(target.as_usize());
                    }
                }
                TerminatorKind::Call {
                    ref target,
                    ref unwind,
                    ..
                } => {
                    if let Some(tt) = target {
                        cfg_block.add_next(tt.as_usize());
                    }
                    if let UnwindAction::Cleanup(tt) = unwind {
                        cfg_block.add_next(tt.as_usize());
                    }
                }
                TerminatorKind::Assert {
                    cond: _,
                    expected: _,
                    msg: _,
                    ref target,
                    ref unwind,
                } => {
                    cfg_block.add_next(target.as_usize());
                    if let UnwindAction::Cleanup(target) = unwind {
                        cfg_block.add_next(target.as_usize());
                    }
                }
                TerminatorKind::Yield {
                    value: _,
                    ref resume,
                    resume_arg: _,
                    ref drop,
                } => {
                    cfg_block.add_next(resume.as_usize());
                    if let Some(target) = drop {
                        cfg_block.add_next(target.as_usize());
                    }
                }
                TerminatorKind::FalseEdge {
                    ref real_target,
                    imaginary_target: _,
                } => {
                    cfg_block.add_next(real_target.as_usize());
                }
                TerminatorKind::FalseUnwind {
                    ref real_target,
                    unwind: _,
                } => {
                    cfg_block.add_next(real_target.as_usize());
                }
                TerminatorKind::InlineAsm {
                    template: _,
                    operands: _,
                    options: _,
                    line_spans: _,
                    ref unwind,
                    targets,
                    asm_macro: _,
                } => {
                    for target in targets {
                        cfg_block.add_next(target.as_usize());
                    }
                    if let UnwindAction::Cleanup(target) = unwind {
                        cfg_block.add_next(target.as_usize());
                    }
                }
                _ => {}
            }

            cfg_blocks.push(cfg_block);
        }

        let cfg = ControlFlowGraph::new(def_id, tcx, cfg_blocks);
        let (block_info, disc_info, aggregate_field_sources, field_projection_source, cast_chains) =
            build_function_info(tcx, def_id, 0);

        let mut local_bases = FxHashMap::default();
        local_bases.insert(def_id, 0);

        PathGraph {
            cfg,
            block_info,
            disc_info,
            aggregate_field_sources,
            field_projection_source,
            cast_chains,
            inline_bindings: FxHashMap::default(),
            inline_parents: FxHashMap::default(),
            inlined_call_blocks: FxHashSet::default(),
            local_bases,
            next_local_base: body.local_decls.len(),
        }
    }

    /// Inline the CFG of inlinable callees into this graph so that path
    /// enumeration covers the callee's branches.
    ///
    /// Inlining is recursive *within the local crate*: a local callee's own
    /// calls are inlined too. Cross-crate callees are inlined only at the level
    /// where a local function calls them — their bodies are not recursed into,
    /// so the standard library's internal branchy precondition machinery
    /// (`is_aligned_to`, `ub_checks`, …) is not pulled in, which would blow up
    /// path enumeration with branches that have no constraint tracking.
    ///
    /// Each callee is otherwise subject to the same shape constraints as
    /// before: cross-crate callees with MIR are always inlined, and a local
    /// callee is inlined only when it is small (at most
    /// [`LOCAL_INLINE_BLOCK_LIMIT`](crate::limit::LOCAL_INLINE_BLOCK_LIMIT) basic
    /// blocks), so branch-free accessors
    /// (`get`, `count_ones`, …) also land in the CFG and their field
    /// provenance is reconstructed element-by-element. Intrinsics
    /// have no MIR; callees with a builtin model are kept opaque because their
    /// summary is more precise than their body.
    ///
    /// Recursion is bounded by an `expanded` set so that (mutually) recursive
    /// local functions do not grow the CFG without bound — a back-edge to an
    /// already-inlined callee is left as an ordinary call edge for the VM's
    /// fallback handling.
    ///
    /// Opt-in — callers that assume a single-function block space (e.g. alias
    /// analysis) must not call this.
    pub fn inline_callees(&mut self) {
        let tcx = self.tcx();
        let caller_def_id = self.def_id();

        let mut expanded: FxHashSet<DefId> = FxHashSet::default();
        expanded.insert(caller_def_id);

        loop {
            let mut pending: Vec<(usize, DefId)> = Vec::new();
            for i in 0..self.cfg.blocks.len() {
                // Only recurse into *local* functions: cross-crate bodies are
                // inlined but never scanned for further calls.
                if self.cfg.block(i).def_id.as_local().is_none() {
                    continue;
                }
                let Some(term) = self.terminator(i) else {
                    continue;
                };
                let TerminatorKind::Call { func, target, .. } = &term.kind else {
                    continue;
                };
                // A diverging call (`panic!` / `unreachable!`) has no normal
                // successor to reconnect through the inlined body, so it is
                // never inlined.
                if target.is_none() {
                    continue;
                }
                // Cross-crate callees keep their raw trait-method def_id (trait
                // methods have no MIR and are left to builtin models). Local
                // callees are resolved to the concrete impl so a user trait
                // method (e.g. `<MyIter as Iterator>::next`) inlines against its
                // actual MIR.
                let Some(base_callee) = crate::helpers::mir_utils::dep_callee_def_id(func) else {
                    continue;
                };
                let cross_crate = base_callee.as_local().is_none();
                let callee = if cross_crate {
                    base_callee
                } else {
                    crate::helpers::mir_utils::dep_callee_resolved_def_id(
                        tcx,
                        self.cfg.block(i).def_id,
                        func,
                    )
                    .unwrap_or(base_callee)
                };
                let has_fn_sim =
                    crate::verify::call_summary::builtin_models::is_modeled(Some(callee));
                // A couple of helpers stay opaque because the VM's
                // interprocedural execution is more precise than their inlined
                // body:
                // - `as_ptr`/`as_mut_ptr` (local re-implementations) lose the
                //   provenance that `eff_alias_ptr`/`handle_callee_entry`
                //   otherwise reconstruct from the argument.
                let is_container_as_ptr =
                    crate::verify::api_classify::is_container_as_ptr(tcx, callee);
                if !tcx.is_mir_available(callee)
                    || expanded.contains(&callee)
                    || has_fn_sim
                    || is_container_as_ptr
                {
                    continue;
                }
                // A local callee is inlined only when it is small (a transitive
                // shape bound that keeps path enumeration tractable; see
                // `LOCAL_INLINE_BLOCK_LIMIT`). Branch-free accessors are no
                // longer excluded: their bodies land in the CFG and the backward
                // slicer/VM reconstruct field provenance through the inlined
                // call chain.
                let small_local = !cross_crate && {
                    let body = tcx.optimized_mir(callee);
                    body.basic_blocks.len() <= LOCAL_INLINE_BLOCK_LIMIT
                };
                if cross_crate || small_local {
                    pending.push((i, callee));
                }
            }

            if pending.is_empty() {
                break;
            }

            // Mark every pending callee as expanded *before* inlining so a
            // callee that (transitively) calls itself or another pending callee
            // is not inlined again on a later iteration.
            for (_, callee) in &pending {
                expanded.insert(*callee);
            }

            for (caller_idx, callee) in pending {
                self.inline_one(caller_idx, callee);
            }
        }
    }

    /// Inline a single callee into `caller_idx`, reconnecting the caller's
    /// normal successor edge through the callee body.
    fn inline_one(&mut self, caller_idx: usize, callee: DefId) {
        let tcx = self.tcx();
        // The caller block may itself be an inlined callee (nested inlining), so
        // its MIR successor indices must be shifted into the global block space.
        let caller_base = caller_idx - self.cfg.block(caller_idx).local_index;
        let (caller_target, caller_unwind, arg_locals, dest_local) = match self.terminator(caller_idx)
        {
            Some(term) => match &term.kind {
                TerminatorKind::Call {
                    target,
                    unwind,
                    args,
                    destination,
                    ..
                } => {
                    let target = target.map(|t| caller_base + t.as_usize());
                    let unwind = match unwind {
                        UnwindAction::Cleanup(t) => Some(caller_base + t.as_usize()),
                        _ => None,
                    };
                    let arg_locals: Vec<usize> = args
                        .iter()
                        .filter_map(|a| a.node.place().map(|p| p.local.as_usize()))
                        .collect();
                    (target, unwind, arg_locals, destination.local.as_usize())
                }
                _ => (None, None, Vec::new(), 0),
            },
            None => (None, None, Vec::new(), 0),
        };
        let Some(target) = caller_target else {
            return;
        };

        let body = tcx.optimized_mir(callee);
        let base = self.cfg.blocks.len();
        let block_count = body.basic_blocks.len();

        // Build the callee's constant/discriminant metadata under its own local
        // namespace so its constraint tracking doesn't clash with the caller's.
        let local_base = self.assign_local_base(callee);
        let (callee_info, callee_disc, callee_agg, callee_fproj, callee_cast) =
            build_function_info(tcx, callee, local_base);

        for i in 0..block_count {
            let bb = &body.basic_blocks[BasicBlock::from(i)];
            let mut cb = CfgBlock {
                index: base + i,
                def_id: callee,
                local_index: i,
                is_cleanup: bb.is_cleanup,
                next: FxHashSet::default(),
                scc: SccInfo::new(base + i),
            };
            if let Some(term) = &bb.terminator {
                match &term.kind {
                    TerminatorKind::Goto { target: t } => {
                        cb.add_next(base + t.as_usize());
                    }
                    TerminatorKind::SwitchInt { targets, .. } => {
                        for (_, t) in targets.iter() {
                            cb.add_next(base + t.as_usize());
                        }
                        cb.add_next(base + targets.otherwise().as_usize());
                    }
                    TerminatorKind::Return => {
                        cb.add_next(target);
                    }
                    TerminatorKind::UnwindResume => {
                        // A callee that unwinds re-enters the caller at its
                        // unwind/cleanup block (the caller's `Cleanup` target of
                        // the inlined call), never at the normal return target.
                        if let Some(u) = caller_unwind {
                            cb.add_next(u);
                        }
                    }
                    TerminatorKind::Call {
                        target: t,
                        unwind,
                        ..
                    } => {
                        if let Some(t) = t {
                            cb.add_next(base + t.as_usize());
                        }
                        if let UnwindAction::Cleanup(tt) = unwind {
                            cb.add_next(base + tt.as_usize());
                        }
                    }
                    TerminatorKind::Drop {
                        target: t, unwind, ..
                    } => {
                        cb.add_next(base + t.as_usize());
                        if let UnwindAction::Cleanup(tt) = unwind {
                            cb.add_next(base + tt.as_usize());
                        }
                    }
                    TerminatorKind::Assert {
                        target: t,
                        unwind,
                        ..
                    } => {
                        cb.add_next(base + t.as_usize());
                        if let UnwindAction::Cleanup(tt) = unwind {
                            cb.add_next(base + tt.as_usize());
                        }
                    }
                    TerminatorKind::FalseEdge { real_target, .. }
                    | TerminatorKind::FalseUnwind { real_target, .. } => {
                        cb.add_next(base + real_target.as_usize());
                    }
                    _ => {}
                }
            }
            self.cfg.blocks.push(cb);
        }

        // Append the callee's per-block metadata and merge its global source
        // maps (all keyed in the callee's own local namespace).
        self.block_info.extend(callee_info);
        self.disc_info.source_of.extend(callee_disc.source_of);
        self.disc_info.variant_count_of.extend(callee_disc.variant_count_of);
        self.aggregate_field_sources.extend(callee_agg);
        self.field_projection_source.extend(callee_fproj);
        self.cast_chains.extend(callee_cast);

        // Record the argument binding for the callee entry.
        self.inline_bindings.insert(
            base,
            InlineBinding {
                arg_locals,
                dest_local,
            },
        );
        self.inline_parents
            .insert(base, self.cfg.block(caller_idx).def_id);
        self.inlined_call_blocks.insert(caller_idx);

        // Reconnect the caller's normal successor edge through the callee entry.
        let caller_block = self.cfg.block_mut(caller_idx);
        caller_block.next.remove(&target);
        caller_block.next.insert(base);
    }

    pub fn find_scc(&mut self) {
        self.cfg.find_scc();
        self.populate_all_child_sccs();
    }

    pub fn def_id(&self) -> DefId {
        self.cfg.def_id
    }

    pub fn tcx(&self) -> TyCtxt<'tcx> {
        self.cfg.tcx
    }

    pub fn cfg_block(&self, index: usize) -> &CfgBlock {
        self.cfg.block(index)
    }

    pub fn cfg_block_mut(&mut self, index: usize) -> &mut CfgBlock {
        self.cfg.block_mut(index)
    }

    /// Retrieve the MIR terminator for the block at `index` on demand.
    pub fn terminator(&self, index: usize) -> Option<&Terminator<'tcx>> {
        self.cfg.terminator(index)
    }

    pub fn is_cleanup_block(&self, index: usize) -> bool {
        self.cfg
            .blocks
            .get(index)
            .map(|b| b.is_cleanup)
            .unwrap_or(false)
    }

    /// The local-index base of `def_id`'s MIR locals in the flat constraint
    /// maps. The root caller is base `0`; inlined callees get a fresh base.
    fn local_base_of(&self, def_id: DefId) -> usize {
        self.local_bases.get(&def_id).copied().unwrap_or(0)
    }

    /// Remap `def_id`'s MIR local `local` into the global constraint namespace.
    fn remap_local(&self, def_id: DefId, local: usize) -> usize {
        self.local_base_of(def_id) + local
    }

    /// Assign a fresh local-namespace base for `def_id` (or return its existing
    /// base if the function has already been inlined).
    fn assign_local_base(&mut self, def_id: DefId) -> usize {
        if let Some(&base) = self.local_bases.get(&def_id) {
            return base;
        }
        let base = self.next_local_base;
        let local_count = self.tcx().optimized_mir(def_id).local_decls.len();
        self.local_bases.insert(def_id, base);
        self.next_local_base = base + local_count;
        base
    }

    /// Get the number of variants for a constraint local (in `def_id`'s local
    /// namespace). First checks the pre-populated `variant_count_of` hashmap,
    /// then falls back to the local's declared type (for ADT locals that gained
    /// their type through field projections in nested destructuring patterns
    /// rather than explicit construction).
    fn get_variant_count(&self, local: usize, def_id: DefId) -> Option<usize> {
        if let Some(&count) = self.disc_info.variant_count_of.get(&local) {
            return Some(count);
        }
        let body = self.cfg.tcx.optimized_mir(def_id);
        let original = local - self.local_base_of(def_id);
        let mut ty = body.local_decls[Local::from_usize(original)].ty;
        while let TyKind::Ref(_, inner_ty, _) | TyKind::RawPtr(inner_ty, _) = ty.kind() {
            ty = *inner_ty;
        }
        match ty.kind() {
            TyKind::Adt(adt_def, _) if adt_def.is_enum() => Some(adt_def.variants().len()),
            _ => None,
        }
    }

    /// Check a single transition `cur -> next` for reachability and update
    /// discriminant constraints. Returns `false` if the transition is
    /// provably unreachable.
    pub fn check_transition(
        &self,
        cur: usize,
        next: usize,
        constraints: &mut FxHashMap<usize, usize>,
    ) -> bool {
        if cur >= self.cfg.blocks.len() || next >= self.cfg.blocks.len() {
            return false;
        }

        if let Some(info) = self.block_info.get(cur) {
            for local in &info.assigned_locals {
                if let Some(&src) = info.constraint_copies.get(local) {
                    if let Some(val) = self.resolve_local_value(src, constraints) {
                        constraints.insert(*local, val);
                        continue;
                    }
                    if let Some(&dst_val) = constraints.get(local) {
                        constraints.insert(src, dst_val);
                        constraints.insert(*local, dst_val);
                        continue;
                    }
                }
                if let Some(&val) = info.constants.get(local) {
                    constraints.insert(*local, val);
                    continue;
                }
                constraints.remove(local);
            }
            for local in &info.known_nonnull_locals {
                constraints.insert(*local, usize::MAX);
            }
        }

        // Also clear constraints for locals assigned by the terminator
        // (e.g. _13 = Iterator::next() in a Call terminator). The block's
        // assigned_locals only covers statement-level assignments, so
        // terminator-side assignments are handled here.
        if let Some(terminator) = self.terminator(cur) {
            let local_base = self.local_base_of(self.cfg.block(cur).def_id);
            let assigned = match &terminator.kind {
                TerminatorKind::Call { destination, .. } => {
                    Some(local_base + destination.local.as_usize())
                }
                TerminatorKind::Yield { resume_arg, .. } => {
                    Some(local_base + resume_arg.local.as_usize())
                }
                _ => None,
            };
            if let Some(local) = assigned {
                // Propagate known nullness from BlockConstantInfo.
                if let Some(block_info) = self.block_info.get(cur) {
                    if let Some(&val) = block_info.constants.get(&local) {
                        constraints.insert(local, val);
                    } else if block_info.known_nonnull_locals.contains(&local) {
                        constraints.insert(local, usize::MAX);
                    } else {
                        constraints.remove(&local);
                    }
                } else {
                    constraints.remove(&local);
                }
            }
        }

        let successors = &self.cfg.block(cur).next;
        if !successors.contains(&next) {
            if !self.is_unwind_target(cur, next) {
                return false;
            }
        }

        if !self.check_switch_transition(cur, next, constraints) {
            return false;
        }

        if !self.check_assert_transition(cur, next, constraints) {
            return false;
        }

        true
    }

    fn check_assert_transition(
        &self,
        cur: usize,
        next: usize,
        constraints: &FxHashMap<usize, usize>,
    ) -> bool {
        let Some(terminator) = self.cfg.terminator(cur) else {
            return true;
        };
        let TerminatorKind::Assert { cond, target, .. } = &terminator.kind else {
            return true;
        };
        let base = cur - self.cfg.block(cur).local_index;
        if next != base + target.as_usize() {
            return true;
        }
        let cond_local = match cond {
            Operand::Copy(p) | Operand::Move(p) => {
                self.remap_local(self.cfg.block(cur).def_id, p.local.as_usize())
            }
            Operand::Constant(c) => {
                let typing_env =
                    rustc_middle::ty::TypingEnv::post_analysis(self.cfg.tcx, self.cfg.def_id);
                return c
                    .const_
                    .try_eval_bool(self.cfg.tcx, typing_env)
                    .unwrap_or(true);
            }
            #[cfg(rapx_ge_95)]
            Operand::RuntimeChecks(_) => return true,
        };
        self.resolve_bool_local(cond_local, constraints)
            .is_none_or(|v| v == 1)
    }

    fn resolve_simple_bool(
        &self,
        local: usize,
        constraints: &FxHashMap<usize, usize>,
    ) -> Option<usize> {
        if let Some(&val) = constraints.get(&local)
            && val <= 1
        {
            return Some(val);
        }
        for info in &self.block_info {
            if let Some(&val) = info.constants.get(&local)
                && val <= 1
            {
                return Some(val);
            }
            if let Some(cmp) = info.comparison_sources.get(&local) {
                if matches!(cmp.op, BinOp::Eq | BinOp::Ne) {
                    let is_eq = matches!(cmp.op, BinOp::Eq);
                    if cmp.rhs_is_constant {
                        if let Some(lhs_val) = self.resolve_local_value(cmp.lhs_local, constraints)
                        {
                            return Some(if is_eq {
                                if lhs_val == cmp.rhs_local { 1 } else { 0 }
                            } else {
                                if lhs_val != cmp.rhs_local { 1 } else { 0 }
                            });
                        }
                    } else {
                        let lhs_val = self.resolve_local_value(cmp.lhs_local, constraints);
                        let rhs_val = self.resolve_local_value(cmp.rhs_local, constraints);
                        if let Some(lhs_val) = lhs_val {
                            if let Some(rhs_val) = rhs_val {
                                return Some(if is_eq {
                                    if lhs_val == rhs_val { 1 } else { 0 }
                                } else {
                                    if lhs_val != rhs_val { 1 } else { 0 }
                                });
                            }
                        } else if let Some(rhs_val) = rhs_val {
                            return Some(if is_eq {
                                if cmp.lhs_local == rhs_val { 1 } else { 0 }
                            } else {
                                if cmp.lhs_local != rhs_val { 1 } else { 0 }
                            });
                        }
                    }
                }
            }
        }
        None
    }

    fn resolve_bool_local(
        &self,
        local: usize,
        constraints: &FxHashMap<usize, usize>,
    ) -> Option<usize> {
        let mut stack = vec![(local, false)];
        let mut seen = FxHashSet::default();
        while let Some((cur, negated)) = stack.pop() {
            let key = if negated { cur | (1 << 31) } else { cur };
            if !seen.insert(key) {
                continue;
            }
            if let Some(v) = self.resolve_simple_bool(cur, constraints) {
                return Some(if negated { 1 - v } else { v });
            }
            for info in &self.block_info {
                if let Some(&src) = info.constraint_copies.get(&cur) {
                    stack.push((src, negated));
                }
                if let Some(&src) = info.negation_sources.get(&cur) {
                    stack.push((src, !negated));
                }
                if let Some(&(lhs, rhs)) = info.and_sources.get(&cur) {
                    let a = self.resolve_simple_bool(lhs, constraints);
                    let b = self.resolve_simple_bool(rhs, constraints);
                    if let (Some(a), Some(b)) = (a, b) {
                        let r = if a == 1 && b == 1 { 1 } else { 0 };
                        return Some(if negated { 1 - r } else { r });
                    }
                }
            }
            if let Some(&src) = self.cast_chains.get(&cur) {
                stack.push((src, negated));
            }
        }
        None
    }

    /// Check whether `cur → next` is a valid `SwitchInt` transition given
    /// current discriminant constraints. Returns `false` when the transition
    /// contradicts a known discriminant value. Also records newly learned
    /// constraints from the taken branch into `constraints`.
    fn check_switch_transition(
        &self,
        cur: usize,
        next: usize,
        constraints: &mut FxHashMap<usize, usize>,
    ) -> bool {
        let Some(terminator) = self.cfg.terminator(cur) else {
            return true;
        };
        // Base offset of the function owning `cur` (0 for the caller, the
        // callee's global start for inlined blocks). Switch targets are local
        // MIR block indices, so they must be shifted into the global space.
        let base = cur - self.cfg.block(cur).local_index;

        match &terminator.kind {
            TerminatorKind::SwitchInt { discr, targets } => {
                // The discriminant local is remapped into its function's
                // namespace so it matches `disc_info`/`constraints` keys.
                let discr_local = discr
                    .place()
                    .map(|p| self.remap_local(self.cfg.block(cur).def_id, p.local.as_usize()));
                let constraint_local = discr_local
                    .and_then(|l| self.disc_info.source_of.get(&l).copied())
                    .or(discr_local);

                // Collect all possible successor blocks for this switch.
                let all_targets: FxHashSet<usize> = targets
                    .iter()
                    .map(|(_, bb)| base + bb.as_usize())
                    .chain(std::iter::once(base + targets.otherwise().as_usize()))
                    .collect();

                if !all_targets.contains(&next) {
                    return false;
                }

                // Try to evaluate a concrete constant for the discriminant.
                let const_val = match discr {
                    Operand::Constant(c) => c
                        .const_
                        .try_eval_target_usize(
                            self.cfg.tcx,
                            TypingEnv::post_analysis(self.cfg.tcx, self.cfg.def_id),
                        )
                        .map(|v| v as usize),
                    _ => None,
                };

                if let Some(val) = const_val {
                    // Discriminant is a literal constant — only one target is
                    // reachable.
                    let expected = resolve_switch_target(targets, val as u128);
                    if next != base + expected {
                        return false;
                    }
                    if let Some(local) = constraint_local {
                        constraints.insert(local, val);
                    }
                    return true;
                }

                if let Some(local) = constraint_local {
                    if let Some(&known_val) = constraints.get(&local) {
                        let expected = resolve_switch_target(targets, known_val as u128);
                        if next != base + expected {
                            return false;
                        }
                        return true;
                    }
                }

                // Try to infer the discriminant from a comparison source
                // (e.g. `_X = Ne(ptr, 0)`) when we know whether `ptr` is null.
                if let Some(discr_local) = discr_local
                    && let Some(info) = self.block_info.get(cur)
                    && let Some(cmp) = info.comparison_sources.get(&discr_local)
                    && matches!(cmp.op, BinOp::Ne | BinOp::Eq)
                {
                    let is_ne = matches!(cmp.op, BinOp::Ne);
                    let pointer_is_nonnull =
                        self.local_is_known_nonnull(constraints, cmp.lhs_local);
                    let pointer_is_null = self.local_is_known_null(constraints, cmp.lhs_local);
                    if pointer_is_nonnull {
                        let expected_val = if is_ne { 1 } else { 0 };
                        let expected = resolve_switch_target(targets, expected_val);
                        let val = expected_val as usize;
                        constraints.insert(discr_local, val);
                        if let Some(local) = constraint_local {
                            constraints.insert(local, val);
                        }
                        if next != base + expected {
                            return false;
                        }
                        return true;
                    }
                    if pointer_is_null {
                        let expected_val = if is_ne { 0 } else { 1 };
                        let expected = resolve_switch_target(targets, expected_val);
                        let val = expected_val as usize;
                        constraints.insert(discr_local, val);
                        if let Some(local) = constraint_local {
                            constraints.insert(local, val);
                        }
                        if next != base + expected {
                            return false;
                        }
                        return true;
                    }

                    // General Eq/Ne integer comparison: resolve both operands
                    // and prune the infeasible branch when both are known.
                    let is_eq = matches!(cmp.op, BinOp::Eq);
                    let lhs_val = self.resolve_local_value(cmp.lhs_local, constraints);
                    let rhs_val = if cmp.rhs_is_constant {
                        Some(cmp.rhs_local)
                    } else {
                        self.resolve_local_value(cmp.rhs_local, constraints)
                    };
                    if let (Some(lhs), Some(rhs)) = (lhs_val, rhs_val) {
                        let val = if is_eq {
                            if lhs == rhs { 1 } else { 0 }
                        } else {
                            if lhs != rhs { 1 } else { 0 }
                        };
                        let expected = resolve_switch_target(targets, val as u128);
                        if let Some(local) = constraint_local {
                            constraints.insert(local, val);
                        }
                        if next != base + expected {
                            return false;
                        }
                        return true;
                    }
                }

                // Try to resolve a boolean comparison with concrete-value
                // reasoning (handles Lt/Le/Gt/Ge with fully known operands).
                // Only filter when the discriminant resolves to a definite value
                // from a comparison with BOTH operands as known constants
                // (not derived via increments, which may be imprecise across
                // SCC boundaries).
                if let Some(discr_local) = discr_local
                    && let Some(info) = self.block_info.get(cur)
                    && let Some(cmp) = info.comparison_sources.get(&discr_local)
                    && matches!(cmp.op, BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge)
                {
                    // Resolve LHS directly from constants (no increment chains)
                    let lhs_val = self.resolve_local_value_direct(cmp.lhs_local, constraints);
                    let rhs_val = if cmp.rhs_is_constant {
                        Some(cmp.rhs_local)
                    } else {
                        self.resolve_local_value_direct(cmp.rhs_local, constraints)
                    };
                    if let (Some(lhs), Some(rhs)) = (lhs_val, rhs_val) {
                        let val = match cmp.op {
                            BinOp::Lt => {
                                if lhs < rhs {
                                    1
                                } else {
                                    0
                                }
                            }
                            BinOp::Le => {
                                if lhs <= rhs {
                                    1
                                } else {
                                    0
                                }
                            }
                            BinOp::Gt => {
                                if lhs > rhs {
                                    1
                                } else {
                                    0
                                }
                            }
                            BinOp::Ge => {
                                if lhs >= rhs {
                                    1
                                } else {
                                    0
                                }
                            }
                            _ => unreachable!(),
                        };
                        let expected = resolve_switch_target(targets, val as u128);
                        if let Some(local) = constraint_local {
                            constraints.insert(local, val);
                        }
                        if next != base + expected {
                            return false;
                        }
                        return true;
                    }
                }

                // No prior constraint — conservatively allow any valid target
                // and record the newly learned constraint from the taken branch.
                if next == targets.otherwise().as_usize() {
                    if let Some(local) = constraint_local {
                        if let Some(num_variants) =
                            self.get_variant_count(local, self.cfg.block(cur).def_id)
                        {
                            let all_covered = (0..num_variants)
                                .all(|v| targets.iter().any(|(tv, _)| tv == v as u128));
                            if all_covered {
                                return false;
                            }
                        }
                    }
                }

                self.learn_constraint_with_backprop(
                    cur,
                    constraint_local,
                    targets,
                    next,
                    constraints,
                );

                true
            }
            _ => true,
        }
    }

    /// After learning a constraint for a discriminant local, propagate the
    /// constraint backward through the copy chain so that source locals also
    /// receive the value. This prevents losing track of the constraint when
    /// the destination temporary is reassigned on loop back-edges.
    fn learn_constraint_with_backprop(
        &self,
        cur: usize,
        constraint_local: Option<usize>,
        targets: &SwitchTargets,
        next: usize,
        constraints: &mut FxHashMap<usize, usize>,
    ) {
        let Some(local) = constraint_local else {
            return;
        };
        let Some((val, _)) = targets.iter().find(|(_, bb)| bb.as_usize() == next) else {
            if let Some(inferred) = self.infer_otherwise_value(cur, targets, local) {
                constraints.insert(local, inferred);
                self.backprop_constraint(cur, local, inferred, constraints);
            }
            return;
        };
        let val = val as usize;
        constraints.insert(local, val);
        self.backprop_constraint(cur, local, val, constraints);
    }

    fn backprop_constraint(
        &self,
        cur: usize,
        local: usize,
        val: usize,
        constraints: &mut FxHashMap<usize, usize>,
    ) {
        let Some(info) = self.block_info.get(cur) else {
            return;
        };
        let mut current = local;
        while let Some(&src) = info.constraint_copies.get(&current) {
            if current == src {
                break;
            }
            constraints.insert(src, val);
            current = src;
        }
    }

    /// Recursively resolve a local's value through constraint copies,
    /// cast chains, field projections, and aggregate sources (global maps).
    /// Like `resolve_local_value` but does NOT follow increment chains.
    /// Used in conservative path filtering where we need high confidence.
    fn resolve_local_value_direct(
        &self,
        local: usize,
        constraints: &FxHashMap<usize, usize>,
    ) -> Option<usize> {
        let mut stack = vec![local];
        let mut seen = FxHashSet::default();
        while let Some(cur) = stack.pop() {
            if !seen.insert(cur) {
                continue;
            }
            if let Some(&val) = constraints.get(&cur) {
                if val != usize::MAX {
                    return Some(val);
                }
            }
            for info in &self.block_info {
                if let Some(&src) = info.constraint_copies.get(&cur) {
                    stack.push(src);
                }
                if let Some(&val) = info.constants.get(&cur) {
                    return Some(val);
                }
            }
            if let Some(&cast_src) = self.cast_chains.get(&cur) {
                stack.push(cast_src);
            }
        }
        None
    }

    fn resolve_local_value(
        &self,
        local: usize,
        constraints: &FxHashMap<usize, usize>,
    ) -> Option<usize> {
        let mut stack = vec![(local, 0isize)];
        let mut seen = FxHashSet::default();
        while let Some((cur, offset)) = stack.pop() {
            if !seen.insert(cur) {
                continue;
            }
            if let Some(&val) = constraints.get(&cur) {
                if val == usize::MAX {
                    // Sentinel for known-nonnull; not a concrete integer value.
                } else if offset >= 0 {
                    return Some(val + offset as usize);
                } else {
                    return val.checked_sub((-offset) as usize);
                }
            }
            // Follow constraint copies in any block (per-block metadata).
            for info in &self.block_info {
                if let Some(&src) = info.constraint_copies.get(&cur) {
                    stack.push((src, offset));
                }
                if let Some(&val) = info.constants.get(&cur) {
                    if offset >= 0 {
                        return Some(val + offset as usize);
                    } else {
                        return val.checked_sub((-offset) as usize);
                    }
                }
                // Follow increments: if cur = src + incr, the effective value
                // of cur is value_of(src) + incr + offset.
                if let Some(&(incr_src, incr_amt)) = info.increments.get(&cur) {
                    stack.push((incr_src, offset + incr_amt as isize));
                }
                // Follow remainder: cur = rem_src % rem_div.
                // Resolve rem_src recursively, compute remainder, then apply offset.
                if let Some(&(rem_src, rem_div)) = info.remainders.get(&cur) {
                    if let Some(src_val) = self.resolve_local_value(rem_src, constraints) {
                        let rem = src_val % rem_div;
                        let result = if offset >= 0 {
                            Some(rem + offset as usize)
                        } else {
                            rem.checked_sub((-offset) as usize)
                        };
                        if let Some(v) = result {
                            return Some(v);
                        }
                    }
                }
            }
            // Follow global cast chains.
            if let Some(&cast_src) = self.cast_chains.get(&cur) {
                stack.push((cast_src, offset));
            }
            // Follow field projection -> aggregate source.
            if let Some(&encoded) = self.field_projection_source.get(&cur) {
                if let Some((agg_local, field_idx)) = decode_aggregate_field(encoded) {
                    let key = encode_aggregate_field(agg_local, field_idx);
                    if let Some(&source) = self.aggregate_field_sources.get(&key) {
                        stack.push((source, offset));
                    }
                }
            }
        }
        None
    }

    /// For the "otherwise" branch of a `SwitchInt`, try to infer the single
    /// concrete value that the discriminant must have (because all other
    /// possible values are covered by explicit targets).
    fn infer_otherwise_value(
        &self,
        cur: usize,
        targets: &SwitchTargets,
        discr_local: usize,
    ) -> Option<usize> {
        let body = self.cfg.tcx.optimized_mir(self.cfg.block(cur).def_id);
        let def_id = self.cfg.block(cur).def_id;
        let original = discr_local - self.local_base_of(def_id);
        let mut discr_ty = body.local_decls[Local::from_usize(original)].ty;
        while let TyKind::Ref(_, inner, _) | TyKind::RawPtr(inner, _) = discr_ty.kind() {
            discr_ty = *inner;
        }

        let possible_values: Vec<usize> = match discr_ty.kind() {
            TyKind::Bool => vec![0, 1],
            TyKind::Adt(adt_def, _) if adt_def.is_enum() => (0..adt_def.variants().len()).collect(),
            _ => return None,
        };

        let explicit_values: FxHashSet<usize> = targets.iter().map(|(v, _)| v as usize).collect();
        let remaining: Vec<usize> = possible_values
            .into_iter()
            .filter(|v| !explicit_values.contains(v))
            .collect();

        if remaining.len() == 1 {
            Some(remaining[0])
        } else {
            None
        }
    }

    /// Check whether `next` is an unwind target reachable from `cur` via a
    /// call or drop terminator (may not be recorded as a normal CFG successor).
    fn is_unwind_target(&self, cur: usize, next: usize) -> bool {
        let Some(terminator) = self.cfg.terminator(cur) else {
            return false;
        };

        let unwind = match &terminator.kind {
            TerminatorKind::Call { unwind, .. }
            | TerminatorKind::Drop { unwind, .. }
            | TerminatorKind::Assert { unwind, .. } => unwind,
            _ => return false,
        };

        if let UnwindAction::Cleanup(target) = unwind {
            let base = cur - self.cfg.block(cur).local_index;
            return base + target.as_usize() == next;
        }
        false
    }

    /// Return true if `local` is known to be a non-null pointer.
    fn local_is_known_nonnull(&self, constraints: &FxHashMap<usize, usize>, local: usize) -> bool {
        let Some(&val) = constraints.get(&local) else {
            return false;
        };
        val > 0
    }

    /// Return true if `local` is known to be a null pointer.
    fn local_is_known_null(&self, constraints: &FxHashMap<usize, usize>, local: usize) -> bool {
        let Some(&val) = constraints.get(&local) else {
            return false;
        };
        val == 0
    }

    /// Populate the `child_sccs` field for a given SCC entry block, then
    /// recurse into those child SCCs. Called eagerly from `find_scc()` so
    /// that enumeration can be purely read-only on the graph.
    fn populate_child_sccs(&mut self, enter: usize) {
        let nodes: Vec<usize> = self.cfg.block(enter).scc.nodes.iter().cloned().collect();
        let mut child_enters = Vec::new();
        let mut seen = FxHashSet::default();

        for node in nodes {
            if let Some(block) = self.cfg.blocks.get(node) {
                let node_enter = block.scc.enter;
                let non_trivial = !block.scc.nodes.is_empty();
                if node_enter != enter && non_trivial && seen.insert(node_enter) {
                    child_enters.push(node_enter);
                }
            }
        }

        self.cfg.block_mut(enter).scc.child_sccs = child_enters;

        let child_count = self.cfg.block(enter).scc.child_sccs.len();
        for i in 0..child_count {
            let child_enter = self.cfg.block(enter).scc.child_sccs[i];
            self.populate_child_sccs(child_enter);
        }
    }

    fn populate_all_child_sccs(&mut self) {
        let mut visited = FxHashSet::default();
        let block_count = self.cfg.blocks.len();
        for i in 0..block_count {
            let scc = &self.cfg.block(i).scc;
            let enter = scc.enter;
            if scc.nodes.is_empty() || !visited.insert(enter) {
                continue;
            }
            self.populate_child_sccs(enter);
        }
    }
}

/// Hash of the constraint state accumulated along a path prefix.
///
/// Computed by walking the prefix, collecting `(local → constant_value)`
/// bindings from each block's [`BlockConstantInfo`], sorting them, and
/// hashing the result.  Used by [`PathEnumerator::visited_sccs`] to
/// skip redundant re-entries into the same SCC with the same state.
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, Default)]
pub struct ConstraintHash(u64);

impl ConstraintHash {
    fn from_path(path: &[usize], graph: &PathGraph<'_>) -> Self {
        let mut hasher = DefaultHasher::new();
        let mut constraints: FxHashMap<usize, usize> = FxHashMap::default();

        for &block in path.iter() {
            if let Some(info) = graph.block_info.get(block) {
                for local in &info.assigned_locals {
                    if let Some(&src) = info.constraint_copies.get(local) {
                        if let Some(&src_val) = constraints.get(&src) {
                            constraints.insert(*local, src_val);
                            continue;
                        }
                        if let Some(&dst_val) = constraints.get(local) {
                            constraints.insert(src, dst_val);
                            constraints.insert(*local, dst_val);
                            continue;
                        }
                    }
                    if let Some(&val) = info.constants.get(local) {
                        constraints.insert(*local, val);
                        continue;
                    }
                    constraints.remove(local);
                }
            }
        }

        let mut entries: Vec<(usize, usize)> = constraints.into_iter().collect();
        entries.sort();
        entries.hash(&mut hasher);
        ConstraintHash(hasher.finish())
    }
}

/// Key for [`PathEnumerator::scc_paths`] and [`PathEnumerator::visited_sccs`] and [`PathEnumerator::visited_sccs`]:
/// which SCC entry block, with what constraint state, and how many
/// additional postfix repeats are allowed.
///
/// In `scc_paths` the `constraint` field is unused (cache keyed by
/// `entry` + `repeat`); in `visited_sccs` the `repeat` field is
/// unused (deduplicated by `entry` + `constraint`).
#[derive(Debug, Clone, Hash, PartialEq, Eq)]
pub struct SccKey {
    pub entry: usize,
    pub repeat: usize,
    pub constraint: ConstraintHash,
}

/// Builds a [`PathTree`] by depth-first enumeration of whole-CFG paths.
///
/// The enumerator holds a `&PathGraph` (which must have `find_scc()` called
/// beforehand) and two caches:
///
/// The **constraint hash** used by `visited_sccs` is a
/// [`ConstraintHash`]: it walks the current path prefix, accumulates
/// `(local → constant_value)` bindings from each block's
/// [`BlockConstantInfo`], sorts them, and hashes the result.  Different
/// constraint states (e.g. a loop variable changing from `true` to
/// `false`) produce different hashes.
///
/// 1. `scc_paths` — maps [`SccKey`] to a list of acyclic paths through
///    that SCC.  Reused across repeated enumerations of the same function
///    with different repeat counts.
///
/// 2. `visited_sccs` — set of [`SccKey`] entries already explored
///    (matched by `entry` + `constraint`, ignoring `repeat`).
///    When the same SCC is reached with the same constraint state, its
///    sub-paths are identical, so the re-entry is skipped.
///
/// Constraint-based filtering runs incrementally during DFS via
/// [`PathGraph::check_transition`], so only feasible paths are inserted
/// into the resulting tree.
pub struct PathEnumerator<'g, 'tcx> {
    graph: &'g PathGraph<'tcx>,
    scc_paths: FxHashMap<SccKey, Vec<SccPath>>,
    visited_sccs: FxHashSet<SccKey>,
}

impl<'g, 'tcx> PathEnumerator<'g, 'tcx> {
    pub fn new(graph: &'g PathGraph<'tcx>) -> Self {
        PathEnumerator {
            graph,
            scc_paths: FxHashMap::default(),
            visited_sccs: FxHashSet::default(),
        }
    }

    /// Enumerate all whole-CFG paths, pruning infeasible transitions via
    /// incremental constraint-based filtering during DFS.
    ///
    /// SCC regions are flattened into a bounded set of acyclic paths.
    pub fn enumerate_paths(&mut self) -> PathTree {
        self.enumerate_paths_repeat(0)
    }

    /// Enumerate whole-CFG paths allowing each SCC postfix segment to repeat
    /// up to `postfix_repeat` additional times. `postfix_repeat = 0` gives
    /// the same result as `enumerate_paths`.
    ///
    /// Enumeration stops once [`crate::limit::path_limit`] paths are
    /// collected and the tree is marked truncated.
    pub fn enumerate_paths_repeat(&mut self, postfix_repeat: usize) -> PathTree {
        let mut tree = PathTree::new();

        if self.graph.cfg.blocks.is_empty() {
            return tree;
        }

        self.collect_whole_cfg_paths(
            0,
            &mut vec![0],
            &mut tree,
            0,
            postfix_repeat,
            &FxHashMap::default(),
        );

        tree
    }

    /// Enumerate all acyclic paths through `scc` starting at `start`,
    /// allowing each postfix segment to repeat up to `postfix_repeat`
    /// additional times.
    ///
    /// Results are cached per `(def_id, scc_enter, postfix_repeat)`.
    pub fn find_scc_paths_repeat(
        &mut self,
        start: usize,
        scc: &SccInfo,
        postfix_repeat: usize,
    ) -> Vec<SccPath> {
        let cache_key = SccKey {
            entry: scc.enter,
            repeat: postfix_repeat,
            constraint: ConstraintHash::default(),
        };
        if let Some(cached) = self.scc_paths.get(&cache_key) {
            return cached.clone();
        }

        let mut out = Vec::new();
        let mut seen: FxHashSet<Vec<usize>> = FxHashSet::default();
        let mut path = vec![start];
        let mut segment_counts = FxHashMap::default();

        self.dfs_scc_tree(
            scc,
            start,
            &mut path,
            &mut segment_counts,
            postfix_repeat,
            &mut out,
            &mut seen,
            0,
        );

        if self.scc_paths.len() >= SCC_PATH_CACHE_LIMIT {
            self.scc_paths.clear();
        }
        self.scc_paths.insert(cache_key, out.clone());

        out
    }

    /// Recursive DFS through one level of the SCC tree.
    ///
    /// Enumerates structurally possible paths through the SCC to exit points.
    /// No constraint tracking — `check_postfix_segment` prunes repeated
    /// loop-body segments purely by block-id sequence.
    ///
    /// When `postfix_repeat > 0`, allows the same postfix segment to repeat
    /// up to `postfix_repeat` additional times beyond the first occurrence.
    ///
    /// Child SCC paths are pre-enumerated via `find_scc_paths_repeat` and treated as
    /// atomic building blocks (no recursive descent into child SCC internals).
    #[allow(clippy::too_many_arguments)]
    fn dfs_scc_tree(
        &mut self,
        scc: &SccInfo,
        cur: usize,
        path: &mut Vec<usize>,
        segment_counts: &mut FxHashMap<Vec<usize>, usize>,
        postfix_repeat: usize,
        out: &mut Vec<SccPath>,
        seen_paths: &mut FxHashSet<Vec<usize>>,
        depth: usize,
    ) {
        if depth > SCC_MAX_DEPTH {
            return;
        }
        if out.len() >= SCC_MAX_SEEN_PATHS {
            return;
        }
        if path.len() > SCC_MAX_PATH_LEN {
            return;
        }
        if cur != scc.enter && !scc.nodes.contains(&cur) {
            return;
        }

        if cur == scc.enter && path.len() > 1 {
            if !check_postfix_segment(path, scc.enter, segment_counts, postfix_repeat) {
                if (postfix_repeat > 0 || segment_counts.len() > 1)
                    && scc.exits.iter().any(|e| e.exit == cur)
                {
                    self.record_unique_path(path, scc, out, seen_paths);
                }
                return;
            }
        }

        if scc.exits.iter().any(|e| e.exit == cur) {
            self.record_unique_path(path, scc, out, seen_paths);
        }

        let is_child = scc.child_sccs.contains(&cur);

        if is_child {
            let ctx = self.constraint_context(path);
            if !self.visited_sccs.insert(SccKey {
                entry: cur,
                repeat: 0,
                constraint: ctx,
            }) {
                return;
            }

            let child_scc = self.graph.cfg_block(cur).scc.clone();
            let child_paths = self.find_scc_paths_repeat(cur, &child_scc, postfix_repeat);

            for child_path in &child_paths {
                let orig_len = path.len();
                if child_path.blocks.len() > 1 {
                    path.extend(&child_path.blocks[1..]);
                }

                let mut branch_counts = segment_counts.clone();
                for &next in &child_path.exit_successors {
                    path.push(next);
                    self.dfs_scc_tree(
                        scc,
                        next,
                        path,
                        &mut branch_counts,
                        postfix_repeat,
                        out,
                        seen_paths,
                        depth + 1,
                    );
                    path.pop();
                }
                path.truncate(orig_len);
            }
            return;
        }

        let successors: Vec<usize> = self.graph.cfg.block(cur).next.iter().copied().collect();
        let saved_counts = segment_counts.clone();
        for next in successors {
            if next != scc.enter && !scc.nodes.contains(&next) {
                self.record_unique_path(path, scc, out, seen_paths);
                continue;
            }
            let mut branch_counts = saved_counts.clone();
            path.push(next);
            self.dfs_scc_tree(
                scc,
                next,
                path,
                &mut branch_counts,
                postfix_repeat,
                out,
                seen_paths,
                depth + 1,
            );
            path.pop();
        }
    }

    /// Build a [`ConstraintHash`] from the constraint state along `path`.
    fn constraint_context(&self, path: &[usize]) -> ConstraintHash {
        ConstraintHash::from_path(path, self.graph)
    }

    /// Depth-first enumeration of all CFG paths from `current` to a terminator.
    ///
    /// SCC nodes are flattened via `find_scc_paths_repeat`; non-SCC blocks are followed
    /// one by one.  No cycle detection is needed because the post-SCC CFG is a DAG.
    /// Constraints are maintained incrementally — each transition is checked
    /// via `PathGraph::check_transition` before recursing, and infeasible
    /// branches are pruned early.
    fn collect_whole_cfg_paths(
        &mut self,
        current: usize,
        path: &mut Vec<usize>,
        tree: &mut PathTree,
        depth: usize,
        postfix_repeat: usize,
        constraints: &FxHashMap<usize, usize>,
    ) {
        if current >= self.graph.cfg.blocks.len() {
            return;
        }
        if depth > WHOLE_CFG_PATH_DEPTH_LIMIT
            || tree.len() >= crate::limit::path_limit()
        {
            tree.mark_truncated();
            return;
        }

        let scc_info = self.graph.cfg_block(current).scc.clone();
        let is_scc = current == scc_info.enter && !scc_info.nodes.is_empty();
        if is_scc {
            let scc = self.sort_scc_tree(&scc_info);
            let segments = self.find_scc_paths_repeat(current, &scc, postfix_repeat);

            if segments.is_empty() {
                tree.insert(path);
                return;
            }

            for seg in segments {
                if tree.len() >= crate::limit::path_limit() {
                    tree.mark_truncated();
                    break;
                }

                let orig_len = path.len();
                let mut seg_constraints = constraints.clone();
                let mut reachable = true;

                if seg.blocks.len() > 1 {
                    for i in 0..seg.blocks.len() - 1 {
                        if !self.graph.check_transition(
                            seg.blocks[i],
                            seg.blocks[i + 1],
                            &mut seg_constraints,
                        ) {
                            reachable = false;
                            break;
                        }
                    }
                    if reachable {
                        path.extend_from_slice(&seg.blocks[1..]);
                    }
                }

                if reachable {
                    if seg.exit_successors.is_empty() {
                        tree.insert(path);
                    } else {
                        for &next in &seg.exit_successors {
                            let mut next_constraints = seg_constraints.clone();
                            let last = *path.last().unwrap();
                            if self
                                .graph
                                .check_transition(last, next, &mut next_constraints)
                            {
                                path.push(next);
                                self.collect_whole_cfg_paths(
                                    next,
                                    path,
                                    tree,
                                    depth + 1,
                                    postfix_repeat,
                                    &next_constraints,
                                );
                                path.pop();
                            }
                        }
                    }
                }

                path.truncate(orig_len);
            }
            return;
        }

        // Non-SCC block: follow CFG successors.
        let successors: Vec<usize> = self.graph.cfg_block(current).next.iter().copied().collect();
        if successors.is_empty() {
            tree.insert(path);
            return;
        }

        for next in successors {
            let mut next_constraints = constraints.clone();
            if self
                .graph
                .check_transition(current, next, &mut next_constraints)
            {
                path.push(next);
                self.collect_whole_cfg_paths(
                    next,
                    path,
                    tree,
                    depth + 1,
                    postfix_repeat,
                    &next_constraints,
                );
                path.pop();
            }
        }
    }

    fn sort_scc_tree(&self, scc: &SccInfo) -> SccInfo {
        self.graph.cfg_block(scc.enter).scc.clone()
    }

    fn record_unique_path(
        &self,
        path: &[usize],
        scc: &SccInfo,
        out: &mut Vec<SccPath>,
        seen_paths: &mut FxHashSet<Vec<usize>>,
    ) {
        if !seen_paths.insert(path.to_vec()) {
            return;
        }
        let exit_successors = self.compute_exit_successors(path, scc);
        out.push(SccPath {
            blocks: path.to_vec(),
            exit_successors,
        });
    }

    fn compute_exit_successors(&self, path: &[usize], scc: &SccInfo) -> Vec<usize> {
        let Some(&last) = path.last() else {
            return vec![];
        };
        scc.exits
            .iter()
            .filter(|e| e.exit == last)
            .map(|e| e.to)
            .filter(|&n| {
                !scc.child_sccs
                    .contains(&self.graph.cfg.block(n).scc.enter())
            })
            .collect()
    }
}

/// Resolve a concrete discriminant value to the corresponding `SwitchInt`
/// successor block index.
fn resolve_switch_target(targets: &SwitchTargets, val: u128) -> usize {
    targets
        .iter()
        .find(|(v, _)| *v == val)
        .map(|(_, bb)| bb.as_usize())
        .unwrap_or_else(|| targets.otherwise().as_usize())
}