Automatically Proving the
Correctness of Compiler Optimizations
In ACM SIGPLAN
Conference on Programming Language Design and Implementation (PLDI
2003), San Diego, California, June 9-11, 2003. Best Paper Award
Sorin Lerner,
Todd Millstein, and
Craig Chambers,
We describe a technique for automatically proving compiler
optimizations sound, meaning that their transformations are
always semantics-preserving. We first present a domain-specific
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 implemented our soundness-checking strategy using the Simplify
automatic theorem prover, and we have used this implementation to
automatically prove our optimizations correct. Our checker found
many subtle bugs during the course of developing our optimizations.
We also implemented an execution engine for
Cobalt optimizations as part of the Whirlwind compiler
infrastructure.
[Postscript |
PDF]