Evolute: Evolution of Software Systems with Extensible Languages and DSLs
Final Report Abstract
A static analysis is a computer program that systematically analyzes the source code of another program without executing it. Static analyses help compilers to produce efficient code by enabling compiler optimizations. While a compiler translates code from a source language to a target language, it tries to employ compiler optimizations to improve the performance of the generated code. Compiler optimizations are crucial for achieving satisfactory performance. However, the compiler may only apply an optimization if it can guarantee that the optimized code behaves identical to the unoptimized code–they must have the same semantics. That is, a compiler optimization may not change the program behavior except for making it perform better. To determine whether an optimization is applicable to a particular program, compilers rely on static analysis. For example, an optimization of (foo()*0) to 0 is only valid if a static analysis can show that foo() is free of side-effects and therefore can indeed be skipped. It is crucial that the analysis is sound, because only then the compiler can guarantee not to alter program behavior. This project established a new foundation for developing sound static analyses based on reusable analysis components. Since each analysis component only is responsible for one concern of the analyzed program, the development of analysis components is relatively simple. Moreover, analysis components can be tested and verified sound independently, which reduces the complexity significantly. This project provides a thorough theory for analysis components that formally establishes the properties of analysis components. A particular focus of the theory is on how analysis components can be composed to create full-fledged static analyses. The central formal result here is that the composition of sound analysis components is guaranteed to yield a sound static analysis. That is, with this theory it is not necessary anymore to prove soundness for the whole static analysis. Instead, it suffices to verify the contributing analysis components.
Publications
-
The IDE Portability Problem and its Solution in Monto. In Proceedings of Software Language Engineering (SLE), 152–162. ACM, 2016
Keidel, Sven; Pfeiffer, Wulf & Erdweg, Sebastian
-
Toward Abstract Interpretation of Program Transformations. In Proceedings of International Workshop on Meta-Programming Techniques and Reflection (META), 1–5. ACM, 2017
Keidel, Sven & Erdweg, Sebastian
-
Compositional soundness proofs of abstract interpreters. In Proceedings of the ACM on Programming Languages, vol. 2, no. ICFP, pages 72:1–72:26. ACM, 2018
Keidel, Sven; Poulsen, Casper Bach & Erdweg, Sebastian
-
Sound and Reusable Components for Abstract Interpretation. In Proceedings of the ACM on Programming Languages, vol. 3, no. OOPSLA, pages 176:1–176:28. ACM, 2019
Keidel, Sven & Erdweg, Sebastian
-
(2020) A Systematic Approach to Abstract Interpretation of Program Transformations. In: Beyer D., Zufferey D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2020. Lecture Notes in Computer Science, vol 11990. Springer, Cham. S. 136
Keidel, Sven & Erdweg, Sebastian
