Type elaboration and subtype completion for Java bytecode

ABSTRACT

Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely typed bytecode by inferring types for local variables. There are situations where, technically, there are not enough types in the original type hierarchy to type a bytecode program. Subtype completion is a technique for adding necessary types to an arbitrary type hierarchy to make type elaboration possible for all verifiable Java bytecode. Type elaboration with subtype completion has been implemented as part of the Marmot Java compiler.

REFERENCES

• ABLN89: Hassan Aït-Kaci , Robert Boyer , Patrick Lincoln , Roger Nasr, Efficient implementation of lattice operations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.115-146, Jan. 1989 [doi>10.1145/59287.59293]
• Bac97: David Francis Bacon , Susan L. Graham, Fast and effective optimization of statically typed object-oriented languages, 1997
• Ben93: Marcin Benke, Efficient Type Reconstruction in the Presence of Inheritance, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.272-280, August 30-September 03, 1993
• Bir95: C. Birkhoff. Lattice Theory, volume 25 of Colloquium Publications. American Mathematical Society, Providence, RI, third edition, 1995.
• Cas93: Yves Caseau, Efficient handling of multiple inheritance hierarchies, Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, p.271-287, September 26-October 01, 1993, Washington, D.C., United States
• CFR+89: R. Cytron , J. Ferrante , B. K. Rosen , M. N. Wegman , F. K. Zadeck, An efficient method of computing static single assignment form, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.25-35, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75280]
• CGQ98: Susan Eisenbach, Formal underpinnings of Java, Addendum to the 1998 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), January 1998, Vancouver, British Columbia, Canada [doi>10.1145/346852.346968]
• DP90: B.A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge Mathematical Textbooks, Cambridge University Press, 1990.
• FKR+: Robert Fitzgerald , Todd B. Knoblock , Erik Ruf , Bjarne Steensgaard , David Tarditi, Marmot: an optimizing compiler for Java, Software—Practice & Experience, v.30 n.3, p.199-232, Mar.1.2000 [doi>10.1002/(SICI)1097-024X(200003)30:3<199::AID-SPE296>3.0.CO;2-2]
• FM98: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, ACM SIGPLAN Notices, v.33 n.10, p.310-327, Oct. 1998
• FM99: Stephen N. Freund and John C. Mitchell. A type system for Java bytecode subroutines and exceptions. Technical report, Standford Univeristy, Computer Science Department, April 1999.
• Fre98: Susan Eisenbach, Formal underpinnings of Java, Addendum to the 1998 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), January 1998, Vancouver, British Columbia, Canada [doi>10.1145/346852.346968]
• GH99: Etienne Gagnon and Laurie Hendren. Intra, procedural inference of static types for java bytecode. Technical Report 1, McGill University, 1999.
• GJS96: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• Gol97: Allen Goldberg. A specification of Java loading and bytecode verification. Technical Report KES.U.92.1, Kestrel Institute, December 1997.
• HM95: My Hoang , John C. Mitchell, Lower bounds on type inference with subtypes, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.176-185, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199481]
• IBM98: IBM. IBM high performance compiler for Java: An optimizing native code compiler for Java applications. http: //www. alphaworks, ibm. corn/ graphics.nsf/system/graphics/HPCJ/ $file/highpcj.html, May 1998.
• Ins98: Instantiations, Inc. Jove: Super optimizing deployment environment for Java. http://www.instantiations.com/j avaspeed / jovereport.htm, July 1998.
• KR99: Todd Knoblock and Jakob Rehof. Type elaboration and subtype completion for java bytecode. Technical Report MSR-TR-99-79, Microsoft Research, Redmond, WA, USA, November 1999.
• LM92: Patrick Lincoln , John C. Mitchell, Algorithmic aspects of type inference with subtypes, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.293-304, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143227]
• LO98: Proceedings of the Second International Workshop on Types in Compilation, March 1998
• LST99: Christopher League , Zhong Shao , Valery Trifonov, Representing Java classes in a typed intermediate language, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.183-196, September 27-29, 1999, Paris, France
• LY99: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• Mac37: H.M. MacNeille. Partially ordered sets. Transactions of the American Mathematical Society, 42:90-96, 1937.
• Mor95: J. Gregory Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, December 1995. Published as CMU Technical Report CMU-CS-95-226.
• MWCG97: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From System F to Typed Assembly Language (Extended Version), Cornell University, Ithaca, NY, 1997
• Nat98: NaturalBridge, LLC. Bullettrain Java compiler technology. http://www.naturalbridge.com/, 1998.
• Nec98: George Ciprian Necula , Peter Lee, Compiling with proofs, 1998
• O’C99: Robert O'Callahan, A simple, comprehensive type system for Java bytecode subroutines, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-78, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292549]
• ON99: David von Oheimb , Tobias Nipkow, Machine-Checking the Java Specification: Proving Type-Safety, Formal Syntax and Semantics of Java, p.119-156, January 1999
• PO95: Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
• PT96: Vaughan Pratt , Jerzy Tiuryn, Satisfiability of inequalities in a poset, Fundamenta Informaticae, v.28 n.1-2, p.165-182, Nov. 1996
• Pus99: Cornelia Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.89-103, March 22-28, 1999
• Qia98: Zhenyu Qian, A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subrountines, Formal Syntax and Semantics of Java, p.271-312, January 1999
• Qia99: Zhenyu Qian. Least types for memory locations in (Java) bytecode. Technical report, Kestrel Institute, 1999. http://www.kestrel, edu / HTM L/people/ qian/pub-list.html.
• SA98: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
• Shi91: Olin Shivers. Data-flow analysis and type recovery in scheme. In Peter Lee, editor, Topics in Advanced Language Implementation, chapter 3, pages 47-87. The MIT Press, 1991.
• Sup98: SuperCede, Inc. SuperCede for Java, Version 2.03~ Upgrade Edition. http://www.supercede.com/, September 1998.
• Sym97: Don Syme. Proving JavaS type soundness. Technical Report 427, University of Cambridge Computer Laboratory, 1997.
• Tar72: Robert E. Tarjan. Depth first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146-160, 1972.
• Tar96: David Tarditi. Design and implementation o} Coite Optimizations for a Type-Directed Compiler for Standard ML. PhD thesis, Carnegie Mellon University, December 1996.
• Tiu92: J. Tiuryn. Subtype inequalities. In Prec. 7th Annual IEEE Syrup. on Logic in Computer Science (LICS), Santa Cruz, California, pages 308-315. IEEE Computer Society Press, June 1992.
• Yel99: Phillip M. Yelland, A compositional account of the Java virtual machine, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.57-69, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292548]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Design, Languages