Toward a complete transformational toolkit for compilers

ABSTRACT

PIM is an equational logic designed to function as a “transformational toolkit” for compilers and other programming tools that analyze and manipulate imperative languages. It has been applied to such problems as program slicing, symbolic evaluation, conditional constant propagation, and dependence analysis. PIM consists of the untyped lambda calculus extended with an algebraic data type that characterizes the behavior of lazy stores and generalized conditionals. A graph form of PIM terms is by design closely related to several intermediate representations commonly used in optimizing compilers. In this article, we show that PIM's core algebraic component, PIMt, possesses a complete equational axiomatization (under the assumption of certain reasonable restrictions on term formation). This has the practical consequence of guaranteeing that every semantics-preserving transformation on a program representable in PIMt can be derived by application of PIMt rules. We systematically derive the complete PIMt logic as the culmination of a sequence of increasingly powerful equational systems starting from a straightforward “interpreter” for closed PIMt terms. This work is an intermediate step in a larger program to develop a set of well-founded tools for manipulation of imperative programs by compilers and other systems that perform program analysis.

REFERENCES

• 1: Zahira Ammarguellat, A Control-Flow Normalization Algorithm and its Complexity, IEEE Transactions on Software Engineering, v.18 n.3, p.237-251, March 1992 [doi>10.1109/32.126773]
• 2: Karl J. Ottenstein , Robert A. Ballance , Arthur B. MacCabe, The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.257-271, June 1990, White Plains, New York, United States
• 3: H P Barendregt , M C J D Eekelen , J R W Glauert , J R Kennaway , M J Plasmeijer , M R Sleep, Term graph rewriting, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.141-158, March 1987, Eindhoven, The Netherlands
• 4: J. A. Bergstra , J. Heering, Which data types have &ohgr;-complete initial algebra specifications?, Theoretical Computer Science, v.124 n.1, p.149-168, Feb. 14, 1994 [doi>10.1016/0304-3975(94)90057-4]
• 5: BERGSTRA, J. t. AND TUCKER, J. V. 1995. The data type variety of stack algebras. Ann. Pure Applied Logic 73, 1 (May), 11-36.
• 6: Andrew Berlin , Daniel Weise, Compiling Scientific Code Using Partial Evaluation, Computer, v.23 n.12, p.25-37, December 1990 [doi>10.1109/2.62091]
• 7: Hans-Juergen Boehm, Side effects and aliasing can have simple axiomatic descriptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.4, p.637-655, Oct. 1985 [doi>10.1145/4472.4474]
• 8: G Boudol, Computational semantics of term rewriting systems, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 9: E. Cartwright , M. Felleisen, The semantics of program dependence, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.13-27, June 19-23, 1989, Portland, Oregon, United States
• 10: C. Chambers , D. Ungar, Customization: optimizing compiler technology for SELF, a dynamically-typed object-oriented programming language, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.146-160, June 19-23, 1989, Portland, Oregon, United States
• 11: Cliff Click, Global code motion/global value numbering, ACM SIGPLAN Notices, v.30 n.6, p.246-257, June 1995
• 12: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 13: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 14: ERSHOV, A. P. 1982. Mixed computation: Potential applications and problems for study. Theoret. Comput. Sci. 18, 41-67.
• 15: A. P. Ershov , B. N. Ostrovski, Controlled mixed computation and its application to systematic development of language-oriented parsers, The IFIP TC2/WG 2.1 Working Conference on Program specification and transformation, p.31-48, June 1987, Bad To:9Ailz, Germany
• 16: M. Felleisen , D. P. Friedman, A syntactic theory of sequential state, Theoretical Computer Science, v.69 n.3, p.243-287, Dec. 18, 1989 [doi>10.1016/0304-3975(89)90069-8]
• 17: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 18: Jeanne Ferrante , Karl J. Ottenstein , Joe D. Warren, The program dependence graph and its use in optimization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.319-349, July 1987 [doi>10.1145/24039.24041]
• 19: FIELD, J. 1992. A simple rewriting semantics for realistic imperative programs and its application to program analysis. In Proceedings of the A CM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. ACM, New York, 98-107. Also available as Yale Univ. Technical Report YALEU/DCS/RR-909.
• 20: John Field , G. Ramalingam , Frank Tip, Parametric program slicing, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.379-392, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199534]
• 21: FRAUS, U. 1994. Inductive theorem proving for algebraic specifications--TIP system user's manual. Tech. Rep. MIP 9401, Univ. of Passau. The TIP system is available at ftp://forwiss.unipassau.de/pub/local/tip.
• 22: GARLAND, S. AND GUTTAG, J. 1991. A Guide to LP, The Larch Prover. Tech. Rep. 82, DEC Systems Research Center, Palo Alto, Calif. December.
• 23: HEERING, J. 1985. Variaties op het thema 'stack'. Tech. Rep. CS-N8502, CWI, Amsterdam. In Dutch.
• 24: J Heering, Partial evaluation and &ohgr;-completeness of algebraic specifications, Theoretical Computer Science, v.43 n.2-3, p.149-167, July 1986
• 25: C. A. R. Hoare , I. J. Hayes , He Jifeng , C. C. Morgan , A. W. Roscoe , J. W. Sanders , I. H. Sorensen , J. M. Spivey , B. A. Sufrin, Laws of programming, Communications of the ACM, v.30 n.8, p.672-686, Aug. 1987 [doi>10.1145/27651.27653]
• 26: S. Horwitz , J. Prins , T. Reps, On the adequacy of program dependence graphs for representing programs, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.146-157, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73573]
• 27: Jieh Hsiang , Nachum Dershowitz, Rewrite Methods for Clausal and Non-Clausal Theorem Proving, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.331-346, July 18-22, 1983
• 28: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 29: G. Kahn, Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences on STACS 87, p.22-39, February 1987, Passau, Germany
• 30: J. R. Kennaway , J. W. Klop , M. R. Sleep , F. J. de Vries, On the adequacy of graph rewriting for simulating term rewriting, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.493-523, May 1994 [doi>10.1145/177492.177577]
• 31: J. W. Klop, Term rewriting systems, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 32: A. Lazrek , P. Lescanne , J. J. Thiel, Tools for proving inductive equalities, relative completeness, and &ohgr;-completeness, Information and Computation, v.84 n.1, p.47-70, Jan. 1990 [doi>10.1016/0890-5401(90)90033-E]
• 33: I. Mason , C. Talcott, A sound and complete axiomatization of operational equivalence of programs with memory, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.284-293, June 1989, Pacific Grove, California, United States
• 34: K. Meinke , J. V. Tucker, Universal algebra, Handbook of logic in computer science (vol. 1): background: mathematical structures, Oxford University Press, Inc., New York, NY, 1993
• 35: J Meseguer , J A Goguen, Initiality, induction, and computability, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 36: Fritz Müller, Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, v.41 n.6, p.293-299, April 17, 1992 [doi>10.1016/0020-0190(92)90155-O]
• 37: Dimitri Naidich , T. B. Dinesh, Implicit induction techniques for the verification of{\sc Pim} -- a transformational toolkit for compilers, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1996
• 38: Vivek Nirkhe , William Pugh, Partial evaluation of high-level imperative programming languages with applications in hard real-time systems, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.269-280, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143223]
• 39: Martin Odersky , Dan Rabin , Paul Hudak, Call by name, assignment, and the lambda calculus, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.43-56, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158521]
• 40: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• 41: PLOTKIN, G. D. 1974. The ~-calculus is or-incomplete. J. Symbol. Logic 39, 2 (June), 313-317.
• 42: RAMALINGAM, G. AND REPS, T. 1989. Semantics of program representation graphs. Tech. Rep. 900, Computer Sciences Dept., Univ. of Wisconsin, Madison, Wisc. December.
• 43: R. Parsons-Selke, A rewriting semantics for program dependence graphs, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-24, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75279]
• 44: SELKE, R. P. 1989b. Transforming program dependence graphs. Tech. Rep. TR90-131, Dept. of Computer Science, Rice Univ., Houston, Tex. July.
• 45: Vipin Swarup , Uday S. Reddy , Evan Ireland, Assignments for applicative languages, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.192-214, June 1991, Cambridge, Massachusetts, United States
• 46: Arie Van Deursen , Jan Heering , Paul Klint, Language Prototyping: An Algebraic Specification Approach: Vol. V, World Scientific Publishing Co., Inc., River Edge, NJ, 1996
• 47: WAND, M. AND WANG, Z.-Y. 1990. Conditional lambda-theories and the verification of static properties of programs. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science. IEEE, New York.
• 48: Daniel Weise , Roger F. Crew , Michael Ernst , Bjarne Steensgaard, Value dependence graphs: representation without taxation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.297-310, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177907]
• 49: Martin Wirsing, Algebraic specification, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 50: YANG, W., HORWITZ, S., AND REPS, T. 1989. Detecting program components with equivalent behaviors. Tech. Rep. 840, Univ. of Wiconsin, Madison, Wisc. April.
• 51: Wuu Yang , Susan Horwitz , Thomas Reps, A program integration algorithm that accommodates semantics-preserving transformations, Proceedings of the fourth ACM SIGSOFT symposium on Software development environments, p.133-143, December 03-05, 1990, Irvine, California, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Partial evaluation

General Terms:
Languages, Theory

Keywords:
compiler intermediate representation, completion, imperative language, partial evaluation, program transformation, term-rewriting