From 3a4d6304dd10520b04499f4f5d778b546015ab19 Mon Sep 17 00:00:00 2001 From: Ed_ Date: Fri, 14 Aug 2026 01:22:54 -0400 Subject: [PATCH] static analysis: immeidate field awarenss --- scripts/duffle.lua | 46 +++++++++++++++ scripts/passes/static_analysis.lua | 91 ++++++++++++++++++++++++++++++ 2 files changed, 137 insertions(+) diff --git a/scripts/duffle.lua b/scripts/duffle.lua index 47cea62..7ceb02a 100644 --- a/scripts/duffle.lua +++ b/scripts/duffle.lua @@ -1962,6 +1962,52 @@ M.INSTRUCTION_GPR_EFFECTS = { shift_aright_var = { reads = {2, 3}, writes = {1} }, } +------------------------------------------------------------------------------- +-- IMMEDIATE_FIELD_WIDTHS — maps instruction names to their immediate-argument +-- positions (1-based) and field widths (in bits). Consumed by the +-- `immediate_field_width` static-analysis check. Parallel to +-- INSTRUCTION_GPR_EFFECTS. +-- +-- `signed = true` means the field is sign-extended (the value must fit in +-- the signed range). `signed = false` (default) means zero-extended. +------------------------------------------------------------------------------- +M.IMMEDIATE_FIELD_WIDTHS = { + -- CPU I-type immediates: 16-bit signed (addiu/addi/slti sign-extend) + add_ui = { { arg = 3, width = 16, signed = true } }, + add_si = { { arg = 3, width = 16, signed = true } }, + add_ui_self = { { arg = 2, width = 16, signed = true } }, + slt_si = { { arg = 3, width = 16, signed = true } }, + slt_ui = { { arg = 3, width = 16, signed = true } }, + -- CPU I-type immediates: 16-bit unsigned (andi/ori/xori zero-extend) + and_i = { { arg = 3, width = 16 } }, + or_i = { { arg = 3, width = 16 } }, + or_i_self = { { arg = 2, width = 16 } }, + xor_i = { { arg = 3, width = 16 } }, + load_upper_i = { { arg = 2, width = 16 } }, + -- Load/store offsets: 16-bit signed + load_word = { { arg = 3, width = 16, signed = true } }, + load_half = { { arg = 3, width = 16, signed = true } }, + load_half_u = { { arg = 3, width = 16, signed = true } }, + load_byte = { { arg = 3, width = 16, signed = true } }, + load_byte_u = { { arg = 3, width = 16, signed = true } }, + store_word = { { arg = 3, width = 16, signed = true } }, + store_half = { { arg = 3, width = 16, signed = true } }, + store_byte = { { arg = 3, width = 16, signed = true } }, + -- Shift amount: 5-bit unsigned + shift_lleft = { { arg = 3, width = 5 } }, + shift_lleft_self = { { arg = 2, width = 5 } }, + shift_lright = { { arg = 3, width = 5 } }, + shift_aright = { { arg = 3, width = 5 } }, + shift_aright_var = { { arg = 3, width = 5 } }, + -- Branch offsets: 16-bit signed + branch_equal = { { arg = 3, width = 16, signed = true } }, + branch_ne = { { arg = 3, width = 16, signed = true } }, + branch_le_zero = { { arg = 2, width = 16, signed = true } }, + branch_lt_zero = { { arg = 2, width = 16, signed = true } }, + branch_ge_zero = { { arg = 2, width = 16, signed = true } }, + branch_gt_zero = { { arg = 2, width = 16, signed = true } }, +} + -- Bounded GPR-value rules consumed by the same forward event walk as `INSTRUCTION_GPR_EFFECTS`. -- A rule describes a literal/constant-producing transform; if its required inputs are not constant, the destination is invalidated rather than carrying a stale value. -- The lattice is deliberately closed to `{kind = "unknown"}` and `{kind = "constant", value = }`. diff --git a/scripts/passes/static_analysis.lua b/scripts/passes/static_analysis.lua index 7be1a9d..30c6bbd 100644 --- a/scripts/passes/static_analysis.lua +++ b/scripts/passes/static_analysis.lua @@ -2566,6 +2566,96 @@ local function check_gte_cr_TR_naming(atom, _pipe_ctx, findings) 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. +local function check_immediate_field_width(atom, pipe_ctx, findings) + local widths = duffle.IMMEDIATE_FIELD_WIDTHS or {} + local events = atom.paths and atom.paths.word_events or {} + local line_for_word_event = pipe_ctx.line_for_word_event + for _, ev in ipairs(events) do + local ev_ident = ev.encoder or ev.ident or "?" + local rules = widths[ev_ident] + if rules then + local ev_args = ev.args or {} + local ev_line = line_for_word_event and line_for_word_event(ev) or atom.line + for _, rule in ipairs(rules) do + local arg_str = ev_args[rule.arg] + if arg_str then + local value = parse_integer_literal(arg_str) + if value then + local width = rule.width + 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. + local signed_value = value + if is_signed and value >= 0x80000000 then + signed_value = value - 0x100000000 + end + 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. + local check_value = is_signed and signed_value or value + local field_max = bit.lshift(1, width) - 1 + 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. + 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 + -- CHECK_RULES — data-driven check dispatch (Muratori: data over control flow) -- ════════════════════════════════════════════════════════════════════════════ @@ -2595,6 +2685,7 @@ local CHECK_RULES = { { name = "gte_cr_alias_writes", per_atom = check_gte_cr_alias_writes }, { 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 },