Automatically proving the correctness of compiler optimizations

• DOI: 10.1145/781131.781156
• Publication Date: 2004-04-19T17:18:43Z
• Authors: Sorin Lerner; Todd Millstein; Craig Chambers
• Keywords: Soundness; Gas meter prover; Control flow

We describe a technique for automatically proving compiler optimizations sound, meaning that their transformations are always semantics-preserving. first present domain-specific language, called Cobalt, implementing as guarded rewrite rules. Cobalt operate over C-like intermediate representation including unstructured control flow, pointers to local variables and dynamically allocated memory, recursive procedures. Then we the soundness of optimizations. Our requires an automatic theorem prover discharge small set simple, optimization-specific proof obligations each optimization. have written variety forward backward intraprocedural dataflow in constant propagation folding, branch full partial redundancy elimination, dead assignment simple forms points-to analysis. implemented our soundness-checking strategy using Simplify prover, used this implementation prove correct. checker found many subtle bugs during course developing also execution engine part Whirlwind infrastructure.