Ground-truth semantics for x86-64 instructions, measured on real hardware — an 11th Gen Intel® Core™ i7-1165G7 (Tiger Lake, 4 cores / 8 threads @ 2.80 GHz).
binit is a dataset of concrete execution traces for individual x86-64 instructions. For each instruction we pick a set of initial CPU states (general-purpose registers, status flags, and an optional memory operand), execute the single instruction on a ground-truth backend, and record the resulting final state.
The result is a large table of
(opcode, initial state) → (final state) facts that
describe how real hardware actually behaves — including the messy
corners of the flags and undefined-behavior edges. It is meant to be used
as an oracle: a way to test emulators, lifters, decompilers, and other
binary-analysis tools against reality instead of against the manual.
The methodology, coverage, and findings are described in the paper: binit (PDF).
The export is three Parquet files:
| File | One row per… | Key columns |
|---|---|---|
instructions.parquet |
mnemonic |
instruction_id, undefined_flags,
tags
|
test_cases.parquet |
opcode (encoded instruction) |
test_case_id, opcode,
initial_states
|
test_results.parquet |
initial state |
test_case_id, state_index,
final_state, exception_kind
|
A state is a small JSON object of 64-bit values keyed by register name
(rax, rbx, …), the packed
flag register, and an optional mem0_value memory
operand. state_index in a result points at the matching entry
in the test case's initial_states list.
To validate a tool, replay each initial state through it and compare its final state against ours. The contract is:
mem0, if present).
opcode.undefined_flags, since the
hardware leaves those unspecified.
Here is a minimal, self-contained runner using
Unicorn. It has
inline dependencies, so uv run unicorn_check.py just works:
# /// script
# dependencies = ["duckdb>=1.5", "unicorn==2.1.4"]
# ///
import json, tempfile, urllib.request
from pathlib import Path
import duckdb
import unicorn
import unicorn.x86_const as x86
BASE_URL = "https://binit.wazab.in"
MASK64 = (1 << 64) - 1
ENTRY = 0x666666660000 # where we place the instruction
PAGE = 0x1000
REGS = ("rax", "rbx", "rcx", "rdx", "r8", "r9", "rbp", "rsp")
REG_IDS = {n: getattr(x86, f"UC_X86_REG_{n.upper()}") for n in REGS}
FLAG_BITS = {"CF": 0, "PF": 2, "AF": 4, "ZF": 6, "SF": 7, "OF": 11}
class Runner:
"""One reused emulator: building a fresh Uc per state is the slow part."""
def __init__(self):
self.emu = unicorn.Uc(unicorn.UC_ARCH_X86, unicorn.UC_MODE_64)
self.emu.mem_map(ENTRY, PAGE)
self.loaded = None
def run(self, opcode_hex, initial):
code = bytes.fromhex(opcode_hex.strip())
start = ENTRY + PAGE - len(code)
if self.loaded != (start, code): # rewrite code only when it changes
self.emu.mem_write(start, code)
self.loaded = (start, code)
for name, reg_id in REG_IDS.items(): # set every reg, so no state leaks
self.emu.reg_write(reg_id, initial.get(name, 0) & MASK64)
self.emu.reg_write(x86.UC_X86_REG_RFLAGS, initial.get("flag", 0) & MASK64)
self.emu.reg_write(x86.UC_X86_REG_RIP, start)
self.emu.emu_start(start, start + len(code), count=1)
out = {n: self.emu.reg_read(r) & MASK64 for n, r in REG_IDS.items()}
out["flag"] = self.emu.reg_read(x86.UC_X86_REG_RFLAGS) & MASK64
return out
def flag_mask(undefined):
mask = 0
for name, bit in FLAG_BITS.items():
if name not in undefined:
mask |= 1 << bit
return mask
# Download the export and expose it as in-memory SQL views.
tmp = Path(tempfile.mkdtemp())
for f in ("instructions.parquet", "test_cases.parquet", "test_results.parquet"):
urllib.request.urlretrieve(f"{BASE_URL}/data/{f}", tmp / f)
con = duckdb.connect(":memory:")
for t in ("instructions", "test_cases", "test_results"):
con.read_parquet(str(tmp / f"{t}.parquet")).create_view(t)
rows = con.execute(
"""
SELECT i.instruction_id, tc.opcode, tc.instruction, tc.initial_states,
r.state_index, r.final_state, r.exception_kind, i.undefined_flags
FROM test_results r
JOIN test_cases tc ON tc.test_case_id = r.test_case_id
JOIN instructions i ON i.instruction_id = tc.instruction_id
WHERE NOT list_contains(i.tags, 'avx') -- this example ignores SIMD memory operands
ORDER BY i.instruction_id -- group states by mnemonic
LIMIT 5000
"""
).fetchall()
runner = Runner()
failed = set() # mnemonics already known to be wrong
processed = mismatches = 0
for insn_id, opcode, insn, initial_states, idx, final_state, exc, undefined in rows:
if insn_id in failed:
continue # skip the rest of a broken mnemonic
if exc or final_state is None:
continue # skip faulting cases for brevity
initial = {k: int(v) for k, v in json.loads(initial_states)[idx].items()}
if "mem0_value" in initial:
continue # memory operands omitted here; see full script
expected = {k: int(v) for k, v in json.loads(final_state).items()}
actual = runner.run(opcode, initial)
processed += 1
mask = flag_mask(set(undefined or []))
for name, want in expected.items():
if name not in actual:
continue
got = actual[name]
if name == "flag":
want, got = want & mask, got & mask
if (want & MASK64) != (got & MASK64):
mismatches += 1
failed.add(insn_id) # stop testing this mnemonic
print(f"mismatch {insn}: {name} expected {want:#x} got {got:#x}")
break
print(f"processed={processed} mismatches={mismatches}")
This trimmed version skips memory-operand and exception cases to stay readable. The full runner that handles those is available here: test_unicorn_public_parquet.py.
Both the snippet above and the full script are released into the public domain under the Unlicense — copy, modify, and reuse them freely, with or without attribution.