Automatic validation of code-improving transformations on low-level program representations

This paper presents a general approach for automatically validating code-improving transformations on low-level program representations. The approach ensures the correctness of compiler and hand-specified optimizations at the machine instruction level. The method verifies the semantic equivalence of the program representation before and after a transformation to determine the validity of the transformation. To verify that the transformation is semantics preserving, the method derives semantic effects from the instructions that span the execution paths affected by the transformation. The semantics are preserved if the normalized semantic effects are unchanged. A validating compilation system was implemented that is able to validate traditional compiler transformations and more powerful transformations that modify the branch structure of a program.