Compilers perform a static analysis of a program prior to optimization. The precision of this analysis is limited, however, by strict time budgets for compilation. We explore an alternative, new approach, which links external sound static analysis tools into compilers. One of the key problems to be solved is that of propagating the source-level information gathered by a static analyzer deeper into the optimization pipeline. We propose a method to achieve this, and demonstrate its feasibility through an implementation using the LLVM compiler infrastructure. We show how assertions obtained from the Frama-C source code analysis platform are propagated through LLVM and are then used to substantially improve the effectiveness of several optimizations.
CITATION STYLE
Gjomemo, R., Namjoshi, K. S., Phung, P. H., Venkatakrishnan, V. N., & Zuck, L. D. (2015). From verification to optimizations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8931, pp. 300–317). Springer Verlag. https://doi.org/10.1007/978-3-662-46081-8_17
Mendeley helps you to discover research relevant for your work.