Type-Safe Method Inlining

Neal Glew^{1} and Jens Palsberg^{2}

                       1 aglew@acm.org

2 Purdue University, Dept of Computer Science, W Lafayette, IN 47907, USA,

                   palsberg@cs.purdue.edu.

Abstract. In a typed language such as Java, inlining of virtual methods does not always preserve typability. The best known solution to this problem is to insert type casts, which may hurt performance. This paper presents a solution that never hurts performance. The solution is based on a transformation that modifies static type annotations and changes some virtual calls into static calls, which can then be safely inlined. The transformation is parameterised by a flow analysis, and for any analysis that satisfies certain conditions, the transformation is correct and idempotent. The paper presents the transformation, the conditions on the flow analysis, and proves the correctness properties; all in the context of a variant of Featherweight Java.

1 Introduction

1.1 Background

A number of recent compilers use typed intermediate languages (e.g., [11, 12, 21, 6]) to obtain debugging and optimisation benefits [11, 19]. Such compilers require transformations that are typability preserving, that is, transformations that produce output that type checks. This paper is concerned with one such transformation, that of inlining of method calls in a statically-typed objectoriented language. While there has been substantial previous work on method inlining (e.g., [2, 3]), the known approaches are either for an untyped language, or have to rely on adding type casts or extra types, as we explain next.

Consider the following well-typed Java program:

class B {                        // a code snippet:
  B m() { return this; }         B x = new C();
}                                x = x.m();
                                 x = ((B)new C()).m();
class C extends B {
  C f;
  B m() {
    return this.f;
  }
}

Both of the method calls x.m() and ((B)new C()).m() have a unique target method that is a small code fragment, so it makes sense to inline these calls.

In both cases, a compiler could inline by taking the body of m and replacing this with the actual receiver expression to get:

     x = x.f;                         // does not type check
     x = ((B)new C()).f               // does not type check

These two assignments do not type check. The reason is that while this in class C has static type C, both x and (B)new C() have static type B. Hence, both x.f and ((B)new C()).f will yield the compile-time error that there is no f-field in

either x or (B)new C().

The problem can be solved by inserting type casts. In their Java compiler, Wright et al. [21] insert type casts (in the form of a typecase expression) of this in all translated method bodies. Applying this idea to our example program produces the following declaration for method m in class C:

       B m() {
         return ((C)this).f;
       }

After inlining, the two assignments type check:

     x = ((C)x).f;                        // type checks
     x = ((C)((B)new C())).f;             // type checks

A different approach was taken by Gagnon et al. [5] who first compile Java to an untyped representation of Java bytecode, and then infer types to regain static type annotations. Their results show that this works well for a substantial suite of benchmark programs. In general, however, their algorithm for type inference may fail, and in such cases they revert to inserting type casts.

A third approach, which does not require type casts at all, is to add new types to the program. Knoblock and Rehof [10] demonstrated how to do that automatically in such a way that type inference will succeed for all verifiable Java bytecode programs.

In general, inserting type casts may hurt performance, and adding new types may not be acceptable. Since these type casts and types are not added in the untyped setting, they are there just for the purposes of satisfying the type system. It is intellectually unsatisfying that we cannot just use the untyped techniques. Until now, it has remained an open problem to devise a scheme for supporting typability-preserving method inlining in a way that does not require the insertion of type casts or new types.

1.2 Our Result

We present an approach to typability-preserving method inlining that never hurts performance, and does not require the insertion of type casts or new types. Our approach is based on a transformation that modifies static type annotations and changes some virtual calls into static calls, which can then be safely inlined. The transformation is parameterised by a flow analysis, and for any analysis that satisfies certain conditions, the transformation is correct and idempotent. We present the transformation, the conditions on the flow analysis, and prove the correctness properties; all in the context of a variant of Featherweight Java. It is straightforward to extend our approach to full Java.

Note that our transformation, like most previous work, is a whole-program transformation. By making suitable conservative assumptions it could be used to transform separate program fragments. How effective this might be is beyond the scope of this paper. We also leave open the question of how suitable the transformation might be to a just-in-time compiler.

The flow analysis approximates the results of evaluating expressions. For each expression, it determines a set of classes such that every possible result of evaluating the expression is an instance of one of those classes. Given such a set the transformation can use the least upper bound as the new explicit type information. For our example program, the best flow set for both receiver expressions in the program is {C}, and the least upper bound for this set is C. Therefore, in the transformed program the code snippet is as follows—and it type checks:

     C x = new C();         // the type of x has been changed to C
     x = x.m();
     x = ((C)new C()).m();  // the type cast has been changed to C

Inlining then produces the following well-typed code snippet:

     C x = new C();
     x = x.f;                         // type checks
     x = ((C)new C()).f;              // type checks

One result of our study is the need to align the flow analysis with the type system, and this is crucial to our proofs. In particular, there were several aspects of Java’s type system that lead to unusual conditions on the flow analysis. One example is Java’s lack of a bottom type leading to a nonemptyness condition on flow sets. Another example is the mixed use of subset [1, 14] and equality constraints [4]. (An idea also studied by Fähndrich and Aiken [4].) We were lead to this mixture by well known results about aligning flow analyses with type systems [16, 7, 15, 17, 10], and in particular that subset constraints correspond to subtyping. The Java type system allows the use of subtyping in some places but not in others. Thus, our flow analyses must satisfy subset constraints in some places and equality constraints in others.

Our approach does method inlining in two steps:

1. change some dynamic method invocations to static method invocations (and change the type annotations and the classes used in type casts) and

2. inline the static method invocations.

The idea is, as in previous work, that in a dynamic method dispatch e.m(e_{1}, ..., e_{n}), if all the objects that e could evaluate to are instances of classes which inherit m from a fixed class D, then the dynamic dispatch can be transformed to a static dispatch e.D::m(e_{1}, ..., e_{n}). (The expression e.D::m(e_{1}, ..., e_{n}) invokes D’s version of m on e with e_{1} through e_{n} as arguments.) A static dispatch e.D::m(e_{1}, ..., e_{n}) can be inlined to e′{this, x_{1}, …, x_{n} := e, e_{1}, …, e_{n}} where D has for method m, body e' and parameters x_{1} through x_{n}. This is nothing other than applying a nonstandard reduction rule at compile time, and it is straightforward to show that the rule is typability preserving.

The following section presents our variant of Featherweight Java, Section 3 presents the constraints flow analyses must satisfy, and Section 4 presents the program transformation. The proofs of the correctness theorems are presented in three appendices.

2 The Language

We formalise our results in Featherweight Java [8] (FJ) extended with a static dispatch construct, a language we call FJS. The language and its presentation follow the original FJ paper as closely as possible.

As in FJ, an FJS program is a list of class definitions and an expression to be evaluated. Each class definition is in a stylised form. Every class extends another, top level classes extend Object. Every class has exactly one constructor. This constructor has one parameter for each of the fields of the class, with the same names and in the same order. It first calls the superclass constructor with the parameters that correspond to the superclass’s fields. Then it uses the remaining parameters to initialise the fields declared in the class. Constructors are the only place where super or = appear in an FJS program. The receiver of a field access or method invocation is always explicit, this is used to refer to an object’s fields and methods. FJS is functional, so a method body consists just of a return statement with an expression and there is no void type. There are just six forms of expressions: variables, field access, object constructors, dynamic casts, dynamic method invocation, and static method invocation. Although FJS does not have super, static method invocation can be used to call a superclass’s methods. The remainder of this section formalises the language.

2.1 Syntax and Semantics

The syntax of FJS is:

      P  ::=(\overline{CD},e)
      CD::=class C extends C \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\}
      K  ::=C(\overline{C} \overline{f}) \{super(\overline{f}); this.\overline{f} = \overline{f};\}
      M  ::=C m(\overline{C} \overline{x^{ℓ}}) \{return^{ℓ}e;\}
      e  ::=x^{ℓ} | e.f^{ℓ} | new^{ℓ} C(\overline{e}) | (C)^{ℓ}e | e.m(\overline{e})^{ℓ} | e.C::m(\overline{e})^{ℓ}

The metavariables A, B, C, D, and E range over class names; f and g range over field names; m ranges over method names; x ranges over variables; d and e range over expressions; M ranges over method definitions; K ranges over constructors; CD ranges over class definitions; and P ranges over programs. Object is a class name, but no program may give it a definition; this is a variable, but no program may use it as a parameter. The over bar notation denotes sequences, so \overline{f} abbreviates f_{1}, ..., f_{n}. This notation also denotes pairs of sequences in an obvious way—\overline{C} \overline{f^{ℓ}} abbreviates C_{1} f_{1}^{ℓ_{1}}, ..., C_{n} f_{n}^{ℓ_{n}}, \overline{C} \overline{f^{ℓ}}; abbreviates C_{1} f_{1}^{ℓ_{1}}; ⋯; C_{n} f_{n}^{ℓ_{n}};, and this.\overline{f}=\overline{f} abbreviates this.f_{1}=f_{1}; ⋯; this.f_{n}=f_{n}. The empty sequence is •, and comma concatenates sequences. Sequences of class definitions, field declarations, method definitions, and parameter declarations may not contain duplicate names. We abuse notation and consider a sequence of class definitions to also be a mapping from class names to class definitions, and write \overline{CD}(C) to mean the definition of C under the map corresponding to \overline{CD}. Any class name C except Object appearing in a program must be given a definition by that program, and the extends clauses of a program must be acyclic.

Class definition class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\} declares class C a subclass of D. In addition to the fields of its superclass, C has fields \overline{f^{ℓ}} of types \overline{C}. K is the constructor for the class, and has the stylised form described above. \overline{M} are the methods declared by C, they may be new methods or might override those of D. C also inherits all methods of D that it does not override. Method declaration C m(\overline{C} \overline{x^{ℓ}}) \{return^{ℓ}e;\} declares a method m with return type C, with parameters \overline{x^{ℓ}} of types \overline{C}, and that when invoked evaluates expression e and returns it as the result of the invocation.

As mentioned above, there are six forms of expression: variables x, field selection e.f^{ℓ}, object constructors new^{ℓ} C(\overline{e}), casts (C)^{ℓ}e, dynamic method invocations e.m(\overline{e})^{ℓ}, and static method invocations e.C::m(\overline{e})^{ℓ}. The latter invokes C’s version of method m on object e, which should be in C or one of its subclasses.

Metavariable ℓ ranges over a set of labels. Notice that there is a label associated with all expressions, fields, method returns, and formal arguments; these labels are assumed to be unique. For a program P, labels(P) denotes the set of labels used in P. To simplify the technical definitions later, all the field names and argument names must be distinct. Furthermore, the label on any variable occurrence must be the same as the label on its declaration, and any two occurrences of this in a class must have the same label. Any well-typed program can easily be transformed to satisfy these conditions. Function lab maps an expression, a field name, or an argument name to its label.

Some auxiliary definitions that are used in the rest of the paper appear in Figure 1. Unlike the FJ paper, we do not make the list of class declarations global, but have them appear explicitly as parameters to functions, predicates, and rules. Function fields(\overline{CD}, C) returns a list of C’s fields and their types; mtype(\overline{CD}, C, m) returns the type of method m in class C, this type has the form \overline{C} → C where C is the return type and \overline{C} are the argument types; mbody(\overline{CD}, C, m) returns the body of method m in class C, this has the form (ℓ, \overline{x}, e) where ℓ is the label of the return statement, e is the expression to evaluate, and \overline{x} are the parameter names; impl(\overline{CD}, C, m) returns the class from which class C inherits method m (this might be C itself if C declares m), this has the form D::m where D is the class.

Field Lookup:

fields(\overline{CD}, Object) = •

(1)

         \frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\}  fields(\overline{CD}, D) = \overline{D} \overline{g}}{fields(\overline{CD}, C) = \overline{D} \overline{g}, \overline{C} \overline{f}}  (2)

Method Type Lookup:

  \frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ_{1}}}; K \overline{M}\}    B_{0} m(\overline{B} \overline{x^{ℓ_{2}}}) \{return^{ℓ}e;\} ∈ \overline{M}}{mtype(\overline{CD}, C, m) = \overline{B} → B_{0}} (3)

\frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\}    m not defined in \overline{M}}{mtype(\overline{CD}, C, m) = mtype(\overline{CD}, D, m)}  (4)

Method Body Lookup:

  \frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ_{1}}}; K \overline{M}\}    B_{0} m(\overline{B} \overline{x^{ℓ_{2}}}) \{return^{ℓ}e;\} ∈ \overline{M}}{mbody(\overline{CD}, C, m) = (ℓ, \overline{x}, e)} (5)

\frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\}    m not defined in \overline{M}}{mbody(\overline{CD}, C, m) = mbody(\overline{CD}, D, m)}  (6)

Class of Method Lookup:

  \frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ_{1}}}; K \overline{M}\}    B_{0} m(\overline{B} \overline{x^{ℓ_{2}}}) \{return^{ℓ}e;\} ∈ \overline{M}}{impl(\overline{CD}, C, m) = C::m} (7)

\frac{\overline{CD}(C) = class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\}    m not defined in \overline{M}}{impl(\overline{CD}, C, m) = impl(\overline{CD}, D, m)}  (8)

Valid Method Overriding:

\frac{mtype(\overline{CD}, D, m) = \overline{D} → D_{0} implies \overline{C} = \overline{D} and C_{0} = D_{0}}{override(\overline{CD}, D, m, \overline{C} → C_{0})}  (9)

Fig. 1. Auxiliary Definitions

                    \frac{fields(\overline{CD}, C) = \overline{C} \overline{f}}{(\overline{CD},X⟨new^{ℓ_{1}} C(\overline{e}).f_{i}^{ℓ_{2}}⟩) ↦ (\overline{CD},X⟨e_{i}⟩)}  (10)

                \frac{\overline{CD} ⊢ C<:D}{(\overline{CD},X⟨(D)^{ℓ_{1}}new^{ℓ_{2}} C(\overline{e})⟩) ↦ (\overline{CD},X⟨new^{ℓ_{2}} C(\overline{e})⟩)}  (11)

       \frac{mbody(\overline{CD}, C, m) = (ℓ, \overline{x}, e_{0})}{(\overline{CD},X⟨new^{ℓ_{1}} C(\overline{e}).m(\overline{d})^{ℓ_{2}}⟩) ↦ (\overline{CD},X⟨e_{0}\{this, \overline{x} := new^{ℓ_{1}} C(\overline{e}), \overline{d}\}⟩)}  (12)

    \frac{mbody(\overline{CD}, D, m) = (ℓ, \overline{x}, e_{0})}{(\overline{CD},X⟨new^{ℓ_{1}} C(\overline{e}).D::m(\overline{d})^{ℓ_{2}}⟩) ↦ (\overline{CD},X⟨e_{0}\{this, \overline{x} := new^{ℓ_{1}} C(\overline{e}), \overline{d}\}⟩)}  (13)

Fig. 2. Operational Semantics

Predicate override(\overline{CD}, D, m, \overline{C} → C) is true when method m of type \overline{C} → C may be declared in a subclass of D. It checks that if D declares or inherits m then it has the same type, as required by Java’s type system. The more general rule with contravariant argument types and covariant result types could be used, and the results of this paper would still hold (the definition of acceptable flow would change slightly).

The operational semantics of the language appear in Figure 2. Metavariable X ranges over evaluation contexts, which are expressions with exactly one hole; X⟨e⟩ denotes the expression formed by replacing the hole in X by the expression e. Unlike the FJ paper, in addition to making the list of class declarations explicit in the rules we make the evaluation context explicit as well.

Because the language is functional and each class has exactly one constructor of a particular form, the values of the language, which are all objects, can be represented using object constructors new^{ℓ} C(\overline{e}). Field access reduces to the appropriate element of \overline{e}. The cast (C)^{ℓ_{1}}new^{ℓ_{2}} D(\overline{e}) reduces to the object new^{ℓ_{2}} D(\overline{e}) if D is a subclass of C. If D is not a subclass of C then the cast is irreducible representing that the cast fails as a checked run-time error. The reduction rule for method invocation new^{ℓ_{1}} C(\overline{e}).m(\overline{d})^{ℓ_{2}} looks up the method body of m in C, if this is (ℓ, \overline{x}, e_{0}) then the reduced expression is the body e_{0} with the actuals \overline{d} substituted for the formals \overline{x} and the object new^{ℓ_{1}} C(\overline{e}) substituted for this. Static method invocation new^{ℓ_{1}} C(\overline{e}).D::m(\overline{d})^{ℓ} reduces similarly except that the method is looked up in D not C. Note that this method lookup can be done at compile time and a static method invocation can be implemented as a direct call rather than an indirect call through a virtual-dispatch table.

An irreducible expression is stuck if it is of the form X⟨e.f^{ℓ}⟩, X⟨e.m(\overline{e})^{ℓ}⟩, or X⟨e.D::m(\overline{e})^{ℓ}⟩. The type system prevents stuck expressions from occurring during execution of a program. Irreducible expressions that are not stuck are of the form v::=new^{ℓ} C(\overline{v}) or X⟨(C)^{ℓ_{1}}new^{ℓ_{2}} D(\overline{e})⟩ where D is not a subclass of C; the former represents normal termination with a fully evaluated object, the latter represents a failed cast.

2.2 Type System

The type system consists of the following judgements:

Judgement  Meaning
\overline{CD} ⊢ C<:D    C is a subtype of D
\overline{CD}; Γ ⊢ e ∈ C  e is well formed and of type C
\overline{CD} ⊢ M OK in CM is well formed in class C
\overline{CD} ⊢ CD OK CD is well formed
⊢ P ∈ C       P is well formed and of type C

A typing context Γ has the form \overline{x}:\overline{C} where there are no duplicate variable names. The only types are the names of classes, and such a type includes all instances of that class and its subclasses. The rules appear in Figure 3. The bar notation denotes sequences of typing judgements, so \overline{CD}; Γ ⊢ \overline{e} ∈ \overline{C} abbreviates \overline{CD}; Γ ⊢ e_{1} ∈ C_{1}, …, \overline{CD}; Γ ⊢ e_{n} ∈ C_{n}.

Subtyping:

                                \overline{\overline{CD} ⊢ C<:C}  (14)
                         \frac{\overline{CD} ⊢ C<:D    \overline{CD} ⊢ D<:E}{\overline{CD} ⊢ C<:E}  (15)
                      \frac{\overline{CD}(C) = class C extends D \{...\}}{\overline{CD} ⊢ C<:D}  (16)

Expression Typing:

\overline{\overline{CD}; Γ ⊢ x^{ℓ} ∈ Γ (x)}  (17)
\frac{\overline{CD}; Γ ⊢ e_{0} ∈ C_{0}  fields(\overline{CD}, C_{0}) = \overline{C} \overline{f}}{\overline{CD}; Γ ⊢ e_{0}.f_{i}^{ℓ} ∈ C_{i}}  (18)

               \frac{fields(\overline{CD}, C) = \overline{D} \overline{f}    \overline{CD}; Γ ⊢ \overline{e} ∈ \overline{E}    \overline{CD} ⊢ \overline{E}<:\overline{D}}{\overline{CD}; Γ ⊢ new^{ℓ} C(\overline{e}) ∈ C}  (19)

\frac{\overline{CD}; Γ ⊢ e_{0} ∈ D}{\overline{CD}; Γ ⊢ (C)^{ℓ}e_{0} ∈ C}  (20)
\frac{\overline{CD}; Γ ⊢ e_{0} ∈ C_{0}  mtype(\overline{CD}, C_{0}, m) = \overline{D} → C    \overline{CD}; Γ ⊢ \overline{e} ∈ \overline{C}    \overline{CD} ⊢ \overline{C}<:\overline{D}}{\overline{CD}; Γ ⊢ e_{0}.m(\overline{e})^{ℓ} ∈ C} (21)

                          \frac{\overline{CD}; Γ ⊢ e_{0} ∈ C_{0} \overline{CD} ⊢ C_{0} <:D mtype(\overline{CD}, D, m) = \overline{E} → E_{0} \overline{CD}; Γ ⊢ \overline{e} ∈ \overline{C} \overline{CD} ⊢ \overline{C}<:\overline{E}}{\overline{CD}; Γ ⊢ e_{0}.D::m(\overline{e})^{ℓ} ∈ E_{0}}  (22)

Method Typing:

                    \frac{\overline{CD}; this : C, \overline{x} : \overline{C} ⊢ e_{0} ∈ E_{0} \overline{CD} ⊢ E_{0} <:C_{0} \overline{CD}(C) = class C extends D \{...\} override(\overline{CD}, D, m, \overline{C} → C_{0})}{\overline{CD} ⊢ C_{0} m(\overline{C} \overline{x^{ℓ}}) \{return^{ℓ}e_{0};\} OK in C}  (23)

Class Typing:

\frac{\overline{CD} ⊢ \overline{M} OK in C  fields(\overline{CD}, D) = \overline{D} \overline{g}    K = C(\overline{D} \overline{g}, \overline{C} \overline{f}) \{super(\overline{g}); this.\overline{f}=\overline{f};\}}{\overline{CD} ⊢ class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\} OK}

(24)

Program Typing:

                        \frac{\overline{CD} ⊢ \overline{CD} OK  \overline{CD}; • ⊢ e ∈ C}{⊢ (\overline{CD},e) ∈ C}  (25)

Fig. 3. Typing Rules

The rules for constructors and method invocation check that each actual has a subtype of the corresponding formal. The typing rule for dynamic method dispatch looks up the type of the method in the class of the receiver. The typing rule for static method dispatch e.D::m(\overline{e})^{ℓ} requires that e has some subtype of D and looks up the type of the method in D. As in FJ, the typing rules allow stupid casts, such as (C)^{ℓ_{1}}new^{ℓ_{2}} D(\overline{e}) where D is not a subclass of C and the cast will always fail. Allowing stupid casts is needed to prove type preservation. Unlike in FJ, FJS has only one rule for casts, which just requires the expression being cast to have some type. This rule is equivalent to FJ’s three rules except that it does not issue stupid-cast warnings. The type system is sound, that is, well-typed programs never get stuck. This fact is stated in the following theorem, which can be proved by standard methods [13, 20, 8].

Theorem 1 (Type Soundness). If ⊢ P ∈ C then P does not reduce to a program with a stuck expression.

The rules are syntax directed, with the exception of the rules for subtyping. So, disregarding the details of how subtyping judgments are derived, for any program there is exactly one derivation possible. Thus for a program P and any ℓ, which can be the label of a field, method parameter, method return, or expression appearing in P, there is a uniquely determined static type for the program point labeled ℓ, written static-type(ℓ, P).

3 Flow Analysis

A flow analysis approximates the results of evaluating expressions. In our setting, flow information for an expression is a set of classes such that the expression will evaluate to an instance of one of those classes.

For a program P, classes(P) denotes the set of class names declared in P, flow(P) is the powerset of classes(P); subclasses(P, C) is the set of subclasses of C (including C). Flow information for P is a member of flow-information(P) = labels(P) → flow(P). Metavariables S and T range over flow(P) and φ ranges over flow-information(P). We order flow-information(P) such that φ_{1} ≤ φ_{2} if and only if φ_{1}(ℓ) ⊆ φ_{2}(ℓ) for every ℓ ∈ labels(P). In flow-information(P), the least element is λℓ.∅ and the greatest element is λℓ.classes(P).

Some members of flow-information(P) are not valid approximations of the results of evaluating expressions in P, and do not support our program transformation. The flow analyses with the desired properties are the ones that are both acceptable and type respecting. (The term “type respecting” was coined by Jagannathan et al. [9].) Intuitively, an acceptable analysis contains sets that are big enough, in that it correctly approximates the results of evaluating expressions. A type-respecting analysis contains sets that are small enough, in that it is at least as precise as the static type system, that is, each flow only contains classes that are subclasses of the corresponding static type. For a program P, we define:

acceptable(P) = { φ ∈ flow-information(P) |

φ satisfies the conditions listed in Figure 4 }

type-respecting(P) = { φ ∈ flow-information(P) |

∀ℓ ∈ labels(P) : φ(ℓ) ⊆ subclasses(P, static-type(ℓ, P)) }

flow-analysis(P) = acceptable(P) ∩ type-respecting(P).

The conditions in Figure 4 for a flow analysis to be acceptable are somewhat unusual. The design of those conditions is influenced by the way the program transformation will use flow information to change type annotations: for a program point with label ℓ, the transformation uses the least upper bound of φ(ℓ), written ⊔φ(ℓ), as the new type annotation. With that in mind, here is a closer look at the rules in Figure (4).

First, notice that Rule (40) ensures that least upper bounds are of a nonempty set. Rules (26)–(37) are related to one way of specifying 0-CFA [18, 14, 15]. The unusual aspect of them is that they are a mixture of subset constraints [14] and equality constraints [15]. If the sole purpose were to approximate the results of evaluating expressions, then all of the equality constraints can be relaxed to be subset constraints. The reason for using equality constraints in some cases is to align the flow analysis with the type system. The type system does not have a general subsumption rule that allows subtyping to be used everywhere. Rather, in the type rules in Figure 3, subtyping is used in four places: Rule (19) for new-expressions, Rule (21) for calls, Rule (22) for static calls, and Rule (23) for method typing. In each case, there is a subset constraint in the corresponding rule for acceptable flow analyses in Figure 4: Rule (27) for new-expressions, Rule (30) for dynamic method invocations, Rule (33) for static method invocations, and Rule (37) for method typing. In contrast, Rule (18) for field selection requires the type of the field to equal the type of the field-selection expression; this is matched by the equality constraint in Rule (26). A similar comment applies to Rules (31) and (34). Rules (29), (32), and (35) have no counterparts in the type system and are needed to ensure that the flow analysis approximates the results of evaluating expressions. Rule (36) is rather conservative: it says that the this object always can be an object of the class in which this occurs. The rule is needed because of Rule (23) for method typing, which asserts that this has type C. Finally, Rules (38) and (39) ensure that the signature of a method and the signature of an overriding method are the same.

A variant of Class Hierarchy Analysis [2] (CHA) can be defined as follows:

CHA(P) = λℓ.subclasses(P, static-type(ℓ, P)).

It is straightforward to show that CHA(P) is the coarsest flow analysis of P, as stated in the following theorem.

Theorem 2. (CHA) CHA(P) is the greatest element of flow-analysis(P).

Note that flow-analysis(P) does not have a least element. This is due to Rule (40) that requires all flows to be nonempty. If Java had a bottom type, then this type could be used as the least upper bound of the empty set and Rule (40) would not be needed. Then flow-analysis(P) would be a meet semilattice with both a

– for each e.f^{ℓ} in P:

φ(lab(f)) = φ(ℓ)  (26)

– for each new^{ℓ} D(\overline{e}) in P, where fields(\overline{CD}, D) = \overline{E} \overline{f}:

φ(lab(\overline{e})) ⊆ φ(lab(\overline{f}))  (27)
D ∈ φ(ℓ)  (28)

– for each (D)^{ℓ}e in P:

φ(lab(e)) ∩ subclasses(P, D) = φ(ℓ)  (29)

– for each e.m(\overline{e})^{ℓ} in P and each class D in P, where mbody(\overline{CD}, D, m) = (ℓ′, \overline{x}, e′), impl(\overline{CD}, D, m) = E::m, and ℓ′′ is the label for E’s this occurrences:

D ∈ φ(lab(e)) ⇒ φ(lab(\overline{e})) ⊆ φ(lab(\overline{x}))  (30)
D ∈ φ(lab(e)) ⇒ φ(ℓ′) = φ(ℓ)  (31)
φ(lab(e)) ⊆ φ(ℓ′′)  (32)

– for each e.D::m(\overline{e})^{ℓ} in P, where mbody(\overline{CD}, D, m) = (ℓ′, \overline{x}, e′), impl(\overline{CD}, D, m) = E::m, and ℓ′′ is the label for E’s this occurrences

φ(lab(\overline{e})) ⊆ φ(lab(\overline{x}))  (33)
φ(ℓ′) = φ(ℓ)  (34)
φ(lab(e)) ⊆ φ(ℓ′′)  (35)

– for each class C in P, where ℓ is the label for C’s this occurrences:

C ∈ φ(ℓ)  (36)

– for each method in P, with body {return^{ℓ}e_{0};}

φ(lab(e_{0})) ⊆ φ(ℓ)  (37)

– for each method name m declared or inherited in class C of P, if

                        \overline{CD}(C) = class C extends D \{\overline{C} \overline{f}; K \overline{M}\}

mbody(\overline{CD}, C, m) = (ℓ_{1}, \overline{x}_{1}, e_{1})
mbody(\overline{CD}, D, m) = (ℓ_{2}, \overline{x}_{2}, e_{2})

then

φ(lab(\overline{x}_{1})) = φ(lab(\overline{x}_{2}))  (38)
φ(ℓ_{1}) = φ(ℓ_{2})  (39)

– for each ℓ ∈ labels(P):

φ(ℓ) ≠ ∅  (40)

Fig. 4. Requirements for an acceptable flow analyses φ of a program P = (\overline{CD},e).

greatest and least element. However, Java does not have a bottom type, so we have kept this constraint.

The property of being a flow analysis is preserved during computation, as stated in the following theorem, which is proved in Appendix A. (Palsberg [14] proved a similar result for the λ-calculus.)

Theorem 3 (Flow Preservation). If φ ∈ flow-analysis(P_{1}) and P_{1} ↦ P_{2}, then φ ∈ flow-analysis(P_{2}).

It is straightforward to compute CHA(P). However, since CHA(P) is the greatest element of flow-analysis(P), it is the most conservative choice of flow analysis and will lead to the least number of inlinings. This raises the question of whether other polynomial-time algorithms could do better. The main difficulty is that flow-analysis(P) does not have a least element so there is not a unique best choice of flow analysis that improves on CHA(P).

To illustrate that indeed there is a better polynomial time algorithm, we now define a flow analysis with mixed constraints and nonempty sets; the analysis is called MN(P) (for Mixed and Nonempty). First, the notion of lifting a flow analysis is:

lift(φ) : flow-information(P) → flow-information(P)
lift(φ) = λℓ. \{ \begin{matrix}φ(ℓ) & if ⊔ φ(ℓ) exists \\ \{ static-type(ℓ, P) \} & otherwise \end{matrix}

Notice that lift(φ)(ℓ) ≠ ∅ for all ℓ ∈ labels(P). For Featherweight Java and FJS, ⊔φ(ℓ) exists for all nonempty sets φ(ℓ). The full Java type system enables multiple subtyping among interfaces which can lead to nonempty flows without a least upper bound.

Second, the definition of MN(P) is:

φ_{0} = the least flow analysis satisfying Rules (26)–(39)
MN(P) = the least flow analysis greater than lift(φ_{0}) satisfying Rules (26)–(39)

This algorithm is polynomial time: φ_{0} takes polynomial time to compute using the technique of Fähndrich and Aiken [4], which intuitively is a fixed-point computation with λℓ.∅ as the starting point. Lifting clearly takes polynomial time, and MN(P) takes polynomial time to compute by using the Fähndrich-Aiken algorithm again, but this time with lift(φ_{0}) as the starting point for the fixed-point computation. This two-step procedure makes ⊔MN(P)(ℓ) equal to static-type(ℓ, P) for any ℓ ∈ labels(P) such that φ_{0}(ℓ) = ∅. Thus the program transformation based on MN(P) will not change the type annotation for the program points labeled by such ℓ.

There might be worthwhile elements of flow-analysis(P) other than CHA(P) and MN(P). Any element of flow-analysis(P) can be used as an argument to the program transformation, which we present next.

4 Program Transformation

The program transformation is parameterized by a flow analysis, and it operates on program fragments and type environments in a compositional fashion. It transforms each program fragment into a similar program fragment with the same label, and it transforms each type environment into a type environment which defines the same variables. The changes made by the transformation are that:

– it changes some dynamic method invocations to static method invocations,

– it changes the type annotations, and

– it changes the classes used in type casts.

In each case, the change is made on the basis of the supplied flow analysis. Specifically, (1) a dynamic call is changed to a static call when the flow analysis determines that there is a unique target method and (2) a type annotation and the class in a type cast are changed to the least upper bound of the classes in the corresponding flow. Taking the least upper bound of the classes in a flow is justified because the transformation is restricted to flow analyses that are acceptable and type respecting, so: (i) all flows are nonempty, (ii) nonempty sets of classes admit least upper bounds because FJS is a single-inheritance language, and (iii) the property of being type respecting implies that the new types (that is, the least upper bounds) can only more refined than the old ones.

The transformation consists of the following cases:

Transformation Meaning
[[P]]_{φ}  the transformation of P using φ
[[CD]]\overline{CD} ; φ  the transformation of CD using φ and \overline{CD}
[[K]]_{φ}  the transformation of K using φ
[[M]]\overline{CD} ; φ  the transformation of M using φ and \overline{CD}
[[e]]\overline{CD} ; φ  the transformation of e using φ and \overline{CD}
[[Γ]]_{φ}  the transformation of Γ using φ

The definition of the transformation appears in Figure 5.

We now present four correctness theorems: the transformation preserves typability, the transformation is operationally correct, a flow analysis of the original program is also a flow analysis of the transformed program, and the transformation is idempotent. First our main result, which is proved in Appendix B.

Theorem 4 (Typability Preservation). Suppose φ ∈ flow-analysis(P) and P = (\overline{CD},e). If ⊢ P ∈ C then ⊢ [[P]]_{φ} ∈ ⊔φ(lab(e)).

The transformation is also operationally correct, in that the transformed program simulates the original program step for step and vice versa, as stated in the following theorem, which is proved in Appendix C. Operational correctness for a multistep computation follows from Theorems 3 and 5.

   [[(\overline{CD},e)]]_{φ}  = ([[\overline{CD}]]\overline{CD} ; φ,[[e]]\overline{CD} ; φ)
   [[class C extends D \{\overline{C} \overline{f^{ℓ}}; K \overline{M}\}]]\overline{CD} ; φ = class C extends D \{

⊔φ(\overline{ℓ}) \overline{f^{ℓ}}; [[K]]_{φ} [[\overline{M}]]\overline{CD} ; φ\}

   [[C(\overline{D} \overline{f}) \{super(\overline{f1}); this.\overline{f2}=\overline{f2}\}]]_{φ} = C(⊔φ(lab(\overline{f})) \overline{f})

                                       \{super(\overline{f1}); this.\overline{f2}=\overline{f2}\}

   [[D m(\overline{E} \overline{x^{ℓ}}) \{return^{ℓ}e;\}]]\overline{CD} ; φ  = ⊔φ(ℓ) m(⊔φ(\overline{ℓ}) \overline{x^{ℓ}})\{return^{ℓ}[[e]]\overline{CD} ; φ;\}

[[x^{ℓ}]]\overline{CD} ; φ  = x^{ℓ}
[[e.f^{ℓ}]]\overline{CD} ; φ  = [[e]]\overline{CD} ; φ.f^{ℓ}

   [[new^{ℓ} D(\overline{e})]]\overline{CD} ; φ  = new^{ℓ} D([[\overline{e}]]\overline{CD} ; φ)

[[(D)^{ℓ}e]]\overline{CD} ; φ  = (⊔φ(ℓ))^{ℓ}[[e]]\overline{CD} ; φ

   [[e.m(\overline{e})^{ℓ}]]\overline{CD} ; φ  = [[e]]\overline{CD} ; φ.D::m([[\overline{e}]]\overline{CD} ; φ)^{ℓ}

where ∀E ∈ φ(lab(e)) : impl(\overline{CD}, E, m) = D::m

   [[e.m(\overline{e})^{ℓ}]]\overline{CD} ; φ  = [[e]]\overline{CD} ; φ.m([[\overline{e}]]\overline{CD} ; φ)^{ℓ}

otherwise

   [[e.D::m(\overline{e})^{ℓ}]]\overline{CD} ; φ  = [[e]]\overline{CD} ; φ.D::m([[\overline{e}]]\overline{CD} ; φ)^{ℓ}

[[x_{1} : C_{1}, …, x_{n} : C_{n}]]_{φ}  = x_{1} : ⊔φ(lab(x_{1})), …, x_{n} : ⊔φ(lab(x_{n}))

Fig. 5. The Transformation of Dynamic to Static Dispatch

Theorem 5 (Operational Correctness). If φ ∈ flow-analysis(P_{1}) then: P_{1} ↦ P_{2} if and only if [[P_{1}]]_{φ} ↦ [[P_{2}]]_{φ}.

It is straightforward to prove that a flow analysis of a program is also a flow analysis of the transformed program, as stated in the following theorem.

Theorem 6 (Analysis Preservation). If φ ∈ flow-analysis(P), then φ ∈ flow-analysis([[P]]_{φ}).

Given a flow analysis, it is sufficient to apply the transformation only once; applying it again will not lead to any further change. We can state this as the following idempotence property of the transformation, which is straightforward to prove.

Theorem 7 (Idempotence). If φ ∈ flow-information(P) then [[[[P]]_{φ}]]_{φ} = [[P]]_{φ}.

5 Conclusion

Type-safe method inlining can be done for a single-inheritance language without resorting to the insertion of type casts or new types. Our approach is based on flow analysis, and our experience is that it is tricky to get the requirements for the flow analysis right. During the process of proving correctness, we discovered the need for flow constraints that would not usually be used in a flow analysis, e.g., Rule (36). The requirement that all flow sets must be nonempty is unusual, and it entails that there is no unique best analysis that satisfies the requirements. While Class Hierarchy Analysis and our own MN analysis satisfy requirements, more work in needed to investigate alternatives. Future work includes implementing and experimenting with our approach in the context of Java.

Acknowledgements. We thank the 84 students who took Palsberg’s graduate course on programming languages in 1999-2001 and tried, as a homework, to find and implement a solution to the problem of type-safe method inlining for a subset of Java. Only 10 of the implementations seemed not to have errors, leading to the realization that the problem is considerably harder than flow-directed inlining for an untyped language. We thank Mayur Naik and the anonymous referees for helpful comments on a draft of the paper.

Palsberg is supported by a National Science Foundation Faculty Early Career Development Award, CCR–9734265.

A Proof of Theorem 3

First, observe that labels(P_{2}) ⊆ labels(P_{1}) so φ (restricted to labels(P_{2})) is a flow analysis of P_{2}. Let P_{i} = (\overline{CD},X⟨e_{i}⟩) where e_{1} and e_{2} are as in the rules of Figure 2. Since P_{1} and P_{2} differ only in e_{1} and e_{2}, φ satisfies the conditions for acceptability and type respecting for P_{2} except for the conditions on e_{2} and its subexpressions that are not subexpressions of e_{1}, and on the expression that e_{1} appears immediately within. The last condition will hold if φ(lab(e_{2})) ⊆ φ(lab(e_{1})). Thus, we need just to show the latter and that φ satisfies the conditions for e_{2} and its subexpressions that are not subexpressions of e_{1}. Consider the various cases for the reduction rule.

field selection: In this case e_{1} = new^{ℓ_{1}} C(\overline{e}).f_{i}^{ℓ_{2}}, e_{2} = e_{i}, and fields(\overline{CD}, C) = \overline{C} \overline{f}. Thus, e_{2} is a subexpression of e_{1}. By the conditions for acceptability, φ(lab(e_{i})) ⊆ φ(lab(f_{i})) and φ(lab(f_{i})) = (ℓ_{2}). By transitivity, φ(e_{2}) =

φ(lab(e_{i})) ⊆ φ(ℓ_{2}) = φ(lab(e_{1})).

cast: In this case e_{1} = (C)^{ℓ_{1}} new^{ℓ_{2}} D(\overline{e}), e_{2} = new^{ℓ_{1}} D(\overline{e}), and \overline{CD} ⊢ D <: C. The only subexpressions of e_{2} that are not subexpressions of e_{1} is e_{2} itself. For acceptability, it must be that D ∈ φ(ℓ_{1}) and φ(lab(\overline{e})) ⊆ φ(\overline{f}) where fields(\overline{CD}, D) = \overline{C} \overline{f}. The latter follows by the acceptability conditions for e_{1}. The same conditions also give that D ∈ φ(ℓ_{2}) and φ(ℓ_{2}) ∩ subclasses(P_{1}, C) = φ(ℓ_{1}). Since D is a subclass of C, D ∈ φ(ℓ_{1}) as required. For type respecting, it must be that \overline{CD} ⊢ E <: D for each E ∈ φ(ℓ_{1}) (∗). By type respecting for lab(e_{1}), \overline{CD} ⊢ E <: D for each E ∈ φ(ℓ_{2}). Since φ(ℓ_{1}) = φ(ℓ_{2}) ∩ subclasses(P_{1}, C), (∗) holds. Finally, φ(lab(e_{2})) = φ(ℓ_{1}) = φ(lab(e_{2})).

dynamic method invocation: In this case e_{1} = new^{ℓ_{1}} C(\overline{e}).m(\overline{d})^{ℓ_{2}} and e_{2} = e\{this, \overline{x} := new^{ℓ_{1}} C(\overline{e}), \overline{d}\} where mbody(\overline{CD}, C, m) = (ℓ′, \overline{x}, e). By the conditions for acceptability φ(lab(\overline{d})) ⊆ φ(lab(\overline{x})) and φ(ℓ_{1}) ⊆ φ(lab(this)). By Lemma 1, φ satisfies the conditions for acceptability and type respecting for e_{2} and all its subexpressions. Also by the conditions for acceptability φ(ℓ′) = φ(ℓ_{2}) and φ(lab(e)) ⊆ φ(ℓ′). Thus φ(lab(e_{2})) = φ(lab(e)) ⊆ φ(ℓ_{2}) =

φ(lab(e_{1})).

static method invocation: In this case e_{1} = new^{ℓ_{1}} C(\overline{e}).D::m(\overline{d})^{ℓ_{2}} and e_{2} = e\{this, \overline{x} := new^{ℓ_{1}} C(\overline{e}), \overline{d}\} where mbody(\overline{CD}, D, m) = (ℓ′, \overline{x}, e). By the conditions for acceptability φ(lab(\overline{d})) ⊆ φ(lab(\overline{x})) and φ(ℓ_{1}) ⊆ φ(lab(this)). By Lemma 1, φ satisfies the conditions for acceptability and type respecting for e_{2} and all its subexpressions. Also by the conditions for acceptability φ(ℓ′) = φ(ℓ_{2}) and φ(lab(e)) ⊆ φ(ℓ′). Thus φ(lab(e_{2})) = φ(lab(e)) ⊆ φ(ℓ_{2}) = φ(lab(e_{1})).

Lemma 1. If φ satisfies the conditions for acceptability and type respecting for all labels in e and \overline{d} and if φ(lab(\overline{d})) ⊆ φ(lab(\overline{x})) then φ satisfies the conditions for acceptability and type respecting for all labels in e\{\overline{x} := \overline{d}\}.

Proof. Straightforward.

B Proof of Theorem 4

Theorem 4 follows immediately from Rule (25), and from Lemma 2 and Lemma 4, as stated and proved below.

Lemma 2. Suppose φ ∈ acceptable(P) ∩ type-respecting(P), and P = (\overline{CD},e_{0}). If \overline{CD} ⊢ \overline{CD} OK, then [[\overline{CD}]]\overline{CD} ; φ ⊢ [[\overline{CD}]]\overline{CD} ; φ OK.

Proof. Immediate from Lemma 3 and Lemma 7, using Rule (24).

Lemma 3. Suppose φ ∈ acceptable(P) ∩ type-respecting(P), and P = (\overline{CD},e_{0}). If \overline{CD} ⊢ \overline{M} OK in C, then [[\overline{CD}]]\overline{CD} ; φ ⊢ [[\overline{M}]]\overline{CD} ; φ OK in C.

Proof. Straightforward from Lemmas 4, 5, 8, 9, using Rules (17), (23), (36), (37).

Lemma 4. Suppose φ ∈ acceptable(P) ∩ type-respecting(P), and P = (\overline{CD},e_{0}). If \overline{CD}; Γ ⊢ e ∈ D, then [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e]]\overline{CD} ; φ ∈ ⊔φ(lab(e)).

Proof. We proceed by induction on the structure of the derivation of \overline{CD}; Γ ⊢ e ∈ D. There are six cases, depending on which one of Rules (17)–(22) was the last one to be used to derive \overline{CD}; Γ ⊢ e ∈ D.

– (17) e ≡ x^{ℓ}. We have [[x^{ℓ}]]\overline{CD} ; φ = x^{ℓ} and [[Γ]]_{φ}(x) = ⊔φ(ℓ), so we can derive,

using Rule (17), [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e]]\overline{CD} ; φ ∈ ⊔φ(ℓ), as desired.

– (18) e ≡ e_{0}.f_{i}^{ℓ}. We have \overline{CD}; Γ ⊢ e_{0} ∈ C_{0} and fields(\overline{CD}, C_{0}) = \overline{C} \overline{f}, where f_{i} occurs in \overline{f}. From the induction hypothesis we have [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e_{0}]]\overline{CD} ; φ ∈ ⊔φ(lab(e_{0})). From φ ∈ type-respecting(P) we have \overline{CD} ⊢ ⊔φ(lab(e_{0})) <: C_{0} so fields(\overline{CD}, ⊔φ(lab(e_{0}))) = \overline{D} \overline{g} \overline{C} \overline{f}. Hence, from Lemma 7, we have fields([[\overline{CD}]]\overline{CD} ; φ, ⊔φ(lab(e_{0}))) = ⊔φ(lab(\overline{g})) \overline{g} ⊔φ(lab(\overline{f})) \overline{f}. From Rule (26) we have φ(lab(f_{i})) = φ(ℓ), so ⊔φ(lab(f_{i})) = ⊔φ(ℓ), so we can derive, using Rule (18), that [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e]]\overline{CD} ; φ ∈ ⊔φ(ℓ), as desired.

– (19) e ≡ new^{ℓ} C(\overline{e}). We have fields(\overline{CD}, C) = \overline{D} \overline{f}, and \overline{CD}; Γ ⊢ \overline{e} ∈ \overline{E}, and \overline{CD} ⊢ \overline{E} <: \overline{D}. From Lemma 7 we have fields([[\overline{CD}]]\overline{CD} ; φ, C) = ⊔φ(lab(\overline{f})) \overline{f}. From the induction hypothesis we have [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[\overline{e}]]\overline{CD} ; φ ∈ ⊔φ(lab(\overline{e})). From Rule (27), we have φ(lab(\overline{e})) ⊆ φ(lab(\overline{f})), so from Lemma 9 we have \overline{CD} ⊢ ⊔φ(lab(\overline{e})) <: ⊔φ(lab(\overline{f})), and so from Lemma 8 we have [[\overline{CD}]]\overline{CD} ; φ ⊢ ⊔φ(lab(\overline{e})) <: ⊔φ(lab(\overline{f})). Finally we have from Rule (28) that C ∈ φ(ℓ), and since new^{ℓ} C(\overline{e}) has static type C and φ ∈ type-respecting(P), we have ⊔φ(ℓ) = C. We conclude, using Rule (19), that we have [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢

new^{ℓ} C([[\overline{e}]]\overline{CD} ; φ) ∈ C.

– (20) e ≡ (C)^{ℓ}e_{0}. We have \overline{CD}; Γ ⊢ e_{0} ∈ D. From the induction hypothesis we have [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e_{0}]]\overline{CD} ; φ ∈ ⊔φ(lab(e_{0})). From Rule (20) we have that we can derive [[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ (⊔φ(ℓ))^{ℓ}[[e_{0}]]\overline{CD} ; φ ∈ ⊔φ(ℓ).

– (21) e ≡ e_{0}.m(\overline{e})^{ℓ}. There are two cases. First, assume that there is a class D in P such that ∀E ∈ φ(lab(e_{0})) : impl(\overline{CD}, E, m) = D::m. We have

\overline{CD}; Γ ⊢ e_{0} ∈ C_{0}  (41)
mtype(\overline{CD}, C_{0}, m) = \overline{D} → C  (42)
\overline{CD}; Γ ⊢ \overline{e} ∈ \overline{C}  (43)

From (41), (43), and the induction hypothesis, we have

[[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e_{0}]]\overline{CD} ; φ ∈ ⊔φ(lab(e_{0}))  (44)
[[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[\overline{e}]]\overline{CD} ; φ ∈ ⊔φ(lab(\overline{e}))  (45)

We have \overline{CD} ⊢ ⊔φ(lab(e_{0})) <:D, so from Lemma 8, we have

[[\overline{CD}]]\overline{CD} ; φ ⊢ ⊔φ(lab(e_{0})) <:D,  (46)

and together with (42), we have mtype(\overline{CD}, D, m) = \overline{D} → C. Suppose also mbody(\overline{CD}, D, m) = (ℓ′, \overline{x}, e′), From Lemma 6 we have

mtype([[\overline{CD}]]\overline{CD} ; φ, D, m) = (⊔φ(lab(\overline{x}))) → (⊔φ(ℓ′)).  (47)

From Rule (40) we have φ(lab(e_{0})) ≠ ∅, so suppose E_{0} ∈ φ(lab(e_{0})). Suppose also mbody(\overline{CD}, E_{0}, m) = (ℓ′′, \overline{x′′}, e′′), From Rules (30)–(31) we have

φ(lab(\overline{e})) ⊆ φ(lab(\overline{x′′}))
φ(ℓ′′) = φ(ℓ).

Finally, from Rules (38)–(39) we have

φ(lab(\overline{x})) ⊆ φ(lab(\overline{x′′}))
φ(ℓ′) = φ(ℓ′′),

so

φ(lab(\overline{e})) ⊆ φ(lab(\overline{x}))  (48)
φ(ℓ′) = φ(ℓ).  (49)

Thus, from Rule (22), and from (44)–(49), we have that we can derive

[[\overline{CD}]]\overline{CD} ; φ; [[Γ]]_{φ} ⊢ [[e_{0}]]\overline{CD} ; φ.D::m([[\overline{e}]]\overline{CD} ; φ)^{ℓ} ∈ ⊔φ(ℓ)

as desired.

Second, suppose we have the “otherwise” case from the definition of the transformation of a method call. The proof of this case is similar to the first case, we omit the details.

– (22) e ≡ e_{0}.D::m(\overline{e})^{ℓ}. The proof of this case is similar to the previous case, we omit the details.

Lemma 5. Suppose φ ∈ acceptable(P) ∩ type-respecting(P), and P = (\overline{CD},e_{0}). If override(\overline{CD}, D, m, \overline{C} → C_{0}), \overline{CD} ⊢ C<:D, and mbody(\overline{CD}, C, m) = (ℓ, \overline{x}, e), then

override([[\overline{CD}]]\overline{CD} ; φ, D, m, (⊔φ(lab(\overline{x}))) → (⊔φ(ℓ))).

Proof. Immediate from Lemma 6, using Rule (9), (14)–(16).

Lemma 6. Suppose φ ∈ acceptable(P) ∩ type-respecting(P), and P = (\overline{CD},e_{0}). If mtype(\overline{CD}, D, m) = \overline{D} → D_{0}, \overline{CD} ⊢ C<:D, and mbody(\overline{CD}, C, m) = (ℓ, \overline{x}, e), then

mtype([[\overline{CD}]]\overline{CD} ; φ, D, m) = (⊔φ(lab(\overline{x}))) → (⊔φ(ℓ)).

Proof. Straightforward, using the rules Rules (3)–(6), (14)–(16), (38)–(39).

Lemma 7. Suppose φ ∈ acceptable(P) ∩ type-respecting(P), and P = (\overline{CD},e_{0}). If fields(\overline{CD}, D) = \overline{D} \overline{g}, then fields([[\overline{CD}]]\overline{CD} ; φ, D) = ⊔φ(lab(\overline{g})) \overline{g}.

Proof. Straightforward, by induction on the structure of the derivation of the judgment fields(\overline{CD}, D) = \overline{D} \overline{g}, using Rules (1)–(2).

Lemma 8. If \overline{CD} ⊢ C<:D, then [[\overline{CD}]]\overline{CD} ; φ ⊢ C<:D.

Proof. Immediate from the definition of subtyping, that is, Rules (14)–(16).

Lemma 9. Suppose S, T ∈ flow(P) \ ∅. If S ⊆ T, then \overline{CD} ⊢ ⊔S <: ⊔T.

Proof. Immediate from the observation that the subtyping order forms a tree and therefore admits least upper bounds of nonempty sets.

C Proof of Theorem 5

(⇒) Let P_{1} =(\overline{CD},X⟨e_{1}⟩) and P_{2} =(\overline{CD},X⟨e_{2}⟩) where e_{1} and e_{2} are given by one of the rules in Figure 2. Clearly [[P_{i}]]_{φ} = ([[\overline{CD}]]\overline{CD} ; φ,[[X]]\overline{CD} ; φ⟨[[e_{i}]]\overline{CD} ; φ⟩), so it re-

mains to show that [[e_{1}]]\overline{CD} ; φ ↦ [[e_{2}]]\overline{CD} ; φ. The interesting cases are when e_{1} is a cast and when e_{1} is a dynamic method invocation that is transformed to a static method invocation. Case 1, e_{1} =(C)^{ℓ_{1}}new^{ℓ_{2}} D(\overline{e}): In this case e_{2} =new^{ℓ_{1}} D(\overline{e}), [[e_{1}]]\overline{CD} ; φ = (⊔φ(ℓ_{1}))^{ℓ_{1}}new^{ℓ_{2}} D([[\overline{e}]]\overline{CD} ; φ), and \overline{CD} ⊢ D <: C. By the acceptability of φ, D ∈ φ(ℓ_{2}) and φ(ℓ_{2}) ∩ subclasses(P_{1}, C) ⊆ φ(ℓ_{1}). Thus D ∈ φ(ℓ_{1}), so \overline{CD} ⊢ D<: ⊔φ(ℓ_{1}). By the reduction rules [[e_{1}]]\overline{CD} ; φ ↦ new^{ℓ_{1}} D([[\overline{e}]]\overline{CD} ; φ) = [[e_{2}]]\overline{CD} ; φ. Case

2, e_{1}=new^{ℓ_{1}} C(\overline{e}).m(\overline{d})^{ℓ_{2}} and [[e_{1}]]\overline{CD} ; φ = new^{ℓ_{1}} C([[\overline{e}]]\overline{CD} ; φ).D::m([[\overline{d}]]\overline{CD} ; φ)^{ℓ_{2}}: In this case, ∀E ∈ φ(ℓ_{1}) : impl(\overline{CD}, E, m) = D::m and e_{2} = e\{this, \overline{x} := new^{ℓ_{1}} C(\overline{e}), \overline{d}\} where mbody(\overline{CD}, C, m) = (ℓ, \overline{x}, e). By the acceptability of φ, C ∈ φ(ℓ_{1}). So impl(\overline{CD}, C, m) = D::m. By inspecting the definitions, mbody(\overline{CD}, D, m) = (ℓ, \overline{x}, e). Thus:

             [[e_{1}]]\overline{CD} ; φ = new^{ℓ_{1}} C([[\overline{e}]]\overline{CD} ; φ).D::m([[\overline{d}]]\overline{CD} ; φ)^{ℓ_{2}}

↦ [[e]]\overline{CD} ; φ\{this, \overline{x} := new^{ℓ_{1}} C([[\overline{e}]]\overline{CD} ; φ), [[\overline{d}]]\overline{CD} ; φ\}
= [[e_{2}]]\overline{CD} ; φ

(⇐) If [[P_{1}]]_{φ} takes any step then it is easy to see that P_{1} has the form

(\overline{CD},X⟨e_{1}⟩) and that [[P_{1}]]_{φ} ↦ ([[\overline{CD}]]\overline{CD} ; φ,[[X]]\overline{CD} ; φ⟨e′⟩) for [[e_{1}]]\overline{CD} ; φ and e' as in the rules

in Figure 2. It remains to show that e_{1} ↦ e_{2} and [[e_{2}]]\overline{CD} ; φ = e′. The interesting cases are when e_{1} is a cast and when e_{1} is a dynamic method invocation that is transformed to a static method invocation. Case 1, e_{1} =(C)^{ℓ_{1}}new^{ℓ_{2}} D(\overline{e}): In this case [[e_{1}]]\overline{CD} ; φ = (⊔φ(ℓ_{1}))^{ℓ_{1}}new^{ℓ_{2}} D([[\overline{e}]]\overline{CD} ; φ), e′ = new^{ℓ_{1}} D([[\overline{e}]]\overline{CD} ; φ), and \overline{CD} ⊢ D <: ⊔φ(ℓ_{1}). Since φ is type respecting \overline{CD} ⊢ ⊔φ(ℓ_{1}) <: C. By transitivity of subtyping, \overline{CD} ⊢ D <: C. Letting e_{2} be new^{ℓ_{1}} D(\overline{e}) then e_{1} ↦ e_{2} and [[e_{2}]]\overline{CD} ; φ =

e′. Case 2, e_{1}=new^{ℓ_{1}} C(\overline{e}).m(\overline{d})^{ℓ_{2}} and [[e_{1}]]\overline{CD} ; φ = new^{ℓ_{1}} C([[\overline{e}]]\overline{CD} ; φ).D::m([[\overline{d}]]\overline{CD} ; φ)^{ℓ_{2}}:

In this case, ∀E ∈ φ(ℓ_{1}) : impl(\overline{CD}, E, m) = D::m and e′ = [[e]]\overline{CD} ; φ\{this, \overline{x} :=

new^{ℓ_{1}} C([[\overline{e}]]\overline{CD} ; φ), [[\overline{d}]]\overline{CD} ; φ\} where mbody(\overline{CD}, D, m) = (ℓ, \overline{x}, e). By the acceptability of φ, C ∈ φ(ℓ_{1}). So impl(\overline{CD}, C, m) = D::m. By examination of the auxiliary definitions, mbody(\overline{CD}, C, m) = (ℓ, \overline{x}, e). Letting e_{2} be e\{this, \overline{x} := new^{ℓ_{1}} C(\overline{e}), \overline{d}\} then e_{1} ↦ e_{2} and [[e_{2}]]\overline{CD} ; φ = e′.

References

1. Lars Ole Andersen. Self-applicable C program specialization. In Proceedings of PEPM’92, Workshop on Partial Evaluation and Semantics-Based Program Manipulation, pages 54–61, June 1992. (Technical Report YALEU/DCS/RR-909, Yale University).

2. Jeffrey Dean, David Grove, and Craig Chambers. Optimization of object-oriented programs using static class hierarchy analysis. In Proceedings of European Conference on Object-Oriented Programming, pages 77–101, Aarhus, Denmark, August 1995. Springer-Verlag (LNCS 952).

3. David Detlefs and Ole Agesen. Inlining of virtual methods. In Proceedings of ECOOP’99, pages 258–278. Springer-Verlag (LNCS 1628), 1999.

4. Manuel Fähndrich and Alexander Aiken. Program analysis using mixed term and set constraints. In Proceedings of SAS’97, International Static Analysis Symposium, pages 114–126. Springer-Verlag (LNCS), 1997.

5. Etienne M. Gagnon, Laurie J. Hendren, and Guillaume Marceau. Efficient inference of static types for Java bytecode. In Proceedings of SAS’00, International Static Analysis Symposium, pages 199–219. Springer-Verlag (LNCS 1824), 2000.

6. Neal Glew. An efficient class and object encoding. In Proceedings of OOPSLA’00, ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, pages 311–324, Minneapolis, Minnesota, October 2000.

7. Nevin Heintze. Control-flow analysis and type systems. In Proceedings of SAS’95, International Static Analysis Symposium, pages 189–206. Springer-Verlag (LNCS 983), Glasgow, Scotland, September 1995.

8. Atsushi Igarashi, Benjamion Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 132–146, Denver, CO, USA, October 1999.

9. Suresh Jagannathan, Andrew Wright, and Stephen Weeks. Type-directed flow analysis for typed intermediate languages. In Proceedings of SAS’97, International Static Analysis Symposium. Springer-Verlag (LNCS), 1997.

10. Todd Knoblock and Jakob Rehof. Type elaboration and subtype completion for Java Bytecode. ACM Transactions on Programming Languages and Systems, 23(2):243–272, March 2001.

11. Greg Morrisett, David Tarditi, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. The TIL/ML compiler: Performance and safety through types. In ACM SIGPLAN Workshop on Compiler Support for System Software, Tucson, AZ, USA, February 1996.

12. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Progamming Languages and Systems, 21(3):528–569, May 1999.

13. Flemming Nielson. The typed lambda-calculus with first-class processes. In Proceedings of PARLE, pages 357–373, April 1989.

14. Jens Palsberg. Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems, 17(1):47–62, January 1995. Preliminary version in Proceedings of CAAP’94, Colloquium on Trees in Algebra and Programming, Springer-Verlag (LNCS 787), pages 276–290, Edinburgh, Scotland, April 1994.

15. Jens Palsberg. Equality-based flow analysis versus recursive types. ACM Transactions on Programming Languages and Systems, 20(6):1251–1264, 1998.

16. Jens Palsberg and Patrick M. O’Keefe. A type system equivalent to flow analysis. ACM Transactions on Programming Languages and Systems, 17(4):576–599, July 1995. Preliminary version in Proceedings of POPL’95, 22nd Annual SIGPLAN– SIGACT Symposium on Principles of Programming Languages, pages 367–378, San Francisco, California, January 1995.

17. Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. Journal of Functional Programming, 11(3):263– 317, May 2001. Preliminary version in Proceedings of POPL’98, 25th Annual SIGPLAN–SIGACT Symposium on Principles of Programming Languages, pages 197–208, San Diego, California, January 1998.

18. Jens Palsberg and Michael I. Schwartzbach. Object-Oriented Type Systems. John Wiley & Sons, 1994.

19. David Tarditi, Greg Morrisett, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181–192, Philadelphia, PA, USA, May 1996. ACM Press.

20. Andrew Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

21. Andrew Wright, Suresh Jagannathan, Cristian Ungureanu, and Aaron Hertzmann. Compiling Java to a typed lambda-calculus: A preliminary report. In ACM Workshop on Types in Compilation, Kyoto, Japan, March 1998.