Compiler optimization correctness by temporal logic

Abstract. Rewrite rules with side conditions can elegantly express many classi-cal compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are speci¯ed in a temporal logic suitable for describing program data °ow. The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if when-ever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. 1