Robert O'Callahan
ABSTRACT
A type system with proven soundness is a prerequisite for the safe and efficient execution of Java bytecode programs. So far, efforts to construct such a type system have followed a "forward dataflow" approach, in the spirit of the original Java Virtual Machine bytecode verifier. We present an alternative type system, based on conventional ideas of type constraints, polymorphic recursion and continuations. We compare it to Stata and Abadi's JVML-0 type system for bytecode subroutines, and demonstrate that our system is simpler and able to type strictly more programs, including code that could be produced by Java compilers and cannot be typed in JVML-0. Examination of real Java programs shows that such code is rare but does occur. We explain some of the apparently arbitrary constraints imposed by previous approaches by showing that they are consequences of our simpler type rules, or actually unnecessary.
- 1.D. Dean, E. Felten and D. Wallach. Java Security: From HotJava to Netscape and beyond. 1996 IEEE Symposium on Security and Privacy, May 1996. Google Scholar
Digital Library
- 2.S. Freund and J. Mitchell. A type system for object initialization in the Java bytecode language. Proceedings of the ACM SIGPLAN '98 Conference on Object-Oriented Programming Systems, Languages and Applications, October 1998. Google ScholarDigital Library
- 3.F. Henglein. Type inference with polymorphic recursion. TOPLAS, Volume 15, No. 2, 1993. Google ScholarDigital Library
- 4.M. Hagiya and A. Towaza. On a new method for dataflow analysis of Java Virtual Machine subroutines. Proceedings of the Fifth International Static Analysis Symposium, Springer- Verlag LNCS, 1998.Google ScholarCross Ref
- 5.T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley. Google ScholarDigital Library
- 6.G. Morrisett, K. Crary, N. Glew and D. Walker. Stack-Based Typed Assembly Language. 1998 Workshop on Types in Compilation. Google ScholarDigital Library
- 7.Z. Qian. A formal specification of Java virtual machine instructions. Formal Syntax and Semantics of Java, Springer- Vedag LNCS, 1998.Google Scholar
- 8.R. Stata and M. Abadi. A type system for Java bytecode subroutines. Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles Of Programming Languages, January 1998. Google ScholarDigital Library
Index Terms
- A simple, comprehensive type system for Java bytecode subroutines
Recommendations
A type system for Java bytecode subroutines
Java is typically compiled into an intermediate language, JVML, that is interpreted by the Java Virtual Machine. Because mobile JVML code is not always trusted, a bytecode verifier enforces static constraints that prevent various dynamic errors. Given ...
Compile-time type-checking for custom type qualifiers in Java
OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companionWe have created a system that enables programmers to add custom type qualifiers to the Java language in a backward-compatible way. The system allows programmers to write type qualifiers in their programs and to create compiler plug-ins that enforce the ...
Compile-time type-checking for custom type qualifiers in Java
OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companionWe have created a system that enables programmers to add custom type qualifiers to the Java language in a backward-compatible way. The system allows programmers to write type qualifiers in their programs and to create compiler plug-ins that enforce the ...
Comments