Yutaka Matsuno
Atsushi Ohori
ABSTRACT
This paper develops a static type system equivalent to static single assignment (SSA) form. In this type system, a type of a variable at some program point represents the control flows from the assignment statements that reach the program point. For this type system, we show that a derivable typing of a program corresponds to the program in SSA form. By this result, any SSA transformation can be interpreted as a type inference process in our type system. By adopting a result on efficient SSA transformation, we develop a type inference algorithm that reconstructs a type annotated code from a given code. These results provide a static alternative to SSA based compiler optimization without performing code transformation. Since this process does not change the code, it does not incur overhead due to insertion of φ functions. Another advantage of this type based approach is that it is not constrained to naming mechanism of variables and can therefore be combined with other static properties useful for compilation and code optimization such as liveness information of variables. As an application, we express optimizations as type-directed code transformations
- Bowen Alpern, Mark N. Wegman, and F. Kenneth Zadeck. Detecting equality of variables in programs. In POPL, pages 1--11, 1988.]] Google Scholar
Digital Library
- Andrew W. Appel. SSA is functional programming. ACM SIGPLAN Notices, 33(4):17--20, 1998.]] Google ScholarDigital Library
- Nick Benton. Simple relational correctness proofs for static analyses and program transformations. In POPL, pages 14--25, 2004.]] Google ScholarDigital Library
- Gianfranco Bilardi and Keshav Pingali. Algorithms for computing the static single assignment form. J. ACM, 50(3):375--425, 2003.]] Google ScholarDigital Library
- Preston Briggs, Keith D. Cooper, Timothy J. Harvey, and L. Taylor Simpson. Practical improvements to the construction and destruction of static single assignment form. Software Practice and Experience, 28(8):859--881, 1998.]] Google ScholarDigital Library
- M. Chakravarty, P. Keller, and P. Zadarnowski. A functional perspective on SSA optimisation algorithms. Technical Report 0217, University of New South Wales, 2003.]]Google Scholar
- Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. Automatic construction of sparse data flow evaluation graphs. In POPL, pages 55--66, 1991.]] Google ScholarDigital Library
- Keith D. Cooper, L. Taylor Simpson, and Christopher A. Vick. Operator strength reduction. TOPLAS, 23(5):603--625, 2001.]] Google ScholarDigital Library
- Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 13(4):451--490, 1991.]] Google ScholarDigital Library
- Dibyendu Das and U. Ramakrishna. A practical and fast iterative algorithm for phi-function computation using dj graphs. TOPLAS, 27(3):426--440, 2005.]] Google ScholarDigital Library
- Richard A. Kelsey. A correspondence between continuation passing style and static single assignment form. ACM SIGPLAN Notices, 30(3):13--22, 1995.]] Google ScholarDigital Library
- Robert Kennedy, Sun Chan, Shin-Ming Liu, Raymond Lo, Peng Tu, and Fred Chow. Partial redundancy elimination in SSA form. TOPLAS, 21(3):627--676, 1999.]] Google ScholarDigital Library
- Jens Knoop, Oliver Ruthing, and Bernhard Steffen. Lazy code motion. In PLDI, pages 224--234, 1992.]] Google ScholarDigital Library
- David Lacey, Neil Jones, Eric Van Wyk, and Carl Christian Frederikson. Proving correctness of compiler optimizations by temporal logic. Higher-Order and Symbolic Computation, 17(2), 2004.]] Google ScholarDigital Library
- Sorin Lerner, Todd D. Millstein, and Craig Chambers. Automatically proving the correctness of compiler optimizations. In PLDI, pages 220--231, 2003.]] Google ScholarDigital Library
- Sorin Lerner, Todd D. Millstein, Erika Rice, and Craig Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In POPL, pages 364--377, 2005.]] Google ScholarDigital Library
- Xavier Leroy. Java bytecode verification: Algorithms and formalizations. J. Autom. Reasoning, 30(3-4):235--269, 2003.]] Google ScholarDigital Library
- Vijay S. Menon, Neal Glew, Brian R. Murphy, Andrew McCreight, Tatiana Shpeisman, Ali-Reza Adl-Tabatabai, and Leaf Petersen. A verifiable ssa program representation for aggressive compiler optimization. In POPL, pages 397--408, 2006.]] Google ScholarDigital Library
- Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. TOPLAS, 21(3):527--568, 1999.]] Google ScholarDigital Library
- George Necula. Proof-carrying code. In POPL, pages 106--119, 1997.]] Google ScholarDigital Library
- Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999.]] Google ScholarDigital Library
- Atsushi Ohori. The logical abstract machine: A curry-howard isomorphism for machine code. In Fuji International Symposium on Functional and Logic Programming, pages 300--318, 1999. (An extended version is available under the title "A Proof Theory for Machine Code" from the author's home page: http://www.pllab.riec.tohoku.ac.jp/~ohori/.)]] Google ScholarDigital Library
- Atsushi Ohori. Register allocation by proof transformation. Sci. Comput. Program (also in ESOP'03)., 50(1-3):161--187, 2004.]] Google ScholarDigital Library
- Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Global value numbers and redundant computations. In POPL, pages 12--27, 1988.]] Google ScholarDigital Library
- Vugranam C. Sreedhar, Roy Dz-Ching Ju, David M. Gillies, and Vatsa Santhanam. Translating out of static single assignment form. In SAS, pages 194--210, 1999.]] Google ScholarDigital Library
- Raymie Stata and Martín Abadi. A type system for Java bytecode subroutines. In POPL, pages 149--160, 1998.]] Google ScholarDigital Library
- Michael Weiss. The transitive closure of control dependence: The iterated join. LOPLAS, 1(2):178--190, 1992.]] Google ScholarDigital Library
- The SML# Home page. http://www.pllab.riec.tohoku.ac.jp/smlsharp/]]Google Scholar
Index Terms
- A type system equivalent to static single assignment
Recommendations
Finitary polymorphism for optimizing type-directed compilation
We develop a type-theoretical method for optimizing type directed compilation of polymorphic languages, implement the method in SML#, which is a full-scale compiler of Standard ML extended with several advanced features that require type-passing ...
An idea for a type system of multi-paradigm language with extensible syntax
CompSysTech '12: Proceedings of the 13th International Conference on Computer Systems and TechnologiesThis article proposes a type system for a multi-paradigm language paradigm. A practical solution that provides the benefits of both static and dynamic typing is proposed, while using the features of the prototype - extensible declarative syntax. A ...
A practical type system and language for reference immutability
OOPSLA '04: Proceedings of the 19th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applicationsThis paper describes a type system that is capable of expressing and enforcing immutability constraints. The specific constraint expressed is that the abstract state of the object to which an immutable reference refers cannot be modified using that ...
Comments