Sciweavers

Share
PLDI
2003
ACM

Automatically proving the correctness of compiler optimizations

9 years 2 months ago
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 ...
Sorin Lerner, Todd D. Millstein, Craig Chambers
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where PLDI
Authors Sorin Lerner, Todd D. Millstein, Craig Chambers
Comments (0)
books