Automatically Proving the Correctness of Compiler Optimizations

We describe a technique for automatically proving compiler optimizations sound, meaning that their transformations are always semantics-preserving. We rst present a domain- specic language, called Cobalt, for implementing optimiza- tions as guarded rewrite rules. Cobalt optimizations operate over a C-like intermediate representation including unstruc- tured control o w, pointers to local variables and dynami- cally allocated memory, and recursive procedures. Then we describe a technique for automatically proving the sound- ness of Cobalt optimizations. Our technique requires an au- tomatic theorem prover to discharge a small set of simple, optimization-specic proof obligations for each optimiza- tion. We have written a variety of forward and backward intraprocedural datao w optimizations in Cobalt, includ- ing constant propagation and folding, branch folding, full and partial redundancy elimination, full and partial dead assignment elimination, and simple forms of points-to analy- sis. We implemented our soundness-checking strategy using the Simplify automatic theorem prover, and we have used this implementation to automatically prove our optimiza- tions correct. Our checker found many subtle bugs during the course of developing our optimizations. We also imple- mented an execution engine for Cobalt optimizations as part of the Whirlwind compiler infrastructure. Categories and Subject Descriptors