Extending jit.util.tracesnap to return pc

[ligurio]

We are developing ljopt ¹ - a tool for verifying the correctness of optimizations in LuaJIT. The approach is a state of the art technology and used for verification of LLVM using Alive2; we want to use the same approach for LuaJIT. In brief, ljopt executes a given Lua program twice (with optimizations enabled and disabled), translates the LuaJIT IR from each run into the SMT-LIB format, and uses an SMT solver to verify that the resulting formulas are undecidable. The tool has already proven its value: it discovered a new issue in LuaJIT #1432 and reproduced several known optimization bugs.

The primary goal of ljopt is to model the semantics of LuaJIT IR as accurately as possible. However, traces often lack sufficient information for accurate modeling. To compensate, we extract certain necessary data directly from LuaJIT during Lua code execution – for example, the address of bytecode pointed to by the snapshot. Currently, we obtain this information using a custom function implemented via a patch to LuaJIT ². As a result, ljopt's source code depends on this patch. While it would be possible to implement the missing functions using the FFI, doing so would require describing LuaJIT's internal structures, making the solution fragile – especially since these structures may change over time.

The LuaJIT internal API includes the function jit.util.tracesnap(tr, sn) ³. In principle, this function could be extended to return the program counter (pc). The patch below adds this capability, as the second value jit.util.tracesnap() will return pc.

Mike, we would be very grateful if you could consider adding this feature to LuaJIT.

Patch:

@@ -363,6 +401,8 @@ LJLIB_CF(jit_util_tracesnap)
   if (T && sn < T->nsnap) {
     SnapShot *snap = &T->snap[sn];
     SnapEntry *map = &T->snapmap[snap->mapofs];
+    const BCIns *pc = snap_pc(&map[snap->nent]);
+    const BCIns *bc_base = pc;
     MSize n, nent = snap->nent;
     GCtab *t;
     lua_createtable(L, nent+2, 0);
@@ -372,7 +412,13 @@ LJLIB_CF(jit_util_tracesnap)
     for (n = 0; n < nent; n++)
       setintV(lj_tab_setint(L, t, (int32_t)(n+2)), (int32_t)map[n]);
     setintV(lj_tab_setint(L, t, (int32_t)(nent+2)), (int32_t)SNAP(255, 0, 0));
-    return 1;
+
+    while (bc_op(*bc_base) < BC_FUNCF) {
+      bc_base--;
+    }
+    setintV(L->top++, (int)(pc - bc_base));
+
+    return 2;
   }
   return 0;
 }

Footnotes

1. https://github.com/ligurio/ljopt ↩

2. https://github.com/ligurio/ljopt/blob/b67ac03ecb852f84cc7c8534d892b44d7b2bd8f0/lua_patches/0001-patch-some-internal-to-expose-snapshot-pc-in-bytecod.patch ↩

3. https://github.com/luvit/luajit-2.0/blob/8d2f7a062208e5112d078523c45a842ea975eb3e/src/lib_jit.c#L345-L365 ↩