Cobalt: A Language for Writing Provably-Sound Compiler Optimizations

AbstractWe 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