static analysis: immeidate field awarenss

This commit is contained in:
ed
2026-08-14 01:22:54 -04:00
parent a535d381ed
commit 3a4d6304dd
2 changed files with 137 additions and 0 deletions
+46
View File
@@ -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 = <U4>}`.
+91
View File
@@ -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 },