FaJITa: Verifying Optimizations on Just-In-Time Programs
summary
FaJITa is a translation validator that checks semantic equivalence of JavaScript functions after Firefox JIT optimizations by combining symbolic execution with targeted static analyses and an SMT backend. It models hundreds of MIR ops as uninterpreted functions and uses a specialized memory model that statically tracks object locations and field offsets, letting most Firefox test-suite functions verify in under a second with few false positives. It reproduces past optimizer bugs, integrates with a fuzzing trace collector to hunt new bugs, and still needs better generators to reach rare misoptimizations.
AI-written summary · about
chapters (14)
- 0:00Start
- 4:58Finding bugs - semantics-aware fuzzing
- 5:34Overview
- 6:07How should we verify the optimizer - ideal
- 7:03Using symbolic execution (symex)
- 7:24Proving semantic equivalence
- 9:25Verifying MIR: approximate most semantics
- 12:04Optimizing the memory model for symex
- 15:19Optimizations make verification tractable
- 16:13FaJITa as bug finding tool
- 17:04Guided fuzzing
- 18:04FaJITa for online eventual verification
- 18:39Takeaway
- 21:34Finding bugs our target
related talks
26mJavaScript JITs
18mOptimization-Directed Compiler Fuzzing for Continuous Translation Validation
25mJavaScript engines how do they even?
36mFast and Dynamic
18mPreview: Verification (Correctness & Debugging)
31mJavaScript Compilers For Fun and Profit
31mJavaScript Compilation Techniques or "Wasn't JavaScript supposed to be slow?"
29mExtreme JavaScript Performance