Cobalt: A Language for Writing Provably-Sound Compiler Optimizations

Electronic Notes in Theoretical Computer Science (ENTCS), 132(1):5-17, May 2005.
Sorin Lerner, Todd Millstein, Craig Chambers
This paper is a short invited contribution overviewing the Cobalt language. A detailed discussion of Cobalt can be found in our PLDI 2003 paper, and Cobalt's successor language, called Rhodium, is described in our POPL 2005 paper.

We overview the current status and future directions of the Cobalt project. Cobalt is a domain-specific language for implementing compiler 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. The design of Cobalt engenders a natural inductive strategy for proving the soundness of optimizations. This strategy is fully automated by requiring an automatic theorem prover to discharge a small set of simple 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. The implementation of our soundness-checking strategy employs the Simplify automatic theorem prover, and we have used this implementation to automatically prove the above optimizations correct. An execution engine for Cobalt optimizations is implemented as part of the Whirlwind compiler infrastructure.