Testing static analyses for precision and soundness
| Autor: | Zhengyang Liu, John Regehr, Jubi Taneja |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Soundness
Computer science Programming language 020207 software engineering 02 engineering and technology Static analysis Formal methods computer.software_genre Dead code elimination 020204 information systems Satisfiability modulo theories 0202 electrical engineering electronic engineering information engineering Code (cryptography) Compiler computer Compile time |
| Zdroj: | CGO |
| DOI: | 10.1145/3368826.3377927 |
| Popis: | Static analyses compute properties of programs that are true in all executions, and compilers use these properties to justify optimizations such as dead code elimination. Each static analysis in a compiler should be as precise as possible while remaining sound and being sufficiently fast. Unsound static analyses typically lead to miscompilations, whereas imprecisions typically lead to missed optimizations. Neither kind of bug is easy to track down. Our research uses formal methods to help compiler developers create better static analyses. Our contribution is the design and evaluation of several algorithms for computing sound and maximally precise static analysis results using an SMT solver. These methods are too slow to use at compile time, but they can be used offline to find soundness and precision errors in a production compiler such as LLVM. We found no new soundness bugs in LLVM, but we can discover previously-fixed soundness errors that we re-introduced into the code base. We identified many imprecisions in LLVM’s static analyses, some of which have been fixed as a result of our work. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|