Formal Verification of Transformations for Peephole Optimization

A. Dold, F. W. von Henke, H. Pfeifer, H. Rueß

In this paper we describe a formal verification of transformations for peephole optimization using the PVS system. Our basic approach is to develop a generic scheme to mechanize these kinds of verifications for a large class of machine architectures. This generic scheme is instantiated with a formalization of a non-trivial stack machine and a PDP-11 like two-address machine, and we prove the correctness of more than 100 published peephole optimization rules for these machines. In the course of verifying these transformations we found several errors in published peephole transformation steps. From the information of failed proof attempts, however, we were able to discover strengthened preconditions for correcting the erroneous transformations.

Available as Postscript (114 KB) or gzipped Postscript (45 KB)

PVS Specification files: peephole.dump or gzipped peephole.dump.gz

@InProceedings{DHPR97,
  author =       "A. Dold and F.W. von Henke and H. Pfeifer and H. Rue{\ss}",
  title =        "Formal Verification of Transformations for Peephole
                  Optimization",
  editor =       "J. Fitzgerald, C.B. Jones, P. Lucas",
  volume =       "1313",
  series =       "Lecture Notes in Computer Science",
  pages =        "459--472",
  booktitle =    "{FME} '97: Formal Methods: Their Industrial Application 
                     and Strengthened Foundations}", 
  year =         1997,
  publisher =    "Springer Verlag",
  month =        September
}