Research on "Formal Methods in Computing"

Polymorphic Bytecode: Compositional Compilation for Java-like Languages

ABSTRACT. We define compositional compilation to be the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but depends on the compilation context. In this paper, we propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard Java) bytecode that can be obtained by replacing type variables with class names satisfying the associated constraints. We illustrate our proposal by developing a type inference and a linking algorithm for a small subset of Java. The type inference algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment with the needed constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, when a self-contained collection of fragments is taken, linking either fails, or produces standard Java bytecode (which is the same as the one which would have been produced by standard Java compilation of all fragments together).

BIBTEX.

@inproceedings{Ancona-Damiani-Drossopoulou-Zucca:POPL-2005,
author    = {D. Ancona and F. Damiani and S. Drossopoulou and E. Zucca},
title     = {Polymorphic Bytecode: 
Compositional Compilation for Java-like Languages},
booktitle = {{POPL'05}},
year      = {2005},
publisher = {ACM},
pages     = {26-37}
}