Compiler-assisted Translation Validation
summary
LLVM is instrumented to emit translation records (per-instruction actions and instruction manipulation events) and a validator uses those traces plus static control-flow analysis and SMT (Alive2) to check debug-location updates and equivalence. The system reports ~46 real bugs and supplies 46 accepted patches; temporal and spatial decomposition break monolithic proofs, speeding Alive2 about 2× and solving cases that previously timed out. The implementation runs and produces both diagnostics and concrete fixes.
AI-written summary · about
chapters (11)
- 0:00Compiler-assisted translation validation
- 1:05What is a compiler
- 2:33Traditional validation approaches
- 3:59Limitations of compiler testing
- 8:01Translation validation framework
- 10:49Debug info validation
- 27:46Fixing compiler bugs
- 29:13Q&A on debugger validation
- 37:14Speeding up SMT validation
- 48:45Future directions
- 50:13Q&A on spatial decomposition
related talks
53mFrom Within: Compiler Testing and Validation via Compilers
15mTranslation Validation for LLVM's AArch64 Backend
18mRobustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
15mInterleaving Large Language Models for Compiler Testing
24mGenerating BPF Verifier Friendly Code with Clang
21mTowards Compiler-Guided Static Analysis
18mCompiling countermeasures against fault attacks with “Tracing LLVM”
16mCounterexample-Guided Correlation Algorithm for Translation Validation