Automatically Proving the Correctness of Compiler Optimizations

We describe a technique for automatically proving compiler optimizations sound, meaning that their trans-formations are always semantics-preserving. We rst present a domain-specic language for implementing optimizations as guarded rewrite rules. Optimizations operate over a C-like intermediate representation including unstructured control ow, pointers to local variables and dynamically allocated memory, and re-cursive procedures. Then we describe a technique for automatically proving the soundness of optimizations implemented in this language. Our technique requires only a small set of optimization-specic proof obli-gations to be discharged for each optimization by an automatic theorem prover. We have written a variety of forward and backward intraprocedural data ow optimizations in our language, including constant propa-gation and folding, branch folding, (partial) redundancy elimination, (partial) dead assignment elimination, and simple forms of points-to analysis. We have implemented our proof strategy with the Simplify automatic theorem prover, and we have used this implementation to automatically prove our optimizations correct. Our system also found many subtle bugs during the course of developing our optimizations.