# Static Single Information Form for Abstract Compilation

Davide Ancona, Giovanni Lagorio

► To cite this version:

Davide Ancona, Giovanni Lagorio. Static Single Information Form for Abstract Compilation. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.10-27, 10.1007/978-3-642-33475-7_2 . hal-01556212

HAL Id: hal-01556212

https://inria.hal.science/hal-01556212

Submitted on 4 Jul 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Static single information form for abstract
compilation*

Davide Ancona and Giovanni Lagorio

DIBRIS, Università di Genova, Italy
{Davide.Ancona,Giovanni.Lagorio}@unige.it

**Abstract.** In previous work we have shown that more precise type analysis can be achieved by exploiting union types and static single assignment (SSA) intermediate representation (IR) of code.

In this paper we exploit static single information (SSI), an extension
of SSA proposed in literature and adopted by some compilers, to allow
assignments of more precise types to variables in conditional branches.
In particular, SSI can be exploited rather easily and effectively to infer
more precise types in dynamic object-oriented languages, where explicit
runtime typechecking is frequently used.

We show how the use of SSI form can be smoothly integrated with ab-
stract compilation, our approach to static type analysis. In particular,
we define abstract compilation based on union and nominal types for
a simple dynamic object-oriented language in SSI form with a runtime
typechecking operator, to show how precise type inference can be.

# 1 Introduction

In previous work [6] we have shown that more precise type analysis can be achieved by exploiting union types and static single assignment (SSA) [8] intermediate representation (IR) of code. Most modern compilers (among others, GNU's GCC [15], the SUIF compiler system [14], Java HotSpot [12], and Java Jikes RVM [10]) and formal software development tools implement efficient algorithms for translating code in advanced forms of IR particularly suitable for static analysis, thus offering the concrete opportunity of exploiting such IRs to obtain more precise type analysis and inference, and to fruitfully reuse those software components devoted to IR generation.

*Abstract compilation* [5,4,6] is a modular approach to static type analysis aiming to reconcile types and symbolic execution: an expression *e* is well-typed if the goal generated by compiling *e* succeeds w.r.t. the coinductive<fnref n="1" /> model of the constraint logic program obtained by compiling the source program in which the expression is executed. In such a model terms are types representing possibly infinite sets of values, and goal resolution corresponds to symbolic execution.

<footnote>* This work has been partially supported by MIUR DISCO - Distribution, Interaction, Specification, Composition for Object Systems.</footnote>

<footnote n="1">¹ Coinduction allows proper treatment of recursive types and methods [5].</footnote>
Abstract compilation is particularly suited for implementing type inference and global type analysis of dynamic object-oriented languages in a modular way since one can provide several compilation schemes for the same language, each corresponding to a different kind of analysis, without changing the inference engine, which typically implements coinductive constraint logic programming [17,16,4]. For instance, in previous work we have defined compilation schemes based on union and structural object types, to support parametric and data polymorphism, (that is, polymorphic methods and fields) to obtain precise type analysis, and a smooth integration with the nominal type annotations contained in the programs and the inferred structural types [5]; other proposed compilation schemes aim to detect uncaught exceptions [4], or to integrate SSA IR in the presence of imperative features [6].

In this paper we exploit static single information (SSI), an extension of SSA proposed in literature [2,19], to allow more precise type inference in conditional branches guarded by runtime typechecks. SSI has been already adopted by compiler frameworks as LLVM [20], PyPy [3], and SUIF [18], and proved to be more effective than SSA for performing data flow analysis, program slicing, and interprocedural analysis. Similar IRs are adopted as well in formal software development tools.

We show how SSI can be exploited rather easily and effectively by abstract compilation to improve type inference of dynamic object-oriented languages, where explicit runtime typechecks are frequently used.

To this aim, we formally define the operational semantics of a simple dynamic object-oriented language in SSI form equipped with a runtime typechecking operator, and then provide an abstract compilation scheme based on union and nominal types supporting more precise type inference of branches guarded by explicit runtime typechecks.

The paper is structured as follows: Section 2 introduces SSA and SSI IRs and motivates their usefulness for type analysis; Section 3 formally defines the SSI IR of a dynamic object-oriented language equipped with an operator **instanceof** for runtime typechecking. Section 4 presents a compilation scheme for the defined IR, based on nominal and union types, and Section 5 concludes with some considerations on future work. Abstract compilation of the code examples in Section 2 together with the results of the resolution of some goals can be found in an extended version of this paper.<fnref n="2" />

## 2 Type analysis with SSA and SSI

In this section SSA and SSI IRs are introduced and their usefulness for type analysis is motivated.

<footnote n="2">² Available at ftp://ftp.disi.unige.it/person/AnconaD/tcs12long.pdf</footnote>
Type analysis with static single assignment form

Method `read()` declared below, in a dynamic object-oriented language, creates and returns a shape which is read through method `nextLine()` that reads the next available string from some input source. The partially omitted methods `readCircle()` and `readSquare()` read the needed data from the input, create, and return a new corresponding instance of `Circle` or `Square`.

```java
class ShapeReader {
    ...
    nextLine() {...}
    readCircle() { ... return new Circle(...); }
    readSquare() { ... return new Square(...); }
    read() {
        st = this.nextLine();
        if(st.equals("circle")) {
            sh = this.readCircle();
            this.print("A circle with radius ");
            this.print(sh.getRadius());
        }
        else if(st.equals("square")) {
            sh = this.readSquare();
            this.print("A square with side ");
            this.print(sh.getSide());
        }
        else throw new I/OException();
        this.print("Area = ");
        this.print(sh.area());
        return st;
    }
}
```

Although method `read()` is type safe, no type can be inferred for `sh` to correctly typecheck the method; indeed, when method `area()` is invoked, variable `sh` may hold an instance of `Circle` or `Square`, therefore the most precise type that can be correctly assigned to `sh` is `Circle ∨ Square`. However, if `sh` has type `Circle ∨ Square`, then both `sh.getRadius()` and `sh.getSide()` do not typecheck.

There are two different kinds of approaches to solve the problem shown above. One can either define a rather sophisticated flow-sensitive type system, where each occurrence of a single variable can be associated with a different type, or typecheck the SSA IR, in which the method can be compiled.

In an SSA IR the value of each variable is determined by exactly one assignment statement [8]. To obtain this property, a flow graph is built, and a suitable renaming of variables is performed to keep track of the possibly different versions of the same variable; following Singer's terminology [19] we call these versions *virtual registers*. Conventionally, this is achieved by using a different subscript for each virtual register corresponding to the same variable. For instance, in the SSA IR of method `read()` there are three virtual registers (`sh₀`, `sh₁` and `sh₂`) for the variable `sh`.

```java
read() {
    b1:{st₀ = this.nextLine();
        if(st₀.equals("circle"))
            jump b2;
        else
            jump b3;}
    b2:{sh₀this.readCircle();
        this.print("A circle with radius ");
```
```java
this.print(sh0.getRadius());
jump b5;}
b3:{if (st0.equals("square"))
    jump b4;
else
    jump b6;}
b4:{sh1 = this.readSquare();
    this.print("A square with side ");
    this.print(sh1.getSide());
    jump b5;}
b5:{sh2 = this.sh0.sh1;
    this.print("Area = ");
    this.print(sh2.area());
    jump out;}
b6:{throw new exception();}
out:{return sh2;}
}
```

To transform a program into SSA form, a pseudo-function, conventionally called $\varphi$-function, needs to be introduced to correctly deal with merge points. For instance, in block b5 the value of sh can be that of either sh0 or sh1, therefore a new virtual register sh2 has to be introduced to preserve the SSA property. The expression $\varphi(\mathbf{sh}_0, \mathbf{sh}_1)$ simply keeps track of the fact that the value of sh2 is determined either by sh0 or sh1.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Type theoretic interpretation of $\varphi$-function and $\sigma$-function</figcaption></figure>

At the level of types, the $\varphi$-function naturally corresponds to the union type constructor (Figure 1): arrows correspond to data flow and, as usual, to ensure soundness the type at the origin of an arrow must be a subtype of the type the arrow points to. That is, for the types shown in the figure, $\tau_0, \tau_1 \le \tau_0 \lor \tau_1 \le \tau_2$.

Thanks to pretty standard and efficient algorithms for transforming source programs into SSA IR [8,9], the flow analysis phase, where source code is transformed into IR, can be kept separate from the subsequent type analysis phase, favoring simplicity and reuse. Indeed, flow analysis and consequent transformation into IR is implemented by most compilers and formal software development tools. Abstract compilation makes such an approach even more modular, by dividing the overall process into three separate stages. First, the source code is transformed into a suitable IR. Then, the IR is compiled into a set of Horn clauses and a goal. Finally, the goal is resolved with an appropriate inference engine (typically, implementing coinductive constraint logic programming [4]).
This paper mainly focuses on the second stage of the overall process (that is, compilation from IR into Horn clauses), in the particular case when the adopted IR allows precise flow analysis, as happens with SSI, of dynamic object-oriented languages.

## Type analysis with static single information form

Let us consider method `largerThan(sh)` of class `Square`, where `instanceof` is exploited to make the method more efficient in case the parameter `sh` contains an instance of (a subclass) of `Square`.

```java
class Square {
    ...
    largerThan(sh) {
        if(sh instanceof Square)
            return thisside > shside;
        else
            return thisarea() > sharea();
    }
}
```

The method is transformed into the following SSA IR:

```java
largerThan(sh0) {
    b1: {if(sh0 instanceof Square)
          jump b2;
        else
          jump b3;}
    b2: {r0 = thisside > sh0side;
          jump out;}
    b3: {r1 = thisarea() > sh0area();
          jump out;}
    out: {r2 = ϕ(r0, r1);
          return r2;}
}
```

Since variable `sh` is not updated, both blocks `b2` and `b3` refer to the same virtual register `sh0`. As a consequence, the only possible type that can be correctly associated with `sh0` is `Square`, thus making the method of little use. However, this problem can be addressed if one considers the SSI IR of the method [2,19].

```java
largerThan(sh0) {
    b1: {if(sh0 instanceof Square) with (sh1, sh2) = σ(sh0)
          (this1, this2) = σ(this0)
          jump b2;
        else
          jump b3;}
    b2: {r0 = this1side > sh1side;
          jump out;}
    b3: {r1 = this2area() > sh2area();
          jump out;}
    out: {r2 = ϕ(r0, r1);
          return r2;}
}
```

SSI is an extension of SSA enforcing the additional constraint that all variables must have different virtual registers in the branches of conditional expressions. Such a property is obtained by a suitable renaming and by the insertion of a pseudo function, called σ-function. As a consequence, suitable virtual registers
and a σ-function have to be introduced also for the read-only pseudo-variable **this**.

The notion of σ-function is the dual of ϕ-function (Figure 1); the type theoretic interpretation of σ depends on the specific kind of guard. If it is a runtime typecheck (of the form `(sh₀ instanceof Square)` as in the example), then σ splits the type `τ₀` of `sh₀` in the type `τ₀∧Square`, assigned to `sh₁`, and in the type `τ₀\Square`, assigned to `sh₂`, where the intersection and the complement operators have to be properly defined (see Section 4). For instance, if `sh₀` has type `Square∨Circle`, then `sh₁` has type `(Square∧Circle)∧Square=Square`, and `sh₂` has type `(Square∧Circle)\Square=Circle`, therefore `Square∧Circle` turns out to be a valid type for the parameter `sh₀` of the method `largerThan`.

For what concerns **this**, in this particular example no real split would be necessary: `this₀` has type `Square`, so `Square` is split into `(Square, Square)`, that is, both `this₁` and `this₂` have the same type `Square`.

## 3 Language definition

In this section we formally define an SSI IR for a simple dynamic object-oriented language equipped with an **instanceof** operator for performing runtime type-checking. Even though we have chosen a familiar Java-like syntax both for the IR and the source code used in the examples, the language is fully dynamic: code does not contain any type annotation, hence, under this point of view the language is quite different from Java.

prog ::= $\overline{cd}^n \{\overline{b}^n\}$
cd ::= class $c_1$ extends $c_2$ { $\overline{f}^n \overline{md}^k$ } (c₁ ≠ Object)
md ::= $m(\overline{r}^n) \{\overline{b}^n\}$
b ::= l:e
r ::= xᵢ
e ::= r | new $c(\overline{e}^n)$ | e.f | $e_0$.m($\overline{e}^n$) | $e_1$; $e_2$ | r = e
| $e_1$.f = $e_2$ | jump l | r = ϕ($\overline{r}^n$) | return r
| if (r **instanceof** c) with ($\overline{r'}$, $\overline{r''}$) = σ($\overline{r'''}$) **jump** l₁ **else** jump l₂

**Syntactic assumptions:** inheritance is not cyclic, method bodies are in correct SSI form and are terminated with a unique **return** statement, method and class names are disjoint, no name conflicts in class, field, method and parameter declarations, main expression and declared parameters cannot be **this**.

<caption>**Fig. 2.** SSI intermediate language</caption>

A program is a collection of class declarations followed by an anonymous main method with no parameters and contained in an anonymous class (conventionally its fully qualified name is `e.e`), whose body is a sequence of blocks (see the comments on method bodies below).
The notation $\overline{cd}^n$ is a shortcut for $cd_1, \dots, cd_n$. A class declares its direct superclass (only single inheritance is supported), its fields, and its methods. *Object* is the usual predefined root class of the inheritance tree; every class comes equipped with the implicit constructor with parameters corresponding to all fields, in the same order as they are inherited and declared. For simplicity, no user constructors can be declared.

Method bodies are sequences of uniquely labeled blocks that contain sequences of expressions. We assume that all blocks contain exactly one jump, necessarily placed at the end of the block. Three different kinds of jumps are considered: local unconditional and conditional jumps, and returns from methods. Method bodies are implicitly assumed to be in correct SSI IR: each virtual register is determined by exactly one assignment statement, and all variables must have different virtual registers in the branches of conditional expressions. Finally, all method bodies contain exactly one return expression, which is always placed at the end of the body.<fnref n="3" />

Virtual registers have the form $x_i$, where $x$ is the corresponding variable. If $r$ is a virtual register, then $var(r)$ returns the variable the register refers to, therefore if $r = x_i$, then $var(r) = x_i$. The receiver object can be referred inside method bodies with the special implicit parameter *this*, hence the IR contains virtual registers of the form $this_i$.

Besides usual statements and expressions, we consider $\varphi$ and $\sigma$ pseudo-function assignments. Conditional jumps contain $\sigma$-functions which split each virtual register $r$ occurring in either branches into two new distinct versions used in the blocks labeled by $l_1$ and $l_2$, respectively. The guard can only be of the form ($r$ **instanceof** $c$); however, more elaborated guards can be easily expressed in terms of this primitive one by suitable transformations during the compilation from the source code to the IR. Depending on the types and abstract compilation scheme, there could be other kinds of guards for which SSI would improve type analysis; for instance, if one includes the type corresponding to the null references, then a guard of the form ($r == null$) would take advantage of SSI to enhance null reference analysis. For those guards for which no type refinement is possible the $\sigma$-function performs no split, that is, $\sigma(\tau)=(\tau, \tau)$.

*Semantics:* To define the small step semantics of the language we first need to specify values $v$ (see Figure 3), which are just identities $o$ of dynamically created objects. Furthermore, we add *frame expressions* $ec\{e\}$, where $ec$ is an execution context; frame expressions are *runtime expressions* needed for defining the small step semantics of method calls. An execution context $ec$ is a pair consisting of a stack frame $fr$ and a fully qualified name $\mu$. A frame expression $\langle fr, \mu \rangle\{e\}$ corresponds to the execution of a call to a method $m$ declared in class $c$, where $e$ is the residual expression (yet to be evaluated) of the currently executed block,

<footnote n="3">³ Such a constraint does not imply any loss of generality, since it is always possible to add new virtual registers and to insert a $\varphi$-function when the source code contains multiple returns.</footnote>
$fr$ is the stack frame of the method call, and $\mu = c.m$ is the fully qualified name of the method.

```
v ::= o (values)
e ::= v | ec{e} | ... (runtime expressions)
ec ::= ⟨fr, μ⟩ (execution context)
fr ::= r ↦→ v^k (stack frames)
μ ::= c.m (full method names)
H ::= o ↦→ ⟨c, f ↦→ v⟩^k (heaps)
C[·] ::= [·] | ec{C[·]} | new c(v¯^n, C[·], e¯^j) | C[·].f | C[·].m(v¯^k) | v₀.m(v¯^j, C[·], e¯^k)
| C[·]; e | x = C[·] | C[·].f = e | v.f = C[·]
| if (C[·]) with (x', x'') = σ(x''')^n jump l₁ else jump l₂
```

<caption>**Fig. 3.** Syntactic definitions instrumental to the operational semantics</caption>

Stack frames $fr$ map virtual registers to their corresponding values. Each association is labeled with a distinct time-stamp $t$, which specifies how recently the register has been updated (higher time-stamp values correspond to more recent updates). Such labels are used to define the semantics of $\varphi$-function assignments.

Heaps $\mathcal{H}$ map object identifiers $o$ to objects, that is, pairs consisting of a class name $c$ and the set of field names $f$ with their corresponding value $v$.

Figure 4 shows the execution rules. Three different judgments are defined: the main judgment $\overline{cd}^n \{\overline{b}^n\} \Rightarrow v$ states that the main method $\{\overline{b}^n\}$ of program $\overline{cd}^n$ evaluates to value $v$. Such a judgment directly depends on the auxiliary judgment $\mathcal{H} \vdash e \rightarrow \mathcal{H}', e'$, stating that $e$ rewrites to $e'$ in $\mathcal{H}$, yielding the new heap $\mathcal{H}'$, and whose definition uses the auxiliary judgment $\mathcal{H}, ec \vdash e \rightarrow \mathcal{H}', ec', e'$, having the meaning that redex $e$ rewrites to $e'$ in $\mathcal{H}$ and $ec$, yielding the new execution context $ec'$ and heap $\mathcal{H}'$. All the auxiliary judgments and functions<fnref n="4" /> should be parametrized by the whole executing program, $\overline{cd}^n$, which, however, is kept implicit to favor readability.

Rule (main) defines the main judgment; a value $v$ is returned if the runtime expression $⟨\epsilon_{fr}, \epsilon.\epsilon⟩\{e\}$, where $e$ is the first block (retrieved by the auxiliary function firstBlock) of the main method, transitively rewrites to $v$ (and a heap $\mathcal{H}$ which is discarded). The evaluation context $⟨\epsilon_{fr}, \epsilon.\epsilon⟩$ of the frame expression specifies that initially the frame $(\epsilon_{fr})$ is empty (neither this, nor parameters are accessible), and that execution starts in the main method, whose fully qualified name is $\epsilon.\epsilon$ (recall that, conventionally, the main method is anonymous and is contained in an anonymous class).

The auxiliary judgment $\mathcal{H} \vdash e \rightarrow \mathcal{H}', e'$ is defined by the three rules (method) (a new execution context is created), (ctx) (evaluation continues in the currently active execution context), and (return) (the current execution context is closed).

<footnote n="4">⁴ The straightforward definitions of the auxiliary functions have been omitted.</footnote>
$$ (\text{main}) \frac{\text{firstBlock}(\epsilon.\epsilon) = e \quad \epsilon_H \vdash \langle \epsilon_{fr}, \epsilon.\epsilon \rangle \{e\} \to^* \mathcal{H}, v}{\overline{cd}^n \{\overline{b}^n\} \Rightarrow v} $$

$$ \mathcal{H}(o) = \langle c, \neg \rangle $$

$$ \text{firstBlock}(c.m) = e $$

$$ \text{params}(c.m) = \bar{r}^n $$

$$ (\text{meth-call}) \frac{\overline{fr} = \overline{r} \mapsto \overline{v}^n, \mathbf{this}_0 \mapsto o}{\mathcal{H} \vdash \mathcal{C}[o.m(\overline{v}^n)] \quad \rightarrow \mathcal{H}, \mathcal{C}[\langle fr, c.m \rangle \{e\}]} $$

$$ \text{currentEC}(\mathcal{C}[\cdot]) = \text{ec} $$

$$ \mathcal{H}, \text{ec} \vdash e \rightarrow \mathcal{H}', \text{ec}', e' $$

$$ (\text{ctx}) \frac{\mathcal{C}'[\cdot] = \text{updateEC}(\mathcal{C}[\cdot], \text{ec}')}{\mathcal{H} \vdash \mathcal{C}[e] \rightarrow \mathcal{H}', \mathcal{C}'[e']}, $$

$$ (\text{return}) \frac{\overline{\mathcal{H}} \vdash \mathcal{C}[\langle fr, \mu \rangle \{\text{return } r \}]}{\rightarrow \mathcal{H}, \mathcal{C}[fr(r)]} \quad (\text{fld-acc}) \frac{\mathcal{H}(o) = \langle c, \overline{f} \mapsto \overline{v}^n \rangle \quad f = f_j}{\mathcal{H}, \text{ec} \vdash o.f \rightarrow \mathcal{H}, \text{ec}, v_j} $$

$o$ fresh in $\mathcal{H}$

$$ (\text{reg}) \frac{\overline{\mathcal{H}}, \langle fr, \mu \rangle \vdash r \rightarrow \mathcal{H}, \langle fr, \mu \rangle, fr(r)}{(\text{new}) \frac{\overline{\mathcal{H}}, \text{ec} \vdash \textbf{new} c(\overline{v}^n)}{\rightarrow \mathcal{H}[\langle c, \overline{f} \mapsto \overline{v}^n \rangle/o], \text{ec}, o}} $$

$$ (\text{seq}) \frac{\overline{\mathcal{H}}, \text{ec} \vdash v; e \rightarrow \mathcal{H}, \text{ec}, e}{(\text{reg-asn}) \frac{\overline{\mathcal{H}}, \langle fr, \mu \rangle \vdash r = v}{\rightarrow \mathcal{H}, \langle fr[v/r], \mu \rangle, v}} $$

$$ \mathcal{H}(o) = \langle c, \overline{f} \mapsto \overline{v}^n \rangle $$

$$ f = f_j \quad \text{if } i = j \text{ then } v_i' = v $$

$$ \text{else } v_i' = v_i $$

$$ (\text{fld-asn}) \frac{\overline{\mathcal{H}}, \text{ec} \vdash o.f = v}{\rightarrow \mathcal{H}[\langle c, \overline{f} \mapsto v'^n \rangle/o], \text{ec}, v} \quad (\text{jump}) \frac{\overline{\text{block}}(\mu, l) = e}{\mathcal{H}, \langle fr, \mu \rangle \vdash \textbf{jump } l} \quad \rightarrow \mathcal{H}, \langle fr, \mu \rangle, e $$

$$ (\text{phi}) \frac{\overline{\mathcal{H}}, \langle fr, \mu \rangle \vdash r_0 = \varphi(\bar{r}^n) \rightarrow \mathcal{H}, \langle fr[mru fr, \bar{r}^n]/r_0 \rangle, \mu \rangle, v}{\overline{\mathcal{H}}(fr(r)) = \langle c', \neg \rangle} $$

$$ \mathcal{H}(fr(r)) = \langle c', \neg \rangle $$

$$ \text{if } c' \le c \text{ then } l' = l_1, fr' = fr[\overline{fr(r''')/r'^n}] $$

$$ \text{else } l' = l_2, fr' = fr[\overline{fr(r''')/r''^n}] $$

$$ (\text{if}) \frac{\overline{\text{block}}(\mu, l')}{\mathcal{H}, \langle fr, \mu \rangle \vdash \textbf{if } (r \text{ instanceof } c) \text{ with } (r', r'') = \sigma(r''')^n \quad \text{jump } l_1 \text{ else jump } l_2} \quad \rightarrow \mathcal{H}, \langle fr, \mu \rangle, e $$

<caption>Fig. 4. Small-step semantics</caption>
In rule (meth-call), the object referenced by *o* is retrieved from the heap to find its class, *c*. Then, the auxiliary functions *firstBlock* and *params* return the first block of the method and its parameters, respectively. The result of the evaluation is a frame expression, where the new stack frame maps parameters to their corresponding arguments, and *this*₀ to *o*, the fully qualified name *c.m* corresponds to the invoked method, and the expression is the first block of the method. Rule (*ctx*) deals with context closure. Contexts (the standard definition is in Figure 3) correspond to a deterministic call-by-value and left-to-right evaluation strategy. A single computation step in the current execution context (corresponding to the most nested frame expression) is performed. The active execution context is extracted by *currentEC*; then, if the redex *e* rewrites to *e'* yielding *H'* and *ec'* (see the other rules defining the auxiliary evaluation judgment), then the *C[e]* rewrites to *C*[*e*'], yielding the new heap *H'*; context *C*[*] is obtained from *C*[*] by updating the frame expression corresponding to the active execution context with the new execution context *ec'*. In rule (*return*) the current execution context is closed, the heap is unaffected, and the result is the value associated with the returned virtual register *r* in the frame of the closing context.

The remaining rules define the auxiliary judgment $\mathcal{H}, ec \vdash e \rightarrow \mathcal{H}', ec', e'$, one for any distinct kind of redex. In rule (**reg**) a virtual register is accessed by extracting the corresponding value from the stack frame *fr*. Variable and field assignments evaluate to their right values; rule (**reg-asn**) has the side effect of updating, in the current stack frame *fr*, the value of the virtual register *r* and its associated time-stamp (this is implicit in the definition of *fr*[*v*/*r*]) since, after the assignment, *r* becomes the most recently updated register. Rule (**fld-asn**) deals with field assignments: the object referenced by *o* is retrieved from the heap, and its value updated. In rule (**seq**) the left-hand-side value in a sequence expression is discarded to allow evaluation to proceed with the next expression. In rule (**phi**), register *r*₀ is updated with the value (denoted by *mru*(*fr*, $\overline{r}^n$)) of the most recently updated register in the stack frame, between $\overline{r}^n$. In rule (**new**) a new object, identified by a fresh reference *o*, is added to the heap *H*. The fields $\overline{r}^n$ of the newly created object are initialized by the values passed to the constructor. In rule (**fld-acc**) field accesses are evaluated: the object is retrieved from the heap, and the resulting expression is the value of the selected field. Rules (**jump**) and (**if**) deal with unconditional and conditional jumps, respectively. The evaluation of a jump returns the expression *e* contained in the block labeled by *l'* in the method $\mu$ of the current execution context. The conditional jump (rule (**if**)) selects which branch to execute and which virtual registers have to be updated, depending on whether the value *fr*(*r*) of the register *r* is a reference to an object of a subclass of *c*. If it is the case, then the returned expression is that labeled by *l*₁ and the virtual registers $\overline{r}^n$ are updated; otherwise, the returned expression is that labeled by *l*₂ and the virtual registers $\overline{r}''^n$ are updated.

As an example, let us consider the expression $x_0 = \text{new } c(); \text{return } x_0$ in a program where *c* is defined and has no fields.
Then $\epsilon_H \vdash \langle \epsilon_{fr}, \epsilon.\epsilon \rangle \{x_0=\mathbf{new C()} ; \mathbf{return x_0}\} \to \mathcal{H}, \langle \epsilon_{fr}, \epsilon.\epsilon \rangle \{x_0=\mathbf{o} ; \mathbf{return x_0}\}$ by rules (ctx) (with context $x_0=[\cdot]$; return $x_0$) and (new), where $\mathcal{H} = \mathbf{o} \mapsto \langle \mathbf{C}, \epsilon \rangle$; $\mathcal{H} \vdash \langle \epsilon_{fr}, \epsilon.\epsilon \rangle \{x_0=\mathbf{o} ; \mathbf{return x_0}\} \to \mathcal{H}, \langle fr, \epsilon.\epsilon \rangle \{\mathbf{o} ; \mathbf{return x_0}\}$ by rules (ctx) (with context $[\cdot]$; return $x_0$) and (var-asn), where $fr = \mathbf{x} \mapsto \mathbf{o}, x_0 \mapsto \mathbf{o}$; $\mathcal{H} \vdash \langle fr, \epsilon.\epsilon \rangle \{\mathbf{o} ; \mathbf{return x_0}\} \to \mathcal{H}, \langle fr, \epsilon.\epsilon \rangle \{\mathbf{return x_0}\}$ by rules (ctx) (with context $\langle fr, \epsilon.\epsilon \rangle \{[\cdot]\}$) and (seq); finally, $\mathcal{H} \vdash \langle fr, \epsilon.\epsilon \rangle \{\mathbf{return x_0}\} \to \mathcal{H}, \mathbf{o}$ by rule (return) (with context $[\cdot]$).

# 4 Abstract compilation

In this section we define an abstract compilation scheme for programs in the SSI IR presented in Section 3. Programs are translated into a Horn formula $Hf$ (that is, a logic program) and a goal $B$; type analysis and inference amounts to coinductive resolution of $B$, that is the greatest Herbrand model of $Hf$ [5] is considered. The proof of soundness of such a translation is sketched in the Appendix.

In previous work [5,6] we have used expressive structural types; however, since SSI favors more precise type analysis, we have preferred to follow a simpler approach based on nominal types. Structural types could be used as well to allow data polymorphism, with the downside that subtyping relation becomes much more involved and termination issues must be addressed.

Subtyping is treated as an ordinary predicate, thus allowing only global analysis; compositional analysis can be obtained by considering subtyping as a constraint, and by using coinductive constraint logic programming [4].

The compilation of programs, class, and method declarations is defined in Figure 5. We follow the usual syntactic conventions for logic programs: logical variable names begin with upper case, whereas predicate and functor names begin with lower case letters. Underscore denotes anonymous logical variables that occur only once in a clause; $[]$ and $[e|l]$ respectively represent the empty list, and the list where $e$ is the first element, and $l$ is the rest of the list.

Each rule defines a different compilation judgment. The judgment $cd^n e \rightsquigarrow (Hf^d \cup \overline{Hf}^n | B)$ states that the program $cd^n e$ is compiled into the pair $(Hf^d \cup \overline{Hf}^n | B)$, where $Hf^d \cup \overline{Hf}^n$ is a Horn formula (that is, a set of Horn clauses), and $B$ is a goal.<fnref n="5" /> Type inference of the main expression is obtained by coinductive resolution of the goal $B$ in $Hf^d \cup \overline{Hf}^n$. The Horn formula $Hf^d$ contains all clauses that are independent of the program (Figure 7), whereas each $Hf_i$ is obtained by compiling the class declaration $cd_i$ (see below); the goal $B$ is generated from the compilation of the main expression $e$ (see below); the term $t$ corresponds to the returned type of $e$; it is ignored here, but it is necessary for compiling expressions.

The compilation of a class declaration `class c1 extends c2 { f^n md^k }` is a set of clauses, including each clause $Hf_i$ obtained by compiling the method

<footnote n="5">⁵ For simplicity we use the same meta-variable $B$ to denote conjunctions of atoms (that is, clause bodies), and goals, even though more formally goals are special clauses of the form `false ← B`.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 5. Compilation of programs, class, and method declarations and bodies.</figcaption></figure>

$md_i$ (see below), clauses asserting that class $c_1$ declares field $f_i$, for all $i = 1..n$, and three specific clauses for predicates *class*, *extends*, and *new*. The clause for *new* deserves some explanations: the atom $new(ce, c, [\bar{t}^n])$ succeeds iff the invocation of the implicit constructor of *c* with *n* arguments of type $\bar{t}^n$ is type safe in the global class type environment *ce*. The class environment *ce* is required for compiling field access and update expressions (Figure 6): it is a finite map (simply represented by a list) associating class names with field records (finite maps again simply represented by lists) assigning types to all fields of a class. Class environments are required because of nominal types: abstract compilation with structural types allows data polymorphism on a per-object basis, whereas here we obtain only a very limited form of data polymorphism on a per-class basis. Type safety of object creation is checked by ensuring that object creation for the direct superclass $c_2$ is correct, where only the first part *h* of the arguments corresponding to the inherited fields (returned by the auxiliary function *inhFields* whose straightforward definition has been omitted) are passed; then, predicate *field-upd* defined in Figure 7 checks that all remaining *n* arguments, corresponding to the new fields declared in $c_1$, have types that are compatible with those specified in the class environment. The clause dealing with the base case for the root class *Object* is also defined in Figure 7.

The judgment $m(\bar{r}^n)\{\bar{b}^n\} \text{ in } c \rightsquigarrow Hf$ states that the method declaration $m(\bar{r}^n)\{\bar{b}^n\}$ contained in class *c* compiles to Horn clauses *Hf*. Two clauses are generated per method declaration: the first simply states that method *m* is declared in class *c* (and is needed to deal with inherited methods Figure 7), whereas the second is obtained by compiling the body of the method. The atom *has_meth*(*ce*, *c*, *m*, [*t*₀, *t*ⁿ], *t*) succeeds iff, in class environment *ce* method *m* of
class c can be safely invoked on target object of type t₀, with n arguments of
type $\bar{t}^n$ and returned value of type t. The predicate subclass (defined in Figure 7)
ensures that the method can be invoked only on objects that are instances of c
or one of its subclasses. For simplicity we assume that all names (including this)
are translated to themselves, even though, in practice, appropriate injective re-
naming should be applied [5]. The compilation of a method body $\bar{b}^n$ l:return r
consists of the type of the returned virtual register r, and the conjunction of all
the atoms generated by the compilation of blocks $\bar{b}^n$.

Figure 6 defines abstract compilation for blocks, and expressions.

<figure><img src="image_4.png" /><figcaption>Fig. 6. Compilation of blocks and expressions</figcaption></figure>

Compiling a block *l:e* returns the conjunction of atoms obtained by compiling *e*; the type *t* of *e* is discarded. The compilation of *e*₁; *e*₂ returns the type of *e*₂ and the conjunction of atoms generated from the compilation of *e*₁ and *e*₂. The compilation of an unconditional jump generates the type *void* and the empty conjunction of atoms *true*. A conditional jump has type *void* as well, but a non-empty sequence of predicates is generated to deal with the splitting performed by the *σ*-functions; predicates *inter* and *diff* (defined in Figure 7) compute the
intersection *T* and the difference *F* between the type of *r* and *c*, respectively, and predicate *var_upd* (defined in Figure 7) ensures that the type of virtual registers *r*ᵢ' and *r*ᵢ'' are compatible with the pairs of types returned by the *σ*-functions. In case *r*ᵢ''' refers to the same variable of *r* the types of such a pair are the computed intersection *T* and difference *F*, respectively, otherwise the pair (*r*ᵢ''', *r*ᵢ''') is returned (hence, no split is actually performed). Compilation of assignments to virtual registers and fields yields the conjunction of the atoms generated from the corresponding sub-expressions, together with the atoms that ensure that the assignment is type compatible (with predicates *var_upd* and *field_upd* defined in Figure 7). The returned type is the type of the right-hand side expression. Compilation of φ-function assignments to virtual registers is just an instantiation of rule (*var-upd*) where the type of the expression is the union of the types of the virtual registers passed as arguments to φ. Compilation rules for object creation, field selection, and method invocation follow the same pattern: the type of the expression is a fresh logical variable (except for object creation) corresponding to the type returned by the specific predicate (*new*, *field*, and *invoke* defined in Figure 7). The generated atoms are those obtained from the compilation of the sub-expressions, together with the atom specific of the expression. Rules (*var*) is straightforward.

The clauses (see *Hf*<sup>*d*</sup> in (prog)) that do not depend on the specific program are defined in Figure 7 in the Appendix.

Predicate *subtype* defining the subtyping relation deserves some comments: as expected, classes *c*₁ and *c*₂ are both subtypes of *c*₁ ∨ *c*₂, but *c*₁ is not a subtype of *c*₂ when *C*₁ is a proper subclass of *c*₂: since no rule is imposed on method overriding, subclassing is not subtyping. Consider for instance the following source code snippet:

class Square { ... equals(s){return this side==s side;} ... }
class ColoredSquare extends Square {
  ... equals/cs{/}return this .side==cs .side&&this .color==cs .color;} ... }

According to our compilation scheme, the expression `s1 equals(s2)` has type
`Bool` if `s1` and `s2` have type `Square` and `Square ∨ ColoredSquare`, respectively,
but the same expression is not well-typed if `s1` has type `ColoredSquare` (hence,
`ColoredSquare ∼≤ Square`), since `s2` cannot contain an instance of `Square` for which
field `color` is not defined. Subtyping is required for defining the predicates
`var_upd` and `field_upd` for virtual register and field updates: the type of the
source must be a subtype of the type of the destination.

Type *empty* is the bottom of the subtyping relation. The predicates *inter* and *diff* (see below) can generate *empty* when a branch is unreachable. Of course, field accesses and method invocations on type *empty* are correct (in practice they can only occur in dead code).

Predicate *field* looks up the type of a field in the global class environment, and is defined in terms of the auxiliary predicates *has_field*, *class_fields*, *field_type*, and *no_def*. In particular, predicate *has_field* checks that a class has actually a certain field, either declared or inherited. The definitions of *class_fields*, *field_type*, and *no_def* are straightforward (*no_def* ensures that a map does not
contain multiple entries for a key), whereas the clause for *has_field* dealing with
inherited fields is similar to the corresponding one for *invoke* (see below).

If the target object has a class type *c*, then the correctness of method invo-
cation is checked with predicate *has_meth* applied to class *c* and to the same list
of arguments where, however, the type *c* of *this* is added at the beginning. If the
target object has a union type, predicate *invoke* checks that method invocation
is correct for both types of the union, and then merges the types of the results
into a single union type.

Finally, the clause for *has_meth* deals with the inherited methods: if class *c*
does not declare method *m*, then *has_meth* must hold on the direct superclass
of *c*.

Predicates *inter* and *diff* define type splitting for *σ*-functions; both predicates never fail, but the type *empty* is returned when a branch is not reachable. Their definition is straightforward: the former keeps all classes that satisfies the runtime typechecking, the latter all classes that do not satisfy it.

5 Conclusion

We have shown how SSI IR can be exploited by abstract compilation for static
global type analysis of programs written in a dynamic object-oriented language
equipped with an **instanceof** operator for runtime typechecks. The approach
allows a rather precise analysis with just nominal and union types.

We have stated soundness of type inference and sketched the proof; to do
that, a small step operational semantics of the SSI IR language has been for-
mally defined; this is also an original contribution, since, to our knowledge, no
prior formal definition of the semantics of an SSI IR language can be found in
literature.

There already exists interesting work on type inference of dynamic object-
oriented languages, and several papers have defined and studied flow sensitive
type systems [7,1,11,13] (to mention just a few). The main distinguishing feature
of abstract compilation, when compared with all other approaches, is its modu-
larity. Abstract compilation allows one to implement different kinds of analysis,
for different languages with a suitable compilation scheme, by using the same
inference engine. Furthermore, abstract compilation is particularly suited for di-
rectly compiling IR languages, as SSI, to greatly improve the precision of the
analysis.

Guarded type promotion [21] for Java allows more precise type analysis of branches guarded by dynamic type checks in a very similar way as in our approach. However, here we consider the more challenging problem of inferring types for a dynamic language where no type annotations are provided by the programmers.

References

1. J. An, A. Chaudhuri, J.S. Foster, and M. Hicks. Dynamic inference of static types for Ruby. In *POPL*, pages 459–472, 2011.
2. C. S. Ananian. The static single information form. Technical Report MITLCS-TR-801, MIT, 1999.

3. D. Ancona, M. Ancona, A Cuni, and N. Matsakis. RPython: a Step Towards Reconciling Dynamically and Statically Typed OO Languages. In *DLS'07*, pages 53–64. ACM, 2007.

4. D. Ancona, A. Corradi, G. Lagorio, and F. Damiani. Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? In *FoVeOOS 2010, Revised Selected Papers*, volume 6528 of LNCS. Springer Verlag, 2011.

5. D. Ancona and G. Lagorio. Coinductive type systems for object-oriented languages. In *ECOOP 2009*, volume 5653 of LNCS, pages 2–26. Springer Verlag, 2009. Best paper prize.

6. D. Ancona and G. Lagorio. Idealized coinductive type systems for imperative object-oriented programs. *RAIRO - Theoretical Informatics and Applications*, 45(1):3–33, 2011.

7. C. Anderson, P. Giannini, and S. Drossopoulou. Towards type inference for javascript. In *ECOOP 2005 - Object-Oriented Programming*, volume 3586 of LNCS, pages 428–452. Springer Verlag, 2005.

8. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. *TOPLAS*, 13:451–490, 1991.

9. D. Das and U. Ramakrishna. A practical and fast iterative algorithm for phi-function computation using DJ graphs. *TOPLAS*, 27(3):426–440, 2005.

10. B. Alpern et. al. The jalapeño virtual machine. *IBM Systems Journal*, 39, 2000.

11. J.S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In *PLDI*, pages 1–12, 2002.

12. R. Griesemer and S. Mitrovic. A compiler for the java hotspott virtual machine. In *The School of Niklaus Wirth, "The Art of Simplicity"*, pages 133–152, 2000.

13. P. Heidegger and P. Thiemann. Recency types for analyzing scripting languages. In *ECOOP 2010 - Object-Oriented Programming*, volume 6183 of LNCS, pages 200–224. Springer Verlag, 2010.

14. G. Holloway. The machine-SUIF static single assignment library. Technical report, Harvard School of Engineering and Applied Sciences, 2001.

15. D. Novillo. Tree SSA - a new optimization infrastructure for GCC. In *GCC Developers' Summit*, pages 181–193, 2003.

16. L. Simon, A. Bansal, A. Mallya, and G. Gupta. Co-logic programming: Extending logic programming with coinduction. In *ICALP 2007*, pages 472–483, 2007.

17. L. Simon, A. Mallya, A. Bansal, and G. Gupta. Coinductive logic programming. In *ICLP 2006*, pages 330–345, 2006.

18. J. Singer. Static single information form in machine SUIF. Technical report, University of Cambridge Computer Laboratory, UK, 2004.

19. J. Singer. *Static Program Analysis based on Virtual Register Renaming*. PhD thesis, Christs College, 2005.

20. A. Tavares, F.M. Pereira, M. Bigonha, and R. Bigonha. Efficient SSI conversion. In *SBLP 2010*, 2010.

21. J. Winther. Guarded type promotion (eliminating redundant casts in Java). In *FTfJP 2011*. ACM, 2011.
class(object) ← true.
subclass(X, X) ← class(X).
subclass(X, Y) ← extends(X, Z), subclass(Z, Y).
subtype Kash, T) ← true.
subtype(T, T) ← true.
subtype(T1 ∨ T2, T) ← subtype(T1, T), subtype(T2, T).
subtype(T, T1 ∨ T2) ← subtype(T, T1).
subtype(T, T1 ∨ T2) ← subtype(T, T2).
field(CE, empty, -, -) ← true.
field(CE, C, F, T) ← has_field(C, F), class_fields(CE, C, R), field_type(R, F, T).
field(CE, T1 ∨ T2, F, FT1 ∨ FT2) ← field(CE, T1, F, FT1),
field(CE, T2, F, FT2).
class_fields([C : R | CE], C, R) ← no_def(C, CE).
class_fields([C1 : - | CE], C2, R) ← class_fields(CE, C2, R), C1 ≠ C2.
field_type([F : T | R], F, T) ← no_def(F, R).
field_type([F1 : - | R], F2, T) ← field_type(R, F2, T), F1 ≠ F2.
no_def(-, []) ← true.
no_def(K1, [K2 : - | Tl]) ← no_def(K1, Tl), K1 ≠ K2.
invoke(-, empty, -, -, -) ← true.
invoke(CE, C, M, A, RT) ← has_meth(CE, C, M, [C | A], RT).
invoke(CE, T1 ∨ T2, M, A, RT1 ∨ RT2) ← invoke(CE, T1, M, A, RT1),
invoke(CE, T2, M, A, RT2).
new(-, object, []) ← true.
has_field(C, F) ← dec_field(C, F).
has_field(C, F) ← extends(C, P), has_field(P, F), ¬dec_field(C, F).
has_meth(CE, C, M, A, R) ← extends(C, P), has_meth(CE, P, M, A, R),
¬dec_meth(C, M).
var_upd(T1, T2) ← subtype(T2, T1).
field_upd(CE, C, F, T2) ← field(CE, C, F, T1), subtype(T2, T1).
inter(C1, C2, C1) ← subclass(C1, C2).
inter(C1, C2, empty) ← ¬subclass(C1, C2).
inter(T1 ∨ T2, C, IT1 ∨ IT2) ← inter(T1, C, IT1), inter(T2, C, IT2).
diff(C1, C2, C1) ← class(C1), ¬subclass(C1, C2).
diff(C1, C2, empty) ← class(C1), subclass(C1, C2).
diff(T1 ∨ T2, C, IT1 ∨ IT2) ← diff(T1, C, IT1), diff(T2, C, IT2).

<caption>Fig. 7. Clauses defining the predicates used by the abstract compilation</caption>
A Proof of soundness

To sketch the proof of soundness of abstract compilation, abstract compilation of expressions has to be extended to cover also runtime expressions, hence we define the new judgment $\mathcal{H}, fr, e \rightsquigarrow (t | B)$ (defined in Figure 8) stating that the runtime expression $e$ compiles to the type $t$ and the conjunction of atoms $B$ in the heap $\mathcal{H}$ and stack frame $fr$. Heaps and stack frames are needed for compiling object values and virtual registers. All rules obtained as straightforward extension of the corresponding rules in Figure 6 have been omitted. In the sequel, all

$$ (\text{obj}) \frac{\mathcal{H}(o) = \langle c, \rangle}{\mathcal{H}, fr, o \rightsquigarrow (c | \text{true})} \qquad (\text{frame}) \frac{\mathcal{H}, fr', e \rightsquigarrow (t | B)}{\mathcal{H}, fr, \langle fr', \mu \rangle \{e\} \rightsquigarrow (t | B)} $$

$$ (\text{c-jmp-then}) \frac{\text{fr}(r) = c' \quad c' \le c \quad \forall i = 1..n \text{ fr}(r_i') = t_i' \quad \text{if } \text{var}(r_i'') = \text{var}(r) \quad \text{then } t_i'' = c' \text{ else } t_i'' = \text{fr}(r_i'')} {\mathcal{H}, fr, \text{ if } (r \text{ instanceof } c) \text{ with } (r', r'') = \sigma(r'')^n \text{ jump } l_1 \text{ else jump } l_2 \text{ in } \rightsquigarrow (\text{void} | \text{var\_upd}(t', t'')^n)} $$

$$ (\text{c-jmp-else}) \frac{\text{fr}(r) = c' \quad c' \not\le c \quad \forall i = 1..n \text{ fr}(r_i'') = t_i' \quad \text{if } \text{var}(r_i'') = \text{var}(r) \quad \text{then } t_i'' = c' \text{ else } t_i'' = \text{fr}(r_i'')} {\mathcal{H}, fr, \text{ if } (r \text{ instanceof } c) \text{ with } (r', r'') = \sigma(r'')^n \text{ jump } l_1 \text{ else jump } l_2 \text{ in } \rightsquigarrow (\text{void} | \text{var\_upd}(t', t'')^n)} $$

$$ (\text{var-upd}) \frac{\mathcal{H}, fr, e \rightsquigarrow (t | B) \quad \text{fr}(r) = t'}{\mathcal{H}, fr, r = e \rightsquigarrow (t | B, \text{var\_upd}(t', t))} $$

$$ (\text{phi}) \frac{\forall i = 0..n \text{ fr}(r_i) = t_i}{\mathcal{H}, fr, r_0 = \varphi(\bar{r}^n) \rightsquigarrow (\sqrt{\bar{t}^n} | \text{var\_upd}(t_0, \sqrt{\bar{t}^n}))} \qquad (\text{var}) \frac{\text{fr}(r) = t}{\mathcal{H}, fr, r \rightsquigarrow (t | \text{true})} $$

<caption>Fig. 8. Compilation of runtime expressions</caption>

statements depend on a particular program $\overline{cd}^n$; furthermore, we state that the coinductive resolution of a goal succeeds to mean that it succeeds w.r.t. the abstract compilation of $\overline{cd}^n$.

**Lemma 1 (Progress).** If $\mathcal{H}, \epsilon_{fr}, e \rightsquigarrow (t | B)$, and the coinductive resolution of $B$ succeeds, then either $e$ is a value, or there exist $\mathcal{H}'$ and $e'$ s.t. $\mathcal{H} \vdash e \rightarrow \mathcal{H}', e'$.

**Lemma 2 (Subject Reduction).** If $\mathcal{H} \vdash e \rightarrow \mathcal{H}', e'$ and $\mathcal{H}, \epsilon_{fr}, e \rightsquigarrow (t | B)$ and the coinductive resolution of $B$ succeeds with grounding substitution $\theta$, then there exist $t'$ and $B'$ s.t. $\mathcal{H}, \epsilon_{fr}, e' \rightsquigarrow (t' | B')$, the coinductive resolution of $B'$ succeeds with grounding substitution $\theta'$, and subtype($\theta' t'$, $\theta t$) succeeds.

**Theorem 1 (Soundness).** If $\mathcal{H}, \epsilon_{fr}, e \rightsquigarrow (t | B)$ and the coinductive resolution of $B$ succeeds with grounding substitution $\theta$, and $\mathcal{H} \vdash e \rightarrow \mathcal{H}', e'$, and there exist no $\mathcal{H}''$ and $e''$ s.t. $\mathcal{H}' \vdash e' \rightarrow \mathcal{H}'', e''$, then $e'$ is an object value o s.t. $\mathcal{H}'(o) = \langle c, \rangle$, and subtype($c, \theta t$) succeeds.