An Extensible Verified Validator For

Recent advances in theorem proving technology have made it possible to write a com-pletely 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 verified validation technique will reduce verification efforts significantly and thus make it feasible to provide a formal guarantee of correctness for the full LLVM compiler. As a first step towards the grand goal, we have developed an extensible verified valida-tor 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.