Verifying the correctness of compiler transformations on basic blocks using abstract interpretation
Timothy S. McNerney · 1991
Interpretation Timothy S. McNerney Thinking Machines Corporation 245 First Street Cambridge, MA 02142 [email protected] Abstract We seek to develop thorough and reliable methods for testing compiler transformations by systematically generating a set of test cases, and then for each case, automatically proving that the transformation preserves correctness. We have implemented a specialized program equivalence prover for the domain of assembly language programs emitted by the Connection Machine Fortran compiler and targeted for the CM-2 massively parallel SIMD computer. Using abstract interpretation, the prover removes details such as register and stack usage, as well as explicit evaluation order within functional blocks, thereby reducing the problem to a trivial tree comparison. By performing limited loop unrolling, the prover also verifies that the compiler transformation preserves the inductive properties of simple loops. We have used this prover to successfully validate the re...