The role of linearity in sharing analysis

Abstract

Sharing analysis is used to statically discover data structures which may overlap in object-oriented programs. Using the abstract interpretation framework, we show that sharing analysis greatly benefits from linearity information. A variable is linear in a program state when different field paths starting from it always reach different objects. We propose a graph-based abstract domain which can represent aliasing, linearity, and sharing information and define all the necessary abstract operators for the analysis of a Java-like language.

1. Introduction

In the context of static analysis of object-oriented programs, the aim of sharing analysis is to discover when two data structures may overlap. For instance, this may happen in Java programs, whose objects are stored in a shared memory called heap. Sharing information can be exploited in program parallelization and distribution, since methods working on data structures that do not overlap can be executed on different processors, using disjoint memory. Moreover, knowing sharing information is very useful for improving other kinds of analyses like shape, pointer, class, and cyclicity analysis.

Consider a class $\mathtt{Tree}$ with two fields ${\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{r}}}$ defined as follows:

class Tree { Tree l; Tree r; }

A concrete state in an object-oriented program is usually described by a frame, which is a map from program variables to memory locations (or ${\mathord{\mathtt{null}}}$ ), and a memory, which is a map from locations to objects. Figure 1 shows two states with two variables x and y referring to two different objects of class $\mathtt{Tree}$ . In the state of Figure 1A, the variables x and y share, since $x.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}$ and $y.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}$ point to the same object.

Figure 1. Two concrete states illustrating pair sharing.

Traditionally, sharing analysis has been designed in two different ways: set-sharing analysis and pair-sharing analysis. In set-sharing analysis, we look for sets of variables which share a common object, while in pair-sharing analysis we are only interested in discovering pairs of variables which share. In this paper, we deal with field-sensitive pair-sharing properties.

We abstract concrete states into a new kind of graph we call Aliasing Linearity Pair Sharing ( $\mathsf{ALPS}$ ) graph. For instance, the state in Figure 1A is abstracted into the $\mathsf{ALPS}$ graph in Figure 1A where the dotted edges between two nodes encode the information that they share. All $\mathsf{ALPS}$ graphs have at most two levels. The first level consists of nodes which are labeled with program variables and may have both incoming and outgoing edges. Second level nodes are unlabeled, are connected by at least an incoming edge with first level nodes, and cannot have outgoing edges. Edges are labeled with field names. Dotted edges encode sharing information and can connect two nodes at any level.

As it is customary in the abstract interpretation theory (Cousot and Cousot 1977, 1992), the correspondence between $\mathsf{ALPS}$ graphs and concrete states is given by a concretization function that maps each graph to the set of all concrete states it abstracts. In this section, we try to describe the main feature of $\mathsf{ALPS}$ graphs while remaining at an informal level. Precise definitions will be given in the next sections.

1.1 Field-sensitive pair-sharing information

Sharing properties for logic programs has been studied extensively. The large literature on this topic and the paper by Secci and Spoto (2005a) on object-oriented programs have been the starting point for designing our abstract domain for sharing analysis.

We say that two locations share when it is possible to reach from them a common location. Consider the concrete state depicted in Figure 1A. Here x and y are bound to two different data structures which overlap, since $x.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}$ and $y.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}$ are bound to the same object: we say that x and y share. In the abstract graph, we represent this information with an (undirected) dotted edge between the two nodes. For instance, the sharing information in Figure 1A is captured by the four dotted edges in Figure 2A. In the following, in order to keep the graphs as simple as possible, we omit those dotted edges which can be inferred by other features of the graph. In this case, the only nonredundant edge is the one between $x.{\mathord{\mathtt{r}}}$ and $y.{\mathord{\mathtt{l}}}$ , as shown in Figure 2B.

Figure 2. Abstractions of the concrete states in Figure 1.

Note that our graphs encode possible pair-sharing information: the presence of a dotted edge means that the corresponding locations might share, while the absence of the dotted edge means that the corresponding locations do not share for sure. Therefore, the graphs in Figure 2 are correct abstractions also for the concrete state in Figure 1B, although $x.{\mathord{\mathtt{r}}}$ and $y.{\mathord{\mathtt{l}}}$ do not share in the latter.

1.2 Aliasing and nullness

$\mathsf{ALPS}$ graphs may encode definite nullness of variables and fields: a variable is null when it does not appear as a label, while a field $v.{\mathord{\mathtt{f}}}$ is null when there is no edge labeled with ${\mathord{\mathtt{f}}}$ departing from the node v. For example, in Figure 4 the field $v_1.{\mathord{\mathtt{r}}}$ is null. Definite nullness means that when a node is null in the graph, then it has to be null in the corresponding concrete states, but the converse is not true. For example, all the graphs in Figure 3 are correctly abstracted by Figure 4, since in all of them $v_1.{\mathord{\mathtt{r}}}$ is null, although $v_2.{\mathord{\mathtt{r}}}$ is null in some states (Figure 3B and C) but not in others (Figure 3A).

Figure 3. Three concrete states illustrating nullness and aliasing.

Figure 4. Abstraction of the concrete states in Figure 3. Both $v_1$ and $v_2$ are first level nodes, even if there is an edge pointing to $v_1$ .

Figure 5. Concrete and abstract states illustrating aliasing.

The graph also encodes definite weak aliasing: two variables or fields are weakly aliased when they point to the same location or they point both to ${\mathord{\mathtt{null}}}$ . For instance, the variable $v_1$ and the field $v_2.{\mathord{\mathtt{l}}}$ in the concrete state of Figure 3A are aliased, since they are bound to the same object. $\mathsf{ALPS}$ graphs encode aliasing information by using a single node for abstracting both variables/fields. For example, in Figure 4, the same node is labeled by both $v_1$ and the $v_2.{\mathord{\mathtt{l}}}$ (more precisely, the node $v_1$ is reached by the edge labeled ${\mathord{\mathtt{l}}}$ departing from the node $v_2$ ). Note that, due to the definition of weak aliasing, $v_1$ and $v_2.{\mathord{\mathtt{l}}}$ are considered to be aliased even in the concrete state of Figure 3C, hence Figure 3C is still correctly abstracted by Figure 4. Another example is in Figure 5.

We use the adjective weak to distinguish our treatment of aliasing by other proposals which consider two identifiers to be aliased only if they point to the same non-null location (see, e.g., Pollet et al. 2001).

1.3 Linearity information

In the field of logic programming, the use of a linearity property has proved to be very useful when dealing with sharing information (see Bagnara et al. 2005 for a comprehensive evaluation). We show how the same idea can be reused to enhance sharing analysis of object-oriented programs. We propose a new combined analysis of sharing, aliasing, and linearity properties for Java-like programs based on abstract interpretation, inspired by the corresponding domains on logic programs.

We say that a location is nonlinear when there are two different paths starting from it and reaching a common location. Consider for instance Figure 6. Starting from $v_5.{\mathord{\mathtt{r}}}$ , we reach the same object by either $v_5.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{r}}}$ or $v_5.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{l}}}$ . Therefore, we say that $v_5.{\mathord{\mathtt{r}}}$ is nonlinear. It is easy to note that also $v_5$ is nonlinear. In general, whenever a field $v.{\mathord{\mathtt{f}}}$ is nonlinear, the variable v is nonlinear too. We represent possible nonlinearity information by means of a double circle. For instance, the concrete state for variables $v_5$ and $v_6$ in Figure 6 is abstracted as in Figure 7.

Figure 6. A concrete state illustrating nonlinearity.

Figure 7. Abstraction of the concrete state in Figure 6.

1.4 An example program

Linearity plays a key role in sharing analysis, since it allows us to propagate precise sharing information when dealing with method calls. We show how the analysis works and the relevance of linearity information with the help of the example program in Figure 8.

Figure 8. The example program.

We consider again the class $\mathtt{Tree}$ previously defined. The method makeTree defined in Figure 8 (left) builds a complete tree of depth n, whose nodes are all distinct. Actually, with a bottom-up static analysis using $\mathsf{ALPS}$ graphs, we can easily infer that, for any input $n\geq 2$ , makeTree returns a data structure which may be described by the graph in Figure 9A, where the label ${\mathord{\mathtt{out}}}$ denotes the return value of the method. Since there are no undirected dotted edges between ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{r}}}$ , it means that ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{r}}}$ do not share. Moreover, since there are no double circles, everything is guaranteed to be linear. The latter property implies that, in any concrete state approximated by the $\mathsf{ALPS}$ graph in Figure 9A, two different fields of the same object can never share. In particular, we know that ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{r}}}$ do not share.

Figure 9. Two $\mathsf{ALPS}$ graphs for the example program.

The useTree method in Figure 8 (right) calls makeTree and extracts two subtrees which do not share. In detail, in the useTree method, since we know that ${\mathord{\mathtt{t}}}$ is linear, we can infer that ${\mathord{\mathtt{tl}}}$ is linear too. Since ${\mathord{\mathtt{tl}}}$ is linear, its fields ${\mathord{\mathtt{tl}}}.{\mathord{\mathtt{r}}}$ and ${\mathord{\mathtt{tl}}}.{\mathord{\mathtt{l}}}$ do not share, and therefore ${\mathord{\mathtt{right}}}$ and ${\mathord{\mathtt{left}}}$ do not share. Note that linearity of ${\mathord{\mathtt{t}}}$ is not needed to prove that ${\mathord{\mathtt{t}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{t}}}.{\mathord{\mathtt{r}}}$ do not share (sharing is enough for this). We need linearity when we want to go deeper and prove that ${\mathord{\mathtt{t}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{t}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{r}}}$ do not share. Linearity of ${\mathord{\mathtt{t}}}$ is essential here in proving that ${\mathord{\mathtt{left}}}$ and ${\mathord{\mathtt{right}}}$ do not share. The heap at the end of the useTree method may be described by the graph in Figure 9B.

Due to the interaction between sharing and linearity, different $\mathsf{ALPS}$ graphs may represent the same set of concrete states. For example, adding a dotted edge between ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{out}}}.{\mathord{\mathtt{r}}}$ in Figure 9A does not allow them to share, since that would violate the linearity of ${\mathord{\mathtt{out}}}$ . In sec:alps, we will introduce a closure operator on graphs to deal with these interactions.

1.5 Plan of the paper

The rest of the paper is organized as follows. Section 2 summarizes the notations used through the paper and describes our simple Java-like language. Section 3 defines the basic notions of reachability, sharing, linearity, and aliasing. In Section 4, we introduce the domain of aliasing graphs, which encodes weak aliasing for variables and fields. Then, in Section 5 we enrich aliasing graphs with information regarding sharing and linearity, obtaining what we call $\mathsf{ALPS}$ graphs. Section 6 defines an abstract semantics (analysis) over $\mathsf{ALPS}$ graphs and states its correctness. Section 7 contains a discussion about related work and Section 8 concludes. Appendix A contains all the proofs of the properties and theorems in the paper.

This paper is an extended and revised version of Amato et al. (2015). With respect to the conference version, this paper includes: (1) definitions for all the operators used in the abstract and concrete semantics; (2) the notion of graph morphism and closure; (3) all the proofs; and (4) many new examples.

2. Preliminaries

2.1 Notations

We use a special notation for ordered pairs. The two components of an ordered pair are separated by $\mathbin{\star}$ . A definition of a pair $s=a\mathbin{\star} b$ silently defines the pair of selectors $s.a$ and $s.b$ .

A total (partial) function f from A to B is denoted by $A \to B$ ( $A \nrightarrow B$ , respectively). Given $f: A \nrightarrow B$ and $x \in A$ , we write $f(x)=\bot$ when f is undefined on x. The composition of functions f and g is denoted by $f \circ g$ . The domain and range of f are, respectively, dom(f) and rng(f). We denote by $[v_1 \mapsto t_1,\ldots,v_n \mapsto t_n]$ the function f such that $dom(f) = \{v_1,\ldots,v_n\}$ and $f(v_i)=t_i$ for $i=1,\ldots,n$ . We denote by $f[w_1\mapsto d_1,\ldots,w_m\mapsto d_m]$ an update of f, with a possibly enlarged domain. By $f|_s$ ( $f|_{-s}$ ), we denote the restriction of f to $s\subseteq dom(f)$ (to $dom(f)\setminus s$ , respectively).

Given a set X, we denote by $\mathcal{P}(X)$ the powerset of X and with $\mathcal{P}_2(X)$ those subsets of X of cardinality 1 or 2. Given $f: A \nrightarrow B$ , $Y \in \mathcal{P}(B)$ and $Z \subseteq \mathcal{P}_2(B)$ , we denote by $f^{-1}(Y)=\{a \in A \mid f(a) \in Y\}$ and $f^{-1}(Z)=\{\{a,a'\} \in \mathcal{P}_2(A) \mid \{f(a),f(a')\} \in Z\}$ .

For an ordered set $\mathit{S}\mathbin{\star}\mathord\le$ , if $s\in S$ , then $\downarrow s=\{s'\in S\mid s'\le s\}$ is the downward closure of S. For a preordered set $\mathit{S}\mathbin{\star}\mathord\le$ , we say that $s_1, s_2 \in S$ are equivalent, and we write $s_1 \sim s_2$ , when $s_1 \leq s_2$ and $s_2 \leq s_1$ . The set $\mathit{S}/{\sim}$ of equivalence classes modulo $\sim$ is ordered by $[s_1] \le [s_2]$ iff $s_1 \le s_2$ . We will freely use preordered sets in the place where ordered sets are expected, implicitly referring to the induced ordered set.

We recall now the basics of abstract interpretation from Cousot and Cousot (1977, 1992). Given two posets $\mathit{C}\mathbin{\star}\mathord\le$ and $\mathit{A}\mathbin{\star}\mathord\preceq$ (the concrete and the abstract domain), a Galois connection is a pair of monotonic maps $\alpha:\mathit{C}\mapsto\mathit{A}$ and $\gamma:\mathit{A}\mapsto\mathit{C}$ such that $\gamma \circ \alpha$ is extensive and $\alpha \circ \gamma$ is reductive. It is a Galois insertion when $\alpha \circ \gamma$ is the identity map, that is, when the abstract domain does not contain useless elements. This is equivalent to $\alpha$ being onto, or $\gamma$ one-to-one.

We say that $a \in A$ is a correct approximation of $c \in C$ when $\alpha(c) \preceq a$ or, equivalently, $c \leq \gamma(a)$ . An abstract operator $f^A:\mathit{A}^n\mapsto\mathit{A}$ is correct w.r.t. $f:\mathit{C}^n\rightarrow\mathit{C}$ if, given $a_1, \ldots, a_n$ correct abstractions of $c_1, \ldots, c_n$ , we have that $f^A(a_1, \ldots, a_n)$ is a correct abstraction of $f(c_1, \ldots, c_n)$ . This is equivalent to $f(\gamma(a_1), \ldots, \gamma(a_n)) \leq \gamma(f^A(a_1, \ldots, a_n))$ for every tuple $a_1,\ldots, a_n$ of abstract objects.

2.2 The language

We use the Java-like object-oriented language defined by Secci and Spoto (2005a), which is a normalized version of Java with downward casts, and which we extend with upper casts. The details of the concrete semantics first appeared in a long version of the above paper (Secci and Spoto 2005b) which is unpublished. Here we present the semantics for the sake of completeness.

2.2.1 Syntax

Each program has a set of identifiers $\mathord{\mathit{Ide}}$ and a finite set of classes (or types) $\mathcal{K}$ ordered by a subclass relation $\le$ such that $\mathcal{K}\mathbin{\star}\mathord\le$ is a poset. The set $\mathord{\mathit{Ide}}$ includes the special identifiers ${\mathord{\mathtt{this}}}$ , ${\mathord{\mathtt{res}}}$ , ${\mathord{\mathtt{out}}}$ . Since we do not allow multiple inheritance, for any class $\kappa\in \mathcal{K}$ , the set $\{\kappa'\mid \kappa' \geq\kappa\}$ is a chain. In the following, we assume that $\mathord{\mathit{Ide}}$ and $\mathcal{K}$ have been fixed beforehand.

We use type environments to describe the identifiers in scope in a given program point. A type environment is a map from a finite set of identifiers to the associated class. The set of type environments is

\begin{equation*} \mathord{\mathit{TypEnv}}=\{\tau: \mathord{\mathit{Ide}}\nrightarrow\mathcal{K}\mid dom(\tau)\text{ is finite}\} .\end{equation*}

We call variables the identifiers in $dom(\tau)$ . Any class $\kappa\in\mathcal{K}$ defines a type environment, also denoted by $\kappa$ , which maps the fields of $\kappa$ (including both the fields defined in $\kappa$ and those inherited by the superclasses) to their types.

We require that fields cannot be redefined in subclasses. It means that if ${\mathord{\mathtt{f}}} \in dom (\kappa)$ and $\kappa' \leq \kappa$ , then ${\mathord{\mathtt{f}}} \in dom (\kappa')$ and $\kappa'({\mathord{\mathtt{f}}})=\kappa({\mathord{\mathtt{f}}})$ . For consistency of notation, we write $\kappa.{\mathord{\mathtt{f}}}$ in place of $\kappa({\mathord{\mathtt{f}}})$ for the type of the field ${\mathord{\mathtt{f}}}$ in the class $\kappa$ .

Finally, we require the existence of a class $\top$ with no fields which is the common ancestor of all other classes.

In the examples, we will describe the set of classes and the corresponding type environment using a notation inspired by class definitions in Java.

Example 1. Classes in the example program in Section 1.4 may be described by the following Java-like syntax:

class Tree { Tree l; Tree r; }class Integer { }

Formally, we have $\mathcal{K}=\{\top,\mathtt{Tree},\mathtt{Integer}\}$ with a flat ordering. Moreover, $\mathtt{Tree}=[{\mathord{\mathtt{l}}}\mapsto\mathtt{Tree}, {\mathord{\mathtt{r}}}\mapsto\mathtt{Tree}]$ and $\mathtt{Integer}=[]$ .

Expressions and commands are normalized versions of those in Java. Their syntax is the following:

\begin{align*}\mathit{exp} ::= &\ {\mathord{\mathtt{null}}}\ \kappa\mid\mathtt{new}\ \kappa\mid v\mid\mathit{v}.{\mathord{\mathtt{f}}}\mid\mathtt{(}\kappa\mathtt{)}v\mid\mathit{v}\mathtt{.m(}v_1,\ldots,v_n\mathtt{)}\\\mathit{com} ::= &\ v\mathbin{\mathtt{\unicode{x02254}}}\mathit{exp} \mid v.{\mathord{\mathtt{f}}}\mathbin{\mathtt{\unicode{x02254}}}\mathit{exp}\mid\mathtt{\{}\mathit{com}\mathtt{;}\cdots\mathtt{;}\mathit{com}\mathtt{\}}\\&\ \mid\mathtt{if\ }v\ \mathtt{=}\ w\mathtt{\ then\ }\mathit{com}\mathtt{\ else\ }\mathit{com}\mid\mathtt{if\ }v\ \mathtt{=null\ then\ }\mathit{com}\mathtt{\ else\ }\mathit{com}\end{align*}

where $\kappa\in\mathcal{K}$ , ${\mathord{\mathtt{f}}}\in\mathord{\mathit{Ide}}$ and $v,w,v_1,\ldots,v_n\in\mathord{\mathit{Ide}}\setminus\{{\mathord{\mathtt{res}}}\}$ are distinct when they appear in the same clause. Each method $\kappa.{\mathord{\mathtt{m}}}$ of a class $\kappa$ is defined with a statement like

\begin{equation*}\mathtt{\kappa_0\ m(}w_1\!:\!\kappa_1,\ldots,w_n\!:\!\kappa_n\mathtt{)}\mathtt{\ with\ }w_{n+1}\!:\!\kappa_{n+1},\ldots,w_{n+m}\!:\!\kappa_{n+m}\mathtt{\ is\ }\mathit{com}\end{equation*}

where $w_1,\ldots,w_n,w_{n+1},\ldots,w_{n+m}\in\mathord{\mathit{Ide}}$ are distinct and are not ${\mathord{\mathtt{res}}}$ nor ${\mathord{\mathtt{this}}}$ nor ${\mathord{\mathtt{out}}}$ . Their declared types are $\kappa_1,\ldots,\kappa_n,\kappa_{n+1},\ldots,\kappa_{n+m}\in\mathcal{K}$ , respectively. Variables $w_1,\ldots,w_n$ are the formal parameters of the method, and $w_{n+1},\ldots,w_{n+m}$ are its local variables. The method can also use a variable ${\mathord{\mathtt{out}}}$ of type $\kappa_0$ which holds its return value. We define $\mathit{body}(\kappa.{\mathord{\mathtt{m}}})=\mathit{com}$ and $\mathit{returnType}(\kappa.{\mathord{\mathtt{m}}})=\kappa_0$ . Overriding methods cannot change the formal parameters but may specialize the return type.

Given a type environment $\tau$ , with an abuse of notation we denote with $\tau(\mathit{exp})$ the static type of an expression $\mathit{exp}$ , defined as follows:

\begin{gather*} \tau(v.{\mathord{\mathtt{f}}})=\tau(v).{\mathord{\mathtt{f}}} \qquad \tau(\mathtt{new}\ \kappa) =\tau({\mathord{\mathtt{null}}}\ \kappa) =\tau(\mathtt{(}\kappa\mathtt{)}v)=\kappa\\ \tau(v.\mathtt{m(}v_1,\ldots,v_n\mathtt{)})= \mathit{returnType}(\tau(v).{\mathord{\mathtt{m}}}). \end{gather*}

Note that the static type of a field of class $\kappa$ is recovered from the definition of $\kappa$ , while the static type of the return value of a method call is the return type of the method.

We require expressions, commands, and methods to be well-typed, according to the standard definition in Java. We also require that all casts are explicit, so that in any assignment $v\mathbin{\mathtt{\unicode{x02254}}}\mathit{exp}$ (resp. $v.{\mathord{\mathtt{f}}}\mathbin{\mathtt{\unicode{x02254}}}\mathit{exp}$ ) the types of v (resp. $v.{\mathord{\mathtt{f}}}$ ) and $\mathit{exp}$ coincide. The same is required for formal and actual parameters. This is not a limitation since we allow upward and downward casts.

2.2.2 Semantics

The semantics of the language is defined by means of frames, objects, and memories defined as follows:

\begin{align*}\mathord{\mathit{Frame}}_\tau & =\{\phi\mid\phi\in dom(\tau)\to\mathord{\mathit{Loc}}\cup\{{\mathord{\mathtt{null}}}\}\}\\\mathord{\mathit{Obj}} & =\{\kappa\mathbin{\star}\phi\mid\kappa\in\mathcal{K}, \ \phi\in\mathord{\mathit{Frame}}_{\kappa}\}\\\mathord{\mathit{Memory}} & =\{\mu\in\mathord{\mathit{Loc}}\nrightarrow\mathord{\mathit{Obj}}\mid dom(\mu)\text{ is finite}\}\end{align*}

where $\mathord{\mathit{Loc}}$ is an infinite set of locations. A frame binds identifiers to locations or ${\mathord{\mathtt{null}}}$ . A memory binds such locations to objects, which contain a class tag and the frame for their fields. A new object of class $\kappa$ is $\mathtt{new}(\kappa)=\kappa\mathbin{\star}\phi$ , with $\phi(v)={\mathord{\mathtt{null}}}$ for each $v\in dom(\kappa)$ .

Example 2. Let $\tau=[v_7\mapsto \mathtt{Tree}, v_8\mapsto \mathtt{Tree}]$ and consider the state depicted in Figure 10, whose abstraction is in Figure 11. We have that $\phi = [ v_7\mapsto l_0, v_8\mapsto l_1]$ and

\begin{align*} \mu = [ & l_0 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto l_2, {\mathord{\mathtt{r}}}\mapsto l_3], l_1 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto l_4, {\mathord{\mathtt{r}}}\mapsto {\mathord{\mathtt{null}}}],\\ & l_2 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto {\mathord{\mathtt{null}}}, {\mathord{\mathtt{r}}}\mapsto {\mathord{\mathtt{null}}}], l_3 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto {\mathord{\mathtt{null}}}, {\mathord{\mathtt{r}}}\mapsto l_5],\\ & l_4 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto l_6, {\mathord{\mathtt{r}}}\mapsto {\mathord{\mathtt{null}}}], l_5 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto {\mathord{\mathtt{null}}}, {\mathord{\mathtt{r}}}\mapsto l_7], \\ & l_6 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto l_7, {\mathord{\mathtt{r}}}\mapsto {\mathord{\mathtt{null}}}], l_7 \mapsto \mathtt{Tree}\mathbin{\star}[{\mathord{\mathtt{l}}}\mapsto {\mathord{\mathtt{null}}}, {\mathord{\mathtt{r}}}\mapsto {\mathord{\mathtt{null}}}] ] \enspace .\end{align*}

Figure 10. A concrete state with variables $v_7,v_8$ .

Figure 11. Abstraction of the concrete state in Figure 10.

Our language is strongly typed, which means that the static type of an expression should be consistent with its runtime type. We formalize here the notion of type correctness for a frame and a memory.

Definition 3 (Types of locations) Let $\phi\in\mathord{\mathit{Frame}}_\tau$ , $\mu\in\mathord{\mathit{Memory}},$ and $l \in dom(\mu)$ , we write $\tau(l)=\mu(l).\kappa$ for the runtime type of location l.

If v is a variable, the object associated with v should be of a subtype of the static type of v. This leads to the definition of weak correctness:

Definition 4 (Weak $\tau$ -correctness) Let $\phi\in\mathord{\mathit{Frame}}_\tau$ and $\mu\in\mathord{\mathit{Memory}}$ . We say that $\phi \mathbin{\star} \mu$ is weakly $\tau$ -correct if for every $v\in dom(\phi)$ such that $\phi(v)\not={\mathord{\mathtt{null}}}$ we have $\phi(v)\in dom(\mu)$ and $\tau(\phi(v))\le\tau(v)$ .

We strengthen the correctness notion of Definition 4 by requiring that it also holds for the fields of the objects in memory.

Definition 5 ( $\tau$ -correctness) Let $\phi\in\mathord{\mathit{Frame}}_\tau$ and $\mu\in\mathord{\mathit{Memory}}$ . We say that $\phi \mathbin{\star} \mu$ is $\tau$ -correct and write $\phi\mathbin{\star}\mu:\tau$ , if

1. (1). $\phi \mathbin{\star} \mu$ is weakly $\tau$ -correct and,

2. (2). for every $o\in rng(\mu)$ , $o.\phi \mathbin{\star} \mu$ is weakly $o.\kappa$ -correct.

We call state a pair $\phi \mathbin{\star} \mu$ which is $\tau$ -correct for some type environment $\tau$ . The set of $\tau$ -correct states is

\begin{equation*} \Sigma_\tau=\{\phi\mathbin{\star}\mu\mid \phi\in\mathord{\mathit{Frame}}_\tau,\ \mu\in\mathord{\mathit{Memory}},\ \phi\mathbin{\star}\mu:\tau\} .\end{equation*}

Example 6 (Noncorrect state) Let $\tau \in \mathord{\mathit{TypEnv}}=[ u \mapsto \mathtt{Tree}, v \mapsto \mathtt{Tree}, w \mapsto \mathtt{Integer} ]$ , $\phi \in \mathord{\mathit{Frame}}_\tau = [ u \mapsto l_0, v \mapsto {\mathord{\mathtt{null}}}, w \mapsto l_1 ]$ and $\mu \in \mathord{\mathit{Memory}}$ such that $\mu(l_1)=\mathtt{Integer} \mathbin{\star} []$ and $\mu(l_0) = \mathtt{Tree} \mathbin{\star} [ {\mathord{\mathtt{l}}} \mapsto l_0, {\mathord{\mathtt{r}}} \mapsto l_1 ]$ . This may be depicted graphically as follows:

It turns out that $\phi \mathbin{\star} \mu$ is weakly $\tau$ -correct, but it is not $\tau$ -correct, since the right child of u points to an integer node instead of a tree node.

The semantics of an expression is a partial map $\mathcal{E}_{\tau}^{I}\unicode{x0301A}{\mathit{exp}}\unicode{x0301B}: \Sigma_\tau\nrightarrow\Sigma_{\tau+\mathit{exp}}$ from an initial to a final state, containing a distinguished variable ${\mathord{\mathtt{res}}}$ holding the value of the expression, where $\tau+\mathit{exp}=\tau[{\mathord{\mathtt{res}}}\mapsto \tau(\mathit{exp})]$ .

Definition 7 (Semantics of expressions) Let $\tau$ describe the variables in scope and I be an interpretation. The semantics for expressions $\mathcal{E}_{\tau}^{I}\unicode{x0301A}{\mathit{exp}}\unicode{x0301B}: \Sigma_\tau \nrightarrow\Sigma_{\tau+\mathit{exp}}$ is defined as

\begin{align*} \mathcal{E}_{\tau}^{I}\unicode{x0301A}{{\mathord{\mathtt{null}}}\ \kappa}\unicode{x0301B}(\phi\mathbin{\star}\mu) &=\phi[{\mathord{\mathtt{res}}}\mapsto{\mathord{\mathtt{null}}}]\mathbin{\star}\mu \\ \mathcal{E}_{\tau}^{I}\unicode{x0301A}{\mathtt{new}\ \kappa}\unicode{x0301B}(\phi\mathbin{\star}\mu) &=\phi[{\mathord{\mathtt{res}}}\mapsto l]\mathbin{\star}\mu[l\mapsto\mathtt{new}(\kappa)]\quad \text{with $l\in\mathord{\mathit{Loc}}\setminus dom(\mu)$} \\ \mathcal{E}_{\tau}^{I}\unicode{x0301A}{{v}}\unicode{x0301B}(\phi\mathbin{\star}\mu)&=\phi[{\mathord{\mathtt{res}}}\mapsto\phi(v)]\mathbin{\star}\mu \\ \mathcal{E}_{{\tau}}^{I}\unicode{x0301A}{v.{\mathord{\mathtt{f}}}}\unicode{x0301B}(\phi\mathbin{\star}\mu)&=\begin{cases} \phi[{\mathord{\mathtt{res}}}\mapsto \phi(v).{\mathord{\mathtt{f}}}]\mathbin{\star}\mu & \text{if $\phi(v)\not={\mathord{\mathtt{null}}}$} \\ \bot & \text{otherwise} \end{cases}\\ \mathcal{E}_{\tau}^{I}\unicode{x0301A}{\mathtt{(}\kappa\mathtt{)}v}\unicode{x0301B}(\phi\mathbin{\star}\mu)&= \begin{cases} \phi[{\mathord{\mathtt{res}}}\mapsto \phi(v)]\mathbin{\star}\mu & \text{if $\phi(v)={\mathord{\mathtt{null}}}$ or}\\ & \text{$\phi(v)\not={\mathord{\mathtt{null}}}$ and $\{\tau(\phi(v)),\kappa\}$ is a chain}\\ \bot & \text{otherwise} \end{cases} \\ \mathcal{E}_{\tau}^{{I}}\unicode{x0301A}{v.\mathtt{m(}v_1,\ldots,v_n\mathtt{)}}\unicode{x0301B}(\phi\mathbin{\star}\mu) &=\begin{cases} \phi[{\mathord{\mathtt{res}}}\mapsto\phi'({\mathord{\mathtt{out}}})]\mathbin{\star}\mu' & \text{if $\phi(v)\not={\mathord{\mathtt{null}}}$} \\ \bot & \text{otherwise} \end{cases} \end{align*}

with $\phi'\mathbin{\star}\mu'=I(\tau(v).{\mathord{\mathtt{m}}})(\sigma^\unicode{x2020})$ and $\sigma^\unicode{x2020}= [{\mathord{\mathtt{this}}}\mapsto\phi(v),w_1\mapsto\phi(v_1),\ldots, w_n\mapsto\phi(v_n)]\mathbin{\star}\mu$ .

The semantics of a command is a partial map from an initial to a final state: $\mathcal{C}_{{\tau}}^{{I}}\unicode{x0301A}{{\mathit{com}}}\unicode{x0301B}:\Sigma_\tau\nrightarrow\Sigma_\tau$ . We assume that $\tau$ in both $\mathcal{E}_{\tau}^{I}\unicode{x0301A}{\_}\unicode{x0301B}$ and $\mathcal{C}_{{\tau}}^{{I}}\unicode{x0301A}{{\_}}\unicode{x0301B}$ does not contain the variable ${\mathord{\mathtt{res}}}$ .

Definition 8 (Semantics of commands) Let $\tau$ describe the variables in scope, I be an interpretation and

\begin{align*} \mathit{setVar}_\tau^v&=\lambda(\phi\mathbin{\star}\mu)\in\Sigma_\tau. \phi|_{-{\mathord{\mathtt{res}}}}[v\mapsto\phi({\mathord{\mathtt{res}}})]\mathbin{\star}\mu\\ \mathit{setField}_\tau^{v.{\mathord{\mathtt{f}}}}&= \lambda(\phi\mathbin{\star}\mu)\in\Sigma_\tau.\begin{cases} \phi|_{-{\mathord{\mathtt{res}}}}\mathbin{\star}\mu[l\mapsto\mu(l)[{\mathord{\mathtt{f}}}\mapsto\phi({\mathord{\mathtt{res}}})]] & \text{if $\phi(v)=l\neq{\mathord{\mathtt{null}}}$} \\ \bot & \text{otherwise.} \end{cases} \end{align*}

The semantics for commands $\mathcal{C}_{{\tau}}^{{I}}\unicode{x0301A}{{\mathit{com}}}\unicode{x0301B}:\Sigma_\tau\nrightarrow\Sigma_\tau$ is defined as

\begin{align*} \mathcal{C}_{{\tau}}^{{I}}\unicode{x0301A}{{v\mathbin{\mathtt{\unicode{x02254}}}\mathit{exp}}}\unicode{x0301B}&= \mathit{setVar}_{\tau+\mathit{exp}}^v \circ \mathcal{E}_{\tau}^{I}\unicode{x0301A}{\mathit{exp}}\unicode{x0301B} \\ \mathcal{C}_{{\tau}}^{I}\unicode{x0301A}{v.{\mathord{\mathtt{f}}} \mathbin{\mathtt{\unicode{x02254}}}\mathit{exp}}\unicode{x0301B}&= \mathit{setField}_{\tau+\mathit{exp}}^{v.{\mathord{\mathtt{f}}}} \circ \mathcal{E}_{\tau}^{I}\unicode{x0301A}{\mathit{exp}}\unicode{x0301B}\\ \mathcal{C}_{{\tau}}^{{I}}\unicode{x0301A}{{\begin{aligned} \mathtt{if\ v=w\ then\ }\mathit{com}_1\\ \mathtt{else\ }\mathit{com}_2 \end{aligned}}}\unicode{x0301B}(\phi\mathbin{\star}\mu)&=\begin{cases} \mathcal{C}_{\tau}^{I}\unicode{x0301A}{{\mathit{com}_1}}\unicode{x0301B}(\phi\mathbin{\star}\mu) & \text{if $\phi(v)=\phi(w)$} \\ \mathcal{C}_{{\tau}}^{I}\unicode{x0301A}{{\mathit{com}_2}}\unicode{x0301B}(\phi\mathbin{\star}\mu) & \text{if $\phi(v)\not=\phi(w)$} \end{cases} \\ \mathcal{C}_{{\tau}}^{{I}}\unicode{x0301A}{{\begin{aligned} \mathtt{if\ v=null\ then\ }\mathit{com}_1\\ \mathtt{else\ }\mathit{com}_2 \end{aligned}}}\unicode{x0301B}(\phi\mathbin{\star}\mu)&=\begin{cases} \mathcal{C}_{\tau}^{I}\unicode{x0301A}{\mathit{com}_1}\unicode{x0301B}(\phi\mathbin{\star}\mu) & \text{if $\phi(v)={\mathord{\mathtt{null}}}$} \\ \mathcal{C}_{\tau}^{i}\unicode{x0301A}{{\mathit{com}_2}}\unicode{x0301B}(\phi\mathbin{\star}\mu) & \text{if $\phi(v)\not={\mathord{\mathtt{null}}}$} \end{cases}\\ \mathcal{C}_{\tau}^{I}\unicode{x0301A}{\{\mathit{com}_1;\ldots;\mathit{com}_p\}}\unicode{x0301B}&= (\lambda\sigma\in\Sigma_\tau.\sigma) \circ\mathcal{C}_{{\tau}}^{I}\unicode{x0301A}{{\mathit{com}_p}}\unicode{x0301B}\circ\cdots\circ \mathcal{C}_{\tau}^{{I}}\unicode{x0301A}{\mathit{com}_1}\unicode{x0301B}. \end{align*}

The identity function $\lambda\sigma\in\Sigma_\tau.\sigma$ in the semantics of the sequence of commands is needed when $p=0$ .

Each method $\kappa.{\mathord{\mathtt{m}}}$ is denoted by a partial function from input to output states and an interpretation I maps methods to partial functions on states, such that $I({\kappa.{\mathord{\mathtt{m}}}}):\Sigma_{\mathit{input}(\kappa.{\mathord{\mathtt{m}}})}\nrightarrow\Sigma_{\mathit{output}(\kappa.{\mathord{\mathtt{m}}})}$ , with the type environments:

\begin{align*}\mathit{input}(\kappa.{\mathord{\mathtt{m}}}) & = [{\mathord{\mathtt{this}}}\mapsto\kappa,w_1\mapsto\kappa_1,\ldots,w_n\mapsto\kappa_n] \\\mathit{output}(\kappa.{\mathord{\mathtt{m}}})&=[{\mathord{\mathtt{out}}}\mapsto\kappa_0,w'_1\mapsto\kappa_1,\ldots,w'_n\mapsto\kappa_n] \mbox{ and}\\\mathit{scope}(\kappa.{\mathord{\mathtt{m}}})&=\begin{aligned}[t]\mathit{input}(\kappa.{\mathord{\mathtt{m}}})& \cup \mathit{output}(\kappa.{\mathord{\mathtt{m}}}) \\& \cup [w_{n+1}\mapsto\kappa_{n+1},\ldots,w_{n+m}\mapsto \kappa_{n+m}]\end{aligned}\end{align*}

where $w'_1,\ldots,w'_n$ are fresh variables used to keep track of the actual parameters. Each $w'_i$ is automatically assigned to the same value of the corresponding $w_i$ at the beginning of the method execution, and it is never changed later.

Example 9. Consider the method ${\mathord{\mathtt{makeTree}}}$ in Section 1.4. We have that

\begin{align*} \mathit{input}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}) & =[{\mathord{\mathtt{this}}} \mapsto \mathtt{Tree}, n \mapsto \mathtt{Integer}] \\ \mathit{output}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}) & = [{\mathord{\mathtt{out}}} \mapsto \mathtt{Tree},n' \mapsto \mathtt{Integer}]\\ \mathit{scope}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}) & = \begin{aligned}[t] \mathit{input}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}) & \cup \mathit{output}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}) \cup [m \mapsto \mathtt{Integer}] . \end{aligned} \end{align*}

The denotational semantics of a program is the least fixpoint of a transformer on interpretations which maps an interpretation I into a new interpretation I’ evaluating the bodies of the methods in I from an input state where local variables are bound to ${\mathord{\mathtt{null}}}$ . If $\kappa.{\mathord{\mathtt{m}}}$ is defined as

\begin{equation*}\mathtt{\kappa_0\ m(}w_1\!:\!\kappa_1,\ldots,w_n\!:\!\kappa_n\mathtt{)}\mathtt{\ with\ }w_{n+1}\!:\!\kappa_{n+1},\ldots,w_{n+m}\!:\!\kappa_{n+m}\mathtt{\ is\ }\mathit{com}\end{equation*}

we have

\begin{equation*}\begin{array}{lll}I'(\kappa.{\mathord{\mathtt{m}}}) &= &(\lambda\phi\mathbin{\star}\mu\in\Sigma_{\mathit{scope}(\kappa.{\mathord{\mathtt{m}}})}.\,\phi|_{dom(\mathit{output}(\kappa.{\mathord{\mathtt{m}}}))}\mathbin{\star}\mu) \, \circ \, \mathcal{C}_{\mathit{scope}(\kappa.{\mathord{\mathtt{m}}})}^{I}\unicode{x0301A}{\mathit{body}(\kappa.{\mathord{\mathtt{m}}})}\unicode{x0301B} \circ \\&&(\lambda\phi\mathbin{\star}\mu\in\Sigma_{\mathit{input}(\kappa.{\mathord{\mathtt{m}}})}.\,\phi[{\mathord{\mathtt{out}}}\mapsto{\mathord{\mathtt{null}}}, w'_1 \mapsto \phi(w_1),\ldots, w'_n \mapsto \phi(w_n),\\&& \quad \quad w_{n+1}\mapsto{\mathord{\mathtt{null}}},\ldots,w_{n+m}\mapsto{\mathord{\mathtt{null}}}]\mathbin{\star}\mu) \enspace .\end{array}\end{equation*}

3. Reachability, Sharing, Linearity, and Aliasing

We formalize here the concepts of reachability, sharing, linearity, and aliasing for objects. In a later section, we will use these concepts to introduce the new abstract domain $\mathsf{ALPS}$ . The following definition will simplify notation later.

Definition 10 (Fields of locations) Given $\sigma=\phi\mathbin{\star}\mu \in \Sigma_\tau$ , $l \in dom(\mu)$ , ${\mathord{\mathtt{f}}}$ an identifier and $\bar {\mathord{\mathtt{f}}} = {\mathord{\mathtt{f}}}_1,\ldots, {\mathord{\mathtt{f}}}_n$ a possibly empty sequence of identifiers, when they exist we write

• • $l.{\mathord{\mathtt{f}}}$ for $\mu(l).\phi({\mathord{\mathtt{f}}})$ , the location reachable from l through the field ${\mathord{\mathtt{f}}}$ ;

• • $l.\bar{\mathord{\mathtt{f}}}$ for $l.{\mathord{\mathtt{f}}}_1.\ldots.{\mathord{\mathtt{f}}}_n$ ; if $\bar {\mathord{\mathtt{f}}}$ is empty, $l.\bar {\mathord{\mathtt{f}}}=l$ .

Every time we use these notations, we implicitly require that the conditions guaranteeing their existence are satisfied. The following proposition states very simple results relating types and states.

Proposition 11. Given $\sigma=\phi\mathbin{\star}\mu \in \Sigma_\tau$ , ${\mathord{\mathtt{f}}}$ an identifier and $l, l' \in dom(\mu)$ , then:

1. (1). $l.{\mathord{\mathtt{f}}}$ exists iff $\tau(l).{\mathord{\mathtt{f}}}$ exists;

2. (2). if $l.{\mathord{\mathtt{f}}}$ exists and $l.{\mathord{\mathtt{f}}}\neq {\mathord{\mathtt{null}}}$ , then $\tau(l.{\mathord{\mathtt{f}}}) \leq\tau(l).{\mathord{\mathtt{f}}}$ .

These properties essentially derive from the $\tau$ -correctness of $\sigma$ . In particular, (2) means that the actual type of the object pointed to by a field is a subtype of the formal type of the field.

Definition 12 (Sharing and linearity for locations) Given $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ and $l_1, l_2 \in dom(\mu)$ , we say that:

1. (1). $l_1$ and $l_2$ share in $\sigma$ when there are $\bar {\mathord{\mathtt{f}}}_1$ , $\bar {\mathord{\mathtt{f}}}_2$ such that $l_1.\bar {\mathord{\mathtt{f}}}_1 = l_2.\bar {\mathord{\mathtt{f}}}_2 \neq {\mathord{\mathtt{null}}}$ ;

2. (2). $l_1$ is nonlinear in $\sigma$ when there are $\bar{{\mathord{\mathtt{f}}}}_1 \neq \bar{{\mathord{\mathtt{f}}}}_2$ such that $l_1.\bar {\mathord{\mathtt{f}}}_1 = l_1.\bar {\mathord{\mathtt{f}}}_2 \neq {\mathord{\mathtt{null}}}$ ; otherwise, $l_1$ is said to be linear.

Note that, for any location $l \in dom(\mu)$ , we have that l shares with itself.

Example 13. Consider the state $\sigma=\phi\mathbin{\star}\mu$ in Example 2. We have that $l_0$ and $l_1$ share in $\sigma$ , since $l_0.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}} = l_1.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}} = l_7$ , while $l_2$ and $l_4$ do not share. Moreover, all the locations are linear.

If $l.{\mathord{\mathtt{f}}}=l'$ it means that l’ is reachable from l. If we ignore the field ${\mathord{\mathtt{f}}}$ , we obtain the standard notion of reachability.

Definition 14 (Reachability relations) Given $\sigma= \phi\mathbin{\star}\mu \in \Sigma_\tau$ and $l, l' \in dom(\mu)$ , we write

• • $l \xrightarrow{}_\sigma l'$ iff there is a field ${\mathord{\mathtt{f}}}$ such that $l' = l.{\mathord{\mathtt{f}}}$ ;

• • $l \xrightarrow{*}_\sigma l'$ iff there is a sequence of fields $\bar{{\mathord{\mathtt{f}}}}$ such that $l' = l.\bar {\mathord{\mathtt{f}}}$ .

Moreover, we denote by $\mathord{\mathit{RLoc_\sigma}}(l) = \{l' \in dom(\mu) \mid l \xrightarrow{*}_\sigma l'\}$ the set of locations reachable from $l \in dom(\mu)$ . By convention, we assume $\mathord{\mathit{RLoc_\sigma}}(l) = \emptyset$ for $l \notin dom(\mu)$ .

Example 15. Consider the state $\sigma=\phi\mathbin{\star}\mu$ in Example 2. We have that:

\begin{align*} \mathord{\mathit{RLoc_\sigma}}(l_0) & = \{l_0,l_2,l_3,l_5,l_7\} & \mathord{\mathit{RLoc_\sigma}}(l_4) & = \{l_4,l_6,l_7\}\\ \mathord{\mathit{RLoc_\sigma}}(l_1) & = \{l_1,l_4,l_6,l_7\} & \mathord{\mathit{RLoc_\sigma}}(l_5) & = \{l_5,l_7\}\\ \mathord{\mathit{RLoc_\sigma}}(l_2) & = \{l_2\} & \mathord{\mathit{RLoc_\sigma}}(l_6) & = \{l_6,l_7\}\\ \mathord{\mathit{RLoc_\sigma}}(l_3) & = \{l_3,l_5,l_7\} & \mathord{\mathit{RLoc_\sigma}}(l_7) & = \{l_7\}\end{align*}

Using reachability we may give an alternative characterization of sharing between locations.

Proposition 16. Given $\sigma =\phi\mathbin{\star}\mu \in \Sigma_\tau$ and locations $l_1, l_2 \in dom(\mu)$ , we have that $l_1$ shares with $l_2$ iff $\mathord{\mathit{RLoc_\sigma}}(l_1) \cap \mathord{\mathit{RLoc_\sigma}}(l_2) \neq \emptyset$ .

An analogous characterization for linearity is not possible, since we need to discern among different ways of reaching the same location.

Using reachability, we refine our definition of interpretation, by requiring that a method does not access locations L of the input state which are not reachable from the actual parameters. Programming languages such as Java and that of Section 2.2 satisfy these constraints. This restriction will let us prove the correctness of method calls in the abstract semantics.

Definition 17 (Interpretation) An intepretation I maps methods to partial functions on state, that is, $I({\kappa.{\mathord{\mathtt{m}}}}): \Sigma_{\mathit{input}(\kappa.{\mathord{\mathtt{m}}})}\nrightarrow\Sigma_{\mathit{output}(\kappa.{\mathord{\mathtt{m}}})}$ , in such a way that if $I(\kappa.{\mathord{\mathtt{m}}})(\phi\mathbin{\star}\mu)=\phi'\mathbin{\star}\mu'$ and $L=dom(\mu)\setminus(\bigcup\{ \mathord{\mathit{RLoc_\sigma}}(\phi(v))\mid v\in dom({\mathit{input}(\kappa.{\mathord{\mathtt{m}}})})\})$ then $\mu|_L=\mu'|_L$ , $\phi'({\mathord{\mathtt{out}}})\not\in L$ and $\bigcup\{rng(\mu'(l).\phi)\cap L\mid l\in dom(\mu'|_{-L})\}=\emptyset$ .

Note that the transformer of interpretations in Section 2.2.2 respects the conditions in Definition 17. Interpretations could be further restricted in such a way that if $I(\kappa.{\mathord{\mathtt{m}}})(\phi\mathbin{\star}\mu)=\phi'\mathbin{\star}\mu'$ then $rng(\phi')\cap L = \emptyset$ . We do not enforce this condition since it is not necessary to prove correctness of the abstract semantics.

3.1 Reachability among identifiers

As we said before, we want to record sharing and linearity information not only for variables in the type environment but also for their fields. Therefore, we introduce some notation to treat variables and their fields as uniformly as possible.

Definition 18 (Qualified fields and identifiers) Given a type environment $\tau$ , we call qualified field an expression $v.{\mathord{\mathtt{f}}}$ where $v \in dom(\tau)$ and ${\mathord{\mathtt{f}}} \in dom(\tau(v))$ and we call qualified identifier either a variable in $dom(\tau)$ or a qualified field. We denote by $Q_\tau$ and $I_\tau$ the set of qualified fields and identifiers, respectively.

It is worth noting that we only consider fields that are in the declared type of the variables, and we do not consider further fields that are in the actual type. This choice, although it may decrease the precision of the analysis, simplifies a lot the correspondence between abstract and concrete semantics and may increase the speed of the analysis. Note that since $dom(\tau)$ is finite, we have that $I_\tau$ is also finite.

Example 19. In Example 2, the qualified fields are $Q_\tau=\{ \mathit{v_7}.{\mathord{\mathtt{l}}},\mathit{v_7}.{\mathord{\mathtt{r}}},\mathit{v_{8}}.{\mathord{\mathtt{l}}}, \mathit{v_{8}}.{\mathord{\mathtt{r}}} \}$ and the qualified identifiers are $I_\tau = \{\mathit{v_7},\mathit{v_{8}} \}\cup Q_\tau$ .

Definition 20 (Locations for qualified fields) If $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ and $v.{\mathord{\mathtt{f}}} \in Q_\tau$ , for uniformity of notation with variables we define $\phi(v.{\mathord{\mathtt{f}}}) = {\mathord{\mathtt{null}}}$ if $\phi(v)={\mathord{\mathtt{null}}}$ , $\phi(v.{\mathord{\mathtt{f}}})=\phi(v).{\mathord{\mathtt{f}}}$ otherwise. In other words, if $\phi(v.{\mathord{\mathtt{f}}}) \neq {\mathord{\mathtt{null}}}$ , then $\phi(v.{\mathord{\mathtt{f}}})$ is the location pointed to by the field ${\mathord{\mathtt{f}}}$ in the variable v.

The following proposition states that the runtime type of a qualified identifiers is a subtype of its declared type.

Proposition 21. For each $i \in I_\tau$ and $\sigma= \phi\mathbin{\star}\mu\in\Sigma_\tau$ , we have that $\phi(i) \neq {\mathord{\mathtt{null}}}$ implies $\tau(\phi(i)) \leq \tau(i)$ .

We now lift the definitions and properties of sharing and linearity from locations to identifiers.

Definition 22. (Sharing, linearity, and aliasing) Let $\sigma \in \Sigma_\tau$ and $i_1, i_2 \in I_\tau$ . We say that:

• • $i_1 $ and $i_2$ share in $\sigma$ when $\phi(i_1) \neq {\mathord{\mathtt{null}}} \neq \phi(i_2)$ and $\phi(i_1)$ , $\phi(i_2)$ share in $\sigma$ ;

• • $i_1$ is nonlinear in $\sigma$ when $\phi(i_1) \neq{\mathord{\mathtt{null}}}$ and $\phi(i_1)$ is nonlinear in $\sigma$ ; otherwise, $i_1$ is said to be linear.

• • $i_1 $ and $i_2$ are (weakly) aliased in $\sigma$ when $\phi(i_1)=\phi(i_2)$ .

Note that two identifiers that are both ${\mathord{\mathtt{null}}}$ are considered to be weakly aliased.

Example 23. In Figure 10, the field $\mathit{v_7}.{\mathord{\mathtt{r}}}$ shares with $\mathit{v_8}.{\mathord{\mathtt{l}}}$ . As a consequence, $\mathit{v_7}$ shares with $\mathit{v_8}.{\mathord{\mathtt{l}}}$ and $\mathit{v_8}$ . The field $\mathit{v_7}.{\mathord{\mathtt{l}}}$ shares only with itself and the parent. The identifiers $v_7$ and $v_8$ are linear, while $v_5$ , $\mathit{v_5}.{\mathord{\mathtt{r}}},$ and $v_6$ in Figure 6 are not linear.

Note that a qualified identifier $i \in I_\tau$ shares with itself if and only if it is not ${\mathord{\mathtt{null}}}$ . Moreover, each $i \in I_\tau$ such that $\phi(i)= {\mathord{\mathtt{null}}}$ is linear and does not share with any other identifier.

Definition 24 (Reachability for qualified identifiers) Let $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ and $i \in I_\tau$ . We define the set of locations reachable from i in $\sigma$ as $\mathord{\mathit{RLoc_\sigma}}(i)=\mathord{\mathit{RLoc_\sigma}}(\phi(i))$ if $\phi(i)\neq {\mathord{\mathtt{null}}}$ , $\emptyset$ otherwise.

Note that the reachability set for a variable is related to the reachability set of its qualified fields. This is formalized by the following result.

Proposition 25. Let $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ and $v \in dom(\tau)$ . If $\phi(v)\neq{\mathord{\mathtt{null}}}$ , then

\begin{equation*} \mathord{\mathit{RLoc_\sigma}}(v) \supseteq \{ \phi(v) \} \cup \bigcup_{v.{\mathord{\mathtt{f}}} \in Q_\tau} \mathord{\mathit{RLoc_\sigma}}(v.{\mathord{\mathtt{f}}}) \enspace . \end{equation*}

Equality does not hold since there is some sharing information in $\mathord{\mathit{RLoc_\sigma}}(v)$ which is not derivable from the sharing information of its fields. This is due to the fact that we consider only fields in the declared type of a variables. Thus, further sharing relationships may exist in other fields which do not belong to the declared type.

3.2 Class-induced reachability

It must be observed that two qualified identifiers might never be able to share if their static types do not let them be bound to overlapping data structures. Analogously, certain qualified identifiers are forced to be linear.

Example 26. In Example 1, we have that a $\mathtt{Tree}$ is not an $\mathtt{Integer}$ , an $\mathtt{Integer}$ is not a $\mathtt{Tree}$ , and they do not have any field which can share. Therefore, any identifier of type $\mathtt{Tree}$ can never share with any identifier of type $\mathtt{Integer}$ . Moreover, any identifier of type $\mathtt{Integer}$ may only be linear.

Example 27. Consider the following classes:

class A { B b; } class C { }class B { C c; } class B1 extends B { }

Then, every object of class $\mathtt{A}$ is linear.

Identifying pair of classes which cannot share, or that are forced to be linear, may improve the result of the analysis. This is the topic of the rest of this section.

Definition 28 (Class reachability) We define a reachability relation between classes given by $\kappa \xrightarrow{}\kappa'$ iff exists an identifier ${\mathord{\mathtt{f}}}$ such that $\kappa' \leq \kappa.{\mathord{\mathtt{f}}}$ . We denote by $\xrightarrow{*}$ the reflexive and transitive closure of $\xrightarrow{}$ .

In Definition 28, if a class $\kappa'$ (different from $\kappa$ ) is reachable from $\kappa$ , then all its subclasses $\downarrow\kappa'$ are considered reachable. This reflects the fact that we consider a language with (checked) casts. The following proposition relates reachability with class reachability: if location $l_2$ is reachable from $l_1$ , the type of $l_2$ should be reachable from the type of $l_1$ .

Proposition 29. Given $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ and $l_1, l_2 \in dom(\mu)$ , if $l_1 \xrightarrow{*}_\sigma l_2$ , then $\tau(l_1) \xrightarrow{*} \tau(l_2)$ .

This notion of class reachability corresponds to the one in Secci and Spoto (2005a) if we denote by $C(\kappa)$ the set of classes reachable by $\downarrow \kappa$ , that is,

\begin{equation*}C(\kappa) = \{ \kappa' \mid \kappa'' \in \downarrow \kappa\text{ and } \kappa'' \xrightarrow{*} \kappa' \} \enspace .\end{equation*}

We introduce this alternative notation since it will be convenient in the next definitions.

Example 30. Consider the classes in Example 1, we have that $C(\mathtt{Tree})=\{\mathtt{Tree}\}$ and $C(\mathtt{Integer})=\{\mathtt{Integer}\}$ . Therefore, any identifier of type $\mathtt{Tree}$ can never share with an identifier of type $\mathtt{Integer}$ . Given the classes in Example 27, we have $C(\mathtt{A})=\{ \mathtt{A},\mathtt B, \mathtt{B1}, \mathtt{C} \}$ .

We will denote by NL the set of classes whose instances may be nonlinear and by ${SH} \,$ the set of pair of classes which may share. Both NL and SH may be computed using class reachability, that is, by typing information only.

First of all, note that identifiers $i_1$ and $i_2$ may share only if there is a common location l which is reachable both from $\phi(i_1)$ and $\phi(i_2)$ . Therefore, the class $\tau(l)$ should be class reachable from both $\tau(\phi(i_1))$ and $\tau(\phi(i_2))$ . This is formalized by the following:

Definition 31 (The SH set) Given the type environment $\tau$ , we define the set of pairs of classes which may share:

\begin{equation*} {SH}=\{ (\kappa, \kappa') \mid C(\kappa) \cap C(\kappa') \neq \emptyset \} \enspace . \end{equation*}

Proposition 32. Given $i_1, i_2 \in I_\tau$ , and $\sigma \in \Sigma_\tau$ , if $i_1$ and $i_2$ share in $\sigma$ , then $(\tau(i_1), \tau(i_2)) \in {SH}$ .

We now consider the problem of linearity induced by type information. In general, an object of class $\kappa$ may be nonlinear either if $\kappa$ has two fields which may share, it has a field which may share with itself or if a nonlinear class $\kappa'$ is reachable from $\kappa$ . This is formalized by the following:

Definition 33 (The NL set) The set NL of nonlinear classes is the upward closure of the least solution of the equation:

\begin{multline*}\mathcal S = \{ \kappa \mid C(\kappa.{\mathord{\mathtt{f}}}_1) \cap C(\kappa.{\mathord{\mathtt{f}}}_2) \neq \emptyset,{\mathord{\mathtt{f}}}_1 \neq {\mathord{\mathtt{f}}}_2 \}\cup \{ \kappa \mid \kappa \in C(\kappa.{\mathord{\mathtt{f}}}) \} \cup \{ \kappa \mid \kappa\xrightarrow{} \kappa', \kappa' \in \mathcal S \}\enspace .\end{multline*}

Note that $\mathit{NL}$ is upward closed by definition. If $\kappa$ is possibly nonlinear, the same holds for any $\kappa' \geq \kappa$ since a variable of type $\kappa'$ may actually point to an object of class $\kappa$ .

Proposition 34. Given $\sigma \in \Sigma_\tau$ and $i \in I_\tau$ , if i is not linear in $\sigma$ , then $\tau(i) \in {NL}$ .

In the following sections, we use the concepts of sharing, linearity, and aliasing introduced before to define a new abstract domain, called $\mathsf{ALPS}$ (Aliasing Linearity Pair Sharing), for the analysis of Java-like programs.

4. Aliasing Graphs

We start by defining a basic domain encoding definite aliasing. The domain will also encode definite nullness, which is a useful and basic property of Java programs.

Definition 35 (Pre-aliasing graphs) A pre-aliasing graph over the type environment $\tau$ is a directed graph $G = N \mathbin{\star} E \mathbin{\star} \ell$ such that:

• • N is the finite set of nodes;

• • $E \subseteq N \times \mathord{\mathit{Ide}} \times N$ is the set of directed edges, each labeled by an identifier;

• • $\ell: dom(\tau) \nrightarrow N$ is a partial map from variables to nodes;

with the additional condition that

• • $\forall n \in N, \forall {\mathord{\mathtt{f}}} \in \mathord{\mathit{Ide}}$ , there is at most an outgoing edge from n labeled by ${\mathord{\mathtt{f}}}$ and

• • $\forall n \in N, \forall {\mathord{\mathtt{f}}} \in \mathord{\mathit{Ide}}$ , if $n \xrightarrow{{\mathord{\mathtt{f}}}} n' \in E$ then there exists $v \in dom(\tau)$ such that $\ell(v)=n$ and $v.{\mathord{\mathtt{f}}} \in Q_\tau$ .

When it is clear from the context, we denote $G.N$ , $G.E$ , and $G.\ell$ just by N, E, and $\ell$ . Moreover, we denote $G_i.N$ , $G_i.E$ , and $G_i.\ell$ by $N_i$ , $E_i$ , $\ell_i$ , and similarly for other typographical variants of G.

Example 36. Consider three classes $\mathtt{A},\mathtt{B},\mathtt{C}$ where $\mathtt{B}$ extends $\mathtt{A}$ and has two fields ${\mathord{\mathtt{f}}}$ and $\mathtt{g}$ of class $\mathtt{B}$ . We have that $\mathcal{K}=\{\top,\mathtt{A},\mathtt{B},\mathtt{C}\}$ with $\mathtt{B} \leq \mathtt{A}$ and $\mathtt{B}=[{\mathord{\mathtt{f}}} \mapsto \mathtt{B},\mathtt{g} \mapsto \mathtt{B}]$ , while $\mathtt{A}=\mathtt{C}=[]$ . Given variables $a_1,a_2,b_1,b_2,c \in \mathord{\mathit{Ide}}$ with $\tau=[a_1 \mapsto \mathtt{A},a_2 \mapsto \mathtt{A}, b_1 \mapsto \mathtt{B},b_2 \mapsto \mathtt{B},c \mapsto \mathtt{C}]$ , Figure 12A shows a pre-aliasing graph over $\tau$ .

Figure 12. A pre-aliasing graph for the type environment in Example 36.

We can extend $\ell$ from variables to qualified fields. Note that $\ell(v.{\mathord{\mathtt{f}}})$ only depends on $\ell(v)$ and not from v itself.

Definition 37 (Extension of $\ell$ ) Given a pre-aliasing graph $G = N \mathbin{\star} E \mathbin{\star} \ell$ , we extend $\ell$ on qualified fields $v.{\mathord{\mathtt{f}}} \in Q_\tau$ by

\begin{equation*}\ell(v.{\mathord{\mathtt{f}}}) = \begin{cases}n & \text{if $\ell(v) \neq \bot \wedge \ell(v)\xrightarrow{{\mathord{\mathtt{f}}}} n \in E$}\\\bot & \text{otherwise}\end{cases}\end{equation*}

When it helps readability, we will annotate nodes in aliasing graphs both with variables and qualified fields. See, for example, Figure 12B. Moreover, in the examples we will denote a node n by any identifier i such that $\ell(i)=n$ .

The idea of a pre-aliasing graph is that, given an identifier $i \in I_\tau$ , $\ell(i)=\bot$ means i is definitely ${\mathord{\mathtt{null}}}$ , while $\ell(i)=\ell(j)$ means that i and j are either both ${\mathord{\mathtt{null}}}$ or aliased. Since we aim at designing a domain which encodes definite aliasing and nullness, we define a preorder on pre-aliasing graphs such that $G_1 \preceq G_2$ when $G_1$ has more aliasing and nullness information than $G_2$ .

Definition 38 (Preordering on pre-aliasing graphs) Given two pre-aliasing graphs $G_1$ and $G_2$ , we say that $G_1 \preceq G_2$ iff

• • for each $i, i' \in I_\tau$ , $\ell_2(i)=\ell_2(i') \Rightarrow\ell_1(i)=\ell_1(i')$ ;

• • for each $i \in I_\tau$ , $\ell_2(i)=\bot \Rightarrow \ell_1(i)=\bot$ .

Note that, given their intended meaning, some pre-aliasing graphs contain redundant information. For example, nodes which are not labeled by any qualified identifiers may be removed. On the converse, two identifiers $i_1,i_2$ of incomparable types may be (weak) aliased only if they are both ${\mathord{\mathtt{null}}}$ . We therefore restrict our attention to the pre-aliasing graphs which present some additional regularity conditions.

Definition 39 (Aliasing graph) An aliasing graph is a pre-aliasing graph G such that, for all $n \in N$ , $\{ \tau(i) \mid i \in I_\tau \wedge \ell(i)=n \}$ is a nonempty chain. We denote by $\mathcal{G}_\tau$ the set of aliasing graphs over the type environment $\tau$ , by $\tau_G(n) = \bigwedge \{ \tau(i) \mid i \in I_\tau \wedge \ell(i)=n \}$ the type of the node n and by $\psi_G(n) = \bigwedge \{ \tau(w) \mid w \in dom(\tau) \wedge \ell(w)=n \}$ for the type that may be inferred by variables only, with the proviso that the meet of an empty set of classes is $\top$ .

Note that, although the type $\tau_G(n)$ depends on all the qualified identifiers labeling that node, the edges possibly departing from the nodes depend on $\psi_G(n)$ only. We could have also adopted another approach for pre-aliasing graphs and allow edges $n \xrightarrow{{\mathord{\mathtt{f}}}} m$ if ${\mathord{\mathtt{f}}}$ is a field in $\tau_G(n)$ . Although this could potentially improve precision, it comes at the cost of a greater complexity of several operations.

Example 40. The pre-aliasing graph in Figure 12A is not an aliasing graph due to the rightmost node $b_2 c$ since $\tau(b_2)=\mathtt{B}$ , $\tau(c)=\mathtt{C}$ but $\{\mathtt{B},\mathtt{C}\}$ is not a chain. This means that the variables $b_2$ and c can never be aliased (and thus are both ${\mathord{\mathtt{null}}}$ ).

4.1 Morphisms of aliasing graphs

We give in this section a different characterization of the preordering over aliasing graphs.

Definition 41 (Morphism of aliasing graphs) A morphism of aliasing graphs $h: G_1 \rightarrow G_2$ in $\mathcal{G}_\tau$ is a partial map $h: N_1 \nrightarrow N_2$ such that, for each $i \in I_\tau$ , $h(\ell_1(i))= \ell_2(i)$ .

This notion of morphism respects the intended meaning of aliasing graphs. If $h: G_1 \rightarrow G_2$ and $\ell_1(v) = \bot$ , then $\ell_2(v)=\bot$ . Moreover, if $\ell_1(v)=\ell_1(w)$ , then $\ell_2(v)=\ell_2(w)$ . Aliasing morphisms enjoys many interesting properties. In particular,

Theorem 42. Given two aliasing graphs $G_1, G_2$ , there exists a morphism from $G_2$ to $G_1$ if and only if $G_1 \preceq G_2$ . Moreover, the morphism, when it exists, is unique.

It is often easier to think in terms of morphism than to check whether Definition 38 holds: most of the proofs of the properties in this section use graph morphisms and the characterization in Theorem 42. Moreover, morphisms will be pivotal in Section 5 when comparing sharing and linearity information attached to different aliasing graphs.

Example 43. Let us consider the following classes:

class B; class A extends B { B l; B r; }

and the type environment $\tau = [a \mapsto \mathtt{A}, b \mapsto \mathtt{B}]$ . Consider the aliasing graphs $G_1$ and $G_2$ , respectively, in Figure 13A and B. There is a morphism $h: G_2 \to G_1$ given by $\{n_3 \mapsto n_1, n_6 \mapsto n_1, n_4 \mapsto n_2 \}$ , since

\begin{gather*} h(\ell_2(a))= h(n_3) = n_1 = \ell_1(a) \qquad h(\ell_2(b))= h(n_6) = n_1 = \ell_1(b) \\ h(\ell_2(a.{\mathord{\mathtt{l}}}))=h(n_4) = n_2 = \ell_1(a.{\mathord{\mathtt{l}}}) \qquad h(\ell_2(a.{\mathord{\mathtt{r}}}))=h(n_5)=\bot = \ell(a.{\mathord{\mathtt{r}}}) \end{gather*}

By Theorem 42, we have that $G_1 \preceq G_2$ .

Figure 13. Comparison of aliasing graphs. We have explicitly annotated each node with its identity.

4.2 The lattice of aliasing graphs

We now show that $\preceq$ for aliasing graphs has least upper bounds and greatest lower bounds, and we show how to build them.

We begin by defining a new aliasing graph $G_1 \curlyvee G_2$ , which we will later prove to be the least upper bound. In the definition, we use the inverse function $\ell^{-1}$ . Note that $\ell^{-1}$ may be different if we consider $\ell$ as the map $\ell: dom(\tau) \nrightarrow N$ in Definition 35 or as the map $\ell: I_\tau \nrightarrow N$ in Definition 37. When it is not specified, the latter is assumed.

Definition 44. Given $G_1, G_2\in \mathcal{G}_\tau$ , let $X=\ell_1^{-1}(N_1) \cup \ell_2^{-1}(N_2)$ and let $\sim \subseteq X \times X$ be the equivalence relation on $I_\tau$ such that $i \sim i' \iff \ell_1(i)=\ell_1(i') \wedge \ell_2(i)=\ell_2(i')$ . We define the aliasing graph $G_1 \curlyvee G_2 = N \mathbin{\star} E \mathbin{\star} \ell$ where

• • $N = X/\mathrm{\sim}$ is the set of equivalence classes of X;

• • for any $v \in dom(\tau)$ , $\ell(v)=[v]_\sim$ if $v \in X$ , $\ell(v)=\bot$ otherwise;

• • $S_1 \xrightarrow{{\mathord{\mathtt{f}}}} S_2 \in E$ iff there exists $v \in S_1$ s.t. $v.{\mathord{\mathtt{f}}} \in S_2$ .

Example 45. Let us consider the same classes and type environment of Example 43. Figure 14 shows an example of lub of aliasing graphs. Note that, even without knowing the class definitions, the graphs contain enough information to justify the result of the operation. For example, in Figure 14A, the fact that the left child of the node ab does not contain $b.{\mathord{\mathtt{l}}}$ means that that ${\mathord{\mathtt{l}}}$ is not a field of $\tau(b)$ , hence $\tau(a)$ is a subclass of $\tau(b)$ .

Figure 14. Least upper bound of aliasing graphs.

An analogous, although more complex, definition may be given for $G_1 \curlywedge G_2$ , which we will later prove to be the greatest lower bound of aliasing graphs.

Definition 46. Given $G_1, G_2\in \mathcal{G}_\tau$ , let $\sim \subseteq I_\tau \times I_\tau$ be the least equivalence relation on $I_\tau$ such that $\ell_1(i) =\ell_1( i') \vee \ell_2(i) =\ell_2( i') \Rightarrow i \sim i'$ . Moreover, let N be the largest subset of $I_\tau/\sim$ such that:

• • $N \subseteq \{[i]_\sim \mid i \in I_\tau, \tau([i]_\sim) \text{ is a chain and } [i]_{\sim} \subseteq \ell_1^{-1}(N_1) \cap \ell_2^{-1}(N_2)\}$ ;

• • if $[v]_\sim \notin N$ , then $[v.{\mathord{\mathtt{f}}}]_\sim \notin N$ .

We define the aliasing graph $G_1 \curlywedge G_2 = N \mathbin{\star} E \mathbin{\star} \ell$ where

• • $\ell: dom(\tau) \nrightarrow N$ such that $\ell(v)=[v]_\sim$ if $[v]_\sim \in N$ , $\ell(v)=\bot$ otherwise;

• • $S_1 \xrightarrow{{\mathord{\mathtt{f}}}} S_2 \in E$ iff there exists $v \in dom(\tau), v \in S_1$ s.t. $v.{\mathord{\mathtt{f}}} \in S_2$ .

The definition above is similar to the one for $\curlyvee$ : we start from defining an equivalence relation $\sim$ which propagates weak aliasing and we define $G_1 \curlywedge G_2$ whose nodes are equivalence classes of identifiers modulo $\sim$ . However, propagation of nullness is more complex. There are several situations which may force an identifier to be null.

• • It may be that $i_1 \sim i_2$ , but $i_2$ is null in either $G_1$ or $G_2$ . In this case, both $i_1$ and $i_2$ are forced to be null. This is the reason of the condition “ $[i]_{\sim} \subseteq \ell_1^{-1}(N_1) \cap \ell_2^{-1}(N_2)$ ” in the first clause of the definition for N.

• • Assume $\tau(i) = \kappa$ , $\tau(i_1)=\kappa_1$ , and $\tau(i_2)=\kappa_2$ , such that $\kappa_1 \leq \kappa$ , $\kappa_2 \leq \kappa$ with $\kappa_1$ and $\kappa_2$ incomparable. It may happen that $\ell_1(i)=\ell_1(i_1)$ and $\ell_2(i)=\ell_2(i_2)$ , which implies $i \sim i_1 \sim i_2$ . However, this forces i, $i_1$ , and $i_2$ to be null, since there is no object which is both an element of $\kappa_1$ and $\kappa_2$ . This is cared by the condition “ $\tau([i]_\sim)$ is a chain” in the first clause of the definition for N.

• • If variable v is forced to be null for one of the reasons above, then fields of v cannot exist. This is cared of by the second clause of the definition for N.

Example 47. Let us consider the following classes:

class A { A l; } class B extends A { A r; }

and the type environment $\tau = [a \mapsto \mathtt{A}, b \mapsto \mathtt{B}]$ . Figure 15 shows an example of glb of aliasing graphs.

Figure 15. Greatest lower bound of aliasing graphs.

The following theorem proves that $\curlyvee$ and $\curlywedge$ are actually the least upper bound and greatest lower bound of aliasing graphs.

Theorem 48. The preordered set $(\mathcal{G}_\tau, \preceq)$ has

• • a least element $\bot_\tau = \emptyset \mathbin{\star} \emptyset \mathbin{\star} \bot$ where $\bot$ is the always undefined map;

• • a greatest element $\top_\tau = I_\tau \mathbin{\star} E \mathbin{\star} {id}$ where $n_1 \xrightarrow{{\mathord{\mathtt{f}}}} n_2 \in E \iff n_1 = v \in dom(\tau) \wedge n_2= v.{\mathord{\mathtt{f}}} \in Q_\tau$ ;

• • a least upper bound $G_1 \curlyvee G_2$ for each $G_1, G_2 \in \mathcal{G}_\tau$ ;

• • a greatest lower bound $G_1 \curlywedge G_2$ for each $G_1, G_2 \in \mathcal{G}_\tau$ .

4.3 Projection

Several operations may be defined on aliasing graphs. Most of them will be introduced later, since they depend on the concrete semantics of our language. We introduce here only the operation of restriction of a graph to a subset of variables.

Definition 49 (Projection) Given a pre-aliasing graph G and a set of nodes X, we denote by $G|_X$ the tuple $X \mathbin{\star} E' \mathbin{\star} \ell'$ where

\begin{equation*} E' = E \cap (X \times \mathord{\mathit{Ide}} \times X) \qquad \ell'(v) = \begin{cases} \ell(v) & \text{if $\ell(v) \in X$},\\ \bot & \text{otherwise} \end{cases} \end{equation*}

It is immediate to check that $G|_X$ is a pre-aliasing graph. Given a pre-aliasing graph $G = N \mathbin{\star} E \mathbin{\star} \ell$ , a set of nodes $X \subseteq N$ is said to be backward closed when, for each $n \in X$ , if there exists $n' \xrightarrow{{\mathord{\mathtt{f}}}} n \in E$ , then $n' \in X$ . Given a set of nodes X, we denote by $\overleftarrow X$ the smallest backward closed set of nodes containing X. Symmetrically, we define forward closed sets and the forward closure operator $\overrightarrow X$ .

It turns out that if X is backward closed, then $G|_X \preceq G$ . Moreover, if G is an aliasing graph, $G|_X$ is too. More precisely, the following hold:

Proposition 50. If $G \in \mathcal{G}_\tau$ and $X \subseteq N$ is backward closed, then $G|_X \in \mathcal{G}_\tau$ . Moreover, for each $n \in X$ , $\tau_{G|_X}(n)= \tau_G(n)$ and $\psi_{G|_X}(n) = \psi_G(n)$ .

Proposition 51. If G is a pre-aliasing graph and $X \subseteq N$ is backward closed, then $G|_X \preceq G$ .

We will come back to this point when we introduce the abstract semantics.

4.4 The domain of aliasing graphs

Given a concrete state $\sigma \in \Sigma_\tau$ , we may abstract it into an aliasing graph which conveys the relevant information.

Definition 52. Given $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ , we define the abstraction of $\sigma$ as an aliasing graph $\alpha_a(\sigma) = G \in \mathcal{G}_\tau$ where

• • $N =\{ l \in \mathord{\mathit{Loc}} \mid \exists i \in I_\tau. \phi(i)=l \}$ ;

• • for each $v \in dom(\tau)$ , $\ell(v) = \phi(v)$ if $\phi(v) \neq {\mathord{\mathtt{null}}}$ , $\ell(v)=\bot$ otherwise;

• • $l \xrightarrow{{\mathord{\mathtt{f}}}} l' \in E$ iff there exists $v \in dom(\tau)$ such that $\ell(v)=l$ , $v.{\mathord{\mathtt{f}}} \in Q_\tau$ and $l.{\mathord{\mathtt{f}}}=l'$ .

The abstraction of a state $\sigma$ is essentially the representation of the environment and stores as an aliasing graph, limited to the locations reachable from a qualified identifier.

The following proposition shows that the abstraction of a concrete state is an aliasing graph.

Proposition 53. Given $\sigma = \phi \mathbin{\star} \mu \in \Sigma_\tau$ , $G = \alpha_a(\sigma)$ is an aliasing graph and, for each $i \in I_\tau$ , $\ell(i)=\phi(i)$ if $\phi(i) \neq{\mathord{\mathtt{null}}}$ , $\ell(i)=\bot$ otherwise.

We say that $G \in \mathcal{G}_\tau$ is a correct abstraction of $\sigma=\phi \mathbin{\star} \mu \in \Sigma_\tau$ iff $\alpha_a(\sigma) \preceq G$ . Note that if $\alpha_a(\sigma) \preceq G$ and $G.\ell(i)=\bot$ , then $\phi(i) = {\mathord{\mathtt{null}}}$ , hence $\ell$ may actually be used to represent definite nullness. Moreover, if $G.\ell(i_1)=G.\ell(i_2)$ , then either $\phi(i_1)=\phi(i_2) \in \mathord{\mathit{Loc}}$ or $\phi(i_1)=\phi(i_2)={\mathord{\mathtt{null}}}$ . Hence, $\ell$ actually encodes definite weak aliasing between variables.

The following propositions show that each aliasing graph can be viewed as the abstraction of a concrete state.

Proposition 54. Given $G \in \mathcal{G}_\tau$ , there exists $\sigma \in \Sigma_\tau$ s.t. $\alpha_a(\sigma)$ and G are equivalent, that is, $\alpha_a(\sigma) \sim~G$ .

The map $\alpha_a$ of Definition 52 may be lifted to the abstraction map of a Galois insertion from $\mathcal{P}(\Sigma_\tau)$ to $\mathcal{G}_\tau$ given by $\alpha_a(S)= \unicode{x0059}_{\sigma \in S} \alpha_a(\sigma)$ . The abstraction map induces the concretization map $\gamma_a: \mathcal{G}_\tau \rightarrow \mathcal{P}(\Sigma_\tau)$ , which maps aliasing graphs to the set of concrete states they represent. Its explicit definition, below, is straightforward:

\begin{equation*}\gamma_a(G) = \{ \sigma \in \Sigma_\tau \mid \alpha_a(\sigma) \preceq G \} .\end{equation*}

Theorem 55. The preorder $\preceq$ is the same preorder induced by $\gamma_a$ , that is, given $G_1, G_2 \in \mathcal{G}_\tau$ , $G_1\preceq G_2$ iff $\gamma_a(G_1) \subseteq \gamma_a(G_2)$ .

The above theorem may be considered the analogous of injectivity of $\gamma_a$ when the abstract domain is preordered instead of partially ordered. It allows to prove that $\gamma_a(G_1) \subseteq\gamma_a(G_2)$ by just checking $G_1 \preceq G_2$ .

5. $\mathsf{ALPS}$ Graphs

Aliasing graphs are a very concrete representation of the part of the program state which is reachable from variables through a single field access. Pair sharing and linearity, instead, summarize global properties of the state. We want to add possible pair sharing and possible nonlinearity information to an aliasing graph.

Definition 56. (Pre- $\mathsf{ALPS}$ graph) A pre- $\mathsf{ALPS}$ graph $\mathbb{G} = G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ is an aliasing graph G with a set $\mathit{sh} \subseteq \{ \{n,m\} \mid n,m \in N \}$ and a set $\mathit{nl} \subseteq N$ .

When it is clear from the context, we denote $\mathbb{G}.G, \mathbb{G}.\mathit{sh}, \mathbb{G}.\mathit{nl}$ by $G, \mathit{sh}, \mathit{nl}$ and $\mathbb{G}_i.G, \mathbb{G}_i.\mathit{sh}, \mathbb{G}_i.\mathit{nl}$ by $G_i, \mathit{sh}_i, \mathit{nl}_i$ . Similarly for other variants of $\mathbb{G}$ .

The set $\mathit{sh}$ in a pre- $\mathsf{ALPS}$ graph encodes possible pair sharing, while $\mathit{nl}$ encodes possible nonlinearity. In particular, two identifiers $i, j \in I_\tau$ may share when $\{ \ell(i), \ell(j) \} \in \mathit{sh}$ , while i may be nonlinear when $\ell(i) \in \mathit{nl}$ . This suggests to extend the preorder on aliasing graphs to $\mathsf{ALPS}$ graphs as follows:

Proposition 57. Pre- $\mathsf{ALPS}$ graphs are preordered by the relation $\preceq$ defined as:

\begin{equation*}\begin{split}\mathbb{G}_1 \preceq \mathbb{G}_2 \iff &G_1 \preceq G_2 \text{ and } \forall i \in I_\tau. \ \ell_1(i) \in \mathit{nl}_1 \Rightarrow \ell_2(i) \in \mathit{nl}_2\text{ and }\\&\quad \forall i,j \in I_\tau. \ \{\ell_1(i), \ell_1(j)\} \in \mathit{sh}_1 \Rightarrow \{\ell_2(i), \ell_2(j)\} \in \mathit{sh}_2 \enspace .\end{split}\end{equation*}

Not all the pre- $\mathsf{ALPS}$ graphs make sense, due to the way aliasing, nonlinearity, and sharing interact. In particular, some nonlinearity or sharing information is redundant, since it cannot happen in practice due to the class hierarchy under consideration: pairs $\{n,m\} \in \mathit{sh}$ such that classes $\tau_G(n)$ and $\tau_G(m)$ cannot share, or variables $n \in \mathit{nl}$ such that $\tau_G(n) \notin {NL}$ . This is formalized by the following:

Definition 58 (Graph compatibility) Given an aliasing graph $G \in \mathcal{G}_\tau$ , we say $\{n,m\} \subseteq N$ is G-SH-compatible if $(\tau_G(n) , \tau_G(m)) \in {SH}$ . We say $n \in N$ is G-NL-compatible if $\tau_G(n) \in {NL}$ . Sets $\mathit{sh} \subseteq \mathcal{P}_2(N)$ (and $\mathit{nl} \subseteq N$ ) are G-SH-compatible (G-NL-compatible) if all their elements are G-SH-compatible (G-NL-compatible).

We define a reduction operation which takes pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ and removes spurious sharing and linearity information.

Definition 59. (Reduced pre- $\mathsf{ALPS}$ graphs) Given a pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ , let $\mathit{sh}' \mathbin{\star} \mathit{nl}'$ be the sharing and nonlinearity information contained in $\mathit{sh} \mathbin{\star} \mathit{nl}$ which is G-SH and G-NL, compatible, that is,

\begin{align*} \mathit{sh}' &= \mathit{sh} \cap \{\{ n, m \} \in \mathcal{P}_2(N) \mid \{n,m\} \text{ is \textit{G}-SH-compatible} \} \enspace , \\ \mathit{nl}'&= \mathit{nl} \cap \{ n \mid n \text{ is \textit{G}-NL-compatible} \} \enspace . \end{align*}

We define the reduction of $\mathbb{G}$ to be the pre- $\mathsf{ALPS}$ graph $red(\mathbb{G})=G \mathbin{\star} \mathit{sh}' \mathbin{\star} \mathit{nl}'$ and we say that a pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ is reduced if $red(\mathbb{G})=\mathbb{G}$ .

Moreover, some sharing and nonlinearity information can be derived from other information. For example, if n is a node in G, then $\{n\}$ should be in $\mathit{sh}$ , otherwise any identifier i s.t. $\ell(i)=n$ is forced to be ${\mathord{\mathtt{null}}}$ and G could be simplified by removing the node n.

Definition 60. (Closed pre- $\mathsf{ALPS}$ graphs) We define a pre- $\mathsf{ALPS}$ graph $\mathbb{G}=G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ closed when it satisfies all the following properties:

1. (1). $n \in N \Rightarrow \{n\} \in \mathit{sh}$ ;

2. (2). there is a loop in G involving n $\Rightarrow n \in \mathit{nl}$ ;

3. (3). $\{ n,m \} \in \mathit{sh} \wedge n' \xrightarrow{{\mathord{\mathtt{f}}}} n \Rightarrow \{ n', m \} \in \mathit{sh}$ ;

4. (4). $n \xrightarrow{{\mathord{\mathtt{f}}}_1} m_1$ , $n \xrightarrow{{\mathord{\mathtt{f}}}_2} m_2$ , ${\mathord{\mathtt{f}}}_1 \neq {\mathord{\mathtt{f}}}_2$ , $\{m_1, m_2 \} \in \mathit{sh} \Rightarrow n \in \mathit{nl}$ ;

5. (5). $n \in \mathit{nl} \wedge n' \xrightarrow{{\mathord{\mathtt{f}}}} n \Rightarrow n' \in \mathit{nl}$ .

Point (1) is standard in sharing domains since each non-null variable shares with itself. Point (2) expresses the fact that any variable in a loop cannot be linear. Point (5) means that $\mathit{nl}$ is backward closed, while Point (3) is obvious generalization of backward closure to sharing pairs. Finally, Point (4) formalizes the fact that if two different fields of an object o share, then o is not linear.

Example 61 (Pre- $\mathsf{ALPS}$ graphs with loops) Consider the concrete state in Figure 16A. Locations $l_0$ and $l_1$ are nonlinear, since $l_0.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}=l_0$ and $l_1.{\mathord{\mathtt{r}}}.{\mathord{\mathtt{r}}}=l_1$ . This state is correctly abstracted by the pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ in Figure 16B, where nodes a and b are marked as nonlinear. On the contrary, the same concrete state is not correctly approximated by the pre- $\mathsf{ALPS}$ graph $\mathbb{G}'$ in Figure 16C, since the latter does not allow for the nonlinearity of a and b. Actually, the only concrete states which are correctly abstracted by $\mathbb{G}'$ are the ones where both a and b are null, since every other situation would violate either the aliasing constraints ( $a.{\mathord{\mathtt{r}}} = b$ and $b.{\mathord{\mathtt{r}}} =a$ ) or the linearity constraint. The Pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ is closed according to Definition 60, while $\mathbb{G}'$ is not and it is essentially not used, since it may be replaced by the empty pre- $\mathsf{ALPS}$ graph.

Figure 16. Two pre- $\mathsf{ALPS}$ graphs with a loop and a concrete state which is in the concretization of the Pre- $\mathsf{ALPS}$ graphs $\mathbb{G}$ in Figure 16B.

We want to restrict our attention only to those pre- $\mathsf{ALPS}$ graphs which do not contain any spurious information and where all sharing and nonlinearity information is explicit.

Definition 62 ( $\mathsf{ALPS}$ graph) An $\mathsf{ALPS}$ graph $\mathbb{G}$ is a pre- $\mathsf{ALPS}$ graph which is reduced and closed. We denote by $\mathsf{ALPS}_\tau$ the set of $\mathsf{ALPS}$ graphs over the type environment $\tau$ .

5.1 Projection

Analogously to aliasing graphs, we define a projection operator for $\mathsf{ALPS}$ graphs.

Definition 63 (Projection of pre- $\mathsf{ALPS}$ graphs) Given a pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ and $X \subseteq N$ backward closed, we denote by $\mathbb{G}|_X$ the pre- $\mathsf{ALPS}$ graph $G|_X \mathbin{\star} \mathit{sh}' \mathbin{\star} \mathit{nl}'$ where

\begin{equation*} \mathit{sh}' = \mathit{sh} \cap \mathcal{P}_2(X) \qquad \mathit{nl}' = \mathit{nl} \cap X \enspace . \end{equation*}

In the definition above, the hypothesis that X is backward closed is needed in order to ensure that $G|_X$ is an aliasing graph and not just a pre-aliasing graph. It is immediate to check that projection maps $\mathsf{ALPS}$ graphs to $\mathsf{ALPS}$ graphs. More specifically:

Proposition 64. If $\mathbb{G} \in \mathsf{ALPS}_\tau$ and $X \subseteq N$ is backward closed, then $\mathbb{G}|_X \in \mathsf{ALPS}_\tau$ .

Moreover, the following holds:

Proposition 65. If $\mathbb{G}$ is a pre- $\mathsf{ALPS}$ graph and $X \subseteq N$ is backward closed, then $\mathbb{G}|_X \preceq \mathbb{G}$ .

5.2 Up- and down-closures of pre- $\mathsf{ALPS}$ graphs

Given a pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ , the up-closure of $\mathbb{G}$ is a new pre- $\mathsf{ALPS}$ graph, obtained by adding derived sharing and nonlinearity information to the $\mathit{sh}$ and $\mathit{nl}$ components. Moreover, if $\mathbb{G}$ is reduced (i.e., it does not contain spurious sharing and nonlinearity elements which are not G-SH-compatible and G-NL-compatible, respectively), then the up-closure of $\mathbb{G}$ is an $\mathsf{ALPS}$ graph.

Definition 66. (Up-closure of pre- $\mathsf{ALPS}$ graphs) Given a pre- $\mathsf{ALPS}$ graph $\mathbb{G}= G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ , we define the up-closure of $\mathbb{G}$ as the pre- $\mathsf{ALPS}$ graph $cl^{\uparrow}(\mathbb{G}) = G \mathbin{\star} \mathit{sh}' \mathbin{\star} \mathit{nl}'$ such that $\mathit{sh}' \mathbin{\star} \mathit{nl}'$ is the smallest pair, under the component-wise ordering, which contains $\mathit{sh} \mathbin{\star} \mathit{nl}$ and $G \mathbin{\star} \mathit{sh}' \mathbin{\star} \mathit{nl}'$ is closed.

It is immediate to see that the up-closure of a pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ always exists and can be simply computed starting from $\mathit{sh} \mathbin{\star} \mathit{nl}$ and adding new elements according to the five properties in Definition 60. Note that the graph G does not change when computing the up-closure.

Symmetrically, we can define the down-closure as follows.

Definition 67. (Down-closure of pre- $\mathsf{ALPS}$ graphs) Given a pre- $\mathsf{ALPS}$ graph $\mathbb{G}$ , we define the down-closure of $\mathbb{G}$ as the pre- $\mathsf{ALPS}$ graph $cl^{\downarrow}(\mathbb{G})$ such that $cl^{\downarrow}(\mathbb{G})$ is the greatest pre- $\mathsf{ALPS}$ graph smaller than or equal to $\mathbb{G}$ and such that $cl^{\downarrow}(\mathbb{G})$ is closed.

Note that, differently from the up-closure, when computing the down-closure the graph G can possibly change, since some nodes could be removed. The next proposition shows how to compute the down-closure.

Theorem 68. Given a pre- $\mathsf{ALPS}$ graph $\mathbb{G}= G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ , the down-closure $cl^{\downarrow}(\mathbb{G})$ can be computed as follows. Let $\mathit{sh}^* \mathbin{\star} \mathit{nl}^*$ be the greatest pair, under the component-wise ordering, such that

1. (1). $\mathit{nl}^*= \mathit{nl} \setminus \{n \mid m \not\in \mathit{nl}^* \wedge m \xrightarrow{{\mathord{\mathtt{f}}}} n \in E\}$ ;

2. (2). $\mathit{sh}^* = \mathit{sh} \setminus \{ \{m_1, m_2 \} \mid n \not\in \mathit{nl}^*, n \xrightarrow{{\mathord{\mathtt{f}}}_1} m_1 \in E, n \xrightarrow{{\mathord{\mathtt{f}}}_2} m_2 \in E, {\mathord{\mathtt{f}}}_1 \neq {\mathord{\mathtt{f}}}_2\} \setminus \{\{ n, m \} \mid \{ n',m \} \not\in \mathit{sh}^* \wedge n' \xrightarrow{{\mathord{\mathtt{f}}}} n \in E \}$ .

Then, we have that

\begin{equation*}cl^{\downarrow}(\mathbb{G}) = (G \mathbin{\star} \mathit{sh}^* \mathbin{\star} \mathit{nl}^*)|_{N\setminus \overrightarrow X}\end{equation*}

where $X=\{n \mid n\not\in \mathit{nl}^*$ , there is a loop in G such that $n \xrightarrow{{\mathord{\mathtt{f}}}_1} \cdots \xrightarrow{{\mathord{\mathtt{f}}}_k} n \in E\} \cup \{n \mid \{n\} \not\in \mathit{sh}^*\}$ . Moreover, if $\mathbb{G}$ is closed w.r.t. red, then $cl^{\downarrow}(\mathbb{G})$ is an $\mathsf{ALPS}$ graph.

The down-closure shows the interaction between the three components of aliasing (which is encoded in the graph structure), sharing, and nonlinearity. It precisely describes how linearity and sharing information propagate to the other components.

The first point states that whenever a node m is linear, then all its children are linear too. The second point explains the interaction between sharing and linearity: when a node n is linear, then its children cannot share. Moreover, when a node n’ does not share with a node m, the same holds for the children of n’. Note that, whenever in a loop of the graph a node is linear, then all the nodes in the loop and all their children must be null. This is reflected in the projection on $N \setminus \overrightarrow X$ .

Example 69. Figure 17 shows the aliasing graph G and the $\mathsf{ALPS}$ graph $\mathbb{G} = G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ where

\begin{equation*} \mathit{sh}=\{ \{a b\}, \{c\}, \{a.{\mathord{\mathtt{r}}}\,c.{\mathord{\mathtt{l}}}\}, \{c.{\mathord{\mathtt{r}}}\}, \{a b, a.{\mathord{\mathtt{r}}}\,c.{\mathord{\mathtt{l}}} \}, \{c, a.{\mathord{\mathtt{r}}}\,c.{\mathord{\mathtt{l}}} \}, \{c, c.{\mathord{\mathtt{r}}} \}, \{ab, c\} \} \end{equation*}

\begin{equation*} \mathit{nl}=\{ c, c.{\mathord{\mathtt{r}}} \} \end{equation*}

In Figure 17B, nonlinearity is represented with a double circle, while sharing information is represented as follows:

Figure 17. Example of an $\mathsf{ALPS}$ graph.

• • the sharing information of the singletons $\{a b\}, \{c\}, \{a.{\mathord{\mathtt{r}}}\,c.{\mathord{\mathtt{l}}}\}, \{c.{\mathord{\mathtt{r}}}\}$ can be deduced from the existence of the nodes in the aliasing graph;

• • the sharing information of a node with its field, for example, $\{c, c.{\mathord{\mathtt{r}}} \}$ , can be deduced from the corresponding edge in the aliasing graph $c \xrightarrow{{\mathord{\mathtt{r}}}} c.r$ ;

• • additional sharing information is represented with a dotted line, for example, between the nodes a b and c.

5.3 The lattice of $\mathsf{ALPS}$ graphs

In order to define an abstract domain of $\mathsf{ALPS}$ graphs, we start by defining the least upper bound $\mathbb{G}_1 \curlyvee \mathbb{G}_2$ and greatest lower bound $\mathbb{G}_1 \curlywedge \mathbb{G}_2$ of $\mathsf{ALPS}$ graphs.

We use morphisms when we need to combine sharing and nonlinearity information coming from different graphs with different sets of nodes.

Definition 70. Let $\mathbb{G}_1$ and $\mathbb{G}_2$ be $\mathsf{ALPS}$ graphs. We define $\mathbb{G}= \mathbb{G}_1 \curlyvee \mathbb{G}_2$ as:

• • $G=G_1 \curlyvee G_2$ , with morphisms $h_1: G \rightarrow G_1$ and $h_2: G \rightarrow G_2$ ;

• • $\mathit{sh}= h_1^{-1}(\mathit{sh}_1) \cup h_2^{-1}(\mathit{sh}_2)$ and

• • $\mathit{nl} =h_1^{-1}(\mathit{nl}_1) \cup h_2^{-1}(\mathit{nl}_2)$ .

Example 71. Consider the $\mathsf{ALPS}$ graphs in Figure 18A and B. For ease of notation, we assume a node to be denoted by its label. The morphisms $h_1: G_1 \curlyvee G_2 \rightarrow G_1$ and $h_2: G_1 \curlyvee G_2 \rightarrow G_2$ are defined as follows:

\begin{equation*}h_1=[a \mapsto a b, b \mapsto a b, a.{\mathord{\mathtt{l}}} \mapsto a.{\mathord{\mathtt{l}}} ]\end{equation*}

\begin{equation*}h_2=[a \mapsto a, b \mapsto b, a.{\mathord{\mathtt{r}}} \mapsto a.{\mathord{\mathtt{r}}} ]\end{equation*}

We have that:

Figure 18. Least upper bound of $\mathsf{ALPS}$ graphs.

Definition 72. Let $\mathbb{G}_1$ and $\mathbb{G}_2$ be $\mathsf{ALPS}$ graphs. We define $\mathbb{G} = \mathbb{G}_1 \curlywedge \mathbb{G}_2$ as $\mathbb{G}=cl^{\downarrow}(\mathbb{G}')$ , where

• • $G' = G_1 \curlywedge G_2$ with morphisms $h_1:G_1 \rightarrow G$ and $h_2: G_2 \rightarrow G$ ;

• • $\mathit{sh}' = \{ \{n,m\} \in \mathcal{P}_2(N) \mid \forall k \in \{1,2\}\ h_k^{-1}(\{\{n,m\}\}) \subseteq \mathit{sh}_k \}$ ;

• • $\mathit{nl}' = \{ n \in N \mid \forall k \in \{1,2\}\ h_k^{-1}(n) \subseteq\mathit{nl}_k \}$ ;

Example 73. Consider the $\mathsf{ALPS}$ graphs in Figure 19A and B. For ease of notation, we assume a node to be denoted by its label. The morphisms $h_1: G_1 \rightarrow G_1 \curlywedge G_2 $ and $h_2: G_2 \rightarrow G_1 \curlywedge G_2 $ are defined as follows:

\begin{align*}h_1 & =[ ab \mapsto a b, b.{\mathord{\mathtt{r}}} \mapsto b.{\mathord{\mathtt{r}}}]\\ h_2 & =[a \mapsto a b, b \mapsto a b, b.{\mathord{\mathtt{r}}} \mapsto b.{\mathord{\mathtt{r}}} ]\end{align*}

We have that:

Figure 19. Greatest lower bound of $\mathsf{ALPS}$ graphs.

Theorem 74. The preordered set of $\mathsf{ALPS}$ graphs has

• • a least element $\bot_\tau \mathbin{\star} \emptyset \mathbin{\star} \emptyset$ ;

• • a greatest element $\top_\tau \,\mathbin{\star} \,\mathit{sh} \,\mathbin{\star} \, \mathit{nl}$ , where

• • $\mathit{sh} = \{\{ n, m \} \in \mathcal{P}_2(I_\tau) \mid (\tau(n),\tau(m)) \in {SH}\}$ and

• • $\mathit{nl} = \{ n \in I_\tau \mid \tau(n) \in {NL}\}$ ;

• • a least upper bound $\mathbb{G}_1 \curlyvee \mathbb{G}_2$ for each pair $\mathbb{G}_1$ and $\mathbb{G}_2$ of $\mathsf{ALPS}$ graphs;

• • a greatest lower bound $\mathbb{G}_1 \curlywedge \mathbb{G}_2$ for each pair $\mathbb{G}_1$ and $\mathbb{G}_2$ of $\mathsf{ALPS}$ graphs.

With an abuse of language, we denote the top and bottom of $\mathsf{ALPS}$ graphs for the domain environment $\tau$ with $\top_{\tau}$ and $\bot_\tau$ , which are the same symbols used for aliasing graphs. We omit the index $\tau$ when it is clear from or not relevant in the context.

5.4 The domain of $\mathsf{ALPS}$ graphs

Given a concrete state $\sigma \in \Sigma_\tau$ , we may abstract it into an aliasing graph which conveys the relevant information.

Definition 75 (Abstraction map on $\mathsf{ALPS}$ graph) Given $\sigma \in \Sigma_\tau$ , we define the abstraction $\alpha: \Sigma_\tau \rightarrow \mathsf{ALPS}$ as $\alpha(\sigma)= \alpha_a(\sigma) \mathbin{\star} \mathit{sh} \mathbin{\star}\mathit{nl}$ where

\begin{align*}\mathit{sh} &= \{ \{l_1, l_2\} \subseteq N \mid l_1 \text{ and } l_2 \text{ share in } \sigma \} \enspace ,\\\mathit{nl} &= \{ l \in N \mid l \text { is not linear in } \sigma \} \enspace .\end{align*}

We say $\mathbb{G}$ is a correct abstraction of $\sigma$ when $\alpha(\sigma) \preceq \mathbb{G}$ .

The abstraction of a state $\sigma$ is essentially the representation of the environment and stores as an $\mathsf{ALPS}$ graph, limited to the locations reachable from a qualified identifier.

Given $\sigma \in \Sigma_\tau$ and $\alpha(\sigma) \preceq \mathbb{G}$ , if $i_1, i_2 \in I_\tau$ share in $\sigma$ , then $\{\mathbb{G}.\ell(i_1), \mathbb{G}.\ell(i_2)\} \in \mathbb{G}.\mathit{sh}$ . Moreover, if $i \in I_\tau$ is nonlinear in $\sigma$ , then $\mathbb{G}.\ell(i) \in \mathbb{G}.\mathit{nl}$ . Hence, $\mathbb{G}$ actually encodes possible sharing and nonlinearity among variables and fields.

We may define a concretization map $\gamma: \mathsf{ALPS}_\tau \rightarrow \mathcal{P}(\Sigma_\tau)$ which maps $\mathsf{ALPS}$ graphs to the set of concrete states they represent as $\gamma(\mathbb{G}) = \{ \sigma \in \Sigma_\tau \mid \alpha(\sigma) \preceq \mathbb{G} \}$ . If we lift the map $\alpha$ in Definition 75 to an additive map $\alpha: \mathcal{P}(\Sigma_\tau) \rightarrow \mathsf{ALPS}_\tau$ as $\alpha(S)= \unicode{x0059}_{\sigma \in S} \alpha(\sigma)$ , then $\alpha$ and $\gamma$ form a Galois connection.

Proposition 76. (Concretization of $\mathsf{ALPS}$ graphs) The concretization map induced by the abstraction map $\alpha$ satisfies the following property:

\begin{equation*}\begin{split}\gamma(\mathbb{G}) = \big\{ \sigma \in \Sigma_\tau \mid\& \sigma \in\gamma_a(G), \\& \forall i \in I_\tau.\ i \text{ nonlinear in } \sigma \Rightarrow \ell(i) \in \mathit{nl},\\& \forall i,i' \in I_\tau.\ i \text{ share with } i' \text{ in } \sigma\Rightarrow \{ \ell(i), \ell(i')\} \in \mathit{sh} \big\} \enspace .\end{split}\end{equation*}

Note that $\mathsf{ALPS}$ -graphs do not form a Galois insertion with concrete states, as shown in the following example.

Example 77 ( $\mathsf{ALPS}$ -graphs do not form a Galois insertion) Consider the following set of classes:

class A { C f; } class B { C g; } class C { }

Since all classes may share among them, we have $SH=\{ (\kappa, \kappa') \mid \kappa, \kappa' \in \{A, B, C\} \}$ . Let $\tau$ be the type environment $\tau=\{ x \mapsto A, y \mapsto B \}$ and consider the $\mathsf{ALPS}$ -graph $\mathbb{G}$ given by:

It turns out that there is no set of states S such that $\alpha(S)=\mathbb{G}$ . This is because, due to the set of classes we have available, x and y may only share through the class C, that is, through the fields ${\mathord{\mathtt{f}}}$ and ${\mathord{\mathtt{g}}}$ . But according to $\mathbb{G}$ , ${\mathord{\mathtt{f}}}$ and ${\mathord{\mathtt{g}}}$ should be ${\mathord{\mathtt{null}}}$ , making sharing impossible. Therefore, $\alpha$ is not surjective and $\langle \alpha, \gamma \rangle$ is a Galois connection but not a Galois insertion.

Obtaining a Galois insertion would require the addition of new closure conditions on $\mathsf{ALPS}$ graphs. This is possible, but would make the definitions more cumbersome, and we have decided not to follow this line. While Galois insertions are more theoretical appealing since they do not contain redundant abstract elements, precise and efficient analysis can be obtained even without them. In the literature of numerical abstract domains (Cousot and Cousot 1976; Amato and Scozzari 2012) there are many examples of analysis which do not form a Galois insertion and not even a Galois connection, such as the polyhedral analysis of imperative programs (Cousot and Halbwachs 1978) and the parallelotope abstract domain (Amato et al. 2017), which nonetheless enjoy interesting completeness properties (Amato and Scozzari 2011)

In the next section, we will define the necessary operations on the domain of $\mathsf{ALPS}$ graphs in order to define an abstract semantics for sharing analysis. Note that, since the abstract domain is finite, we do not need a widening operator to ensure the termination of the analysis.

6. An Abstract Semantics on $\mathsf{ALPS}$

We present the abstract semantics on the domain $\mathsf{ALPS}_\tau$ . We provide a correct abstract counterpart for each concrete operator in the standard semantics. The abstract counterpart of an interpretation is an $\mathsf{ALPS}$ interpretation, defined as follows.

Definition 78. An $\mathsf{ALPS}$ interpretation I maps methods to total functions such that $I({\kappa.{\mathord{\mathtt{m}}}}):\mathsf{ALPS}_{\mathit{input}(\kappa.{\mathord{\mathtt{m}}})}\to \mathsf{ALPS}_{\mathit{output}(\kappa.{\mathord{\mathtt{m}}})}$ for each method $\kappa.{\mathord{\mathtt{m}}}$ .

6.1 Auxiliary operators

First of all, we introduce some auxiliary operators which will be used later in the abstract semantics for commands and expressions.

6.1.1 Pruning

Given a triple $\mathbb{G} = G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ (not necessarily an $\mathsf{ALPS}$ graph), the operation $\textsf{prune}$ removes extraneous nodes and adds inferred information:

\begin{equation*}\textsf{prune}(\mathbb{G})=cl^{\uparrow}(\mathbb{G}|_{N'})\end{equation*}

where $N' = \{\ell(w)\mid w\in dom(\tau)\} \cup \{n\mid w\in dom(\tau),\ell(w) \xrightarrow{{\mathord{\mathtt{f}}}} n\in E, {\mathord{\mathtt{f}}} \in dom(\tau(w)) \}$ .

6.1.2 Restriction

Consider the operation on concrete states which, given $S \subseteq \Sigma_\tau$ and a set of variables $V \subseteq dom(\tau)$ , returns the set of states in S restricted to the variables in V, that is,

\begin{equation*}S_{\Vert V} = \{\phi|_{V} \mathbin{\star} \mu \mid \phi \mathbin{\star} \mu \in S \} \subseteq\Sigma_{\tau|_{V}}\enspace .\end{equation*}

Starting from a correct abstraction $\mathbb{G} \in\mathsf{ALPS}_\tau$ of the set of states S, we would like to define a new abstraction $\mathbb{G}' \in \mathsf{ALPS}_{\tau|_{V}}$ which correctly approximates $S_{\Vert V}$ .

Definition 79 (Abstract restriction) Given $\mathbb{G} \in \mathsf{ALPS}_\tau$ and $V \subseteq dom(\tau)$ , we define $\mathbb{G}_{\Vert V} = \textsf{prune}( N \mathbin{\star} E \mathbin{\star} \ell |_{V} \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl})\enspace .$

Let $W=V \cup \{v.{\mathord{\mathtt{f}}} \in Q_\tau \mid v \in V\}$ and let $\mathbb{G}_{\Vert V}= N' \mathbin{\star} E' \mathbin{\star} \ell' \mathbin{\star} \mathit{sh}' \mathbin{\star} \mathit{nl}'$ . Since $\ell'$ is obtained by restricting $\ell$ to the variables in V, we have that for any $x \in dom(\tau) \setminus V$ , $\ell'(x)=\ell| _{V} (x)=\bot$ . Then for each $n' \in N'$ , ${\ell'}^{-1} (n) \subseteq W$ and all the nodes in $\mathbb{G}$ which are not the image of a qualified identifier in W are removed from the graph. By construction and since $\mathbb{G} \in \mathsf{ALPS}_\tau$ , we have that N’ is backward closed and $\mathbb{G}_{\Vert V} \in \mathsf{ALPS}_{\tau|_{V}}$ .

Proposition 80. For each $\mathbb{G} \in \mathsf{ALPS}_\tau$ and $V\subseteq dom(\tau)$ , $\gamma(\mathbb{G})_{\Vert V} \subseteq \gamma(\mathbb{G}_{\Vert V})$ .

6.1.3 Nullness propagation

Consider the operation on concrete states which, given $S \subseteq \Sigma_\tau$ and an identifier $i \in I_\tau$ , returns the subset of those states in S where i is ${\mathord{\mathtt{null}}}$ , that is,

\begin{equation*}S_{|i={\mathord{\mathtt{null}}}} = \{ \sigma = \phi \mathbin{\star} \mu \in S \mid \phi(i) = {\mathord{\mathtt{null}}} \} \enspace .\end{equation*}

If $\mathbb{G}$ is a correct abstraction of S, it is also a correct abstraction of $S_{|i={\mathord{\mathtt{null}}}}$ , but we would like to refine $\mathbb{G}$ into a more precise abstract state which still correctly approximates $S_{|i={\mathord{\mathtt{null}}}}$ . This suggests the following definition.

Definition 81 (Abstract nullness propagation) Given $\mathbb{G} \in \mathsf{ALPS}_\tau$ and an identifier $i \in I_\tau$ , we define $\mathbb{G}_{|i={\mathord{\mathtt{null}}}} = \mathbb{G}|_{N_v}$ where $N_v = N \setminus \overrightarrow{\{\ell(i)\}}$ .

In $\mathbb{G}_{|i={\mathord{\mathtt{null}}}}$ , since the identifier i is forced to be ${\mathord{\mathtt{null}}}$ , all the nodes reachable from i need to be removed from the graph since they do not really exist. Given that $N \setminus \overrightarrow{\{\ell(i)\}}$ is backward closed, we know from Propositions 64 and 65 that $\mathbb{G}_{|i={\mathord{\mathtt{null}}}}$ is an $\mathsf{ALPS}$ graph and $\mathbb{G}_{|i={\mathord{\mathtt{null}}}} \preceq \mathbb{G}$ .

Nullness propagation is a special case of greatest lower bound between $\mathsf{ALPS}$ graphs, as proved in the following:

Proposition 82. For each $\mathbb{G} \in \mathsf{ALPS}_\tau$ and $i \in I_\tau$ , $\mathbb{G}_{|i={\mathord{\mathtt{null}}}} = \mathbb{G} \curlywedge \top_{|i={\mathord{\mathtt{null}}}}$ .

In turn, this allows us to prove that:

Proposition 83. For each $\mathbb{G} \in \mathsf{ALPS}_\tau$ and $i \in I_\tau$ , $\gamma(\mathbb{G})_{|i={\mathord{\mathtt{null}}}} \subseteq \gamma(\mathbb{G}_{|i={\mathord{\mathtt{null}}}})$ .

In the rest of the paper, given $i, j \in I_\tau$ , we use $\mathbb{G}_{|i={\mathord{\mathtt{null}}}, j={\mathord{\mathtt{null}}}}$ as a short form for $(\mathbb{G}_{|i={\mathord{\mathtt{null}}}})_{|j={\mathord{\mathtt{null}}}}$ .

6.1.4 Restriction to aliasing

Consider the operation on concrete states which, given $S \subseteq \Sigma_\tau$ and two variables v, w, returns the subset of those states in S where v is weakly aliased with w, that is,

\begin{equation*}S_{|v=w} = \{ \sigma = \phi \mathbin{\star} \mu \in S \mid \phi(v) = \phi(w) \} \enspace .\end{equation*}

Similarly to what we have done in the previous section, we aim to determine a correct approximation of $S_{|v=w}$ . Given $\mathbb{G} \in \mathsf{ALPS}_\tau$ , we define

\begin{equation*} \begin{array}{ll}\mathbb{G}_{|v=w} = &\mathbb{G} \curlywedge \top_{v=w}\end{array}\end{equation*}

where

\begin{equation*}\top_{v=w} = \begin{cases}\textsf{prune}(\top.N \mathbin{\star} \top.E \mathbin{\star} \top.\ell[w \mapsto v] \mathbin{\star} \top.\mathit{sh} \mathbin{\star} \top.\mathit{nl}) &\text{if $\tau(v)\leq \tau(w)$;}\\\textsf{prune}(\top.N \mathbin{\star} \top.E \mathbin{\star} \top.\ell[v \mapsto w] \mathbin{\star} \top.\mathit{sh} \mathbin{\star} \top.\mathit{nl})&\text{if $\tau(w) < \tau(v)$;}\\\top_{|v={\mathord{\mathtt{null}}}, w={\mathord{\mathtt{null}}}} & \text{otherwise.}\end{cases}\end{equation*}

Proposition 84. For each $\mathbb{G} \in \mathsf{ALPS}_\tau$ and $v, w \in dom(\tau)$ , $\gamma(\mathbb{G})_{|v=w} \subseteq \gamma(\mathbb{G}_{|v=w})$ .

In the rest of the paper, we will use $\mathbb{G}_{|v_1=w_1,\ldots,w_n=w_n}$ as a shorthand for $((\mathbb{G}_{|v_1=w_1})\ldots)_{|v_n=w_n}$ .

6.2 Abstract semantics for expressions

The abstract semantics specifies how each expression $\mathit{exp}$ transforms input abstract states $\mathbb{G} = N \mathbin{\star} E \mathbin{\star} \ell \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ into final abstract states $\mathbb{G}' = N' \mathbin{\star} E' \mathbin{\star} \ell' \mathbin{\star} \mathit{sh}' \mathbin{\star}\mathit{nl}'$ where ${\mathord{\mathtt{res}}}$ holds the $\mathit{exp}$ ’s value. Abstract semantics for expressions (and later commands) is given compositionally on their syntax.

Definition 85. Let $\tau$ describe the variables in scope and I be an $\mathsf{ALPS}$ interpretation. Figure 20 defines the $\mathsf{ALPS}$ semantics for expression (except method calls) $\mathcal{S\!E}_{{\tau}}^{I}\unicode{x0301A}{\mathit{exp}}\unicode{x0301B}:\mathsf{ALPS}_\tau\to\mathsf{ALPS}_{\tau+\mathit{exp}}$ .

Figure 20. The $\mathsf{ALPS}$ interpretation for expressions.

We briefly explain the behavior of the abstract semantic operators with respect to the corresponding concrete ones. The concrete semantics of ${\mathord{\mathtt{null}}}\ \kappa$ stores ${\mathord{\mathtt{null}}}$ in the variable ${\mathord{\mathtt{res}}}$ . Therefore, in the abstract semantics, we only need to add the new variable ${\mathord{\mathtt{res}}}$ into the type environment, without modifying the abstract state.

The concrete semantics of $\mathtt{new} \ \kappa$ stores in ${\mathord{\mathtt{res}}}$ a reference to a new object o, whose fields are ${\mathord{\mathtt{null}}}$ . The other variables do not change. Since o is only reachable from ${\mathord{\mathtt{res}}}$ , variable ${\mathord{\mathtt{res}}}$ shares with itself only and is clearly linear. Therefore, we only need to add a new node labeled with ${\mathord{\mathtt{res}}}$ and the corresponding sharing singleton, without affecting nonlinearity information.

The concrete semantics of v simply makes ${\mathord{\mathtt{res}}}$ an alias for v. Since the types of v and ${\mathord{\mathtt{res}}}$ coincide, we only need to add the variable v to the same node of ${\mathord{\mathtt{res}}}$ . The other variables are unchanged.

When $v={\mathord{\mathtt{null}}}$ , then $\mathtt{(}\kappa\mathtt{)}v$ behaves like ${\mathord{\mathtt{null}}}\ \kappa$ . If $\kappa$ and the type of v are not compatible, then $\mathtt{(}\kappa\mathtt{)}v$ only returns a nonfailed state when $v={\mathord{\mathtt{null}}}$ . Therefore, in the abstract semantics, $\mathtt{(}\kappa\mathtt{)}v$ restricts the input graph $\mathbb{G}$ to those states where $v={\mathord{\mathtt{null}}}$ . In the other cases, the cast $\mathtt{(}\kappa\mathtt{)}v$ stores in ${\mathord{\mathtt{res}}}$ the value of v. We use an auxiliary operator $add(\mathbb{G},n,\kappa)$ , explained in the following section, which adds the label ${\mathord{\mathtt{res}}}$ to the node n, and possibly adds new nodes for the fields of ${\mathord{\mathtt{res}}}$ which are not fields of $\psi_G(n)$ . In this case, we can exploit the notion of linearity. In fact, when v is linear, we know that fields of ${\mathord{\mathtt{res}}}$ cannot share with each other and are linear.

The concrete semantics of $v.{\mathord{\mathtt{f}}}$ stores in ${\mathord{\mathtt{res}}}$ the value of the field ${\mathord{\mathtt{f}}}$ of v, provided v is not ${\mathord{\mathtt{null}}}$ . When $v.{\mathord{\mathtt{f}}}$ is not ${\mathord{\mathtt{null}}}$ , this essentially amounts to the same procedure of the previous case.

6.2.1 Assignment to a node

The auxiliary operator $add(\mathbb{G}, n, \kappa)$ adds a new variable ${\mathord{\mathtt{res}}}$ of type $\kappa$ as an alias of the node $n \in N$ . The operator also adds children of ${\mathord{\mathtt{res}}}$ when needed to have an $\mathsf{ALPS}$ graph.

\begin{equation*}add(\mathbb{G},n,\kappa) = \begin{cases} \bot & \text{if$\{\tau_G(n), \kappa\}$ is not a chain}\\cl^{\uparrow}(\mathbb{G}')& \text{otherwise}\end{cases}\end{equation*}

Given $\mathbb{G} = G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ , in order to define $\mathbb{G}'$ , let $\kappa' = \psi_{G} (n)$ be the inferred type for node n in $\mathbb{G}$ (from variables only) and $F' = dom (\kappa)\setminus dom (\kappa') = \{{\mathord{\mathtt{f}}}_1,\ldots,{\mathord{\mathtt{f}}}_m \}$ be the set of the new fields in class $\kappa$ which are not currently considered in $\mathbb{G}$ ; let also $\{n_{{\mathord{\mathtt{f}}}_1},\ldots, n_{{\mathord{\mathtt{f}}}_m} \}$ be a set of fresh nodes, that is, such that $\{n_{{\mathord{\mathtt{f}}}_1},\ldots, n_{{\mathord{\mathtt{f}}}_m} \} \cap N=\emptyset$ ; then:

Definition of G’ is straightforward: we just add the new nodes as children of node n, each one pointed through the corresponding field in F’. If n is nonlinear, then all new nodes are nonlinear, all new nodes share among them and with other nodes n’ sharing with n. This procedure might add spurious sharing or nonlinearity information: we solve this problem by filtering with SH and NL.

When n is linear, then all new nodes are linear, do not share among them, and do not share with any node n’ reachable from n through a nonempty sequence of fields $ {\mathord{\mathtt{f}}}'_1, \ldots, {\mathord{\mathtt{f}}}'_k$ in E, but share with all the other nodes sharing with n.

6.3 Abstract semantics for commands

In the concrete semantics, each command $\mathit{com}$ transforms an initial state into a final state. On the abstract domain, it transforms an initial $\mathsf{ALPS}$ graph $G \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl}$ into an $\mathsf{ALPS}$ graph $G' \mathbin{\star} \mathit{sh}'\mathbin{\star} \mathit{nl}'$ .

Definition 86. Let $\tau$ describe the variables in scope and I be an $\mathsf{ALPS}$ interpretation. Figures 21–23 show the $\mathsf{ALPS}$ semantics for commands $\mathcal{SC}_{{\tau}}^{{I}}\unicode{x0301A}{{\mathit{com}}}\unicode{x0301B}: \mathsf{ALPS}_\tau \to \mathsf{ALPS}_\tau$ .

Figure 21. The $\mathsf{ALPS}$ interpretation for simple commands.

Figure 22. The $\mathsf{ALPS}$ interpretation for assignment to field.

Figure 23. The $\mathsf{ALPS}$ interpretation for method calls. The auxiliary function $match_{v.{\mathord{\mathtt{m}}}}$ is defined later in Figure 24.

The concrete semantics of $v\mathbin{\mathtt{\unicode{x02254}}}\mathit{exp}$ evaluates $\mathit{exp}$ and stores its result into v. Thus, the final abstract state is obtained by first computing $\mathcal{S\!E}_{\tau}^{I}\unicode{x0301A}{\mathit{exp}}\unicode{x0301B}$ and then renaming ${\mathord{\mathtt{res}}}$ into v. Some of the nodes may become unlabeled and must be removed. This is accomplished by the auxiliary operation $\textsf{prune}$ which removes unnecessary information, in particular unlabeled nodes and fields which are not in the declared type of the variables.

To determine a correct approximation of the conditional “ $\mathtt{if\ }v\\mathtt{=null}$ ” we check whether $\ell(v)=\bot$ . If this is the case, then we know that v is null and we evaluate $com_1$ . Otherwise, we evaluate both branches and compute the lub. When evaluating the first branch, we may improve precision by using the auxiliary operator $\mathbb{G}_{|v={\mathord{\mathtt{null}}}}$ (Section 6.1.3) which returns a correct approximation of the program states $\{ \phi \mathbin{\star} \mu \mid \alpha(\phi\mathbin{\star} \mu) \preceq \mathbb{G} \wedge \phi(v)={\mathord{\mathtt{null}}} \}$ , that is, the states correctly approximated by $\mathbb{G}$ where v is ${\mathord{\mathtt{null}}}$ . Note that, since our domain does not model definite non-nullness, there is no way to define a projection $\mathbb{G}_{|v\neq{\mathord{\mathtt{null}}}}$ to improve the input for $\mathcal{SC}_{{\tau}}^{{I}}\unicode{x0301A}{{\mathit{com}_2}}\unicode{x0301B}$ as in $\mathcal{SC}_{{\tau}}^{{I}}\unicode{x0301A}{{\mathit{com}_1}}\unicode{x0301B}(\mathbb{G}_{|v={\mathord{\mathtt{null}}}})$ .

Similarly for the conditional “ $\mathtt{if\ }v\ \mathtt{=}\ w$ ” where we use another auxiliary operator $\mathbb{G}_{|v=w}$ (Section 6.1.4) which returns a correct approximation of the set of program states $\{ \phi \mathbin{\star} \mu \mid \alpha(\phi \mathbin{\star} \mu) \preceq \mathbb{G} \wedge\phi(v)=\phi(w) \}$ . Again, since our domain does not model definite not aliasing, we cannot improve the input for the second branch.

The composition of commands is denoted by functional composition over $\mathsf{ALPS}$ , where the identity map $\lambda s\in \mathsf{ALPS}_\tau.s$ is needed when $p=0$ . The evaluation of $v.{\mathord{\mathtt{f}}} \mathbin{\mathtt{\unicode{x02254}}} \mathit{exp}$ in Figure 22 is the most complex operation of the abstract semantics. Although it may seem similar to the assignment $v \mathbin{\mathtt{\unicode{x02254}}} \mathit{exp}$ , we must take into account that v might be aliased to many different nodes. The candidates are those variables, denoted by $V_{comp}$ , which share with $\ell(v)$ and have compatible types. For each node labeled by a variable in $V_{comp}$ , we add a new fresh node in $N_{new}$ pointed by an edge (labeled by the field ${\mathord{\mathtt{f}}}$ ) in $E_{new}$ . Finally, all possible sharing and nonlinearity are added. A slightly different treatment is devoted to the special case when the result of the expression is definitely ${\mathord{\mathtt{null}}}$ .

6.4 Abstract semantics of method call

The concrete semantics of the method call $v.\mathtt{m(}v_1,\ldots,v_n\mathtt{)}$ builds an input state containing the local variables $w_1,\ldots,w_n$ and the special variable $\mathit{this}$ , and executes the method body. In order to improve the precision of methods call, we also use a copy of the local variables $w'_1,\ldots,w'_n$ which will be used when returning from the method call to match the original variables $v_1,\ldots,v_n$ . This allows a change to the object pointed by $w_i$ to be distinguished from a change to $w_i$ itself.

When a method $v.{\mathord{\mathtt{m}}}$ is called, the class of v is inspected and the correct overloaded method for ${\mathord{\mathtt{m}}}$ is selected. The abstract domain contains only a partial information on the runtime class of v, since we only know that the class of v must be a superclass of the class of any variable aliased with v, namely a superclass of $\tau_G(\ell(v))$ . We exploit this information in computing the abstract semantics of a method call in Figure 23. In practice, we conservatively assume that every method ${\mathord{\mathtt{m}}}$ in any subclass of $\tau_G(\ell(v))$ may be called. Note that methods defined only in superclasses of $\kappa$ are already considered in $\kappa$ .

When exiting from a method call, we need to rename ${\mathord{\mathtt{out}}}$ into ${\mathord{\mathtt{res}}}$ since, from the point of view of the caller, the returned value of the callee ( ${\mathord{\mathtt{out}}}$ ) is the value of the method call expression ( ${\mathord{\mathtt{res}}}$ ). We use an auxiliary operation $match_{v.{\mathord{\mathtt{m}}}}$ which, given an initial and final state, updates the initial state trying to guess a possible matching of variables in the abstract states. The definition of $match_{v.{\mathord{\mathtt{m}}}}$ is given in Figure 24.

Figure 24. The $match_{v.{\mathord{\mathtt{m}}}}$ auxiliary operation.

Theorem 87. The abstract semantics formalized in Figures 20–24 is correct wrt the concrete semantics in Section 2.2.2.

Analougously to the concrete case, we may define an abstract transformer which, given a $\mathsf{ALPS}$ interpretation I, returns a new $\mathsf{ALPS}$ interpretation I’ such that

\begin{equation*}\begin{array}{lll}I'(\kappa.{\mathord{\mathtt{m}}}) &=&(\lambda \mathbb{G} \in \mathsf{ALPS}_{\mathit{scope}(\kappa.{\mathord{\mathtt{m}}})}.\mathbb{G} _{\Vert dom(\mathit{output}(\kappa.{\mathord{\mathtt{m}}}))}) \ \circ \\&& \mathcal{SC}_{{\mathit{scope}(\kappa.{\mathord{\mathtt{m}}})}}^{{I}}\unicode{x0301A}{{\mathit{body}(\kappa.{\mathord{\mathtt{m}}})}}\unicode{x0301B} \ \circ \\ && (\lambda \mathbb{G} \in \mathsf{ALPS}_{\mathit{input}(\kappa.{\mathord{\mathtt{m}}})}. N \mathbin{\star} E \mathbin{\star} \ell' \mathbin{\star} \mathit{sh} \mathbin{\star} \mathit{nl})\end{array}\end{equation*}

where $\ell' = \ell[w'_1 \mapsto \ell(w_1),\ldots, w'_n \mapsto \ell(w_n)]$ .

The new interpretation returned by the abstract transformer is computed by first adding primed variables which are used to hold a copy of the original actual parameters, then evaluating the body of the method and finally restricting the graph to the output variables. The abstract denotational semantics is the least fixpoint of this transformer.

Theorem 88. The abstract denotational semantics is correct wrt the concrete one.

Example 89. Consider the method $\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}$ in Section 1.4, where

\begin{align*}\begin{split}\mathit{scope}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})=[ & {\mathord{\mathtt{this}}} \mapsto \mathtt{Tree}, n\mapsto \mathtt{Integer}, n' \mapsto \mathtt{Integer},m \mapsto \mathtt{Integer},{\mathord{\mathtt{out}}} \mapsto \mathtt{Tree}].\end{split}\end{align*}

We can compute a new $\mathsf{ALPS}$ interpretation from the least informative $\mathsf{ALPS}$ interpretation $I_\bot(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}}) = \lambda\mathbb{G}.\bot_{{\mathord{\mathtt{out}}}(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})}$ :

\begin{equation*}\begin{split} I^1(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})(\mathbb{G})= & N \cup \{n_{out}\} \mathbin{\star} E \mathbin{\star} {} \ell[n' \mapsto \ell(n), out \mapsto n_{out}] \mathbin{\star} \mathit{sh} \cup \{\{n_{out}\}\} \mathbin{\star} \mathit{nl} \end{split}\end{equation*}

Now, starting from $I^1(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})$ , we can compute a new interpretation as follows:

\begin{equation*}\begin{split} &I^2(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})(\mathbb{G})= N \cup \{n_{out}, n_{out.l},n_{out.r},\} \mathbin{\star} {}\\ & \qquad E \cup \{n_{out} \xrightarrow{{\mathord{\mathtt{l}}}} n_{out.l}, n_{out} \xrightarrow{{\mathord{\mathtt{r}}}} n_{out.r} \}\mathbin{\star} {} \\ & \qquad \ell[n' \mapsto \ell(n), out \mapsto n_{out} ] \mathbin{\star} {}\\ & \qquad \mathit{sh} \cup \{\,\{n_{out}\}, \{n_{out.l}\},\{n_{out.r}\}, \{n_{out},n_{out.l} \}, \{n_{out},n_{out.r} \}\, \}\mathbin{\star} \mathit{nl} \end{split}\end{equation*}

which is the least fixpoint. Relatively to the case $\ell(n)\neq {\mathord{\mathtt{null}}}$ , the abstract states $I^1(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})(\mathbb{G})$ and $I^2(\mathtt{Tree}.{\mathord{\mathtt{makeTree}}})(\mathbb{G})$ are depicted in Figure 25. From this graph, it appears that the tree generated by this method is linear and does not share with ${\mathord{\mathtt{this}}}$ (the object on which we call the makeTree method). Moreover since n and n’ are aliased we know that the method does not modify the variable n.

Figure 25. $\mathsf{ALPS}$ interpretations for the makeTree method.

7. Related Work

Sharing properties has been deeply studied for logic programs, see for instance: Jacobs and Langen (1992), Hans and Winkler (1992), Muthukumar and Hermenegildo (1992), Codish et al. (1999), Bagnara et al. (2002), and Amato and Scozzari (2009). The large literature on this topic has been the starting point for designing our enhanced abstract domain for sharing analysis. In particular, the use of a linearity property, for example, Codish et al. (1991), Hans and Winkler (1992), Muthukumar and Hermenegildo (1992), King (1994), and Amato and Scozzari (2010, 2014), has proved to be very useful when dealing with sharing information (see Bagnara et al. 2005 for a comparative evaluation).

Outside of the logic programming community, sharing information is generally regarded as a by-product of shape analysis. One of the first papers that explicitly deals with sharing information is Jones and Muchnick (1979), which presents a combined intra-procedural analysis of aliasing, reachability, and cyclicity for imperative and functional languages with records. The focus of their analysis is not pair sharing, but detecting the set of shared nodes, that is, heap cells which may be reached by variables using at least two different paths. Shared nodes and cyclicity are used to optimize memory management.

The property of sharing for object-oriented languages has been studied in a few works. Secci and Spoto (2005a) propose a simple domain of pair sharing for a simple Java-like language and MÉndez-Lojo and Hermenegildo (2008) extend this domain proposing a combined analysis of set sharing, nullness, and classes for exactly the same language. The main differences of our paper w.r.t. these proposals are

• • the $\mathsf{ALPS}$ abstract domain encodes linearity and aliasing information, in addition to sharing;

• • the analysis is field sensitive, that is, information is encoded at the level of the fields of the objects.

The analysis in Secci and Spoto (2005a) has also been refined by Zanardini (2018) which proposes a field-sensitive sharing analysis for a very similar language. Linearity information is not exploited in this paper either.

Pollet et al. (2001) propose a framework for the analysis of object-oriented languages and introduce two abstract domains for definite aliasing and possible aliasing, respectively. The abstract objects of these domains are similar to aliasing graphs, but without being restricted to two levels. Termination is guaranteed by widening. These domains may be enriched by providing type information for the leaves of the graphs. However, they do not consider sharing or linearity properties.

In the context of pure functional programming with no destructive updates, sharing is just an implementation detail and has not impact on the behavior of the program. Nonetheless, sharing analysis may help in optimizing program execution. For example, the first part of Jones and Muchnick (1979) deals with sharing in pure functional programs in order to avoid the use of garbage collection and reference counting.

More recently, PeÑa-MarÍ et al. (2006) present a pair-sharing analysis for SAFE, which is a functional language with explicit control for copy and destruction of data structures. The result of the analysis is used during type checking. Due to the particular features of the programming language, the sharing analysis distinguishes between generic sharing and sharing of recursive substructures (e.g., two lists share a recursive substructure when they have a common tail). The analysis is field insensitive and cannot represent neither definite aliasing nor definite nullness and linearity. This analysis has been vastly improved in Montenegro et al. (2015), where each pair of sharing variables is annotated with the set of possible paths through which the sharing may happen. Although definite aliasing and definite nullness are still not representable in the new domain, definite linearity is inferable by the extended pair-sharing information: if x shares with itself only through the empty path, then x is linear.

8. Conclusions

We propose the new abstract domain $\mathsf{ALPS}$ which combines aliasing, linearity, and sharing analysis for an object-oriented language and provide all the necessary abstract operations.

The combination with linearity information allows us to improve the precision of the analysis in blocks of assignments, method calls, and thus on recursion. This is a fundamental issue that has not been considered in any previous analysis. We have shown in Section 1.4 a simple example where linearity plays a fundamental role in proving that two subtrees do not share. More generally, an important point is that linearity information allows us to distinguish a tree from a direct acyclic graph (DAG). For instance, the result of makeTree in Figure 8 is a tree. However, the abstract representation of a tree in any abstract domain containing only information about reachability, sharing, acyclicity, nullness, and aliasing (and the corresponding negated properties such as cyclicity, non-nullness, etc.) cannot be distinguished from the abstraction of a DAG. For example, the data structure ${\mathord{\mathtt{t2}}}$ :

Tree t2 = new Tree ()t2.l = new Tree ()t2.r = new Tree ()t2.l.l = new Tree ()t2.l.r = t2.l.l

has the same sharing, acyclicity, nullness, etc. properties of a tree, but ${\mathord{\mathtt{t2}}}$ is not linear, while ${\mathord{\mathtt{t}}}$ in Figure 8 is linear. At the end of the method useTree, ${\mathord{\mathtt{left}}}$ is equal to ${\mathord{\mathtt{t}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}$ , ${\mathord{\mathtt{right}}}$ is ${\mathord{\mathtt{t}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{r}}}$ , but they do not share since ${\mathord{\mathtt{t}}}$ is a tree. However, ${\mathord{\mathtt{t2}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{l}}}$ and ${\mathord{\mathtt{t2}}}.{\mathord{\mathtt{l}}}.{\mathord{\mathtt{r}}}$ share. Linearity allows to distinguish these two situations. None of the works discussed in Section 7 can distinguish a DAG from a tree, with the exception of Montenegro et al. (2015) which cannot be directly applied to a Java-like language since it does not support updates.

Regarding modularity of the analysis, although the most precise results are obtained by analyzing the entire program as a whole, it is possible to analyze single libraries (or even single methods) by assuming the every external method returns the largest possible abstract object. In this way, when a real object will we plugged in the final program, its behavior will be correctly abstracted.

From the point of view of performance, note that in a domain which tracks possible sharing information, it usually happens that the more precise an abstract object is, the smaller its representation is. For example, the best correct abstraction of a concrete state where no sharing happens is an $\mathsf{ALPS}$ graph without edges. However, if our analysis is not precise enough to compute the best correct abstraction, some edges will be included in the abstract object, which may negatively impact the performance of succeeding operations. Therefore, improving the precision of the analysis, from the one side, increases the computational cost, but from the other side may lead to smaller abstract objects which partially compensates this cost. A detailed evaluation of the trade-off between precision and performance may only be conducted experimentally. We plan to carry on this evaluation once we implement $\mathsf{ALPS}$ as an abstract domain for the $\mathsf{Jandom}$ static analyzer (Amato et al. 2013).

Although we have presented $\mathsf{ALPS}$ graphs in the context of object-oriented programs, the same domain can be immediately applied to functional programs. In this regard, note that the example program in Figure 8 may be rewritten in functional style and the benefits of linearity are the same already discussed for object-oriented programs.

The domain of $\mathsf{ALPS}$ graphs may be easily extended by annotating nodes with additional information in a modular way. For example, class analysis might be integrated by adding a set of possible classes for each node, while nodes representing numerical entities may be annotated with intervals for integrating range analysis. Obviously, if we want to maximize the benefits of the integration, at the very least, new operators should be devised which use the information of one domain to improve the precision of the other.

To the best of our knowledge, this is the first attempt to combine sharing with linearity for imperative or object-oriented languages.