Skip to content

AUDIT_v0.80.x.md

Latest commit

 

History

History
109 lines (89 loc) · 5.01 KB

AUDIT_v0.80.x.md

File metadata and controls

109 lines (89 loc) · 5.01 KB
Raw

WildX JIT Marathon Audit — v0.80.x

Date: 2026-07-11 Status: ✅ COMPLETE Versions: v0.80.0 → v0.80.4

Marathon Overview

The v0.80.x series implements comprehensive JIT infrastructure for the Nitpick runtime, spanning instruction encoding, register allocation, calling conventions, SIMD support, debugging integration, and formal verification across x86_64 and AArch64 architectures.

Release Summary

Version Title Key Deliverables
v0.80.0 JIT Opcode Triage Instruction selection audit, load/store offset fixes, conditional branch repair
v0.80.1 Register Allocator Liveness Stale-def bug fix in linear scan, high register pressure tests
v0.80.2 Calling Convention & GDB System V N-arg executor, JIT→JIT calls, GDB JIT interface, in-memory ELF
v0.80.2b AArch64 Encoder Parity Full integer ISA: add/sub/mul, logical, shifts, wide moves, load/store, branches (14 tests)
v0.80.3 SIMD & CPUID SSE2/AVX2 emission, VEX encoding, CPUID runtime detection, AArch64 NEON (16 tests)
v0.80.4 Verification & Close Z3 proofs, ESBMC/KLEE harnesses, guide chapters, tracker close, doc sync

Test Results

Test Suite Count Status
x86_64 JIT core (v0.72) Variable ✅ Pass
Register allocator (v0.73 + v0.80.1) Variable ✅ Pass
JIT optimization (v0.74) Variable ✅ Pass
ABI/calling convention (v0.80.2) Variable ✅ Pass
AArch64 integer encoder (v0.80.2b) 14 ✅ Pass
x86_64 SIMD/CPUID (v0.80.3) 9 ✅ Pass
AArch64 NEON (v0.80.3) 7 ✅ Pass

Formal Verification Results

Tool Harness Properties Status
Z3 verification/z3/jit/jit_safety_properties.py 6 (W^E, token, spill) ✅ All PROVED
ESBMC verification/esbmc/jit_state_harness.c State machine + W^E ✅ VERIFICATION SUCCESSFUL
KLEE verification/klee/harnesses/jit_emitter_harness.c 281 paths, 0 errors ✅ All paths clean

Documentation Delivered

Artifact Location
Chapter 6: Register Allocator nitpick-docs/guide/jit/ch06_register_allocator.md
Chapter 7: SIMD with JIT nitpick-docs/guide/jit/ch07_simd.md
Chapter 8: Debugging JIT'd Code nitpick-docs/guide/jit/ch08_debugging.md
Chapter 9: AArch64 nitpick-docs/guide/jit/ch09_aarch64.md
asm_specs.txt (SIMD tables) nitpick-docs/specs/asm_specs.txt
Man pages (regenerated) nitpick-docs/man/man7/
Web docs (deployed) ailp-website/nitpick/docs/

JIT Tracker Final Tally

Category Total ✅ Done 🔶 Deferred
REGALLOC 5 4 1
ENCODER-X86 7 3 4
ENCODER-A64 6 6 0
ABI 6 4 2
DEBUG 2 2 0
SIMD 5 4 1
VALID 5 5 0
Total 36 28 8

Deferred Items → v0.80.5

ID Description Rationale
JIT-004 XMM register spilling Requires SIMD register allocator
JIT-010 CMOV (conditional move) Not needed for SIMD focus
JIT-011 SETCC (set byte on condition) Not needed for SIMD focus
JIT-012 LOCK prefix (atomics) Separate concern from SIMD
JIT-013 CVTSI2SD (int↔float conversion) FP not in SIMD scope
JIT-032 Struct by-value passing Complex ABI feature
JIT-034 AArch64 FP arg passing (v0-v7) FP calling convention
JIT-054 SIMD register allocator Requires significant reg alloc rework

Additionally from v0.80.3 roadmap:

  • Phase 4: Real-world JIT benchmarks (matrix multiply, string scan, histogram)
  • Phase 5: SIMD register allocator extension (xmm/ymm/v0-v31 in linear scan)

Files Changed Across v0.80.x

New Files

  • src/runtime/assembler/aarch64_encoder.cpp — AArch64 instruction encoder
  • src/runtime/assembler/aarch64_encoder.h — AArch64 encoder declarations
  • src/runtime/assembler/cpuid.cpp — CPUID runtime detection
  • src/runtime/jit_gdb.cpp — GDB JIT interface
  • include/runtime/jit_gdb.h — GDB JIT declarations
  • tests/runtime/test_jit_aarch64_v0802b.cpp — AArch64 integer tests
  • tests/runtime/test_jit_abi_v0802.cpp — ABI/calling convention tests
  • tests/runtime/test_jit_regalloc_v0801.cpp — Register allocator tests
  • tests/runtime/test_jit_simd_v0803.cpp — x86_64 SIMD tests
  • tests/runtime/test_jit_neon_v0803.cpp — AArch64 NEON tests
  • verification/z3/jit/jit_safety_properties.py — Z3 proofs
  • verification/esbmc/jit_state_harness.c — ESBMC harness
  • verification/klee/harnesses/jit_emitter_harness.c — KLEE harness

Modified Files

  • include/runtime/assembler.h — SIMD opcodes, CPUID API, ABI declarations
  • src/runtime/assembler/assembler.cpp — SSE2/AVX2 emission, N-arg executor
  • src/backend/ir/ir_generator.cpp — IR patches for v0.80.0 triage
  • src/runtime/math/lbim_extended.cpp — Extended math for v0.80.0
  • CMakeLists.txt — Build system updates
  • README.md — Version bumps and release notes