11institutetext: fortiss GmbH, Guerickestraße 25, 80805 Munich, Germany

# Inferring Region Types via an Abstract Notion of Environment
Transformation††thanks: Supported by the German Research Foundation (DFG)
under the research grant 250888164 (GuideForce).

Ulrich Schöpp  0000-0002-5445-9461 Chuangjie Xu  0000-0001-6838-4221

###### Abstract

Region-based type systems are a powerful tool for various kinds of program
analysis. We introduce a new inference algorithm for region types based on an
abstract notion of environment transformation. It analyzes the code of a
method only once, even when there are multiple invocations of the method of
different region types in the program. Elements of such an abstract
transformation are essentially constraints for equality and subtyping that
capture flow information of the program. In particular, we work with access
graphs in the definition of abstract transformations to guarantee the
termination of the inference algorithm, because they provide a finite
representation of field access paths.

###### Keywords:

program analysis region type type inference environment transformation type
constraint Featherweight Java

##  1 Introduction

Programs typically make extensive use of libraries. Analyzing a program thus
often involves analysis of big libraries which can be heavy and expensive. The
situation gets worse for those analyses where multiple invocations of the same
library method requires to re-analyze the library. Therefore, it is
significant for analyses to be _compositional_ , that is, the analysis result
of a program can be computed from the results of its components. Once a
library has been analyzed, the result can be directly used to analyze programs
that use the library. This work aims at making _region type inference_
compositional.

Region-based type systems have been illustrated to be a powerful tool for e.g.
memory management [7, 8], pointer analysis and taint analysis [5, 14, 15]. The
usage of regions in effect-and-type systems can improve the precision of
analysis of trace properties [10, 11]. The idea of these type-based analysis
approaches are to infer the type of a program which allows one to verify if
the program satisfies certain properties. However, the type inference
algorithms for the region type systems for Featherweight Java from the
previous work [5, 10, 11, 14] are _not_ compositional. The type of a method is
inferred from the ones of its arguments. If the method is called with
arguments of different types, its code is analyzed multiple times, one for
each invocation.

To avoid redundant analysis, we introduce a new inference algorithm based on
an abstract notion of environment transformation. The idea is to summarize the
flow information of the program using an abstract transformation. Then we
derive the type of a method by applying its abstract transformation to the
types of its arguments. When analyzing some new code which invokes some
methods that have been analyzed, we can use the abstract transformations
computed in the previous round of analysis, rather than re-analyzing the code
of the methods as in the previous work [5, 10, 11, 14]. We now explain the
idea in more detail.

##### Region Types and Typing Environments.

We work with the region type system of Beringer et al. [5] for Featherweight
Java [16]. But our approach can be adapted for other type systems. In our type
system, _region types_ represent some properties of values. For example, we
consider a region $\texttt{CreatedAt}\mathopen{}\left(\ell\right)\mathclose{}$
for references to objects that were created in the position with label $\ell$.
One can think of the label $\ell$ as a line number in the source code. This
region enables us to track where in the program an object originates. We allow
_typing environments_ to carry field typing. For example, the environment

$E=(x:\texttt{CreatedAt}\mathopen{}\left(\ell_{1}\right)\mathclose{},\
\texttt{CreatedAt}\mathopen{}\left(\ell_{1}\right)\mathclose{}.f:\texttt{CreatedAt}\mathopen{}\left(\ell_{2}\right)\mathclose{})$

means that $x$ points to an object which is created at position $\ell_{1}$ and
the field $f$ of any object created at $\ell_{1}$ is an object created at
$\ell_{2}$.

##### Environment Transformations.

Inferring region types is essentially a flow analysis. The execution of a
program may change the types of its variables and fields. Thus we want to
assign it an _environment transformation_ that captures how the types are
updated in the program. For example, the program

$\begin{array}[]{l}y=x.f;\\\ x=\texttt{new}^{\ell_{3}}\;C();\end{array}$

can be assigned the transformation

$[y:\mapsto x.f,\
x:\mapsto\texttt{CreatedAt}\mathopen{}\left(\ell_{3}\right)\mathclose{}].$

It updates the environment $E$ to

$(x:\texttt{CreatedAt}\mathopen{}\left(\ell_{3}\right)\mathclose{},\
y:\texttt{CreatedAt}\mathopen{}\left(\ell_{2}\right)\mathclose{},\
\texttt{CreatedAt}\mathopen{}\left(\ell_{1}\right)\mathclose{}.f:\texttt{CreatedAt}\mathopen{}\left(\ell_{2}\right)\mathclose{}).$

Note that the substitutions are performed simultaneously. If the program
returns the variable $x$, then we look it up in the above updated environment
and conclude that the program has return type
$\texttt{CreatedAt}\mathopen{}\left(\ell_{3}\right)\mathclose{}$, meaning that
it returns an object created at position $\ell_{3}$.

##### Field Access Graphs.

Directly using field access paths like $x.f$ in environments as above is
problematic, because the lengths of access paths may be unbounded. The
computation of environment transformations involving such access paths may not
terminate. For example, consider a class of linked lists with a field
$\texttt{next}:\texttt{Node}$ pointing to the next node. The following method
returns the last node of a list.

$\begin{array}[]{l}\texttt{Node}\ \texttt{last}()\ \\{\\\ \quad\mathtt{if}\
(\texttt{next}\ \mathtt{==}\ \texttt{null})\ \\{\mathtt{return}\
\texttt{this};\\}\\\ \quad\mathtt{else}\ \\{\mathtt{return}\
\texttt{next}.\texttt{last}();\\}\\\ \\}\end{array}$

Its return type can be the same as the type of variable this, or the types of
the paths $\texttt{this}.\texttt{next}$,
$\texttt{this}.\texttt{next}.\texttt{next}$ and so on, resulting in an
infinite set of access paths. To solve this, we work with _access graphs_
which provide a finite representation of access paths [18, 26]. For example,
the Node class has three access graphs to represent all its access paths. The
return type of last is then computed via the set containing these three
graphs.

##### Field Update and Constraints.

We work with _weak update_ for field typing as in [5]: If a field $f$ of some
object is assigned a value of type $B$, and in another occasion it is assigned
a value of type $C$, then the field should have a type containing both $B$ and
$C$. Therefore, for an assignment statement like $y.f=x$, we assign it a
_constraint_ $y.f:\geq x$, meaning that the type of the field $f$ of any
object of the type of $y$ should be greater than or equal to the type of $x$.

##### Abstract Transformations.

With the above ingredients, we introduce a notion of abstract transformation.
An _abstract transformation_ consists of assignments $x:\mapsto u$ and
constraints $\kappa:\geq v$. The value such as $u,v$ is a formal disjunction
of some atoms. An _atom_ is a variable, a type or a field graph following a
variable or a type. The key $\kappa$ is a non-empty graph representing access
paths. To capture how types are updated in a program, we define the following
operations on abstract transformations. We _instantiate_ an abstract
transformation to an endofunction on typing environments. It computes the
types of variables and fields of a program with a given initial typing. We
define the _composition_ of abstract transformations to model type updates in
a statement followed by another. We also define the _join_ of abstract
transformations to tackle conditional branches.

##### Type Inference.

Suppose we have a table $T$ assigning an abstract transformation to each
method of a program. Then we can compute an abstract transformation for any
expression $e$ of the program by induction on $e$. For example, when $e$ is an
invocation of a method, we lookup the table $T$ to get the abstract
transformation; and when $e$ is a conditional expression, we join the abstract
transformations of its branches. For any well-typed program, we have a fixed-
point algorithm to compute such a table $T$ for it. To infer the type of a
method, we find its abstract transformation from $T$, feed it with the
argument types, and then get the type of the return variable from the
resulting typing environment.

####  1.0.1 Related Work

Constraint-based analysis is a common technique for type inference with a rich
history [1, 2, 3, 21, 22, 27, 28, 29]. It may be divided into two main phases.
The first phase is to generate constraints by traversing the program. To
improve the efficiency of type inference, some simplification may be performed
on the generated constraints. Our computation of the table $T$ of abstract
transformations corresponds to constraint generation, where constraints are
simplified by the composition operation of abstract transformations. The
second phase is to solve the generated constraints. There are many different
constraint solvers. In our approach, we instantiate the abstract
transformations in $T$ to infer the type of the program, which corresponds to
constraint solving. Therefore, our approach is essentially a constraint-based
type inference algorithm. But it departs from the existing work in the
following aspects. We make use of constraints to infer region information of
the program rather than implementation types (i.e., sets of classes) [1, 22,
29]. Moreover, we work with access graphs for the constraint language to
guarantee the termination of our inference algorithm, rather than requiring an
additional termination test [27, 29].

Our approach is also closely related to the framework for Interprocedural
Distributive Environments (IDE) of Sagiv et al. [25]. The main idea of the IDE
framework is to reduce a program-analysis problem to a pure graph-reachability
problem. A user defines a set of environment transformers, that is,
endofunctions on environments describing the effect of a statement, and then
uses an IDE solver such as Heros [6, 23] to compute analysis results for the
entire program. In particular, IDE requires environment transformers to be
distributive: transforming the join of any environments gives the same result
of joining the transformed environments. We attempted to use IDE to infer
region types, but the environment transformer for statement such as $x=y.f$ is
not distributive, because it needs to access the input environment multiple
times in order to get the type of $y.f$. This failed attempt motivated us to
develop a symbolic representation of environment transformers for type
inference, resulting in our notion of abstract transformation.

##  2 Background

We briefly recall the definitions of Featherweight Java and access graphs.

###  2.1 Featherweight Java

We work with a variant of Featherweight Java (FJ) using the formulation of
[10]. It extends FJ [16] with field updates, and has primitive if- and let-
expressions for convenience. In the presence of field updates, we omit
constructors for simplicity.

The syntax of the language uses four kinds of names.

$\begin{array}[]{rlcrl}\text{variables: }&x,y\in\mathit{Var}&&\text{classes:
}&C,D\in\mathit{Cls}\\\ \text{fields: }&f\in\mathit{Fld}&&\text{methods:
}&m\in\mathit{Mtd}\end{array}$

Program expressions are defined as follows:

$\displaystyle\mathit{Expr}\ni e::=\ x$
$\displaystyle\,\mid\,\texttt{let}\;x=e_{1}\;\texttt{in}\;e_{2}\,\mid\,\texttt{if}\;x=y\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}$
$\displaystyle\,\mid\,\texttt{null}\,\mid\,\texttt{new}^{\ell}\;C\,\mid\,(C)\,e\,\mid\,x^{C}.m(\bar{y})\,\mid\,x^{C}.f\,\mid\,x^{C}.f:=y$

The expression $\texttt{new}^{\ell}\;C$ creates a new object of class $C$ with
all fields initiated to null. It is annotated with a label
$\ell\in\mathit{Pos}$. We use labels only to distinguish different occurrences
of $\mathtt{new}$ in a program, since our type system will track where objects
were created. In a few expressions we have added type annotations and write
$x^{C}$ for a variable of class $C$. They will be needed when looking up in
the class table. This is simpler than working with typed variable
declarations, since we do not need to find the declarations in order to get
the type of a variable. We sometimes omit annotations when they are not
needed.

We assume three distinguished formal elements:
$\texttt{Object},\texttt{NullType}\in\mathit{Cls}$ and
$\texttt{this}\in\mathit{Var}$. The NullType class plays the role of the type
of null from the Java language specification [13, §4]. It may not be used in
programs, i.e. we require $C\not=\texttt{NullType}$ in create expression
$\texttt{new}^{\ell}\;C$ and casting expression $(C)\,e$. When $x$ is not a
free variable of $e_{2}$, we may write $e_{1};e_{2}$ rather than
$\texttt{let}\;x=e_{1}\;\texttt{in}\;e_{2}$.

An FJ program $(\prec,\mathit{fields},\mathit{methods},\mathit{mtable})$
consists of

  * •

a subtyping relation
${\prec}\in\mathcal{P}^{\text{fin}}(\mathit{Cls}\times\mathit{Cls})$ with
$C\prec D$ meaning that $C$ is an immediate subclass of $D$,

  * •

a field list
$\mathit{fields}:\mathit{Cls}\to\mathcal{P}^{\text{fin}}(\mathit{Fld})$
mapping a class to its fields,

  * •

a method list
$\mathit{methods}:\mathit{Cls}\to\mathcal{P}^{\text{fin}}(\mathit{Mtd})$
mapping a class to its methods,

  * •

a method table
$\mathit{mtable}:\mathit{Cls}\times\mathit{Mtd}\rightharpoonup\mathit{Var}^{*}\times\mathit{Expr}$
mapping a method to the pair of its formal parameters and its body.

All components are required to be well-formed. We refer the reader to e.g.
[10, Section 3] for details. Let $\preceq$ be the reflexive and transitive
closure of $\prec$. Then we have $C\preceq\texttt{Object}$ and
$\texttt{NullType}\preceq C$ for any class $C\in\mathit{Cls}$.

In the standard FJ type system [16], types are simply classes. In the rest of
this paper, we consider only FJ programs that are well-typed with respect to
the standard FJ type system.

###  2.2 Access Graphs

For recursive data types such as linked lists, the lengths of access paths may
be unbounded. If environment transformations are defined upon access paths,
their computation may not terminate. In this paper, we choose to work with the
finite representation of access paths given by access graphs [18, 26] among
the others [9, 17, 19].

An _access graph_ $x.G$ consists of a local variable $x$, called its _base_ ,
and a field graph $G$. A _field graph_ is a directed graph whose nodes are
fields. The empty field graph is denoted by $\mathcal{E}$. The access graph
$x.\mathcal{E}$ represents the plain variable $x$. Thus we often omit the
empty field graph $\mathcal{E}$ and simply write $x$. If a field graph is not
empty, it has a head node $h\in\mathit{Fld}$ and a tail node
$t\in\mathit{Fld}$ such that for each node $n\in\mathit{Fld}$ within the field
graph there exists a path from $h$ to $t$ passing through $n$. Note that the
head and tail can be the same. A non-empty field graph can be uniquely
identified by its head $h$, tail $t$ and edge set
$E\subseteq\mathit{Fld}\times\mathit{Fld}$; thus, we write $\langle
h,E,t\rangle$ to denote it. Each access graph $x.\langle h,E,t\rangle$
represents the set of access paths obtained by traversing the field graph from
the head to the tail. We write $\mathcal{F}$ to denote the set of field graphs
and use $G,G^{\prime}$ to range over field graphs in the paper.

###### Example 1

Consider the following access graphs for a class of nodes for linked lists.
The field $v$ is the value stored in the current node and the field $n$ points
to the next node.

(1) $x$(2) $x$$v$(3) $x$$n$$v$

In the above diagrams, each bold circle represents a tail. These access graphs
represent access paths as explained below:

  1. (1)

$x.\mathcal{E}$ represents the variable $x$.

  2. (2)

$x.\langle v,\emptyset,v\rangle$ represents the path $x.v$.

  3. (3)

$x.\langle n,\\{(n,n),(n,v)\\},v\rangle$ represents the paths $x.n.v$,
$x.n.n.v$ and so on. ∎

Given any two field graphs $G$ and $G^{\prime}$, we _concatenate_ them and
obtain a field graph $G.G^{\prime}\in\mathcal{F}$ as follows:

$\displaystyle G.\mathcal{E}$ $\displaystyle:=G$
$\displaystyle\mathcal{E}.G^{\prime}$ $\displaystyle:=G^{\prime}$
$\displaystyle\langle h,E,t\rangle.\langle
h^{\prime},E^{\prime},t^{\prime}\rangle$ $\displaystyle:=\langle
h,E\cup\\{(t,h^{\prime})\\}\cup E^{\prime},t^{\prime}\rangle.$

Intuitively, the concatenation of a path in $G$ with one in $G^{\prime}$ lives
in $G.G^{\prime}$. This operation is needed for defining composition of
environment transformations.

We work with a generalization of access graphs $b.G$ where $b$ can be either a
variable or a type in order to model field typing as explained in Session 3.2.

##  3 A Theory of Abstract Transformations

Our idea is to type a program via environment transformations. Consider the
simple example given in Fig. 1. Each statement of the program is assigned an
environment transformation. They are composed into an environment
transformation $\sigma$ for the whole program. For any given initial typing
environment $\mathit{env}$, we obtain the updated environment
$\sigma(\mathit{env})$ containing the typing information after executing the
program. Lastly, we get the return type of the program from the updated typing
environment $\sigma(\mathit{env})$. In this section, we explain what
environment transformations are and how they update typing environments.

`x = y.f;` `y = new C();` `y.f = x` $[x:\mapsto y.f]$ $[y:\mapsto C]$
$[y.f:\geq x]$ $\sigma=[x:\mapsto y.f,\,y:\mapsto C,\,C.f:\geq y.f]$
$\mathit{env}=(y:A,\,A.f:B)$
$\sigma(\mathit{env})=(x:B,\,y:C,\,A.f:B,\,C.f:B)$ Figure 1: An example
illustrating the idea of typing via environment transformations

This section is organized as follows. Section 3.1 presents the assumptions and
definitions of types and typing environments. Section 3.2 introduces our
abstract notion of environment transformation which is based on access graphs.
Lastly, Section 3.3 demonstrates some operations on abstract transformations
which are essential for modeling the type updates of the program.

###  3.1 Types and Environments

We use abstract transformations to encode the changes of types in the program.
But our approach is general and works for various type systems including those
in the previous work [5, 14, 10, 11]. We target at flow type systems in the
spirit of Microsoft’s TypeScript [20] and Facebook’s Flow [12], rather than
the standard FJ typing [16]. We leave the notion of type generic in this
section. For instance, when working with classes, our approach can infer
implementation types [1, 22, 29]. In the next section, we work with region
types to present a new algorithm for inferring region information using
abstract transformations.

In this section, we assume a finite set $\mathit{Typ}$ of atomic _types_ and
use $A,B,C$ to range over atomic types. In addition, we assume a set
$\mathit{Cls}(A)\subseteq\mathit{Cls}$ of actual classes of an object of type
$A$. This allows us to get the set $\mathit{Fld}(A)\subseteq\mathit{Fld}$ of
fields of (objects of) type $A$. We write $A.f$ to denote the field
$f\in\mathit{Fld}(A)$.

We consider the field typing as a part of an environment; thus, a typing
_environment_ is a mapping
$\mathit{Var}\cup\mathit{Typ}\times\mathit{Fld}\rightharpoonup\mathcal{P}(\mathit{Typ})$
that assigns a variable or a field its possible types. We work with a partial
order $\sqsubseteq$ on environments given by
$\mathit{env}\sqsubseteq\mathit{env}^{\prime}$ iff
$\mathit{env}(\kappa)\subseteq\mathit{env}^{\prime}(\kappa)$ for all
$\kappa\in\mathrm{dom}(\mathit{env})$. Given an environment $\mathit{env}$, we
write
$\mathit{env}|_{\mathrm{v}}:\mathit{Var}\rightharpoonup\mathcal{P}(\mathit{Typ})$
and
$\mathit{env}|_{\mathrm{f}}:\mathit{Typ}\times\mathit{Fld}\rightharpoonup\mathcal{P}(\mathit{Typ})$
to denote the typings of variables and fields of $\mathit{env}$ respectively.
Given a variable typing
$V:\mathit{Var}\rightharpoonup\mathcal{P}(\mathit{Typ})$ and a field typing
$F:\mathit{Typ}\times\mathit{Fld}\rightharpoonup\mathcal{P}(\mathit{Typ})$, we
write $(V,F)$ to denote the environment combining the typings from $V$ and
$F$. In particular, we have
$\mathit{env}=(\mathit{env}|_{\mathrm{v}},\mathit{env}|_{\mathrm{f}})$.

We often call a set of atomic types a _type_. We simply write $A$ to denote
the singleton set $\\{A\\}$ and misuse the disjunction symbol $\vee$ for set
unions. The set $\\{A,B,C\\}$ for example is thus denoted as $A\vee B\vee C$.
In particular, we write $\bot$ to denote the empty set of atomic types. For
instance, $(x:A,\ A.f:B\vee C)$ is an environment stating that the variable
$x$ has type $A$ and the field $f$ of any object of type $A$ can have type $B$
or $C$.

###  3.2 Abstract Transformations

Now we define our notion of abstract transformation which encodes type updates
of the variables and fields of a program.

When assigning transformations to statements in the program, the interesting
cases are the assignment statements. Consider a statement $x=e$ and its
following possible transformations:

  * •

If $e$ is a constant of type $A$, then the resulting transformation is
$[x:\mapsto A]$, meaning that the type of $x$ is $A$.

  * •

If $e$ is a variable $y$ whose type is unknown yet, then the resulting
transformation is $[x:\mapsto y]$, meaning that $x$ has the same type as $y$.

  * •

If $e$ is a field $y.f$ and the type of $y$ is known to be $A$, then the
resulting transformation is $[x:\mapsto A.f]$, meaning that $x$ has the same
type as the field $f$ of any object of type $A$.

  * •

If $e$ is a field $y.f$ and the type of $y$ is unknown, then the resulting
transformation is $[x:\mapsto y.f]$, meaning that $x$ has the same type as the
field $f$ of any object of the type of $y$.

The above cases list four _atomic_ kinds of assignment values: atomic type
$A$, variable $y$, fields $A.f$ and $y.f$ of a type and a variable. As
discussed earlier, we work with access graphs instead of access paths to avoid
non-terminating computation. All of above assignment values can be represented
using a generalization $b.G$ of access graphs where the base $b$ can also be a
type. For instance, the type $A$ is represented by $A.\mathcal{E}$ where
$\mathcal{E}$ is the empty field graph, and the field $A.f$ is represented by
$A.\langle f,\emptyset,f\rangle$. We consider one more possible case of $e$:

  * •

If $e$ involves some branches and thus has type $B\vee C$, then $x=e$ results
in a transformation $[x:\mapsto B\vee C]$, meaning that $x$ has type $B$ or
$C$.

More generally, the value $v$ of an assignment $x:\mapsto v$ can be the
‘formal disjunction’ of some access graphs $b.G$. These cases bring the
following definition of terms to represent assignment values.

######  Definition 1 (Atoms and terms)

_Atoms_ are a generalization of access graphs whose base is either a variable
or an atomic type. We write $b.G$ to denote the atom with base
$b\in\mathit{Var}\cup\mathit{Typ}$ and field graph $G\in\mathcal{F}$.

A _term_ is simply a set (or a formal disjunction) of atoms. We write $\bot$
to denote the empty term, i.e., the empty set of atoms, and $u\vee v$ to
denote the join of terms $u$ and $v$, i.e., the union of the two sets $u,v$ of
atoms. Therefore, we have $u\vee\bot=u=\bot\vee u$ for any term $u$.

When the field graph $G$ is empty, the atom $b.G$ represents a variable or an
atomic type. Thus we often omit $G$ and simply write $b$ to denote the atom.
If $G=\langle f,\emptyset,f\rangle$, that is, a graph consisting of only the
singleton field access path $f$, then we may write $b.f$ rather than
$b.\langle f,\emptyset,f\rangle$.

By definition, each term $u$ has the form $\bigvee^{n}_{i=1}b_{i}.G_{i}$ where
$u=\bot$ if $n=0$. We _concatenate_ a term $u$ with a field graph $G$ by

$\textstyle
u.G=(\bigvee^{n}_{i=1}b_{i}.G_{i}).G=\bigvee^{n}_{i=1}b_{i}.(G_{i}.G)$

where the concatenation $G_{i}.G$ of field graphs has been defined in Section
2.2.

A term is a formal expression that can be instantiated into a concrete type
with a given typing environment (see Definition 6). We denote the set of terms
by Tm and use $u,v,w$ to range over terms.

######  Definition 2 (Assignments)

An _assignment_ is a pair consists of a variable $x$ and a term $u$, written
as $x:\mapsto u$. It means that the type of variable $x$ is the instantiation
of the term $u$ w.r.t. any typing environment. We call $x$ the _key_ of the
assignment.

We want a notion of environment transformation that encodes also the update of
field typing. In particular, we choose to work with _weak update_ for field
typing as in the previous work [5, 10, 11, 14]: If a field $f$ of an object of
type $A$ is assigned a value of type $B$ and $f$ of another object of the same
type $A$ is assigned a value of type $C$, then the field $A.f$ of any object
of type $A$ should have a type containing both $B$ and $C$. Therefore, for a
statement like $y.f=x$, we cannot give it the assignment $y.f:\mapsto x$ as it
expresses that $y.f$ has the same type of $x$. Instead, we assign it a
constraint $y.f:\geq x$, meaning that the type of the field $f$ of any object
of the type of $y$ should be greater than or equal to the type of $x$. If $y$
has type $A$, then the constraint becomes $A.f:\geq x$. More generally, we
define constraints as follows.

######  Definition 3 (Constraints)

A _constraint_ is a pair consisting of a nonempty access graph $b.G$ and a
term $u$, written as $b.G:\geq u$. It means that the type of any field
reachable via some path of $b.G$ is greater than or equal to the instantiation
of the term $u$ w.r.t. any typing environment. We call $b.G$ the key of the
constraint.

Abstract transformations consists of assignments and/or constraints.

######  Definition 4 (Abstract transformations)

An _abstract transformation_

$[x_{1}:\mapsto u_{1},\ldots,x_{n}:\mapsto u_{n},\,\kappa_{1}:\geq
v_{1},\ldots,\kappa_{m}:\geq v_{m}]$

is a finite set consisting of assignments $x_{i}:\mapsto u_{i}$ and
constraints $\kappa_{j}:\geq v_{j}$ such that all the keys are different and
$x_{i}\not=u_{i}$ for all $i\in\\{1,\ldots,n\\}$ and $v_{j}\not=\bot$ for all
$j\in\\{1,\ldots,m\\}$. Let $\sigma$ be the above abstract transformation. We
write $\mathrm{dom}(\sigma)$ to denote its _domain_ , that is, the set of keys
$\\{x_{1},\ldots,x_{n},\,\kappa_{1},\ldots,\kappa_{m}\\}$.

Let $\mathcal{K}$ be the set of _keys_ , that is, variables and nonempty
access graphs. Each abstract transformation $\sigma$ is a representation of a
total function from $\mathcal{K}$ to Tm

$\displaystyle\sigma(x)$ $\displaystyle:=\begin{cases}u&\text{if }(x:\mapsto
u)\in\sigma\\\ x&\text{if }x\not\in\mathrm{dom}(\sigma)\end{cases}$
$\displaystyle\sigma(\kappa)$ $\displaystyle:=\begin{cases}v&\text{if
}(\kappa:\geq v)\in\sigma\\\ \bot&\text{if
}\kappa\not\in\mathrm{dom}(\sigma).\end{cases}$

In other words, identity assignments $x:\mapsto x$ and bottom constraints
$\kappa:\geq\bot$ are omitted in abstract transformations. This is because
they add no information to the transformations. For instance, if a
transformation contains only identity assignments and bottom constraints, then
it is instantiated into the identity function on typing environments according
to Definition 7.

We write ATrans to denote the set of abstract transformations and use
$\sigma,\theta$ to range over abstract transformations in the paper. The empty
transformation is denoted as $[]$, and the one consisting of only bottom
assignments $x:\mapsto\bot$ for all variable $x$ is denoted as $\bot$. As will
become clear, $[]$ is the identity environment transformation and $\bot$ the
‘least’ environment transformation.

###### Example 2

Consider again the example in Fig. 1. The program

$\verb|x = y.f; y = new C(); y.f = x|$

results in the transformation

$[x:\mapsto y.f,\,y:\mapsto C,\,C.f:\geq y.f].$

For `x = y.f`, the type of $\mathtt{y}$ is not known yet and thus it leads to
the assignment $x:\mapsto y.f$. In this example, we assume that the type of
$\mathtt{new\ C()}$ is some type $C$ which can be different from class
$\mathtt{C}$. Thus $\verb|y = new C()|$ leads to $y:\mapsto C$. The last
statement $\verb|y.f = x|$ by itself results in the constraint $y.f:\geq x$.
But because of $x:\mapsto y.f$ and $y:\mapsto C$, the constraint is updated to
$C.f:\geq y.f$ by substituting $y$ in the key $y.f$ by $C$ and the constraint
value $x$ by $y.f$. In Section 0.A we will demonstrate how to compose
$[x:\mapsto y.f]$, $[y:\mapsto C]$ and $[y.f:\geq x]$ to get $[x:\mapsto
y.f,\,y:\mapsto C,\,C.f:\geq y.f]$. ∎

###  3.3 Operations on Abstract Transformations

Consider again the example from Fig. 1. In this section, we firstly
demonstrate how the transformation $\sigma=[x:\mapsto y.f,\,y:\mapsto
C,\,C.f:\geq y.f]$ updates the environment $\mathit{env}=(y:A,\,A.f:B)$ to
$\sigma(\mathit{env})=(x:B,\,y:C,\,A.f:B,\,C.f:B)$. Then we show that abstract
transformations can be composed and joined so that we can construct the
transformation $\sigma$ for the program from those of its statements.

To begin with, we look into how the type of $x$ is computed in
$\sigma(\mathit{env})$. There is an assignment $x:\mapsto y.f$ in $\sigma$,
meaning that $x$ has the same type as $y.f$. We have to instantiate the term
$y.f$ using the typing information given by the input environment
$\mathit{env}$. Because $y$ has type $A$ in $\mathit{env}$, we instantiate
$y.f$ to $A.f$. And because $A.f$ has type $B$ in $\mathit{env}$, we
instantiate $y.f$ further to $B$. Therefore, $x$ has type $B$ in the updated
environment $\sigma(\mathit{env})$.

We have seen from the above example that we need to instantiate a term to a
type according to the environment which we want to update. In particular, we
consider how to instantiate an atom $A.\langle h,E,t\rangle$. For example, let
us instantiate $A.f.g$ according to $(A.f:A\vee B,\,B.g:C,\,C.g:D)$. The goal
is to compute the type of the field $g$ of $A.f$. Which field in the
environment should be considered, $B.g$ or $C.g$? Because $A.f$ can have type
$A$ or $B$, we can _reach_ the field $B.g$ but not $C.g$. Therefore, we should
instantiate $A.f.g$ only to $C$, i.e., the type of $B.g$.

In the following, we describe how to compute the _reachable fields_ from a
field $A.h$ via an edge set $E$ according to the field typing in an
environment $\mathit{env}$. Then, to instantiate $A.\langle h,E,t\rangle$
w.r.t. $\mathit{env}$, we simply join the types of all fields $B.t$ in
$\mathit{env}$ which are reachable from $A.h$.

######  Definition 5 (Reachable fields)

Let $A$ be an atomic type, $h$ a field, $E$ an edge set and $\mathit{env}$ an
environment. We construct the set
$\mathcal{R}(A.h,E,\mathit{env})\subseteq\mathit{Typ}\times\mathit{Fld}$ of
_reachable fields_ from $A.h$ via $E$ according to $\mathit{env}$ as follows:

  * (1)

Let $\mathcal{R}(A.h,E,\mathit{env})=\\{A.h\\}$.

  * (2)

For each $B.f\in\mathcal{R}(A.h,E,\mathit{env})$, let
$\mathcal{R}(A.h,E,\mathit{env})=\mathcal{R}(A.h,E,\mathit{env})\cup\mathcal{S}_{B.f}$,
where $\mathcal{S}_{B.f}$ is the set of _immediate successors_ of $B.f$
defined by

$\mathcal{S}_{B.f}:=\\{C.g\mid C\in\mathit{env}(B.f)\text{ and }(f,g)\in
E\text{ and }g\in\mathit{Fld}(C)\\}.$

  * (3)

Repeat (2) until $\mathcal{R}(A.h,E,\mathit{env})$ cannot be updated anymore.

Any field $A.f$ is reachable from itself. To compute the other reachable
fields from $A.f$, the above algorithm simply gets the immediate successors of
$A.f$, and then those of the immediate successors and so on.

###### Example 3

Let $\mathit{env}=(A.f:A\vee B,\,B.g:C)$ and assume
$\mathit{Fld}(A)=\\{f,g\\}$ and $\mathit{Fld}(B)=\\{g\\}$. By definition, we
have

$\mathcal{R}(A.f,\emptyset,\mathit{env})=\\{A.f\\}$

because the edge set is empty and thus $f$ has no successors. We have

$\mathcal{R}(A.f,\\{(f,g)\\},\mathit{env})=\\{A.f,A.g,B.g\\}$

indicating that $A.g$ and $B.g$ are also reachable from $A.f$. That’s because
$g$ is a successor of $f$ and $g$ is a field of both $A$ and $B$. ∎

The instantiation $(A.\langle
h,E,t\rangle)[\mathit{env}]\subseteq\mathit{Typ}$ is given by the join of
$\mathit{env}(B.t)$ for all reachable fields
$B.t\in\mathcal{R}(A.h,E,\mathit{env})$. With this, we can instantiate
arbitrary atoms and thus terms.

######  Definition 6 (Instantiation of terms)

Let $\mathit{env}$ be an environment. We define the _instantiation_
$(b.G)[\mathit{env}]\subseteq\mathit{Typ}$ of atom $b.G$ as follows:

$\displaystyle A[\mathit{env}]$ $\displaystyle:=A$ $\displaystyle(A.\langle
h,E,t\rangle)[\mathit{env}]$
$\displaystyle:=\textstyle\bigvee\left\\{\mathit{env}(B.t)\mid
B.t\in\mathcal{R}(A.h,E,\mathit{env})\right\\}$
$\displaystyle(x.G)[\mathit{env}]$
$\displaystyle:=\textstyle\bigvee\left\\{(A.G)[\mathit{env}]\mid
A\in\mathit{env}(x)\right\\}.$

The instantiation of a term $u$ is the join of the instantiations of its
atoms, i.e.,

$\textstyle
u[\mathit{env}]=(\bigvee^{n}_{i=1}b_{i}.G_{i})[\mathit{env}]:=\bigvee^{n}_{i=1}(b_{i}.G_{i})[\mathit{env}].$

In the above definition, we assume that if
$a\not\in\mathrm{dom}(\mathit{env})$ then $\mathit{env}(a)=\bot$, that is, the
empty set of types, where $a$ is a variable $x$ or a field $A.f$. Therefore,
we have $x[\mathit{env}]=\mathit{env}(x)$ and
$(A.f)[\mathit{env}]=\mathit{env}(A.f)$.

###### Example 4

Let $\mathit{env}=(A.f:A\vee B,\,B.g:C)$ and assume
$\mathit{Fld}(A)=\\{f,g\\}$ and $\mathit{Fld}(B)=\\{g\\}$ as in Example 3. By
definition, we have

$(A.f)[\mathit{env}]=\mathit{env}(A.f)=A\vee B$

and

$\displaystyle(A.f.g)[\mathit{env}]$ $\displaystyle=(A.\langle
f,\\{(f,g)\\},g\rangle)[\mathit{env}]$
$\displaystyle=\textstyle\bigvee\\{\mathit{env}(X.g)\mid
X.g\in\mathcal{R}(A.f,\\{(f,g)\\},\mathit{env})\\}$
$\displaystyle=\mathit{env}(A.g)\vee\mathit{env}(B.g)$ $\displaystyle=\bot\vee
C=C$

because from Example 3 we know both $A.g$ and $B.g$ are reachable from $A.f$.
∎

Lastly, we instantiate abstract transformations to endofunctions on typing
environments. The type of a variable is computed by instantiated the its
assigned term in the transformation, as discussed above. To compute the types
of fields, we solve the constraints using a fixed-point algorithm.

######  Definition 7 (Instantiation of abstract transformations)

Let $\sigma$ be an abstract transformation. We define an endofunction
$\varphi_{\sigma}$ on environments by

$\displaystyle\varphi_{\sigma}(\mathit{env})(x)$
$\displaystyle:=\begin{cases}u[\mathit{env}]&\text{if }(x:\mapsto
u)\in\sigma\\\ \mathit{env}(x)&\text{otherwise}\end{cases}$
$\displaystyle\varphi_{\sigma}(\mathit{env})(A.f)$
$\displaystyle:=\mathit{env}(A.f)\vee\textstyle\bigvee\\{u[\mathit{env}]\mid(b.\langle
h,E,f\rangle:\geq u)\in\sigma\text{ and }$ $\displaystyle\hskip 116.0ptB\in
b[\mathit{env}]\text{ and }A.f\in\mathcal{R}(B.h,E,\mathit{env})\\}.$

Let $\mathit{env}$ be an environment. We define an environment
$\sigma(\mathit{env})$ by

  1. 1.

Let $\mathit{env}^{\prime}=\mathit{env}$.

  2. 2.

Let
$\mathit{env}^{\prime\prime}=\varphi_{\sigma}(\mathit{env}|_{\mathrm{v}},\mathit{env}^{\prime}|_{\mathrm{f}})$,
where $(\mathit{env}|_{\mathrm{v}},\mathit{env}^{\prime}|_{\mathrm{f}})$ is
the environment obtained by combining the variable typing of $\mathit{env}$
and the field typing of $\mathit{env}^{\prime}$.

  3. 3.

If $\mathit{env}^{\prime}\not=\mathit{env}^{\prime\prime}$, then let
$\mathit{env}^{\prime}=\mathit{env}^{\prime\prime}$ and go back to Step 2.
Otherwise, let $\sigma(\mathit{env})=\mathit{env}^{\prime}$.

This procedure results in an environment transformation mapping $\mathit{env}$
to $\sigma(\mathit{env})$.

To instantiate an abstract transformation $\sigma$, we use the above fixed-
point algorithm to solve the constraints for field typings in $\sigma$. What
crucial is the function $\varphi_{\sigma}$ that updates the environment in
each iteration towards the fixed point. If $(x:\mapsto u)\in\sigma$, then
$\varphi_{\sigma}(\mathit{env})$ assigns $x$ to the instantiation
$u[\mathit{env}]$; otherwise, $x$ is assigned the type as claimed in
$\mathit{env}$. Because of weak update for field typing,
$\varphi_{\sigma}(\mathit{env})$ assigns a field $A.f$ to the join containing
its previous type $\mathit{env}(A.f)$ given by the environment and the
instantiations of constraint values from whose keys the field $A.f$ can reach.

Note that, in each iteration towards the fixed point, the input of
$\varphi_{\sigma}$ consists of the variable typing
$\mathit{env}|_{\mathrm{v}}$ from the original environment $\mathit{env}$ and
the field typing $\mathit{env}^{\prime}|_{\mathrm{f}}$ from the result
$\mathit{env}^{\prime}$ of the previous iteration. This is because types of
variables and of fields are updated in different manners. We ‘accumulate’ the
field typing by feeding $\varphi_{\sigma}$ with the field typing from the
previous iteration due to weak update as explained earlier. However, variable
typing is not updated in this way. For instance, consider the code `x = y; y =
new C()`, resulting in the transformation $\sigma=[x:\mapsto y,\,y:\mapsto
C]$, and the environment $\mathit{env}=(y:A)$. We have
$\varphi_{\sigma}(\mathit{env})=(x:A,\,y:C)$ which gives the correct type to
$x$, because $x$ should have the same type of $y$ before the assignment `y =
new C()` which is $A$. But applying $\varphi_{\sigma}$ to the updated
environment would give $x$ type $C$.

By definition, the empty transformation $[]$ is identity on environments. For
a more interesting example, we consider the transformation from Fig. 1.

###### Example 5

Recall the abstract transformation from Fig. 1:

$\sigma=[x:\mapsto y.f,\,y:\mapsto C,\,C.f:\geq y.f].$

Let $\mathit{env}=(y:A,\,A.f:B)$. The variables and fields that should appear
in the updated environment $\sigma(\mathit{env})$ consist of $x$, $y$, $A.f$
and $C.f$. By definition, we have

$\displaystyle\varphi_{\sigma}(\mathit{env})(x)$
$\displaystyle=(y.f)[\mathit{env}]=B$
$\displaystyle\varphi_{\sigma}(\mathit{env})(y)$
$\displaystyle=C[\mathit{env}]=C$
$\displaystyle\varphi_{\sigma}(\mathit{env})(A.f)$
$\displaystyle=\mathit{env}(A.f)\vee\bot=B$
$\displaystyle\varphi_{\sigma}(\mathit{env})(C.f)$
$\displaystyle=\mathit{env}(C.f)\vee(y.f)[\mathit{env}]=\bot\vee B=B.$

Because
$\varphi_{\sigma}(\mathit{env})=\varphi_{\sigma}(\mathit{env}|_{\mathrm{v}},\varphi_{\sigma}(\mathit{env})|_{\mathrm{f}})$,
we reach the fixed point and get the updated environment
$\sigma(\mathit{env})=\varphi_{\sigma}(\mathit{env})=(x:B,\,y:C,\,A.f:B,\,C.f:B)$.
∎

As explained in the next section, each statement of a program can be assigned
a transformation indicating the assignment or constraint of the involved type.
To combine them into one transformation that summarizes the type updates of
the whole program, the operations of composition and join for transformations
are needed. Due to the lack of space, we characterize these operations in the
following theorems. Details of their (non-surprising) constructions are
available in Appendix 0.A.

######  Theorem 3.1 (Composition of abstract transformations)

For any abstract transformations $\sigma$ and $\theta$, we can construct an
abstract transformation $\delta$ such that
$\sigma(\theta(\mathit{env}))\sqsubseteq\delta(\mathit{env})$. We write
$\sigma\theta$ to denote $\delta$ and call it the _composition_ of $\sigma$
and $\theta$. Moreover, we have $\sigma[]=\sigma=[]\sigma$ for any
transformation $\sigma$, where $[]$ is the empty transformation. ∎

The difficult part of the work is to come up with the right notion of abstract
transformation that supports composition. But the construction of composition
and its correctness are then straightforward. The idea to compose our abstract
transformations is similar to the one for substitutions (see e.g. [4, §2.1]).
And its correctness can be proved with a standard inductive argument on the
length of the abstract transformation.

Note that we have only
$\sigma(\theta(\mathit{env}))\sqsubseteq(\sigma\theta)(\mathit{env})$ where
$\sqsubseteq$ is the ordering on environments defined pointwisely. This is
because $\sigma\theta$ involves concatenation of field graphs which causes the
over approximation. For instance, concatenating a singleton path $f$ with
itself does not give the path $f.f$. Instead it results in the field graph
$\langle f,\\{(f,f)\\},f\rangle$ which represents all the paths consisting of
$f$ with length greater than 1. However, the type inference algorithm
presented in next section is still sound. It may give a less precise type to
the program.

######  Theorem 3.2 (Join of abstract transformations)

For any abstract transformations $\sigma$ and $\theta$, we can construct an
abstract transformation $\delta$ such that
$\sigma(\mathit{env})\sqcup\theta(\mathit{env})\sqsubseteq\delta(\mathit{env})$.
We write $\sigma\vee\theta$ to denote $\delta$ and call it the _join_ of
$\sigma$ and $\theta$. Moreover, we have $\sigma\vee\theta=\theta\vee\sigma$
and $\sigma\vee\bot=\sigma$ for all $\sigma$ and $\theta$, where $\bot$ is the
bottom transformation that assigns all variables to the bottom type. ∎

The join $\sigma\vee\theta$ is constructed componentwise using the join
operator on terms. It does not preserve fixed points and we have only
$\sigma(\mathit{env})\sqcup\theta(\mathit{env})\sqsubseteq(\sigma\vee\theta)(\mathit{env})$.
As discussed above, this causes no harm to the soundness of the type
inference.

##  4 Type Inference via Abstract Transformations

In this section, we demonstrate how to infer the type of an FJ program using
abstract transformations. The idea is to use abstract transformations to
capture the flow information of a program, which leads to a more efficient
type inference algorithm. As an example, we work with the region type system
of Beringer et al. [5]. Our inference algorithm firstly computes an abstract
transformation for each method of the program, and then uses them for the type
inference rather than analyzing the method bodies.

###  4.1 Region Type System

We briefly recall the region type system of Beringer et al. [5].

A _region_ represents a property of a value such as its provenance
information. In this paper, we use the following definition of regions:

$\displaystyle\mathit{Reg}\ni r,s\ ::=\
\texttt{Null}\,\mid\,\texttt{CreatedAt}\mathopen{}\left(\ell\right)\mathclose{}$

The region Null contains only the value $\mathit{null}$. The region
$\texttt{CreatedAt}\mathopen{}\left(\ell\right)\mathclose{}$ contains all
references to objects that were created by an expression of the form
$\texttt{new}^{\ell}\;C$. This region allows us to track where in the program
an object originates. One can use a richer definition of regions to capture
other properties of interest such as taintedness [10]. We keep it simple here
because we focus on the type inference.

Region type information is complementary to FJ type information and can be
captured without repeating the FJ type system. Therefore, we directly work
with region types rather than refining FJ types as in the original system [5,
Section 3].

As for FJ, we need a class table to record the region types of methods and
fields. This is needed to formulate typing rules for method call and field
access. A _class table_ $(F,M)$ consists of

  * •

a _field typing_
$F:\mathit{Cls}\times\mathit{Reg}\times\mathit{Fld}\rightharpoonup\mathcal{P}(\mathit{Reg})$
that assigns to each class $C$, region $r$ and field $f\in\mathit{fields}(C)$
a set $F(C,r,f)$ of regions of the field $f$, and

  * •

a _method typing_
$M:\mathit{Cls}\times\mathit{Reg}\times\mathit{Mtd}\times\mathit{Reg}^{*}\rightharpoonup\mathcal{P}(\mathit{Reg})$
that assigns to each class $C$, region $r$, method
$m\in\mathit{methods}\left(C\right)$ and sequence $\bar{s}$ of regions of
$m$’s formal arguments a set $M(C,r,m,\bar{s})$ of regions of the method $m$.

The typing functions are required to be well-formed, which reflects the
subtyping properties of FJ. See [11, Definition 4.2] for the details.

Typing judgments take the form $\Gamma\vdash e:R$, where
$\Gamma:\mathit{Var}\rightharpoonup\mathit{Reg}$ is a typing environment for
variables, $e\in\mathit{Expr}$ a term expression and $R\subseteq\mathit{Reg}$
a set of regions. The typing rules are listed in Figure 2. For instance, the
call rule looks up the method typing $M$ for all possible regions where the
object $x$ and arguments $\bar{y}$ may reside and joins the matched entries as
the return type of the method invocation $x.m(\bar{y})$.

$\inferrule*[left={var}]{}{\Gamma,\,x{:}\,R\vdash
x:R}\qquad\inferrule*[left={null}]{}{\Gamma\vdash\texttt{null}:\texttt{Null}}\qquad\inferrule*[left={new}]{}{\Gamma\vdash\texttt{new}^{\ell}\;C:\texttt{CreatedAt}\mathopen{}\left(\ell\right)\mathclose{}}$

$\inferrule*[left={sub}]{\Gamma\vdash e:R\\\ R\subseteq
R^{\prime}}{\Gamma\vdash
e:R^{\prime}}\qquad\inferrule*[left={cast}]{\Gamma\vdash
e:R}{\Gamma\vdash(D)\,e:R}$

$\inferrule*[left={if}]{\Gamma,\,x{:}\,R\cap S,\,y{:}\,R\cap S\vdash
e_{1}:T_{1}\\\ \Gamma,\,x{:}\,R,\,y{:}\,S\vdash
e_{2}:T_{2}}{\Gamma,\,x{:}\,R,\,y{:}\,S\vdash\texttt{if}\;x=y\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}:T_{1}\cup
T_{2}}$

$\inferrule*[left={let}]{\Gamma\vdash e_{1}:R\\\ \Gamma,\,x{:}\,R\vdash
e_{2}:T}{\Gamma\vdash\texttt{let}\;x=e_{1}\;\texttt{in}\;e_{2}:T}\qquad\inferrule*[left={call}]{\textstyle
T=\bigcup\\{M(C,r,m,\bar{s})\mid r\in
R,\bar{s}\in\bar{S}\\}}{\Gamma,\,x{:}\,R,\,\bar{y}{:}\,\bar{S}\vdash
x^{C}.m(\bar{y}):T}$

$\inferrule*[left={get}]{\textstyle T=\bigcup\\{F(C,r,f)\mid r\in
R\\}}{\Gamma,\,x{:}\,R\vdash x^{C}.f:T}\qquad\inferrule*[left={set}]{\forall
r\,\mathord{\in}\,R.\ S\subseteq F(C,r,f)}{\Gamma,\,x{:}\,R,\,y{:}\,S\vdash
x^{C}.f:=y:S}$

Figure 2: The region type system of Beringer et al. [5]

An FJ program $(\prec,\mathit{fields},\mathit{methods},$ $\mathit{mtable})$ is
_well-typed_ w.r.t. a class table $(F,M)$ if for any $(C,r,m,\bar{s})$ with
$M(C,r,m,\bar{s})=R$ and $\mathit{mtable}\left(C,m\right)=(\bar{x},e)$, the
typing judgment $\mathtt{this}{:}\,r,\,\bar{x}{:}\,\bar{s}\vdash e:R$ is
derivable. A soundness theorem has been proved in [5, Theorem 1], stating
that, for any expression $e$ in a well-typed FJ program with respect to a
class table $(F,M)$, if $e$ evaluates to some value $v$ and $e$ has type $R$,
then $v$ is in some region in $R$.

###  4.2 Inferring Region Types via Abstract Transformations

Let an FJ program $P$ be given. Now we introduce an algorithm to construct a
class table $(F,M)$ with respect to which $P$ is well-typed. As mentioned
above, our approach is based on abstract transformations. From now on, the
atomic types we are working with are the regions, i.e., take
$\mathit{Typ}=\mathit{Reg}$ for the development of abstract transformations.

We firstly compute an abstract transformation $\sigma$ and a term $t$ for each
FJ expression $e$. The transformation $\sigma$ encodes the type updates of the
variables and fields in $e$, while the term $t$ pre-calculates type of $e$.
Once we are given a typing environment $\mathit{env}$, we update it using
$\sigma$ and then instantiate $t$ with the updated environment to compute the
type of $e$, i.e., $e$ has type $t[\sigma(\mathit{env})]$.

For this, we define the following operations on pairs of abstract
transformations and terms: Let
$(\sigma,s),(\theta,t)\in\textit{ATrans}\times\textit{Tm}$.

  * •

_Composition_ : We define $(\sigma,s)\theta:=(\sigma\theta,s\theta)$, where
$\sigma\theta$ is the composition of transformations, and $s\theta$ is term
substitution.

  * •

_Join_ : We define $(\sigma,s)\vee(\theta,t):=(\sigma\vee\theta,s\vee t)$.

Suppose we have a function
$T:\mathit{Cls}\times\mathit{Mtd}\to\textit{ATrans}\times\textit{Tm}$, called
an _abstract method table_ , that assigns an abstract transformation and a
term to each method. The transformations capture the type updates for the
method and the term will be instantiated to the type for the method. Then we
define a pair $[\\![e]\\!]:\textit{ATrans}\times\textit{Tm}$ by induction on
the FJ expression $e$:

$\displaystyle[\\![x]\\!]$ $\displaystyle:=([],x)$
$\displaystyle[\\![\texttt{if}\;x=y\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}]\\!]$
$\displaystyle:=[\\![e_{1}]\\!]\vee[\\![e_{2}]\\!]$
$\displaystyle[\\![\texttt{let}\;x=e_{1}\;\texttt{in}\;e_{2}]\\!]$
$\displaystyle:=[\\![e_{2}]\\!]([x:\mapsto t]\theta)\quad\text{where
}(\theta,t)=[\\![e_{1}]\\!]$ $\displaystyle[\\![\texttt{null}]\\!]$
$\displaystyle:=([],\texttt{Null})$
$\displaystyle[\\![\texttt{new}^{\ell}\;C]\\!]$
$\displaystyle:=([],\texttt{CreatedAt}\mathopen{}\left(\ell\right)\mathclose{})$
$\displaystyle[\\![(D)\,e]\\!]$ $\displaystyle:=[\\![e]\\!]$
$\displaystyle[\\![x.f]\\!]$ $\displaystyle:=([],x.f)$
$\displaystyle[\\![x.f:=y]\\!]$ $\displaystyle:=([x.f:\geq y],y)$
$\displaystyle[\\![x^{C}.m(\bar{y})]\\!]$
$\displaystyle:=T(C,m)[\texttt{this}:\mapsto
x,\mathit{args}(C,m):\mapsto\bar{y}]$

where $\mathit{args}(C,m)$ denotes the arguments of $m$, i.e., if
$\mathit{mtable}(C,m)=(\bar{x},e)$ then $\mathit{args}(C,m)=\bar{x}$.

Given an FJ program, we compute an abstract method table $T$ as follows:

  1. 1.

Initialize $T$ with $T(C,m)=([],\bot)$ for all $m\in\mathit{methods}(C)$,
where $\bot$ is the empty term, i.e., the empty set of atoms.

  2. 2.

For each method, compute an abstract transformation and a term for its body,
and then update the corresponding entry in $T$. Specifically, for each
$m\in\mathit{methods}(C)$ with $(\bar{x},e)=\mathit{mtable}(C,m)$, let
$T(C,m)=T(C,m)\vee[\\![e]\\!]$.

  3. 3.

Close $T$ under the subclass relation, i.e., let $T(C,m)=T(C,m)\vee T(D,m)$ if
$D$ is a subclass of $C$.

  4. 4.

Repeat steps 2 and 3 until no more update of $T$ is possible.

After computing the table $T$, we compute a class table $(F,M)$ as follows:

  * (a)

Initialize $F$ and $M$ with the least type, i.e., the empty set of regions.

  * (b)

Use $T$ to update the entries in $F$ and $M$. Specifically, for each
$C,r,m,\bar{s}$ with $(\sigma,u)=T(C,m)$, we update the environment and get
$\mathit{env}=\sigma(\Gamma,F)$ where
$\Gamma=\texttt{this}{:}\,r,\,\mathit{args}(C,m){:}\,\bar{s}$. Then we update
the class table by taking $F=F\vee\mathit{env}|_{\mathrm{f}}$ and
$M(C,r,m,\bar{s})=M(C,r,m,\bar{s})\vee u[\mathit{env}]$.

  * (c)

Ensure that $(F,M)$ are well-formed. For instance, if $D$ is a subclass of
$C$, then both $F(C,r,f)$ and $F(D,r,f)$ are set to their join.

  * (d)

Repeat steps (b) and (c) until no more update of $F$ and $M$ is possible.

To summarize, the inference algorithm has two steps. It firstly computes an
abstract method table $T$. The abstract transformations in $T$ capture the
flow information of each method. This step is similar to constraint generation
and preprocessing such as simplification or closure in the constraint-based
type inference [27, 29]. Then it computes the class table $(F,M)$ by
instantiating the abstract transformations in $T$. This step solves the
constraints collected in $T$ via a least fixed-point argument.

The inference algorithm in the previous work [10, Appendix F] analyzes the
same method body multiple times when the method is fed with arguments of
different types at different invocations. Our algorithm instead uses the
abstract transformation stored in $T$ to infer the types of different method
calls. Therefore, it can effectively enhance the efficiency of analysis
especially when the analyzed program contains many method invocations with
arguments of different types. Appendix 0.B has an example demonstrating how to
compute and use $T$ to analyze invocations of the same method.

Lastly, the computed class table $(F,M)$ reveals the region information of the
program in the following sense.

######  Theorem 4.1 (Correctness of type inference)

Let $P$ be an FJ program. The above algorithm gives a class table $(F,M)$ with
respect to which $P$ is well-typed. In particular, for any $C,r,m,\bar{s}$
with $M(C,r,m,\bar{s})=R$ and for any $x:r$ and $\bar{y}:\bar{s}$, if
$x.m(\bar{y})$ evaluates to a value $v$, then $v$ resides in some region in
$R$. ∎

The second part of the above theorem is a corollary of the soundness result
[5, Theorem 1]. It states that the type of each method computed by $M$ is
correct. We sketch the proof of the first claim that the program is well-typed
with respect to the class table $(F,M)$ given by our algorithm. Because the
typings $F$ and $M$ are computed by the abstract transformations of the table
$T$, we only need to prove that these abstract transformations compute types
greater than the ones from typing derivation. More precisely, we need to prove

$\text{if }\Gamma\vdash e:R\text{ then
}R\subseteq\mathsf{Type}([\\![e]\\!](\Gamma))$

where $\mathsf{Type}([\\![e]\\!](\Gamma))$ is the type of the expression $e$
obtained by firstly applying the transformation component of $[\\![e]\\!]$ to
$\Gamma$ to obtained an updated environment and then instantiating the term
component with the updated environment. The above statement can be proved by
induction on the length of typing derivation as usual, because the definition
of $[\\![e]\\!]$ reflects the typing rules.

##  5 Conclusion, Implementation and Discussion

In this paper, we develop a theory of abstract transformations to capture type
changes in programs. The elements of an abstract transformation can be viewed
as equality and subtyping constraints. In particular, we work with access
graphs when defining these constraints. Access graphs provide a finite
representation of field access paths and thus ensure the termination of the
procedure to compute abstract transformations for the program. We instantiate
abstract transformations to endofunctions on typing environments to compute
the types of the program, which solves the constraints in the abstract
transformations. As an example, we work with the region type system of
Beringer et al. [5] to demonstrate how to use our inference algorithm based on
abstract transformations to compute region information of Featherweight Java
programs. The advantage is that the code of a method is analyzed only once
even when it is invoked with arguments of different region types in multiple
occasions of the program.

We have a prototype implementation of the type inference algorithm using the
Soot framework [24]. It takes a Java bytecode program as input and computes
the region types of the program. The implementation of abstract
transformations and their operations follows the definitions in this paper.
The function $[\\![-]\\!]$ computing an abstract transformation and a type
term for FJ expressions becomes a forward flow analysis for the control flow
graphs of the program. In particular, it has a flow-through method that
computes an abstract transformation for each node in the control flow graph
and then concatenates it with the one generated from the previous nodes. Then
a fixed point procedure is implemented to compute an abstract transformation
for each method in the program using the flow analysis. Lastly, the generated
abstract transformations are instantiated to compute the types of the methods
in the program. The prototype implementation is available at our GitHub
repository111https://github.com/cj-xu/AbstractTransformation.

Region types can make the analysis of trace properties more precise [10, 11].
By extending region type systems with effect annotations to give information
about possible event traces of the program, a method invocation $x.m(\bar{y})$
can have different effects for $x,\bar{y}$ in different regions. Our approach
can be extended to reason also such region-sensitive trace effects. Our idea
is to make the abstract method table $T$ to compute also a formal expression
capturing the information of traces and method calls. For example, consider
the following FJ program

$\texttt{emit}(a);\ x.f(\bar{y});\ \texttt{emit}(b);\ x.g(\bar{z})$

where $\texttt{emit}(a)$ is a primitive method that emits the event $a$. We
can assign it a formal expression

$\\{a\\}\cdot X_{(x,f,\bar{y})}\cdot\\{b\\}\cdot X_{(x,g,\bar{z})}$

meaning that any trace generated by the program starts with the event $a$,
followed by a trace generated by the method call $x.f(\bar{y})$ and then the
event $b$ and a trace generated by $x.g(\bar{z})$. Here $x,\bar{y},\bar{z}$
are variables and can be instantiated to region types with a given
environment; thus, the formal expression can be instantiated such that it
contains only variables like $X_{(r,f,\bar{s})}$ for the effect of the method
call of $f$ for an object in region $r$ with arguments in regions $\bar{s}$.
For each method in a calling context, we use its abstract transformation to
update the environment and then use the updated environment to instantiate its
call expression. In this way, we obtained a set of call expressions, one for
each method invocation in a calling context. Then we can use a least fixed
point algorithm to compute the trace effect of each method from these call
expressions. Currently we are still tackling the details to develop such a
compositional algorithm for inferring region-sensitive trace effects.

####  5.0.1 Acknowledgements

We thank Fredrick Nordvall Forsberg for the fruitful discussion on this work
and the anonymous reviewers for their valuable comments and suggestions on the
paper and its accompanying artifact.

## References

  * [1] Agesen, O.: Constraint-based type inference and parametric polymorphism. In: Static Analysis (SAS 1994). Lecture Notes in Computer Science, vol. 864, p. 78–100. Springer, Berlin, Heidelberg (1994). https://doi.org/10.1007/3-540-58485-4_34
  * [2] Aiken, A., Wimmers, E.L.: Type inference with subtypes. In: European Symposium on Programming (ESOP 1988). Lecture Notes in Computer Science, vol. 300, p. 31–41. Springer, Berlin, Heidelberg (1988). https://doi.org/10.1145/165180.165188
  * [3] Aiken, A., Wimmers, E.L.: Type inclusion constraints and type inference. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA 1993). p. 31–41. Association for Computing Machinery, New York, NY, USA (1993). https://doi.org/10.1145/165180.165188
  * [4] Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 445–532. Elsevier and MIT Press (2001). https://doi.org/10.1016/b978-044450813-3/50010-2
  * [5] Beringer, L., Grabowski, R., Hofmann, M.: Verifying pointer and string analyses with region type systems. Computer Languages, Systems and Structures 39(2), 49–65 (2013). https://doi.org/10.1016/j.cl.2013.01.001
  * [6] Bodden, E.: Inter-procedural data-flow analysis with IFDS/IDE and Soot. In: Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis (SOAP 2012). p. 3–8. Association for Computing Machinery (2012). https://doi.org/10.1145/2259051.2259052
  * [7] Boyapati, C., Salcianu, A., Beebee, W., Rinard, M.: Ownership types for safe region-based memory management in Real-Time Java. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003). p. 324–337. Association for Computing Machinery, New York, NY, USA (2003). https://doi.org/10.1145/781131.781168
  * [8] Chin, W.N., Craciun, F., Qin, S., Rinard, M.: Region inference for an object-oriented language. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation (PLDI 2004). p. 243–254. Association for Computing Machinery, New York, NY, USA (2004). https://doi.org/10.1145/996841.996871
  * [9] Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation (PLDI 1994). vol. 29(6), p. 230–241. Association for Computing Machinery (1994). https://doi.org/10.1145/773473.178263
  * [10] Erbatur, S., Hofmann, M., Zălinescu, E.: Enforcing programming guidelines with region types and effects. In: Chang, B.Y.E. (ed.) Programming Languages and Systems (APLAS 2017). Lecture Notes in Computer Science, vol. 10695, pp. 85–104. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-71237-6_5, appendices are available in the arXiv version: arXiv:1801.07647 [cs.PL].
  * [11] Erbatur, S., Schöpp, U., Xu, C.: Type-based enforcement of infinitary trace properties for Java. In: 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021). pp. 18:1–18:14. Association for Computing Machinery (2021). https://doi.org/10.1145/3479394.3479413
  * [12] Facebook: Flow - A static type checker for JavaScript, https://flow.org
  * [13] Gosling, J., Joy, B., Steele, G., Bracha, G., Buckley, A.: The Java Language Specification. Oracle America, Inc., Java SE 14 edn. (2020), http://docs.oracle.com/javase/specs/jls/se14/jls14.pdf
  * [14] Grabowski, R., Hofmann, M., Li, K.: Type-based enforcement of secure programming guidelines — code injection prevention at SAP. In: Barthe, G., Datta, A., Etalle, S. (eds.) Formal Aspects of Security and Trust (FAST 2011). Lecture Notes in Computer Science, vol. 7140, pp. 182–197. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29420-4_12
  * [15] Huang, W., Dong, Y., Milanova, A.: Type-based taint analysis for Java web applications. In: Fundamental Approaches to Software Engineering (FASE 2014). Lecture Notes in Computer Science, vol. 8411, p. 140–154. Springer, Berlin, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54804-8_10
  * [16] Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23(3), 396–450 (2001). https://doi.org/10.1145/503502.503505
  * [17] Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of LISP-like structures. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1979). p. 244–256. Association for Computing Machinery (1979). https://doi.org/10.1145/567752.567776
  * [18] Khedker, U.P., Sanyal, A., Karkare, A.: Heap reference analysis using access graphs. ACM Transactions on Programming Languages and Systems 30(1), 1–41 (2007). https://doi.org/10.1145/1290520.1290521
  * [19] Lerch, J., Späth, J., Bodden, E., Mezini, M.: Access-path abstraction: Scaling field-sensitive data-flow analysis with unbounded access paths. In: Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015). p. 619–629. IEEE Press (2015). https://doi.org/10.1109/ASE.2015.9
  * [20] Microsoft: TypeScript - Typed JavaScript at any scale, https://www.typescriptlang.org/
  * [21] Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theory and Practice of Object Systems 5(1), 35–55 (1999). https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1¡35::AID-TAPO4¿3.0.CO;2-4
  * [22] Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. SIGPLAN Notices 26(11), 146–161 (1991). https://doi.org/10.1145/118014.117965
  * [23] Sable Group, M.U.: Heros IFDS/IDE solver, https://github.com/Sable/heros
  * [24] Sable Group, M.U.: Soot - A framework for analyzing and transforming Java and Android applications, https://soot-oss.github.io/soot/
  * [25] Sagiv, S., Reps, T.W., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science 167(1–2), 131–170 (1996). https://doi.org/10.1016/0304-3975(96)00072-2
  * [26] Späth, J., Do, L.N.Q., Ali, K., Bodden, E.: Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In: Krishnamurthi, S., Lerner, B.S. (eds.) 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 56, pp. 22:1–22:26. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2016). https://doi.org/10.4230/LIPIcs.ECOOP.2016.22
  * [27] Traytel, D., Berghofer, S., Nipkow, T.: Extending Hindley-Milner type inference with coercive structural subtyping. In: Programming Languages and Systems (APLAS 2011). Lecture Notes in Computer Science, vol. 7078, p. 89–104. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-25318-8_10
  * [28] Wand, M., O’Keefe, P.: On the complexity of type inference with coercion. In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA 1989). p. 293–298. Association for Computing Machinery, New York, NY, USA (1989). https://doi.org/10.1145/99370.99394
  * [29] Wang, T., Smith, S.F.: Precise constraint-based type inference for Java. In: Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP 2001). p. 99–117. Springer-Verlag (2001). https://doi.org/10.5555/646158.679874

##  Appendix 0.A Composition and Join of Abstract Transformations

We explain how the operations of composition and join for abstract
transformations are defined. They are essential for modeling type updates of
programs.

When composing an abstract transformation $\sigma$ with another one $\theta$,
we need to substitute each term in $\sigma$ according to $\theta$.

######  Definition 8 (Substitution of terms)

We _substitute_ an atom $b.G$ according to a given abstract transformation
$\theta$ to obtain a term $(b.G)\theta\in\textit{Tm}$ as follows:

$\displaystyle(b.G)\theta$
$\displaystyle:=\begin{cases}b.G&\text{$b\not\in\mathrm{dom}(\theta)$}\\\
u.G&\text{if $(b:\mapsto u)\in\theta$}.\end{cases}$

The _substitution_ of a term is the join of the substitutions of its atoms,
i.e.,

$u\theta=\textstyle(\bigvee^{n}_{i=1}b_{i}.G_{i})\theta:=\textstyle\bigvee^{n}_{i=1}(b_{i}.G_{i})\theta.$

In other words, if $\theta$ contains an assignment $x:\mapsto v$, then every
occurrence of $x$ in $u$ is ‘replaced’ by $v$ using field graph composition to
obtain the term $u\theta$. For instance, we have $x\theta=v$ if $(x:\mapsto
v)\in\theta$, while $A\theta=A$ because $A$ as a type cannot be in
$\mathrm{dom}(\theta)$. In particular, substituting with the empty
transformation $[]$ makes no change to the term, i.e., $u[]=u$ for all terms
$u$.

For assignment $(x:\mapsto u)\in\sigma$, we only need to substitute its value
$u$ by $\theta$ when constructing the composition $\sigma\theta$. However, for
constraint $(y.G:\geq v)\in\sigma$, we need to substitute also the variable
$y$ in its key according to $\theta$. Because $\theta$ may assign $y$ to an
arbitrary term $w$, the substitution $w.G$ of the key $y.G$ may not be a key
but instead a set of keys. Therefore, the substitution $(y.G:\geq v)\theta$ is
a set of constraints mapping each new key to $v\theta$.

######  Definition 9 (Substitution of constraints)

We _substitute_ a constraint ${\kappa:\geq u}$ according to an abstract
transformation $\theta$ and get a set $(\kappa:\geq u)\theta$ of constraints
by

$(\kappa:\geq u)\theta:=\\{\alpha_{j}:\geq
u\theta\mid\kappa\theta=\textstyle\bigvee^{n}_{i=1}\alpha_{i}\text{ and }1\leq
j\leq n\\}.$

Note that substitution is required only for constraints whose key involves a
variable. For instance, we have $(A.G:\geq u)\theta=\\{A.G:\geq u\\}$ because
$(A.G)\theta=A.G$. Moreover, substitution of constraints can result in the
empty set. For example, we have $(x.G:\geq u)\theta=\emptyset$ if
$(x:\mapsto\bot)\in\theta$. Lastly, substituting with the empty transformation
$[]$ makes no change to the constraint, i.e., $(\kappa:\geq
u)[]=\\{\kappa:\geq u\\}$.

Now we define the composition $\sigma\theta$ where the type updates of the
transformation $\theta$ are considered to be performed first.

######  Definition 10 (Composition of abstract transformations)

Given two abstract transformations

$\displaystyle\sigma$ $\displaystyle=[x_{1}:\mapsto u_{1},\ldots,x_{n}:\mapsto
u_{n},\,\alpha_{1}:\geq v_{1},\ldots,\alpha_{m}:\geq v_{m}]$
$\displaystyle\theta$ $\displaystyle=[y_{1}:\mapsto s_{1},\ldots,y_{k}:\mapsto
s_{k},\,\beta_{1}:\geq t_{1},\ldots,\beta_{l}:\geq t_{l}]$

we compose them to get an abstraction transformation $\sigma\theta$ as
follows:

  1. 1.

Build the following set of assignments and constraints

$\Delta=\\{x_{1}:\mapsto u_{1}\theta,\ldots,x_{n}:\mapsto
u_{n}\theta\\}\cup(\alpha_{1}:\geq v_{1})\theta\cup\cdots\cup(\alpha_{m}:\geq
v_{m})\theta\cup\theta.$

  2. 2.

Remove from $\Delta$

     * i.

all the identity assignments $x:\mapsto x$,

     * ii.

all the bottom constraints $\kappa:\geq\bot$, and

     * iii.

any assignment $(y:\mapsto s)\in\theta$ such that $y=x_{i}$ for some
$i\in\\{1,\ldots,n\\}$.

  3. 3.

Remove the constraints $(\kappa:\geq w_{1}),\ldots,(\kappa:\geq
w_{o})\in\Delta$ with the same key and add the merged one $(\kappa:\geq
w_{1}\vee\cdots\vee w_{o})$ into $\Delta$.

The resulting set of assignments and constraints is an abstract
transformation.

The idea of the algorithm to compose abstract transformations $\sigma$ and
$\theta$ is the following: We firstly substitute all the assignments and
constraints in $\sigma$ according to $\theta$. The substitution result
together with the elements of $\theta$ forms a “pseudo transformation”
$\Delta$ (Step 1) which needs to be cleaned up. Specifically, all the identity
assignments and bottom constraints should be removed (Steps 2.i and 2.ii), and
the duplicate keys should be taken care of. If there are multiple assignments
with the same variable key, then one of them must come from $\theta$ and it
should be removed (Step 2.iii). This is because the assignments in $\sigma$
are performed after and thus overwrite those in $\theta$. For instance, the
code `x = y; x = z` leads to the composition $[x:\mapsto z][x:\mapsto y]$ (in
“backward” order); the resulting transformation is $[x:\mapsto z]$ as the
earlier assignment $x:\mapsto y$ is overwritten. If there are multiple
constrains with the same field key, then their values should be joined (Step
3). This is due to the _weak update_ for field typing. For instance, if both
$x$ and $y$ refer to some objects of type $A$, then the code `x.f = z; y.f =
z’` leads to the composition $[A.f:\geq z^{\prime}][A.f:\geq z]$ which
evaluates to $[A.f:\geq z\vee z^{\prime}]$.

###### Example 6

We consider again the example from Fig. 1. The statements of the program and
their assigned abstract transformations are given below:

$\begin{array}[]{lll}\verb|x = y.f;|&&[x:\mapsto y.f]\\\ \verb|y = new
C();|&&[y:\mapsto C]\\\ \verb|y.f = x|&&[y.f:\geq x]\\\ \end{array}$

We compose the first two transformations and have

$\theta=[y:\mapsto C][x:\mapsto y.f]=[y:\mapsto C,\,x:\mapsto y.f].$

This easy composition does not involve any substitution. To compose the last
transformation, we need to substitute its constraint according to $\theta$:

$(y.f:\geq x)\theta=\\{\kappa:\geq
x\theta\mid\kappa\in(y.f){\theta}\\}=\\{C.f:\geq y.f\\}$

because $(y.f){\theta}=C.f$ and $x\theta=y.f$. Finally, the composition of the
three transformations is

$[y.f:\geq x]([y:\mapsto C][x:\mapsto y.f])=[x:\mapsto y.f,\,y:\mapsto
C,\,C.f:\geq y.f]$

which does not require cleaning up. ∎

It is clear that (pre- or post-)composing with the empty transformation $[]$
is identity, i.e., $[]\sigma=\sigma=\sigma[]$ for any transformation $\sigma$.

Given two abstract transformations, we join them componentwise as follows.

######  Definition 11 (Join of abstract transformations)

The join $\sigma\vee\theta$ consists of non-identity assignments
$x:\mapsto\sigma(x)\vee\theta(x)$ and constrains
$\kappa:\geq\sigma(\kappa)\vee\theta(\kappa)$ for
$x,\kappa\in\mathrm{dom}(\sigma)\cup\mathrm{dom}(\theta)$.

The above definition uses the convention $\sigma(x)=x$ and
$\sigma(\kappa)=\bot$ for variables $x\not\in\mathrm{dom}(\sigma)$ and
nonempty access graphs $\kappa\not\in\mathrm{dom}(\sigma)$ introduced in
Section 3.2.

Because the join operation of terms is commutative, so is the one of abstract
transformations. Moreover, we have $\sigma\vee\bot=\sigma=\bot\vee\sigma$ for
all transformations $\sigma$, where $\bot$ is the bottom transformation which
consists of assignments $x:\mapsto\bot$ for all variables $x$.

##  Appendix 0.B An Example of Inferring Region Types

We present an example to illustrate how to infer the region type of a program
using the algorithm introduced in Section 4.2.

Consider the following Java code taken from [11].

⬇

class Node {

Node next;

Node last() {

if (next == null) {

return this;

} else {

return next.last();

}

}

}

⬇

class Test {

Node linear() {

Node x = new${}^{\ell_{1}}$ Node();

Node y = new${}^{\ell_{2}}$ Node();

y.next = x;

return y.last();

}

Node cyclic() {

Node z = new${}^{\ell_{3}}$ Node();

z.next = z;

return z.last();

}

}

The two methods in $\mathtt{Test}$ create a linear linked list and a cyclic
one. We illustrate how to compute the entry $T(\texttt{Node},\texttt{last})$
and then use it to infer the types of the methods in $\mathtt{Test}$.

We initialize $T(\texttt{Node},\texttt{last})=([],\bot)$ and then increase it
using $[\\![e_{\texttt{last}}]\\!]$ where $e_{\texttt{last}}$ is the method
body of last:

  * •

In the first iteration, we have

$\displaystyle[\\![e_{\texttt{last}}]\\!]$
$\displaystyle=([],\texttt{this})\vee(T(\texttt{Node},\texttt{last})[\texttt{this}:\mapsto\texttt{this}.\texttt{next}])$
$\displaystyle=([],\texttt{this})\vee([\texttt{this}:\mapsto\texttt{this}.\texttt{next}],\bot)$
$\displaystyle=([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}],\texttt{this})$
$\displaystyle T(\texttt{Node},\texttt{last})$
$\displaystyle=T(\texttt{Node},\texttt{last})\vee[\\![e_{\texttt{last}}]\\!]$
$\displaystyle=([],\bot)\vee([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}],\texttt{this})$
$\displaystyle=([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}],\texttt{this}).$

  * •

In the second iteration, we have

$\displaystyle[\\![e_{\texttt{last}}]\\!]=\cdots$
$\displaystyle=([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}\vee\texttt{this}.\overline{\texttt{next}}],$
$\displaystyle\hskip 18.0pt\texttt{this}.\texttt{next})$ $\displaystyle
T(\texttt{Node},\texttt{last})=\cdots$
$\displaystyle=([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}\vee\texttt{this}.\overline{\texttt{next}}],$
$\displaystyle\hskip 18.0pt\texttt{this}\vee\texttt{this}.\texttt{next})$

where
$\texttt{this}.\overline{\texttt{next}}=\texttt{this}.\langle\texttt{next},\\{(\texttt{next},\texttt{next})\\},\texttt{next}\rangle$
is the access graph consisting of all paths with at least two next’s.

  * •

In the third iteration, we have

$\displaystyle[\\![e_{\texttt{last}}]\\!]=\cdots$
$\displaystyle=([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}\vee\texttt{this}.\overline{\texttt{next}}],$
$\displaystyle\hskip 18.0pt\texttt{this}.\texttt{next})$ $\displaystyle
T(\texttt{Node},\texttt{last})=\cdots$
$\displaystyle=([\texttt{this}:\mapsto\texttt{this}\vee\texttt{this}.\texttt{next}\vee\texttt{this}.\overline{\texttt{next}}],$
$\displaystyle\hskip
18.0pt\texttt{this}\vee\texttt{this}.\texttt{next}\vee\texttt{this}.\overline{\texttt{next}}).$

Then we reach the fixed point and have computed
$T(\texttt{Node},\texttt{last})$.

Let $r_{i}=\texttt{CreatedAt}\mathopen{}\left(\ell_{i}\right)\mathclose{}$ be
the regions for objects created at $\ell_{1},\ell_{2},\ell_{3}$. We compute
the return types of linear and cyclic, that is, the possible regions where the
returned object resides. The linear method returns `y.last()` resulting in
$T(\texttt{Node},\texttt{last})[\texttt{this}:\mapsto\mathtt{y}]$ whose second
component is a term

$t=\mathtt{y}\vee\mathtt{y}.\texttt{next}\vee\mathtt{y}.\overline{\texttt{next}}.$

It is obvious that then environment at the return site is

$\mathit{env}=(\mathtt{x}:r_{1},\,\mathtt{y}:r_{2},\,r_{1}.\texttt{next}:\texttt{Null},\,r_{2}.\texttt{next}:r_{1}).$

The return type of linear is the instantiation

$t[\mathit{env}]=r_{1}\vee r_{2}.$

With a similar computation, we have that the return type of cyclic is $r_{3}$.