[WIP]: FFI support#65
Draft
aleksisch wants to merge 7 commits into
Draft
Conversation
aleksisch
force-pushed
the
aleksisch/support-ffi
branch
4 times, most recently
from
a913b9f to
080374f
Compare
aleksisch
force-pushed
the
aleksisch/support-ffi
branch
from
080374f to
ed9ea35
Compare
Looking at all the variables is too strict. SLOAD types is enough.
The trace UID embedded a signature of every live local read via
`debug.getlocal` at a hardcoded stack level. That frame differs
between the unoptimised (-O0) and optimised (-O3) recording runs,
so the two IDs for the same trace never matched and the pair was
dropped ("no trace recorded"). Derive the entry signature from the
trace's own SLOAD IR types instead, which are stable across opt
levels for the same Lua program.
Recovers matched trace pairs for previously-dropped reproducers
(e.g. lj_606, lj_1244, lj_1295); existing suites stay green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
aleksisch
force-pushed
the
aleksisch/support-ffi
branch
from
ed9ea35 to
4c7292d
Compare
Adds a 0-arg `nil-val` constructor to the MemCell datatype and uses it for the `nil` HSTORE variant (HSTORE on `nil`-typed right operand). `zero_pointer` default is now `nil-val`, so unwritten cells read as nil too. HLOAD num emits a real type guard: te[ssa] = (not ((_ is nil-val) raw_cell)) instead of the previous unconditional `true`. This is what "guarded HLOAD" means at the IR level — a `>` flag fires the side exit when the loaded slot turned out to be nil. Plumbing: MemoryStack.store_index_raw / load_index_raw expose pre-wrapped MemCell expressions so HSTORE-nil can write `nil-val` directly and HLOAD's type-guard can run `(_ is nil-val)` on the raw cell. Note: alone this still doesn't catch lj_1133 — that test hinges on t1/t2 aliasing through different VM-stack slots, which ljopt currently models as independent memory regions. A separate aliasing layer is needed to surface the bug. No regressions on detected reproducers (lj_783, lj_1079, lj_299, lj_524, lj_651, lj_1086, lj_fix-fold-simplify-conv- sext). Existing tests unchanged. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Implements `XLOAD int` / `XLOAD i64` via a shared
`(Array (_ BitVec 64) MemCell)` declared per trace pair.
To handle the pointer arithmetic we also implement:
* SLOAD cdt now also stores the cdata's mem-slot id in
op_stack as i64, mirroring SLOAD tab. This gives the
pointer SSA a concrete 64-bit value that p64 ADD can
consume.
* ADD p64 and MUL i64 are added as BinOpI64 aliases, so
the `cdata + i*4 + 8` chain emits real bvadd/bvmul
instead of dummies.
Models `CALLXS` as an uninterpreted SMT function `callxs_<arity>` (declared in `LJOPT_SMTLIB` for arities 1..4). Both unopt and opt traces apply the same function to congruent arguments, so equivalent FFI calls match by UF congruence even though ljopt has no semantic model of the underlying C routine. CARG was already routed to ir_node_dummy (Stage 3); the chain is walked here via `op:get_carg()` to gather argument SSAs. Test (`tests/tests.lua`): hot loop calling `ffi.C.abs(-i)`. Result is discarded — keeps the formula free of FP↔BV roundtrip chains that otherwise drive Z3 into timeout (see prior bisection on snap-slot reasoning).
Two pre-existing bugs in CNEW.lua surfaced when running FFI reproducers (lj_299) against this branch: 1. `maybe_size:get_num()` asserted when size came from an SSA (e.g. variable-length array `vla_t(n)` where n is loaded at runtime). Dispatch by is_num/is_ssa: load i64 from op_stack for runtime size, keep const path for compile-time size. 2. `mem_stack:store_index(idx, k, v)` was called without the required 5th `type` argument, hitting the "attempt to concatenate local 'type' (a nil value)" assert in MemoryStack.store_index. Pass 'i64' explicitly for both cdata.ctypeid and cdata.size stores. After the fix, lj_299 produces UNSAT (1 formula).
`ljopt_init_new_trace` asserted on the second LJ trace whose bytecode-hash + SLOAD-types signature collided with an existing record. Real reproducers (e.g. tests/reproducers/lj_311.lua) record many small traces from many call sites; a fingerprint collision crashed the whole recording pass with "Trace with exactly this bytecode already exists ...". Skip the duplicate (nil out traces_num[tr] so subsequent ljopt_savetrace / ljopt_savesnap drop their data) and continue. The first trace with that fingerprint stays; only the colliding ones are dropped. No false-positive risk: an uncomparable trace just isn't paired across opt levels. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The #1069 bug (NEWREF lacks a NaN-key guard) is a recorder/lowering bug: the guard is missing at *every* optimisation level, so plain opt-vs-unopt equivalence can't see it -- both traces agree. Catch it by injecting the mandatory lowering guard on the reference (unopt) side and letting the optimised trace's own recorded guard stand on the other side: - ir_smtlib.lua: expose ctx.is_reference (true for the unopt trace). - ir/NEWREF.lua: on the reference side, emit `not (fp.isNaN key)` as a trace exit and flag the node as a guard so the snapshot bitvector includes it. A buggy optimised trace, lacking the equivalent guard, diverges on a NaN key (SAT); a fixed trace carries the guard and stays equivalent (UNSAT). - ir/BinOp.lua: model the recorded `EQ x x` NaN-check idiom as `not (fp.isNaN x)`. SMT-LIB `=` is structural, so `(= x x)` is always true -- without this the recorded guard is a no-op and a present NaN check is indistinguishable from a missing one. - buggy_luajit_tests.lua: lj_1069 now uses reproduce_bug_using_smt (SAT on the buggy build, UNSAT on the fixed build). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
aleksisch
force-pushed
the
aleksisch/support-ffi
branch
from
4c7292d to
4518061
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Full FFI support
Closed #56