Reproducer coverage: which LuaJIT bugs the SMT check can prove, and what blocks the rest

[aleksisch]

Reproducer tracking: SMT-equivalence coverage status

Tracking issue for the LuaJIT-bug reproducers under
tests/reproducers/: which bugs the SMT equivalence check can
prove today, and what blocks the rest, grouped by root cause.

Method

Each reproducer is run through the full pipeline
(ljopt.ir.traces_to_smt + LJOPT_SMTLIB, relaxed mode) on the
correct build af5d38f1 plus the buggy builds ab0c0793~ (#783)
and 203a98682~ (#817), solved with the standalone master
../z3/build/z3 (4.17.0). The emitted formulas are then read by
hand.

Two things that make a passing UNSAT meaningless

1. NYI dropping. In relaxed mode any unimplemented opcode is
   dropped. If the bug's own opcode is dropped, z3 proves
   equivalence of a formula that no longer contains the bug.
2. Loop-body dropping. Everything from the LOOP marker onward
   is treated as NYI. But LuaJIT peels the first iteration before
   LOOP, and that peeled iteration is kept — so for most loop
   reproducers the bug ops are still encoded in iteration 1. The
   real blocker is almost always an NYI opcode that appears in the
   first iteration, not the loop. (Earlier this group was
   mislabeled "Loops"; first-iteration analysis disproved that.)

Categorization (every reproducer)

Type	LuaJIT issues
Supported (proven via SMT)	#783, #817, #1079, #1236, math.abs/FP-neg*
False positive (spurious SAT)	#540
Encoded, needs buggy build (iter-1 fully encoded)	#791
Unimplemented ABC (array-bounds fold)	#606, #794, #1084, #6163, #6976
Unimplemented string builtins (lj_str_*, SNEW/STRREF/TOSTR)	#505
Unimplemented FFI (cdata/XLOAD/XSTORE; #651 crash)	#524, #651, #1069, #1086, #1244, lj_fix-fold-simplify-conv-sext
GC 64	#299
Unimplemented memory/upvalue/TDUP (HREF*/TDUP/table.clear/UREF*)	#584, #784, #792, #980, #994, #1133, #1295
Genuine PHI/loop dependency	#797
No trace recorded (opt-level mismatch / collision / env)	#311, #799, #1094, #1194, lj_ir_ksimd
Out of scope for SMT (compiler crash / memory-safety)	#1262

Notes per group

• Supported — straight-line scalar/CONV code that survives
  encoding, with a buggy build (or no upstream fix → force_sat:
  #1236). math.abs/FP-neg* is a vacuous placeholder
  (test:ok("reproduce using SMT")), no reproducer/check yet.
  #1236 ffi variant (lj_1236_2) is a boxed-local FP, see Support TNEW and TDUP #38.
• Encoded, needs buggy build — #791's peeled first iteration has
  zero NYI drops, so it is fully encoded. Needs the pre-fix build to
  show SAT; the BUFHDR-append form may only appear in the dropped
  loop body, so confirm whether iter-1 suffices.
• Unimplemented ABC — the array-bounds-check fold is dropped in
  iteration 1, so the bug never reaches z3. High-value op: it blocks
  five reproducers. #794/#1194 are also upstream segfault bugs.
• Unimplemented string builtins — #505 drops CALLN lj_str_find,
  SNEW, STRREF, TOSTR (string.find/sub machinery).
• Unimplemented FFI — cdata box/unbox (FLOAD cdata.int,
  CNEWI), XLOAD/XSTORE, FFI vararg calls (#1244). #299 (VLA
  uint8_t[?]) and #651 (struct) crash translation outright.
• Unimplemented memory/upvalue/TDUP — HREF/HREFK are
  implemented but these need TDUP forwarding, table.clear
  (CALLS) invalidation, or upvalue ops (ULOAD/USTORE/UREF*,
  e.g. the __newindex closure in #1133). #1133/#584 are not even
  loops.
• Genuine PHI/loop dependency — #797 is literally a "missing phi
  check in bufput_bufstr fold," so it needs the loop body, not just
  iteration 1.
• No trace recorded — after the ljopt: match traces correctly #73 pairing fix these still
  yield no checkable pair: #1094/#1194 compile a root trace at -O0
  but none at -O3 (and are upstream crash bugs, so effectively out of
  scope); #311 hits an ID-collision assertion in the recorder; #799
  needs string.buffer, absent from the pinned build; lj_ir_ksimd
  produces no root trace.
• Out of scope for SMT — #1262 is a stack-buffer-overflow in
  narrow_conv_backprop() (ASAN-only). Opt and unopt compute the
  same value; no buggy build can make it SAT.

Next steps (impact order)

1. Implement ABC — unblocks the most reproducers (5).
2. Make NYI-dropping loud: report "bug not encoded" instead of a
   silent UNSAT.
3. String builtins (lj_str_*) for #505.
4. FFI cdata value model (FLOAD cdata/CNEWI/XLOAD/XSTORE).
5. table.clear/TDUP/upvalue ops for the memory group.
6. Triage #540 false positive; fix #299/#651 crashes.
7. Fetch matching pre-fix builds once a bug's IR survives encoding.

Fixed along the way

• ljopt: match traces correctly #73 — trace pairing was dropping valid pairs because the trace UID
  hashed all live locals at a fixed stack level (differs between
  -O0/-O3). Now derived from SLOAD IR types; recovered #606,
  #1244, #1295.