--- passes/static_analysis.lua — Per-atom static-analysis checks. --- Ownership: `ctx.shared.corpus` canonical merged registry; per-source fallback synthesis is rejected. --- `atom.paths` supplies the emitted and analysis projections consumed by this pass. --- --- Per-atom rules: --- 1. transfer_hazards: A single forward walker (`analyze_hardware_relations`) reads `atom.paths.word_events` once per atom. --- For each emitted word event it (a) inspects pending CPU / COP0 / COP2 / GTE relations against the event as CONSUMER --- (recording a hazard on `atom.paths.hazards` when the producer→consumer gap is below the required retire-slot count), --- (b) Applies the event's GPR value effects (`duffle.INSTRUCTION_GPR_EFFECTS`) to `atom.paths.forward_state.gpr_values`, --- applies bounded constant propagation, and stages matching relation rows as PRODUCERS (with `destination_match` filters, e.g. for the IRGB fan-out). --- The `transfer_hazards` CHECK_RULES reader projects `atom.paths.hazards` into per-atom findings. --- The reader does NOT re-walk source. The walker runs once per atom before the per-atom dispatch; the reader runs inside the same dispatch. --- 2. control_transfer_delay_slot_use: For every emitted branch/jump/call encoder in `duffle.CONTROL_TRANSFER_DELAY_SLOT_POLICIES` --- (the six `branch_*` encoders plus `jump` / `jump_reg` / `jump_link` / `call_reg` / `call_addr`), inspect the next emitted event in `atom.paths.word_events`. --- Emit an `info`-severity finding when the successor is `nop` or absent (the next emitted word IS the hardware delay slot). --- `jump_reg(R_AtomJmp)` is suppressed by policy (the fixed `mac_yield()` handshake). --- `nop2` needs no special case: emission-model emits two `nop` events for it, so the first expansion is the hardware delay slot. --- `atom_label` also needs no special case (zero events). --- 3. mac_yield uniformity: Every atom body must contain exactly one `mac_yield()` call (control transfer pattern). --- 4. Binding handoff: Every `atom_bind(Binds_X)` must reference a `typedef Struct_(Binds_X) { ... }` declaration. --- 5. GPU Port-Store Shape: Per-shape (`f3`/`f4`/`g4`/etc.) the sum of `mac_format_X_color` + `mac_gte_store_X_*` + `mac_insert_ot_tag_X` words --- must equal the GP0 cmd's expected packet size. --- 6. Per-Atom Cycle Budget: Sum each atom body's instruction latencies — non-`mac_*` tokens look up `duffle.INSTRUCTION_LATENCY[ident]`; --- `mac_*` tokens look up `pipe_ctx.components_by_name[bare_name].cycle_cost` (auto-derived from the original `MipsAtomComp_` body by `passes/components.lua::compute_components_metadata`). --- Report total. --- --- Per-source rules (registry-driven): --- 8. enum_alias_membership: Every `R_X` referenced from `atom_dbg_reg_default`, `atom_reg_types`, `atom_type(...)`, `atom_reads`, or `atom_writes` --- must be in `corpus.register_alias_registry`. --- 9. atom_type_consistency: Every `reg_type_overrides[R_X].type_name` must resolve in `corpus.type_name_registry`. --- 10. binds_no_substruct_deref: Every `load_word(R_A, R_B, O_(Type, Field))` and `store_word(...)` in every atom body must reference a leaf scalar --- (pointer-to-struct counts as leaf; nested struct members fail the leaf test). --- --- --- Findings carry an explicit `kind` ("error" / "warning" / "info"). --- The renderer maintains three independent severity collections; `info` is never folded into warnings. --- Scan/cycle summary rows are kept in a separate `summaries` collection (rendered as trailing summary lines, not findings). --- The report header includes `Info: N` alongside Findings / Errors / Warnings, and a dedicated --- `── Info` section renders finding-level info between `── Warnings` and the per-atom cycle counts. --- --- The structural handshake checks (`mac_yield_uniformity`, `hazard_nop_use`, `control_transfer_delay_slot_use`) skip atoms/components with `debug_skip == true`. --- `atom_dbg_skip` marker designates runtime-helper declarations whose structure is fixed by the tape runtime (e.g. `tape_exit`, `ac_yield`). --- Flagging them as "missing mac_yield" or "BD slot is redundant". --- Other checks (transfer_hazards, gpu_portstore_shape, abi_handoff, enum_alias_membership, …) still apply to debug_skip declarations because real hazards / typos can still surface in them. --- --- The orchestrator (`ps1_meta.lua`) wires this module in via the PASSES table: --- `["static-analysis"] = { --- module = "passes.static_analysis", --- kind = "diagnostic", --- deps = {"word-counts", "components"}, --- } --- `kind = "diagnostic"` keeps every finding visible in the projection; the orchestrator does not exit non-zero on static-analysis errors. --- Annotation and header-output validation remain build-stopping. -- ════════════════════════════════════════════════════════════════════════════ -- Module-scope requires + package.path setup -- ════════════════════════════════════════════════════════════════════════════ -- Bootstrap: load `scripts/duffle_paths.lua` (sets package.path + package.cpath). -- Uses `debug.getinfo` to find this file's own directory, so it works both standalone and when require'd from the orchestrator. -- Bootstrap: load `duffle_paths.lua` via `debug.getinfo(1, "S").source` (works both standalone + when require'd). -- duffle_paths.lua sets package.path then returns `require("duffle")` at the bottom, so the dofile value IS the duffle module. --- @type string local _bootstrap_dir = debug.getinfo(1, "S").source:match("^@?(.*[/\\])") or "./" --- @type DuffleExport local duffle = dofile(_bootstrap_dir .. "../duffle_paths.lua") -- ════════════════════════════════════════════════════════════════════════════ -- Constants -- ════════════════════════════════════════════════════════════════════════════ -- Atom declaration + component declaration identifiers. --- @type string local ATOM_DECL = "MipsAtom_" --- @type string local ATOM_COMP = "MipsAtomComp_" --- @type string local ATOM_COMP_PROC = "MipsAtomComp_Proc_" -- Marker-call identifiers inside atom bodies. --- @type string local ATOM_LABEL = "atom_label" --- @type string local ATOM_OFFSET = "atom_offset" --- @type string local ATOM_INFO = "atom_info" --- @type string local ATOM_BIND = "atom_bind" --- @type string local ATOM_READS = "atom_reads" --- @type string local ATOM_WRITES = "atom_writes" --- @type string local ATOM_YIELD = "mac_yield" --- @type string local WORD_COUNT_PRAGMA = "WORD_COUNT(" -- ASCII byte values used in tokenization. --- @type integer local BYTE_NEWLINE = 10 --- @type integer local BYTE_HASH = 35 -- '#' --- @type integer local BYTE_OPEN_PAREN = 40 --- @type integer local BYTE_OPEN_BRACE = 123 --- @type integer local BYTE_OPEN_BRACK = 91 --- @type integer local BYTE_SEMI = 59 -- Per-check output paths (relative to ctx.out_root). --- @type string local OUTPUT_EXTENSION = ".static_analysis.txt" -- ════════════════════════════════════════════════════════════════════════════ -- Type declarations -- ════════════════════════════════════════════════════════════════════════════ -- SourceFile, PassCtx, PassResult: see ps1_meta.lua --- @alias CheckName string -- "transfer_hazards" | "control_transfer_delay_slot_use" | "mac_yield_uniformity" | "yield_load_tail_pairing" | "abi_handoff" | "gpu_portstore_shape" | "per_atom_cycle_budget" | "enum_alias_membership" | "atom_type_consistency" | "binds_no_substruct_deref" --- @class AtomBody --- @field line integer -- Source line of the atom declaration --- @field name AtomName -- Atom name (e.g. "cube_g4_face") --- @field body string -- Brace-delimited body (without the braces) --- @field body_off integer -- char offset of body[1] in source --- @field kind string -- "atom" | "comp_bare" | "comp_proc" --- @class Token --- @field tok string -- Raw token text (trimmed) --- @field line integer -- Source line of the token's start --- @field ident string|nil -- Leading ident of the token (if any) --- @field kind string -- "n_words" | "mac_yield" | "gte_cmdw" | "mac_format" | "mac_gte_store" | "mac_insert_ot_tag" | "atom_label" | "atom_offset" | "other" --- @class CheckFinding --- @field line integer -- Source line of the finding --- @field atom AtomName -- Atom this finding is for (or "") --- @field check CheckName -- Check identifier --- @field kind string -- "error" | "warning" | "info" --- @field msg string -- Finding message --- @class CheckRule --- @field name string --- @field per_atom (fun(item: AtomEntry, pipe_ctx: PipeCtx, findings: CheckFinding[]): nil)|nil --- @field per_source (fun(item: SourceFile, pipe_ctx: PipeCtx, findings: CheckFinding[]): nil)|nil --- @field post (fun(item: nil, pipe_ctx: PipeCtx, findings: CheckFinding[]): nil)|nil --- @field per_macro (fun(item: MacroEntry, pipe_ctx: PipeCtx, findings: CheckFinding[]): nil)|nil --- @field per_skip_marker (fun(item: DebugSkipMarker, pipe_ctx: PipeCtx, findings: CheckFinding[]): nil)|nil --- @class AtomAnalysis --- @field atom AtomBody --- @field tokens Token[] -- Tokens in the atom body, annotated --- @field findings CheckFinding[] -- Findings for this atom --- @field total_cycles integer -- Sum of token cycle costs -- ════════════════════════════════════════════════════════════════════════════ -- Per-word-event helpers -- ════════════════════════════════════════════════════════════════════════════ -- Pick the source-line field that best represents "where in the user's source file is this word?". -- `word_events` (populated by `passes/emission_model.lua::stamp_root_provenance`) carry four line fields: -- * `call_line` — physical line in the ROOT atom's source (the line of the `mac_X(...)` call site that triggered this emission, or `body_line` for direct words in the atom body) -- * `body_line` — physical line in the body containing the emitted word (the atom body for direct words; the component body for words expanded inside `mac_X(...)`) -- * `def_line` — line of the COMPONENT's declaration in its source file (only meaningful for words emitted inside a component expansion) -- * `line` — body-relative line in the source text (not a physical source line; rarely useful in rendered findings) -- -- For component-expanded words (e.g. the BD-slot nop of `jump_reg(R_AtomJmp)` inside `mac_yield()`), -- `body_line` points into the COMPONENT's source file (e.g. `lottes_tape.h:110` for `ac_yield`'s body). -- The user editing their atom body expects the line to point at THEIR source — i.e. the line where `mac_yield()` -- was called (e.g. `hello_gte_tape.c:35`). That line is `call_line`. -- -- For direct words in the atom body (no invocation wrapping them), `call_line == body_line` already, so `call_line` works for both cases. --- @param ev WordEvent|nil --- @return integer local function line_for_word_event(ev) if ev == nil then return 0 end return ev.call_line or ev.body_line or ev.line or ev.def_line or 0 end -- True iff the given atom/component declaration has the bare `atom_dbg_skip` marker. -- Used by the structural handshake checks (`mac_yield_uniformity`, `hazard_nop_use`, -- `control_transfer_delay_slot_use`) to exempt runtime-helper declarations (`tape_exit`, `ac_yield`, -- and the `ac_*` macro components) from findings whose contract they intentionally don't satisfy. --- @param atom AtomEntry|nil --- @return boolean local function is_runtime_helper(atom) return atom and atom.debug_skip == true end -- ════════════════════════════════════════════════════════════════════════════ -- stamp_event_fields — per-word-event classification -- ════════════════════════════════════════════════════════════════════════════ -- ONE forward pass over `atom.paths.word_events` stamps the fields the -- abi / gpu / binds readers consume. Emission already sets is_yield / -- is_load / is_branch; this pass re-stamps those and adds o_arg1 / o_arg2 / -- s_arg1 / mac_format_shape / R_TapePtr / R_PrimCursor finds. -- -- Each event has: -- ident — ev.encoder or ev.ident -- nop_words — 0 / 1 / 2 (for "nop" / "nop2" / anything else) -- nop_prefix — consecutive nop words ending just BEFORE this event -- is_yield — true if ident is `mac_yield` or `mac_yield_tail` -- is_atom_label — true if ident is `atom_label`; label_name has the name -- is_branch — true if duffle.instr(ident).kind == "branch" OR jump/call_addr -- is_unconditional_jump — true if ident is `jump` or `call_addr` -- is_terminal_jump — true if ident is `jump_reg` / `call_reg` / `jump_link` -- is_load — true if isa.kind == "load" -- is_store_word — true if ident is `store_word` --- @class TokClass --- @field ident string -- lLading identifier --- @field nop_words integer -- 0 / 1 / 2 --- @field nop_prefix integer -- Consecutive nop words before this token --- @field is_yield boolean --- @field is_atom_label boolean --- @field label_name string|nil -- For atom_label(name) --- @field is_branch boolean -- Conditional branch OR unconditional-jump-with-offset --- @field is_unconditional_jump boolean -- `jump` / `call_addr` only --- @field is_terminal_jump boolean -- `jump_reg` / `call_reg` / `jump_link` only --- @field branch_label string|false|nil -- For branch_*(..., atom_offset(F, label)) OR jump/call_addr --- @field is_load boolean -- load_word | load_half | load_half_u | load_byte | load_byte_u | gte_lw | gte_lwc2 --- @field is_store_word boolean --- @field mac_format_shape string|nil -- "f3" / "g4" etc. for mac_format_X_color; nil otherwise --- @field is_gte_store boolean -- Ident matches `mac_gte_store_` --- @field is_ot_tag boolean -- Ident matches `mac_insert_ot_tag_` --- @field writes_r_prim_cursor boolean -- store_word targeting R_PrimCursor --- @field reads_r_tape_ptr boolean -- Any token referencing R_TapePtr --- @field o_arg1 string|nil -- First arg of O_(, ) captures; nil for non-O_ tokens --- @field o_arg2 string|nil -- Second arg of O_(, ) captures --- @field s_arg1 string|nil -- Arg of S_() captures; nil for non-S_ tokens -- WordEvent, AtomPaths: see emission_model.lua (AtomPaths augmented below) -- PipeCtx: see annotation.lua (augmented below) -- ForwardState, GprLatticeSlot: see report.lua (augmented below) -- AtomEntry, SourceScan, AtomInfoEntry, BindsEntry, TypeNameEntry, TypeField, -- AliasEntry, DebugSkipMarker, RegTypeDefault, RegTypeOverride: see scan_source.lua -- InstructionRow, InstructionValue, InstructionImm, GteCommandRow, GteCommandPort, -- GteCommandLatch, HardwareRelationRow, Cu2TransitionPolicy, GteCrAliasGroup, -- GtePackedSlotRelation: see duffle_isa.lua -- ComponentDef, Component: see components.lua -- ComponentBodyEntry, EmissionItem, EmissionMarker, InvocationRecord, BodyToken: see duffle_emit.lua -- AutoRegPass: see auto_reg.lua -- Corpus, PassCtx, PassResult, PassOutputEntry, SourceFile: see ps1_meta.lua / duffle.lua --- @class BitLib --- @field bor fun(a: integer, b: integer): integer --- @field band fun(a: integer, b: integer): integer --- @field bxor fun(a: integer, b: integer): integer --- @field lshift fun(a: integer, b: integer): integer --- @class PendingProducer --- @field relation HardwareRelationRow --- @field destination string --- @field word integer --- @field required integer|nil --- @field source_path string|nil --- @field line integer|nil --- @field violation_kind string|nil --- @class RelationTouch --- @field relation_id string --- @field semantic string|nil --- @field producer_word integer --- @field consumer_word integer --- @field destination string|nil --- @field gap integer --- @field required integer|nil --- @field satisfied boolean|nil --- @class Cu2Transition --- @field producer_word integer --- @field producer_line integer --- @field producer_source string --- @field status_register integer|nil --- @field status_value integer|nil --- @field target_enabled boolean|nil --- @field target_state string --- @field required integer --- @field evidence_source string|nil --- @class PostCommandRole --- @field role string --- @field command string --- @field command_register string --- @field producer_word integer --- @field producer_line integer --- @class C2CtrlWrite --- @field alias string --- @field src string|nil --- @field line integer --- @class DelaySlotPolicy --- @field family string --- @field suppress_arg1 table|nil -- bag: GPR ident -> reason --- @class ScanSummary --- @field line integer --- @field msg string --- @class ValidateResult --- @field atoms AtomEntry[] --- @field findings CheckFinding[] --- @field errors CheckFinding[] --- @field warnings CheckFinding[] --- @field info CheckFinding[] --- @field summaries ScanSummary[] --- @class StaticAnalysisDirResult --- @field atoms AtomEntry[] --- @field findings CheckFinding[] --- @field errors CheckFinding[] --- @field warnings CheckFinding[] --- @field info CheckFinding[] --- @field summaries ScanSummary[] --- @field sources SourceFile[] --- @class Ctc2LiveRec --- @field src string|nil --- @field alias string|nil --- @field dest string|nil --- @field line integer|nil --- @field atom string|nil --- @class PackedWrite --- @field alias string --- @field src string|nil --- @field line integer --- @field atom string|nil --- @field idx integer|nil --- @class OffsetTargetMap --- @field [string] integer -- bag: target name -> 0-based word index --- @class OffsetMapByEncoder --- @field [string] OffsetTargetMap --- @class RelationRowsByToken --- @field [string] HardwareRelationRow[] --- @class ConsumerMatchers --- @field cop2_input fun(ev: WordEvent, prod: PendingProducer): boolean --- @field gpr_read fun(ev: WordEvent, prod: PendingProducer): boolean --- @field overwrite_same_dest fun(ev: WordEvent, prod: PendingProducer): boolean --- @class StaticAnalysisPass --- @field run fun(ctx: PassCtx): PassResult --- @class AtomPaths --- @field tok_class TokClass[]|nil --- @field cycles_min integer|nil --- @field cycles_max integer|nil --- @field branches integer|nil --- @field paths integer|nil --- @field has_loops boolean|nil --- @field unknown_macros string[]|nil --- @field forward_state ForwardState|nil --- @field relations RelationTouch[]|nil --- @field hazards CheckFinding[]|nil --- @class AtomEntry --- @field paths AtomPaths|nil --- @field body_tokens BodyToken[]|nil --- @field source_path string|nil --- @field info AtomInfoEntry|nil --- @class PipeCtx --- @field info_by_atom table|nil --- @field binds_index table|nil --- @field unknown_seen table|nil -- bag: macro name -> first atom line --- @field atoms AtomEntry[]|nil --- @field types table|nil --- @field atom_infos_list AtomInfoEntry[]|nil --- @field register_alias_registry table|nil --- @field type_name_registry table|nil --- @field components_by_name table|nil --- @field atoms_by_name table|nil --- @field tape_chains table|nil --- @field source_order SourceFile[]|nil --- @field component_atom_infos AtomInfoEntry[]|nil --- @field atom_infos_all AtomInfoEntry[]|nil --- @field component_body_index table|nil --- @field gte_cr_alias_groups GteCrAliasGroup[]|nil --- @field line_for_word_event (fun(ev: WordEvent): integer)|nil --- @class CheckFinding --- @field source string|nil --- @field relation_id string|nil --- @field semantic string|nil --- @field direction string|nil --- @field producer_destination string|nil --- @field producer_word integer|nil --- @field producer_line integer|nil --- @field producer_source string|nil --- @field consumer_word integer|nil --- @field consumer_token string|nil --- @field gap integer|nil --- @field required integer|nil --- @field evidence_confidence string|nil --- @field evidence_source string|nil --- @field target_state string|nil --- @field status_register integer|nil --- @field status_value integer|nil --- @field producer_command string|nil --- @field nop_classification string|nil --- @field nop_word_index integer|nil --- @field retired_relation string|nil --- @field slot_kind string|nil --- @field command string|nil --- @field role string|nil --- @field actual_register string|nil --- @field expected_register string|nil --- @field relation HardwareRelationRow|nil --- @class ForwardState --- @field pending PendingProducer[]|nil --- @field cu2_state string|nil --- @field cu2_transition Cu2Transition|nil --- @field c2_ctrl_writes C2CtrlWrite[]|nil --- @field _analysis_complete boolean|nil --- @field post_command_roles table|nil --- @class WordEvent --- @field is_delay_marker boolean|nil --- @field delay_marker string|nil --- @field nop_prefix integer|nil --- @field is_atom_label boolean|nil --- @field label_name string|nil --- @field branch_label string|false|nil --- @field is_store_word boolean|nil --- @field mac_format_shape string|nil --- @field is_gte_store boolean|nil --- @field is_ot_tag boolean|nil --- @field writes_r_prim_cursor boolean|nil --- @field reads_r_tape_ptr boolean|nil --- @field o_arg1 string|nil --- @field o_arg2 string|nil --- @field s_arg1 string|nil --- @field is_raw_yield_tail boolean|nil --- @field is_raw_yield_load boolean|nil --- @field source string|nil --- @field word integer|nil --- @field line integer|nil -- Load-delay idents are M.INSTRUCTION rows with kind == "load". -- Patterns for O_(, ) and S_() captures. -- UNANCHORED, the substring can appea anywhere in the token (e.g., `load_word(R_T0, R_TapePtr, O_(Binds_X, field))` matches at position ~24). -- The binds_name match is deferred to check_abi_handoff (which compares ev.o_arg1 == atom.info.binds). --- @type string local O_PATTERN = "O_%(([%w_]+),%s*([%w_]+)%s*%)" --- @type string local S_PATTERN = "S_%(([%w_]+)%s*%)" -- jump_rel is already INSTRUCTION.kind == "branch". Branch flags come from duffle.instr(ident).kind. --- @param events WordEvent[]|nil --- @return nil local function stamp_event_fields(events) --- @type integer local nop_run = 0 --- @type integer, WordEvent for _, ev in ipairs(events or {}) do --- @type string local ident = ev.encoder or ev.ident or "" --- @type string local haystack = (ev.call_text or "") .. " " .. table.concat(ev.args or {}, ",") --- @type boolean local is_delay_marker = false --- @type string|nil local delay_marker = nil if duffle.DELAY_MARKERS and duffle.DELAY_MARKERS[ident] then is_delay_marker = true delay_marker = ident end --- @type integer local nop_words = 0 if ident == "nop" then nop_words = 1 elseif ident == "nop2" then nop_words = 2 end -- mac_yield_tail is the lego-split terminator (addiu_self; jr R_AtomJmp; nop). -- Treat it as a yield for the mac_yield_uniformity check. --- @type boolean local is_yield = ident == "mac_yield" or ident == "mac_yield_tail" --- @type boolean local is_atom_label = false --- @type string|nil local label_name = nil --- @type boolean local is_branch = false --- @type boolean local is_unconditional_jump = false --- @type boolean local is_terminal_jump = false --- @type string|false|nil local branch_label = nil --- @type InstructionRow|nil local isa = duffle.instr(ident) --- @type boolean local is_load = isa and isa.kind == "load" --- @type boolean local is_store_word = ident == "store_word" --- @type string|nil local mac_format_shape = nil --- @type boolean local is_gte_store = false --- @type boolean local is_ot_tag = false --- @type boolean local writes_r_prim_cursor = false --- @type boolean local reads_r_tape_ptr = false --- @type string|nil, string|nil local o_arg1, o_arg2 = nil, nil --- @type string|nil local s_arg1 = nil if ident == "atom_label" then is_atom_label = true label_name = haystack:match("([%w_]+)") elseif isa and isa.kind == "branch" then is_branch = true branch_label = haystack:match("atom_offset%s*%([^,]+,%s*([%w_]+)%s*%)") or false elseif ident == "jump" or ident == "call_addr" then is_branch = true is_unconditional_jump = true branch_label = haystack:match("atom_offset%s*%([^,]+,%s*([%w_]+)%s*%)") or false elseif ident == "jump_reg" or ident == "call_reg" or ident == "jump_link" then is_terminal_jump = true end --- @type string|nil local shape = ident:match("^mac_format_([%w_]+)_color$") if shape then mac_format_shape = shape end if ident:match("^mac_gte_store_[%w_]+$") then is_gte_store = true end if ident == "mac_insert_ot_tag" or ident:match("^mac_insert_ot_tag_[%w_]+$") then is_ot_tag = true end o_arg1, o_arg2 = haystack:match(O_PATTERN) if not o_arg1 then s_arg1 = haystack:match(S_PATTERN) end if haystack:find("R_TapePtr", 1, true) then reads_r_tape_ptr = true end if is_store_word and haystack:find("R_PrimCursor", 1, true) then writes_r_prim_cursor = true end ev.ident = ident ev.is_delay_marker = is_delay_marker ev.delay_marker = delay_marker ev.nop_words = nop_words ev.nop_prefix = nop_run ev.is_yield = is_yield ev.is_atom_label = is_atom_label ev.label_name = label_name ev.is_branch = is_branch ev.is_unconditional_jump = is_unconditional_jump ev.is_terminal_jump = is_terminal_jump ev.branch_label = branch_label ev.is_load = is_load ev.is_store_word = is_store_word ev.mac_format_shape = mac_format_shape ev.is_gte_store = is_gte_store ev.is_ot_tag = is_ot_tag ev.writes_r_prim_cursor = writes_r_prim_cursor ev.reads_r_tape_ptr = reads_r_tape_ptr ev.o_arg1 = o_arg1 ev.o_arg2 = o_arg2 ev.s_arg1 = s_arg1 -- is_raw_yield_load / is_raw_yield_tail stamped after items are walked. if nop_words > 0 then nop_run = nop_run + nop_words else nop_run = 0 end end end -- Raw handshake: load_word(R_AtomJmp, R_TapePtr, _) … jump_reg(R_AtomJmp), BdSlot_ . -- BdSlot_ may hold nop or useful work. No extra annotation. --- @param atom AtomEntry --- @return nil local function stamp_raw_yield_handshake(atom) --- @type EmissionItem[] local items = atom.paths and atom.paths.items or {} --- @type WordEvent[] local events = atom.paths and atom.paths.word_events or {} --- @type table -- bag local bd_after = {} --- @type integer, EmissionItem for idx, it in ipairs(items) do if it.kind == "word" then --- @type EmissionItem|nil local nxt = items[idx + 1] if nxt and nxt.kind == "delay" and nxt.name == "BdSlot_" then bd_after[it.i] = true end end end --- @type integer, WordEvent for _, ev in ipairs(events) do --- @type string local enc = ev.encoder or ev.ident or "" --- @type string[] local args = ev.args or {} --- @type string local rct = ev.root_call_text or ev.call_text or "" --- @type boolean local from_mac = type(rct) == "string" and rct:sub(1, #"mac_yield") == "mac_yield" if enc == "jump_reg" and args[1] == "R_AtomJmp" and bd_after[ev.i] and not from_mac then ev.is_raw_yield_tail = true ev.is_yield = true end if (enc == "load_word" or ev.is_load) and args[1] == "R_AtomJmp" and args[2] == "R_TapePtr" and not from_mac then ev.is_raw_yield_load = true end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #1: transfer-hazard analysis (forward walker + reader). -- -- Single typed CPU/COP0/COP2/GTE relation analysis via the forward walker (`analyze_hardware_relations`). -- Hazards are projected into findings by the `transfer_hazards` CHECK_RULES reader (`check_transfer_hazards`). -- -- The forward walker (`analyze_hardware_relations`) reads `atom.paths.word_events` once per atom. -- For every emitted word event it: -- 1. Inspects current pending relations against the event as CONSUMER. -- A producer's destination is "consumed" by: -- * a `gte_cmdw_*` whose command input set contains the destination (or any fan-out destination of an IRGB write); OR -- * any encoder whose `OPERAND_READ_POSITIONS` includes the GPR destination of an MFC2/CFC2/MFC0 relation. -- The consumer check computes `gap = consumer.word - producer.word - 1` and records a hazard on `atom.paths.hazards` when `gap < required`. -- 2. Applies the event's GPR value effects (`duffle.INSTRUCTION_GPR_EFFECTS`) to `atom.paths.forward_state.gpr_values`. -- Unknown writers invalidate the destination GPR's lattice value to `{kind="unknown"}`. -- The lattice is closed: `{kind="unknown"}` and `{kind="constant", value=}`. -- Bounded constant propagation handles load_upper_i / add_ui / or_i / and_i / xor_i + their self variants) on top of the same forward walker; -- The writer invalidation is the conservative default. -- 3. Stages any relation rows whose `token` matches the event as PRODUCERS. -- The destination operand is `event.args[relation.writes.arg]`. -- Rows with a `destination_match` filter are only staged when the destination operand equals the filter (e.g. C2_IRGB for the IRGB fan-out row). -- The MTC2 ordinary row and the MTC2-IRGB row are both inspected. -- Only the matching row stages (the non-matching row is ignored for that event). -- -- After the walker runs, the `transfer_hazards` CHECK_RULES reader (`check_transfer_hazards`) copies every entry on `atom.paths.hazards` into the per-atom findings list. -- The first `transfer_hazards` reader comment above records the projection contract. -- -- The walker is called once before the CHECK_RULES per-atom dispatch (see `validate()`); -- The reader runs as part of the same CHECK_RULES dispatch so its findings land in `findings` alongside the other checks. -- -- The producer's own emitted word does NOT retire the relation (per the PSX-SPX rule in `docs/psx-spx/docs/cpuspecifications.md:407-419`): -- "Store delays are counted in numbers of clock cycles (not in numbers of opcodes). -- For 3 cycle delay, one must usually insert 3 cached opcodes (or one uncached opcode)." `gap = consumer.word - producer.word - 1` -- therefore counts ONLY words strictly between the producer and the consumer. -- ───────────────────────────────────────────────────────────────────────── -- True iff `consumer_event` is a GTE command (gte_cmdw_* or one of the human-readable aliases mapped in `duffle.GTE_COMMAND_ALIASES`). -- Used by the LWC2 retirement-regime dispatch in the forward walker: a GTE-command consumer can read the LWC2 result in the very next slot -- (the GTE pipeline latches the LWC2 data); any other consumer must observe the standard MIPS load delay (gap >= 1). --- @param consumer_event WordEvent --- @return boolean local function is_gte_command(consumer_event) --- @type string local tok = consumer_event.encoder or consumer_event.ident or "" if tok:sub(1, 9) == "gte_cmdw_" then return true end return duffle.gte(tok) ~= nil end -- True iff `consumer_word` falls inside the COP2 command's input set OR inside the producer's `fanout_to` set (for IRGB writes). -- Used by the consumer-match step of the forward walker. --- @param consumer_event WordEvent --- @param destination string --- @param producer_rel HardwareRelationRow --- @return boolean local function is_cop2_consumer_of(consumer_event, destination, producer_rel) --- @type string local consumer_token = consumer_event.encoder or consumer_event.ident -- Direct match: the consumer's argument is the destination. -- (Reserved for future relations where the consumer literally reads the destination register; -- not used by MTC2/CTC2 today because the "consumer" is a GTE command and its reads are not operand positions.) --- @type string[] local args = consumer_event.args or {} --- @type integer, integer for _, pos in ipairs(args) do if pos == destination then return true end end -- Match via the command's input set: the consumer encoder resolves to a `gte_cmdw_*` -- short form whose GTE_COMMAND.inputs includes the destination (or a fan-out target). --- @type GteCommandRow|nil local gte = duffle.gte(consumer_token) --- @type string local canonical = duffle.gte_canon(consumer_token) if gte or canonical:sub(1, 9) == "gte_cmdw_" then --- @type string[]|nil local cmd_inputs = gte and gte.inputs if cmd_inputs then -- Direct hit. --- @type integer, string for _, in_reg in ipairs(cmd_inputs) do if in_reg == destination then return true end end -- Fan-out hit (IRGB writes fan out to C2_IR1/C2_IR2/C2_IR3). --- @type integer, string for _, fanout in ipairs(producer_rel.fanout_to or {}) do --- @type integer, string for _, in_reg in ipairs(cmd_inputs) do if in_reg == fanout then return true end end end end end return false end --- @param event WordEvent|nil --- @param pos integer --- @return string|nil local function gpr_identity(event, pos) --- @type string[]|nil local keys = event and event.gpr_keys if keys and keys[pos] then return keys[pos] end --- @type string local arg = event and event.args and event.args[pos] if type(arg) == "string" and arg:sub(1, 2) == "R_" then return arg end return nil end -- True iff `consumer_event` reads the GPR operand at any position the destination register occupies. -- read_pos lookup consults `duffle.OPERAND_READ_POSITIONS` for the consumer's encoder and walks each `args[pos]` to find an operand-equal match. --- @param consumer_event WordEvent --- @param destination string --- @return boolean local function is_gpr_consumer_of(consumer_event, destination) --- @type string local consumer_token = consumer_event.encoder or consumer_event.ident --- @type table local read_pos = duffle.OPERAND_READ_POSITIONS or {} --- @type integer[]|nil local positions = read_pos[consumer_token] if not positions then return false end --- @type integer, integer for _, pos in ipairs(positions) do if gpr_identity(consumer_event, pos) == destination then return true end end return false end -- Bounded U4 arithmetic for the GPR-value lattice. LuaJIT supplies the `bit` module; -- the arithmetic fallback keeps this pass Lua 5.3-compatible without adding a dependency to the metaprogram. --- @type boolean, BitLib|nil local bit_ok, bit = pcall(require, "bit") if not bit_ok then bit = nil end --- @type integer local U4_MODULUS = 0x100000000 --- @param value number|nil --- @return integer|nil local function wrap_u4(value) if type(value) ~= "number" then return nil end value = value % U4_MODULUS if value < 0 then value = value + U4_MODULUS end return value end --- @param left number --- @param right number --- @param operation string --- @return integer|nil local function bit_binary(left, right, operation) left = wrap_u4(left) right = wrap_u4(right) if left == nil or right == nil then return nil end if bit then --- @type integer|nil local value if operation == "or" then value = bit.bor( left, right) elseif operation == "and" then value = bit.band(left, right) else value = bit.bxor(left, right) end return wrap_u4(value) end --- @type integer local result = 0 --- @type integer local place = 1 --- @type integer for _ = 1, 32 do --- @type integer local left_bit = left % 2 --- @type integer local right_bit = right % 2 --- @type boolean local take if operation == "or" then take = left_bit == 1 or right_bit == 1 elseif operation == "and" then take = left_bit == 1 and right_bit == 1 else take = left_bit ~= right_bit end if take then result = result + place end left = (left - left_bit) / 2 right = (right - right_bit) / 2 place = place * 2 end return result end --- @param value number --- @param amount number --- @return integer|nil local function shift_left_u4(value, amount) value = wrap_u4(value) amount = tonumber(amount) if value == nil or amount == nil then return nil end amount = math.floor(amount) % 32 if bit then return wrap_u4(bit.lshift(value, amount)) end return wrap_u4(value * (2 ^ amount)) end -- Resolve only a standalone integer literal. -- Compound C expressions remain unknown by design; the analyzer must not pretend to be a C evaluator. --- @param raw string|nil --- @return integer|nil local function parse_integer_literal(raw) if type(raw) ~= "string" then return nil end raw = duffle.trim(raw) while raw:sub(1, 1) == "(" and raw:sub(-1) == ")" do raw = duffle.trim(raw:sub(2, -2)) end --- @type integer local sign = 1 if raw:sub(1, 1) == "-" then sign = -1; raw = raw:sub(2) elseif raw:sub(1, 1) == "+" then raw = raw:sub(2) end raw = raw:gsub("[uUlL]+$", "") --- @type integer|nil local value if raw:match("^0[xX][%da-fA-F]+$") then value = tonumber(raw:sub(3), 16) elseif raw:match("^%d+$") then value = tonumber(raw, 10) else return nil end if value == nil then return nil end return wrap_u4(sign * value) end --- @param value integer --- @return integer local function sign_extend_i16(value) value = value % 0x10000 if value >= 0x8000 then return value - 0x10000 end return value end --- @param operand string|nil --- @return boolean local function is_gpr_operand(operand) return type(operand) == "string" and operand:sub(1, 2) == "R_" end --- @param operand string|nil --- @return boolean local function is_tracked_gpr(operand) return is_gpr_operand(operand) or (type(operand) == "string" and operand:sub(1, 7) == "reguse:") end --- @param gpr_values table --- @param operand string --- @return integer|nil local function constant_for_operand(gpr_values, operand) if operand == "R_0" then return 0 end --- @type GprLatticeSlot|nil local slot = is_gpr_operand(operand) and gpr_values[operand] or nil if slot and slot.kind == "constant" then return wrap_u4(slot.value) end return nil end --- @param gpr_values table --- @param operand string --- @return nil local function invalidate_gpr(gpr_values, operand) if is_tracked_gpr(operand) and operand ~= "R_0" then gpr_values[operand] = { kind = "unknown" } end end --- @param gpr_values table --- @param operand string --- @param value integer|nil --- @return nil local function store_gpr_constant(gpr_values, operand, value) if not is_tracked_gpr(operand) or operand == "R_0" then return end if value == nil then gpr_values[operand] = { kind = "unknown" } else gpr_values[operand] = { kind = "constant", value = wrap_u4(value) } end end --- @type table local VALUE_OPS = { add_ui = function(source, imm) return wrap_u4(source + sign_extend_i16(imm)) end, or_i = function(source, imm) return bit_binary(source, imm % 0x10000, "or") end, and_i = function(source, imm) return bit_binary(source, imm % 0x10000, "and") end, xor_i = function(source, imm) return bit_binary(source, imm % 0x10000, "xor") end, shift_lleft = function(source, imm) return shift_left_u4(source, imm) end, add_u = function(a, b) return wrap_u4(a + b) end, or_u = function(a, b) return bit_binary(a, b, "or") end, } --- @param rule InstructionValue --- @param ev_args string[] --- @param gpr_values table --- @return integer|nil local function evaluate_gpr_value_rule(rule, ev_args, gpr_values) --- @type string local operation = rule.op if operation == "load_upper_i" then --- @type integer|nil local immediate = parse_integer_literal(ev_args[rule.immediate]) if immediate == nil then return nil end return shift_left_u4(immediate % 0x10000, 16) end -- Encoders that take `R_0` implicitly (e.g. `li_s(rt, imm)` which is `add_ui(rt, R_0, imm)`) have a non-GPR operand at the source position. -- Fall back to R_0 = 0. -- The implicit-R_0 macros also use a different immediate position (e.g. `li_s`'s `add_ui` rule has source = 2 / immediate = 3 -- but the macro takes 2 args); when the configured immediate position is out of bounds. -- Fall back instead to scanning the macro's args for the first integer literal and use that as the immediate. --- @type integer local source = 0 if rule.source then if is_gpr_operand(ev_args[rule.source]) then source = constant_for_operand(gpr_values, ev_args[rule.source]) if source == nil then return nil end end -- Non-GPR at source position = implicit R_0; source stays 0. end --- @type integer|nil local immediate = nil if rule.immediate and ev_args[rule.immediate] ~= nil then immediate = parse_integer_literal(ev_args[rule.immediate]) if immediate == nil then return nil end elseif rule.immediate then -- Immediate position out of bounds: scan for the first integer literal in the args. --- @type integer, string for _, arg in ipairs(ev_args) do immediate = parse_integer_literal(arg) if immediate ~= nil then break end end if immediate == nil then return nil end end --- @type fun(...): integer|nil local op = VALUE_OPS[operation] if not op then return nil end if rule.sources then --- @type integer[] local values = {} --- @type integer, integer for index, position in ipairs(rule.sources) do values[index] = constant_for_operand(gpr_values, ev_args[position]) if values[index] == nil then return nil end end return op(values[1], values[2]) end return op(source, immediate) end -- Apply the GPR read/write effects of one emitted event to the forward_state GPR-value lattice. -- Encoders without an explicit effect row conservatively invalidate every R_-prefixed operand. -- Recognized value rules are evaluated before their destination is invalidated. -- A failed/unknown evaluation writes `{kind = "unknown"}` instead. --- @param ev WordEvent --- @param forward_state ForwardState --- @return nil local function apply_gpr_effects(ev, forward_state) --- @type string local ev_ident = ev.encoder or ev.ident --- @type string[] local ev_args = ev.args or {} --- @type table local gpr_values = forward_state.gpr_values --- @type InstructionRow|nil local isa = duffle.instr(ev_ident) --- @type InstructionRow|nil local row = isa and (isa.reads or isa.writes) and isa or nil if row == nil and duffle.gte(ev_ident) then row = { reads = {}, writes = {} } end if row == nil then --- @type integer, string for pos, operand in ipairs(ev_args) do --- @type string local key = gpr_identity(ev, pos) or operand if type(key) == "string" and (key:sub(1, 2) == "R_" or key:sub(1, 7) == "reguse:") then if key ~= "R_0" then gpr_values[key] = { kind = "unknown" } end end end return end --- @type InstructionValue|nil local value_rule = isa and isa.value --- @type integer|nil local value = value_rule and evaluate_gpr_value_rule(value_rule, ev_args, gpr_values) or nil --- @type integer, integer for _, position in ipairs(row.writes or {}) do --- @type string|nil local destination = gpr_identity(ev, position) if destination then if value_rule and position == value_rule.dest and value ~= nil then store_gpr_constant(gpr_values, destination, value) else if destination ~= "R_0" then gpr_values[destination] = { kind = "unknown" } end end end end end -- Look up the alias of a GTE command ident. -- Defaults to the input ident so unknown idents surface rather than silently inheriting a 0-cycle command input set. --- @param ident string --- @return string local function canonical_command(ident) return duffle.gte_canon(ident) end -- True for a COP2/GTE use that can make a pending SR.CU2 transition observable. -- Atom entry intentionally starts at `unobserved`; this helper never creates a finding without a preceding Status write. --- @param ident string --- @return boolean local function is_cop2_use(ident) --- @type string local canonical = canonical_command(ident) return canonical:sub(1, 9) == "gte_cmdw_" or ident:sub(1, 4) == "gte_" end --- @param atom AtomEntry --- @param event WordEvent --- @param forward ForwardState --- @param transition Cu2Transition --- @param gap integer --- @param kind string --- @param confidence string --- @param message string --- @return nil local function append_cu2_finding(atom, event, forward, transition, gap, kind, confidence, message) --- @type string local event_ident = event.encoder or event.ident or "?" --- @type Cu2TransitionPolicy|DelaySlotPolicy|nil local policy = duffle.CU2_TRANSITION_POLICY or {} --- @type HardwareRelationEvidence local evidence = policy.evidence or {} --- @type integer local event_line = line_for_word_event(event) atom.paths.hazards[#atom.paths.hazards + 1] = { check = "transfer_hazards", kind = kind, atom = atom.name, line = event_line, source = event.def_path or event.source or "", relation_id = "mtc0_cu2_visibility", semantic = "MTC0", direction = "gpr_to_cop0_status", producer_destination = "SR.CU2", producer_word = transition.producer_word, producer_line = transition.producer_line, producer_source = transition.producer_source, consumer_word = event.i or event.word or 0, consumer_token = event_ident, gap = gap, required = transition.required, evidence_confidence = confidence, evidence_source = evidence.source or transition.evidence_source or "", target_state = transition.target_state, status_register = transition.status_register, status_value = transition.status_value, msg = message, } end -- Read `sys_mov_to_cop0(source, 12)` before applying any writes from the current event. -- A known source stages a target transition; an unknown source stages an ambiguity that is reported only if a later COP2 use reaches it. --- @param ev_ident string --- @param ev_args string[] --- @param ev_word integer --- @param ev_line integer --- @param ev_source string --- @param forward ForwardState --- @return nil local function stage_cu2_transition(ev_ident, ev_args, ev_word, ev_line, ev_source, forward) if ev_ident ~= "sys_mov_to_cop0" then return end --- @type Cu2TransitionPolicy|DelaySlotPolicy|nil local policy = duffle.CU2_TRANSITION_POLICY if not policy then return end --- @type integer|nil local status_register = parse_integer_literal(ev_args[2]) if status_register ~= policy.status_register then return end --- @type integer|nil local status_value = constant_for_operand(forward.gpr_values, ev_args[1]) --- @type string local target_state = "unknown" --- @type boolean|nil local target_enabled = nil if status_value ~= nil then target_enabled = bit_binary(status_value, policy.enable_bit, "and") ~= 0 target_state = target_enabled and "enabled" or "disabled" end forward.cu2_transition = { producer_word = ev_word, producer_line = ev_line, producer_source = ev_source, status_register = status_register, status_value = status_value, target_enabled = target_enabled, target_state = target_state, required = policy.required, evidence_source = policy.evidence and policy.evidence.source or "", } forward.cu2_state = "pending" end -- Consume a pending Status/CU2 transition at the first relevant COP2 event. -- The producer and consumer endpoints are excluded from the strict gap. -- A conservative early transition emits once and then settles to its target; -- Unknown Status emits one info edge and clears. A settled disable emits the exact COP2-unavailable finding required by the contract. --- @param atom AtomEntry --- @param event WordEvent --- @param ev_word integer --- @param forward ForwardState --- @return nil local function consume_cu2_transition(atom, event, ev_word, forward) if not is_cop2_use(event.encoder or event.ident or "") then return end --- @type Cu2Transition|nil local transition = forward.cu2_transition if not transition then return end --- @type integer local gap = ev_word - transition.producer_word - 1 --- @type string local target = transition.target_state --- @type integer local event_line = line_for_word_event(event) if target == "unknown" then append_cu2_finding(atom, event, forward, transition, gap, "info", "unknown", string.format("%s at line %d uses COP2 after an MTC0 Status write whose CU2 value is unknown (gap=%d, configured boundary=%d)" , atom.name, event_line , gap, transition.required ) ) forward.cu2_state = "unknown" forward.cu2_transition = nil return end if gap < transition.required then --- @type string local verb = target == "enabled" and "enable" or "disable" append_cu2_finding(atom, event, forward, transition, gap, "warning", "conservative", string.format("%s at line %d uses COP2 before the SR.CU2 %s transition has settled (gap=%d, required=%d; timing is conservative)" , atom.name, event_line , verb, gap, transition.required ) ) forward.cu2_state = target forward.cu2_transition = nil return end forward.cu2_transition = nil if target == "enabled" then forward.cu2_state = "enabled" else append_cu2_finding(atom, event, forward, transition, gap, "error", "exact", string.format("%s at line %d: COP2 unavailable after SR.CU2 was disabled" .. " (gap=%d, required=%d)", atom.name, event_line, gap, transition.required)) forward.cu2_state = "disabled" end end -- The forward walker. Populates `atom.paths.forward_state`, `.relations`, and `.hazards`. -- Called once per atom before the per-atom CHECK_RULES dispatch loop. --- @param atom AtomEntry --- @return nil local function analyze_hardware_relations(atom) --- @type WordEvent[] local events = atom.paths and atom.paths.word_events or {} --- @type ForwardState|nil local prior_state = atom.paths.forward_state --- @type table local seed_values = {} if prior_state and not prior_state._analysis_complete then --- @type string, GprLatticeSlot for register, slot in pairs(prior_state.gpr_values or {}) do if type(slot) == "table" and slot.kind == "constant" then seed_values[register] = { kind = "constant", value = wrap_u4(slot.value), } elseif type(slot) == "table" and slot.kind == "unknown" then seed_values[register] = { kind = "unknown" } end end end --- @type ForwardState local forward = { gpr_values = seed_values, pending = {}, cu2_state = "unobserved", cu2_transition = nil, c2_ctrl_writes = {}, _analysis_complete = false, } -- The architectural zero register is always a known U4 zero and cannot be invalidated by an emitted writer. forward.gpr_values.R_0 = { kind = "constant", value = 0 } atom.paths.forward_state = forward atom.paths.relations = {} atom.paths.hazards = {} --- @type CheckFinding[] local hazards = atom.paths.hazards --- @type RelationTouch[] local relations = atom.paths.relations --- @type PendingProducer[] local pending = forward.pending --- @type HardwareRelationRow[] local relations_table = duffle.HARDWARE_RELATIONS or {} -- Build a token-indexed lookup once per walker pass. --- @type RelationRowsByToken local rows_by_token = {} --- @type integer, HardwareRelationRow for _, row in ipairs(relations_table) do --- @type string local token = row.token if token then rows_by_token[token] = rows_by_token[token] or {} rows_by_token[token][#rows_by_token[token] + 1] = row end end --- @type integer, WordEvent for _, ev in ipairs(events) do --- @type string local ev_ident = ev.encoder or ev.ident or "?" --- @type integer local ev_line = line_for_word_event(ev) --- @type string local ev_source = ev.def_path or ev.source or "" --- @type string[] local ev_args = ev.args or {} -- `word_events` use `i` as the 0-based word index across the entire expansion. -- Default to 0 if the field is absent (the producer's own word). --- @type integer local ev_word = ev.i or 0 -- Read a Status source, then apply current-event GPR writes, then consume a pending CU2 transition at the first relevant COP2 use. -- Both operations are part of this one event walk. stage_cu2_transition(ev_ident, ev_args, ev_word, ev_line, ev_source, forward) consume_cu2_transition(atom, ev, ev_word, forward) if ev_ident == "gte_mv_to_ctrl_r" then forward.c2_ctrl_writes = forward.c2_ctrl_writes or {} --- @type string|nil local alias = ev_args[2] if type(alias) ~= "string" or not alias:match("^gte_cr_") then alias = tostring(ev.call_text or ""):match("gte_cr_[%w_]+") or tostring(ev.root_call_text or ""):match("gte_cr_[%w_]+") end --- @type string|nil local src = ev_args[1] if type(src) == "string" then src = src:match("[%w_]+") end if alias then forward.c2_ctrl_writes[#forward.c2_ctrl_writes + 1] = { alias = alias, src = src, line = ev_line or atom.line, } end end -- ── 1. Inspect pending relations against the event as CONSUMER. ── -- Walk pending in REVERSE so `table.remove` doesn't shift indexes still to be inspected. --- @type ConsumerMatchers local CONSUMER = { cop2_input = function(ev, prod) --- @type HardwareRelationRow local relation = prod.relation if relation.id == "lwc2_to_gte_command" then return is_gte_command(ev) and is_cop2_consumer_of(ev, prod.destination, relation) end if relation.id == "lwc2_to_other_consumer" then return (not is_gte_command(ev)) and is_cop2_consumer_of(ev, prod.destination, relation) end return is_cop2_consumer_of(ev, prod.destination, relation) end, gpr_read = function(ev, prod) return is_gpr_consumer_of(ev, prod.destination) end, overwrite_same_dest = function(ev, prod) --- @type string local ident = ev.encoder or ev.ident --- @type string[] local args = ev.args or {} return (ident == "gte_mv_to_data_r" or ident == "gte_mv_to_ctrl_r") and args[2] == prod.destination end, } --- @type integer for pending_idx = #pending, 1, -1 do --- @type PendingProducer local prod = pending[pending_idx] --- @type HardwareRelationRow local relation = prod.relation --- @type (fun(ev: WordEvent, prod: PendingProducer): boolean)|nil local match_fn = CONSUMER[relation.consumer] --- @type boolean|nil local is_match = match_fn and match_fn(ev, prod) if is_match then --- @type integer local gap = ev_word - prod.word - 1 --- @type integer|nil local required = prod.required -- A following COP2 command waits at the transfer boundary. -- Software nops are not required for that consumer class. if is_gte_command(ev) and relation.consumer == "cop2_input" and relation.id ~= "mtc2_irgb_visibility" and relation.id ~= "lwc2_to_gte_command" and relation.id ~= "lwc2_to_other_consumer" then required = 0 end --- @type boolean local unknown_visibility = relation.visibility and relation.visibility.kind == "unknown_consumer" if unknown_visibility then hazards[#hazards + 1] = { check = "transfer_hazards", kind = "info", atom = atom.name, line = ev_line, source = ev_source, relation_id = relation.id, semantic = relation.semantic, direction = relation.direction, producer_destination = prod.destination, producer_word = prod.word, producer_line = prod.line, producer_source = prod.source_path, consumer_word = ev_word, consumer_token = ev_ident, gap = gap, required = nil, evidence_confidence = relation.evidence and relation.evidence.confidence or "unknown", evidence_source = relation.evidence and relation.evidence.source or "", msg = string.format("%s at line %d: %s relation %s has an unknown memory-side visibility (producer %s at word %d, consumer at word %d, gap=%d) [%s]" , atom.name, ev_line, relation.semantic, relation.id , prod.destination, prod.word, ev_word, gap , (relation.evidence and relation.evidence.confidence or "unknown") ), } elseif required ~= nil and gap < required then --- @type CheckFinding local payload = { check = "transfer_hazards", kind = prod.violation_kind or "error", atom = atom.name, line = ev_line, source = ev_source, relation_id = relation.id, semantic = relation.semantic, direction = relation.direction, producer_destination = prod.destination, producer_word = prod.word, producer_line = prod.line, producer_source = prod.source_path, consumer_word = ev_word, consumer_token = ev_ident, gap = gap, required = required, evidence_confidence = relation.evidence and relation.evidence.confidence or "unknown", evidence_source = relation.evidence and relation.evidence.source or "", msg = string.format("%s at line %d: %s relation %s (producer %s at word %d, %s:%d) violated: consumer at word %d (gap=%d, required=%d) [%s]" , atom.name, ev_line, relation.semantic, relation.id , prod.destination, prod.word, prod.source_path, prod.line , ev_word, gap, prod.required , (relation.evidence and relation.evidence.confidence or "unknown") ), } -- Surface producer_command on the payload (post-command latch relations store it on the relation row. -- Copy it to the top-level payload for the renderer). if relation.producer_command then payload.producer_command = relation.producer_command end hazards[#hazards + 1] = payload end --- @type boolean|nil local satisfied = nil if not unknown_visibility then satisfied = gap >= required end -- Record the relation touch on `paths.relations` even when the gap is satisfied. -- Unknown relations are informational, not numeric pass/fail measurements. relations[#relations + 1] = { relation_id = relation.id, semantic = relation.semantic, producer_word = prod.word, consumer_word = ev_word, destination = prod.destination, gap = gap, required = required, satisfied = satisfied, } table.remove(pending, pending_idx) end end -- ── 2. Apply GPR value effects. ── apply_gpr_effects(ev, forward) -- ── 3. Stage producers created by this event. ── --- @type HardwareRelationRow[] local rows = rows_by_token[ev_ident] if rows then --- @type integer, HardwareRelationRow for _, row in ipairs(rows) do -- `stage = false` rows document a direction but do not create a later command-input producer (SWC2 and ordinary MTC0). if row.stage ~= false then --- @type integer|nil local dest_arg = row.writes and row.writes.arg --- @type string|nil local destination = dest_arg and (gpr_identity(ev, dest_arg) or ev_args[dest_arg]) or nil if destination then -- Apply the destination_match filter when present. if row.destination_match and row.destination_match ~= destination then goto continue_stage end -- A later write supersedes an unknown LWC2 edge for the same C2 destination before any command consumes it. --- @type integer for prior_idx = #pending, 1, -1 do --- @type PendingProducer local prior = pending[prior_idx] if prior.relation.semantic == "LWC2" and prior.destination == destination then table.remove(pending, prior_idx) end end --- @type integer|nil local required = row.visibility and row.visibility.required if required == nil and not (row.visibility and row.visibility.kind == "unknown_consumer") then required = 1 end pending[#pending + 1] = { relation = row, destination = destination, word = ev_word, required = required, source_path = ev_source, line = ev_line, violation_kind = row.violation_kind or "error", } end end ::continue_stage:: end end -- ── 4. Update semantic role state and stage post-command latch relations. ── -- A GTE command emits outputs with semantic roles (latest_screen_xy, otz, latest_color, etc.) per `duffle.GTE_COMMAND_OUTPUTS`. -- The walker records these on `forward_state.post_command_roles[]` so the `gte_role_mismatch` reader can later detect a reader that picks the wrong register. -- -- The walker also stages POST-COMMAND LATCH relations (kind = "command_latch_input"): a subsequent MTC2/CTC2 overwrite of a latched output before the measured boundary is a hazard. -- The relation kind is intentionally separate from the preceding MTC2 → command relation (`MTC2` / `CTC2` / `LWC2`). -- They describe different directions of the same memory subsystem and would otherwise be conflated. if canonical_command(ev_ident) ~= ev_ident then -- Not a GTE command; skip. else --- @type string local canonical = canonical_command(ev_ident) if canonical:sub(1, 9) == "gte_cmdw_" then -- Update the post-command role state. --- @type GteCommandRow|nil local gte_row = duffle.gte(canonical) --- @type GteCommandPort[]|nil local cmd_outputs = gte_row and gte_row.outputs if cmd_outputs then --- @type integer, GteCommandPort for _, out in ipairs(cmd_outputs) do if out.register then forward.post_command_roles = forward.post_command_roles or {} forward.post_command_roles[out.register] = { role = out.role, command = canonical, command_register = out.register, producer_word = ev_word, producer_line = ev_line, } end end end -- Stage post-command latch relations for every measured output. --- @type GteCommandLatch[]|nil local cmd_latches = gte_row and gte_row.latch if cmd_latches then --- @type integer, GteCommandLatch for _, latch in ipairs(cmd_latches) do if latch.register and latch.required then -- A later MTC2/CTC2 overwrite of the same register before the measured boundary is the consumer of this relation. pending[#pending + 1] = { relation = { id = "command_latch_input", semantic = "command_latch", consumer = "overwrite_same_dest", direction = "gte_command_to_cop2_register", token = canonical, evidence = { confidence = "conservative", source = "gtepipelinetimings.md", }, violation_kind = "warning", producer_command = canonical, producer_register = latch.register, }, destination = latch.register, word = ev_word, required = latch.required, source_path = ev_source, line = ev_line, violation_kind = "warning", } end end end end end end forward._analysis_complete = true end -- ───────────────────────────────────────────────────────────────────────── -- Check #1b: transfer_hazards (READER for analyze_hardware_relations output). -- -- The single forward walker `analyze_hardware_relations` (defined above) has already populated `atom.paths.hazards`. -- This check copies every entry on that list into the per-atom `findings` table. -- The first `transfer_hazards` reader comment above records the projection contract. -- -- The walker also populates `atom.paths.relations` (one entry per satisfied-or-violated relation touch) and `atom.paths.forward_state` (the GPR-value lattice). -- Neither of those is rendered as a finding here; bounded-value rules and LWC2 unknown edges share on top of the same forward walker and adds additional readers. -- -- Static-analysis pass kind remains non-stopping (diagnostic): -- The transfer-hazards findings appear in `result.errors` / `result.warnings` (according to the row's `violation_kind`) without changing the build exit status. -- This preserves the documented PASSES["static-analysis"] policy in `ps1_meta.lua`. -- ───────────────────────────────────────────────────────────────────────── --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_transfer_hazards(atom, _pipe_ctx, findings) --- @type CheckFinding[] local hazards = atom.paths and atom.paths.hazards or {} --- @type integer, CheckFinding for _, hazard in ipairs(hazards) do findings[#findings + 1] = hazard end end -- ───────────────────────────────────────────────────────────────────────── -- Check #1d: gte_input_latch (READER for analyze_hardware_relations output). -- -- The forward walker stages post-command latch relations on `atom.paths.hazards` with `relation_id = "command_latch_input"`. -- This reader filters those entries and re-emits them under the `gte_input_latch` check name so the test contract can target them independently of the transfer_hazards check. -- The first `transfer_hazards` reader comment above records the projection contract. -- ───────────────────────────────────────────────────────────────────────── --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gte_input_latch(atom, _pipe_ctx, findings) --- @type CheckFinding[] local hazards = atom.paths and atom.paths.hazards or {} --- @type integer, CheckFinding for _, hazard in ipairs(hazards) do if hazard.relation_id == "command_latch_input" then --- @type CheckFinding local payload = {} --- @type string, string|integer|boolean|nil for k, v in pairs(hazard) do payload[k] = v end payload.check = "gte_input_latch" -- Surface `producer_command` on the emitted payload: -- The hazard relation record carries it under `relation.producer_command` (since it lives on the relation row); -- copy it to the top-level payload for the renderer and the focused tests. if payload.producer_command == nil and payload.relation and payload.relation.producer_command then payload.producer_command = payload.relation.producer_command end findings[#findings + 1] = payload end end end -- ───────────────────────────────────────────────────────────────────────── -- Check #1e: gte_role_mismatch (READER for forward_state semantic roles). -- -- A GTE command emits outputs with semantic roles (latest_screen_xy, otz, latest_color, etc.) per `duffle.GTE_COMMAND_OUTPUTS`. -- The forward walker records `forward_state.post_command_roles[]` after each command. -- -- A subsequent MFC2 (or any encoder that reads a C2 register) that picks the WRONG register for the active role emits a `result_role_mismatch` warning. -- For example, reading `C2_SXY0` after RTPS is wrong: the `latest_screen_xy` role is `C2_SXY2`. -- -- Note: the OLD `gte_result_position` check also emitted table-gap info findings for `_post_` components missing a row in `duffle.GTE_COMPONENT_RESULT_CONTRACTS`. -- That table-gap check was based on the `_post_` NAMING convention rather than hardware truth, and was removed -- (the user did not want naming to encode ordering semantics; A proper `atom_info` directive for ordering semantics is a future TODO). -- -- The first `transfer_hazards` reader comment above records the projection contract. -- ───────────────────────────────────────────────────────────────────────── --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gte_role_mismatch(atom, _pipe_ctx, findings) --- @type ForwardState local forward = atom.paths and atom.paths.forward_state if not forward or not forward.post_command_roles then return end --- @type WordEvent[] local events = atom.paths.word_events or {} -- For each word event whose encoder is `gte_mv_from_data_r`, look up the register being read in `forward_state.post_command_roles`. -- If a role is set, the reader's register must match the role's register (the registered "latest_" target). --- @type integer, WordEvent for _, ev in ipairs(events) do --- @type string local ev_ident = ev.encoder if ev_ident == "gte_mv_from_data_r" then --- @type string[] local args = ev.args or {} --- @type string local reg = args[2] -- Find any post-command `latest_screen_xy` role entry recorded by a prior command. -- The newest projected screen coordinate is recorded under the command name. -- Reading from C2_SXY0 (the older projection slot) when a `latest_screen_xy` role was set to C2_SXY2 by RTPS / RTPT is a semantic mismatch. --- @type PostCommandRole|nil local latest_screen_xy_entry = nil --- @type string, PostCommandRole for r, e in pairs(forward.post_command_roles or {}) do if e.role == "latest_screen_xy" then latest_screen_xy_entry = e break end end if reg and latest_screen_xy_entry then -- The reader picked C2_SXY0 but the latest_screen_xy role was set to C2_SXY2 by the prior command. -- This is a semantic mismatch. if reg ~= latest_screen_xy_entry.command_register and (reg == "C2_SXY0" or reg == "C2_SXY1") then --- @type integer local ev_line = line_for_word_event(ev) findings[#findings + 1] = { check = "gte_role_mismatch", kind = "warning", atom = atom.name, line = ev_line, source = ev.def_path or ev.source or "", relation_id = "result_role_mismatch", semantic = "result_position", command = latest_screen_xy_entry.command, role = latest_screen_xy_entry.role, actual_register = reg, expected_register = "C2_SXY2", producer_word = latest_screen_xy_entry.producer_word, producer_line = latest_screen_xy_entry.producer_line, msg = string.format("%s at line %d: reading %s after %s but the %s role is C2_SXY2 (not %s)" , atom.name, ev_line , reg, latest_screen_xy_entry.command , latest_screen_xy_entry.role , reg), } end end end end end -- ───────────────────────────────────────────────────────────────────────── -- Check #1f: hazard_nop_use (READER for forward_state NOP classification). -- -- Each emitted `nop` word event is classified by inspecting the forward-state immediately before the word: -- * `modeled-required`: a pending modeled relation exists that the nop retires -- (the nop is needed to retire the relation, even if it can be replaced by independent useful work). -- * `modeled-redundant`: no modeled relation is pending immediately before the nop (the nop is a redundant hazard). -- -- Branch/jump delay-slot NOPs belong to `control_transfer_delay_slot_use`, so this check leaves them unclassified. -- The fixed `mac_yield()` handshake (`jump_reg(R_AtomJmp), nop`) is preserved as suppressed. -- -- Both classifications emit at `info` severity: `modeled-required` documents the model boundary and `modeled-redundant` -- is a soft observation ("you have a redundant nop; consider replacing it"). -- Neither is a logic failure, so neither rises to `warning`. -- -- `atom_dbg_skip` runtime helpers (`tape_exit`, `ac_yield`, the `ac_*` macro components) are exempt: -- their structural nops are part of the fixed handshake and not author choices. -- -- The first `transfer_hazards` reader comment above records the projection contract. -- ───────────────────────────────────────────────────────────────────────── --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_hazard_nop_use(atom, _pipe_ctx, findings) --- @type ForwardState local forward = atom.paths and atom.paths.forward_state --- @type WordEvent[] local events = atom.paths.word_events or {} -- GPR effects table used to resolve load destinations when classifying load-delay-slot nops. if not events or #events == 0 then return end -- Runtime-helper atoms / components (e.g. tape_exit, ac_yield) carry `debug_skip = true` from the bare -- `atom_dbg_skip` marker; their structural nops are part of the fixed handshake and not author choices. if is_runtime_helper(atom) then return end -- The walker does not currently snapshot the pending state per event; we replay the same forward walk cheaply here. -- The replay is observation-only (no staging); the only output is one finding per non-BD-slot nop with its classification. --- @type PendingProducer[] local pending_snapshot = {} --- @type WordEvent|nil local prev_ev = nil --- @type integer, WordEvent for event_idx, ev in ipairs(events) do --- @type string local ev_ident = ev.encoder or "" --- @type string[] local ev_args = ev.args or {} --- @type integer local ev_word = ev.i or 0 --- @type integer local ev_line = line_for_word_event(ev) -- Classify the nop BEFORE its event is applied to the pending state. if ev_ident == "nop" and prev_ev ~= nil then -- Skip BD-slot nops that are exclusively owned by control_transfer_delay_slot_use -- (the nop after a branch/jump — covered by that check separately). -- Every BD-slot nop is structural; this check never reports on it. -- (The earlier `if not suppressed then is_bd_slot = true end` form inverted the suppression - the `mac_yield()` handshake's `jump_reg(R_AtomJmp)` was incorrectly flagged.) --- @type string local prev_ident = prev_ev.encoder or "" --- @type InstructionRow|nil local prev_isa = duffle.instr(prev_ident) --- @type boolean|nil local is_bd_slot = prev_isa and (prev_isa.kind == "branch" or prev_isa.kind == "jump" or prev_isa.kind == "call") and prev_isa.delay_slot ~= false if not is_bd_slot then -- Find a pending modeled relation that this nop would retire. --- @type PendingProducer|nil local retired = nil --- @type integer, PendingProducer for _, prod in ipairs(pending_snapshot) do if prod.required and (prod.word + prod.required + 1) > ev_word then retired = prod break end end if retired then -- Look ahead for the would-be consumer (the next emitted command or read after the nop that the relation would retire). -- For an MTC2 -> command relation, the consumer is the next GTE command after the nop. --- @type string|nil local would_be_consumer = nil --- @type integer, WordEvent for _, future_ev in ipairs(events) do --- @type integer local f_word = future_ev.i or future_ev.word or 0 if f_word > ev_word then --- @type string local f_ident = future_ev.encoder or future_ev.ident or "" --- @type string[] local f_args = future_ev.args or {} --- @type GteCommandRow|nil local f_gte = duffle.gte(f_ident) --- @type string local canonical = duffle.gte_canon(f_ident) if canonical:sub(1, 9) == "gte_cmdw_" then --- @type string[]|nil local cmd_inputs = f_gte and f_gte.inputs if cmd_inputs then --- @type integer, string for _, in_reg in ipairs(cmd_inputs) do if in_reg == retired.destination then would_be_consumer = f_ident break end end end elseif f_ident == "gte_mv_to_data_r" or f_ident == "gte_mv_to_ctrl_r" then if f_args[2] == retired.destination then would_be_consumer = f_ident end end if would_be_consumer then break end end end findings[#findings + 1] = { check = "hazard_nop_use", kind = "info", atom = atom.name, line = ev_line, source = ev.def_path or ev.source or "", nop_classification = "modeled-required", nop_word_index = ev_word, retired_relation = retired.relation.id, producer_destination = retired.destination, consumer_token = would_be_consumer or "", msg = string.format("%s at line %d: nop at word %d is modeled-required (retires %s for %s)" , atom.name, ev_line, ev_word, retired.relation.id, retired.destination ), } else -- Track the slot_kind so the BD-separation case can assert the mac_yield handshake is still suppressed. --- @type string local slot_kind = "plain" -- MIPS load-delay slot: a `load_*` wrote a register in the previous slot, and the result is unavailable for 1 cycle. -- This `nop` is structurally required; classifying it as `modeled-required` is the correct signal -- (removing it would make the following instruction read the OLD value of the loaded register, a load-use hazard). -- The `load_delay_violations` check (Concern 3) catches the actual read-side error; here we suppress the `modeled-redundant` misclassification. --- @type boolean|nil local is_load_delay = prev_isa and prev_isa.kind == "load" if is_load_delay then -- Determine the destination register from the load's `writes` field. --- @type integer[] local prev_writes = prev_isa.writes or {} --- @type integer|nil local dest_pos = prev_writes[1] --- @type string local load_dest = dest_pos and (gpr_identity(prev_ev, dest_pos) or (prev_ev.args or {})[dest_pos]) or "" --- @type string local authored = dest_pos and (prev_ev.args or {})[dest_pos] or load_dest --- @type string local shown = authored if type(load_dest) == "string" and load_dest:sub(1, 7) == "reguse:" then --- @type GprLatticeSlot|nil local slot = load_dest:match("([^:]+)$") if slot then shown = authored .. " (slot " .. slot .. ")" end end findings[#findings + 1] = { check = "hazard_nop_use", kind = "info", atom = atom.name, line = ev_line, source = ev.def_path or ev.source or "", nop_classification = "modeled-required", nop_word_index = ev_word, retired_relation = "load_delay_slot", producer_destination = load_dest, consumer_token = "", msg = string.format("%s at line %d: nop at word %d is modeled-required (load-delay slot for %s)" , atom.name, ev_line, ev_word, shown ), } else findings[#findings + 1] = { check = "hazard_nop_use", kind = "info", atom = atom.name, line = ev_line, source = ev.def_path or ev.source or "", nop_classification = "modeled-redundant", nop_word_index = ev_word, retired_relation = nil, slot_kind = slot_kind, msg = string.format("%s at line %d: nop at word %d is modeled-redundant (no pending modeled relation)" , atom.name, ev_line, ev_word ), } end end end end -- Update the pending snapshot for the next iteration. -- The replay is observation-only; we mirror the walker's staging -- behavior for MTC2 / CTC2 / LWC2 / MFC2 / CFC2 / MFC0 / command_latch. --- @type string local canonical = duffle.gte_canon(ev_ident) if ev_ident == "gte_mv_to_data_r" or ev_ident == "gte_mv_to_ctrl_r" then --- @type HardwareRelationRow[] local relations_table = duffle.HARDWARE_RELATIONS or {} --- @type integer, HardwareRelationRow for _, row in ipairs(relations_table) do if row.token == ev_ident and row.stage ~= false then --- @type integer|nil local dest_arg = row.writes and row.writes.arg --- @type string|nil local destination = dest_arg and (gpr_identity(ev, dest_arg) or ev_args[dest_arg]) or nil if destination and (not row.destination_match or row.destination_match == destination) then --- @type integer|nil local required = row.visibility and row.visibility.required if required == nil and not (row.visibility and row.visibility.kind == "unknown_consumer") then required = 1 end pending_snapshot[#pending_snapshot + 1] = { relation = row, destination = destination, word = ev_word, required = required, } end end end elseif canonical:sub(1, 9) == "gte_cmdw_" then -- Command: stage post-command latch relations (same as the walker). --- @type GteCommandLatch[]|nil local cmd_latches = (duffle.gte(canonical) or {}).latch if cmd_latches then --- @type integer, GteCommandLatch for _, latch in ipairs(cmd_latches) do if latch.register and latch.required then pending_snapshot[#pending_snapshot + 1] = { relation = { id = "command_latch_input", semantic = "command_latch", consumer = "overwrite_same_dest", }, destination = latch.register, word = ev_word, required = latch.required, } end end end end prev_ev = ev end end -- ───────────────────────────────────────────────────────────────────────── -- Check #1c: control-transfer delay-slot use. -- -- Reads `atom.paths.word_events` (the semantic emitted-word stream from `passes/emission_model.lua`). -- For each event whose `encoder` is in `duffle.CONTROL_TRANSFER_DELAY_SLOT_POLICIES`, inspect the next emitted event in the SAME `events` array. -- The next event is the hardware delay-slot word (the duffle pipeline already absorbs the BD-slot into the branch's cost in `analyze_atom_paths`. -- This check observes, it does not reschedule. -- -- Emit one `info`-severity finding when: -- * the successor event is absent (no following emitted word); `slot_ident` is reported as ``; OR -- * the successor event's `ident == "nop"` (the first emitted word of `nop2` is also `nop`). -- -- Suppress the finding when `policy.suppress_arg1[first_arg]` is non-nil. -- The only current suppression is `jump_reg(R_AtomJmp)`, the fixed `mac_yield()` handshake. -- -- `atom_dbg_skip` runtime helpers (`tape_exit`, `ac_yield`, the `ac_*` macro components) are exempt: -- their BD slots are part of the fixed handshake (`jump_reg(rret_addr), nop` for tape_exit, `jump_reg(R_AtomJmp), nop` for ac_yield). -- -- `pipe_ctx` is unused; the uniform `(atom, pipe_ctx, findings)` signature is preserved so the check plugs into -- the existing CHECK_RULES dispatch without modifying the per-atom loop or analyze_atom_paths. -- `passes/emission_model` already normalizes `nop2` to two `nop` events and `atom_label` to zero events, so no special-case branching is needed for either. -- ───────────────────────────────────────────────────────────────────────── --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_control_transfer_delay_slot_use(atom, pipe_ctx, findings) --- @type WordEvent[] local events = atom.paths.word_events or {} if not events or #events == 0 then return end -- Runtime-helper atoms / components (e.g. tape_exit, ac_yield) carry `debug_skip = true` from the bare -- `atom_dbg_skip` marker; their structural BD slots are part of the fixed handshake. if is_runtime_helper(atom) then return end --- @type integer, WordEvent for event_idx, event in ipairs(events) do -- Canonical word_events use `encoder` as the leading identifier of the emitting token). -- Focused inputs may supply `ident` when constructing isolated events. --- @type string local event_ident = event.encoder or event.ident --- @type string local slot_ident_field = event.encoder and "encoder" or "ident" --- @type InstructionRow|nil local event_isa = duffle.instr(event_ident) --- @type Cu2TransitionPolicy|DelaySlotPolicy|nil local policy = event_isa and (event_isa.kind == "branch" or event_isa.kind == "jump" or event_isa.kind == "call") and event_isa.delay_slot ~= false and { family = event_isa.kind, suppress_arg1 = event_isa.suppress_arg1 } if policy then --- @type string|nil local arg1 = event.args and event.args[1] or nil --- @type string|nil local suppressed = policy.suppress_arg1 and policy.suppress_arg1[arg1] or nil if not suppressed then --- @type GprLatticeSlot|nil local slot = events[event_idx + 1] --- @type string local slot_ident = slot and (slot.encoder or slot.ident) or "" if slot == nil or (slot.encoder or slot.ident) == "nop" then -- Prefer `call_line` (the line of the `mac_X(...)` call site in the atom body) so the rendered -- finding points at the user's source, not at the vendored component body. --- @type integer local ev_line = line_for_word_event(event) findings[#findings + 1] = { atom = atom.name, line = ev_line, check = "control_transfer_delay_slot_use", kind = "info", msg = string.format("%s at line %d has `%s` whose emitted delay-slot word is `%s`; useful work may replace that no-op if its dependencies are valid on both paths" , atom.name, ev_line, event_ident, slot_ident), } end end end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #1d: load-delay slot violations (per-atom) -- �═══════════════════════════════════════════════════════════════════════════ --- Walk every emitted word event of one atom. For each `is_load` event (lw / lh / lhu / lb / lbu / lwc2), --- mark the destination register as "volatile through" the NEXT emitted slot — MIPS I R3000A load-delay --- semantics. If any subsequent event in that 1-slot window reads the volatile register, emit a `load_delay_violation` --- finding (severity: error — the load result is unavailable in the delay slot). --- --- The register becomes non-volatile again at word N+2 (the load has retired), OR sooner if a non-load instruction overwrites the register --- (the overwriter's write is the fresh producer; the load's value is shadowed and never observed by any reader). --- --- Runtime-helper atoms / components (`debug_skip == true`) are exempt from some checks, but load-delay --- safety applies to their emitted instructions as well. --- --- The walker reads `duffle.OPERAND_READ_POSITIONS[event.encoder]` to determine which args are read-source --- (the destination of a load is in `writes`, not `reads` — see `duffle.INSTRUCTION_GPR_EFFECTS`). --- The check is purely structural; it does not consult the GPR-value lattice --- (no constant propagation needed for load-delay detection — the volatility window is unconditional). --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_load_delay_slots(atom, pipe_ctx, findings) -- The load-delay check applies to every atom and component body, including debug-skipped components (`ac_*` and `atom_dbg_skip MipsAtom_(...)`). -- The `atom_dbg_skip` marker controls debugger stepping, not instruction safety. -- `atom_proc` atoms have full bodies with loads that need delay slots, so the check applies to them too. --- @type AtomPaths local p = atom.paths or {} if atom.kind ~= "atom" and atom.kind ~= "atom_proc" then return end --- @type WordEvent[] local events = p.word_events or {} if #events == 0 then return end --- @type table local read_positions = duffle.OPERAND_READ_POSITIONS or {} -- volatile_until[reg] = 1-based word_events index; the slot AFTER which the register is safe. -- `nil` means "not currently volatile". --- @type table local volatile_until = {} -- Compute the "net reads" of an event: read-positions MINUS write-positions. -- A position that is BOTH read and written (e.g. `add_ui rt, rs, imm` where the duffle table lists position 1 as both. -- See `duffle.OPERAND_READ_POSITIONS["add_ui"] = {1, 2}` and `INSTRUCTION_GPR_EFFECTS["add_ui"].writes = {1}` — -- and for genuine RMW ops like `add rt, rs, rt` where position 1 IS both read+written) is not a "read" for load-delay purposes: -- The write shadows whatever value the register previously held. Only positions that are reads WITHOUT a co-occurring write to the same register count as net reads. --- @param event_ident string --- @param args string[] --- @return integer[] local function net_reads(event_ident, args) --- @type InstructionRow|nil local effect = duffle.instr(event_ident) --- @type integer[]|nil local positions = read_positions[event_ident] if not positions then return {} end --- @type table -- bag local writes_set = {} if effect and effect.writes then --- @type integer, integer for _, pos in ipairs(effect.writes) do writes_set[pos] = true end end --- @type integer[] local net = {} --- @type integer, integer for _, pos in ipairs(positions) do if not writes_set[pos] then net[#net + 1] = pos end end return net end --- @type integer, WordEvent for event_idx, event in ipairs(events) do --- @type string local event_ident = event.encoder or event.ident --- @type string[] local args = event.args or {} --- @type InstructionRow|nil local event_isa = duffle.instr(event_ident) --- @type boolean local is_load = event_isa and event_isa.kind == "load" -- (1) Is this event reading a register that's still volatile from a previous load? -- Skip the load instruction itself (the load's own argument list may "read" its destination via `OPERAND_READ_POSITIONS`: -- e.g. `addiu rt, rs, imm` lists position 1 (rt) as a "read", but rt is the destination; the within-load argument list is not a separate consumer). -- Use `net_reads` to ignore RMW positions (write shadows read within the same instruction). if not is_load then --- @type integer, integer for _, pos in ipairs(net_reads(event_ident, args)) do --- @type string local reg = gpr_identity(event, pos) if reg then --- @type integer local until_idx = volatile_until[reg] if until_idx and event_idx <= until_idx then --- @type integer local ev_line = line_for_word_event(event) --- @type string local authored = args[pos] or reg findings[#findings + 1] = { atom = atom.name, line = ev_line, check = "load_delay_violation", kind = "error", msg = string.format("%s at line %d reads %s at word %d, but a prior load's " .. "delay slot is not over until word %d; insert a `nop` between the " .. "load and this instruction.", atom.name, ev_line, authored, event_idx, until_idx), } end end end end -- (2) Update the volatile set based on what this event writes. --- @type InstructionRow|nil local effect = event_isa if effect and effect.writes then --- @type integer, integer for _, pos in ipairs(effect.writes) do --- @type string local reg = gpr_identity(event, pos) if reg then if is_load then -- Load: destination volatile for exactly 1 slot (the delay slot). volatile_until[reg] = event_idx + 1 else -- Non-load write to this register: overwrites shadow the load; the volatile state ends. -- If another reader comes later, it sees the overwriter's value (or unknown), not the stale load value. volatile_until[reg] = nil end end end end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #2: mac_yield uniformity -- ════════════════════════════════════════════════════════════════════════════ --- Every atom body must contain exactly one `mac_yield()` call and it must be the LAST top-level token in the body --- (so the tape runtime can pick up cleanly at the next atom's bound registers). --- --- Empty bodies are not currently flagged — runtime infrastructure atoms like --- `MipsAtom_(yield) { mac_yield() }` and `MipsAtom_(tape_exit) { jump_reg(rret_addr), nop }` --- are valid as-is; mac_yield at the end is the contract. --- --- Runtime helpers carrying the bare `atom_dbg_skip` marker (`tape_exit`, `ac_yield`, the `ac_*` macro components) are exempt: --- they intentionally do not follow the standard "1 yield at the end" contract. `tape_exit` performs its own `jump_reg(rret_addr), --- nop` to return from the tape runner; `ac_yield` IS the `mac_yield()` implementation. --- Flagging them as "missing mac_yield" is signal noise, not a logic failure. --- --- Uses the standard `(atom, pipe_ctx, findings)` signature; `pipe_ctx` is unused. --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_mac_yield_uniformity(atom, pipe_ctx, findings) -- Runtime-helper atoms / components (e.g. tape_exit, ac_yield) carry `debug_skip = true` from the bare -- `atom_dbg_skip` marker; they intentionally break the "1 yield at the end" contract. if is_runtime_helper(atom) then return end -- Per-kind semantics: -- MipsAtom_ (baked atom): exactly 1 mac_yield at the end of the body. Control transfer is the atom's job. -- MipsAtom_Proc_ (runtime-proc atom): exactly 1 mac_yield at the end of the body. Same as baked atom; -- the proc IS the atom; the runtime call to `atombuilder_unroll` doesn't introduce a parent atom. -- MipsAtomComp_ (bare static-array component): ZERO mac_yield. -- The component is invoked from inside an atom body; the parent atom does the yield. -- MipsAtomComp_Proc_ (procedural component): ZERO mac_yield. -- Same reasoning -- it's a function returning a MipsAtom slice, invoked from a parent atom. -- -- The GTE pipeline-fill check applies to all 3 kinds (see check_gte_pipeline_fill). Only the mac_yield rule branches on kind. --- @type WordEvent[] local events = atom.paths.word_events or {} --- @type integer local n = #events -- Emission sets is_yield on encoder mac_yield / mac_yield_tail. -- Expanded component words keep the call_text lead; count one call, not every word. --- @param ev WordEvent --- @return boolean local function event_is_yield(ev) if ev.is_yield or ev.is_raw_yield_tail then return true end --- @type string local ident = ev.encoder or ev.ident or "" if ident == "mac_yield" or ident == "mac_yield_tail" then return true end --- @type string|nil local lead = tostring(ev.call_text or ""):match("^([%w_]+)") or tostring(ev.root_call_text or ""):match("^([%w_]+)") return lead == "mac_yield" or lead == "mac_yield_tail" end --- @type integer local count = 0 --- @type integer local last_idx = 0 --- @type table -- bag local seen_inv = {} --- @type integer for ev_idx = 1, n do --- @type WordEvent local ev = events[ev_idx] if event_is_yield(ev) then --- @type string|integer local inv_id = ev.outermost_invocation_id if inv_id == nil or inv_id == 0 then inv_id = "w" .. tostring(ev.i or ev_idx) end if not seen_inv[inv_id] then seen_inv[inv_id] = true count = count + 1 end last_idx = ev_idx end end --- @param idx integer --- @return integer local function line_for(idx) --- @type WordEvent local ev = events[idx] if ev and ev.line then return ev.line end return atom.line end if atom.kind == "atom" or atom.kind == "atom_proc" then -- Baked atom: exactly 1 yield at the end. if count == 0 then findings[#findings + 1] = { atom = atom.name, line = atom.line, check = "mac_yield_uniformity", kind = "warning", msg = string.format("%s at line %d has no `mac_yield()`; every atom must hand control to the next via mac_yield at end" , atom.name, atom.line), } elseif count > 1 then findings[#findings + 1] = { atom = atom.name, line = line_for(last_idx), check = "mac_yield_uniformity", kind = "warning", msg = string.format("%s at line %d has %d `mac_yield()` calls; exactly 1 is allowed", atom.name, line_for(last_idx), count), } elseif last_idx < n then -- 1 call, but not the last event. We DON'T fail if the post-event is just `nop` or `nop2`. -- It's the standard "yield, then BD nop" idiom. --- @type boolean local post_non_nop = false --- @type integer for search_idx = last_idx + 1, n do --- @type WordEvent local ev = events[search_idx] --- @type string local enc = ev.encoder or ev.ident or "" if (ev.nop_words or 0) == 0 and enc ~= "" then post_non_nop = true break end end if post_non_nop then findings[#findings + 1] = { atom = atom.name, line = line_for(last_idx), check = "mac_yield_uniformity", kind = "warning", msg = string.format("%s at line %d has `mac_yield()` at word %d/%d; the yield must be the LAST non-nop event in the body" , atom.name, line_for(last_idx), last_idx, n), } end end else -- Component (comp_bare or comp_proc): ZERO yields. -- The parent atom does the yield. -- A yield inside a component would either be dead code (bare) or prematurely terminate the function (proc). -- Both are bugs. -- `atom_proc` atoms are NOT components; they're runtime-proc atoms that own their own yield (handled in the `if` branch above). if count > 0 then findings[#findings + 1] = { atom = atom.name, line = line_for(last_idx), check = "mac_yield_uniformity", kind = "warning", msg = string.format("%s at line %d is a %s component but has %d `mac_yield()` call(s); components must not yield (the parent atom does)" , atom.name, line_for(last_idx), atom.kind, count), } end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #3: mac_yield_load / mac_yield_tail pairing (the lego split) -- ════════════════════════════════════════════════════════════════════════════ --- Phase 10: walks `word_events` + `markers`, not token indices. --- --- The lego split — `mac_yield_load()` in a branch BD-slot + `mac_yield_tail()` at the branch's target --- label — must be used as a pair. Otherwise `R_AtomJmp` is not loaded for the tail's `jr R_AtomJmp`, --- and the tape runtime would jump to garbage. --- --- Rules: --- 1. Every `mac_yield_load()` must be in a branch BD-slot, or sit between two `atom_label`s. --- Delay-marker events are skipped when reading prev/next events. --- 2. `mac_yield_tail()` is valid if every path that reaches it has already executed a `mac_yield_load()`. --- A load in a branch BD slot always runs. Later branches that target the tail label may carry `nop`. --- 3. `mac_yield_tail()` as the atom-end terminator (last event) is a WARNING, not an error --- (the safe default for atom-endings is `mac_yield()` which re-loads `R_AtomJmp`). --- --- Per-atom. Runtime-helper atoms (`debug_skip`) are exempt. --- Phase 10: reads invocations and markers from `atom.paths`; identifies mac_yield_load by --- `invocation.component_name == "mac_yield_load"` or `load_word` with `root_call_text` starting with "mac_yield_load". --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_yield_load_tail_pairing(atom, _pipe_ctx, findings) if atom.kind ~= "atom" and atom.kind ~= "atom_proc" then return end if is_runtime_helper(atom) then return end --- @type WordEvent[] local events = atom.paths.word_events or {} --- @type InvocationRecord[] local invs = atom.paths.invocations or {} --- @type EmissionMarker[] local markers = atom.paths.markers or {} --- @type integer local n = #events --- @type integer local inv_n = #invs if n == 0 then return end -- Build invocation lookup: inv_id -> inv record. --- @type table local inv_by_id = {} --- @type integer, InvocationRecord for _, inv in ipairs(invs) do inv_by_id[inv.id] = inv end -- Build label markers: name -> position (0-based word index of the next emitted word). -- Marker records often have nil position; derive it from the items stream. --- @type table local label_pos = {} --- @type string[] local pending_labels = {} --- @type integer, EmissionItem for _, it in ipairs(atom.paths.items or {}) do if it.kind == "label" and it.name then pending_labels[#pending_labels + 1] = it.name elseif it.kind == "word" then --- @type integer|nil local wi = it.i --- @type integer, string for _, nm in ipairs(pending_labels) do if wi ~= nil then label_pos[nm] = wi end end pending_labels = {} end end --- @type integer, EmissionMarker for _, m in ipairs(markers) do if m.kind == "label" and m.name and m.position ~= nil and label_pos[m.name] == nil then label_pos[m.name] = m.position end end -- True if an event is a delay-marker event (GteDelay_ etc.) — these emit 0 words. --- @param ev WordEvent --- @return boolean local function is_delay_marker(ev) --- @type string local enc = ev.encoder or ev.ident or "" return duffle.DELAY_MARKERS and duffle.DELAY_MARKERS[enc] == true end -- True if an event is the first word of a mac_yield_load invocation or load_word. -- An event is a mac_yield_load if: -- (a) it is an invocation with component_name == "mac_yield_load", AND ev.i == inv.start_pos (first word); OR -- (b) it is a load_word (kind == "load") AND root_call_text starts with "mac_yield_load". --- @param ev WordEvent --- @param name string --- @return boolean local function call_names(ev, name) --- @type string local enc = ev.encoder or ev.ident or "" --- @type string local rct = ev.root_call_text or ev.call_text or "" if enc == name or rct:sub(1, #name) == name then return true end --- @type string local bare = name:gsub("^mac_", "") if enc == bare then return true end --- @type InvocationRecord local inv = inv_by_id[ev.outermost_invocation_id or 0] if inv and (inv.component_name == name or inv.component_name == bare) then return (ev.i or 0) == (inv.start_pos or 0) end return false end -- word_events.kind is isa_kind (load/alu/…), not "invocation". -- A 3-word tail must match only the first word of the run. --- @param ev WordEvent --- @param ev_idx integer --- @param name string --- @return boolean local function is_named_call_first(ev, ev_idx, name) if not call_names(ev, name) then return false end if ev_idx and ev_idx > 1 then --- @type string|C2CtrlWrite|nil local prev = events[ev_idx - 1] if prev and call_names(prev, name) then return false end end return true end --- @param ev WordEvent --- @param ev_idx integer --- @return boolean local function is_yield_load_first(ev, ev_idx) if ev.is_raw_yield_load then return true end if ev.is_load or ev.kind == "load" then --- @type string local rct = ev.root_call_text or ev.call_text or "" if rct:sub(1, #"mac_yield_load") == "mac_yield_load" then return is_named_call_first(ev, ev_idx, "mac_yield_load") end end return is_named_call_first(ev, ev_idx, "mac_yield_load") end --- @param ev WordEvent --- @param ev_idx integer --- @return boolean local function is_yield_tail_first(ev, ev_idx) if ev.is_raw_yield_tail then return true end return is_named_call_first(ev, ev_idx, "mac_yield_tail") end -- Skip delay-marker events when looking for prev/next. --- @param idx integer --- @param step integer --- @return integer local function skip_delay(idx, step) --- @type integer local i = idx while i >= 1 and i <= n do --- @type WordEvent local ev = events[i] if ev and not is_delay_marker(ev) then break end i = i + step end if i < 1 or i > n then return nil end return i end -- Line for a word_event. --- @param ev WordEvent --- @return integer local function line_for(ev) return ev.call_line or ev.body_line or atom.line end -- ── Rule 1: every `mac_yield_load()` must be in a branch BD-slot, OR sit between two `atom_label`s. --- @type integer for event_idx = 1, n do --- @type WordEvent local ev = events[event_idx] if not is_yield_load_first(ev, event_idx) then goto continue_rule1 end --- @type integer local prev_i = skip_delay(event_idx - 1, -1) --- @type integer local ev_word = ev.i or 0 -- label_pos[name] = word index of the first word after that label (from items). -- Fall-through load: atom_label(A) / mac_yield_load() / atom_label(B) -- → label_pos[A] == ev_word and some label_pos[B] == ev_word + 1. --- @type string|nil local prev_label = false --- @type integer|nil local next_label_pos = nil --- @type string, integer for _, pos in pairs(label_pos) do if pos == ev_word then prev_label = true end if pos == ev_word + 1 then next_label_pos = pos end end -- Raw handshake load may sit in a GTE delay, not a BD slot or label pair. if ev.is_raw_yield_load then goto continue_rule1 end --- @type boolean local natural_fallthrough = prev_label and (next_label_pos ~= nil) if not natural_fallthrough then --- @type WordEvent|nil local prev_ev = prev_i and events[prev_i] --- @type boolean local prev_is_branch = prev_ev and ((prev_ev.kind == "branch") or (prev_ev.is_unconditional_jump == true)) if not prev_is_branch then --- @type string local prev_ident = prev_ev and (prev_ev.encoder or prev_ev.ident or "?") or "" --- @type string local next_ident = next_label_pos and ("atom_label at pos " .. next_label_pos) or "" findings[#findings + 1] = { atom = atom.name, line = line_for(ev), check = "yield_load_tail_pairing", kind = "error", msg = string.format("%s at line %d has `mac_yield_load()` at word %d but the previous event is `%s`, not a branch; and the next label is `%s`. `mac_yield_load()` must fill a branch BD-slot or sit between two `atom_label`s for the natural fall-through load." , atom.name, line_for(ev), event_idx, prev_ident, next_ident), } end end ::continue_rule1:: end -- ── Rule 2: `mac_yield_tail()` is valid if every path that reaches it already ran `mac_yield_load()`. -- Build offset map for branch target resolution. --- @type OffsetMapByEncoder local offset_map = {} --- @type integer, EmissionMarker for _, m in ipairs(markers) do if m.kind == "offset" and m.consuming_encoder and m.target then offset_map[m.consuming_encoder] = offset_map[m.consuming_encoder] or {} offset_map[m.consuming_encoder][m.target] = m.position end end -- Resolve branch target to 0-based word index. --- @param ev WordEvent --- @return integer|nil local function resolve_target(ev) --- @type string local enc = ev.encoder or ev.ident or "" --- @type OffsetTargetMap|nil local off_map = offset_map[enc] --- @type string[] local args = ev.args or {} -- Find the last non-register arg as the target name. --- @type string|nil local target_name = nil --- @type integer for i = #args, 1, -1 do --- @type string local a = tostring(args[i] or "") --- @type integer|nil local off_tgt = a:match("atom_offset%s*%([^,]+,%s*([%w_]+)") if off_tgt then target_name = off_tgt break end if a ~= "R_0" and a ~= "R_AT" and a:match("^[%w_]+$") then target_name = a break end end if off_map and target_name then --- @type integer local pos = off_map[target_name] if pos ~= nil then return pos end end -- Fallback: label marker by name. if target_name then return label_pos[target_name] end return nil end -- Check if an event is a branch. --- @param ev WordEvent --- @return boolean local function is_branch_ev(ev) return (ev.kind == "branch") or (ev.is_unconditional_jump == true) end -- Check if an event is the first word of a mac_yield_load. -- (Use same logic as is_yield_load_first above.) --- @param event_idx integer --- @return boolean local function ev_is_load_first(event_idx) --- @type WordEvent local ev = events[event_idx] return is_yield_load_first(ev, event_idx) end -- DFS to check if all paths to tail_idx have seen a load. --- @param tail_event_idx integer --- @return boolean local function load_covers_tail(tail_event_idx) --- @type boolean local reached_without = false --- @type boolean local reached_any = false --- @type integer local path_n = 0 --- @type integer local MAX_PATHS = 64 --- @param ev_idx integer --- @param saw_load boolean --- @param visited table --- @return nil local function dfs(ev_idx, saw_load, visited) if path_n >= MAX_PATHS then return end if visited[ev_idx] then return end --- @type table -- bag local vis = {} --- @type string, string|integer|boolean|nil for k, v in pairs(visited) do vis[k] = v end vis[ev_idx] = true --- @type WordEvent local ev = events[ev_idx] --- @type boolean local saw = saw_load or ev_is_load_first(ev_idx) -- BD slot (ev_idx + 1): if this is a branch, the BD slot always runs. if is_branch_ev(ev) and ev_idx + 1 <= n then saw = saw or ev_is_load_first(ev_idx + 1) end if ev_idx == tail_event_idx then path_n = path_n + 1 reached_any = true if not saw then reached_without = true end return end -- Terminators: stop. if (ev.is_yield == true) or (ev.is_terminal_jump == true) then return end -- Branches. if is_branch_ev(ev) then -- Fall-through (conditional only). if not ev.is_unconditional_jump and ev_idx + 2 <= n then dfs(ev_idx + 2, saw, vis) end -- Taken path. --- @type integer|nil local target = resolve_target(ev) if target then --- @type string|nil local dest = target + 1 -- first word after label marker if dest >= 1 and dest <= n then dfs(dest, saw, vis) end end return end -- Normal: next event. if ev_idx + 1 <= n then dfs(ev_idx + 1, saw, vis) end end dfs(1, false, {}) if not reached_any then return true end return not reached_without end -- Find mac_yield_tail first-word events and validate. --- @type integer for event_idx = 1, n do --- @type WordEvent local ev = events[event_idx] if not is_yield_tail_first(ev, event_idx) then goto continue_tail end -- Raw handshake: jump_reg(R_AtomJmp), BdSlot_ is the atom-end tail. No label required. if ev.is_raw_yield_tail then if not load_covers_tail(event_idx) then findings[#findings + 1] = { atom = atom.name, line = line_for(ev), check = "yield_load_tail_pairing", kind = "error", msg = string.format( "%s at line %d has `jump_reg(R_AtomJmp)` + BdSlot_ but no path that reaches it has loaded R_AtomJmp from R_TapePtr." , atom.name, line_for(ev)), } end goto continue_tail end -- Find the preceding label marker (must be the atom_label just before this invocation). -- The invocation starts at ev.i (0-based word index). Find the label marker whose position == ev.i. --- @type integer local ev_word = ev.i or 0 --- @type string|nil local prev_label_name = nil --- @type string, integer for name, pos in pairs(label_pos) do if pos == ev_word then prev_label_name = name break end end if not prev_label_name then if event_idx == n then findings[#findings + 1] = { atom = atom.name, line = line_for(ev), check = "yield_load_tail_pairing", kind = "warning", msg = string.format( "%s at line %d has `mac_yield_tail()` as the atom-end terminator. The safe default for atom-endings is `mac_yield()` (which re-loads R_AtomJmp). The split is for BD-slot fill, not atom-endings." , atom.name, line_for(ev)), } else findings[#findings + 1] = { atom = atom.name, line = line_for(ev), check = "yield_load_tail_pairing", kind = "error", msg = string.format( "%s at line %d has `mac_yield_tail()` at word %d but it's not the first event after an `atom_label()` — `mac_yield_tail()` must be the first event of its target label's body." , atom.name, line_for(ev), event_idx), } end goto continue_tail end if not load_covers_tail(event_idx) then findings[#findings + 1] = { atom = atom.name, line = line_for(ev), check = "yield_load_tail_pairing", kind = "error", msg = string.format( "%s at line %d has `mac_yield_tail()` at label `%s` but no path that reaches it has executed `mac_yield_load()` — R_AtomJmp would not be loaded." , atom.name, line_for(ev), prev_label_name), } end ::continue_tail:: end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #4: Binding handoff discipline -- ════════════════════════════════════════════════════════════════════════════ --- For every atom with `atom_bind(Binds_X)`, verify the atom body reads every field of `Binds_X` from R_TapePtr (in any order) --- and advances R_TapePtr by S_(Binds_X) at the end. Mismatches are errors. --- --- Binds_X is the atom phase's input payload (like a C function's argument struct). --- The body must read each input field and advance the input cursor past the payload. The order of reads doesn't matter. --- Each field is at a different offset in the struct, and the advance at the end is what keeps the tape pointer in sync. --- --- Rules: --- 1. Body MUST contain one `load_word(R_*, R_TapePtr, O_(Binds_X, field))` per field of Binds_X. Missing field = error. --- 2. Body MUST contain an `add_ui_self(R_TapePtr, S_(Binds_X))` (or equivalent advance by the struct's byte count). Missing = error. --- 3. atom_bind(Binds_X) where Binds_X doesn't exist = error. --- Per-atom: Verify the atom body reads every field of its `Binds_X` from R_TapePtr and advances R_TapePtr by S_(Binds_X). --- Takes `(atom, pipe_ctx, findings)`; `pipe_ctx` carries the cross-atom `info_by_atom` + `binds_index` tables --- (built once by validate() before the per-atom loop). --- `validate()` owns per-atom iteration; this function evaluates one atom. --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_abi_handoff(atom, pipe_ctx, findings) --- @type AtomInfoEntry|nil local info = pipe_ctx.info_by_atom[atom.name] if not info or not info.binds then return end --- @type string local binds_name = info.binds --- @type BindsEntry|nil local binds = pipe_ctx.binds_index[binds_name] if not binds then findings[#findings + 1] = { atom = atom.name, line = atom.line, check = "abi_handoff", kind = "error", msg = string.format("%s at line %d has `atom_bind(%s)` but no `typedef Struct_(%s)` declaration found in source" , atom.name, atom.line, binds_name, binds_name), } return end --- @type WordEvent[] local events = atom.paths.word_events or {} --- @type table -- bag local found_field_set = {} --- @type boolean local found_advance = false -- Reads o_arg1 / o_arg2 / s_arg1 / reads_r_tape_ptr stamped on word_events. --- @type integer, WordEvent for _, ev in ipairs(events) do -- scan: load_word(R_*, R_TapePtr, O_(, )) if ev.is_load and ev.reads_r_tape_ptr and ev.o_arg1 == binds_name then --- @type string|TypeField|nil local field = ev.o_arg2 if field then found_field_set[field] = true else --- @type integer local body_line = ev.line or atom.line findings[#findings + 1] = { atom = atom.name, line = body_line, check = "abi_handoff", kind = "error", msg = string.format("%s at line %d has load_word(R_TapePtr, O_(%s, )); expected O_(%s, )", atom.name, body_line, binds_name, binds_name), } end end -- scan: add_ui_self(R_TapePtr, S_()) if ev.reads_r_tape_ptr and ev.s_arg1 == binds_name then found_advance = true end end --- @type integer, TypeField for _, f in ipairs(binds.fields) do if not found_field_set[f.name] then findings[#findings + 1] = { atom = atom.name, line = atom.line, check = "abi_handoff", kind = "error", msg = string.format("%s at line %d binds %s but never loads field `%s` from R_TapePtr (expected O_(%s, %s))" , atom.name, atom.line, binds_name, f.name, binds_name, f.name), } end end if not found_advance then findings[#findings + 1] = { atom = atom.name, line = atom.line, check = "abi_handoff", kind = "error", msg = string.format("%s at line %d binds %s but never advances R_TapePtr by S_(%s) (= %d bytes / %d words)" , atom.name, atom.line, binds_name, binds_name, binds.bytes, binds.bytes / 0x04), } end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #4: GPU port-store shape -- ════════════════════════════════════════════════════════════════════════════ --- For every baked atom body, detect which GP0 primitive it's emitting --- (first `format__color` invocation). Sum `gp0_contrib` once per --- matching invocation (`format_*_color` / `gte_store_*` / `insert_ot_tag*`). --- Compare to duffle.GP0_CMD_SIZE[cmd_byte]. Mismatch = error. --- --- Soft behavior (warnings): --- - Atoms emitting a primitive via raw `store_word(R_PrimCursor, ...)` (no `mac_format_X_color` call) emit a "manual packet assembly" advisory. --- Cannot auto-validate. --- - Atoms containing a `mac_(...)` call whose `name` is not registered in `pipe_ctx.components_by_name` emit a "new macro; --- Not in corpus.components" advisory — the auto-derivation returned nil for that name. --- --- Applies only to `kind = "atom"` or `kind = "atom_proc"` (full-atom bodies). Components don't emit full primitives. --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gpu_portstore_shape(atom, pipe_ctx, findings) if atom.kind ~= "atom" and atom.kind ~= "atom_proc" then return end --- @type integer|nil local cmd_byte = nil --- @type integer|nil local cmd_line = nil --- @type integer local contrib = 0 --- @type boolean local saw_format = false --- @type boolean local saw_prim_write = false --- @type boolean local saw_tag = false --- @type table local comps = pipe_ctx.components_by_name or {} -- One gp0_contrib add per matching invocation. Inner store_word / gte_sw -- expansions are already inside that number; do not walk them again. --- @type integer, InvocationRecord for _, inv in ipairs(atom.paths.invocations or {}) do --- @type string local name = inv.component_name or "" --- @type string|nil local shape = name:match("^format_(.+)_color$") if shape then if not cmd_byte and duffle.GP0_CMD_BY_SHAPE[shape] then cmd_byte = duffle.GP0_CMD_BY_SHAPE[shape] cmd_line = atom.line + (inv.call_line or 0) end saw_format = true end if shape or name:match("^gte_store_") or name:match("^insert_ot_tag") then --- @type integer local n = comps[name] and comps[name].gp0_contrib if n then contrib = contrib + n end -- insert_ot_tag's derived contrib is 0 (OT list mutation). -- The packet still has a tag word; count it once. if name:match("^insert_ot_tag") and not saw_tag then contrib = contrib + 1 saw_tag = true end end end --- @type integer, WordEvent for _, ev in ipairs(atom.paths.word_events or {}) do if ev.writes_r_prim_cursor then saw_prim_write = true end -- Source-level O_(Poly_*, tag) store is the packet tag, counted once. if ev.o_arg1 and ev.o_arg1:match("^Poly_") and ev.o_arg2 == "tag" then if ev.is_store_word or ev.ident == "gte_sw" then if not saw_tag then contrib = contrib + 1 saw_tag = true end end end end -- Invocation contrib is 0 when no matching mac_* ran. Then count -- distinct PrimCursor stores. Skip this walk when contrib is non-zero. if contrib == 0 then --- @type table -- bag local seen_field = {} --- @type integer, WordEvent for _, ev in ipairs(atom.paths.word_events or {}) do --- @type string local enc = ev.encoder or "" if enc == "store_word" or enc == "store_half" or enc == "store_byte" or enc == "gte_sw" then --- @type string local text = (ev.call_text or "") .. " " .. (ev.root_call_text or "") if text:find("insert_ot_tag", 1, true) then -- OT list mutation, not a packet word. else --- @type string|TypeField|nil local field = text:match("O_%(([^%)]+)%)") or text if not seen_field[field] then --- @type boolean local hit = text:find("R_PrimCursor", 1, true) if not hit then --- @type integer, string for _, arg in ipairs(ev.args or {}) do if tostring(arg):find("R_PrimCursor", 1, true) then hit = true break end end end if hit then seen_field[field] = true contrib = contrib + 1 end end end end end end if not cmd_byte then if saw_prim_write and not saw_format then findings[#findings + 1] = { atom = atom.name, line = atom.line, check = "gpu_portstore_shape", kind = "warning", msg = string.format("%s at line %d writes to R_PrimCursor via raw store_word(...)" .. " but uses no `mac_format_*_color`; the cmd byte + word count cannot be auto-validated." .. " Consider migrating to `mac_format_X_color` + `mac_gte_store_X_post_*` + `mac_insert_ot_tag_X`." , atom.name, atom.line), } end else --- @type integer|nil local expected = duffle.GP0_CMD_SIZE[cmd_byte] if contrib ~= expected then findings[#findings + 1] = { atom = atom.name, line = cmd_line or atom.line, check = "gpu_portstore_shape", kind = "error", msg = string.format("%s at line %d emits GP0 0x%02X with %d prim word(s); expected %d (cmd 0x%02X total = %d)" , atom.name, cmd_line or atom.line, cmd_byte, contrib, expected, cmd_byte, expected), } end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #5: per-atom cycle budget (uses analyze_atom_paths's unknown_macros) -- ════════════════════════════════════════════════════════════════════════════ --- Walk all paths through an atom body and return per-path cycle sums. --- Phase 10: walks `word_events` + `markers`, not token indices. --- --- Builds a tiny CFG from the emitted word stream: --- * Labels: `paths.markers` where `kind == "label"`. Key = `name`. Position = `word_index` (next emitted word). --- * Branches: `word_events` where `kind == "branch"` or `is_unconditional_jump`. Target = offset marker --- with matching `consuming_encoder` and `target` name; fallback to label marker if no offset marker. --- * Delay slot: next `word_event` (the BD slot always runs). --- * Terminators: `is_yield` or `is_terminal_jump` on the event. `mac_yield` is 4 words — `is_yield` --- is stamped on the FIRST word of the expansion only (the invocation is one logical terminator). --- * Costs: `instr(encoder).cycles` / `gte(encoder).cycles` / `components[bare].cycle_cost` on the invocation. --- Delay-marker events (GteDelay_ etc.) cost 0. --- --- Returns: --- cycles_min - shortest path through the body (sum of event costs) --- cycles_max - longest path through the body --- branches - number of branch events (conditional + unconditional-with-offset) --- paths - number of distinct paths reached (terminated at yield / terminal_jump / end-of-body) --- has_loops - true iff a path re-entered an event it had visited (warning; loops aren't supported) --- unknown_macros - list of unique encoder names with no cost lookup --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @return nil local function analyze_atom_paths(atom, pipe_ctx) --- @type WordEvent[] local events = atom.paths.word_events or {} --- @type EmissionMarker[] local markers = atom.paths.markers or {} --- @type integer local n = #events --- @type table local comps_by_name = pipe_ctx.components_by_name or {} -- Build label map from markers: label name -> 0-based word index of the next emitted word. --- @type table local labels = {} -- Also build offset-marker lookup: [consuming_encoder][target] -> position (0-based word index). --- @type OffsetMapByEncoder local offset_map = {} --- @type integer, EmissionMarker for _, m in ipairs(markers) do if m.kind == "label" and m.name then labels[m.name] = m.position elseif m.kind == "offset" and m.name and m.consuming_encoder then offset_map[m.consuming_encoder] = offset_map[m.consuming_encoder] or {} offset_map[m.consuming_encoder][m.target] = m.position end end -- Pre-compute per-event cycle costs. -- For invocations (`mac_*`): lookup `components_by_name[bare].cycle_cost`. -- For non-invocations: lookup `instr(encoder).cycles` or `gte(encoder).cycles`. -- Delay markers (GteDelay_ etc.) cost 0; unknown encoders cost UNKNOWN_INSTRUCTION_CYCLES. --- @type integer[] local costs = {} --- @type table -- bag local unknown_set = {} --- @type integer for event_idx = 1, n do --- @type WordEvent local ev = events[event_idx] --- @type string local enc = ev.encoder or ev.ident or "" --- @type integer local cost -- Delay markers: GteDelay_ / LdSlot_ / BdSlot_ / DmaSlot_ prefix stripped by duffle_emit; -- but the event's ident still has the prefix if the encoder was not resolved. -- If the encoder is a known delay-marker prefix, cost is 0. if duffle.DELAY_MARKERS and duffle.DELAY_MARKERS[enc] then cost = 0 end if cost == nil then if enc:sub(1, 4) == "mac_" then --- @type string local bare = enc:sub(5) --- @type ComponentDef|AtomEntry|nil local comp = comps_by_name[bare] if comp and comp.cycle_cost ~= nil then cost = comp.cycle_cost else cost = duffle.UNKNOWN_INSTRUCTION_CYCLES unknown_set[enc] = true end else --- @type InstructionRow|nil local isa = duffle.instr(enc) --- @type GteCommandRow|nil local gte_cmd = duffle.gte(enc) cost = (isa and isa.cycles) or (gte_cmd and gte_cmd.cycles) if cost == nil then cost = duffle.UNKNOWN_INSTRUCTION_CYCLES unknown_set[enc] = true end end end costs[event_idx] = cost end -- Terminator / branch predicates on word_events (already classified by duffle_emit). --- @param event_idx integer --- @return boolean local function is_terminator(event_idx) --- @type WordEvent local ev = events[event_idx] return (ev.is_yield == true) or (ev.is_terminal_jump == true) end --- @param event_idx integer --- @return boolean local function is_branch(event_idx) --- @type WordEvent local ev = events[event_idx] return (ev.kind == "branch") or (ev.is_unconditional_jump == true) end --- @param event_idx integer --- @return boolean local function is_unconditional_jump(event_idx) --- @type WordEvent local ev = events[event_idx] return (ev.is_unconditional_jump == true) end -- Resolve branch target to a 0-based word index. -- Uses offset_map (offset marker with matching consuming_encoder) first; fallback to label marker. --- @param event_idx integer --- @return integer|nil local function resolve_target(event_idx) --- @type WordEvent local ev = events[event_idx] --- @type string local enc = ev.encoder or ev.ident or "" --- @type string[] local args = ev.args or {} -- Try offset marker first. --- @type OffsetTargetMap|nil local off_map = offset_map[enc] --- @type string|nil local target_name = nil if off_map then -- Extract the label name from args. The offset arg is the last arg or a named field. --- @type integer for i = #args, 1, -1 do --- @type string local a = tostring(args[i] or "") if a:match("^[%w_]+$") and a ~= "R_0" and a ~= "R_AT" then target_name = a break end end if target_name and off_map[target_name] ~= nil then return off_map[target_name] end end -- Fallback: find label marker by name in args. --- @type integer for i = #args, 1, -1 do --- @type string local a = tostring(args[i] or "") if a ~= "R_0" and a ~= "R_AT" then if labels[a] ~= nil then return labels[a] end end end return nil end -- Successor events for a given event index. -- Returns {succ_indices}, is_terminator. --- @param event_idx integer --- @return integer[], boolean local function successors(event_idx) if is_terminator(event_idx) then return {}, true -- path ends here end if is_branch(event_idx) then --- @type integer[] local succ = {} --- @type integer|nil local target_pos = resolve_target(event_idx) if is_unconditional_jump(event_idx) then -- Unconditional absolute jump: BD slot absorbed; single successor — the taken path. -- The fall-through is unreachable in this atom's execution. if target_pos then -- Label position is 0-based word index of the next emitted word after the label marker. -- target_pos + 1 is the first WORD after the label marker (the label marker itself emits 0 words). succ[#succ + 1] = target_pos + 1 end -- Literal offset (no matching offset/label marker): treat as terminator. return {}, true end -- Conditional branch: BD slot absorbed; two successors — fall-through (event_idx+2) + taken (if target known). if event_idx + 2 <= n then succ[#succ + 1] = event_idx + 2 end if target_pos then succ[#succ + 1] = target_pos + 1 end return succ, false end -- Normal event: just the next one. if event_idx + 1 <= n then return { event_idx + 1 }, false end return {}, true -- implicit end-of-body terminator end -- DFS through all paths. Track cycle sum, visited set (per path), and path count. --- @type integer local MAX_PATHS = 64 --- @type number local cycles_min = math.huge --- @type number local cycles_max = -1 --- @type integer local path_count = 0 --- @type boolean local has_loops = false --- @param event_idx integer --- @param acc integer --- @param visited table --- @return nil local function dfs(event_idx, acc, visited) if path_count >= MAX_PATHS then return end if _G._DEBUG_DFS then io.stderr:write(string.format("dfs(event_idx=%d, acc=%d)\n", event_idx, acc)) end if visited[event_idx] then has_loops = true if _G._DEBUG_DFS_LOOP then io.stderr:write(string.format(" -> LOOP at event_idx=%d (enc=%s) acc=%d\n", event_idx, events[event_idx].encoder or events[event_idx].ident or "?", acc)) end return end -- Add this event's cost. For ANY control-transfer (branch or terminator), -- ADD the BD-slot cost too — MIPS-accurate: the BD slot always runs. -- The delay slot is at event_idx+1; it is NOT in the successor list. --- @type integer local cost = costs[event_idx] if (is_branch(event_idx) or is_terminator(event_idx)) and event_idx + 1 <= n then cost = cost + costs[event_idx + 1] end --- @type integer local new_acc = acc + cost --- @type integer[], boolean local succ, term = successors(event_idx) if term then -- Terminator: record the path's cycle sum. path_count = path_count + 1 if new_acc < cycles_min then cycles_min = new_acc end if new_acc > cycles_max then cycles_max = new_acc end return end visited[event_idx] = true --- @type integer, integer for _, next_idx in ipairs(succ) do dfs(next_idx, new_acc, visited) end visited[event_idx] = nil end if n >= 1 then dfs(1, 0, {}) end -- If no paths were recorded (e.g. atom body is empty), cycles_min/max default to 0. if cycles_min == math.huge then cycles_min = 0 end if cycles_max == -1 then cycles_max = 0 end --- @type string[] local unknown_list = {} --- @type string for macro_name in pairs(unknown_set) do unknown_list[#unknown_list + 1] = macro_name end table.sort(unknown_list) -- branch_count: number of branch events (conditional + unconditional-with-offset). --- @type integer local branch_count = 0 --- @type integer for event_idx = 1, n do if is_branch(event_idx) then branch_count = branch_count + 1 end end -- Mutate atom.paths in place. --- @type AtomPaths local p = atom.paths or {} p.cycles_min = cycles_min p.cycles_max = cycles_max p.branches = branch_count p.paths = path_count p.has_loops = has_loops p.unknown_macros = unknown_list atom.paths = p end --- Per-source check that emits one finding per unknown macro seen --- (deduplicated across atoms so the warning section doesn't get spammed with N copies of the same diagnostic). --- Per-atom: emit one finding per unknown macro seen, deduplicated across atoms --- (so the warning section doesn't get spammed with N copies of the same diagnostic). --- Reuses `analyze_atom_paths`'s per-atom unknown_macros discovery, which walks tokens and computes per-token cycle costs. --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_per_atom_cycle_budget(atom, pipe_ctx, findings) --- @type AtomPaths local p = atom.paths or {} --- @type integer, string for _, name in ipairs(p.unknown_macros or {}) do --- @type string|nil local lead = name and name:match("^([%w_]+)") if duffle.DELAY_MARKERS and lead and duffle.DELAY_MARKERS[lead] then -- Delay prefixes are zero-width. Do not warn under GteDelay_ / LdSlot_ / BdSlot_ / DmaSlot_. elseif not pipe_ctx.unknown_seen[name] then pipe_ctx.unknown_seen[name] = atom.line findings[#findings + 1] = { atom = atom.name, line = atom.line, check = "per_atom_cycle_budget", kind = "warning", msg = string.format("%s at line %d uses macro `%s` with no cycle_cost lookup; " .. "cycle count will be +%d per call (best-case). For `mac_*` idents, ensure the " .. "corresponding `MipsAtomComp_(ac_X)` is in scope of the build so " .. "`passes/components.lua::compute_components_metadata` can derive its cost; " .. "for non-`mac_*` idents, add an entry to `duffle.INSTRUCTION_LATENCY`." , atom.name, atom.line, name, duffle.UNKNOWN_INSTRUCTION_CYCLES), } end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #6: enum_alias_membership -- ════════════════════════════════════════════════════════════════════════════ -- Every R_X referenced from a debug-visible surface — atom_dbg_reg_default, atom_reg_types, atom_type sub-entries, atom_reads, atom_writes; -- MUST be present in `pipe_ctx.register_alias_registry`. -- The registry is the source-derived answer to "is this R_X a real, opt-in alias?" -- (populated by scan_source's `parse_enum_aliases` from `enum { R_X = N atom_reg }` declarations). -- Per-source rule (called once per source via the CHECK_RULES dispatch). -- Signature matches the per_source shape established by check_semantic_reg_defaults. -- -- Physical GPRs are members. Opt-in atom_reg stays for aliases. --- @param reg string --- @return boolean local function is_physical_gpr(reg) return type(reg) == "string" and (reg:match("^R_T[0-7]$") ~= nil or reg:match("^R_V[01]$") ~= nil) end --- @param _src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_enum_alias_membership(_src, pipe_ctx, findings) --- @type table local reg_registry = pipe_ctx.register_alias_registry or {} -- (a) atom_dbg_reg_default(R_X, T) -- pipe_ctx.types. -- source_line is on every entry; emit the diagnostic against the default declaration's own line so the report's -- "Findings by atom" section can attribute the failure to the marker location. --- @type string, AliasEntry for reg, def in pairs(pipe_ctx.types or {}) do if not reg_registry[reg] and not is_physical_gpr(reg) then findings[#findings + 1] = { atom = "", line = def.source_line or 0, check = "enum_alias_membership", kind = "warning", msg = string.format("atom_dbg_reg_default at line %d references unknown register %q (not in register_alias_registry)" , def.source_line or 0, reg), } end end -- (b) atom_reg_types(R_X, T) + (c) atom_type(R_X, T) sub-entries both populate `ai.reg_type_overrides`. -- (d) atom_reads(R_X) + (e) atom_writes(R_X) populate the reads/writes arrays. -- All four are checked against the same registry; the per-rule dispatch iterates `ai` once and covers all three locations -- so we don't re-walk atom_infos for each sub-check. --- @type integer, AtomInfoEntry for _, ai in ipairs(pipe_ctx.atom_infos_list or {}) do --- @type integer local info_line = ai.info_line or 0 --- @type string local atom_name = ai.atom_name or "" if ai.reg_type_overrides then --- @type string for reg in pairs(ai.reg_type_overrides) do if not reg_registry[reg] and not is_physical_gpr(reg) then findings[#findings + 1] = { atom = atom_name, line = info_line, check = "enum_alias_membership", kind = "warning", msg = string.format("atom '%s' at line %d has reg_type_overrides for %q; the alias is not in register_alias_registry" , atom_name, info_line, reg), } end end end --- @type integer, string for _, reg in ipairs(ai.reads or {}) do if not reg_registry[reg] and not is_physical_gpr(reg) then findings[#findings + 1] = { atom = atom_name, line = info_line, check = "enum_alias_membership", kind = "warning", msg = string.format("atom '%s' at line %d has atom_reads for %q; the alias is not in register_alias_registry" , atom_name, info_line, reg), } end end --- @type integer, string for _, reg in ipairs(ai.writes or {}) do if not reg_registry[reg] and not is_physical_gpr(reg) then findings[#findings + 1] = { atom = atom_name, line = info_line, check = "enum_alias_membership", kind = "warning", msg = string.format("atom '%s' at line %d has atom_writes for %q; the alias is not in register_alias_registry" , atom_name, info_line, reg), } end end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #7: atom_type_consistency -- ════════════════════════════════════════════════════════════════════════════ -- Every `reg_type_overrides[R_X].type_name` (populated by BOTH `atom_reg_types(R_X, )` -- and `atom_type(R_X, )` sub-entries inside atom_reads/atom_writes) MUST resolve to a `type_name_registry` entry. -- The registry is the source-derived answer to "is this type name declared in this translation unit?" -- (populated by `typedef Struct_(...)`, `typedef Enum_(...)`, `typedef ... TSet_(...)` declarations). -- Missing type names are errors (the build stops) so the user adds the typedef before re-running. -- Per-source rule. --- @param _src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_atom_type_consistency(_src, pipe_ctx, findings) --- @type table local type_registry = pipe_ctx.type_name_registry or {} --- @type integer, AtomInfoEntry for _, ai in ipairs(pipe_ctx.atom_infos_list or {}) do --- @type integer local info_line = ai.info_line or 0 --- @type string local atom_name = ai.atom_name or "" if ai.reg_type_overrides then --- @type string, RegTypeOverride for reg, ov in pairs(ai.reg_type_overrides) do if not ov.type_name or not type_registry[ov.type_name] then findings[#findings + 1] = { atom = atom_name, line = info_line, check = "atom_type_consistency", kind = "error", msg = string.format("atom '%s' at line %d reg_type_overrides[%q] uses unknown type %q (not in type_name_registry)" , atom_name, info_line, reg, tostring(ov.type_name)), } end end end end end -- ════════════════════════════════════════════════════════════════════════════ -- Check #8: binds_no_substruct_deref -- ════════════════════════════════════════════════════════════════════════════ -- For every `load_word(R_A, R_B, O_(, ))` and matching `store_word(...)` call in every atom body, -- the `` MUST resolve to a leaf scalar of ``. A "leaf scalar" is: -- * a non-struct field with `pointer_depth >= 1` (pointer-to-struct IS a leaf — the field is a pointer; the pointee is unrelated), OR -- * a non-struct field whose type_name resolves to a typedef / enum / builtin in `type_name_registry`. -- A nested struct member (pointer_depth == 0 and type_name resolves to a `kind = "struct"` registry entry) fails the leaf-scalar test. -- The check also flags fields whose Type has no `fields` table (typedefs and enums don't have fields — any Field reference against them is bogus) -- and fields whose name doesn't appear in the resolved Type's fields array. -- -- Walks every atom's stamped `paths.word_events` -- and uses the `o_arg1` / `o_arg2` captures instead of re-matching the event text. -- Resolution consults `pipe_ctx.type_name_registry` -- (Binds_* structs are registered there by scan_source's `register_struct_type`, so a unified lookup works for both Binds_* and non-Binds structs). -- -- Severity: warning (build continues) — this catches a category of bugs -- (passing a struct by value through the tape payload) where the symptom is runtime corruption, not a compile error. -- Look up a field by name in a type's `fields` array. Returns the matching field entry, or nil if not found. -- Helper extracted to keep the caller's nesting depth <= 5 (project convention; this is the 5th nesting level: -- function -> for-atom -> for-token -> if-load/store -> if-type-resolves). --- @param type_entry TypeNameEntry --- @param field_name string --- @return TypeField|nil local function find_field_by_name(type_entry, field_name) --- @type integer, TypeField for _, f in ipairs(type_entry.fields or {}) do if f.name == field_name then return f end end return nil end -- Walk typedef aliases to the struct that owns the fields table. Depth matches propagate_type_sizes. --- @param type_name string --- @param type_registry table --- @param depth integer --- @return TypeNameEntry|nil local function resolve_type_with_fields(type_name, type_registry, depth) if depth > 8 then return nil end --- @type TypeNameEntry|nil local entry = type_registry[type_name] if not entry then return nil end if entry.fields then return entry end if entry.kind == "typedef" and entry.underlying_type and entry.underlying_type ~= "" then return resolve_type_with_fields(entry.underlying_type, type_registry, depth + 1) end return entry end -- True iff a (field, type_registry) pair is a leaf scalar (safe to dereference as a tape-payload field). -- Pointer-to-X is always a leaf; non-pointer struct members fail the leaf test. --- @param field TypeField --- @param type_registry table --- @return boolean local function is_field_leaf(field, type_registry) if field.pointer_depth and field.pointer_depth > 0 then return true end --- @type TypeNameEntry|nil local ftype_entry = type_registry[field.type_name] if ftype_entry and ftype_entry.kind == "struct" then return false end return true end --- @param _src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_binds_no_substruct_deref(_src, pipe_ctx, findings) --- @type table local type_registry = pipe_ctx.type_name_registry or {} --- @type integer, string for _, a in ipairs(pipe_ctx.atoms or {}) do --- @type WordEvent[] local events = a.paths and a.paths.word_events or {} --- @type integer, WordEvent for _, ev in ipairs(events) do if (ev.is_load or ev.is_store_word) and ev.o_arg1 and ev.o_arg2 then --- @type string|nil local type_name = ev.o_arg1 --- @type string|nil local field_name = ev.o_arg2 --- @type integer local body_line = ev.line or a.line --- @type TypeNameEntry|nil local type_entry = resolve_type_with_fields(type_name, type_registry, 1) --- @type boolean local no_fields = not type_entry or not type_entry.fields or #type_entry.fields == 0 --- @type TypeNameEntry|nil local raw_entry = type_registry[type_name] --- @type boolean local is_typedef_to_struct = raw_entry and raw_entry.kind == "typedef" and raw_entry.underlying_type and type_registry[raw_entry.underlying_type] and type_registry[raw_entry.underlying_type].fields -- kind=="struct" with zero fields is opaque (PSYQ DisplayEnv class, empty Struct_()). --- @type boolean local is_opaque_struct = type_entry and type_entry.kind == "struct" and (not type_entry.fields or #type_entry.fields == 0) --- @type boolean local skip_opaque = (no_fields and not is_typedef_to_struct) or is_opaque_struct if skip_opaque then -- leave this token elseif not type_entry or not type_entry.fields then findings[#findings + 1] = { atom = a.name, line = body_line, check = "binds_no_substruct_deref", kind = "warning", msg = string.format("atom '%s' at line %d O_(%s, %s) refers to type %q which has no fields table in type_name_registry" , a.name, body_line, type_name, field_name, type_name), } else --- @type string|TypeField|nil local field = find_field_by_name(type_entry, field_name) if not field then findings[#findings + 1] = { atom = a.name, line = body_line, check = "binds_no_substruct_deref", kind = "warning", msg = string.format("atom '%s' at line %d O_(%s, %s) does not resolve to a field of %s" , a.name, body_line, type_name, field_name, type_name), } elseif not is_field_leaf(field, type_registry) then findings[#findings + 1] = { atom = a.name, line = body_line, check = "binds_no_substruct_deref", kind = "warning", msg = string.format("atom '%s' at line %d O_(%s, %s) dereferences a non-pointer struct field of type %q; nested struct members are forbidden" , a.name, body_line, type_name, field_name, field.type_name), } end end end end end end -- ════════════════════════════════════════════════════════════════════════════ -- GTE control-register alias + RT-diagonal + TR-naming helpers and checks -- ════════════════════════════════════════════════════════════════════════════ --- Resolve a `gte_cr_` ident to its alias-group entry, or nil if the alias is in a distinct-slot group (or the alias name is not a known C2 control-register alias). --- Reads `M.GTE_CR_ALIAS_GROUPS` from `duffle.lua`. --- @param alias_name string --- @param duffle DuffleExport --- @return GteCrAliasGroup|nil local function find_alias_pair_for(alias_name, duffle) --- @type GteCrAliasGroup[] local groups = (duffle and duffle.GTE_CR_ALIAS_GROUPS) or {} --- @type integer, GteCrAliasGroup for _, group in ipairs(groups) do --- @type integer, string for _, name in ipairs(group[2] or {}) do if name == alias_name then return group end end end return nil end -- Resolve a token's source line. -- The per-token `line` is the body-relative line; `atom.line` is the source line of the atom declaration; `line_in_body` (atom.paths) maps a body-relative line to its source line. -- The arithmetic `atom.line + line_in_body[tok.rel] - 1` matches the convention used by check_abi_handoff and check_control_transfer_delay_slot_use elsewhere. --- @param atom AtomEntry --- @param token string --- @param line_in_body table --- @return integer local function atom_body_token_source_line(atom, token, line_in_body) if line_in_body == nil or token == nil or token.rel == nil then return atom.line or 0 end --- @type integer local body_line = line_in_body[token.rel] if body_line == nil then return atom.line or 0 end return (atom.line or 0) + body_line - 1 end --- @param text string --- @return string|nil local function ctrl_alias_from_text(text) return tostring(text or ""):match("gte_cr_[%w_]+") end --- @param atom AtomEntry --- @return C2CtrlWrite[] local function ctrl_writes_in_atom(atom) --- @type ForwardState|nil local fs = atom.paths and atom.paths.forward_state if fs and fs.c2_ctrl_writes then return fs.c2_ctrl_writes end --- @type C2CtrlWrite[] local out = {} --- @type integer, WordEvent for _, ev in ipairs((atom.paths and atom.paths.word_events) or {}) do if (ev.encoder or "") == "gte_mv_to_ctrl_r" then --- @type string|nil local alias = ev.args and ev.args[2] if type(alias) ~= "string" or not alias:match("^gte_cr_") then alias = ctrl_alias_from_text(ev.call_text) or ctrl_alias_from_text(ev.root_call_text) end --- @type string|nil local src = ev.args and ev.args[1] if type(src) == "string" then src = src:match("[%w_]+") end if alias then out[#out + 1] = { alias = alias, src = src, line = ev.line or atom.line, } end end end return out end -- Check #N: gte_cr_alias_writes -- Fires one warning per atom per alias-group when the atom body touches two distinct aliases from the same group. -- Aliases within a group write to the same C2 control-register slot on real silicon; cross-alias writes inside one atom body silently clobber each other. -- -- Severity: warning. Build continues. -- The libgte outer-product convention uses only RT-row aliases (which are NOT in `M.GTE_CR_ALIAS_GROUPS`), so the canonical convention does not trigger this check. --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gte_cr_alias_writes(atom, pipe_ctx, findings) --- @type GteCrAliasGroup[] local groups = pipe_ctx.gte_cr_alias_groups or {} if not next(groups) then return end --- @type WordEvent[] local events = atom.paths and atom.paths.word_events or {} if not next(events) then return end -- Encoder is gte_mv_to_ctrl_r / gte_mv_from_ctrl_r. Alias lives in ev.args -- (or call_text), not a sibling token. --- @type table local touched = {} --- @type integer, WordEvent for _, ev in ipairs(events) do --- @type string local ident = ev.encoder or ev.ident if ident == "gte_mv_to_ctrl_r" or ident == "gte_mv_from_ctrl_r" then --- @type string|nil local alias = ev.args and ev.args[2] if type(alias) ~= "string" or not alias:match("^gte_cr_") then alias = ctrl_alias_from_text(ev.call_text) or ctrl_alias_from_text(ev.root_call_text) or ctrl_alias_from_text(table.concat(ev.args or {}, ",")) end --- @type GteCrAliasGroup|nil local group = alias and find_alias_pair_for(alias, pipe_ctx.duffle) if group then touched[group[1]] = touched[group[1]] or {} touched[group[1]][#touched[group[1]] + 1] = { alias = alias, line = ev.line or atom.line, } end end end -- Fire one warning per group touched with 2+ distinct aliases. --- @type string, C2CtrlWrite[] for slot, hits in pairs(touched) do --- @type table -- bag local seen = {} --- @type C2CtrlWrite[] local distinct = {} --- @type integer, C2CtrlWrite for _, h in ipairs(hits) do if not seen[h.alias] then seen[h.alias] = true distinct[#distinct + 1] = h end end if #distinct >= 2 then --- @type string[] local aliases = {} --- @type integer, C2CtrlWrite for _, d in ipairs(distinct) do aliases[#aliases + 1] = d.alias end findings[#findings + 1] = { atom = atom.name or "", line = distinct[1].line, check = "gte_cr_alias_writes", kind = "warning", msg = string.format("atom '%s' touches %d aliases that share C2[%d]: %s; verify the intent" , atom.name or "", #distinct, slot, table.concat(aliases, ", ")), } end end end -- Check #N+1: rtdiagonal_completeness -- Fires one info per atom body when the bare `gte_cmdw_mvmva` macro is used. -- The bare macro encodes only the cmd field; the canonical libgte-2-pass shape uses `gte_cmdw_mvmva_c11_pass2_exact = 0x4A49E012` (gte.h:430). -- -- Severity: info by default. Escalates to warning when `GTE_RT_DIAGONAL_STRICT=1` env var is set (CI / production builds). -- The bare macro IS the right call for the canonical libgte outer-product convention, so this is an opt-out hint rather than a hard warning. --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_rtdiagonal_completeness(atom, _pipe_ctx, findings) --- @type string[] local tokens = atom.paths and atom.paths.tokens or {} --- @type table local line_in_body = atom.paths and atom.paths.line_in_body if not next(tokens) then return end --- @type boolean local strict = os.getenv("GTE_RT_DIAGONAL_STRICT") == "1" --- @type integer, string for _, token in ipairs(tokens) do --- @type string local ident = (token.tok or ""):match("^([%w_]+)") if ident == "gte_cmdw_mvmva" then findings[#findings + 1] = { atom = atom.name or "", line = atom_body_token_source_line(atom, token, line_in_body), check = "rtdiagonal_completeness", kind = strict and "warning" or "info", msg = string.format("atom '%s' uses the bare gte_cmdw_mvmva macro; " .. "the canonical libgte-2-pass shape is gte_cmdw_mvmva_c11_pass2_exact = 0x4A49E012 " .. "(gte.h:430). The bare macro does not encode RT23/RT31/RT32/RT33; " .. "for a full 3x3 matrix, use the dedicated literal or hand-build via enc_gte_*()." , atom.name or ""), } end end end -- Check #N+2: gte_cr_TR_naming -- Fires one info per atom body when a `gte_cr_TR[XYZ]` alias is used. -- Translation-vector registers are the only 3-letter-suffix C2 aliases (`TRX/TRY/TRZ`); an agent who reads `TRX` might typo it as `RT_X` or -- `RTX0` and either get a compile error (best case) or a build that links but routes the `ctc2` write to the wrong C2 slot. -- -- Severity: info. The convention is correct; this is a documentation-pointer check. --- @param atom AtomEntry --- @param _pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gte_cr_TR_naming(atom, _pipe_ctx, findings) --- @type string[] local tokens = atom.paths and atom.paths.tokens or {} --- @type table local line_in_body = atom.paths and atom.paths.line_in_body if not next(tokens) then return end --- @type table local touched = false --- @type integer|nil local first_line = 0 --- @type integer, string for _, token in ipairs(tokens) do --- @type string local ident = (token.tok or ""):match("^([%w_]+)") if ident and ident:match("^gte_cr_TR[XYZ]$") then touched = true if first_line == 0 then first_line = atom_body_token_source_line(atom, token, line_in_body) end end end if touched then findings[#findings + 1] = { atom = atom.name or "", line = first_line, check = "gte_cr_TR_naming", kind = "info", msg = string.format( "atom '%s' uses gte_cr_TR[XYZ]; translation-vector registers are the only " .. "3-letter-suffix C2 aliases (TRX/TRY/TRZ). See docs/gte_reference.md §" .. "\"The `gte_cmdw_mvmva_c11_pass2_exact` literal\" for the libgte outer-product " .. "convention that uses these names." , atom.name or ""), } end end --- @param src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gte_cr_alias_writes_xatom(src, pipe_ctx, findings) -- Walk tape chains once (first source only). Atoms in no chain stay per-atom. --- @type SourceFile|nil local first = pipe_ctx.source_order and pipe_ctx.source_order[1] if first and src ~= first then return end --- @type table local atoms_by_name = pipe_ctx.atoms_by_name or {} --- @type integer, string[] for _, chain in ipairs(pipe_ctx.tape_chains or {}) do --- @type table local slot_state = {} --- @type integer, string for _, name in ipairs(chain) do --- @type AtomEntry local atom = atoms_by_name[name] if atom then atom.paths = atom.paths or {} atom.paths.forward_state = atom.paths.forward_state or {} --- @type C2CtrlWrite[] local outgoing = {} --- @type string, C2CtrlWrite|nil for slot, prev in pairs(slot_state) do outgoing[slot] = prev end --- @type integer, C2CtrlWrite for _, w in ipairs(ctrl_writes_in_atom(atom)) do --- @type GteCrAliasGroup|nil local group = find_alias_pair_for(w.alias, duffle) if group then --- @type GprLatticeSlot|nil local slot = group[1] --- @type string|C2CtrlWrite|nil local prev = slot_state[slot] if prev and prev.alias ~= w.alias and prev.atom ~= atom.name then findings[#findings + 1] = { atom = atom.name or "", line = w.line, check = "gte_cr_alias_writes_xatom", kind = "warning", msg = string.format("atom '%s' writes %s to C2[%d]; atom '%s' already wrote %s" , atom.name or "", w.alias, slot, prev.atom, prev.alias), } end slot_state[slot] = { alias = w.alias, atom = atom.name, line = w.line } outgoing[slot] = slot_state[slot] end end atom.paths.forward_state.ctrl_writes_by_slot = outgoing end end end end --- @param src table --- @return table local function copy_forward_map(src) --- @type table -- bag local out = {} --- @type string, PostCommandRole for k, v in pairs(src) do out[k] = v end return out end --- @param first_idx integer --- @param rel GtePackedSlotRelation --- @return boolean local function packed_pair_is_wrong(first_idx, rel) --- @type integer local i1 = first_idx[rel.first] --- @type integer local i2 = first_idx[rel.second] return i1 and i2 and i2 < i1 end --- @param atom AtomEntry --- @param writes PackedWrite[] --- @param rel GtePackedSlotRelation --- @param findings CheckFinding[] --- @return nil local function emit_packed_finding(atom, writes, rel, findings) --- @type integer local line = atom.line --- @type integer, C2CtrlWrite for _, w in ipairs(writes) do if w.alias == rel.second or w.alias == rel.first then line = w.line break end end findings[#findings + 1] = { atom = atom.name or "", line = line, check = "gte_packed_writes", kind = "warning", msg = string.format("atom '%s' writes %s before %s on packed C2[%d]" , atom.name or "", rel.second, rel.first, rel.slot), } end -- Packed RT order. first_idx is persisted on the tape chain so a yield -- between the two halves of a packed slot still sees the earlier write. --- @param src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_gte_packed_writes(src, pipe_ctx, findings) --- @type SourceFile|nil local first = pipe_ctx.source_order and pipe_ctx.source_order[1] if first and src ~= first then return end --- @type table local atoms_by_name = pipe_ctx.atoms_by_name or {} --- @type RelationTouch[] local relations = duffle.GTE_PACKED_SLOT_RELATIONS or {} --- @type table -- bag local seen = {} --- @param atom AtomEntry --- @param first_idx integer --- @param idx integer --- @return nil local function ingest_atom(atom, first_idx, idx) atom.paths = atom.paths or {} atom.paths.forward_state = atom.paths.forward_state or {} --- @type PackedWrite[] local writes = ctrl_writes_in_atom(atom) --- @type integer local before = copy_forward_map(first_idx) --- @type integer, C2CtrlWrite for _, w in ipairs(writes) do idx = idx + 1 if first_idx[w.alias] == nil then first_idx[w.alias] = idx end end atom.paths.forward_state.packed_first_idx = copy_forward_map(first_idx) --- @type integer, GtePackedSlotRelation for _, rel in ipairs(relations) do if packed_pair_is_wrong(first_idx, rel) and not packed_pair_is_wrong(before, rel) then emit_packed_finding(atom, writes, rel, findings) end end return idx end --- @type integer, string[] for _, chain in ipairs(pipe_ctx.tape_chains or {}) do --- @type integer local first_idx = {} --- @type integer local idx = 0 --- @type integer, string for _, name in ipairs(chain) do --- @type AtomEntry local atom = atoms_by_name[name] if atom then seen[name] = true idx = ingest_atom(atom, first_idx, idx) end end end --- @type string, AtomEntry for name, atom in pairs(atoms_by_name) do if not seen[name] then ingest_atom(atom, {}, 0) end end end --- @param ev WordEvent --- @return string|nil local function ctc2_event_src(ev) if ev.gpr_keys and ev.gpr_keys[1] then return ev.gpr_keys[1] end --- @type string|nil local src = ev.args and ev.args[1] if type(src) == "string" then src = src:match("^[%w_.]+") end return src end --- @param ev WordEvent --- @return string|nil local function ctc2_event_alias(ev) --- @type string|nil local alias = ev.args and ev.args[2] if type(alias) ~= "string" or not alias:match("^gte_cr_") then alias = ctrl_alias_from_text(ev.call_text) end return alias end --- @param atom AtomEntry --- @param line integer --- @param dest string --- @param findings CheckFinding[] --- @return nil local function emit_ctc2_finding(atom, line, dest, findings) findings[#findings + 1] = { atom = atom.name or "", line = line or atom.line, check = "ctc2_chain_source_preservation", kind = "warning", msg = string.format("atom '%s' reloads %s before a later ctc2 that still names it" , atom.name or "", dest), } end --- @param events WordEvent[] --- @param start_i integer --- @param dest string --- @return string[] local function later_rt_ctc2_names(events, start_i, dest) --- @type integer for j = start_i, #events do --- @type WordEvent local later = events[j] --- @type string local later_enc = later.encoder or "" if later_enc:match("^gte_cmdw_") then return false end if later_enc == "gte_mv_to_ctrl_r" then --- @type string|nil local later_src = ctc2_event_src(later) --- @type string|nil local later_alias = ctc2_event_alias(later) if later_src == dest and later_alias and later_alias:match("^gte_cr_RT") then return true end end end return false end --- @param live table --- @return nil local function clear_rt_live(live) --- @type string, Ctc2LiveRec for gpr, rec in pairs(live) do if rec.alias and rec.alias:match("^gte_cr_RT") then live[gpr] = nil end end end -- Persist {gpr, alias} on the tape chain (same shape as Gap A slot_state). -- Intra-atom: load between two RT ctc2s that name the GPR. -- Cross-atom: load of a GPR whose RT write is still live after a yield. -- A load after the last RT ctc2 in the same atom, before the command, is a legal reload. --- @param atom AtomEntry --- @param live table --- @param findings CheckFinding[] --- @return nil local function walk_ctc2_atom(atom, live, findings) atom.paths = atom.paths or {} atom.paths.forward_state = atom.paths.forward_state or {} --- @type WordEvent[] local events = atom.paths.word_events or {} if #events > 0 then --- @type integer, WordEvent for i, ev in ipairs(events) do --- @type string local enc = ev.encoder or "" if enc == "gte_mv_to_ctrl_r" then --- @type string|nil local src = ctc2_event_src(ev) --- @type string|nil local alias = ctc2_event_alias(ev) if src and alias and alias:match("^gte_cr_RT") then live[src] = { gpr = src, alias = alias, atom = atom.name } end elseif enc == "load_word" then --- @type string|nil local dest = ctc2_event_src(ev) --- @type Ctc2LiveRec|nil local rec = dest and live[dest] if rec then --- @type boolean local from_other = rec.atom ~= atom.name if from_other or later_rt_ctc2_names(events, i + 1, dest) then emit_ctc2_finding(atom, ev.line or atom.line, dest, findings) end live[dest] = nil end elseif enc:match("^gte_cmdw_") then clear_rt_live(live) end end else --- @type string[] local tokens = atom.paths.tokens or {} --- @type integer, string for i, t in ipairs(tokens) do --- @type string local tok = t.tok or "" --- @type string local ident = tok:match("^([%w_]+)") or "" if ident == "gte_mv_to_ctrl_r" then --- @type string|nil local src = tok:match("%(%s*([%w_]+)") --- @type string|nil local alias = ctrl_alias_from_text(tok) if src and alias and alias:match("^gte_cr_RT") then live[src] = { gpr = src, alias = alias, atom = atom.name } end elseif ident == "load_word" then --- @type string|nil local dest = tok:match("%(%s*([%w_]+)") --- @type Ctc2LiveRec|nil local rec = dest and live[dest] if rec then --- @type boolean local from_other = rec.atom ~= atom.name --- @type string[] local later = false --- @type integer for j = i + 1, #tokens do --- @type string local later_tok = tokens[j].tok or "" --- @type string local later_ident = later_tok:match("^([%w_]+)") or "" if later_ident:match("^gte_cmdw_") then break end if later_ident == "gte_mv_to_ctrl_r" then --- @type string|nil local later_src = later_tok:match("%(%s*([%w_]+)") --- @type string|nil local later_alias = ctrl_alias_from_text(later_tok) if later_src == dest and later_alias and later_alias:match("^gte_cr_RT") then later = true break end end end if from_other or later then emit_ctc2_finding(atom, atom.line, dest, findings) end live[dest] = nil end elseif ident:match("^gte_cmdw_") then clear_rt_live(live) end end end atom.paths.forward_state.ctc2_chain_live = copy_forward_map(live) end --- @param src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_ctc2_chain_source_preservation(src, pipe_ctx, findings) --- @type SourceFile|nil local first = pipe_ctx.source_order and pipe_ctx.source_order[1] if first and src ~= first then return end --- @type table local atoms_by_name = pipe_ctx.atoms_by_name or {} --- @type table -- bag local seen = {} --- @type integer, string[] for _, chain in ipairs(pipe_ctx.tape_chains or {}) do --- @type table local live = {} --- @type integer, string for _, name in ipairs(chain) do --- @type AtomEntry local atom = atoms_by_name[name] if atom then seen[name] = true walk_ctc2_atom(atom, live, findings) end end end --- @type string, AtomEntry for name, atom in pairs(atoms_by_name) do if not seen[name] then walk_ctc2_atom(atom, {}, findings) end end end -- check_immediate_field_width — flags integer literals passed to instruction -- macros that exceed the immediate field width. Reads `IMMEDIATE_FIELD_WIDTHS` -- from duffle.lua. Only fires on parseable integer literals; register names, -- O_(...) offsets, atom_offset(...) markers, and enum tokens are skipped. --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_immediate_field_width(atom, pipe_ctx, findings) --- @type WordEvent[] local events = atom.paths and atom.paths.word_events or {} --- @type (fun(ev: WordEvent): integer)|nil local line_for_word_event = pipe_ctx.line_for_word_event --- @type integer, WordEvent for _, ev in ipairs(events) do --- @type string local ev_ident = ev.encoder or ev.ident or "?" --- @type InstructionRow|nil local isa = duffle.instr(ev_ident) --- @type InstructionImm[]|nil local rules = isa and isa.imm if rules then --- @type string[] local ev_args = ev.args or {} --- @type integer local ev_line = line_for_word_event and line_for_word_event(ev) or atom.line --- @type integer, InstructionImm for _, rule in ipairs(rules) do --- @type string|nil local arg_str = ev_args[rule.arg] if arg_str then --- @type integer|nil local value = parse_integer_literal(arg_str) if value then --- @type integer local width = rule.width --- @type boolean local is_signed = rule.signed == true -- parse_integer_literal returns a U4-wrapped value in [0, 2^32). -- For signed fields, re-interpret the high bit as the sign. --- @type integer local signed_value = value if is_signed and value >= 0x80000000 then signed_value = value - 0x100000000 end --- @type integer, integer local lo, hi if is_signed then lo = -(bit.lshift(1, width - 1)) hi = bit.lshift(1, width - 1) - 1 else lo = 0 hi = bit.lshift(1, width) - 1 end -- For unsigned fields, a negative C literal (high bit set in U4) -- is valid if the low `width` bits fit — IMM_MASK truncates it. -- Flag as a warning (code smell), not an error. --- @type integer local check_value = is_signed and signed_value or value --- @type integer local field_max = bit.lshift(1, width) - 1 --- @type boolean local low_bits_fit = (value % (bit.lshift(1, width))) == value or (is_signed and signed_value >= lo and signed_value <= hi) if is_signed then if signed_value < lo or signed_value > hi then findings[#findings + 1] = { check = "immediate_field_width", kind = "error", atom = atom.name, line = ev_line, msg = string.format("%s: immediate %d at arg %d overflows %d-bit %s field (valid %d..%d)" , ev_ident, signed_value, rule.arg, width, "signed", lo, hi), } end else -- Unsigned field: check if the low `width` bits exceed the field. -- A negative C literal (U4 >= 0x80000000) whose low bits fit is -- valid but a code smell — warn, don't error. --- @type integer local low_bits = value % (bit.lshift(1, width)) if value > field_max then if value >= 0x80000000 and low_bits <= field_max then findings[#findings + 1] = { check = "immediate_field_width", kind = "warning", atom = atom.name, line = ev_line, msg = string.format("%s: negative immediate %d at arg %d on unsigned %d-bit field (truncated to %d by IMM_MASK)" , ev_ident, signed_value, rule.arg, width, low_bits), } else findings[#findings + 1] = { check = "immediate_field_width", kind = "error", atom = atom.name, line = ev_line, msg = string.format("%s: immediate %d at arg %d overflows %d-bit unsigned field (valid 0..%d)" , ev_ident, value, rule.arg, width, field_max), } end end end end end end end end end -- Atom-body temps may be omitted from atom_reads / atom_writes. -- Physical names come from auto_reg.POOL (R2-R25). R_AT is never allocated. -- R_TapePtr / R_AtomJmp are reserved carriers; yield always touches them, -- so they are optional in the contract unless the atom listed them. -- R_ScratchBase stays required when used. --- @type AutoRegPass local auto_reg = require("passes.auto_reg") --- @type table -- bag local OPTIONAL_CONTRACT_GPRS = { R_AT = true, R_TapePtr = true, R_AtomJmp = true } --- @type integer, string for _, name in ipairs(auto_reg.POOL) do OPTIONAL_CONTRACT_GPRS[name] = true end --- @param tok string --- @return string[] local function token_arg_list(tok) --- @type string|nil local inner = (tok or ""):match("%b()") if not inner then return {} end return duffle.split_top_level_commas(inner:sub(2, -2)) end --- @param arg string --- @return string|nil local function arg_as_gpr(arg) arg = duffle.trim(arg or "") return arg:match("^R_[%w_]+$") end --- @param ev WordEvent|Token|string --- @return string, string[] local function traffic_ident_args(ev) if type(ev) == "table" and (ev.encoder or ev.ident) then return ev.encoder or ev.ident or "", ev.args or {} end --- @type string local tok = (type(ev) == "table" and ev.tok) or ev if type(tok) ~= "string" then return "", {} end return tok:match("^([%w_]+)") or "", token_arg_list(tok) end --- @param atom_or_tokens AtomEntry|WordEvent[]|BodyToken[] --- @return table, table local function collect_gpr_traffic(atom_or_tokens) --- @type table, table -- bag local reads, writes = {}, {} --- @type WordEvent[] local events = {} if type(atom_or_tokens) == "table" then if atom_or_tokens.paths and atom_or_tokens.paths.word_events then events = atom_or_tokens.paths.word_events elseif atom_or_tokens.word_events then events = atom_or_tokens.word_events else events = atom_or_tokens end end --- @type integer, WordEvent for _, ev in ipairs(events) do --- @type string, string[] local ident, args = traffic_ident_args(ev) if ident:sub(1, 4) ~= "mac_" and not (duffle.DELAY_MARKERS and duffle.DELAY_MARKERS[ident]) and ident ~= "nop" and ident ~= "atom_label" and ident ~= "atom_offset" then --- @type InstructionRow|nil local fx = duffle.instr(ident) if fx then --- @type integer, integer for _, pos in ipairs(fx.reads or {}) do --- @type string|nil local g = arg_as_gpr(args[pos]) if g then reads[g] = true end end --- @type integer, integer for _, pos in ipairs(fx.writes or {}) do --- @type string|nil local g = arg_as_gpr(args[pos]) if g then writes[g] = true end end else --- @type integer, string for _, arg in ipairs(args) do --- @type string|nil local g = arg_as_gpr(arg) if g then reads [g] = true writes[g] = true end end end end end return reads, writes end --- @param list string[]|nil --- @return table local function gpr_set_from_list(list) --- @type table -- bag local s = {} --- @type integer, string for _, name in ipairs(list or {}) do if type(name) == "string" then s[name] = true end end return s end --- @param a table --- @param b table --- @return boolean local function gpr_set_eq(a, b) --- @type string for k in pairs(a) do if not b[k] then return false end end --- @type string for k in pairs(b) do if not a[k] then return false end end return true end --- @param s table --- @return string[] local function gpr_set_keys(s) --- @type string[]|nil local keys = {} --- @type string for k in pairs(s) do keys[#keys + 1] = k end table.sort(keys) return keys end --- @param atom AtomEntry --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_atom_calls_inferred_traffic(atom, pipe_ctx, findings) if atom.kind ~= "atom" and atom.kind ~= "atom_proc" then return end if is_runtime_helper(atom) then return end --- @type AtomInfoEntry|nil local info = pipe_ctx.info_by_atom and pipe_ctx.info_by_atom[atom.name] if not info then return end if #(info.reads or {}) == 0 and #(info.writes or {}) == 0 then return end --- @type BodyToken[]|Token[] local tokens = (atom.paths and atom.paths.tokens) or atom.body_tokens --- @type table, table -- bag local reads, writes = collect_gpr_traffic(atom) --- @type integer, string for _, t in ipairs(tokens or {}) do --- @type string local ident = ((t.tok or t) or ""):match("^([%w_]+)") or "" if ident:sub(1, 4) == "mac_" then --- @type string local bare = ident:sub(5) --- @type ComponentBodyEntry|nil local idx = pipe_ctx.component_body_index and pipe_ctx.component_body_index[bare] --- @type ComponentDef|AtomEntry|nil local comp = (pipe_ctx.components_by_name or {})[bare] or (pipe_ctx.atoms_by_name or {})[bare] --- @type BodyToken[]|nil local body_toks = (idx and idx.body_tokens) or (comp and (comp.body_tokens or (comp.paths and comp.paths.tokens))) --- @type table, table -- bag local cr, cw = collect_gpr_traffic(body_toks) --- @type string for k in pairs(cr) do reads [k] = true end --- @type string for k in pairs(cw) do writes[k] = true end end end --- @type table -- bag local decl_r = gpr_set_from_list(info.reads) --- @type table -- bag local decl_w = gpr_set_from_list(info.writes) --- @param inferred table --- @param declared table --- @return table local function keep_inferred(inferred, declared) --- @type table -- bag local out = {} --- @type string for k in pairs(inferred) do if k == "R_0" or OPTIONAL_CONTRACT_GPRS[k] then if declared[k] then out[k] = true end else out[k] = true end end return out end reads = keep_inferred(reads, decl_r) writes = keep_inferred(writes, decl_w) if not gpr_set_eq(decl_r, reads) or not gpr_set_eq(decl_w, writes) then findings[#findings + 1] = { atom = atom.name, line = info.info_line or atom.line, check = "atom_calls_inferred_traffic", kind = "warning", msg = string.format("atom '%s' declared [%s]/[%s] != inferred [%s]/[%s]" , atom.name , table.concat(gpr_set_keys(decl_r), ",") , table.concat(gpr_set_keys(decl_w), ",") , table.concat(gpr_set_keys(reads), ",") , table.concat(gpr_set_keys(writes), ",")) } end end --- @param src SourceFile --- @param pipe_ctx PipeCtx --- @param findings CheckFinding[] --- @return nil local function check_component_self_consistency(src, pipe_ctx, findings) --- @type SourceFile|nil local first = pipe_ctx.source_order and pipe_ctx.source_order[1] if first and src ~= first then return end --- @type AtomInfoEntry[] local infos = pipe_ctx.component_atom_infos or {} --- @type table local atoms_by_name = pipe_ctx.atoms_by_name or {} --- @type integer, AtomInfoEntry for _, ai in ipairs(infos) do --- @type string local name = ai.atom_name or ai.name --- @type AtomEntry local atom = name and atoms_by_name[name] if atom and not atom.debug_skip then --- @type BodyToken[]|Token[] local tokens = (atom.paths and atom.paths.tokens) or atom.body_tokens --- @type table, table -- bag local reads, writes = collect_gpr_traffic(tokens) --- @type table -- bag local decl_r = gpr_set_from_list(ai.reads) --- @type table -- bag local decl_w = gpr_set_from_list(ai.writes) if not gpr_set_eq(decl_r, reads) or not gpr_set_eq(decl_w, writes) then findings[#findings + 1] = { atom = name, line = ai.info_line or atom.line, check = "component_self_consistency", kind = "warning", msg = string.format("component '%s' atom_reads/atom_writes [%s]/[%s] != body [%s]/[%s]" , name , table.concat(gpr_set_keys(decl_r), ",") , table.concat(gpr_set_keys(decl_w), ",") , table.concat(gpr_set_keys(reads), ",") , table.concat(gpr_set_keys(writes), ",")) } end end end end -- CHECK_RULES — data-driven check dispatch (Muratori: data over control flow) -- ════════════════════════════════════════════════════════════════════════════ -- Each rule is a table entry: { name, }. -- Dispatch shapes: -- per_atom(atom, pipe_ctx, findings) — runs once per atom inside validate()'s single loop -- post(pipe_ctx, findings) — runs once after all per-atom calls complete -- per_macro(macro, wc, findings) — runs once per TAPE_WORDS / _Pragma macro declaration -- per_skip_marker(marker, pipe_ctx, findings) — runs once per src.scan.debug_skip_markers entry -- per_source(src, pipe_ctx, findings) — runs once per source AFTER the per-atom loop completes -- (registry-driven rule; same CHECK_RULES table) -- Each check is one table row and one `check_*` function. -- This is the plex pattern: the iteration is in ONE place (validate), the variation is in DATA (this table). --- @type CheckRule[] local CHECK_RULES = { { name = "transfer_hazards", per_atom = check_transfer_hazards }, { name = "gte_input_latch", per_atom = check_gte_input_latch }, { name = "gte_role_mismatch", per_atom = check_gte_role_mismatch }, { name = "hazard_nop_use", per_atom = check_hazard_nop_use }, { name = "control_transfer_delay_slot_use", per_atom = check_control_transfer_delay_slot_use }, { name = "load_delay_violation", per_atom = check_load_delay_slots }, { name = "mac_yield_uniformity", per_atom = check_mac_yield_uniformity }, { name = "yield_load_tail_pairing", per_atom = check_yield_load_tail_pairing }, { name = "abi_handoff", per_atom = check_abi_handoff }, { name = "gpu_portstore_shape", per_atom = check_gpu_portstore_shape }, { name = "per_atom_cycle_budget", per_atom = check_per_atom_cycle_budget }, { name = "gte_cr_alias_writes", per_atom = check_gte_cr_alias_writes }, { name = "gte_cr_alias_writes_xatom", per_source = check_gte_cr_alias_writes_xatom }, { name = "gte_packed_writes", per_source = check_gte_packed_writes }, { name = "ctc2_chain_source_preservation", per_source = check_ctc2_chain_source_preservation }, { name = "rtdiagonal_completeness", per_atom = check_rtdiagonal_completeness }, { name = "gte_cr_TR_naming", per_atom = check_gte_cr_TR_naming }, { name = "immediate_field_width", per_atom = check_immediate_field_width }, { name = "enum_alias_membership", per_source = check_enum_alias_membership }, { name = "atom_type_consistency", per_source = check_atom_type_consistency }, { name = "binds_no_substruct_deref", per_source = check_binds_no_substruct_deref }, { name = "component_self_consistency", per_source = check_component_self_consistency }, { name = "atom_calls_inferred_traffic", per_atom = check_atom_calls_inferred_traffic }, } -- ════════════════════════════════════════════════════════════════════════════ -- Per-source validation -- ════════════════════════════════════════════════════════════════════════════ --- Build the corpus-wide pipe_ctx ONCE per pass run. --- Reads the merged `corpus.*` registries and the corpus-wide `atom_infos` list (preserving source order + duplicates). --- The corpus supplies shared registries; `src.scan` and per-source projections retain body and declaration ownership. --- --- A context without `ctx.shared.corpus` is rejected with an explicit corpus message. --- Callers construct the context through `build_ctx`. --- @param ctx PassCtx --- @return PipeCtx local function build_corpus_pipe_ctx(ctx) --- @type CorpusView local view = duffle.corpus_view(ctx) view.components_by_name = view.components view.atom_infos_list = view.atom_infos view.gte_cr_alias_groups = duffle.GTE_CR_ALIAS_GROUPS or {} return view end --- @param ctx PassCtx --- @param src SourceFile --- @param corpus_pipe_ctx PipeCtx --- @return ValidateResult local function validate(ctx, src, corpus_pipe_ctx) --- @type SourceScan local scan = src.scan -- Read the corpus word_counts for the per-atom pipeline -- (`atom.paths.word_events` is the emitted projection). --- @type Corpus local corpus = (ctx.shared and ctx.shared.corpus) or {} -- Read atoms + binds + atom_infos from the pre-scanned SourceScan payload. -- The scan was done once upstream by duffle.scan_source(); this pass is pure. --- @type AtomEntry[] local atoms = scan.atoms --- @type AtomInfoEntry[] local atom_infos = scan.atom_infos -- Build per-source Binds_* index. Local to validate() — no cross-source sharing. --- @type table local binds_index = {} --- @type integer, BindsEntry for _, b in ipairs(scan.binds) do binds_index[b.name] = b end -- pipe_ctx: the cross-atom shared state for the per-atom pipeline (Fleury "expose structure"). -- Pre-allocated here, mutated by each per-atom check call below. -- Cross-source lookup tables come from `corpus_pipe_ctx` (built once per pass); -- source-local body / declaration ownership comes from `src.scan`. -- info_by_atom — atom_name -> atom_info (built once; check_abi_handoff reads it) -- binds_index — Binds_X -> binds struct (built once; check_abi_handoff reads it) -- unknown_seen — macro_name -> first atom line (accumulated across atoms; check_per_atom_cycle_budget dedups) -- atoms — full atom list (used by check_binds_no_substruct_deref's per-source body walk) -- types — R_X -> default-type info from atom_dbg_reg_default (check_enum_alias_membership source a) -- atom_infos_list — per-source flat list of atom_info entries (checks #6/#7 iterate it) -- register_alias_registry — R_X -> {name, code, has_atom_reg, source_line} from corpus-wide merge -- type_name_registry — T -> {name, kind, fields, ...} from corpus-wide merge -- All registry fields are READ from the corpus (the dep-closed scan-source merge); this pass never re-parses. --- @type table local info_by_atom = {} --- @type integer, CheckFinding[] for _, info in ipairs(atom_infos) do info_by_atom[info.atom_name] = info end --- @type PipeCtx local pipe_ctx = { info_by_atom = info_by_atom, binds_index = binds_index, unknown_seen = {}, atoms = atoms, types = scan.types or {}, atom_infos_list = atom_infos or {}, register_alias_registry = corpus_pipe_ctx.register_alias_registry, type_name_registry = corpus_pipe_ctx.type_name_registry, -- Per-component metadata (cycle_cost + gp0_contrib) auto-derived from the original `MipsAtomComp_` body by `passes/components.lua::compute_components_metadata`. components_by_name = corpus_pipe_ctx.components_by_name, atoms_by_name = corpus_pipe_ctx.atoms_by_name, tape_chains = corpus_pipe_ctx.tape_chains, source_order = corpus_pipe_ctx.source_order, component_atom_infos = corpus_pipe_ctx.component_atom_infos, atom_infos_all = corpus_pipe_ctx.atom_infos, } -- Shared cross-source component-body index is owned by the corpus (`corpus.component_body_index`, populated by `passes/components.lua`). -- Per-atom checks consume the corpus-owned index directly. pipe_ctx.component_body_index = (corpus and corpus.component_body_index) or {} --- Per-atom pipeline. ONE iteration of atoms; the 5 check_* functions + analyze_atom_paths all run here, sharing a single tokenize_body + build_body_line_index per body. --- Every piece of state derived from an atom body lives on `atom.paths` (per-atom mega-struct); --- readers (analyze_atom_paths, the 5 checks, the renderers) all consume `atom.paths`. --- Each `check_*` function accepts one atom and its shared context. --- Per-source rules run once after this loop completes (no parallel dispatch table). --- --- Body, token, and emission projections come from here (`paths.tokens = body_tokens`, `paths.line_in_body = build_body_line_index` `paths.word_events` --- and related fields are owned by `passes/emission_model.lua` pass (per-atom emission projection). --- This pass reads: `paths.tokens`, `paths.line_in_body`, `paths.items`, `paths.word_events` from the emitted projection, --- then stamps word-event fields and computes `paths.cycles_min/max`, `paths.branches`, `paths.paths`, `paths.has_loops`, `paths.unknown_macros` via `stamp_event_fields` + `analyze_atom_paths`. --- No re-walk of body text or body_tokens happens here. --- --- Canonical contract: `atom.paths` and `atom.paths.word_events` MUST be populated by `passes/emission_model.run(ctx)` before this pass runs. --- The `atom.paths.word_events` projection is owned by the emission-model pass; static-analysis reads it directly. --- @type CheckFinding[] local findings = {} --- @type integer, AtomEntry for _, a in ipairs(atoms) do if a.paths == nil then error("static_analysis: a.paths is nil; emit emission-model first") end if a.paths.word_events == nil then error("static_analysis: a.paths.word_events is nil; emit emission-model first") end -- `paths.tokens` / `paths.line_in_body` / `paths.items` / `paths.word_events` are populated by `passes/emission_model.lua`. -- Supply tokens when no emission projection is present. if a.paths.tokens == nil then a.paths.tokens = a.body_tokens end stamp_event_fields(a.paths.word_events) stamp_raw_yield_handshake(a) -- analyze_atom_paths fills the *cycles / branches / has_loops / unknown_macros* fields of a.paths. analyze_atom_paths(a, pipe_ctx) -- Run the single forward walker for transfer-hazard policy. -- Runs once per atom BEFORE the CHECK_RULES per-atom dispatch so the `transfer_hazards` reader (`check_transfer_hazards`) can -- project `atom.paths.hazards` into `findings` without re-walking source. -- The walker owns `atom.paths.{forward_state, relations, hazards}`; readers never re-iterate events or re-classify tokens. analyze_hardware_relations(a) -- Run all per-atom checks on this one atom via the CHECK_RULES data table. -- Adding a new check = 1 row in CHECK_RULES; this loop never needs editing. duffle.run_check_rules(CHECK_RULES, "per_atom", a, pipe_ctx, findings) end -- Per-source dispatch. Run once per source AFTER the per-atom loop; -- consults pipe_ctx's cross-atom registries (register_alias_registry, type_name_registry). -- Same CHECK_RULES table; no parallel dispatch table. duffle.run_check_rules(CHECK_RULES, "per_source", src, pipe_ctx, findings) -- Three-way severity binning: per-finding severity is set by the check via `f.kind`. -- "error" / "warning" / "info" are all distinct; info findings are NEVER folded into warnings. -- Keep error, warning, and info findings in distinct buckets so the control-transfer delay-slot check remains distinct from warnings.) -- The `info` list returned here is finding-level only; scan/cycle summary lines go into `summaries`. -- An invalid/missing kind is a hard error (no silent fallback to info); this prevents typos like -- kind="warn" or omitted kind fields from being misclassified as info in the rendered report. --- @type CheckFinding[] local errors = {} --- @type CheckFinding[] local warnings = {} --- @type CheckFinding[] local info = {} --- @type integer, CheckFinding for _, f in ipairs(findings) do -- Preserve the diagnostic context so focused tests + the renderer can route by the originating check or relation id. -- Hazard readers (transfer_hazards) populate `f.check`, `f.relation_id`, `f.semantic`, `f.direction`, `f.producer_destination`, `f.gap`, `f.required`, `f.evidence_confidence`, etc.; -- Copying them through keeps the per-severity bucket schema compatible with the renderer while making the diagnostic payload queryable. --- @type CheckFinding local payload = { line = f.line, msg = f.msg, check = f.check, atom = f.atom, source = f.source, relation_id = f.relation_id, semantic = f.semantic, direction = f.direction, producer_destination = f.producer_destination, producer_word = f.producer_word, producer_line = f.producer_line, producer_source = f.producer_source, consumer_word = f.consumer_word, consumer_token = f.consumer_token, gap = f.gap, required = f.required, evidence_confidence = f.evidence_confidence, evidence_source = f.evidence_source, } -- Preserve relation fields such as target_state and status_register status_value, -- and future policy metadata) without making the binner another semantic walker. --- @type string, integer|nil for key, value in pairs(f) do if payload[key] == nil then payload[key] = value end end if f.kind == "error" then errors [#errors + 1] = payload elseif f.kind == "warning" then warnings[#warnings + 1] = payload elseif f.kind == "info" then info [#info + 1] = payload else error(string.format("invalid finding kind %s for check %q (atom=%s, line=%d); expected one of \"error\", \"warning\", \"info\"" , tostring(f.kind), tostring(f.check), tostring(f.atom), f.line or 0), 0) end end -- Per-source "scanned:" / "cycles:" summary lines. These are SCANNER / BUDGET rollups, not findings; They belong in their own collection so the report can render them -- AS summary rows (after Module findings) rather than mixed into the Info finding section. --- @type ScanSummary[] local summaries = {} -- Per-source "scanned:" summary line. -- Includes the source basename for traceability -- Include the source basename so multi-source module summaries remain identifiable. -- Sources with 0 atoms (pure-header files like dsl.h, mips.h, etc.) are SKIPPED. -- The per-module header already lists them in the "Sources:" section, and emitting a noisy "0 atom bodies" line per header is just clutter. if #atoms > 0 or #findings > 0 then summaries[#summaries + 1] = { line = 0, msg = string.format("scanned: %s: %d atom bodies; %d findings", src.basename, #atoms, #findings), } end -- Path-aware cycle-budget summary line. Per-path min/max totals. if #atoms > 0 then --- @type integer local total_min = 0 --- @type integer local total_max = 0 --- @type integer local max_atom_cyc = 0 --- @type string|nil local max_atom_name = nil --- @type integer, AtomEntry for _, a in ipairs(atoms) do --- @type AtomPaths local p = a.paths or {} total_min = total_min + (p.cycles_min or 0) total_max = total_max + (p.cycles_max or 0) if (p.cycles_max or 0) > max_atom_cyc then max_atom_cyc = p.cycles_max max_atom_name = a.name end end summaries[#summaries + 1] = { line = 0, msg = string.format("cycles: path-aware min=%d max=%d across %d atoms; worst atom=%s (%d); best-case, no stalls; BD-slot nops absorbed into branch costs" , total_min, total_max, #atoms, max_atom_name or "?", max_atom_cyc), } end return { atoms = atoms, findings = findings, errors = errors, warnings = warnings, info = info, summaries = summaries, } end -- ════════════════════════════════════════════════════════════════════════════ -- M.run — orchestrator entry -- ════════════════════════════════════════════════════════════════════════════ --- @type StaticAnalysisPass local M = {} --- @param ctx PassCtx --- @return PassResult function M.run(ctx) --- @type PassOutputEntry[] local outputs = {} --- @type CheckFinding[] local errors = {} --- @type CheckFinding[] local warnings = {} -- `info` aggregates finding-level info across every source (the per-source validate() also -- returns a `summaries` collection for scan/cycle rollups; -- those are summary rows and never enter `info`). --- @type CheckFinding[] local info = {} -- Build the corpus-wide pipe_ctx ONCE per pass run. -- The pipe_ctx is shared across every validate() invocation in this M.run so cross-source visibility is constant. --- @type PipeCtx local corpus_pipe_ctx = build_corpus_pipe_ctx(ctx) --- @type Corpus local corpus = ctx.shared.corpus -- Aggregate per-DIRECTORY (per-module). -- One static_analysis.txt per source-directory, emitted only if the directory contains at least one atom. -- Empty-source directories (e.g. duffle headers with no atoms) produce no report. -- Group sources by `src.dir` through the corpus-owned `sources_by_dir`. --- @type table local by_dir = (corpus and corpus.sources_by_dir) or {} --- @type string, SourceFile[] for dir, dir_sources in pairs(by_dir) do -- Run validate() against every source in this directory; accumulate atoms / findings / errors / warnings. -- The validate() function does its own per-source analysis (Binds indexing, atom discovery, all checks) -- and attaches path-aware cycle data to each atom it finds. --- @type AtomEntry[] local all_atoms = {} --- @type CheckFinding[] local all_findings = {} --- @type CheckFinding[] local dir_errors = {} --- @type CheckFinding[] local dir_warnings = {} --- @type CheckFinding[] local dir_info = {} --- @type ScanSummary[] local dir_summaries = {} --- @type integer, SourceFile for _, src in ipairs(dir_sources) do --- @type ValidateResult local result = validate(ctx, src, corpus_pipe_ctx) -- Tag each atom with its source so the render step can prefix the atom line with ":" -- when atoms from multiple sources live in the same module (e.g. lottes_tape.h + atom_dsl.h both declaring atoms). --- @type integer, AtomEntry for _, a in ipairs(result.atoms) do a.source_path = src.path all_atoms[#all_atoms + 1] = a end --- @type integer, CheckFinding for _, f in ipairs(result.findings) do all_findings [#all_findings + 1] = f end --- @type integer, CheckFinding for _, e in ipairs(result.errors) do dir_errors [#dir_errors + 1] = e end --- @type integer, C2CtrlWrite for _, w in ipairs(result.warnings) do dir_warnings [#dir_warnings + 1] = w end --- @type integer, CheckFinding for _, i_ in ipairs(result.info) do dir_info [#dir_info + 1] = i_ end --- @type integer, ScanSummary for _, s in ipairs(result.summaries or {}) do dir_summaries [#dir_summaries + 1] = s end end -- Stash per-module results on the corpus for `report.lua` to consume. -- Avoids re-running validate() in the report pass + avoids rebuilding corpus_pipe_ctx. -- Pattern matches `corpus.atoms_by_name` / `corpus.word_counts` / `corpus.components` -- (one writer: `static_analysis.lua`; one reader: `report.lua`). -- Module basename = last component of `dir` ("code/duffle" -> "duffle"). --- @type string local dir_basename = dir:match("([^/\\]+)$") or dir corpus.static_analysis_results = corpus.static_analysis_results or {} corpus.static_analysis_results[dir_basename] = { atoms = all_atoms, findings = all_findings, errors = dir_errors, warnings = dir_warnings, info = dir_info, summaries = dir_summaries, sources = dir_sources, } -- Aggregate per-dir errors/warnings/info into the orchestrator totals. -- Hoisted out of any per-dir file-emit so `report.lua` can drop the on-disk file emitter without losing the cross-module rollup. --- @type integer, CheckFinding for _, e in ipairs(dir_errors) do errors [#errors + 1] = e end --- @type integer, C2CtrlWrite for _, w in ipairs(dir_warnings) do warnings[#warnings + 1] = w end --- @type integer, CheckFinding for _, i_ in ipairs(dir_info) do info [#info + 1] = i_ end -- (No per-dir emit: per-module findings are stashed on `corpus.static_analysis_results` above. -- `report.lua` reads that projection to render `.atom_meta_report.md` without re-running validate().) end -- Result exposes at least {outputs, errors, warnings, info}. -- Summaries are internal to the renderer; callers (orchestrator, focused tests) consume the four severity-typed collections. return { outputs = outputs, errors = errors, warnings = warnings, info = info } end return M