Verified Credible Compilation Framework For Early CSE in LLVM

Abstract

Compiler verification is important when obtaining a high level of reliability through software verification. Compiler bugs are crucial for software verification because code that running programs are not source code but execution code. However, many C/C++ mainstream compilers, including GCC and LLVM focus on efficiency rather than reliability. Although testing is an effective method to identify bugs, it does not guarantee a high level of reliability. Various approaches have been proposed to examine compiler internal logics, but as yet none have been very successful.

CRELLVM is a compiler framework that validates optimization passes in LLVM to ensure high reliability of LLVM optimizations. It is able to validate major optimizations of LLVM such as Register Promotion and Global Value Numbering.

This thesis shows validation of Early CSE optimization in LLVM, using CRELLVM. For the validation, proof generation code which corresponds to Early CSE in LLVM is implemented and the proof checker has been extended. Early CSE is one of the basic optimizations in LLVM that removes the repeated computations by erasing duplicated instructions.

Based on 5.40 million lines of C code benchmarks, the experiment result shows there is no mis-compilation for Early CSE, which guarantees a high level of reliability of Early CSE in the benchmarks.