Formal verification of transformations for peephole optimization

  • A. Dold
  • F. W. von Henke
  • H. Pfeifer
  • H. Rueß
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


In this paper we describe a formal verification of transformations for peephole optimization using the PVS system [12]. 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 [14] and a PDP-11 like two-address machine [2], 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 [14]. From the information of failed proof attempts, however, we were able to discover strengthened preconditions for correcting the erroneous transformations.


formal verification transformations higher-order logic reusability of specifications 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A Tutorial Introduction to PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park CA 94025, USA, March 1995. To presented at WIFT'95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida.Google Scholar
  2. 2.
    Jack W. Davidson and Christoper W. Fraser. The Design and Application of a Retargetable Peephole Optimizer. ACM Transactions on Programming Languages and Systems, 2(2):191–202, April 1980.Google Scholar
  3. 3.
    Jack W. Davidson and Christoper W. Fraser. Register Allocation and Exhaustive Peephole Optimization. Software-Practice and Experience, 14(9):857–865, September 1984.Google Scholar
  4. 4.
    Jack W. Davidson and Christoper W. Fraser. Automatic Inference and fast Interpretation of Peephole Optimization Rules. Software-Practice and Experience, 17(11):801–812, November 1987.Google Scholar
  5. 5.
    A. Dold, F. W. von Henke, H. Pfeifer, and H. Rueß. A Generic Specification for Verifying Peephole Optimizations. Technical Report UIB-95-14, Universitat Ulm, Fakultät fur Informatik, 89069-Ulm, Germany, December 1995.Google Scholar
  6. 6.
    A. Dold, F.W. von Henke, H. Pfeifer, and H. Rueß. Generic Compilation Schemes for Simple Programming Constructs. Technical Report UIB-96-12, Universität Ulm, Fakultat für Informatik, 89069-U1m, Germany, December 1996.Google Scholar
  7. 7.
    Andrew Gill. A Novel Approach Towards Peephole Optimisations. In Proceedings of the 4th Annual Glasgow Workshop on Functional Programming, Workshops in Computer Science. Springer-Verlag, August 1991.Google Scholar
  8. 8.
    Peter B. Kessler. Discovering Machine Specific Code Improvements. Sigplan Notices, 21(7):249–254, 1986.Google Scholar
  9. 9.
    Robert R. Kessler. Peep — an Architectural Description Driven Peephole Optimizer. Sigplan Notices, 19(6):106–110, June 1984.Google Scholar
  10. 10.
    David Alex Lamb. Construction of a Peephole Optimizer. Software-Practice and Experience, 11(6):639–647, June 1981.Google Scholar
  11. 11.
    Timothy S. McNerney. Verifying the Correctness of Compiler Transformations on Basic Blocks using Abstract Interpretation. Sigplan Notices, 26(9):106–115, 1991.Google Scholar
  12. 12.
    S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for FaultTolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.Google Scholar
  13. 13.
    S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, 1992. Springer-Verlag.Google Scholar
  14. 14.
    Andrew S. Tanenbaum, Hans van Staveren, and Johan W. Stevenson. Using Peephole Optimization on Intermediate Code. ACM Transactions on Programming Languages and Systems, 4(1):21–36, January 1982.Google Scholar
  15. 15.
    P.J. Windley. A Theory of Generic Interpreters. In George J. Milne and Laurence Pierre, editors, Correct Hardware Design and Verification Methods, volume 683 of Lecture Notes in Computer Science, pages 122–134. Springer-Verlag, May 1993.Google Scholar
  16. 16.
    P.J. Windley. Specifying Instruction-Set Architectures in HOL: A Primer. In Thomas F. Melham and Juanito Camilleri, editors, Proceedings of the 7th International Workshop on the Higher-Order Logic Theorem Proving and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 440–455. Springer-Verlag, September 1994.Google Scholar
  17. 17.
    P.J. Windley and M. Coe. Microprocessor Verification: A Tutorial. Technical Report LAL-92-10, University of Idaho, Department of Computer Science, Laboratory for Applied Logic, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • A. Dold
    • 1
  • F. W. von Henke
    • 1
  • H. Pfeifer
    • 1
  • H. Rueß
    • 1
  1. 1.Fakultät für InformatikUniversität UlmUlmGermany

Personalised recommendations