From Within: Compiler Testing and Validation via Compilers
summary
Claims a compiler-centric workflow that instruments LLVM APIs to record instruction manipulations and debug-location updates, then compares those traces to a static-analysis-derived oracle. Validates debug info and a loop vectorizer without executing inputs, uses an alignment automaton plus an SMT solver for equivalence, and reports concrete results: about 46 LLVM fixes and accepted patches for debug-info bugs, plus successful reproductions of recent vectorizer miscompilations.
AI-written summary · about
chapters (6)
- 0:00Compiler testing intro
- 1:49Why compilers need validation
- 8:55Debug info validation
- 28:55Loop vectorization testing
- 41:20Summary and future directions
- 42:33Q&A
related talks
59mCompiler-assisted Translation Validation
01h 06mVerifying a compiler through equational means
18mRobustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
21mTowards Compiler-Guided Static Analysis
53mLocknote: How Badly Do We Want Correct Compilers?- 01h 06mVerifying a compiler through equational means
18mCompiling countermeasures against fault attacks with “Tracing LLVM”
20mRefined Input, Degraded Output: The Counterintuitive World of Compiler Behavior