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

• 1: 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]
• 2: David Francis Bacon , Susan L. Graham, Fast and effective optimization of statically typed object-oriented languages, 1997
• 3: 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
• 4: Birkhoff, G. 1995. Lattice Theory , third ed. Colloquium Publications, vol. 25. American Mathematical Society, Providence, RI.
• 5: 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
• 6: Coglio, A., Goldberg, A., and Qian, Z. 1998. Towards a provably-correct implementation of the JVM bytecode veriaer. Tech. Rep. KES.U.98.5, Kestrel Institue. August 1998. Also availabe in Proceedings of the OOPSLA '98 Workshop on the Formal Underpinnings of Java, Vancouver, B.C., October 1998.
• 7: 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]
• 8: Davey, B. A. and Priestley, H. A. 1990. Introduction to Lattices and Order. Cambridge Mathematical Textbooks, Cambridge University Press.
• 9: 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]
• 10: Freund, S. N. 1998. The costs and benefits of Java bytecode subroutines. In Formal Underpinnings of Java Workshop at OOPSLA. http://ww-dse.doc.ic.ac.edu/ c_sue/ oopsla/cfp.html.
• 11: Stephen N. Freund , John C. Mitchell, A type system for object initialization in the Java bytecode language, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.310-327, October 18-22, 1998, Vancouver, British Columbia, Canada
• 12: Freund, S. N. and Mitchell, J. C. 1999. A type system for Java bytecode subroutines and exceptions. Tech. rep., Stanford Univeristy, Computer Science Department. April.
• 13: Gagnon, E. and Hendren, L. 1999. Intra-procedural inference of static types for Java bytecode. Tech. Rep. 1, McGill University.
• 14: Goldberg, A. 1997. A specification of Java loading and bytecode verification. Tech. Rep. KES.U.92.1, Kestrel Institute. December.
• 15: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 16: 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]
• 17: IBM. 1998. IBM high performance compiler for Java: An optimizing native code compiler for Java applications. http://www.alphaworks.ibm.com/ graphics.nsf/system/graphics/HPCJ/ $file/highpcj.html.
• 18: Instantiations, Inc. 1998. Jove: Super optimizing deployment environment for Java. http://www.instantiations.com/javaspeed/ jovereport.htm.
• 19: Dexter Kozen , Jens Palsberg , Michael I. Schwartzbach, Efficient inference of partial types, Journal of Computer and System Sciences, v.49 n.2, p.306-324, Oct. 1994 [doi>10.1016/S0022-0000(05)80051-0]
• 20: 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
• 21: Proceedings of the Second International Workshop on Types in Compilation, March 1998
• 22: 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]
• 23: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 24: MacNeille, H. M. 1937. Partially ordered sets. Transactions of the American Mathematical Society 42, 90-96.
• 25: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From System F to Typed Assembly Language (Extended Version), Cornell University, Ithaca, NY, 1997
• 26: Morrisett, J. G. 1995. Compiling with types. Ph.D. thesis, Carnegie Mellon University. Published as CMU Technical Report CMU-CS-95-226.
• 27: NaturalBridge, LLC. 1998. Bullettrain Java compiler technology. http://www.naturalbridge.com/.
• 28: George Ciprian Necula , Peter Lee, Compiling with proofs, 1998
• 29: 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]
• 30: David von Oheimb , Tobias Nipkow, Machine-Checking the Java Specification: Proving Type-Safety, Formal Syntax and Semantics of Java, p.119-156, January 1999
• 31: 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]
• 32: Vaughan Pratt , Jerzy Tiuryn, Satisfiability of inequalities in a poset, Fundamenta Informaticae, v.28 n.1-2, p.165-182, Nov. 1996
• 33: 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
• 34: 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
• 35: Qian, Z. 1999. Least types for memory locations in (Java) bytecode. Tech. rep., Kestrel Institute. http://www.kestrel.edu/HTML/people/ qian/pub-list.html.
• 36: Jakob Rehof , Torben Ægidius Mogensen, Tractable constraints in finite semilattices, Science of Computer Programming, v.35 n.2-3, p.191-221, Nov.1.1999 [doi>10.1016/S0167-6423(99)00011-8]
• 37: Shivers, O. 1991. Data- ow analysis and type recovery in scheme. In Topics in Advanced Language Implementation, P. Lee, Ed. The MIT Press, Chapter 3, 47-87.
• 38: 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]
• 39: SuperCede, Inc. 1998. SuperCede for Java, Version 2.03, Upgrade Edition. http://www.supercede.com/.
• 40: Syme, D. 1997. Proving JavaS type soundness. Tech. Rep. 427, University of Cambridge Computer Laboratory.
• 41: Tarditi, D. 1996. Design and implementation of code optimizations for a type-directed compiler for standard ml. Ph.D. thesis, Carnegie Mellon University.
• 42: Tarjan, R. E. 1972. Depth first search and linear graph algorithms. SIAM Journal on Computing 1, 2, 146-160.
• 43: Tiuryn, J. 1992. Subtype inequalities. In Proc. 7th Annual IEEE Symp. on Logic in Computer Science (LICS), Santa Cruz, California. IEEE Computer Society Press, 308-315.
• 44: Wand, M. 1987. A simple algorithm and proof for type inference. Fundamenta Informaticae X, 115-12.
• 45: 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
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
Java compiler, lattice completion, object-oriented type systems, type inference, type reconstruction, type-directed compilation, typed intermediate language