Improving Compiler Optimizations using Program Annotations

In this work we describe a framework that combines the results of from program testing, formal verification and compiler optimization. We focus on how the informations manually provided by the developer, by crowd source formal verification or by static formal verification tools can be used to help the compilation process. This framework is built on top of the LLVM architecture and can be useful to software developers as it will improve performance while significantly enhancing security. By using the results coming from program analyzer’s analysis we show how our framework can reduce the overhead incurred to ensure array bounds checking and how it can help compiler analysis and improve compiler optimizations.