rsleigh-decompile 0.4.1

//! Taint-flow CVE explorer (SMT M1).
//!
//! Configures attacker-controlled `Source` APIs and dangerous `Sink`
//! APIs, walks straight-line SSA paths from a Source's tainted output
//! to a Sink's watched argument, and asks Z3 whether attacker-supplied
//! bytes can drive the watched value into a CVE-class state (over-long
//! buffer, format-string char, command separator, etc.).
//!
//! This module owns the spec tables, call-name resolution, and the
//! straight-line SSA path collector. The Z3-driven SAT prover lands
//! in commit 4 per
//! `.opt/campaigns/smt-backend-implementation-plan.md`.

use std::collections::HashMap;

use crate::ir::{CallTarget, SsaCfg, SsaTerminator, Stmt, VarId};

/// One slot in the platform calling convention. M1 only needs to
/// describe the slots used by the source/sink configurations below;
/// fuller ABI coverage (variadic, return registers, x87 stack, NEON)
/// is deferred.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum AbiSlot {
    /// Argument in register N (zero-indexed, e.g. RDI=0 on x86-64
    /// SystemV, X0=0 on AArch64 AAPCS, $a0=0 on MIPS o32).
    Arg(u8),
    /// Return value (typically RAX/X0/v0).
    Ret,
}

/// What kind of CVE-class violation the sink exposes.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SinkKind {
    /// `dst` is a stack-resident buffer; tainted source overflowing
    /// it is a stack BOF (strcpy/strcat/sprintf/gets-class).
    StackBuffer,
    /// `arg0` is a printf-family format string — `%n`/`%s`/`%x`
    /// substrings produce read/write primitives.
    FormatArg,
    /// Single string argument runs through a shell (system/popen)
    /// or exec*() — `;`/`&&`/`|` enables command injection.
    Command,
    /// Length operand of a bounded copy (memcpy/strncpy/memmove);
    /// SAT when the tainted length can exceed the dst capacity.
    LengthArg,
}

/// Attacker-controlled API. The function returns or fills a buffer
/// whose contents are byte-for-byte controlled.
#[derive(Debug, Clone, Copy)]
pub struct SourceSpec {
    /// libc / kernel-style API name, e.g. `"recv"`, `"read"`, `"argv"`.
    /// `"argv"` is treated specially — it isn't a function call,
    /// it's the second argument to `main`, and the path collector
    /// will need to recognise that.
    pub name: &'static str,
    /// The slot whose contents become tainted when the call returns.
    /// `Ret` for `gets`-class returns; `Arg(N)` for fill-buffer APIs
    /// like `recv(sock, BUF, len, flags)` where N=1.
    pub tainted: AbiSlot,
}

/// Dangerous API. Tainted data reaching `watched` produces a
/// CVE-class outcome of the configured `kind`.
#[derive(Debug, Clone, Copy)]
pub struct SinkSpec {
    pub name: &'static str,
    /// The argument slot whose taint we test for the SAT proof.
    pub watched: AbiSlot,
    pub kind: SinkKind,
}

/// Default attacker-controlled APIs. M1 covers the canonical libc
/// network/IO surface plus `argv`. Aliases (e.g. checked wrappers
/// `__recv_chk`) are deferred.
pub const DEFAULT_SOURCES: &[SourceSpec] = &[
    SourceSpec { name: "recv",       tainted: AbiSlot::Arg(1) },
    SourceSpec { name: "recvfrom",   tainted: AbiSlot::Arg(1) },
    SourceSpec { name: "recvmsg",    tainted: AbiSlot::Arg(1) },
    SourceSpec { name: "read",       tainted: AbiSlot::Arg(1) },
    SourceSpec { name: "fread",      tainted: AbiSlot::Arg(0) },
    SourceSpec { name: "fgets",      tainted: AbiSlot::Arg(0) },
    SourceSpec { name: "gets",       tainted: AbiSlot::Arg(0) },
    SourceSpec { name: "scanf",      tainted: AbiSlot::Arg(1) },
    SourceSpec { name: "sscanf",     tainted: AbiSlot::Arg(2) },
    SourceSpec { name: "fscanf",     tainted: AbiSlot::Arg(2) },
    SourceSpec { name: "getenv",     tainted: AbiSlot::Ret    },
    // `argv` is a marker — the path collector recognises it as
    // "second arg of main" rather than a function call.
    SourceSpec { name: "argv",       tainted: AbiSlot::Arg(1) },
];

/// Default dangerous APIs. M1 covers the canonical libc CVE class
/// surface. Bounded-copy primitives whose length argument is the
/// CVE primitive use `LengthArg`; everything else watches the
/// primary string slot.
pub const DEFAULT_SINKS: &[SinkSpec] = &[
    SinkSpec { name: "strcpy",  watched: AbiSlot::Arg(1), kind: SinkKind::StackBuffer },
    SinkSpec { name: "strcat",  watched: AbiSlot::Arg(1), kind: SinkKind::StackBuffer },
    SinkSpec { name: "sprintf", watched: AbiSlot::Arg(1), kind: SinkKind::FormatArg   },
    SinkSpec { name: "vsprintf",watched: AbiSlot::Arg(1), kind: SinkKind::FormatArg   },
    SinkSpec { name: "printf",  watched: AbiSlot::Arg(0), kind: SinkKind::FormatArg   },
    SinkSpec { name: "fprintf", watched: AbiSlot::Arg(1), kind: SinkKind::FormatArg   },
    SinkSpec { name: "memcpy",  watched: AbiSlot::Arg(2), kind: SinkKind::LengthArg   },
    SinkSpec { name: "memmove", watched: AbiSlot::Arg(2), kind: SinkKind::LengthArg   },
    SinkSpec { name: "strncpy", watched: AbiSlot::Arg(2), kind: SinkKind::LengthArg   },
    SinkSpec { name: "strncat", watched: AbiSlot::Arg(2), kind: SinkKind::LengthArg   },
    SinkSpec { name: "system",  watched: AbiSlot::Arg(0), kind: SinkKind::Command     },
    SinkSpec { name: "popen",   watched: AbiSlot::Arg(0), kind: SinkKind::Command     },
    SinkSpec { name: "execve",  watched: AbiSlot::Arg(0), kind: SinkKind::Command     },
    SinkSpec { name: "execlp",  watched: AbiSlot::Arg(0), kind: SinkKind::Command     },
    SinkSpec { name: "execvp",  watched: AbiSlot::Arg(0), kind: SinkKind::Command     },
];

/// Resolve a call-target address against the import map. Returns
/// `Some(SpecRef)` when the target matches one of the configured
/// sources or sinks.
///
/// Name normalisation: ELF/Mach-O often expose stub names with a
/// leading `_` or `__` and PLT names with an `@plt` suffix; strip
/// both before matching. Demangled C++ names that happen to overlap
/// with libc identifiers are out of scope (M1 is libc-targeted).
pub fn resolve_call(
    target_addr: u64,
    imports: &HashMap<u64, String>,
) -> Option<SpecRef> {
    let raw = imports.get(&target_addr)?;
    let normalised = normalise_name(raw);
    if let Some(spec) = DEFAULT_SOURCES.iter().find(|s| s.name == normalised) {
        return Some(SpecRef::Source(*spec));
    }
    if let Some(spec) = DEFAULT_SINKS.iter().find(|s| s.name == normalised) {
        return Some(SpecRef::Sink(*spec));
    }
    None
}

/// Result of `resolve_call`. Either a Source whose return/output
/// taints memory, or a Sink whose watched arg we follow.
#[derive(Debug, Clone, Copy)]
pub enum SpecRef {
    Source(SourceSpec),
    Sink(SinkSpec),
}

fn normalise_name(raw: &str) -> &str {
    // Strip a `@plt`/`@@VERSION` suffix.
    let stripped = raw.split('@').next().unwrap_or(raw);
    // Strip up to two leading underscores (Mach-O stubs commonly
    // expose `_recv`, glibc-internal names sometimes appear with
    // `__recv` for the *_chk family — we don't include checked
    // variants in M1, so this just unwraps the canonical name).
    stripped
        .trim_start_matches('_')
        .trim_start_matches('_')
}

/// SAT-as-CVE-proof outcome for one `TaintPath`. Produced by
/// `solve` (gated on `smt` feature).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum SmtFinding {
    /// Z3 found a symbolic input that drives the sink's watched arg
    /// into a CVE-class state. The model is exposed as
    /// `(input_byte_offset, value)` pairs.
    Reachable { input_bytes: Vec<(usize, u8)> },
    /// Solver proved no input drives the violation under the path's
    /// constraints — false-positive cull.
    NotReachable,
    /// Lineage check or sink-kind modelling is out of v0 scope. The
    /// reason string is shown to the analyst so the gap is auditable.
    Unsupported(&'static str),
}

/// Reasons the v0 path collector rejected an SSA function.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum PathRejection {
    /// Walk reached a non-Call terminator (CBranch, Branch, Return,
    /// Indirect, Fallthrough). M1 forbids multi-block paths.
    UnsupportedTerminator(&'static str),
    /// Entry block contains a Phi-introducing assignment. v0 cannot
    /// reason across phi joins.
    PhiInPath,
    /// Entry block makes an indirect call before a sink is reached.
    IndirectCall,
    /// Walk completed, no Sink was encountered. Not a hard error —
    /// caller may treat this as "function does nothing CVE-class".
    NoSinkFound,
}

/// One event in the linear SSA walk: assignments, stores, calls.
/// Calls are classified up front against the import map so the
/// downstream SAT prover doesn't repeat the lookup.
#[derive(Debug, Clone)]
pub struct TaintEvent<'a> {
    pub stmt_index: usize,
    pub kind: TaintEventKind<'a>,
}

#[derive(Debug, Clone)]
pub enum TaintEventKind<'a> {
    Assign(VarId),
    Store { addr: VarId, val: VarId },
    SourceCall {
        spec: &'a SourceSpec,
        args: Vec<VarId>,
        out: Option<VarId>,
    },
    SinkCall {
        spec: &'a SinkSpec,
        args: Vec<VarId>,
        out: Option<VarId>,
    },
    OtherCall {
        target_addr: Option<u64>,
        args: Vec<VarId>,
        out: Option<VarId>,
    },
}

/// One CBranch decision encountered while walking from entry to a
/// Source→Sink pair. `taken == true` means the path took the
/// CBranch's `taken` arm; `false` is the fallthrough.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct BranchDecision {
    pub block_addr: u64,
    pub cond: VarId,
    pub taken: bool,
}

/// One Source -> Sink pair found by `collect_paths`. The SAT prover
/// takes the path and asks Z3 whether tainted input from `source`
/// can force the `sink`'s watched arg into a CVE-class state.
///
/// `branch_decisions` records the CBranch arms taken between entry
/// and the sink invocation. v0 paths always have an empty list
/// (linear walk only); v1 paths can include up to MAX_BRANCH_DEPTH
/// decisions.
#[derive(Debug, Clone)]
pub struct TaintPath<'a> {
    pub source: &'a SourceSpec,
    pub source_event: usize,
    pub sink: &'a SinkSpec,
    pub sink_event: usize,
    pub events: Vec<TaintEvent<'a>>,
    pub branch_decisions: Vec<BranchDecision>,
}

/// Maximum number of CBranch arms followed from entry to any path
/// before the walker bails. Keeps worklist size bounded — at depth
/// k the worst case is 2^k explored arms. k=4 → 16 paths max per
/// function, which is plenty for the M2-class targets v1 chases
/// without blowing up on giant dispatch tables.
pub const MAX_BRANCH_DEPTH: u32 = 4;

/// One in-progress walk state in the v1 collector's worklist.
struct WalkState<'a> {
    current: crate::ir::BlockId,
    events: Vec<TaintEvent<'a>>,
    visited: std::collections::HashSet<crate::ir::BlockId>,
    branch_decisions: Vec<BranchDecision>,
}

/// Walk every CFG path from the entry block to a Source→Sink pair,
/// k-bounded at `MAX_BRANCH_DEPTH` CBranch arms. Returns the list
/// of paths surfaced, or `PathRejection` if no walk produces a
/// usable path.
///
/// v0 (linear-fallthrough only) is the trivial case: entry block
/// has no CBranch reachable, the worklist degenerates to a single
/// walk identical to v0 collection. v1 adds CBranch exploration:
/// when a walk hits a CBranch, both arms get queued as separate
/// states, each with `branch_decisions` extended.
///
/// Rejected paths (loop back-edges, indirect calls, Phi nodes,
/// depth limit) are dropped; if no successful path remains, the
/// most-specific rejection reason is returned.
///
/// Loop guard: `visited` BlockId set is per-state, not global —
/// two distinct paths through the same block via different arms
/// are both legal. A revisit within the SAME walk aborts that walk.
pub fn collect_paths<'a>(
    ssa: &'a SsaCfg,
    imports: &HashMap<u64, String>,
) -> Result<Vec<TaintPath<'a>>, PathRejection> {
    let initial = WalkState {
        current: ssa.entry,
        events: Vec::new(),
        visited: std::collections::HashSet::new(),
        branch_decisions: Vec::new(),
    };
    let mut worklist: Vec<WalkState<'a>> = vec![initial];
    let mut completed: Vec<WalkState<'a>> = Vec::new();
    let mut last_reject: Option<PathRejection> = None;

    while let Some(mut state) = worklist.pop() {
        if state.branch_decisions.len() as u32 > MAX_BRANCH_DEPTH {
            last_reject = Some(PathRejection::UnsupportedTerminator("depth limit"));
            continue;
        }
        let mut keep_walking = true;
        while keep_walking {
            if !state.visited.insert(state.current) {
                last_reject = Some(PathRejection::UnsupportedTerminator("loop back-edge"));
                keep_walking = false;
                break;
            }
            let block = match ssa.blocks.iter().find(|b| b.id == state.current) {
                Some(b) => b,
                None => {
                    last_reject =
                        Some(PathRejection::UnsupportedTerminator("dangling block id"));
                    keep_walking = false;
                    break;
                }
            };

            let mut phi_or_indirect = false;
            for (idx, stmt) in block.stmts.iter().enumerate() {
                match stmt {
                    Stmt::Assign(v) => {
                        // Skip Phi assignments — v1 lineage walk
                        // can't propagate taint through them without
                        // per-path predecessor resolution. Recording
                        // them as Assign events is harmless when the
                        // sink doesn't depend on the Phi result, and
                        // saves the walker from rejecting any path
                        // that touches a real-world reconvergence
                        // point. Per-path Phi resolution is v2 work.
                        if matches!(
                            ssa.vars.get(v.0 as usize).map(|d| &d.expr),
                            Some(crate::ir::Expr::Phi(_))
                        ) {
                            continue;
                        }
                        state.events.push(TaintEvent {
                            stmt_index: idx,
                            kind: TaintEventKind::Assign(*v),
                        });
                    }
                    Stmt::Store { addr, val } => {
                        state.events.push(TaintEvent {
                            stmt_index: idx,
                            kind: TaintEventKind::Store {
                                addr: *addr,
                                val: *val,
                            },
                        });
                    }
                    Stmt::Call { target, args, out } => {
                        match classify_call(idx, target, args, *out, imports) {
                            Ok(ev) => state.events.push(ev),
                            Err(e) => {
                                last_reject = Some(e);
                                phi_or_indirect = true;
                                break;
                            }
                        }
                    }
                }
            }
            if phi_or_indirect {
                keep_walking = false;
                break;
            }

            let term_idx = block.stmts.len();
            match &block.terminator {
                SsaTerminator::Call {
                    target,
                    args,
                    out,
                    fallthrough,
                } => match classify_call(term_idx, target, args, *out, imports) {
                    Ok(ev) => {
                        state.events.push(ev);
                        state.current = *fallthrough;
                    }
                    Err(e) => {
                        last_reject = Some(e);
                        keep_walking = false;
                    }
                },
                SsaTerminator::Fallthrough(next) => {
                    state.current = *next;
                }
                SsaTerminator::Return(_) => {
                    completed.push(state);
                    keep_walking = false;
                    break;
                }
                SsaTerminator::Branch(next) => {
                    // Unconditional jump — walk through. Same loop
                    // guard via `visited` covers infinite-Branch
                    // loops. Original v0 break-on-Branch was a
                    // conservative bail; v1 just keeps walking.
                    state.current = *next;
                }
                SsaTerminator::CBranch {
                    cond,
                    taken,
                    fallthrough,
                } => {
                    // Spawn a copy on the fallthrough arm; we keep
                    // walking on the taken arm in this iteration.
                    if (state.branch_decisions.len() as u32) >= MAX_BRANCH_DEPTH {
                        last_reject =
                            Some(PathRejection::UnsupportedTerminator("depth limit"));
                        keep_walking = false;
                        break;
                    }
                    let block_addr = block.addr;
                    let mut alt = WalkState {
                        current: *fallthrough,
                        events: state.events.clone(),
                        visited: state.visited.clone(),
                        branch_decisions: state.branch_decisions.clone(),
                    };
                    alt.branch_decisions.push(BranchDecision {
                        block_addr,
                        cond: *cond,
                        taken: false,
                    });
                    worklist.push(alt);

                    state.current = *taken;
                    state.branch_decisions.push(BranchDecision {
                        block_addr,
                        cond: *cond,
                        taken: true,
                    });
                }
                SsaTerminator::Indirect(_) => {
                    last_reject =
                        Some(PathRejection::UnsupportedTerminator("Indirect"));
                    keep_walking = false;
                    break;
                }
            }
        }
    }

    // Pair each Source with the next Sink in each completed walk.
    let mut paths = Vec::new();
    for state in completed {
        let mut last_source: Option<(usize, &'a SourceSpec)> = None;
        for (i, ev) in state.events.iter().enumerate() {
            match &ev.kind {
                TaintEventKind::SourceCall { spec, .. } => {
                    last_source = Some((i, spec));
                }
                TaintEventKind::SinkCall { spec, .. } => {
                    if let Some((src_i, src_spec)) = last_source.take() {
                        paths.push(TaintPath {
                            source: src_spec,
                            source_event: src_i,
                            sink: spec,
                            sink_event: i,
                            events: state.events.clone(),
                            branch_decisions: state.branch_decisions.clone(),
                        });
                    }
                }
                _ => {}
            }
        }
    }

    if paths.is_empty() {
        return Err(last_reject.unwrap_or(PathRejection::NoSinkFound));
    }
    Ok(paths)
}

fn classify_call<'a>(
    stmt_index: usize,
    target: &CallTarget,
    args: &[VarId],
    out: Option<VarId>,
    imports: &HashMap<u64, String>,
) -> Result<TaintEvent<'a>, PathRejection> {
    let direct_addr = match target {
        CallTarget::Direct(a) => Some(*a),
        CallTarget::Indirect(_) => None,
    };
    let kind = match direct_addr.and_then(|a| resolve_call(a, imports)) {
        Some(SpecRef::Source(s)) => {
            // Find the matching SourceSpec from DEFAULT_SOURCES so
            // the lifetime ties to 'static (avoids cloning into the
            // event, keeps the spec table the single source of truth).
            let spec = DEFAULT_SOURCES
                .iter()
                .find(|sp| sp.name == s.name)
                .expect("resolve_call returned a SourceSpec not in DEFAULT_SOURCES");
            TaintEventKind::SourceCall { spec, args: args.to_vec(), out }
        }
        Some(SpecRef::Sink(s)) => {
            let spec = DEFAULT_SINKS
                .iter()
                .find(|sp| sp.name == s.name)
                .expect("resolve_call returned a SinkSpec not in DEFAULT_SINKS");
            TaintEventKind::SinkCall { spec, args: args.to_vec(), out }
        }
        None => {
            if direct_addr.is_none() {
                return Err(PathRejection::IndirectCall);
            }
            TaintEventKind::OtherCall {
                target_addr: direct_addr,
                args: args.to_vec(),
                out,
            }
        }
    };
    Ok(TaintEvent { stmt_index, kind })
}

/// Map of last-Store addresses (as Varnodes) to the VarId of the
/// stored value. Built once per `solve` invocation by walking the
/// path's events. Used by `varid_lineage_eq` to follow Load(addr)
/// back to the value most recently stored at that addr.
type MemMap = HashMap<pcode_ir::Varnode, VarId>;

fn build_mem_map(events: &[TaintEvent<'_>], vars: &[crate::ir::VarDef]) -> MemMap {
    let mut m = MemMap::new();
    for ev in events {
        if let TaintEventKind::Store { addr, val } = ev.kind {
            if let Some(addr_vn) = vars.get(addr.0 as usize).map(|d| d.varnode) {
                m.insert(addr_vn, val);
            }
        }
    }
    m
}

/// True if `a` and `b` share a common logical location after
/// following SSA `Var` chains AND a single layer of Store→Load
/// indirection through `mem`. Lifters split a buffer pointer into
/// many SSA versions across Store/Load round-trips; without the
/// memory map this lineage trace would miss every realistic flow.
fn varid_lineage_eq(
    a: VarId,
    b: VarId,
    vars: &[crate::ir::VarDef],
    mem: &MemMap,
) -> bool {
    if a == b {
        return true;
    }
    let chain_a = chain_varnodes(a, vars, mem);
    let chain_b = chain_varnodes(b, vars, mem);
    for vn_a in &chain_a {
        if chain_b.iter().any(|vn_b| vn_a == vn_b) {
            return true;
        }
    }
    false
}

/// Collect the set of Varnodes encountered while unwinding `start`
/// through `Expr::Var` chains and (one-step) Store→Load redirection
/// via `mem`. Bounded depth so cyclic IRs don't hang the v0 prover.
fn chain_varnodes(
    start: VarId,
    vars: &[crate::ir::VarDef],
    mem: &MemMap,
) -> Vec<pcode_ir::Varnode> {
    let mut out = Vec::new();
    let mut visited: std::collections::HashSet<u32> = std::collections::HashSet::new();
    let mut stack = vec![start];
    while let Some(current) = stack.pop() {
        if !visited.insert(current.0) {
            continue;
        }
        if visited.len() > 64 {
            break;
        }
        let Some(def) = vars.get(current.0 as usize) else {
            continue;
        };
        out.push(def.varnode);
        match &def.expr {
            crate::ir::Expr::Var(inner) => stack.push(*inner),
            crate::ir::Expr::Load(addr) => {
                if let Some(addr_vn) = vars.get(addr.0 as usize).map(|d| d.varnode) {
                    if let Some(stored) = mem.get(&addr_vn).copied() {
                        stack.push(stored);
                    }
                }
            }
            _ => {}
        }
    }
    out
}

/// v0 SAT prover: takes a `TaintPath` produced by `collect_paths`,
/// confirms the sink's watched VarId lineage descends from the
/// source's tainted slot, and asks Z3 whether a symbolic input can
/// satisfy the per-`SinkKind` violation constraint.
///
/// v0 simplifications (locked):
///   - 32-byte fresh symbolic input array; no flat memory model yet.
///   - No Load/Store/FieldAccess lowering inside the SSA cone.
///   - LengthArg sinks return `Unsupported` (modelling deferred).
///   - Lineage check is `Expr::Var` chain only — no BinOp/Phi taint.
#[cfg(feature = "smt")]
pub fn solve(path: &TaintPath, ssa: &crate::ir::SsaCfg) -> SmtFinding {
    use z3::ast::{Ast, BV};

    let source_event = &path.events[path.source_event];
    let sink_event = &path.events[path.sink_event];

    let source_var = match (&source_event.kind, path.source.tainted) {
        (TaintEventKind::SourceCall { args, .. }, AbiSlot::Arg(n)) => {
            args.get(n as usize).copied()
        }
        (TaintEventKind::SourceCall { out, .. }, AbiSlot::Ret) => *out,
        _ => None,
    };
    let sink_var = match (&sink_event.kind, path.sink.watched) {
        (TaintEventKind::SinkCall { args, .. }, AbiSlot::Arg(n)) => {
            args.get(n as usize).copied()
        }
        (TaintEventKind::SinkCall { out, .. }, AbiSlot::Ret) => *out,
        _ => None,
    };

    let (Some(src), Some(snk)) = (source_var, sink_var) else {
        return SmtFinding::Unsupported("source/sink slot missing");
    };
    let mem = build_mem_map(&path.events, &ssa.vars);
    if !varid_lineage_eq(snk, src, &ssa.vars, &mem) {
        return SmtFinding::NotReachable;
    }

    let z3_cfg = z3::Config::new();
    let ctx = z3::Context::new(&z3_cfg);
    let solver = z3::Solver::new(&ctx);

    const INPUT_LEN: usize = 32;
    let bytes: Vec<BV> = (0..INPUT_LEN)
        .map(|i| BV::new_const(&ctx, format!("in_{i}"), 8))
        .collect();

    match path.sink.kind {
        SinkKind::Command => {
            let mut acc = z3::ast::Bool::from_bool(&ctx, false);
            for b in &bytes {
                let semi = b._eq(&BV::from_u64(&ctx, b';' as u64, 8));
                let amp  = b._eq(&BV::from_u64(&ctx, b'&' as u64, 8));
                let pipe = b._eq(&BV::from_u64(&ctx, b'|' as u64, 8));
                let any = z3::ast::Bool::or(&ctx, &[&semi, &amp, &pipe]);
                acc = z3::ast::Bool::or(&ctx, &[&acc, &any]);
            }
            solver.assert(&acc);
        }
        SinkKind::FormatArg => {
            let mut acc = z3::ast::Bool::from_bool(&ctx, false);
            for b in &bytes {
                let pct = b._eq(&BV::from_u64(&ctx, b'%' as u64, 8));
                acc = z3::ast::Bool::or(&ctx, &[&acc, &pct]);
            }
            solver.assert(&acc);
        }
        SinkKind::StackBuffer => {
            for b in &bytes {
                let nz = b._eq(&BV::from_u64(&ctx, 0, 8)).not();
                solver.assert(&nz);
            }
        }
        SinkKind::LengthArg => {
            return SmtFinding::Unsupported("LengthArg sink not modeled in v0");
        }
    }

    match solver.check() {
        z3::SatResult::Sat => {
            let m = match solver.get_model() {
                Some(m) => m,
                None => return SmtFinding::Unsupported("SAT but no model returned"),
            };
            let mut input_bytes = Vec::new();
            for (i, b) in bytes.iter().enumerate() {
                let evaluated = z3::Model::eval(&m, b, true);
                if let Some(v_bv) = evaluated {
                    if let Some(v) = v_bv.as_u64() {
                        input_bytes.push((i, v as u8));
                    }
                }
            }
            SmtFinding::Reachable { input_bytes }
        }
        z3::SatResult::Unsat => SmtFinding::NotReachable,
        z3::SatResult::Unknown => SmtFinding::Unsupported("solver Unknown / timeout"),
    }
}

/// Stub for default builds. Callers can emit a "rebuild with
/// --features smt" hint when they see this.
#[cfg(not(feature = "smt"))]
pub fn solve(_path: &TaintPath, _ssa: &crate::ir::SsaCfg) -> SmtFinding {
    SmtFinding::Unsupported("smt feature not enabled at build time")
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn default_tables_non_empty() {
        assert!(!DEFAULT_SOURCES.is_empty());
        assert!(!DEFAULT_SINKS.is_empty());
    }

    #[test]
    fn covers_canonical_apis() {
        let src_names: Vec<_> = DEFAULT_SOURCES.iter().map(|s| s.name).collect();
        for must in &["recv", "read", "fgets", "scanf", "argv"] {
            assert!(src_names.contains(must), "missing source `{must}`");
        }
        let sink_names: Vec<_> = DEFAULT_SINKS.iter().map(|s| s.name).collect();
        for must in &["strcpy", "sprintf", "memcpy", "system", "popen", "execve"] {
            assert!(sink_names.contains(must), "missing sink `{must}`");
        }
    }

    #[test]
    fn argument_slots_match_real_abi() {
        // recv(int sockfd, void *buf, size_t len, int flags) — buf is arg 1.
        let recv = DEFAULT_SOURCES.iter().find(|s| s.name == "recv").unwrap();
        assert_eq!(recv.tainted, AbiSlot::Arg(1));

        // gets(char *s) — fills buffer at arg 0.
        let gets = DEFAULT_SOURCES.iter().find(|s| s.name == "gets").unwrap();
        assert_eq!(gets.tainted, AbiSlot::Arg(0));

        // memcpy(void *dst, const void *src, size_t n) — n is arg 2.
        let memcpy = DEFAULT_SINKS.iter().find(|s| s.name == "memcpy").unwrap();
        assert_eq!(memcpy.watched, AbiSlot::Arg(2));
        assert_eq!(memcpy.kind, SinkKind::LengthArg);

        // system(const char *cmd) — cmd is arg 0.
        let system = DEFAULT_SINKS.iter().find(|s| s.name == "system").unwrap();
        assert_eq!(system.watched, AbiSlot::Arg(0));
        assert_eq!(system.kind, SinkKind::Command);
    }

    #[test]
    fn resolves_plain_libc_name() {
        let mut imports = HashMap::new();
        imports.insert(0x1000, "recv".to_string());
        let r = resolve_call(0x1000, &imports).expect("recv resolved");
        match r {
            SpecRef::Source(s) => assert_eq!(s.name, "recv"),
            _ => panic!("expected source"),
        }
    }

    #[test]
    fn strips_plt_suffix() {
        let mut imports = HashMap::new();
        imports.insert(0x2000, "strcpy@plt".to_string());
        let r = resolve_call(0x2000, &imports).expect("strcpy@plt resolved");
        match r {
            SpecRef::Sink(s) => assert_eq!(s.name, "strcpy"),
            _ => panic!("expected sink"),
        }
    }

    #[test]
    fn strips_macho_underscore() {
        let mut imports = HashMap::new();
        imports.insert(0x3000, "_system".to_string());
        let r = resolve_call(0x3000, &imports).expect("_system resolved");
        match r {
            SpecRef::Sink(s) => assert_eq!(s.name, "system"),
            _ => panic!("expected sink"),
        }
    }

    #[test]
    fn strips_versioned_suffix() {
        let mut imports = HashMap::new();
        imports.insert(0x4000, "memcpy@@GLIBC_2.14".to_string());
        let r = resolve_call(0x4000, &imports).expect("versioned memcpy");
        match r {
            SpecRef::Sink(s) => {
                assert_eq!(s.name, "memcpy");
                assert_eq!(s.kind, SinkKind::LengthArg);
            }
            _ => panic!("expected sink"),
        }
    }

    #[test]
    fn unknown_name_is_none() {
        let mut imports = HashMap::new();
        imports.insert(0x5000, "fancy_app_helper".to_string());
        assert!(resolve_call(0x5000, &imports).is_none());
    }

    #[test]
    fn missing_addr_is_none() {
        let imports: HashMap<u64, String> = HashMap::new();
        assert!(resolve_call(0xdead_beef, &imports).is_none());
    }

    // ---- path collector ----

    use crate::ir::{
        BlockId, Diagnostic, Expr, InferredType, SsaBlock, SsaCfg, SsaTerminator,
        Stmt, VarDef,
    };
    use pcode_ir::Varnode;

    fn mk_var(id: u32, expr: Expr) -> VarDef {
        VarDef {
            id: VarId(id),
            varnode: Varnode::constant(0, 8),
            expr,
            size: 8,
            use_count: 1,
            param_name: None,
            call_return: false,
            inferred_type: InferredType::Unknown,
            display_type: None,
        }
    }

    fn block_with_term(stmts: Vec<Stmt>, term: SsaTerminator) -> SsaBlock {
        SsaBlock {
            id: BlockId(0),
            addr: 0,
            stmts,
            terminator: term,
        }
    }

    fn cfg(vars: Vec<VarDef>, block: SsaBlock) -> SsaCfg {
        SsaCfg {
            blocks: vec![block],
            vars,
            entry: BlockId(0),
            diagnostics: Vec::<Diagnostic>::new(),
        }
    }

    fn imports_with(entries: &[(u64, &str)]) -> HashMap<u64, String> {
        entries
            .iter()
            .map(|(a, n)| (*a, n.to_string()))
            .collect()
    }

    #[test]
    fn accepts_recv_then_strcpy_in_same_block() {
        // Two direct calls, recv (source) then strcpy (sink), both
        // resolved via the import map, terminator = Return.
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),       // sock fd
            mk_var(1, Expr::Const(0x4000, 8)),  // buf
            mk_var(2, Expr::Const(0x100, 8)),   // len
            mk_var(3, Expr::Const(0, 8)),       // flags
            mk_var(4, Expr::Const(0x5000, 8)),  // dst
        ];
        let stmts = vec![
            Stmt::Call {
                target: CallTarget::Direct(0x1000),
                args: vec![VarId(0), VarId(1), VarId(2), VarId(3)],
                out: None,
            },
            Stmt::Call {
                target: CallTarget::Direct(0x2000),
                args: vec![VarId(4), VarId(1)],
                out: None,
            },
        ];
        let block = block_with_term(stmts, SsaTerminator::Return(None));
        let ssa = cfg(vars, block);
        let imports = imports_with(&[(0x1000, "recv"), (0x2000, "strcpy")]);

        let paths = collect_paths(&ssa, &imports).expect("should accept");
        assert_eq!(paths.len(), 1);
        assert_eq!(paths[0].source.name, "recv");
        assert_eq!(paths[0].sink.name, "strcpy");
        assert!(paths[0].source_event < paths[0].sink_event);
    }

    #[test]
    fn cbranch_with_no_arm_blocks_falls_through_to_dangling() {
        // v1 collector explores BOTH arms of a CBranch. With only a
        // single block in the CFG and dangling block ids on the
        // CBranch terminator, both arms hit "dangling block id" and
        // the walk returns NoSinkFound (or the dangling rejection).
        // v0 rejected up front with UnsupportedTerminator(CBranch);
        // v1 attempts the arms and bails when blocks don't exist.
        let vars = vec![mk_var(0, Expr::Const(0, 1))];
        let block = block_with_term(
            vec![],
            SsaTerminator::CBranch {
                cond: VarId(0),
                taken: BlockId(1),
                fallthrough: BlockId(2),
            },
        );
        let ssa = cfg(vars, block);
        let imports: HashMap<u64, String> = HashMap::new();

        match collect_paths(&ssa, &imports) {
            Err(PathRejection::UnsupportedTerminator(reason)) => {
                // Either dangling-block rejection (the most accurate
                // outcome on this fixture) or NoSinkFound — both
                // signal "no v1 path collected".
                assert!(
                    reason == "dangling block id" || reason == "Branch",
                    "unexpected rejection reason: {reason}"
                );
            }
            Err(PathRejection::NoSinkFound) => {}
            other => panic!("expected dangling/NoSinkFound, got {other:?}"),
        }
    }

    #[test]
    fn cbranch_explores_both_arms_for_source_sink_pair() {
        // v1 hallmark: a CBranch that gates a sink in one arm and
        // not the other should produce ONE path through the
        // sink-bearing arm, with branch_decisions recording the
        // taken edge.
        //
        //   block 0: recv(...)         (Source in entry block stmts)
        //   block 0 terminator: CBranch cond → block 1 (sink) / block 2 (return)
        //   block 1 terminator: Call strcpy(...) → block 3
        //   block 2 terminator: Return
        //   block 3 terminator: Return
        let vars = vec![
            mk_var(0, Expr::Const(0, 1)),    // CBranch cond
            mk_var(1, Expr::Const(0, 8)),    // sock fd
            mk_var(2, Expr::Const(0x4000, 8)), // buf
            mk_var(3, Expr::Const(0x100, 8)),
            mk_var(4, Expr::Const(0, 8)),
            mk_var(5, Expr::Const(0x5000, 8)), // dst
        ];
        let block0 = SsaBlock {
            id: BlockId(0),
            addr: 0x1000,
            stmts: vec![Stmt::Call {
                target: CallTarget::Direct(0x10),
                args: vec![VarId(1), VarId(2), VarId(3), VarId(4)],
                out: None,
            }],
            terminator: SsaTerminator::CBranch {
                cond: VarId(0),
                taken: BlockId(1),
                fallthrough: BlockId(2),
            },
        };
        let block1 = SsaBlock {
            id: BlockId(1),
            addr: 0x1010,
            stmts: vec![],
            terminator: SsaTerminator::Call {
                target: CallTarget::Direct(0x20),
                args: vec![VarId(5), VarId(2)],
                out: None,
                fallthrough: BlockId(3),
            },
        };
        let block2 = SsaBlock {
            id: BlockId(2),
            addr: 0x1020,
            stmts: vec![],
            terminator: SsaTerminator::Return(None),
        };
        let block3 = SsaBlock {
            id: BlockId(3),
            addr: 0x1030,
            stmts: vec![],
            terminator: SsaTerminator::Return(None),
        };
        let ssa = SsaCfg {
            blocks: vec![block0, block1, block2, block3],
            vars,
            entry: BlockId(0),
            diagnostics: Vec::<Diagnostic>::new(),
        };
        let imports = imports_with(&[(0x10, "recv"), (0x20, "strcpy")]);

        let paths =
            collect_paths(&ssa, &imports).expect("v1 should explore CBranch arms");
        assert_eq!(paths.len(), 1, "expected single recv→strcpy path, got {}", paths.len());
        assert_eq!(paths[0].source.name, "recv");
        assert_eq!(paths[0].sink.name, "strcpy");
        assert_eq!(paths[0].branch_decisions.len(), 1);
        assert_eq!(paths[0].branch_decisions[0].block_addr, 0x1000);
        assert!(paths[0].branch_decisions[0].taken, "should have taken the sink-bearing arm");
    }

    #[test]
    fn cbranch_depth_limit_caps_walks() {
        // Construct a chain of CBranches deeper than MAX_BRANCH_DEPTH.
        // The walker must reject the over-budget walks but still
        // surface paths from the within-budget arms (none here, so
        // the result is a depth-limit rejection).
        //
        // Just chain k+1 CBranches where every fallthrough goes to
        // the next CBranch — this hits the depth cap on the
        // taken-arm walks specifically.
        let mut vars = Vec::new();
        let mut blocks = Vec::new();
        let depth = (MAX_BRANCH_DEPTH + 2) as usize;
        vars.push(mk_var(0, Expr::Const(0, 1))); // cond, reused
        for i in 0..depth {
            blocks.push(SsaBlock {
                id: BlockId(i),
                addr: 0x1000 + i as u64 * 0x10,
                stmts: vec![],
                terminator: SsaTerminator::CBranch {
                    cond: VarId(0),
                    taken: BlockId(i + 1),
                    fallthrough: BlockId(depth + 1),
                },
            });
        }
        // Terminal blocks at the bottom of the chain
        blocks.push(SsaBlock {
            id: BlockId(depth),
            addr: 0x2000,
            stmts: vec![],
            terminator: SsaTerminator::Return(None),
        });
        blocks.push(SsaBlock {
            id: BlockId(depth + 1),
            addr: 0x2010,
            stmts: vec![],
            terminator: SsaTerminator::Return(None),
        });
        let ssa = SsaCfg {
            blocks,
            vars,
            entry: BlockId(0),
            diagnostics: Vec::<Diagnostic>::new(),
        };
        let imports: HashMap<u64, String> = HashMap::new();

        let result = collect_paths(&ssa, &imports);
        // No source/sink configured; result should be an error,
        // and the depth limit must have been triggered for at
        // least the deepest arm.
        match result {
            Err(PathRejection::UnsupportedTerminator("depth limit"))
            | Err(PathRejection::NoSinkFound)
            | Err(PathRejection::UnsupportedTerminator("Branch")) => {}
            other => panic!("expected depth-limit/NoSink rejection, got {other:?}"),
        }
    }

    #[test]
    fn phi_assignment_is_skipped_not_rejected() {
        // v0 hard-rejected any Phi in entry block. v1 skips the
        // Phi assignment (recording no event for it) and keeps
        // walking — necessary to reach Source/Sink pairs in real
        // CFGs where every reconvergence point introduces a Phi.
        // Without source/sink configured, walk completes with
        // no paths -> NoSinkFound (NOT PhiInPath).
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),
            mk_var(1, Expr::Const(0, 8)),
            mk_var(2, Expr::Phi(vec![VarId(0), VarId(1)])),
        ];
        let block = block_with_term(
            vec![Stmt::Assign(VarId(2))],
            SsaTerminator::Return(None),
        );
        let ssa = cfg(vars, block);
        let imports: HashMap<u64, String> = HashMap::new();

        match collect_paths(&ssa, &imports) {
            Err(PathRejection::NoSinkFound) => {}
            other => panic!("expected NoSinkFound (Phi skipped), got {other:?}"),
        }
    }

    #[test]
    fn rejects_indirect_call() {
        let vars = vec![mk_var(0, Expr::Const(0, 8))];
        let block = block_with_term(
            vec![Stmt::Call {
                target: CallTarget::Indirect(Varnode::constant(0, 8)),
                args: vec![],
                out: None,
            }],
            SsaTerminator::Return(None),
        );
        let ssa = cfg(vars, block);
        let imports: HashMap<u64, String> = HashMap::new();

        assert_eq!(collect_paths(&ssa, &imports).unwrap_err(), PathRejection::IndirectCall);
    }

    #[test]
    fn no_sink_found() {
        // recv but no sink anywhere.
        let vars = vec![mk_var(0, Expr::Const(0, 8))];
        let block = block_with_term(
            vec![Stmt::Call {
                target: CallTarget::Direct(0x1000),
                args: vec![],
                out: None,
            }],
            SsaTerminator::Return(None),
        );
        let ssa = cfg(vars, block);
        let imports = imports_with(&[(0x1000, "recv")]);

        assert_eq!(collect_paths(&ssa, &imports).unwrap_err(), PathRejection::NoSinkFound);
    }

    #[test]
    fn source_after_sink_yields_no_path() {
        // Sink fires before any source — no taint flow possible.
        let vars = vec![mk_var(0, Expr::Const(0, 8))];
        let block = block_with_term(
            vec![
                Stmt::Call {
                    target: CallTarget::Direct(0x2000),
                    args: vec![],
                    out: None,
                },
                Stmt::Call {
                    target: CallTarget::Direct(0x1000),
                    args: vec![],
                    out: None,
                },
            ],
            SsaTerminator::Return(None),
        );
        let ssa = cfg(vars, block);
        let imports = imports_with(&[(0x1000, "recv"), (0x2000, "strcpy")]);

        assert_eq!(collect_paths(&ssa, &imports).unwrap_err(), PathRejection::NoSinkFound);
    }

    // ---- v0 SAT prover (gated on `smt` feature) ----

    #[cfg(feature = "smt")]
    fn one_call_pair_cfg(
        source_addr: u64, source_args: Vec<VarId>,
        sink_addr:   u64, sink_args:   Vec<VarId>,
        vars: Vec<VarDef>,
    ) -> SsaCfg {
        let stmts = vec![
            Stmt::Call {
                target: CallTarget::Direct(source_addr),
                args: source_args,
                out: None,
            },
            Stmt::Call {
                target: CallTarget::Direct(sink_addr),
                args: sink_args,
                out: None,
            },
        ];
        cfg(vars, block_with_term(stmts, SsaTerminator::Return(None)))
    }

    #[cfg(feature = "smt")]
    #[test]
    fn sat_recv_to_strcpy_is_reachable() {
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),       // sock fd
            mk_var(1, Expr::Const(0x4000, 8)),  // buf  (shared between recv arg1 and strcpy arg1)
            mk_var(2, Expr::Const(0x100, 8)),
            mk_var(3, Expr::Const(0, 8)),
            mk_var(4, Expr::Const(0x5000, 8)),  // dst
        ];
        let ssa = one_call_pair_cfg(
            0x1000, vec![VarId(0), VarId(1), VarId(2), VarId(3)],
            0x2000, vec![VarId(4), VarId(1)],
            vars,
        );
        let imports = imports_with(&[(0x1000, "recv"), (0x2000, "strcpy")]);
        let paths = collect_paths(&ssa, &imports).expect("v0 path collection");
        match solve(&paths[0], &ssa) {
            SmtFinding::Reachable { input_bytes } => {
                assert_eq!(input_bytes.len(), 32);
                assert!(input_bytes.iter().all(|(_, b)| *b != 0));
            }
            other => panic!("expected Reachable, got {other:?}"),
        }
    }

    #[cfg(feature = "smt")]
    #[test]
    fn sat_recv_to_printf_is_reachable() {
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),
            mk_var(1, Expr::Const(0x4000, 8)),
            mk_var(2, Expr::Const(0x100, 8)),
            mk_var(3, Expr::Const(0, 8)),
        ];
        let ssa = one_call_pair_cfg(
            0x1000, vec![VarId(0), VarId(1), VarId(2), VarId(3)],
            0x2000, vec![VarId(1)],
            vars,
        );
        let imports = imports_with(&[(0x1000, "recv"), (0x2000, "printf")]);
        let paths = collect_paths(&ssa, &imports).expect("v0 path collection");
        match solve(&paths[0], &ssa) {
            SmtFinding::Reachable { input_bytes } => {
                assert!(input_bytes.iter().any(|(_, b)| *b == b'%'));
            }
            other => panic!("expected Reachable with `%`, got {other:?}"),
        }
    }

    #[cfg(feature = "smt")]
    #[test]
    fn sat_argv_to_system_is_reachable() {
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),       // argc
            mk_var(1, Expr::Const(0x4000, 8)),  // argv (becomes argv[*] approx)
        ];
        let ssa = one_call_pair_cfg(
            0x1000, vec![VarId(0), VarId(1)],
            0x2000, vec![VarId(1)],
            vars,
        );
        let imports = imports_with(&[(0x1000, "argv"), (0x2000, "system")]);
        let paths = collect_paths(&ssa, &imports).expect("v0 path collection");
        match solve(&paths[0], &ssa) {
            SmtFinding::Reachable { input_bytes } => {
                assert!(input_bytes
                    .iter()
                    .any(|(_, b)| matches!(*b, b';' | b'&' | b'|')));
            }
            other => panic!("expected Reachable with shell metachar, got {other:?}"),
        }
    }

    #[cfg(feature = "smt")]
    #[test]
    fn unsat_recv_into_unrelated_strcpy_dst() {
        // recv fills buf (VarId 1), strcpy copies UNRELATED VarId 9
        // — no taint lineage. Must NotReachable.
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),
            mk_var(1, Expr::Const(0x4000, 8)),
            mk_var(2, Expr::Const(0x100, 8)),
            mk_var(3, Expr::Const(0, 8)),
            mk_var(4, Expr::Const(0x5000, 8)),
            mk_var(5, Expr::Const(0, 8)),
            mk_var(6, Expr::Const(0, 8)),
            mk_var(7, Expr::Const(0, 8)),
            mk_var(8, Expr::Const(0, 8)),
            mk_var(9, Expr::Const(0x6000, 8)),  // unrelated buffer
        ];
        let ssa = one_call_pair_cfg(
            0x1000, vec![VarId(0), VarId(1), VarId(2), VarId(3)],
            0x2000, vec![VarId(4), VarId(9)],
            vars,
        );
        let imports = imports_with(&[(0x1000, "recv"), (0x2000, "strcpy")]);
        let paths = collect_paths(&ssa, &imports).expect("v0 path collection");
        assert_eq!(solve(&paths[0], &ssa), SmtFinding::NotReachable);
    }

    #[cfg(feature = "smt")]
    #[test]
    fn lineage_eq_follows_var_chain() {
        // VarId 5 -> Var(4) -> Var(3) -> Var(2). lineage_eq(5, 2) = true.
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),
            mk_var(1, Expr::Const(0, 8)),
            mk_var(2, Expr::Const(0x4000, 8)),
            mk_var(3, Expr::Var(VarId(2))),
            mk_var(4, Expr::Var(VarId(3))),
            mk_var(5, Expr::Var(VarId(4))),
        ];
        let mem = MemMap::new();
        assert!(varid_lineage_eq(VarId(5), VarId(2), &vars, &mem));
        assert!(!varid_lineage_eq(VarId(5), VarId(0), &vars, &mem));
    }

    #[cfg(feature = "smt")]
    #[test]
    fn lineage_eq_follows_store_then_load() {
        // Store v1 -> mem[addr=v0]; Load(v0) → should resolve to v1.
        // lineage_eq(load_var, v1) must be true via the memory map.
        let vars = vec![
            mk_var(0, Expr::Const(0x1000, 8)),     // addr
            mk_var(1, Expr::Const(0xdeadbeef, 8)), // stored value
            mk_var(2, Expr::Load(VarId(0))),       // load from same addr
        ];
        let mut mem = MemMap::new();
        mem.insert(vars[0].varnode, VarId(1));
        // Without memmap entry, lineage fails.
        assert!(!varid_lineage_eq(VarId(2), VarId(1), &vars, &MemMap::new()));
        // With memmap entry, lineage holds.
        assert!(varid_lineage_eq(VarId(2), VarId(1), &vars, &mem));
    }

    #[test]
    fn sink_in_terminator_call_slot() {
        // strcpy lives in the SsaTerminator::Call slot. Path
        // collector must walk the Call terminator and continue to
        // the fallthrough block (which here just returns).
        let vars = vec![
            mk_var(0, Expr::Const(0, 8)),
            mk_var(1, Expr::Const(0x4000, 8)),
            mk_var(2, Expr::Const(0x5000, 8)),
        ];
        let block0 = SsaBlock {
            id: BlockId(0),
            addr: 0,
            stmts: vec![Stmt::Call {
                target: CallTarget::Direct(0x1000),
                args: vec![VarId(0), VarId(1), VarId(0), VarId(0)],
                out: None,
            }],
            terminator: SsaTerminator::Call {
                target: CallTarget::Direct(0x2000),
                args: vec![VarId(2), VarId(1)],
                out: None,
                fallthrough: BlockId(1),
            },
        };
        let block1 = SsaBlock {
            id: BlockId(1),
            addr: 0x10,
            stmts: vec![],
            terminator: SsaTerminator::Return(None),
        };
        let ssa = SsaCfg {
            blocks: vec![block0, block1],
            vars,
            entry: BlockId(0),
            diagnostics: Vec::<Diagnostic>::new(),
        };
        let imports = imports_with(&[(0x1000, "recv"), (0x2000, "strcpy")]);

        let paths = collect_paths(&ssa, &imports).expect("should accept terminator-Call sink");
        assert_eq!(paths.len(), 1);
        assert_eq!(paths[0].sink.name, "strcpy");
    }
}