Verified Translation Validation For Register Promotion in LLVM

Abstract

Mainstream C/C++ compilers usually focus on efficiency though reliability is also important as well for compilers. Thus they perform various optimizations for performance, but many bugs are found in GCC and LLVM by recent random testing tools.

To increase the reliability of mainstream compilers without sacrificing their performance, I propose a practical approach for verified compilation using a verified extensible relational Hoare-logic (ERHL) validator. As this approach performs translation validation which separates compilation and validation, it does not sacrifice any compilation performance. Also, I can finally succeed to validate translations or identify compiler bugs because I insert proof generation code for validation directly in the compiler.

As a litmus test to show the possibility of this approach, I successfully validate register promotion in the sroa pass in LLVM 3.7.1. Translation validation for register promotion has enough to show possibility of validating the whole optimization passes in LLVM as register promotion is one of the most performance critical passes in LLVM. This is because register promotion promotes memory locations to LLVM registers and converts corresponding load and store instructions into register read and write operations, and many LLVM optimization focus on optimizing register operations, most of which are introduced in register promotion. Moreover, some of those LLVM registers are transformed into CPU registers which are magnitude faster to access than memory locations.

I validated translation of register promotion for SPEC CPU2006 benchmarks, LLVM Nightly Test, and five C projects, with 7.1M lines of code in total. There are only 10 failures in validation results, but all of them are due to the compiler bug which I found during this work.