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 first present a domainspecific language, called Cobalt, for implementing optimizations as guarded rewrite rules. Cobalt optimizations operate over a C-like intermediate representation including unstructured control flow, pointers to local variables and dynamically allocated memory, and recursive procedures. Then we describe a technique for automatically proving the soundness of Cobalt optimizations. Our technique requires an automatic theorem prover to discharge a small set of simple, optimization-specific proof obligations for each optimization. We have written a variety of forward and backward intraprocedural dataflow optimizations in Cobalt, including constant propagation and folding, branch folding, full and partial redundancy elimination, full and partial dead assignment elimination, and simple forms of points-to analysis. We ...

• Type: Conference
• Year: 2003
• Where: PLDI
• Authors: Sorin Lerner, Todd D. Millstein, Craig Chambers
• Keywords: Automatic Theorem Prover, Cobalt Optimizations, Compiler Optimization, PLDI 2003, Programming Languages