vj-sim 0.1.0

//! Task S3b (`docs/superpowers/plans/2026-09-26-wave-A2-slice.md`): the
//! Activation Record frame layout -- declared SV locals get a permanent
//! slot unconditionally (PR-017, PR-018), and a backward liveness fixpoint
//! over the segmented [`super::cfg::ProcessCfg`] computes which
//! compiler-generated temporaries (if any) also need one (PR-021, PR-016,
//! PR-019). Ledger PR-015..PR-027, CG-100. See `docs/design/process.md` §3.
//!
//! **Why this task never actually constructs a `FrameSlotSource::Temporary`
//! slot (load-bearing, read before touching `lower_to_segments`'s fill
//! rule):** design.md §3 is explicit that the only thing liveness ever
//! decides is "which LLVM SSA temporaries ... need a frame slot at all" --
//! i.e. a *compiler-generated* value with no corresponding `sv_lang::Symbol`
//! at all, minted only when CODEGEN (Task S3c) decomposes an expression into
//! named intermediate LLVM values. At this task's level -- a
//! not-yet-lowered-to-LLVM `ProcessCfg` over plain `sv_lang::Statement`/
//! `Expression` handles -- no such value exists yet: every `NamedValue` leaf
//! this file's backward fixpoint can observe resolves to a real
//! `sv_lang::Symbol`, and in the A2 slice's restricted grammar (no
//! functions/tasks, no nested automatic scopes) that symbol is always
//! either (a) a local declared inside this very process (found via
//! [`collect_declared_locals`], see its own doc comment for why that -- not
//! a per-statement symbol accessor -- is the only available discovery path
//! against the pinned `sv-lang`=0.1.9 C API) or (b) an external
//! module-level port/signal, which does not belong in this process's frame
//! at all regardless of how "live" it is (its value is always fetched
//! through the accessor ABI on demand; STATE, not this frame, owns it).
//! **Neither case is a compiler temporary.** The backward fixpoint below is
//! still a real, generically-correct implementation over the *whole*
//! referenced-symbol universe (not narrowed to declared locals up front --
//! narrowing early would make this a weaker, less faithful implementation
//! of PR-021's literal "standard GEN/KILL per statement" algorithm), because
//! its live-in/live-out results are exactly what a future Task S3c revision
//! of this module intersects with codegen's own materialized temporary set
//! once one exists, and because PR-022's oracle self-check needs a real
//! computed live-in set to check in the first place. For every fixture this
//! task can construct, filtering that result down to "symbols with no
//! declared-local match" is provably empty by the slice grammar's own
//! shape -- which is exactly what `compiler_temporary_dead_before_suspend_
//! gets_no_frame_slot` (PR-019) checks.

use crate::symid::SymbolUid;
use std::collections::HashSet;

use crate::symid::SymbolId;
use sv_lang::kinds::{ExpressionKind, SymbolKind};
use sv_lang::{Expression, Statement, Symbol};

use super::FrameSlot;
use super::cfg::{
    ArgBinding, LoweringError, ProcessCfg, RepeatCount, RepeatCounterId, SuspendPoint, Terminator,
};

/// One frame slot's compile-time layout entry (PR-025, PR-026).
///
/// **Deviation from the plan's literal field list** (`{offset, width_bits,
/// source}`, no `repr`): the ledger's own PR-025/PR-026 text asks for a
/// `repr: FourStateI2N | WideFourState` tag per slot, and `process::
/// FrameSlot` (already committed, `Narrow4State{word_count}` /
/// `Wide4State{aval_word_count, bval_word_count}`) is exactly that shape --
/// reused here rather than re-declared, so there is exactly one "frame
/// slot's physical shape" enum in this crate, not two.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct FrameSlotDesc {
    /// Word offset within the process TEMPLATE's frame (PR-024: decided once
    /// per template, at lowering-plan build time -- never per instance).
    /// Units match `repr`'s own word-count field (a private, per-`FrameLayout`
    /// bump allocation -- see [`compute_liveness`]'s doc comment on why this
    /// is deliberately *not* `state::arena::Arena`-allocated).
    pub offset: u32,
    /// The signal's real, untruncated bit width (CG-100: never a `u16`-
    /// clamped or otherwise narrowed copy -- see
    /// `declared_local_width_is_never_truncated_even_at_the_64_bit_boundary`).
    pub width_bits: u32,
    pub repr: FrameSlot,
    pub source: FrameSlotSource,
    /// A variable shared with a fork branch (`ProcessCfg::captured`): the
    /// slot is one word, a pointer to the cell holding the value (`repr` is
    /// the value's shape).
    pub cell: bool,
    /// A cell variable of the process that forked this one (never
    /// initialized here: it arrives with the parent's pointer).
    pub captured: bool,
}

/// PR-025: `DeclaredVar` is a permanent slot (PR-017/018 -- unconditional,
/// regardless of what the liveness fixpoint computes); `Temporary` is the
/// liveness-driven kind this task's own fixtures never construct -- see this
/// module's own doc comment for exactly why.
///
/// **`SyntheticCounter` (R-run Task 8):** a `repeat(N)` loop's own
/// compiler-synthesized iteration counter (`process::cfg::
/// RepeatCounterId`), minted only when a suspend somewhere in the loop's own
/// body forces `process::cfg::CfgBuilder::walk_repeat_loop` to build a real
/// CFG shape for it (see that id's own doc comment). Unlike `DeclaredVar`,
/// there is no `sv_lang::Symbol` behind it at all -- it is PERMANENT for
/// exactly the same reason `DeclaredVar` is (it must survive the loop's own
/// suspend/resume call boundary), so [`compute_liveness`]/`lower_to_segments`
/// treat the two identically for the "always in live_in/live_out" rule,
/// differing only in how a caller resolves the slot to a physical pointer
/// (`process_lower.rs`'s `counter_locals`, keyed by `RepeatCounterId`, not
/// the `SymbolId`-keyed `frame_locals`/`cx.locals` a `DeclaredVar` uses).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum FrameSlotSource {
    DeclaredVar(SymbolId),
    Temporary(u32),
    SyntheticCounter(RepeatCounterId),
}

/// PR-025: the per-TEMPLATE frame layout `compute_liveness` produces.
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct FrameLayout {
    pub slots: Vec<FrameSlotDesc>,
}

impl FrameLayout {
    /// Total 8-byte words this layout occupies -- the `frame_word_count` a
    /// `CompiledKernelProcess` needs to size its owned frame buffer.
    pub fn total_words(&self) -> u32 {
        self.slots
            .iter()
            .map(|s| match s.repr {
                _ if s.cell => 1,
                FrameSlot::Narrow4State { word_count } => u32::from(word_count),
                FrameSlot::Wide4State {
                    aval_word_count,
                    bval_word_count,
                } => aval_word_count + bval_word_count,
                FrameSlot::Array { rows, row_words } => rows * u32::from(row_words),
            })
            .sum()
    }
}

/// A value's stored width (`state::storage`), 0 for none.
fn storage_width(ty: &sv_lang::Type) -> u64 {
    crate::state::storage::storage_width(ty).unwrap_or(0)
}

/// An automatic `event` variable's frame representation: its handle, the
/// object id in the event pool (`state::event_pool`), 0 = `null`.
pub const EVENT_HANDLE_WIDTH: u64 = 64;

/// A declared local's frame slot: `(width_bits, repr)` -- a packed value of
/// up to 128 bits (2 planes, `2 * width` bits in 64-bit words), or a
/// fixed-size unpacked array of such elements (`FrameSlot::Array`, width
/// the element's). `None` for anything else.
fn local_frame_slot(ty: &sv_lang::Type) -> Option<(u32, FrameSlot)> {
    let words_for = |w: u64| (2 * w).div_ceil(64).max(1);
    // A queue, dynamic or associative array is its 64-bit handle (as in
    // STATE); a fixed-size array of them is rows of handles.
    let is_collection = crate::state::storage::is_collection;
    if ty.is_unpacked_array() && !is_collection(ty) {
        let mut rows: u64 = 1;
        let mut cur = *ty;
        while cur.is_unpacked_array() && !is_collection(&cur) {
            rows *= u64::from(cur.fixed_unpacked_array_range().width());
            cur = cur.element_type()?;
        }
        let w = if cur.is_event() {
            EVENT_HANDLE_WIDTH
        } else {
            storage_width(&cur)
        };
        if w == 0 || w > u64::from(u16::MAX) {
            return None;
        }
        return Some((
            w as u32,
            FrameSlot::Array {
                rows: u32::try_from(rows).ok()?,
                row_words: words_for(w) as u16,
            },
        ));
    }
    let w = if ty.is_event() {
        EVENT_HANDLE_WIDTH
    } else {
        storage_width(ty)
    };
    if w == 0 || w > u64::from(u16::MAX) {
        return None;
    }
    Some((
        w as u32,
        FrameSlot::Narrow4State {
            word_count: words_for(w) as u16,
        },
    ))
}

/// PR-021: the backward-fixpoint, `AnalyzedProcedure::read_set()`-oracle-
/// seeded liveness computation, restricted to the slice's own AST-level
/// fixtures (see this module's doc comment for why `slots` is always
/// `DeclaredVar`-only here).
///
/// **Deviation on the oracle (PR-022):** the plan's literal signature is
/// exactly `compute_liveness(cfg: &ProcessCfg<'d>) -> Result<...>`, with no
/// extra parameter for `AnalyzedProcedure::read_set()`. Verified against the
/// pinned `sv-lang`=0.1.9 API: a bare `Statement<'d>`/`Expression<'d>`
/// handle (everything `ProcessCfg` carries) has no accessor back to the
/// `Design`/`Analysis` that produced it, so a live `read_set()` genuinely
/// cannot be obtained from `&ProcessCfg<'d>` alone -- only from a caller
/// that already holds `design.analyze(..)` (a live `Analysis<'a>`, a
/// *different* lifetime than `ProcessCfg`'s own `'d` elaboration brand).
/// This function therefore derives its own whole-procedure read-set
/// directly from `cfg`'s own AST (every `NamedValue` read reference
/// anywhere in `cfg.blocks`, via the exact same walk the fixpoint itself
/// uses) as a *self-consistency* oracle -- it still catches a real class of
/// bug (a live-in symbol the fixpoint's own successor/GEN-KILL propagation
/// pulled in from the wrong place), just not the independent-implementation
/// class an external `AnalyzedProcedure::read_set()` cross-check would also
/// catch. [`compute_liveness_with_oracle`] is the version a caller that
/// *does* hold a live `Analysis` (this crate's own tests; Task S7's real
/// integration glue) should call instead, passing slang's own `read_set()`
/// as the independent oracle -- exactly what PR-022 asks for.
pub fn compute_liveness<'d>(cfg: &ProcessCfg<'d>) -> Result<FrameLayout, LoweringError> {
    let read_set = aggregate_all_uses(cfg);
    compute_liveness_with_oracle(cfg, &read_set)
}

/// PR-022's real oracle-cross-checked path: `read_set_oracle` should be
/// `AnalyzedProcedure::read_set()`'s symbols (mapped to [`SymbolId`] via
/// `Symbol::id()`) whenever a caller has one; every live-in set the backward
/// fixpoint computes is checked against it, hard-failing
/// ([`LoweringError::liveness_oracle_mismatch`]) the moment it is not a
/// subset.
pub fn compute_liveness_with_oracle<'d>(
    cfg: &ProcessCfg<'d>,
    read_set_oracle: &HashSet<SymbolId>,
) -> Result<FrameLayout, LoweringError> {
    compute_liveness_impl(cfg, read_set_oracle, None)
}

/// PR-022's fault-injection seam, exposed so a test can prove the self-check
/// in [`compute_liveness_with_oracle`] is actually wired -- not merely
/// described -- rather than only ever observing it pass on legitimate input.
/// Behaves exactly like [`compute_liveness_with_oracle`], except the given
/// `bogus` symbol is unconditionally inserted into block 0's computed
/// live-in set before the oracle check runs, so a caller can construct any
/// ordinary process, pick a `SymbolId` that is provably outside its
/// `read_set`, and confirm this returns
/// `Err(LoweringError)` naming it.
pub fn compute_liveness_fault_injected<'d>(
    cfg: &ProcessCfg<'d>,
    read_set_oracle: &HashSet<SymbolId>,
    bogus: SymbolId,
) -> Result<FrameLayout, LoweringError> {
    compute_liveness_impl(cfg, read_set_oracle, Some(bogus))
}

fn compute_liveness_impl<'d>(
    cfg: &ProcessCfg<'d>,
    read_set_oracle: &HashSet<SymbolId>,
    inject_bogus: Option<SymbolId>,
) -> Result<FrameLayout, LoweringError> {
    let declared = collect_declared_locals(cfg)?;
    let declared_ids: HashSet<SymbolId> = declared.iter().map(|(id, _)| id.clone()).collect();

    let mut live_in = backward_fixpoint(cfg);
    if let Some(bogus) = inject_bogus {
        // Test-only: force the fault into block 0's own live-in set,
        // whatever `backward_fixpoint` legitimately computed for it.
        if let Some(first) = live_in.first_mut() {
            first.insert(bogus);
        }
    }

    // PR-022: every computed live-in symbol, at every block, must be a
    // whole-procedure read -- never silently ignored.
    for set in &live_in {
        for sym in set {
            if !read_set_oracle.contains(sym) {
                return Err(LoweringError::liveness_oracle_mismatch(sym.to_string()));
            }
        }
    }

    // PR-017/018: every declared local gets a permanent slot, unconditionally
    // -- never derived from (added or removed by) the fixpoint above. See
    // this module's doc comment for why `Temporary` is never populated here.
    // The variables this process shares with its fork branches, and those
    // it shares with the process that forked it: pointer slots.
    let mut shared: HashSet<SymbolId> = HashSet::new();
    for b in &cfg.blocks {
        if let Terminator::ForkJoin { branches, .. } = &b.terminator {
            for br in branches {
                shared.extend(br.captured.iter().map(|v| v.uid()));
            }
        }
    }
    let mut declared = declared;
    let mut from_parent: HashSet<SymbolId> = HashSet::new();
    for v in &cfg.captured {
        let id = v.uid();
        if !declared.iter().any(|(d, _)| *d == id) {
            shared.insert(id.clone());
            from_parent.insert(id.clone());
            declared.push((id, *v));
        }
    }
    let mut slots = Vec::with_capacity(declared.len());
    let mut next_offset: u32 = 0;
    for (id, sym) in &declared {
        let ty = sym.value_type().ok_or_else(|| {
            LoweringError::malformed(format!("declared local {sym:?} has no value_type()"))
        })?;
        let (width_bits, repr) = local_frame_slot(&ty).ok_or_else(|| {
            LoweringError::unsupported(format!(
                "declared local {} of type {} has no frame representation (a value wider \
                 than 128 bits, a dynamic array, a class handle, ...)",
                sym.name(),
                ty.to_sv_string()
            ))
        })?;
        let words = match repr {
            FrameSlot::Narrow4State { word_count } => u32::from(word_count),
            FrameSlot::Array { rows, row_words } => rows * u32::from(row_words),
            FrameSlot::Wide4State {
                aval_word_count,
                bval_word_count,
            } => aval_word_count + bval_word_count,
        };
        let cell = shared.contains(id);
        slots.push(FrameSlotDesc {
            offset: next_offset,
            width_bits,
            repr,
            source: FrameSlotSource::DeclaredVar(id.clone()),
            cell,
            captured: from_parent.contains(id),
        });
        next_offset += if cell { 1 } else { words };
    }

    // This task's own fixtures never populate a `Temporary` slot -- see this
    // module's doc comment. `declared_ids` is retained (rather than removed
    // as dead code) as the exact filter a future Task S3c revision applies
    // to the fixpoint's raw `live_in`/`live_out` results once a genuine
    // compiler temporary (a live symbol with no declared-local match) can
    // exist; asserting it here would be a gate that cannot fail against
    // today's grammar, so it is documented, not asserted.
    let _ = &declared_ids;

    // R-run Task 8: every `repeat(N)` loop's own synthetic counter
    // (`FrameSlotSource::SyntheticCounter`'s own doc comment) also gets a
    // permanent slot, unconditionally -- allocated after every declared
    // local, in the same first-appearance-in-`cfg.blocks` order
    // `collect_repeat_counters` discovers them (a `RepeatCounterId` is
    // already dense/unique per process by construction, so no dedup pass is
    // needed here the way `collect_declared_locals`'s `SymbolId`-keyed
    // `HashSet` needs one).
    for (counter, count) in collect_repeat_counters(cfg) {
        // A `foreach` element count: a 64-bit counter.
        let bit_width_u64 = match count {
            RepeatCount::Const(_) | RepeatCount::Size(_) | RepeatCount::NestedSize { .. } => 64,
            RepeatCount::Expr(count_expr) | RepeatCount::Inherited(count_expr) => count_expr
                .expr_type()
                .ok_or_else(|| {
                    LoweringError::malformed(format!(
                        "repeat({counter:?}) count expression has no expr_type()"
                    ))
                })?
                .bit_width(),
        };
        if bit_width_u64 == 0 || bit_width_u64 > 64 {
            // Same slice-scope restriction as a declared local's width
            // (see the loop above) -- a named, loud rejection, never a
            // silent truncation.
            return Err(LoweringError::unsupported(format!(
                "repeat({counter:?}) count expression has bit_width {bit_width_u64} (0 or \
                 >64) -- wide/memory repeat counts are out of the A2 slice's scope \
                 (PR-025/CG-100, extended to R-run Task 8's synthetic counters)"
            )));
        }
        let width_bits = bit_width_u64 as u32;
        let word_count_u64 = (2u64 * bit_width_u64).div_ceil(64).max(1);
        let word_count = word_count_u64 as u16;
        slots.push(FrameSlotDesc {
            offset: next_offset,
            width_bits,
            repr: FrameSlot::Narrow4State { word_count },
            source: FrameSlotSource::SyntheticCounter(counter),
            cell: false,
            captured: false,
        });
        next_offset += u32::from(word_count);
    }

    // An intra-assignment-timed assignment's captured right-hand side: a
    // permanent temporary slot shaped like its target.
    let ref_temps: HashSet<u32> = cfg
        .blocks
        .iter()
        .flat_map(|b| b.bindings.iter())
        .filter_map(|b| match b {
            ArgBinding::RefOpen { temp, .. } => Some(*temp),
            _ => None,
        })
        .collect();
    for (temp, target) in cfg.captures.iter().enumerate() {
        // A `ref` to a collection element keeps its runtime reference id.
        if ref_temps.contains(&(temp as u32)) {
            slots.push(FrameSlotDesc {
                offset: next_offset,
                width_bits: 64,
                repr: FrameSlot::Narrow4State { word_count: 2 },
                source: FrameSlotSource::Temporary(temp as u32),
                cell: false,
                captured: false,
            });
            next_offset += 2;
            continue;
        }
        let ty = match cfg.capture_types.get(temp).copied().flatten() {
            Some(formal) => formal.value_type(),
            None => target.expr_type(),
        }
        .ok_or_else(|| {
            LoweringError::malformed("intra-assignment timing target has no expr_type()")
        })?;
        let (width_bits, repr) = local_frame_slot(&ty).ok_or_else(|| {
            LoweringError::unsupported(format!(
                "an intra-assignment-timed assignment to a {} (no frame representation)",
                ty.to_sv_string()
            ))
        })?;
        let words = match repr {
            FrameSlot::Narrow4State { word_count } => u32::from(word_count),
            FrameSlot::Array { rows, row_words } => rows * u32::from(row_words),
            FrameSlot::Wide4State {
                aval_word_count,
                bval_word_count,
            } => aval_word_count + bval_word_count,
        };
        slots.push(FrameSlotDesc {
            offset: next_offset,
            width_bits,
            repr,
            source: FrameSlotSource::Temporary(temp as u32),
            cell: false,
            captured: false,
        });
        next_offset += words;
    }

    Ok(FrameLayout { slots })
}

/// R-run Task 8: every distinct `RepeatCounterId` a suspend-containing
/// `repeat(N)` loop minted anywhere in `cfg.blocks`, paired with its own
/// count expression, in block-index (allocation) order -- the CFG-level
/// analogue of [`collect_declared_locals`], but reading `BasicBlock::
/// repeat_init` (a plain per-block field this crate's own `process::cfg`
/// already populates) rather than walking the AST for a `Symbol`, since a
/// synthetic counter has no `Symbol` to discover in the first place.
fn collect_repeat_counters<'d>(
    cfg: &ProcessCfg<'d>,
) -> Vec<(RepeatCounterId, crate::process::cfg::RepeatCount<'d>)> {
    cfg.blocks
        .iter()
        .filter_map(|b| b.repeat_init.clone())
        .collect()
}

/// PR-017: every declared SV local referenced anywhere in `cfg.body`'s
/// subtree, in first-appearance-in-source (AST pre-order) discovery order,
/// deduplicated by [`SymbolId`].
///
/// **Why this walks `Block` statements' `Statement::block_symbol()` rather
/// than looking at each `VariableDeclaration` statement directly:** verified
/// against the pinned `sv-lang`=0.1.9 C API (`CApiAst.cpp`) -- there is no
/// `slang_stmt_*` accessor that recovers a `VariableDeclStatement`'s own
/// declared symbol (confirmed: `Statement::children()`/`::expressions()`
/// both come back empty for a `VariableDeclaration`-kind leaf). What the
/// binding *does* expose is `Statement::block_symbol()`
/// (`slang::ast::BlockStatement::blockSymbol`), and slang's own
/// `Statement::bind` (`Statement.cpp`) gives an UNNAMED `begin`/`end` block a
/// real (anonymously-named) `StatementBlockSymbol` scope whenever it
/// contains at least one declaration -- confirmed live against this
/// project's own `sv-lang` build (an unnamed `begin int x; ... end` yields
/// `block_symbol() == Some(<anonymous>)`, whose `.members()` lists `x`),
/// not merely inferred from the doc comment's narrower "unnamed -> None"
/// phrasing (which describes the truly decl-free case only). Recursing over
/// every `Block` statement in the tree and collecting each one's
/// `block_symbol()`'s `Variable`-kind members is therefore the only
/// available, non-panicking discovery path.
fn collect_declared_locals<'d>(
    cfg: &ProcessCfg<'d>,
) -> Result<Vec<(SymbolId, Symbol<'d>)>, LoweringError> {
    let mut out: Vec<(SymbolId, Symbol<'d>)> = Vec::new();
    let mut seen: HashSet<SymbolId> = HashSet::new();
    let mut stack = vec![cfg.body.as_sem_node()];
    while let Some(node) = stack.pop() {
        if let Some(stmt) = node.as_statement() {
            for block_sym in super::cfg::block_scopes(&stmt) {
                for member in block_sym.members() {
                    // A static one is the instance's (a STATE signal).
                    if member.kind() == SymbolKind::Variable
                        && !crate::netlist::is_static_procedural_var(&member)
                    {
                        let id = member.uid();
                        if seen.insert(id.clone()) {
                            out.push((id, member));
                        }
                    }
                }
            }
        }
        stack.extend(super::cfg::live_children(&node));
    }
    // Pattern variables (LRM 12.6) are declared by no statement either.
    for v in crate::patterns::pattern_vars(cfg.body.as_sem_node()) {
        let id = v.uid();
        if seen.insert(id.clone()) {
            out.push((id, v));
        }
    }
    // Formals/locals of tasks inlined into this process: declared by no
    // `Block` under `cfg.body` (their declarations live in the task).
    for sym in &cfg.inlined_locals {
        let id = sym.uid();
        if seen.insert(id.clone()) {
            out.push((id, *sym));
        }
    }
    Ok(out)
}

/// The ids of the variables `cfg` declares (its blocks' and its inlined
/// tasks'), for `process::cfg`'s fork capture analysis.
pub(crate) fn declared_local_ids(cfg: &ProcessCfg<'_>) -> HashSet<SymbolId> {
    collect_declared_locals(cfg)
        .map(|v| v.into_iter().map(|(id, _)| id).collect())
        .unwrap_or_default()
}

/// One inlined-task [`ArgBinding`]'s reads and (whole-symbol) definition,
/// in the same shape [`statement_use_def`] reports for a statement.
fn binding_use_def<'d>(b: &ArgBinding<'d>) -> (Vec<Symbol<'d>>, Option<Symbol<'d>>) {
    let mut uses = Vec::new();
    match b {
        ArgBinding::In { formal, actual } => {
            collect_named_values(*actual, &mut uses);
            (uses, Some(*formal))
        }
        ArgBinding::Init { var } => {
            if let Some(init) = var.initializer() {
                collect_named_values(init, &mut uses);
            }
            (uses, Some(*var))
        }
        ArgBinding::Out { actual, formal } => {
            // Conservative: the target's own name counts as a use too (a
            // select target is a read-modify-write), never as a kill.
            collect_named_values(*actual, &mut uses);
            uses.push(*formal);
            (uses, None)
        }
        ArgBinding::Const { var, .. } | ArgBinding::ThisOf { var } => (uses, Some(*var)),
        // Reads the handles the variable holds (and clears it).
        ArgBinding::Release { var } => {
            uses.push(*var);
            (uses, None)
        }
        // A captured value lives in a compiler temporary, not a symbol.
        ArgBinding::Capture { value, .. } => {
            collect_named_values(*value, &mut uses);
            (uses, None)
        }
        ArgBinding::AssignCaptured { target, .. } => {
            collect_named_values(*target, &mut uses);
            (uses, None)
        }
        // The value lives in a compiler temporary, not a symbol.
        ArgBinding::FromCaptured { formal, .. } => (uses, Some(*formal)),
        ArgBinding::ToCaptured { formal, .. } => {
            uses.push(*formal);
            (uses, None)
        }
        ArgBinding::CallResult { .. } | ArgBinding::ClassEventLeave => (uses, None),
        // The caller's `this` (a compiler temporary, not a symbol).
        ArgBinding::CaptureThis { .. } => (uses, None),
        // The reference id lives in a compiler temporary.
        ArgBinding::RefOpen { formal, actual, .. } => {
            collect_named_values(*actual, &mut uses);
            (uses, Some(*formal))
        }
        ArgBinding::RefClose { formal, actual, .. } => {
            collect_named_values(*actual, &mut uses);
            uses.push(*formal);
            (uses, None)
        }
        ArgBinding::Step { var, .. } => {
            uses.push(*var);
            (uses, None)
        }
        ArgBinding::AssocKey {
            var,
            arr,
            path,
            next,
        } => {
            collect_named_values(*arr, &mut uses);
            uses.extend(path.iter().map(|s| s.var));
            if *next {
                uses.push(*var);
            }
            (uses, Some(*var))
        }
    }
}

/// Every `NamedValue` expression's `referenced_symbol()`, reachable anywhere
/// in `expr`'s subtree -- the one shared leaf-collection primitive both
/// [`statement_use_def`] and the terminator-condition walks below reuse
/// (mirrors `cfg.rs`'s own `contains_suspend_trigger` traversal shape).
fn collect_named_values<'d>(expr: Expression<'d>, out: &mut Vec<Symbol<'d>>) {
    let mut stack = vec![expr.as_sem_node()];
    while let Some(node) = stack.pop() {
        if let Some(e) = node.as_expression()
            && crate::symid::is_value_name(e.kind())
            && let Some(sym) = e.referenced_symbol()
        {
            out.push(sym);
        }
        // A call to a function inlined into the process reads its result
        // variable (`CfgBuilder::hoist_suspending_function_calls`).
        if let Some(e) = node.as_expression()
            && e.kind() == ExpressionKind::Call
            && e.is_system_call() != Some(true)
            && let Some(callee) = e.call_subroutine()
            && callee.subroutine_kind() == Some(sv_lang::SubroutineKind::Function)
            && let Some(rv) = callee.subroutine_return_val_var()
        {
            out.push(rv);
        }
        stack.extend(node.children());
    }
}

/// The symbols read by the index expressions of `e` when it selects an
/// element of an unpacked array (`ea[i]`, `ea[i][j]`); nothing for any other
/// event expression.
fn event_index_reads<'d>(e: Expression<'d>, out: &mut Vec<Symbol<'d>>) {
    let mut cur = e;
    while cur.kind() == ExpressionKind::ElementSelect {
        if let Some(sel) = cur.selector() {
            collect_named_values(sel, out);
        }
        match cur.select_value() {
            Some(base) => cur = base,
            None => break,
        }
    }
}

/// One statement's GEN (read uses) / KILL (the one symbol it defines, if
/// any) sets, per PR-021's "standard GEN/KILL per statement". The slice's
/// grammar only ever defines a symbol through a whole-signal blocking/
/// nonblocking `Assignment` with a bare `NamedValue` lvalue (its own "Slice
/// scope" -- no concatenation LHS); anything else conservatively contributes
/// no KILL (safe -- it only ever makes a symbol stay live *longer* than a
/// fully precise analysis would, never shorter, which cannot manufacture a
/// false oracle mismatch since every collected use still comes from a real
/// read reference in the AST).
fn statement_use_def<'d>(stmt: &Statement<'d>) -> (Vec<Symbol<'d>>, Option<Symbol<'d>>) {
    if let Some(top) = stmt.expressions().into_iter().next()
        && top.kind() == ExpressionKind::Assignment
    {
        let mut uses = Vec::new();
        let mut def = None;
        if let Some(lhs) = top.left() {
            if crate::symid::is_value_name(lhs.kind()) {
                def = lhs.referenced_symbol();
            } else {
                // Out-of-scope lvalue shape (e.g. a select) -- conservatively
                // treat it as a read too, never as a silent def.
                collect_named_values(lhs, &mut uses);
            }
        }
        if let Some(rhs) = top.right() {
            collect_named_values(rhs, &mut uses);
        }
        return (uses, def);
    }

    let mut uses = Vec::new();
    for e in stmt.expressions() {
        collect_named_values(e, &mut uses);
    }
    (uses, None)
}

fn successors(t: &Terminator<'_>) -> Vec<u32> {
    match t {
        Terminator::Fallthrough(b) => vec![b.0],
        Terminator::Branch {
            then_blk, else_blk, ..
        } => vec![then_blk.0, else_blk.0],
        Terminator::Assertion {
            pass_blk,
            fail_blk,
            done_blk,
            ..
        } => vec![pass_blk.0, fail_blk.0, done_blk.0],
        Terminator::Suspend { resume_blk, .. } => vec![resume_blk.0],
        Terminator::End { loop_back } => loop_back.iter().map(|b| b.0).collect(),
        // Task 1: each of these is an unconditional edge to exactly one
        // other block in this same `cfg.blocks` graph -- `Loop`'s real
        // per-iteration decision lives on `entry`'s own (separately
        // visited) terminator, never on `Loop` itself (mirrors
        // `lower_terminator`'s identical `Goto(entry)` mapping).
        Terminator::Loop { entry, .. } => vec![entry.0],
        Terminator::ForkJoin { join_blk, .. } => vec![join_blk.0],
        // R-run Task 8: same two-successor shape as `Branch` above (this is
        // `repeat`'s own header decision), just no `cond: Expression` to
        // additionally walk in `terminator_uses` below.
        Terminator::RepeatCheck {
            then_blk, else_blk, ..
        } => vec![then_blk.0, else_blk.0],
        Terminator::Case {
            arms, default_blk, ..
        }
        | Terminator::Switch {
            arms, default_blk, ..
        } => arms
            .iter()
            .chain(std::iter::once(default_blk))
            .map(|b| b.0)
            .collect(),
    }
}

/// **Verified against real `sv-lang`=0.1.9 `AnalyzedProcedure::read_set()`
/// output (not assumed):** a `SignalEventControl`'s edge signal (`clk` in
/// `@(posedge clk)`) does NOT appear in `read_set()` -- it is a sensitivity
/// *trigger*, not a data read, in slang's own dataflow model (consistent
/// with `always_comb`'s implicit sensitivity list being derived separately
/// from the read set, never by re-adding an already-explicit edge signal to
/// it). `SuspendPoint::Edge`'s signal is therefore deliberately excluded
/// here -- including it made the real, non-fault-injected path in
/// `liveness_never_computes_a_symbol_outside_the_procedures_read_set` fail
/// against a genuine `AnalyzedProcedure::read_set()` oracle before this fix.
/// `SuspendPoint::Delay`'s expression is, by contrast, an ordinary value
/// expression (the slice only ever elaborates it to a constant, so this
/// never contributes a `NamedValue` in practice here, but the general case
/// -- an expression delay -- is out of A2-slice scope entirely, PR-006) and
/// is included for the same reason a `Branch` condition is.
fn terminator_uses<'d>(t: &Terminator<'d>, out: &mut Vec<Symbol<'d>>) {
    match t {
        Terminator::Branch { cond, .. } => collect_named_values(*cond, out),
        Terminator::Assertion { stmt, .. } => {
            if let Some(c) = crate::process::cfg::assertion_cond(stmt) {
                collect_named_values(c, out);
            }
        }
        // What selects the arm (a virtual interface, weights, a selector)
        // is read.
        Terminator::Switch { on, .. } => {
            for e in on.reads() {
                collect_named_values(e, out);
            }
        }
        // The selector and every label are read to pick the arm.
        Terminator::Case { stmt, .. } => {
            for e in case_reads(stmt) {
                collect_named_values(e, out);
            }
        }
        Terminator::Suspend {
            point: SuspendPoint::Delay(e, _),
            ..
        } => collect_named_values(*e, out),
        // Task 1: `wait(expr)` is a genuine data read (unlike an edge
        // trigger) -- same treatment as a `Branch` condition.
        Terminator::Suspend {
            point: SuspendPoint::Level(e),
            ..
        } => collect_named_values(*e, out),
        // Task 6: `ImplicitComb`'s captured read-set IS genuine data reads
        // (the guarded body's own AST-derived sensitivity list) -- same
        // treatment as `Level`'s condition above, extended to every member.
        Terminator::Suspend {
            point: SuspendPoint::ImplicitComb(exprs),
            ..
        } => {
            for e in exprs {
                collect_named_values(*e, out);
            }
        }
        // Task 1: `EdgeList`'s member signals are sensitivity triggers, not
        // data reads -- same verified-against-`read_set()` reasoning as
        // plain `Edge` above, extended to every member. Task 6: the revised
        // `CycleDelay`'s `clock` is a trigger too (an edge-
        // sensitivity subscription, never a data read), same reasoning as
        // plain `Edge`/`CycleDelay` before this task.
        // The index of an event-array element in an event control
        // (`@(ea[k])`) is evaluated when the wait starts (LRM 1800-2023
        // 15.5.1): a data read, though the event itself is only a trigger.
        Terminator::Suspend {
            point: SuspendPoint::Edge { signal, iff, .. },
            ..
        } => {
            event_index_reads(*signal, out);
            // The `iff` guard is a data read at every wake (LRM 1800-2023
            // 9.4.2.3), so a local read only there must outlive the suspend.
            if let Some(g) = iff {
                collect_named_values(*g, out);
            }
        }
        Terminator::Suspend {
            point: SuspendPoint::EdgeList(entries, iffs),
            ..
        } => {
            for (e, _) in entries {
                event_index_reads(*e, out);
            }
            for g in iffs.iter().flatten() {
                collect_named_values(*g, out);
            }
        }
        Terminator::Suspend {
            point:
                SuspendPoint::CycleDelay { .. }
                | SuspendPoint::OneStep
                | SuspendPoint::WaitFork
                | SuspendPoint::ByRequest,
            ..
        }
        | Terminator::Fallthrough(_)
        | Terminator::End { .. }
        | Terminator::Loop { .. }
        | Terminator::ForkJoin { .. }
        // R-run Task 8: `RepeatCheck` references no `sv_lang::Symbol` at all
        // (its own counter is compiler-synthesized, `FrameSlotSource::
        // SyntheticCounter`'s own doc comment) -- nothing for this
        // Symbol-liveness walk to collect. Its own `repeat_init` count
        // expression's symbols are, like `step_exprs`', deliberately not
        // walked here either -- see `BasicBlock::step_exprs`'s own doc
        // comment for why omitting them does not under-approximate any
        // `DeclaredVar`/`SyntheticCounter` slot's permanence (both are
        // unconditionally permanent regardless of this fixpoint's result).
        | Terminator::RepeatCheck { .. } => {}
    }
}

/// PR-021: the backward fixpoint itself, over the whole referenced-symbol
/// universe (see this module's doc comment for why narrowing to declared
/// locals up front would be a weaker implementation of the same algorithm).
/// Returns `live_in[block_index]` for every block in `cfg.blocks`.
fn backward_fixpoint<'d>(cfg: &ProcessCfg<'d>) -> Vec<HashSet<SymbolId>> {
    let n = cfg.blocks.len();
    let mut live_in: Vec<HashSet<SymbolId>> = vec![HashSet::new(); n];
    let mut changed = true;
    while changed {
        changed = false;
        for i in (0..n).rev() {
            let block = &cfg.blocks[i];
            let mut live: HashSet<SymbolId> = HashSet::new();
            for succ in successors(&block.terminator) {
                live.extend(live_in[succ as usize].iter().cloned());
            }
            let mut term_uses = Vec::new();
            terminator_uses(&block.terminator, &mut term_uses);
            for sym in term_uses {
                live.insert(sym.uid());
            }
            for stmt in block.stmts.iter().rev() {
                let (uses, def) = statement_use_def(stmt);
                if let Some(d) = def {
                    live.remove(&d.uid());
                }
                for u in uses {
                    live.insert(u.uid());
                }
            }
            for b in block.bindings.iter().rev() {
                let (uses, def) = binding_use_def(b);
                if let Some(d) = def {
                    live.remove(&d.uid());
                }
                for u in uses {
                    live.insert(u.uid());
                }
            }
            if live != live_in[i] {
                live_in[i] = live;
                changed = true;
            }
        }
    }
    live_in
}

/// This task's own (see [`compute_liveness`]'s doc comment) self-derived
/// oracle: every symbol read anywhere in `cfg`'s statements or terminator
/// conditions, via the exact same [`collect_named_values`] leaf collector
/// the fixpoint itself uses.
fn aggregate_all_uses<'d>(cfg: &ProcessCfg<'d>) -> HashSet<SymbolId> {
    let mut out = HashSet::new();
    for block in &cfg.blocks {
        for b in &block.bindings {
            let (uses, _def) = binding_use_def(b);
            for u in uses {
                out.insert(u.uid());
            }
        }
        for stmt in &block.stmts {
            let (uses, _def) = statement_use_def(stmt);
            for u in uses {
                out.insert(u.uid());
            }
        }
        let mut term_uses = Vec::new();
        terminator_uses(&block.terminator, &mut term_uses);
        for u in term_uses {
            out.insert(u.uid());
        }
    }
    out
}

// PR-023's negative gate lives in `tests/process_liveness.rs` as a
// source-text scan of this file (mirrors `sched`'s own `scan_support`
// pattern) -- not here, since a self-referential "this file does not
// contain the string X" check belongs with the other structural/negative
// gates, not inline in the implementation it is scanning.

/// The expressions a [`Terminator::Case`] statement evaluates to choose its
/// arm: for a `case`, the selector, then every item's labels (a `case ...
/// inside` range label's bounds included, as children of its `ValueRange`);
/// for a `unique`/`unique0`/`priority` `if` series, every condition.
pub fn case_reads<'d>(stmt: &sv_lang::Statement<'d>) -> Vec<sv_lang::Expression<'d>> {
    use sv_lang::kinds::StatementKind;
    if stmt.kind() == StatementKind::Conditional {
        // A series the CFG could not lower was rejected when it was built.
        return crate::process::cfg::if_series(*stmt)
            .map(|c| {
                c.links
                    .iter()
                    .flat_map(|l| l.conditions().into_iter().map(|c| c.expr()))
                    .collect()
            })
            .unwrap_or_default();
    }
    if stmt.kind() == StatementKind::PatternCase {
        // The matched expression and every item's `&&&` filter (a pattern
        // itself reads nothing: only constants and bindings).
        return crate::patterns::pattern_case_expr(*stmt)
            .into_iter()
            .chain(stmt.pattern_case_items().iter().filter_map(|i| i.filter()))
            .collect();
    }
    stmt.expr()
        .into_iter()
        .chain(stmt.case_items().iter().flat_map(|i| i.expressions()))
        .collect()
}

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

    /// CG-100's compile-time half (the actual spill/fill IR round-trip is
    /// Task S3c/S4's job, once a real spill site exists -- see this crate's
    /// deviations note): `FrameSlotDesc::width_bits` must be the real,
    /// untruncated bit width, and `repr`'s `word_count` derived from the
    /// FULL `2*width_bits` (never `width_bits` alone, which would silently
    /// halve the unknown/xz plane's storage). A 64-bit declared local is
    /// exactly the boundary case: `word_count` must be 2 (128 bits: 64 val +
    /// 64 unk), never 1 (which would be truncating the unk plane away
    /// entirely).
    #[test]
    fn declared_local_width_is_never_truncated_even_at_the_64_bit_boundary() {
        let design = crate::state::compile_source(
            "module m; initial begin automatic logic [63:0] w; w = 0; end endmodule\n",
        )
        .unwrap();
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let block = body
            .members()
            .find(|s| s.kind() == sv_lang::kinds::SymbolKind::ProceduralBlock)
            .unwrap();
        let root = block.body().unwrap();
        let cfg = super::super::cfg::build_cfg(&root, super::super::cfg::ProcessLoopKind::OneShot)
            .unwrap();
        let frame = compute_liveness(&cfg).unwrap();
        assert_eq!(frame.slots.len(), 1);
        assert_eq!(frame.slots[0].width_bits, 64, "width must not be truncated");
        match frame.slots[0].repr {
            FrameSlot::Narrow4State { word_count } => {
                assert_eq!(
                    word_count, 2,
                    "a 64-bit value's val+unk packing needs 2 u64 words, not 1"
                );
            }
            other => panic!("expected Narrow4State for a 64-bit local, got {other:?}"),
        }
    }

    /// Mutation-coverage regression: `backward_fixpoint`'s per-statement GEN/
    /// KILL step must apply KILL (remove the statement's own def) *before*
    /// GEN (insert its uses) -- `live_in = (live_out - def) ∪ use`, per
    /// PR-021's own "standard GEN/KILL per statement" formula this module's
    /// doc comment cites. A statement whose LHS symbol also appears on its
    /// own RHS (`a = a + 1`) is exactly the case that distinguishes the two
    /// orders: swapping them (GEN then KILL) would insert `a` and then
    /// immediately remove it again, silently dropping a symbol that is
    /// genuinely read in this same statement from the computed live-in set.
    /// `compute_liveness`'s own PR-022 oracle self-check cannot catch this
    /// class of bug (it only rejects an over-approximated live-in symbol,
    /// never an under-approximated one), so this test calls
    /// `backward_fixpoint` directly.
    #[test]
    fn self_referencing_statement_keeps_its_own_rhs_use_live_into_the_block() {
        let design = crate::state::compile_source(
            "module m; initial begin int a; a = a + 1; end endmodule\n",
        )
        .unwrap();
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let block = body
            .members()
            .find(|s| s.kind() == sv_lang::kinds::SymbolKind::ProceduralBlock)
            .unwrap();
        let root = block.body().unwrap();
        let cfg = super::super::cfg::build_cfg(&root, super::super::cfg::ProcessLoopKind::OneShot)
            .unwrap();

        let read_set = aggregate_all_uses(&cfg);
        let a_id = read_set
            .iter()
            .next()
            .expect(
                "`a` is read on the RHS of `a = a + 1`, so the whole-procedure read-set \
                     oracle must contain exactly its SymbolId",
            )
            .clone();
        assert_eq!(
            read_set.len(),
            1,
            "the only symbol ever read in this fixture is `a`"
        );

        let live_in = backward_fixpoint(&cfg);
        assert!(
            live_in.iter().any(|set| set.contains(&a_id)),
            "`a` is used on the RHS of the very statement that defines it -- it must be live \
             going into that block, but backward_fixpoint's computed live-in sets {live_in:?} \
             contain no block with `a`"
        );
    }

    /// LRM 1800-2023 9.4.2.3: an `iff` guard (on a plain edge or an event-list
    /// member) is evaluated at every wake, a data read of its operands. A local
    /// read only there is therefore live across the suspend; the backward
    /// fixpoint must see both guards.
    #[test]
    fn a_symbol_read_only_in_an_iff_guard_is_live_at_the_suspend() {
        let design = crate::state::compile_source(
            "module m; logic c, d; initial begin automatic int g; automatic int h; \
             @(posedge d); @(posedge c iff g); @(posedge c iff h or posedge d); end endmodule\n",
        )
        .unwrap();
        let body = design
            .top_instances()
            .next()
            .unwrap()
            .instance_body()
            .unwrap();
        let block = body
            .members()
            .find(|s| s.kind() == sv_lang::kinds::SymbolKind::ProceduralBlock)
            .unwrap();
        let root = block.body().unwrap();
        let cfg = super::super::cfg::build_cfg(&root, super::super::cfg::ProcessLoopKind::OneShot)
            .unwrap();
        let live_in = backward_fixpoint(&cfg);
        let all: HashSet<SymbolId> = live_in.iter().flatten().cloned().collect();
        let names: Vec<String> = all.iter().map(|id| format!("{id:?}")).collect();
        for local in ["g", "h"] {
            assert!(
                names
                    .iter()
                    .any(|n| n.ends_with(local) || n.contains(&format!(".{local}"))),
                "`{local}` is read only by an iff guard but is not live: {names:?}"
            );
        }
    }
}