An Extensible Veried Validator For Simple Optimizations in LLVM
Sungkeun Cho, Joonwon Choi, Jeehoon Kang, Chung-Kil Hur, Kwangkeun Yi · 2014
Recent advances in theorem proving technology have made it possible to write a completely bug-free compiler such as CompCert. However, this technology have not been fully applied to mainstream compilers such as GCC and LLVM due to the huge amount of work required. Nevertheless, we believe that the veried validation technique will reduce verication eorts signicantly and thus make it feasible to provide a formal guarantee of correctness for the full LLVM compiler. As a rst step towards the grand goal, we have developed an extensible veried validator for simple optimizations in LLVM, mainly targeted for all micro-optimizations (about 400) in the instruction combine pass. Our validator, based on a simple form of relational Hoare reasoning, can be used to validate various kinds of simple optimizations without losing completeness (i.e., it succeeds to validate all correct results at least by design). We achieve both generality and completeness, not by automation, but by extensibility, which allows to freely add inference rules that are proven to be correct.