Ph.D. Thesis: Automatically Proving the Correctness of Program Analyses and Transformations

Sorin Lerner

In this dissertation, I describe a technique for automatically proving compiler optimizations sound, meaning that their transformations are always semantics-preserving. I first present a domain-specific language, called Rhodium, for implementing optimizations using local propagation and transformation rules that manipulate explicit dataflow facts. Then I describe a technique for automatically proving the soundness of Rhodium optimizations. The technique requires an automatic theorem prover to discharge a simple proof obligation for each propagation and transformation rule.

I have written a variety of forward and backward intraprocedural dataflow optimizations in Rhodium, including constant propagation and folding, branch folding, full and partial redundancy elimination, full and partial dead assignment elimination, an intraprocedural version of Andersen's points-to analysis, arithmetic-invariant detection, loop-induction-variable strength reduction, and redundant array load elimination. I implemented Rhodium's soundness-checking strategy using the Simplify theorem prover, and I have used this implementation to automatically prove that the Rhodium optimizations I wrote were sound. I implemented a prototype execution engine for Rhodium so that Rhodium optimizations can be directly executed. I also developed a way of interpreting Rhodium optimizations in both flow-sensitive and -insensitive ways, and of applying them interprocedurally given a separate context-sensitivity strategy, all while retaining soundness.

To get the PDF file, click here.