Compiler Validation via Equivalence Modulo Inputs

作者：Vu Le^*; Afshari Mehrdad; Su Zhendong

来源：ACM Sigplan Notices, 2014, 49(6): 216-226.

DOI：10.1145/2594291.2594334

• Algorithms
• Languages
• Reliability
• Verification
• Compiler testing
• miscompilation
• equivalent program variants
• automated testing

We introduce equivalence modulo inputs (EMI), a simple, widely applicable methodology for validating optimizing compilers. Our key insight is to exploit the close interplay between (1) dynamically executing a program on some test inputs and (2) statically compiling the program to work on all possible inputs. Indeed, the test inputs induce a natural collection of the original program's EMI variants, which can help differentially test any compiler and specifically target the difficult-to-find miscompilations.
To create a practical implementation of EMI for validating C compilers, we profile a program's test executions and stochastically prune its unexecuted code. Our extensive testing in eleven months has led to 147 confirmed, unique bug reports for GCC and LLVM alone. The majority of those bugs are miscompilations, and more than 100 have already been fixed.
Beyond testing compilers, EMI can be adapted to validate program transformation and analysis systems in general. This work opens up this exciting, new direction.

• 出版日期2014-6