Verifying LuaJIT optimizations with SMT

JIT compilers are at the heart of modern dynamic languages. LuaJIT powers Tarantool, OpenResty, and game engines. But JIT optimizations can have bugs - subtle, rare, and hard to reproduce. How can we automatically check that optimized code behaves exactly like unoptimized code?

We present ljopt - a tool for verifying LuaJIT optimizations using bounded translation validation. The idea is simple: run the same Lua program twice - once with optimizations disabled, once with them enabled. Record the IR traces, translate them into SMT-LIB formulas, and hand them to the Z3 SMT solver. If the formula is satisfiable (SAT), we get a concrete counterexample - a bug in an optimization rule. If unsatisfiable (UNSAT), the optimization is correct within our model.

What we’ve done:

• Support for 78 out of 96 LuaJIT IR opcodes: arithmetic, bitwise ops, table operations, type conversions, math library calls.
• A three-dimensional versioned memory model using SMT arrays, handling mutable Lua tables with local/global slot separation.
• Constant propagation through the SMT context - allowing precise verification of constant-folded math.sin() calls and other transcendental functions.
• Loop unrolling instead of Horn clauses, because SMT solvers struggle with the combination of QF_FP, QF_BV, Array and String theories.

Results on real LuaJIT bugs:

• Tested on 33 known LuaJIT bugs and 5 bugs reproduced by SMT verification: LJ#783, LJ#791, LJ#1079, LJ#1236, LJ#817.
• 1 previously unknown bug discovered (LJ#1432).
• 2 bugs found and fixed in the Z3 solver itself (Z3#9488, Z3#9234).

The tool requires no modifications to LuaJIT it hooks into the compiler via jit.attach() and distributed under the MIT license.

Known limitations: Calls to arbitrary C functions (CALLS, CALLA), array bounds checks (ABC), and metamethods are not yet supported.

To the best of our knowledge, ljopt is the first working SMT-based translation validation system for a production trace-based JIT compiler.

If you use LuaJIT in production (Tarantool, OpenResty, or elsewhere), ljopt can help you gain confidence in the optimizations that make your code fast.

This work is collective effort. At different times the following people worked on the project: Aleksey Churkin, Artur Sibgatullin, Evgeny Demidovich, Sergey Bronnikov, Sergey Kaplun.

Source code is available on Github - ligurio/ljopt.