Bidirectional data-flow analyses, type-systematically

ABSTRACT

We show that a wide class of bidirectional data-flow analyses and program optimizations based on them admit declarative descriptions in the form of type systems. The salient feature is a clear separation between what constitutes a valid analysis and how the strongest one can be computed (via the type checking versus principal type inference distinction). The approach also facilitates elegant relational semantic soundness definitions and proofs for analyses and optimizations, with an application to mechanical transformation of program proofs, useful in proof-carrying code. Unidirectional forward and backward analyses are covered as special cases; the technicalities in the general bidirectional case arise from more subtle notions of valid and principal types. To demonstrate the viability of the approach we consider two examples that are inherently bidirectional: type inference (seen as a data-flow problem) for a structured language where the type of a variable may change over a program's run and the analysis underlying a stack usage optimization for a stack-based low-level language.

REFERENCES

• 1: F. Bannwart, P. Müller. A program logic for bytecode. In Proc. of 1st Wksh. on Bytecode Semantics, Verification, Analysis and Transformation, Bytecode 2005, v. 141(1) of Electron. Notes in Theor. Comput. Sci., pp. 255--273, Elsevier, 2005
• 2: G. Barthe, B. Grégoire, C. Kunz, T. Rezk. Certificate translation for optimizing compilers. In K. Yi, ed., Proc. of 13th Int. Symp. on Static Analysis, SAS 2006, v. 4134 of Lect. Notes in Comput. Sci., pp. 301--317, Springer, 2006.
• 3: G. Barthe, C. Kunz. Certificate translation in abstract interpretation. In S. Drossopoulou, ed., Proc. of 17th Europ. Symp. on Programming, ESOP 2008, v. 4960 of Lect. Notes in Comput. Sci., pp. 368--382, Springer, 2008.
• 4: Nick Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.14-25, January 14-16, 2004, Venice, Italy
• 5: Y. N. Srikant , Priti Shankar, Compiler Design Handbook: Optimizations and Machine Code Generation, CRC Press, Inc., Boca Raton, FL, 2002
• 6: Uday P. Khedker , Dhananjay M. Dhamdhere, A generalized theory of bit vector data flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1472-1511, Sept. 1994 [doi>10.1145/186025.186043]
• 7: Uday P. Khedker , Dhananjay M. Dhamdhere, Bidirectional data flow analysis: myths and reality, ACM SIGPLAN Notices, v.34 n.6, June 1999 [doi>10.1145/606666.606676]
• 8: U. P. Khedker, D. M. Dhamdhere, A. Mycroft. Bidirectional data flow analysis for type inferencing. Comput. Lang., Syst. and Struct., 29(1-2):15--44, 2003.
• 9: Maria Joao Frade , Ando Saabas , Tarmo Uustalu, Foundational certification of data-flow analyses, Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, p.107-116, June 06-08, 2007 [doi>10.1109/TASE.2007.27]
• 10: Neil D. Jones , Steven S. Muchnick, Binding time optimization in programming languages: Some thoughts toward the design of an ideal language, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.77-94, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811542]
• 11: Marc A. Kaplan , Jeffrey D. Ullman, A Scheme for the Automatic Inference of Variable Types, Journal of the ACM (JACM), v.27 n.1, p.128-145, Jan. 1980 [doi>10.1145/322169.322181]
• 12: Peeter Laud , Tarmo Uustalu , Varmo Vene, Type systems equivalent to data-flow analyses for imperative languages, Theoretical Computer Science, v.364 n.3, p.292-310, 8 November 2006 [doi>10.1016/j.tcs.2006.08.013]
• 13: Sorin Lerner , Todd Millstein , Erika Rice , Craig Chambers, Automated soundness proofs for dataflow analyses and transformations via local rules, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.364-377, January 12-14, 2005, Long Beach, California, USA
• 14: Hanne Riis Nielson , Flemming Nielson, Flow logic: a multi-paradigmatic approach to static analysis, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
• 15: A. Saabas. Logics for low-level code and proof-preserving program transformations (PhD thesis), Thesis on Informatics and System Engineering C143. Tallinn Univ. of Techn., 2008.
• 16: A. Saabas, T. Uustalu. Program and proof optimizations with type systems. J. of Logic and Algebraic Program., 77(1-2):131--154, 2008.
• 17: Ando Saabas , Tarmo Uustalu, Proof optimization for partial redundancy elimination, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA [doi>10.1145/1328408.1328422]
• 18: Ando Saabas , Tarmo Uustalu, Type Systems for Optimizing Stack-based Code, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.1, p.103-119, July, 2007 [doi>10.1016/j.entcs.2007.02.063]
• 19: A. Tenenbaum. Type determination for very high level languages. Report NSO-3, Courant Inst. of Math. Sci., New York Univ., New York, 1974.
• 20: T. Van Drunen, A. L. Hosking, J. Palsberg. Reducing loads and stores in stack architectures, manuscript, 2000.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Program analysis

General Terms:
Languages, Theory, Verification

Keywords:
mechanical transformation of program proofs, program analyses and optimizations, program logics, type systems