Equivalence checking is an important building block for program synthesis and verification. For a synthesis tool to compete with modern compilers, its equivalence checker should be able to verify the transformations produced by these compilers. We find that the transformations produced by compilers are much varied and the presence of undefined behaviour allows them to produce even more aggressive optimizations. Previous work on equivalence checking has been done in the context of translation validation, where either a pass-by-pass based approach was employed or a set of handpicked optimizations were proven. These settings are not suitable for a synthesis tool where a black-box approach is required. This paper presents the design and implementation of an equivalence checker which can perform black-box checking across almost all the composed transformations produced by modern compilers. We evaluate the checker by testing it across unoptimized and optimized binaries of SPEC benchmarks generated by gcc, clang, ice and ccomp. The tool has overall success rates of 76% and 72% for 02 and 03 optimizations respectively, for this first of its kind experiment.
展开▼
