An Annotation Framework for Low-Level Virtual Machine Compiler Infrastructure

This work has been part of the ongoing results in a research project on compilers, formal methods and computer security to build a defensive optimizer compiler. Modern compilers contain several complex, highly specified, effective optimizations that aim to transform the input program into an equivalent more efficient one. Efficiency can be measured in terms of speed of execution, allocated memory space or energy consumption of the machine running the program. These optimizations are based on very developed heuristics that can obtain very significant results on the output program. However, these algorithms are not able to get some properties that could lead to further optimizations. Properties that, for example, need a formal verification prover to be caught, or that can be inserted externally, for example by the programmer himself. This thesis presents a compiler framework that allows to build optimizations that are capable to exploit this additional information, so as to permit further optimization, and that will be formally verified for correctness. The framework is built upon Low Level Virtual Machine (LLVM), a compiler infrastructure characterized by high modularity and reusability. First an overview of the problem is given, then a theoretical solution is developed and explained. It is seen that this solution can have different implementations on the LLVM infrastructure. To enforce the correctness of these transformations and provide a method to carry the properties through different steps of the optimization, a witness is developed for every transformation. The witness can be checked independently to establish the correctness of the transformation and, if correct, helps transfer invariants from the source to the target program. The thesis presents implemented witnesses for some common optimizations.