Equivalence checking is a fundamental construct in program verification and synthesis. We describe an efficient and robust procedure to automatically generate proofs of equivalence across C-compiled unoptimized and optimized assembly implementations, and use it to validate end-to-end optimizations produced by multiple modern compilers for large C programs compiled to 32-bit x86 ELF executables. To do this, we had to reconstruct a partial C program specification from compiled and unoptimized (O0) ELF executable code and ELF headers.

We find that modeling of aliasing-based C undefined-behaviour semantics is essential for the robustness of our equivalence checker; we describe a provably sound procedure to efficiently model C semantics, including aliasing-based undefined behaviour. Further, we describe a new robust algorithm for automatic generation of equivalence proofs, across compiler transformations. To evaluate robustness, we present first-of-its-kind experiments involving equivalence checks across almost all compiler optimizations, and across multiple compilers, with 76% overall success rates for O2 optimizations and 72% overall success rates for O3 optimizations on the SPEC benchmarks. We also demonstrate the use of our equivalence checker in a preliminary superoptimizer supporting loops; we hope that the end-to-end nature of our equivalence procedure and its soundness and robustness, informs future work in superoptimization and synthesis for C programs. A somewhat surprising conclusion of our work is: computing equivalence across programs compiled to ELF executables is not harder than computing equivalence across programs compiled to higher-level IR.