Towards Compiler-Guided Static Analysis
summary
Proposes extracting compiler internals to help static analyses: translates SMT constraints into LLVM IR, runs selected LLVM optimization passes to simplify SMT constraints via LLVM optimizations, then converts back for Z3 — one example cuts a hard Z3 query from ~600s to ~0.2s, solves thousands of SMT-LIB queries that previously timed out and shows mean speedups (bitvectors ~1.27×, larger gains for floating point/combined). Also instruments LLVM passes to emit transformation records and instrument LLVM passes for translation validation, lining up 27 of 30 vectorized benchmarks from a 38-program suite.
AI-written summary · about
chapters (6)
- 0:00Static analysis introduction
- 1:25Static analysis bottlenecks
- 3:30Compiler-guided SMT solving
- 8:29Translation validation
- 17:15Compiler-guided static analysis
- 20:27Conclusion
related talks
53mFrom Within: Compiler Testing and Validation via Compilers
30mAnalyzing Programs with SMT Solvers
14mCoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
59mCompiler-assisted Translation Validation
10mA quick view into a compiler
19mExploiting Sophisticated Static Analysis for Verilog
29mPartially Evaluating Symbolic Interpreters for All
17mRecent Developments in Optimizing Compilers for RISC-V