Validation of Interprocedural Optimizations
Amir Pnueli, Anna Zaks · 2008
Translation validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code produced by the compiler is a correct translation of the source code. We present a framework for translation validation of compiler optimization run that targets reactive procedural programs. Our algorithm is automatic, requires minor compiler cooperation, and accommodates most classical interprocedural optimizations such as global constant propagation, inlining, tail-recursion elimination, interprocedural dead code elimination, dead argument elimination, and cloning.