From Verification to Optimizations
12 January 2015
Compilers perform static analysis prior to applying an optimization. The analysis results are typically not very precise, however, as compilers operate within strict time budgets, which constrains reasoning. In this paper, we explore how information obtained by dedicated external static analysis tools can be used to augment the internal reasoning done by a compiler, and whether this leads to better optimization. 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 an approach to achieve this and demonstrate its feasibility through an implementation using the LLVM compiler infrastructure. In particular, we show how assertions obtained from the Frama-C static analysis tool are propagated through LLVM and are then used to substantially improve the effectiveness of several optimizations.
