Heap Abstractions for Static Analysis
Vini Kanvar and Uday P. Khedker

arXiv:1403.4910v5 [] 13 May 2015

Department of Computer Science and Engineering
Indian Institute of Technology Bombay
Email: {vini,uday}@cse.iitb.ac.in
14 May, 2015

Abstract
Heap data is potentially unbounded and seemingly arbitrary. As a consequence, unlike
stack and static memory, heap memory cannot be abstracted directly in terms of a fixed
set of source variable names appearing in the program being analysed. This makes it an
interesting topic of study and there is an abundance of literature employing heap
abstractions. Although most studies have addressed similar concerns, their formulations
and formalisms often seem dissimilar and some times even unrelated. Thus, the insights
gained in one description of heap abstraction may not directly carry over to some other
description. This survey is a result of our quest for a unifying theme in the existing
descriptions of heap abstractions. In particular, our interest lies in the abstractions and
not in the algorithms that construct them.
In our search of a unified theme, we view a heap abstraction as consisting of two
features: a heap model to represent the heap memory and a summarization technique for
bounding the heap representation. We classify the models as storeless, store based, and
hybrid. We describe various summarization techniques based on k-limiting, allocation sites,
patterns, variables, other generic instrumentation predicates, and higher-order logics. This
approach allows us to compare the insights of a large number of seemingly dissimilar heap
abstractions and also paves way for creating new abstractions by mix-and-match of models
and summarization techniques.

1

Heap Analysis: Motivation

Heap data is potentially unbounded and seemingly arbitrary. Although there is a plethora of
literature on heap, the formulations and formalisms often seem dissimilar. This survey is a
result of our quest for a unifying theme in the existing descriptions of heap.

1.1

Why Heap?

Unlike stack or static memory, heap memory allows on-demand memory allocation based on
the statements in a program (and not just variable declarations). Thus it facilitates creation
of flexible data structures which can outlive the procedures that create them and whose sizes
can change during execution. With processors becoming faster and memories becoming larger
as well as faster, the ability of creating large and flexible data structures increases. Thus the
role of heap memory in user programs as well as design and implementation of programming
languages becomes more significant.

1.2

Why Heap Analysis?

1.2

Why Heap Analysis?

The increasing importance of the role of heap memory naturally leads to a myriad requirements
of its analysis. Although heap data has been subjected to static as well as dynamic analyses,
in this paper, we restrict ourselves to static analysis.
Heap analysis, at a generic level, provides useful information about heap data, i.e. heap
pointers or references. Additionally, it helps in discovering control flow through dynamic
dispatch resolution. Specific applications that can benefit from heap analysis include program
understanding, program refactoring, verification, debugging, enhancing security, improving
performance, compile time garbage collection, instruction scheduling, parallelization etc.
Further, some of the heap related questions asked during various applications include
whether a heap variable points to null, does a program cause memory leaks, are two pointer
expressions aliased, is a heap location reachable from a variable, are two data structures
disjoint, and many others. Section 8 provides an overview of applications of heap analysis.

1.3

Why Heap Abstraction?

Answering heap related questions using compile time heap analysis is a challenge because of
the temporal and spatial structure of heap memory characterized by the following aspects.
• Unpredictable lifetime. The lifetime of a heap object may not be restricted to the scope
in which it is created. Although the creation of a heap object is easy to discover in a
static analysis, the last use of a heap object, and hence the most appropriate point of its
deallocation, is not easy to discover.
• Unbounded number of allocations.
Heap locations are created on-demand as a
consequence of the execution of certain statements. Since these statement may appear
in loops or recursive procedures, the size of a heap allocated data structure may be
unbounded. Further, since the execution sequence is not known at compile time, heap
seems to have an arbitrary structure.
• Unnamed locations. Heap locations cannot be named in programs, only their pointers
can be named. A compile time analysis of a heap manipulating program therefore,
needs to create appropriate symbolic names for heap memory locations. This is nontrivial because unlike stack and static data, the association between symbolic names and
memory locations cannot remain fixed.
In principle, a program that is restricted only to stack and static data, can be rewritten
without using pointers. However, the use of pointers is unavoidable for heap data because
the locations are unnamed. Thus a heap analysis inherits all challenges of a pointer
analysis of stack and static data1 and adds to them because of unpredictable lifetimes
and unbounded number of allocations.
Observe that none of these aspects are applicable to stack or static memory because their
temporal and spatial structures are far easier to discover. Thus an analysis of stack and static
data does not require building sophisticated abstractions of the memory. Analysis of heap
requires us to create abstractions to represent unbounded allocations of unnamed memory
locations which have statically unpredictable lifetimes. As described in Section 3, two features
common to all heap abstractions are:
1

Pointer analysis is undecidable [13,67]. It is inherently difficult because a memory location can be accessed in
more than one way i.e. via pointer aliases. Therefore, pointer analysis requires uncovering indirect manipulations
of data and control flow. Additionally, modern features such as dynamic typing, field accesses, dynamic field
additions and deletions, implicit casting, pointer arithmetic, etc., make pointer analysis even harder.

2

Heap Abstractions

1.4

Organization of the paper

• models of heap which represent the structure of heap memory, and
• summarization techniques to bound the representations.
We use this theme to survey the heap abstractions found in the static analysis literature.

1.4

Organization of the paper

Section 2 presents the basic concepts. Section 3 defines heap abstractions in terms of models
and summarization techniques. We categorize heap models as storeless, store based, or hybrid
and describe various summarization techniques. These are generic ideas which are then used
in Sections 4, 5, and 6 to describe the related investigations in the literature in terms of
the interactions between the heap models and summarization techniques. Section 7 compares
the models and summarization techniques to explore the design choices and provides some
guidelines. Section 8 describes major heap analyses and their applications. Section 9 mentions
some notable engineering approximations used in heap analysis. Section 10 highlights some
literature survey papers and book chapters on heap analysis. Section 11 concludes the paper
by observing the overall trend. Appendix A compares the heap memory view of C/C++ and
Java.

2

Basic Concepts

In this section, we build the basic concepts required to explain the heap abstractions in later
sections. We assume Java like programs, which use program statements: x := new, x := null,
x := y, x.f := y, and x := y.f. We also allow program statements x.f := new and x.f := null as
syntactic sugar. The dot followed by a field represents field dereference by a pointer variable.
For ease of understanding, we draw our programs as control flow graphs. Inn and Outn denote
the program point before and after program statement n respectively.

2.1

Examples of Heap Related Information

Two most important examples of heap information are aliasing and points-to relations because
the rest of the questions are often answered using them.
• In alias analysis, two pointer expressions are said to be aliased to each other if they
evaluate to the set of same memory locations. There are three possible cases of aliases
between two pointer expressions:
– The two pointer expressions cannot alias in any execution instance of the program.
– The two pointer expressions must alias in every execution instance of the program.
– The two pointer expressions may alias in some execution instances but not
necessarily in all execution instances.
• A points-to analysis attempts to determine the addresses that a pointer holds. A pointsto information also has three possible cases: must-points-to, may-points-to, and cannotpoints-to.
An analysis is said to perform a strong update if in some situations it can remove some
alias/points-to information on processing an assignment statement involving indirections on
the left hand side (for example, *x or x->n in C, or x.n in Java). It is said to perform a weak
update if no information can be removed.
Strong updates require the use of
May 2015

3

2.2

Soundness and Precision of Heap Analysis

1 x := new 1
2 x.g := null 2
3 y := new 2
4 y.f := null 3 6 y := x 6
5 y.g := null 4
7 x.f := new 7
8 x.f := new 7
Figure 1. Example to illustrate soundness and precision of information computed by may
and must analyses.

must-alias/must-points-to information whereas weak updates can be performed using
may-alias/may-points-to information in a flow-sensitive analysis2 .

2.2

Soundness and Precision of Heap Analysis

A static analysis computes information representing the runtime behaviour of the program
being analysed. Two important considerations in a static analysis of a program are soundness
and precision. Soundness guarantees that the effects of all possible executions of the program
have been included in the information computed. Precision is a qualitative measure of the
amount of spurious information which is the information that cannot correspond to any
execution instance of the program; lesser the spurious information, more precise is the
information.
Applications involving program transformations require sound analyses because the
transformations must be valid for all execution instances. Similarly applications involving
verification require a sound approximation of the behaviour of all execution instances. On
the other hand error detection or validation applications can afford to compromise on
soundness and may not cover all possible execution paths.
When an analysis computes information that must hold for all execution instances of a
program, soundness is ensured by under-approximation of the information. When it
computes information that may hold in some execution instances, soundness is ensured by
over-approximation of the information. Precision is governed by the extent of over- or
under-approximation introduced in the process.
Consider the program in Figure 1. Let us consider a may-null (must-null) analysis whose
result is a set of pointers that may (must) be null in order to report possible (guaranteed)
occurrences of null-dereference at statement 8. Assume that we restrict ourselves to the set
{x.f, x.g, y.f, y.g}. We know that both x.g and y.g are guaranteed to be null along all executions
of the program. However, x.f is guaranteed to be non-null because of the assignment in
statement 7 and y.f may or may not be null depending on the execution of the program.
2

A flow-sensitive heap analysis computes, at each program point, an abstraction of the memory, which is a
safe approximation of the memory created along all control flow paths reaching the program point

4

Heap Abstractions

(a) Consider the set {x.g, y.g} reported by an analysis at statement 8. This set is:
• Sound for a must-null analysis because it includes all pointers that are guaranteed to
be null at statement 8. Since it includes only those pointers that are guaranteed to
be null, it is also precise. Any under-approximation of this set (i.e. a proper subset
of this set) is sound but imprecise for a must-null analysis. An over-approximation of
this set (i.e. a proper superset of this set) is unsound for must-null analysis because it
would include a pointer which is not guaranteed to be null as explained in (b) below.
• Unsound for a may-null analysis because it excludes y.f which may be null at
statement 8.
(b) On the other hand, the set {x.g, y.g, y.f} reported at statement 8 is:
• Sound for a may-null analysis because it includes all pointers that may be null at
statement 8. Since it includes only those pointers that may be null, it is also precise.
Any over-approximation of this set (i.e. a proper superset of this set) is sound but
imprecise for a may-null analysis. Any under-approximation of this set (i.e. a proper
subset of this set) is unsound for a may-null analysis because it would exclude a
pointer which may be null as explained in (a) above.
• Unsound for a must-null analysis because it includes y.f which is not guaranteed be
null at statement 8.

3

Heap Abstractions

In this section we define some generic ideas which are then used in the subsequent sections to
describe the work reported in the literature.

3.1

Defining Heap Abstractions

The goal of static analysis of heap memory is to abstract it at compile time to derive useful
information. We define a heap abstraction as the heap modeling and summarization of the heap
memory which are introduced below
• Let a snapshot of the runtime memory created by a program be called a concrete memory.
A heap model is a representation of one or more concrete memories. It abstracts away less
useful details and retains information that is relevant to an application or analysis [59].
For example, one may retain only the reachable states in the abstract memory model.
We categorize the models as storeless, store based, and hybrid. They are defined in
Section 3.2.
• Deriving precise runtime information of non-trivial programs, in general, is not
computable within finite time and memory (Rice theorem [70]). For static analysis of
heap information, we need to summarize the modeled information. Summarization
should meet the following crucial requirements: (a) it should make the problem
computable, (b) it should compute a sound approximation of the information
corresponding to any runtime instance, and (c) it should retain enough precision
required by the application.
The summarizations are categorized based on using allocation sites, k-limiting, patterns,
variables, other generic instrumentation predicates, or higher-order logics. They are
defined in Section 3.3.
May 2015

5

Memory

Heap Models

Store based
model

Hybrid
model

Models

Unbounded
heap memory

Storeless
model

Generic
instrumentation
predicates
Higher-order
kHigher-order
klogics
limiting
logics
limiting
Generic
Allocation
instrumentation
Generic
sites
predicates
Patterns instrumentation
predicates
Variables

Summarizations

3.2

Figure 2. Heap memory can be modeled as storeless, store based, or hybrid. These models are
summarized using allocation sites, k-limiting, patterns, variables, other generic instrumentation
predicates, or higher-order logics.

Some combinations of models and summarization techniques in common heap abstractions
are illustrated in Figure 2.

3.2

Heap Models

Heap objects are dynamically allocated, are unbounded in number, and do not have fixed
names. Hence, various schemes are used to name them at compile time. The choice of naming
them gives rise to different views of heap. We define the resulting models and explain them
using a running example in Figure 3. Figure 4 associates the models with the figures that
illustrate them for our example program.
• Store based model. A store based model explicates heap locations in terms of their
addresses and generally represents the heap memory as a directed graph [7, 10, 15, 18,
26, 37, 61, 68, 77, 84, 87]. The nodes of the graph represent locations or objects in the
memory. An edge x → o1 in the graph denotes the fact that the pointer variable x may
hold the address of object o1 . Since objects may have fields that hold the addresses,
f

we can also have a labelled edge x → o1 denoting the fact that the field f of object x
may hold the address of object o1 . Let V be the set of root variables, F be the set of
fields names, and O be the set of heap objects. Then a concrete heap memory graph
can be viewed as a collection of two mappings: V 7→ O and O × F 7→ O. Observe that
this formalization assumes that O is not fixed and is unbounded. It is this feature that
warrants summarization techniques.
An abstract heap memory graph3 is an approximation of concrete heap memory graph
which collects together all addresses that a variable or a field may hold
3

6

In the rest of the paper, we refer to an abstract heap memory graph simply by a memory graph.

Heap Abstractions

3.2

Heap Models

1 x := new 1
2 y := x 2
3 y.f := new 3
4 y := y.f 4
5 y.f := new 5
6 y := y.f 6

l1
x l3
l2
y l7

l3

l4

l5

l6

l7

f l4

f l5

f l6

f l7

f ...
1

(b) Execution snapshot showing an unbounded heap graph at Out6 of the
program in Figure 3a. Here we have shown the heap graph after iterating
twice over the loop. Stack locations x and y point to heap locations l3 and
l7 , respectively. Heap locations l3 , l4 , l5 , and so on point to heap locations
l4 , l5 , l6 , and so on, respectively.

(a) Example

Figure 3. Running example to illustrate heap models and summarizations, which have been
shown in Figures 5, 6, and 7. In the program we have purposely duplicated the program
statements in order to create a heap graph where variable y is at even number of indirections
from variable x after each iteration of the loop. Not all summarization techniques are able to
capture this information.

– at all execution instances of the same program point, or
– across all execution instances of all program points.
Hence the ranges in the mappings have to be extended to 2O for an abstract memory
graph. Thus a memory graph can be viewed as a collection of mappings4 V 7→ 2O and
O × F 7→ 2O .
Figure 3 shows our running example and an execution snapshot of the heap memory
created and accessed by it. The execution snapshot shows stack locations x and y and
heap locations with the addresses l3 , l4 , l5 , l6 , and l7 . The address inside each box
denotes the location that the box points to. This structure is represented using a store
based model in Figure 5. Here the root variable y points to a heap location that is at
even number of indirections via f from x after each iteration of the loop in the program
in Figure 3a.
• Storeless model. The storeless model (originally proposed by Jonkers [40]) views the
heap as a collection of access paths [8, 17, 24, 40, 43, 49, 60, 63]. An access path consists of
a pointer variable which is followed by a sequence of fields of a structure. The desired
properties of both a concrete and an abstract heap memory are stored as relations on
access paths. The storeless model does not explicate the memory locations or objects
corresponding to these access paths. Given V as the set of root variables and F as the set
of field variable names, the set of access paths is defined as V × F ∗ . For example, access
path x.f.f.f.f represents a memory location reachable from x via four indirections of field
f. Observe that the number of access paths is potentially infinite and the length of each
access path is unbounded. It is this feature that warrants summarization techniques.
The heap memory at Out6 of our running example (Figure 3) is represented using
4

In principle a graph may be represented in many ways. We choose a collection of mappings for convenience.

May 2015

7

Memory

Heap Summarization Techniques

Unbounded
heap memory

Store based
model

Hybrid
model

Storeless
model

(Figure 5)

(Figure 7)

(Figure 6)

Models

(Figure 3b)

Generic
instrumentation
predicates
(Figure 7b)

klimiting

Higher-order
logics

(Figure 5b)

Allocation
sites
(Figure 5c)

Generic
instrumentation
predicates

klimiting

Higher-order
logics

(Figure 6b)

Generic
Patterns instrumentation
(Figure 6c) predicates

Summarizations

3.3

Variables
(Figure 5d)

Figure 4. Figures illustrating various heap models and their summarizations for the program
in Figure 3.

storeless model in Figure 6. The alias information is stored as a set of equivalence
classes containing access paths that are aliased. Access paths x.f.f.f.f and y are put in
the same equivalence class at Out6 because they are aliased at some point in the
execution time of the program.
• Hybrid model. Chakraborty [14] describes a hybrid heap model which represents heap
structures using a combination of store based and storeless models [16, 25, 50, 72]. Heap
memory of Figure 3b is represented using the hybrid model in Figure 7. The model stores
both objects (as in a store based model) and access paths (as in a storeless model).

3.3

Heap Summarization Techniques

In the presence of loops and recursion, the size of graphs in a store based model and the lengths
of the access paths (and hence their number) in a storeless model is potentially unbounded.
For fixpoint computation of heap information in a static analysis, we need to approximate the
potentially unbounded heap memory in terms of summarized heap locations called summarized
objects. A summarized object is a compile time representation of one or more runtime (aka
concrete) heap objects.
3.3.1

Summarization

Summarized heap information is formally represented as Kleene closure or wild card in regular
expressions, summary node in heap graphs, or recursive predicates.
• Summarized access paths are stored as regular expressions [17] of the form r.e, where
r is a root variable and e is a regular expression over field names defined in terms of
8

Heap Abstractions

3.3
y

x
f

f

Heap Summarization Techniques

y
f

f

...

(a) Unbounded store based model.

y

x
f

f

1
f

(b) k-limiting (k = 2)
summarization.

y

x
f

3

f

5

f
(c) Allocation site based
summarization.

y

x
f

f
f

(d) Variable based
summarization.

Figure 5. Store based heap graphs at Out6 for the program in Figure 3a. Figures 5b, 5c,
and 5d are bounded representations of heap information in Figure 5a. The numbers inside the
graph nodes indicate the object’s allocation sites in the program in Figure 3a.

concatenation (.), Kleene closure (∗ and + used as superscripts), and wild card (∗ used
inline) operators. For example, access path x.f.∗ represents an access path x.f followed
by zero or more dereferences of any field. Access path x(.f)∗ represents an access path x
followed by any number of dereferences of field f.
• Summarized heap graphs are stored by associating each graph node with a boolean
predicate indicating whether it is a summary node representing more than one concrete
heap location [15]. Observe that summary nodes may result in spurious cycles in the
graph if two objects represented by a summary node are connected by an edge.
• Summarized collection of paths in the heap can also be stored in the form of recursive
predicates [26, 63].
3.3.2

Materialization

A collection of concrete nodes with the same property are summarized as a summary node.
However, after creation of a summary node, a program statement could make a root variable
point to one of the heap locations represented by the summary node.
Traditional
summarization techniques [15, 50] do not “un-summarize” this heap location from the
summary node. Thus in traditional summarization techniques, a property discovered for a
summarized node may be satisfied by some of the represented heap locations and not
necessarily by all. For example, when determining which pointer expressions refer to the
same heap location, all pointer expressions pointing to the same summarized object will be
recognized as possible candidates, even though some of them may have been changed by new
assignments. Therefore, a heap analysis using this traditional summarization technique has a
serious disadvantage: it can answer only may-pointer questions. As a result traditional
summarization techniques cannot allow strong updates. In order to compute precise
must-pointer information, Sagiv et al. [75] materialize (“un-summarize”) summarized objects
(explained in Section 5.2). Since this allows the locations that violate the common property
May 2015

9

3.3

Heap Summarization Techniques

{hx.f.f, yi, hx.f.f.f.f, yi, . . . }

{hx.f.f, yi,
hx.f.f.∗, yi}

{hx(.f.f)+ , yi}

(a) Unbounded storeless model.

(b) k-limiting (k = 2).

(c) Pattern based.

Figure 6. Storeless model of heap graph at Out6 of the program in Figure 3a. Figures 6b
and 6c are the bounded representations of heap information in Figure 6a. Equivalence class of
aliased access paths is denoted by h and i.

y

x
hxi

f

hx.fi

f

y

f hx.f.f, f hx.f.f.f f hx.f.f.f.f, f
...
yi
y.fi
y.f.f, yi

(a) Unbounded hybrid model.

y

x
hxi

f

hx(.f)+ i

f hx(.f)+ .f,
yi

(b) Variable based summarization.

Figure 7. Hybrid model of heap graph at Out6 of the program in Figure 3a. Figure 7b is the
bounded representation of the heap information in Figure 7a. Although the access paths in
the nodes can be inferred from the graph itself, they have been denoted for simplicity.

to be removed from the summary node and be represented by a newly created node, this
opens up the possibility that a summary node could represent a must property satisfied by all
locations represented by the summary node. Performing strong updates is an example of
increased precision that can be facilitated by materialization. Literature contains many
approaches for must-pointer analysis, ranging from relatively simple abstractions such as
recency abstraction [4] to sophisticated shape analysis [75].
An analysis involving
materialization is expensive because of the additional examination required and the possible
increase in the size of the graph.
3.3.3

Summarization Techniques

We introduce below the six commonly found summarization techniques using our running
program of Figure 3a. The figures illustrating these techniques have been listed in Figure 4.
Note that our categorization is somewhat arbitrary in that some techniques can be seen as
special cases of some other techniques but we have chosen to list them separately because of
their prevalence.
The main distinction between various summarization techniques lies in how they map a
heap of potentially unbounded size to a bounded size. An implicit guiding principle is to find
a balance between precision and efficiency without compromising on soundness.
1. k-limiting summarization distinguishes between the heap nodes reachable by a sequence
of up to k indirections from a variable (i.e. it records paths of length k in the memory
graph) and over-approximates the paths longer than k.
10

Heap Abstractions

3.3

Heap Summarization Techniques

k-limiting summarization has been performed on store based model [50]. Figure 5b
represents a k-bounded representation of the hybrid model in Figure 5a. For k = 2,
heap nodes beyond two indirections are not stored. A self loop is created on the second
indirection (node corresponding to x.f.f) to over-approximate this information. This
stores spurious aliases for access paths with more than k = 2 indirections (for example,
x.f.f.f and y are spuriously marked as aliases at Out6 ).
k-limiting summarization has also been performed on storeless model [39, 49]. This was
proposed by Jones and Muchnick [39]. Figure 6b represents a k-bounded representation
of the storeless model in Figure 6a. This also introduces the same spurious alias pairs as
in Figure 5b.
2. Summarization using allocation sites merges heap objects that have been allocated at
the same program site. This technique is used for approximating store based heap
model [4, 61] and hybrid model [50]. It gives the same name to all objects allocated in a
given program statement. The summarization is based on the premise that nodes
allocated at different allocation sites are manipulated differently, while the ones
allocated at the same allocation site are manipulated similarly. Figure 5c represents
allocation site based summarization heap graph of the store based model in Figure 5a.
Here all objects allocated at program statements 3 and 5 are respectively clustered
together. This summarization on the given example does not introduce any spurious
alias pairs. We will show spuriousness introduced due to this summarization in
Section 6.1.
3. Summarization using patterns merges access paths based on some chosen patterns of
occurrences of field names in the access paths. Pattern based summarization has been
used to bound the heap access paths [17, 43, 60]. Figure 6c represents pattern based
summarization of the storeless model in Figure 6a. For this example, it marks every
second dereference of field f (along the chain rooted by x) as aliased with y which is
precise.
4. Summarization using variables merges those heap objects that are pointed to by the
same set of root variables. For this, Sagiv et al. [78] use the predicate pointed-to-by-x on
nodes for all variables x to denote whether a node is pointed to by variable x. Thus, all
nodes with the same pointed-to-by-x predicate values are merged and represented by a
summary node. Variable based summarization has been performed on store based heap
model [7,15,75,76]. Figure 5d represents variable based summarization of the store based
model in Figure 5a. After the first iteration of the loop of the program in Figure 3a,
there are three nodes—the first pointed to by x and the third pointed to by y. In the
second iteration of the loop, nodes reachable by access paths x.f, x.f.f, and x.f.f.f are
not pointed to by any variable (as shown in Figure 3b). Therefore, they are merged
together as a summary node represented by dashed lines in Figure 5d which shows the
graphs after the first and the second iterations of the loop. The dashed edges to and from
summary nodes denote indefinite connections between nodes. This graph also records
x.f.f.f and y as aliases at Out6 which is spurious.
Figure 7b is a variable based summarized representation of the unbounded hybrid
model in Figure 7a. A summary node (shown with a dashed boundary in the figure) is
created from nodes that are not pointed to by any variable. Summarized access paths
are appropriately marked on the nodes in the hybrid model.
5. Summarization using other generic instrumentation predicates merge those heap objects
that satisfy a given predicate [4, 24, 37, 68, 72, 77, 78, 87, 90].
May 2015

11

3.3

Heap Summarization Techniques

Note that the summarization techniques introduced above are all based on some
predicate, as listed below:
• k-limiting predicate: Is the heap location at most k indirections from a root variable?
• Allocation site based predicate: Is the heap location allocated at a particular
program site?
• Pattern based predicate: Does the pointer expression to a heap location have a
particular pattern?
• Variable based predicate: Is a heap location pointed to by a root variable?
Since the above four are very commonly used predicates, we have separated them out in
our classification.
Apart from these common predicates, summarization may be based on other predicates
too depending on the requirements of a client analysis. Some examples of these predicates
are: is a heap location part of a cycle, is a heap location pointed to by more than one
object, is a heap location allocated most recently at a particular allocation site, does the
data in a heap node belong to a given type. We group such possible predicates under
generic instrumentation predicates. A shape analysis framework [77, 78, 90] accepts any
set of predicates as parameter to control the degree of efficiency and precision in the
summarization technique.
6. Summarization using higher-order logics includes those logics that have more expressive
power than first order (predicate) logic. Classical logics, like Hoare logic [34], fail when
they are used to reason about programs that manipulate the heap. This is because
classical logics assume that each storage location has a distinct variable name [82], i.e.
there are no aliases in the memory. However, heap memory contains aliases of variables
and becomes difficult to analyse. Therefore, heap specialized logics, such as those listed
below, have been used for heap abstraction.
• Separation Logic [10, 18, 26],
• Pointer Assertion Logic (PAL) [63],
• Weak Alias Logic (wAL) [8],
• Flag Abstraction Language [46, 47],
These are extensions of classical logics. For example, separation logic adds separating
connectives to classical logic to allow separate reasoning for independent parts of
heap [9, 82]. Summarizations using higher-order logics differ from summarizations using
generic instrumentation predicates in the following sense: the former use formal
reasoning in logics specialized for heap memory. Unlike the latter, these techniques may
be highly inefficient and even include undecidable logics; therefore, in order to ensure
their termination, they generally need support with program annotations in the form of
assertions and invariants [38]. In the following sections, we illustrate separation logic,
which is generally based on store based heap models, and PAL, wAL, and Flag
Abstraction Language, which have been used on storeless heap modes.
These heap summarization techniques can be combined judiciously. Most investigations
indeed involve multiple summarization techniques and their variants by using additional
ideas. Section 7 outlines the common factors influencing the possible choices and some broad
guidelines.
12

Heap Abstractions

1 y := x 1
2 z := w 2
y

3 t := y.g 3
4 z.g := t 4

f

x

f

f

g

5 y := y.f 5
g

6 y := y.f 6

w

y
f

f

g
f

g

...

g
f

g

f

...

7 z.f := new 7
z

8 z := z.f 7
9 u := new 7
10 y.f := u 7

z

(b) Execution snapshot showing an unbounded heap graph at Out8
of the program in Figure 8a. y points to x.f.f and z points to w.f
in the first iteration of the loop. In the second iteration, y points
to x.f.f.f.f and z points to w.f.f.

11 v := y.f 7
(a) Example

Figure 8. Running example to illustrate various heap summarization techniques. We assume
that all variables are predefined in the program. Summarized representations of the heap
memory in Figure 8b are shown on a storeless model in Figure 9, and are shown on a hybrid
model in Figures 18 and 19.

4

Summarization in Storeless Heap Model

As described in Section 3.2, a storeless heap model views the heap memory as a collection of
access paths. By contrast, the store based model views the memory as a graph in which nodes
are heap objects and edges are fields containing addresses. The view of storeless model may
seem to be a secondary view of memory that builds on a primary view of memory created by
the store based model. In this section we present the summarization techniques for a storeless
model. Sections 5 and 6 present techniques for a store based model and a hybrid model,
respectively.

4.1

k-Limiting Summarization

May-aliases have been represented as equivalence classes of k-limited access paths [49]. For the
program in Figure 8a, with its unbounded memory graph in Figure 8b, information bounded
using k-limiting summarization of access paths is shown in Figure 9a (alias pairs of variables
y and z are not shown for simplicity). The method records alias pairs precisely up to k
indirections and approximates beyond that. For k = 3, fields up to three indirections from the
root variables in the access paths are recorded; those beyond three indirections are summarized
with a wild card (symbol ∗). Observe that this summarization induces the spurious alias
relationship hx.f.f.f, w.f.fi.
May 2015

13

4.2

Summarization Using Patterns

hx.g, w.gi
hx.f.f.g, w.f.gi
hx.f.f.f.∗, w.f.f.∗i

(a) Alias pairs for variables x
and w at Out8 for k = 3 [49].

x

f5

f6

g3

(d) Live access graph at In1
when variable t is live at
Out11 [43].

hy, x(.f.f)+ i
hz, w(.f)+ i
hx(.f.f)+ .g, w(.f)+ .gi

(b) Aliases at Out8 [60].

x y
x 1 1
y 0 1
Direction
Matrix

x y
x 1 1
y 1 1
Interference
Matrix

(e) Direction and interference
matrices for variables x and
y at Out8 [24].

hx.f2i .g, w.fi .gi

(c) Parameterised alias pairs
for variables x and w at
Out8 [17].

x
S

y
x
f+
y
S
Path Matrix

(f) Path matrix for variables x
and y at Out8 [31].

Figure 9. Summarization techniques on a storeless model for the program in Figure 8a:
k-limiting (Figure 9a), pattern based (Figure 9b, 9c, 9d), and other generic instrumentation
predicates based (Figure 9e, 9f) summarization techniques are shown. (Equivalence class of
aliased access paths is denoted by h and i in Figures 9a, 9b, and 9c.)

4.2

Summarization Using Patterns

A common theme in the literature has been to construct expressions consisting of access paths
approximated and stored either as a regular expression or a context free language.
• Consider the possibility of representing access paths in terms of regular expressions [60].
For example, let p be the initial access path outside a program loop. After each iteration
of the loop, if the value of p is advanced into the heap relative to its previous value via
the field left or right, then the access path can be represented as p(.left | .right)∗ .
The bounded alias information for the unbounded memory graph of Figure 8b is shown
in Figure 9b. The example illustrates that the method is able to identify (.f.f) as the
repeating sequence of dereferences in the access path rooted at x and (.f) as the repeating
sequence of dereferences in the access path rooted at w. The alias hx(.f.f)∗ .g, w(.f)∗ .gi
at Out8 , indicates that x.f.f.g is aliased to w.g, which is spurious.
The general problem of detecting possible iterative accesses can be undecidable in the
worst case [60]. This is because a repeated advance into the heap may arise from an
arbitrarily long cycle of pointer relations. Therefore, the focus in the work by Matosevic
and Abdelrahman [60] remains on detecting only consecutive repetitions of the same type
of field accesses. For efficiency, finite state automata are used to compactly represent
sets of access paths that share common prefixes.
• On similar lines, repetition of field dereferences in program loops can be identified more
efficiently and precisely by using the statement numbers where the field dereference
has occurred [43]. This has been used to perform liveness based garbage collection by
computing live access graphs of the program. A live access graph is a summarized
14

Heap Abstractions

4.3

Summarization Using Generic Instrumentation Predicates

representation of the live access paths5 in the form of a graph; here a node denotes both
a field name and the statement number where the field dereference has occurred; the
edges are used to identify field names in an access path.
A live access graph is illustrated in Figure 9d for the program in Figure 8a. Let us assume
that variable t is live at Out11 in the program i.e. it is being used after statement 11.
This implies that access path y.g (or x(.f.f)∗ .g) is live at In3 since it is being accessed
via variable t in the program loop. Therefore, access paths x(.f.f)∗ .g are live at In1 .
These access paths are represented as a summarized live access graph in Figure 9d. The
cycle over nodes f5 and f6 denotes the Kleene closure in the access paths x(.f.f)∗ .g.
This illustrates that the method is able to identify (.f.f) as a repeating sequence in the
live access paths at In1 .
Basically, this is achieved by assigning the same name to the objects that are dereferenced
by a field at the same statement number. For example, the last field in each of the access
paths, x.f, x.f.f.f., and so on, is dereferenced in statement 5; therefore, all these fields
f (dereferenced in statement 5) are represented by the same node f5 in Figure 9d.
Similarly, the last fields f in each of the access paths, x(.f.f)∗ .g, are represented by
the same node f6 because each of them is dereferenced in statement 6. With the use of
statement numbers, unlike the method by Matosevic and Abdelrahman [60], this method
can identify even non-consecutive repetitions of fields efficiently.
In somewhat similar lines, liveness based garbage collection for functional programs has
been performed using a store based model by Inoue et al. [37] and Asati et al. [2] (see
Section 5.3).
• More precise expressions of access paths compared to those in the above methods are
constructed by parameterising the expressions with a counter to denote the number
of unbounded repetitions of the expression [17]. Right-regular equivalence relation on
access paths helps in performing an exact summary of the may-aliases of the program.
The precisely bounded information for the unbounded memory graph of Figure 8b is
illustrated in Figure 9c. The key idea of the summarization is to represent the position
of an element in a recursive structure by counters denoting the number of times each
recursive component of the structure has to be unfolded to give access to this element.
This records the fact that the object reached after dereferencing 2i number of f fields on
access path x is aliased with the object reached after dereferencing i number of f fields
on the access path w. Due to the parameterisation with 2i and i on field f of both aliased
access paths which are rooted at variables x and w respectively, the method excludes the
spurious alias pairs derived from the alias information in Figure 9b.

4.3

Summarization Using Generic Instrumentation Predicates

Since the identification of patterns can be undecidable in the worst case [60], the power of
summarization using patterns is limited by the set of patterns that the algorithm chooses to
identify. Instead of using a fixed set of patterns, summarization using generic instrumentation
predicates enables a richer set of possibilities. We review this approach in this section.
A digression on shape analysis
The use of heap analysis to determine shapes of the heap memory dates back to the work by
Jones and Muchnick [39]. Some of the notable works which also determine shapes are enlisted
below.
5

An access path is live at a program point if it is possibly used after the program point.

May 2015

15

4.3

Summarization Using Generic Instrumentation Predicates

– Analysis to determine shape using a storeless model has been presented by Jones and
Muchnick [39], Hendren and Nicolau [31], Ghiya and Hendren [24], and others (presented
in this section).
– Analysis to determine shape using a store based model has been presented by Chase et
al. [15], Sagiv et al. [75,77,78], Distefano et al. [18], Gotsman et al. [26], Calcagno et al. [10],
and others (see Section 5).
– Analysis to determine shape using a hybrid model has been presented by Rinetzky et al. [72]
and others (see Section 6).
This study of the structure and shape of the heap has been called shape analysis. Below
we discuss shape analysis techniques used on a storeless model.
• Hendren and Nicolau [31] and Ghiya and Hendren [24] classify the shapes of the heap into
tree, DAG, and cyclic graph, and choose to use the following predicates on a storeless
model.
(a) Direction relationship, which is true from pointer x to pointer y, if x can reach y via
field indirections.
(b) Interference relationship, which is true for pointers x and y, if a common heap object
can be accessed starting from x and y. This is a symmetric relationship.
Direction and interference relationships are stored in terms of matrices as shown in
Figure 9e for the program in Figure 8a. Here, the heap has been encoded as access
paths in path matrices (direction and interference) at each program statement. Direction
relationship between pointers x and y is true (represented by 1 in the direction matrix),
since x reaches y via indirections of field f at Out8 of the program in Figure 8a. Since
y cannot reach a node pointed to by x at Out8 , 0 is marked in the corresponding entry
of the direction matrix. Here, from the direction relationship, we can derive that objects
pointed by x and y are not part of a cycle, since x has a path to y, but not vice versa.
Interference relationship between pointers x and y is true, since a common heap object
can be accessed starting from x and y.
• Storeless heap abstraction using reachability matrices can also be summarized using
regular expressions of path relationships between pointer variables [31]. This is used to
identify tree and DAG shaped heap data structures by discovering definite and possible
path relationships in the form of path matrices at each program point. For variables x
and y, an entry in the path matrix, denoted as p[x, y], describes the path relationship
from x to y. In other words, each entry in the path matrix is a set of path expressions of
field dereferences made for pointer x to reach pointer y. Figure 9f shows the summarized
path matrix for pointers x and y at Out8 of the program in Figure 8a. Entry p[x, x] = {S}
denotes that source and destination pointer variables are the same. Entry p[x, y] = {f+ }
denotes that there exists a path from x to y via one or more indirections of field f. An
empty entry p[y, x] denotes that there is no path from pointer y to pointer x.
This analysis calculates the part of the data structure that is between two variables at
each program point. The analysis can differentiate between a tree and a DAG by the
number of paths to a variable calculated in the path matrix. The information is used for
interference detection and parallelism extraction. This approach is, however, restricted
to acyclic data structures. Some follow-up methods [28–30] also use path matrices for
alias analysis of heap allocated data structures.
16

Heap Abstractions

4.4

4.4

Summarization Using Higher-Order Logics

Summarization Using Higher-Order Logics

To describe heap specific properties, various formalisms like Pointer Assertion Logic, Weak
Alias Logic, and Flag Abstraction Language have been proposed in the literature.
• PALE (Pointer Assertion Logic Engine) [63] is a tool that provides a technique to check
the partial correctness of programs annotated manually by the programmer using PAL
(Pointer Assertion Logic). The programmer encodes everything in PAL including the
program code, heap data structures, pre- and post-conditions of various modules of the
program, and loop invariants. PAL is an assertion language which is a monadic
second-order logic, or more precisely, WS2S (weak monadic second-order logic with two
successors). Unlike first-order logic, ordinary second-order logic allows quantification
(existential/universal) over predicates. “Monadic” means that quantification of only
monadic predicates, i.e. sets, is allowed. “Weak” means that quantification over finite
sets is allowed. “With two successors” means that the formulae are interpreted over a
tree domain (which is infinite). Although it is technically “two” successors, it is trivial
to encode any fan-out.
Here is an example [63] of a specification of type binary tree using PAL.
type Tree = {
data left,right:Tree;
pointer root:Tree[rooth(left+right)∗ithis
& empty(rootˆTree.left union rootˆTree.right)];
}
.A memory graph consists of a “backbone” which represents a spanning tree of the
underlying heap data structure. The memory links of the backbone are encoded using
data fields in PAL. Other memory links of the data structure are encoded in PAL using
pointer fields that are defined on top of the backbone6 . The above example defines a
heap location of type Tree which consists of left, right, and root links. The root
link is an extra pointer which points to the root of the tree. It is defined with a formula
specified between the square brackets which is explained below.
– The formula rooth(left+right)∗ ithis specifies that the root location reaches this
location via a sequence of left or right fields. The Kleene closure in this regular
expression helps in summarizing unbounded information.
– In PAL, formula xˆT.p can be read as xˆ(T.p), where ˆ(T.p) represents a step
upwards in the backbone i.e. backwards along field p from a location of type T
in order to reach a location pointed to by x. In the above example, formulae
rootˆTree.left and rootˆTree.right denote that location root can be reached
by moving a step upwards in the backbone along left and right fields from a
location of type Tree. The empty() formula above specifies that locations having
left or right pointers to the root location must be empty.
Once the data structures, loop invariants, pre- and post-conditions are specified by the
programmer in PAL, PALE passes these PAL annotations to the MONA tool [62] for
automatic verification of the program. MONA reports null-pointer dereferences, memory
leaks, violations of assertions, graph type errors, and verifies shape properties of data
structures.
6

Anders Møller, 04 May 2015, personal communication.

May 2015

17

4.4

Summarization Using Higher-Order Logics

Let us take an example of the predicates used in MONA logic. Consider statement 5,
z := y.f which is executed on the linked list of the program in Figure 10a. The linked
list can be specified in PAL as: type Node = {data f: Node;}. For program points
i = In5 and j = Out5 , MONA code [63] generated for this statement is
memfailed j () = memfailed i() | null y i()
ptr z j(v) = ex2 w:

ptr y i(w) & succ Node f i(w,v)

null z j() = ex2 w:

ptr y i(w) & null Node f i(w)

.MONA code uses the following predicates in the above formula:
– memfailed() is true if a null dereference has occurred.
– null p() is true if pointer variable p is null.
– ptr p(v) is true if the destination of pointer variable p is object v.
– succ t f (v, w) is true if object v of type t reaches location w via pointer field f .
– null t f (v) is true if object v of type t reaches a null location via pointer field f .
The predicates in the above MONA code for statement 5 have been indexed with the
program points. For example, for program point i, the value of predicate memfailed() is
memfailed i(). Also, ex2 is an existential quantifier used for Node object w in the above
MONA code.
In the above MONA code, the first line specifies that program point j is in a state of
memory failure if either there was a memory failure at program point i or variable y was
null at i. The second line specifies that if object w is the destination of variable y, and w
reaches object v via pointer field f, then v is the destination of variable z. The third line
specifies that if object w is the destination of variable y, and w reaches a null location
via pointer field f, then variable z is null.
Since MONA’s logic is decidable, PALE will definitely reach a fixpoint. Due to the
overhead of manually adding annotations to the program, the technique is suited for
small input programs only.
• Unlike PAL, which describes a restricted class of graphs, Weak Alias Logic (wAL) deal
with unrestricted graphs [8].
The user annotates the program with pre- and
post-conditions and loop invariants using wAL. The annotations are then automatically
verified for correctness. wAL is an undecidable monadic second order logic that can
describe the shapes of most recursive data structures like lists, trees, and dags. Let X
and Y be heap structures represented as a set of regular expressions or access paths,
and let ρ be a regular expression or a set of regular expressions. In wAL, hXiρ specifies
that X is bound to the heap, which is described by ρ. Also the formula X −1 Y in wAL
denotes all the paths from X to Y . Given below are some predicates in wAL [8].
reach(X, Y ) = hY iXΣ+
share(X, Y ) = ∃Z.reach(X, Z) ∧ reach(Y, Z)
tree(root) = ∀X.hXiroot ⇒ ∀Y, Z.(reach(X, Y ) ∧ reach(X, Z) ⇒ ¬share(Y, Z))
.These predicates are explained below.
18

Heap Abstractions

– Predicate reach(X, Y ) states that location Y is reachable from location X via a
non-empty path Σ+ . The Kleene closure over the set of pointer fields Σ helps in
summarizing unbounded information.
– Predicate share(X, Y ) states that locations X and Y reach a common location via
non-empty paths, respectively.
– Predicate tree(root) describes the shape of a tree structure pointed to by a variable
root. It states that sharing is absent in a tree structure.
Let us derive the pre-condition for statement 3, y.f := x of the program in Figure 10a,
when its post-condition is given.
pre-condition:

{aclist(x) ∧ ∀X, Y [hXix ∧ hY iy ⇒ X −1 Y = ∅]}

assignment statement:
post-condition:

y.f := x
{aclist(y)}

.The post-condition for the assignment statement y.f := x specifies that variable y points
to an acyclic linked list (denoted by predicate aclist(y)). The pre-condition for the
assignment statement is that variable x should be an acyclic linked list and that there
should be no path from x to y (otherwise the assignment statement would create a cycle,
invalidating the post-condition aclist(y)).
Bozga et al. [8] have also designed pAL (Propositional Alias Logic), which is a decidable
subset of wAL. However, pAL can describe only finite graphs and does not have the
ability to describe properties like list-ness, circularity, and reachability.
• Hob [48] is a program analysis framework, which allows a developer to use multiple
analysis plugins for the same program. Each procedure can be verified by a different
analysis plugin; therefore, an efficient analysis plugin can be chosen for each procedure
depending on the properties of the procedure that the developer wishes to verify. The
Hob project has been plugged with the following three analysis plugins [46]:
1. Flag Abstraction Language plugin [47] uses first order boolean algebra extended
with cardinality constraints. It is used to infer loop invariants.
2. PALE plugin [63] uses monadic second order logic to verify properties of tree like
data structures.
3. Theorem proving plugin uses higher-order logic to handle all data structures.

5

Summarization in Store Based Heap Model

It is easier to visualize a memory graph as heap objects connected through fields. This is
the view of a store based heap model as introduced in Section 3.2. The following sections
summarize this unbounded view using techniques involving a combination of allocation sites,
variables, some other generic instrumentation predicates, and higher-order logics.

5.1

Summarization Using Allocation Sites and Variables

Chase et al. [15] were the first to summarize heap nodes using techniques involving allocation
sites and variables. In their method, heap nodes with the following properties are summarized:
May 2015

19

5.1

Summarization Using Allocation Sites and Variables
y
f

1 x := null 1

...

x

2 y := new 2
3 y.f := x 3

f

(b) Execution snapshot showing an unbounded heap graph at Out4
of program in Figure 10a.

4 x := y 4
y
f

5 z := y.f 6
6 y := z 7

(a) Example

x

f

...

f

f

f

...

z

(c) Execution snapshot showing an unbounded heap graph at Out6
of program in Figure 10a.

Figure 10.
Running example to illustrate various heap summarization techniques.
Summarized representations of the heap memories in Figures 10b and 10c are shown on a
store based model in Figures 11, 12, 13, 16, and 17.

1. heap nodes created at the same program point (i.e. allocation site) such that
2. they have the same pointed-to-by-x predicate values for each pointer variable x.
We illustrate this for the program in Figure 10a. The unbounded memory graphs at Out4
and Out6 are shown in Figures 10b and 10c, respectively. The corresponding summarized
graphs created using this method [15] at Out4 and Out6 are shown in Figures 11a and 11b,
respectively. In Figure 11a, we see that nodes have been named by their allocation site, i.e.
statement 2. Also, since this method keeps nodes apart on the basis of pointer variables, we
get two abstract nodes—one node pointed to by pointer variables x and y, and the other node
not pointed to by any variable. The self loop on the second node denotes the presence of
unbounded number of nodes that are not pointed to by any pointer variable.
This method analyses Lisp like programs and constructs shape graphs for heap variables.
It can determine the shape of the allocated heap as tree, simple cycle, and doubly linked list.
In case of lists and trees, if all the nodes are allocated at the same site then the shape graph
would contain a single summary node with a self loop, making all the nodes aliased to each
other. For example, from the graph in Figure 11a, it cannot be inferred whether the structure
is a linear list or it contains a cycle in the concrete heap memory. To avoid this, each node
is augmented with a reference count i.e. the number of references to the corresponding heap
location from other heap locations (and not from stack variables). For example, the reference
count of the summary node not pointed to by any variable in Figure 11a is one. A reference
count of less than or equal to one for each node indicates that the data structure is a tree or a
list; whereas, a reference count of more than one indicates that the data structure is a graph
with sharing or cycles. Therefore, this method can identify at Out4 that the program creates
a linear list.
However, the method cannot perform materialization of summary nodes. For example,
after analysing statements 5 and 6 of the program in Figure 10a, the abstract graph obtained
20

Heap Abstractions

5.2
y
2

y

f
f

2

x
(a) Summarized shape graph at Out4 .

Figure 11.
Figure 10a.

Summarization Using Variables

2
x

f

2

f

z

(b) Summarized shape graph at Out6 .

Summarization using allocation sites and variables [15] for the program in

at Out6 is shown in Figure 11b. It can be seen that the summary node (not pointed to by
any variable) in the graph at Out4 in Figure 11a has not been materialized when y and z
point to the heap locations corresponding to this summary node. The graph in Figure 11b,
therefore, indicates that y and z may possibly point to two different heap locations on a list
which is never true at Out6 of the program. Additionally, due to the lack of materialization,
this method is not able to determine list reversal and list insertion programs. Finally, Sagiv et
al. [75] highlight, “this method does not perform strong updates for a statement of the form
x.f := null, except under very limited circumstances.”

5.2

Summarization Using Variables

Variable based summarization technique has been used in shape analysis. Shape analysis
encompasses all algorithms that compute the structure of heap allocated storage with varying
degrees of power and complexity [78]. Heap nodes not pointed to by any root variable are
summarized as a single summary node. When a program statement creates a pointer from a
new root variable to one of the heap locations represented by the summary node, the algorithm
materializes the summary node. It creates two nodes—one representing a single materialized
heap node pointed to by the new root variable and the other representing the remaining
summary nodes not pointed to by any root variable. We describe below some shape analysis
techniques that summarize using variables.
• Sagiv et al. [75,76] distinguish between heap locations by their pointed-to-by-x predicate
values for all variables x in the program7 . We use the running program in Figure 10a
to illustrate various forms of the shape analysis techniques. Unbounded memory graphs
of the program are shown in Figure 10b and Figure 10c. Fixpoint computation of the
bounded shape graph [75] at Out6 is shown in Figure 12c. Intermediate steps are shown
in Figures 12a and 12b. Let us see how these are obtained. Figure 12a shows a shape
graph at Out4 which contains a node pointed to by both x and y. This node in turn points
to a summary node through link f representing an unbounded number of dereferences
of field f. At Out5 , z points to a node y.f of Figure 12a. For this, a node (pointed
to by z) is created by materializing the summary node y.f. At Out6 , y points to this
materialized node (pointed to by z) (shown in Figure 12b). In the subsequent iteration
of the loop, y and z point to a subsequent node (shown in Figure 12c). The remaining
nodes (not pointed to by any of x, y, and z—those between x and y and those beyond
y) get summarized (represented using dashed lines) as shown in Figure 12c. Here we see
that node pointed to by x either directly points to the node pointed to by y (or z) via
7

A generalized approach of shape analysis [75] is TVLA [77], which uses summarization using generic
instrumentation predicates (see Section 5.3 and Figures 12d and 12e).

May 2015

21

5.2

Summarization Using Variables
f
y

f
f

f
x y

f

x

(a) Shape graph
Out4 [75, 77].

(b) Shape graph at Out6 after one
iteration of statements 5 and 6
[75, 77].

at

x

rx ,
ry , rz

rx
f

f

f
z

f

rx ,
ry , rz

rx

f

x

rx ,
ry , rz

rx
f

(d) Shape graph at Out6 after two iterations of
statements 5 and 6 [77].

y

z

(c) Shape graph at Out6 after
fixpoint [75].

f
y

f
f

x

f
rx

f
z f

f
f

rx ,
ry , rz
f

y

z

f

(e) Shape graph at Out6 after fixpoint [77]. The
two summary nodes are distinguished based on
whether they are reachable from root variables
x, y, and z.

Figure 12. Summarization using variables [75] is shown in Figures 12a, 12b, and 12c.
Summarization using generic instrumentation predicates [77] is shown in Figures 12a, 12b,
12d, and 12e for the program in Figure 10a. Pointer rx denotes whether any variable x can
transitively reach the node. It can be seen that variable z materializes the summary node
pointed to by y.f in Figures 12a and 12b.

field f or points to an unbounded number of nodes before pointing to the node pointed
to by y (or z) via field f.
Let us compare the shape graphs produced by Sagiv et al. [75] (Figures 12a and 12c)
with those of Chase et al. [15] (Figures 11a and 11b). The graphs at Out4 shown in
Figure 11a and Figure 12a store identical information. However, the graph at Out6
shown in Figure 12c is more precise than the graph at Out6 in Figure 11b—unlike the
latter, the former is able to indicate that y and z always point to the same location on
the list due to materialization.
• An imprecision in shape analysis is that its summary nodes do not remember the exact
count of the number of concrete nodes represented by a summary node in an abstract
heap graph. These counts are useful in checking termination of the programs that needs
to consider the size of the list being accessed. An interesting solution to this problem is
the use of a counter with every such summary node in the heap graph in order to denote
the number of concrete heap locations represented by the summary node [7]. This is
used to define a counter automaton abstraction of the state transition behaviour of heap
manipulating programs. This is illustrated in Figure 13 for the program in Figure 10a.
With the use of variables i, j, and k for counters, the algorithm ensures that the analysis
is not unbounded. The automaton starts with a heap graph containing one summary
node (with counter i), pointed to by x and y at In5 . It proceeds to Out5 if counter i > 1,
and materializes the node into a unique node (with a new counter j = 1) pointed to by x
and y, and the remaining summary node (with counter i) pointed to by z. Here counter i
22

Heap Abstractions

5.3

Summarization Using Generic Instrumentation Predicates

i

In5

x, y
[i > 1]
i := i − 1
j := 1

Out5

j

f

x, y

Out6

j
x

i
z

f

Out5

j

f

x
j := j + k

k
y

f

i
z

[i > 1]
i := i − 1
k := 1

i
y, z

Figure 13. Summarization using variables: Counter automaton [7] for the program statements
5 to 6 in Figure 10a is shown. States of the automaton denote the abstract heaps at the program
points shown. Edges of the automaton denote the condition of transition in the automaton.
Counter variables (i, j, and k) corresponding to each abstract node in the heap are depicted
inside the node itself.

used at In5 is decremented at Out5 . The graph at Out5 is then transformed to Out6 under
the influence of program statement 6. To further transform this graph from Out6 to Out5
in the loop, if counter i > 1, it materializes the summary node pointed to by y at Out6
into a new node (with a new counter k = 1) pointed to y, and the remaining summary
node (with counter i) pointed to by z. Here counter i used at Out6 is decremented by
one at Out5 . In the transformation from Out5 to Out6 , since y will start to point to
z, the node with counter k will not be pointed to by any variable. Therefore, nodes
with counters k and j are merged, and their counter values updated (added up) at Out6 .
Bouajjani et al. [7] have used these counters for verifying safety and termination of some
sorting programs.

5.3

Summarization Using Generic Instrumentation Predicates

We describe below some other generic instrumentation predicates based summarization
techniques, including TVLA, type propagation analyses, acyclic call paths, and context free
grammars that have been used for a store based heap model.
• As an improvement over the summarization technique using only variables [75] (see
Section 5.2), the following predicates are used in order to summarize heap nodes more
precisely [77, 78, 90].
– pointed-to-by-x property denotes whether a heap node is pointed directly by variable
x.
May 2015

23

5.3

Summarization Using Generic Instrumentation Predicates

– reachable-from-x-via-f property denotes whether variable x can transitively reach
a heap node via field f .
We use the running program in Figure 10a to illustrate the summarization. Unbounded
memory graphs at Out4 and Out6 of the program are shown in Figures 10b and 10c.
Fixpoint computation of a bounded shape graph using predicates pointed-to-by-x and
reachable-from-x-via-f for summarization at Out6 is shown in Figure 12e. Intermediate
steps are shown in Figures 12a, 12b, and 12d. We have already explained the bounded
shape graph obtained using only pointed-to-by-x predicate [75] for summarization at
Out6 in Figure 12c (see Section 5.2). Compare Figures 12c and 12e to observe that the
bounded shape graphs obtained are the same with respect to the nodes pointed to by a
root pointer variable; however, they differ with respect to the summary nodes not
pointed to by any root pointer variable. This is because of the use of the additional
predicate reachable-from-x-via-f ; this predicate is denoted as rx , ry , and rz in
Figures 12d and 12e. To see how Figure 12e is obtained, further observe the following
in the intermediate step shown in Figure 12d: the node pointed to by rx is kept
separate from the summary node pointed to by rx , ry , and rz . Therefore, the shape
graph in Figure 12e represents unbounded dereferences of field f following root node x
and another sequence of unbounded dereferences of field f following root node y (or z).
This paper builds a parametric framework, which allows the designer of shape analysis
algorithm to identify any desired heap property. The designer can specify different
predicates in order to obtain more useful and finer results, depending on the kind of
data structure used in a program. For example, the use of predicate “is shared” gives
more precise sharing information, and the use of predicate “lies on cycle” gives more
precise information about cycles in the heap memory. Further, 3-valued predicates
(TVLA) [77, 78, 90] help in describing properties of the shape graph using three values,
viz. false, true, and don’t know. Therefore, both may and must pointer information can
be stored. Shape analysis stores and summarizes heap information precisely, but at the
same time, it is expensive due to the use of predicates for each node [10].
• Another way of summarizing unbounded heap locations is based on the types of the heap
locations. Sundaresan et al. [87] merge unnamed heap nodes if the types reaching the
heap locations are the same. For example, for some variables x and y containing field f,
heap locations x.f and y.f are merged and represented as C.f if x and y point to objects
whose class name is C. This method has been used in literature to determine at compile
time which virtual functions may be called at runtime. This involves determining the
runtime types that reach the receiver object of the virtual function. This requires data
flow analysis to propagate types of the receiver objects from allocation to the method
invocation. These techniques that perform data flow analysis of types are called type
propagation analyses [19].
• Lattner and Adve [51] point out that if heap objects are distinguished by allocation sites
with a context-insensitive analysis8 , precision is lost. This is because it cannot segregate
distinct data structure instances that have been created by the same function i.e. at the
same allocation site via different call paths in the program. To overcome this imprecision,
Lattner and Adve [51, 52] propose to name heap objects by the entire acyclic call paths
through which the heap objects were created. They compute points-to graphs called
Data Structure graphs, which use a unification-based approach [86]. Here, all heap nodes
pointed to by the same pointer variable via the same field are merged; in other words,
8

24

A context-sensitive analysis examines a given procedure separately for different calling contexts.

Heap Abstractions

5.3

Summarization Using Generic Instrumentation Predicates
x

APPEND(x,y) :=
if (null x) then y
else cons(car(x),APPEND(cdr(x),y))

APPEND
1

1
1

1
1

1
1

1

(a) Functional language program.

.
.
.

1

1

1

1

y

APPEND1 → cons1 .car1 | cons2 .APPEND1 .cdr1
APPEND2 → ǫ | cons2 .APPEND2
(b) Context free grammar for the program in
Figure 14a [37]. Fi denotes the ith argument
of function F .

(c) Computing result of APPEND from arguments
x and y. The two edges in each rectangle
denote car and cdr fields, respectively. Dashed
locations depict nodes unreachable from the
result of APPEND; therefore, can be garbage
collected.

Figure 14. Computing context free grammar for a functional language program in order to
garbage collect unreachable nodes [37].

every pointer field points to at most one heap node. The use of acyclic call paths and
unification-based approach help in summarizing the potentially infinite number of heap
nodes that can be created in recursive function calls and loops.
• Another way of summarizing is to build a context free grammar of the heap [37]. This has
been done for functional programs, which consist of primitive functions like cons, car,
and cdr. This grammar has been used to detect garbage cells in a functional program
through compile time analysis. It is based on the idea that the unshared locations passed
as parameter to a function that are not a part of the final result of the function, can be
garbage collected after the function call. We describe this by reproducing from the paper
the definition of function APPEND in Figure 14a. Data structures pointed to by variables
x and y (shown in Figure 14c) are passed as arguments to APPEND function. The circular
nodes are reachable from the root of the result of the APPEND function; these circular
nodes can be identified as x(.cdr)∗ .car and y. However, the dashed locations, which
belong to x, are not reachable from the root of the result of the APPEND function; these
dashed locations can be identified as x(.cdr)∗ . These dashed locations can, therefore, be
garbage collected.
In order to identify argument locations that are unreachable from the result of the
called function, the paper analyses the usage of each argument of the called function by
constructing a context free language of each argument. The grammar constructed is
shown in Figure 14b. Each argument of a function, say F (x1 , x2 , . . . , xi , . . . ), is
represented by a non-terminal in a context free grammar. Derivation rule for the ith
argument xi of function F is Fi → s1 | s2 | · · · | sk , where s1 , s2 , . . . , sk are all the strings
obtained from the function body. The first and the second lines in Figure 14b are the
context free grammars of APPEND1 and APPEND2, which denote arguments x and y of the
program in Figure 14a. The strings on the right hand side of the grammar consist of
car1 , cdr1 , cons1 , and cons2 , and user defined functions. Each function name is used
with a subscript indicating the position of argument in the function. Let us study the
May 2015

25

Summarization Using Generic Instrumentation Predicates
v

w

z

hea
d −1

tail −1

3 w := cdr(x) 2

y

head

1 x := cons(y, z) 1

2 v := car(x) 2

x

ta
il

5.3

Figure 15. A control flow graph of a program and its equation dependence graph. Edges
in the equation dependence graph have been labelled with head, tail, head−1 , and tail−1 ;
those shown without labels represent identity relation (label id) [68].

grammar of function APPEND shown in Figure 14b. APPEND2 in the second line denotes
the usage of the second argument of APPEND, y in the function definition. It would
either be used as it is or would be passed as the second argument to cons (denoted by
cons2 ). APPEND1 in the first line denotes the usage of the first argument of APPEND, x in
the function definition. The strings generated by APPEND1 grammar are of the form
consk2 .cons1 .car1 .cdrk1 . By reading the string in the reverse order, we can see that
APPEND decomposes list x, k number of times by the application of cdr, and then a car
selects the element at that position, followed by a cons1 on the element to make it the
left child of a new location, which itself will be acted on by cons2 the same k number of
times. The context free grammar is used to identify reachable paths from the
argument. For example, using the grammar APPEND1, i.e. argument x, it can be seen
that string (cdr1 )k .car1 (obtained from the reverse of string consk2 .cons1 .car1 .cdrk1 )
denotes the locations x(.cdr)∗ .car, which are reachable from the result of APPEND. The
rest of the locations in argument x are unreachable and can be garbage collected.
Liveness based garbage collection has been performed using grammars also by Asati et
al. [2] for creating the notion of a demand that the execution of an expression makes
on the heap memory. In somewhat similar lines, liveness based garbage collection for
imperative programs has been performed using a storeless model by Khedker et al. [43]
(see Section 4.2).
• Another way of building context free grammar of heap access paths is by posing shape
analysis as CFL reachability problem. This has been done for Lisp like languages that do
not support strong updates [68]. A CFL reachability problem is different from the graph
reachability problem in the sense that a path between two variables is formed only if the
concatenation of the labels on the edges of the path is a word in the specified context free
language. Equation dependence graph is constructed by marking all program variables
at each program point in the program’s control flow graph. The edges between these
26

Heap Abstractions

5.4

Summarization Using Allocation Sites and Other Generic Instrumentation Predicates
variables are labelled with head, tail, head−1 , and tail−1 .
We illustrate the use of these labels in the equation dependence graph in Figure 15. For
statement 1, x := cons(y, z), label head is marked on the edge from y before statement
1 to x after statement 1. Similarly, label tail is marked on the edge from z before
statement 1 to x after statement 1. This denotes that x derives its head from y and tail
from z. For program statement 2, v := car(x), label head−1 is marked on the edge from
x before statement 2 to v after statement 2. This denotes that v gets its value using the
head of y. Similarly, tail−1 is labelled for statement 3, w := cdr(x).
Heap language in terms of access paths is identified by concatenating, in order, the labels
of the edges on the paths of the equation dependence graph. For example, the path from
z before statement 1 to w after statement 3 shows that w gets the value z.tail.id.tail−1 ,
which is simply z. Heap properties can be obtained by solving CFL reachability problems
on the equation dependence graph using the following context free grammars [68]:
– id path → id path id path | head id path head−1 | tail id path tail−1 | id | ǫ
This grammar represents paths in which the number of head−1 (tail−1 ) are
balanced by a matching number of head (tail), implying that the heap was used
through head−1 (tail−1 ) as much as it was constructed using head (tail).
– head path → id path head id path
tail path → id path tail id path
These grammars represent paths in which the number of head (tail) is more than
the number of head−1 (tail−1 ), implying that the amount of heap allocated using
head (tail) is more than the amount of heap dereferenced using head−1 (tail−1 ).

5.4

Summarization Using Allocation
Instrumentation Predicates

Sites

and

Other

Generic

As an attempt to reduce the cost of shape analysis, recency-abstraction [4] is used as an
approximation of heap allocated storage. This approach does not use the TVLA tool;
however, it uses concepts from 3-valued logic shape analysis [77]. Here, only the most
recently allocated node at an allocation site is kept materialized representing a unique node.
Therefore, its precision level is intermediate between (a) one summary node per allocation
site and (b) complex shape abstractions [77]. Note that for the program in Figure 10a,
Figure 16a shows that summarization based only on allocation sites creates a summary node
for objects allocated at site 2. Here the summary node is not materialized; therefore,
variables x and y point to the summary node itself at Out4 . Consequently, allocation site
based summarization cannot derive that x and y are must-aliased. Recency-abstraction is
illustrated in Figure 16b for the unbounded graph of Figure 10b. Due to materialization of
the most recently allocated node, the method is able to precisely mark x and y as
must-aliases at Out4 . However, materializing only once is not enough and introduces
imprecision at Out6 . This is shown in Figure 16c, where y and z are marked as may-aliases
(instead of the precise must-alias, as shown by the unbounded runtime memory graph in
Figure 10c).

5.5

Summarization Using Higher-Order Logics

Heap can be abstracted as logical structures of specialized logic like separation logic, which are
more powerful than simple predicate logic. Also, the efficiency of shape analysis can be boosted
by representing independent portions of the heap using formulae in separation logic [69]. To
elaborate, it exploits spatial locality of a code i.e. the fact that each program statement
May 2015

27

5.5

Summarization Using Higher-Order Logics

f

f

Site 2

Site 2

x y

x y

(a) Summarization using only
allocation sites does not
materialize summary node
Site 2. Figure shows alias
graph at Out4 .

f

Site 2

(b) Alias graph at Out4 . With
the materialization of the
most-recent Site 2, hx, yi are
marked as must-aliases [4].

f
Site 2
x

f

Site 2
y

z

(c) Alias graph at Out6 . Node
Site 2 is not materialized
further.
Dashed edges
denote may-alias [4].

Figure 16. Summarization using allocation sites and other generic instrumentation predicates
[4] for the program in Figure 10a is shown in Figures 16b and 16c. For comparison,
summarization using only allocation sites is shown in Figure 16a.

accesses only a very limited portion of the concrete state. Using separation logic, the portion
of heap that is not accessed by the statement(s) can be easily separated from the rest and later
recombined with the modified heap after analysing the statement(s). This dramatically reduces
the amount of reasoning that must be performed, specially if the statement is a procedure call.
Assertions expressed in separation logic may produce infinite sets of concrete states. A
fixpoint computation can be achieved using finitely represented inductive predicate
assertions [10, 26] like list(), tree(), dlist(), representing unbounded number of concrete
states, shaped like a linked list, tree, doubly linked list, respectively. The abstraction comes
from not tracking the precise number of inductive unfoldings from the base case. Note that
unlike logics on storeless model which use access paths and hide locations in their modeling,
separation logic explicates heap locations; therefore, separation logic is categorized under a
store based model.
In separation logic, assertion A 7→ B denotes memory containing heap location A, which
points to heap location B. Assertion A ∗ B denotes memory represented as a union of two
disjoint heaps (i.e. with no common heap locations)—one satisfying A and the other satisfying
B. Assertion A = B denotes that A and B have equal values. Assertion A ∧ B denotes a heap
that satisfies both A and B.
We work out the assertions using separation logic for the program in Figure 10a. In
Figure 17a, we have shown the heap graph and also the assertions in separation logic at Out4
over three iterations of statements 2, 3, and 4 in a loop. Assertion in the first iteration says
that x and y hold the same value, which points to a null value. Assertion in the second iteration
says that x and y hold the same value, which points to a new variable X′ . Separation logic
introduces a variable X′ , which is not used anywhere in the program code. This X′ points to
a null value. Assertion in the third iteration says that x and y hold the same value, which
points to another new variable X′′ , which further points to X′ ; X′ points to a null value. If we
continue in this way, we will get ever longer formulae. This unboundedness is abstracted using
the predicate list(), where list(u, v) says that there is a linked list segment of unbounded
length from u to v. This predicate has the following recursive definition (here emp denotes an
empty heap):
list(u, v) ⇔ emp ∨ ∃w.u 7→ w ∗ list(w, v)
With this, we obtain the abstraction by using the following operation in the second iteration
at Out4 .
28

Heap Abstractions

X′

x y

x y
f

null

f

f

f

null

X′

X′′

x y

f

f

null

x = y ∧ x 7→ null

x = y ∧ x 7→ X′ ∗ X′ 7→ null
≡ x = y ∧ list(x, null)

x = y ∧ x 7→ X′′ ∗ X′′ 7→ X′ ∗ X′ 7→ null
≡ x = y ∧ list(x, null)

Iteration 1

Iteration 2

Iteration 3

(a) Heap at Out4 obtained after respectively three iterations of the program. X′ and X′′ are new
variables not used anywhere in the program code.

X′′′

x
f

y z
f

f

...

f

null

y = z ∧ x 7→ X′′′ ∗ X′′′ 7→ y ∗ list(z, null)
≡ y = z ∧ list(x, z) ∗ list(z, null)

(b) Heap at Out6 after fixpoint computation. X′′′ is a new variable not used anywhere in the program
code.

Figure 17. Summarization using separation logic [10, 26] for the program in Figure 10a.

replace

x = y ∧ x 7→ X′ ∗ X′ 7→ null

with

x = y ∧ list(x, null)

Using a similar way of synthesizing, the assertion at Out6 (shown in Figure 17b) can be obtained
to be y = z ∧ list(x, z) ∗ list(z, null).
The SpaceInvader tool [18] also uses separation logic. The tool works on a subset of
separation logic for inferring basic properties of linked list programs.

6

Summarization in Hybrid Heap Model

For heap applications that need to capture both points-to related properties (using a store
based model) and alias related properties (using a storeless model), the heap memory is best
viewed as a hybrid model combining the storeless and the store based heap model. This model
can also be summarized using various techniques, like allocation sites, k-limiting, variables,
and other generic instrumentation predicates.

6.1

Summarization Using Allocation Sites and k-Limiting

Using the hybrid model, alias graphs record may-aliases [50]. Let us study the abstract memory
graph for the program in Figure 8a. We assume that variable x is initialised before statement
1 to point to an unbounded memory graph shown in Figure 8b. The bounded representation
of this unbounded memory graph is illustrated in Figure 18 using this technique. This method
labels each node with an access path reaching the node. If there is more than one access path
reaching a node, then this method arbitrarily chooses any one of the paths as a label for the
May 2015

29

6.2

k-Limiting Summarization

f
x

x

f

x.f

g
x.g

x.f.f
g
g

w

f

x.f.f.f

f

Site 7

f

x.f.f.f(.f)+
g
x.f.f(.f)+ .g

x.f.f.g

g
w

f

g

f
Figure 18. Summarization using allocation sites and k-limiting (k = 4) on a hybrid model [50]
at Out8 for the program in Figure 8a. Pointer variables y and z are not shown for simplicity.

node. For example, access paths x.g and w.g reach the same node; this node is arbitrarily
labelled as x.g. It can be seen in the summarized graph in Figure 18 that nodes reachable
from x via fields f and g have been summarized using k-limiting; value of k has been set to
4; therefore, the last node pointed to by variable x via field f has the label x.f.f.f(.f)+ . This
node has a self loop, which denotes that the node is a summary node of unbounded locations.
Larus and Hilfinger [50] also proposed allocation site based summarization as a way of
naming the nodes. For this, let us study locations pointed to by z and w for the program in
Figure 8a. Memory locations z(.f)∗ (or w(.f)∗ ) are allocated at program statement 7. Figure 18
shows that these nodes are summarized using allocation sites. A self loop around node, marked
with Site 7, denotes unbounded dereferences of field f. However, this summarization spuriously
stores the alias relationship hx.f.f.g, w.f.f.gi.
To handle this imprecision in summarization using allocation sites, Larus and Hilfinger [50]
distinguish nodes allocated at the same site by labeling each newly allocated node with an
aggregate of arguments passed to the allocation function (cons in Lisp). This hybrid approach
of labeling allocation sites with access paths (arguments of the allocation function) improves
the precision of the graphs. In order to limit the abstract graph to a finite size, summary nodes
are created using the concept of s-l limiting in which no node has more than s outgoing edges
(other than the nodes representing the bottom element), and no node has a label longer than
l.

6.2

k-Limiting Summarization

De and D’Souza [16] highlight an imprecision in saving pointer information as graphs. We
illustrate this imprecision using Figure 19a for statements 9, 10, and 11 of our running program
in Figure 8a. The problem is caused by the fact that a summarized object node may represent
multiple concrete objects; therefore, the analysis cannot perform a strong update on such
objects. At In9 of the program, y is aliased to the summary node x.f.f.f(.f)+ . Therefore,
strong update cannot be performed in statement 10 i.e. the pointer of y.f cannot be removed.
Hence, at Out11 , v will point to all the objects previously pointed to by y.f as well as the new
location pointed to by u. Observe that the former is imprecise.
De and D’Souza [16] believe that this imprecision is caused by storing points-to information
as graphs. Therefore, instead of using graphs, they use access paths. Their technique maps
k-limited access paths (storeless model) to sets of summarized objects (store based model)
(represented as ohni in Figure 19b and Figure 19c). For example, x → {o1} means that the
30

Heap Abstractions

6.2

u
y
x

o1
g

f

o2

o9
g
w

o6

f

f

v
o12

f

o4

o7

y

f

v

o3
g
o10
g

f

k-Limiting Summarization

f

o5
g

f

o11
g
f

z

o8

f

z

(a) Illustrating imprecision in store based model. k-limiting (k = 4) summarized graph at Out11 .
Corresponding to statements 9, 10, and 11, u points to o12, y.f points to both o4 and o12;
therefore, v also points to both o4 and o12. Here v is imprecisely aliased to x.f.f.f.

x → {o1}
x.f → {o2}
x.f.f → {o3}
x.f.f.f → {o4}
x.f.f.f.f → {o5}

w → {o6}
w.f → {o7}
w.f.f → {o8}
...
...

x.g → {o9}
x.f.f.g → {o10}
...
y → {o3, o5}
...

w.g → {o9}
w.f.g → {o10}
...
z → {o7, o8}
...

(b) k-limited (k = 4) points-to information at
In9 [16]. x.g and w.g are aliased.

x → {o1}
x.f → {o2}
x.f.f → {o3}
x.f.f.f → {o4, o12}
x.f.f.f.f → {o5}

w → {o6}
w.f → {o7}
w.f.f → {o8}
...
...

x.g → {o9}
x.f.f.g → {o10}
...
y → {o3, o5}
y.f → {o12}
...
u → {o12}

w.g → {o9}
w.f.g → {o10}
...
z → {o7, o8}
...
...
v → {o12}

(c) k-limited (k = 4) points-to information at
Out11 [16]. Variable v precisely points to only
o12 (pointed to by u) and is not aliased to
x.f.f.f.

Figure 19. Summarization using k-limiting on a hybrid model [16] for the program in
Figure 8a is shown in Figures 19b and 19c. Here ohni represents an object name and the
symbol → denotes points-to relation. For easy visualization, we have shown a summarization
on a store based model at Out11 in Figure 19a.

access path x points to (is mapped to) the object named o1. Since the access paths are precise
up to k length, like any k-limiting abstraction, it can also perform strong updates up to k
length.
In Figure 19b at In9 , y points to a summarized object {o3, o5} (pointed to by x.f.f and
x.f.f.f(.f)+ , respectively), as shown in Figure 19a. Program statement 10 updates the pointer
information of y.f. Therefore, if u points to object o12, then it is sound to say that y.f will
point only to object o12 at Out10 . However, it is not sound to say that x.f.f.f (alias of y.f) will
May 2015

31

6.3

Summarization Using Variables and Other Generic Instrumentation Predicates

point only to object o12 since y points to multiple access paths, viz. x.f.f and x.f.f.f(.f)+ .
Therefore, in Figure 19c, at Out10 , the method strongly updates y.f to {o12} (pointed to by
u), even though y points to multiple objects (o3 and o5) at In10 . Also, for sound results,
x.f.f.f is not strongly updated, and x.f.f.f points to o12 in addition to the previously pointed
object o4. Since y.f points only to o12, at Out10 , access path v also precisely points only to
the new object {o12} (pointed to by u) at Out11 .

6.3

Summarization Using Variables and Other Generic Instrumentation
Predicates

We describe below some application specific predicates that have been used in a hybrid model.
• In order to remove unreachable parts of the heap across functions in interprocedural
analysis, cutpoints are marked on the heap [72]. Cutpoints are objects which separate
the local heap of the invoked function from the rest of the heap. 3-valued logic shape
analysis (classified under the store based model) is used for summarization [77]. Each
cutpoint is identified by an access path (a feature of a storeless model) which is not
relevant to the function being called. When the function returns, the access path of
the cutpoint object is used to update the caller’s local heap with the effect of the call.
Therefore, irrelevant parts of abstract states that will not be used during the analysis
are removed by modeling the heap using both storeless and store based representations.
For example, an acyclic list pointed to by x is passed to the reverse() function, which
reverses the list performing strong updates. Let us say, before the function call, y.g.g
and x.f are aliased and y is not in scope of function reverse(). On return of the function,
we should be able to derive that y.g.g.f and x are aliased. To capture this kind of a
relationship, effect of the function on cutpoints is tracked. In this example, the second
node of list x is a cutpoint and in the function reverse() can be identified with a new alias
relationship between access paths as hC, x.fi, where C is the access path used to label the
second node (cutpoint) in the list. On return of the function reverse(), we will derive
hx, C.fi as the alias relationship. Thus, we will be able to restore the alias relationship
between x and y as hx, y.g.g.fi in the calling function.
• Connection analysis (similar to access paths used in a storeless model) along with store
based points-to analysis has been used as an abstraction [25]. This method first
resolves all pointer relationships on the stack using a store based points-to analysis,
which abstracts all heap locations as a single symbolic location called heap. All
pointers reported to be pointing to heap are then further analysed via a storeless heap
analysis, called connection analysis, and shape analysis.

7

Design Choices in Heap Abstractions

Given a confounding number of possibilities of combining heap models and summarization
techniques for heap abstractions, it is natural to ask the question “which heap abstraction
should I use for my analysis?” This question is one of the hardest questions to answer
because there is no one right answer and the final choice would depend on a wide range of
interdependent, and often conflicting, requirements of varying importance.
This section attempts to provide some guidelines based on
• the properties of heap abstractions,
• the properties of underlying analyses, and
32

Heap Abstractions

7.1

Properties of Heap Models

• the properties of programs being analysed.
The properties of heap abstractions are dominated by the properties of summarization
techniques with the properties of heap models playing a relatively minor role. Among the
properties of summarization, we explore the tradeoffs between precision and efficiency on the
one hand and expressiveness and automatability on the other. The properties of analyses
include flow- and context-sensitivity, bottom up vs. top down traversals over call graphs,
partial soundness, and demand driven nature.
These guidelines are admittedly incomplete and somewhat abstract. Because of the very
nature of heap abstractions and a large variety of uses they can be put to, these guidelines
may need deeper examination and may not be applicable directly.

7.1

Properties of Heap Models

We believe that in general,
• client analyses that explore points-to related properties are easier to model as store
based [18, 72], whereas
• analyses that explore alias related properties are easier to model as storeless [9, 18, 72].
This is because in points-to related properties, heap locations and addresses contained in
locations are important. Store based models are more natural in such situations because they
explicate all locations. On the other hand, alias related properties can leave the locations
implicit which is the case in a storeless model. The metrics like precision and efficiency are
generally not decided by the choice of heap model but by the summarization technique used.

7.2

Properties of Heap Summarization Techniques

In this section, we compare the summarization techniques with respect to efficiency, precision,
expressiveness, and automatability.
7.2.1

Precision vs. Efficiency

In general, if a client analysis requires computing complex heap properties, like shape of the
heap memory, then summarization techniques using variables, generic instrumentation
predicates, and higher-order logics are more precise. On the other hand for computing
simpler heap properties, like finding the pointer expressions that reach a particular heap
location, a client can choose more efficient summarization techniques like those based on
k-limiting and allocation sites.
We describe the other considerations in precision-efficiency tradeoff for specific
summarization techniques.
• k-limiting. This technique does not yield very precise results for programs that
manipulate heap locations that are k indirections from some pointer variable of the
program as illustrated in Figures 5b and 6b. k-limiting merges the access paths that
are longer than a fixed constant k. Thus the tail of even a non-circular linked list will
be (conservatively) represented as a possibly cyclic data structure. Due to the
summarization of heap locations that are beyond k indirections from pointer variables,
this technique lacks strong update operations on these heap locations. Consequently,
Sagiv et al. [75] observe, “k-limiting approach cannot determine that either list-ness or
circular list-ness is preserved by a program that inserts an element into a list.” However,
May 2015

33

7.2

Properties of Heap Summarization Techniques

k-limiting gives reasonably precise results if the user program being analysed does not
need strong updates.
The efficiency of the analysis is heavily dependent on the value of k; larger values improve
the precision but may slow down the analysis significantly [3]. The analysis may be
extremely expensive because as observed by Sagiv et al. [75] “the number of possible shape
graphs is doubly exponential in k.” This is because heap locations beyond k indirections
from some pointer variable have to be (conservatively) assumed to be aliased to every
other heap location. Hence, k-limiting is practically feasible only for small values such as
k ≤ 2 [79]. The price to pay is reduced precision as shown by Chase et al. [15]. In general
it is difficult for a client analysis to know the best value of k a-priori and it should be
guided by empirical observations on representative programs.
• Allocation sites.
This technique may be imprecise when memory allocation is
concentrated within a small number of user written procedures. In such situations,
nodes allocated at the same allocation site but called from different contexts are
merged even though they may have different properties. Figure 18 contains an example
of imprecision using allocation sites. Chase et al. [15] state that “allocation site based
method cannot determine that list-ness is preserved for either the insert program or the
reverse program on a list” because of merging of nodes.
However, regarding efficiency, Sagiv et al. [76] note, “the techniques based on allocation
sites are more efficient than k-limiting summarizations, both from a theoretical
perspective [15] and from an implementation perspective [3].” The size of an allocation
site based graph is bounded by the number of allocation sites in the program.
Therefore, majority of client analyses are likely to find this technique space efficient on
most practical programs.
• Patterns. Identifying precise repeating patterns is undecidable in the most general case
because a repeated advance into the heap may arise from an arbitrarily long cycle of field
dereferences [60]. Therefore, generally the focus remains on detecting only consecutive
repetitions of the same type of field accesses which may be imprecise. Also, it seems
difficult for an analysis to determine if an identified repetition will occur an unbounded
number of times or only a bounded number of times. This approach has been found to
be more efficient than TVLA based shape analysis techniques for discovering liveness of
heap data [43].
• Variables. For complex shape graphs, summarization using variables may be more precise
than k-limiting. Chase et al. [15] observe that two nodes need not have similar properties
just because they occur k indirections away from the root variable in an access path. On
the other hand, two nodes which are pointed to by the same set of variables are more likely
to have similar properties. Further, summarization using variables can perform strong
nullification in a larger number of cases; therefore, it may be more precise. However,
there are situations where summarization using variables can also be imprecise: since
it merges nodes not pointed to by any root variable, sometimes nodes are abstracted
imprecisely as illustrated in Figure 5d. Contrast this with the precise summarization of
Figure 5c.
In general this technique has been found to be inefficient. Since each shape graph node is
labelled with a set of root variables in this technique, Sagiv et al. [75] state, “the number
of shape nodes is bounded by 2|Var| , where Var is the number of root pointer variables
in the program.” They further note, “unfortunately for some pathological programs the
34

Heap Abstractions

7.2

Properties of Heap Summarization Techniques

number of shape nodes can actually grow to be this large, although it is unlikely to arise
in practice.”
• Generic instrumentation predicates. Both the precision and efficiency of a client analysis
depends on the chosen predicate. By identifying one or more suitable predicates, a client
analysis can strike a balance between precision and efficiency.
The implementation of generic instrumentation predicates using TVLA [77] has
potentially exponential runtime in the number of predicates. Therefore, it is not
suitable for large programs [10].
• Higher-order logics. These techniques have the capability of computing complex heap
properties. With the use of program annotations in the form of assertions and loop
invariants, they can compute surprisingly detailed heap properties [38]. Unlike TVLA,
they can also produce counter examples for erroneous programs [63]. However, these
techniques are generally used to verify restricted data structures [8], without considering
the full behaviour of the program and have to be made less detailed for large programs [63]
since they are highly inefficient. An analysis needs to use simpler and less precise logics in
order to improve scalability. For example, Distefano et al. [18] use a subset of separation
logic as the domain of their analysis; the domain is less powerful because it does not
allow nesting of ∗ and ∧ operators.
These techniques may be highly inefficient as they include higher-order and undecidable
logics. For example, quantified separation logic is undecidable [11]. For termination,
these techniques require program annotations in the form of assertions and loop
invariants [8, 38, 63]. Consequently, analyses based on higher-order logics cannot be
made fully automatic. Since the effort of annotating the program can be significant,
these techniques can work efficiently only on small programs [38]. Therefore, these are
mostly used for teaching purposes [38] in order to encourage formal reasoning of small
programs. Again, since they are inefficient, these are considered useful to verify only
safety critical applications [63] where the effort of annotating the program is justified
by the complex properties that these techniques can derive. However, as compared to
TVLA, these techniques are sometimes more scalable due to the use of loop invariants;
empirical measurements show high speedup in these techniques where the use of loop
invariants is more efficient than a fixpoint computation required by TVLA [63]. An
advantage of separation logic is its efficiency due to the following: once the program is
analysed for a part of the memory, it can directly be used to derive properties for the
extended memory [82].
7.2.2

Expressiveness vs. Automatability

Here we discuss degree of expressive power and automation offered by heap summarization
techniques using predicates (for example, k-limiting, allocation sites, variables, pattern, and
other user-defined predicates) and those using higher-order logics.
• Predicates. Parameterised frameworks like TVLA summarize heap data based on any
desired user-defined predicate. Therefore, they achieve good expressiveness as per the
user’s requirements. However, the predefined predicates (for example, k-limiting,
allocation sites, variables, pattern) lack this expressiveness.
Automation of summarization techniques using user-defined predicates in TVLA is not
difficult since TVLA allows only simple predicates. Also, several automated tools are
already available for predefined predicates. For example, LFCPA [42] performs automatic
heap analysis using allocation site based summarization.
May 2015

35

7.3

Properties of Underlying Heap Analysis

• Higher-order logics. Unlike summarizations based on predicates, summarizations based
on higher-order logics do not need to work with a predefined user predicate; with the
use of heap specialized operators and rules, the latter can build upon basic predicates
to be able to compute complex properties of the heap. Depending on the underlying
logic, a client may find these summarization techniques to be more powerful and easier
to express.
However, summarization techniques using higher-order logics are not fully automated and
need user intervention for inference of non-trivial properties specially if the technique is
based on undecidable logics.

7.3

Properties of Underlying Heap Analysis

The choice of heap summarization technique is sometimes dependent on the design dimensions
of the underlying analysis that the client uses. We describe some such dependencies.
• Flow-sensitive analysis.
increased by

The precision benefits of a flow-sensitive analysis can be

• using TVLA whose 3-valued logic enables a more precise meet operation by
distinguishing between the may (i.e. along some paths), must (i.e. along all paths)
and cannot (i.e. along no path) nature of information discovered.
• using techniques that aid strong updates: summarization techniques based on
variables [75, 77] and k-limiting [16], and the materialization [75, 77] of summary
nodes.
• Context-sensitive analysis. A context-sensitive analysis examines a given procedure
separately for different calling contexts. If such a procedure contains an allocation
statement, the allocation site based summarization should be able to distinguish
between the nodes representing different calling contexts. This can be achieved by heap
cloning [91]. In the absence of replication of allocation site based nodes for different
calling contexts, the precision of analysis reduces significantly [65].
• Bottom-up analysis. A bottom-up interprocedural analysis traverses the call graph
bottom up by processing callees before callers. It constructs a summary of the callee
procedures that may access data structures whose allocation is done in the callers.
Thus the allocation site information may not be available in a callee’s heap summary.
Therefore, allocation site based summarization cannot be used with bottom-up
analyses; instead summarization using patterns has been used for computing procedure
summaries [22, 58, 60].
• Partially sound analysis and demand driven analysis. Soundness of an analysis requires
covering behaviours of all (possibly an infinite number of) execution paths. In many
situations such as debugging, useful information may be obtained by covering the
behaviour of only some execution paths. Such partially sound analyses9 are often
demand driven. The other flavour of demand driven analyses (such as assertion
verification) may need to cover all execution paths reaching a particular program point
but not all program points. In either case, these analyses examine a smaller part of the
input program and hence may be able to afford expensive summarization techniques.
Here k-limiting and higher-order logics based summarization techniques permit the
9

Not to be confused with “soundy” analyses which refer to partially unsound analyses that ignore some well
identified hard to analyse constructs [56].

36

Heap Abstractions

7.4

Properties of Programs

client to choose a larger value of k and a more complex logic, respectively thereby
improving precision. Likewise, parametric frameworks like TVLA can also be used with
more complex predicates. Observe that, allocation site and variable based techniques
do not have any inherent parameter for which the analysis may be improved.

7.4

Properties of Programs

The suitability of a technique depends on various properties of the input program. These are
discussed below.
• k-limiting. If the input program contains a small number of indirections from pointer
variables, k-limiting summarization based on a suitable choice of empirically observed k
would give reasonable results.
• Allocation sites. For input programs where allocations are made from sites that are
distributed over the program, rather than being made from a small set of procedures,
summarization using allocation sites will be able to preserve heap properties efficiently.
• Patterns. For input programs containing simple repeating patterns, summarization
techniques based on patterns can produce useful summaries.
• Variables. In our opinion, summarizations based on variables are precise in generally all
types of programs using the heap; however they are usually not as efficient as techniques
using k-limiting, allocation sites, and patterns.
• Higher-order logics. Techniques based on logics are inefficient and need manual
intervention. Therefore, their usefulness may be limited on small input programs.

8

Heap Analyses and Their Applications

In this section, we categorize applications of heap analyses and list common heap analyses in
terms of the properties that they discover.

8.1

Applications of Heap Analyses

We present the applications of heap analyses under the following three broad categories:
– Program understanding. Software engineering techniques based on heap analysis are used to
maintain or reverse engineer programs for understanding and debugging them. Heap related
information like shape, size, reachability, cyclicity, and others are collected for this purpose.
Program slicing of heap manipulating programs [44] can help in program understanding by
extracting the relevant part of a program.
– Verification and validation. Heap analysis is used for detecting memory errors at compile
time (for example, dereferencing null pointers, dangling pointers, memory leaks, freeing
a block of memory more than once, and premature deallocation) [25, 36, 57, 80]. Sorting
programs that use linked lists have been verified using heap analyses [53].
– Optimization. Modern compilers use heap analysis results to produce code that maximizes
performance. An optimization of heap manipulating programs is the garbage collection of
accessible yet unused objects [2, 43] which are otherwise beyond the scope of garbage
collection that depends purely on runtime information. Transformation of sequential heap
manipulating programs for better parallel execution involves heap analysis [5]. Heap
May 2015

37

8.2

Heap Analyses

analysis also helps in performing data prefetching based on future uses and updates on
heap data structures in the program [25]. Data locality of dynamically allocated data has
been identified and exploited using heap analysis by Castillo et al. [12].

8.2

Heap Analyses

A compile time program analysis that needs to discover and verify properties of heap data
could perform one or more of the following analyses.
• Shape analysis [24, 77, 90] also called storage analysis discovers invariants that describe
the data structures in a program and identifies alias relationships between paths in the
heap. Its applications include program understanding and debugging [20], compile time
detection of memory and logical errors, establishing shape properties, code optimizations,
and others.
• Liveness analysis of heap data statically identifies last uses of objects in a program to
discover reachable but unused heap locations to aid garbage collection performed at
runtime [2, 37, 43, 80].
• Escape analysis is a method for determining whether an object is visible outside a given
procedure. It is used for (a) scalar replacement of fields, (b) removal of synchronization,
and (c) stack allocation of heap objects [45].
• Side-effect analysis finds the heap locations that are used (read from or written to) by
a program statement. This analysis can optimize code by eliminating redundant loads
and stores [61].
• Def-use analysis finds point pairs of statements that initialize a heap location and then
read from that location. This analysis is used to check for the uses of undefined variables
and unused variables [61].
• Heap reachability analysis finds whether a heap object can be reached from a pointer
variable via field dereferences for detecting memory leaks at compile time [6].
• Call structure analysis disambiguates virtual calls in object-oriented languages and
function pointers. Presence of heap makes this disambiguation non-trivial. Instead of
relying on a call graph constructed with a relatively less precise points-to analysis, the
program call graph can be constructed on-the-fly with pointer analysis [66, 85, 89].
Receiver objects of a method call can also be disambiguated in order to distinguish
between calling contexts using object-sensitivity [61, 84] and type propagation
analysis [87].

9

Engineering Approximations for Efficiency

Given the vital importance of pointer analysis and the inherent difficulty of performing precise
pointer analysis for practical programs [13, 35, 49, 67], a large number of investigations involve
a significant amount of engineering approximations [41]. A detailed description of these is
beyond the scope of this paper because its focus is on building the basic concepts of various
modeling and summarization techniques for heap. Here we merely list some notable efforts in
engineering approximations used in heap analysis.
Since heap data is huge at compile time Calcagno et al. [10] perform
compositional/modularized analysis, i.e. using function summaries. Heap data can also be
38

Heap Abstractions

restricted by propagating the part of the heap that is sufficient for a procedure [10, 18, 26, 72].
Amount of heap data collection can be controlled by a demand-driven analysis using client
intervention [27, 85]. Rountev et al. [73] restrict the scope of program where high precision is
required. For example, they determine program fragments where accuracy is vital (like
regions of code, pointer variables) and find ways to make the results precise for only for those
critical regions. They have also performed safe analysis for incomplete programs. Limiting
the analysis to live and defined variables of the program has also helped in achieving
scalability without any loss of precision [1, 16, 42]. An inexpensive flow-insensitive heap
analysis over an SSA form [21] of a program seeks a middle ground between a flow-sensitive
and a flow-insensitive heap analysis. Incremental computations [88] and efficient encoding of
information by using BDDs [89] are amongst other engineering techniques employed for
efficient heap analysis.
Given a large body of work on building efficient approximations, Michael Hind observes that
although the problem of pointer analysis is undecidable, “fortunately many approximations
exists” and goes on to note that “unfortunately too many approximations exist” [32]. We
view this trend as unwelcome because a large fraction of pointer analysis community seems to
believe that compromising on precision is necessary for scalability and efficiency. Amer Diwan
adds, “It is easy to make pointer analysis that is very fast and scales to large programs. But
are the results worth anything?” [32].
In our opinion, a more desirable approach is to begin with a careful and precise modeling
of the desired heap properties even if it is not computable. Then the analysis can be
gradually refined into a computable version which can further be refined to make it scalable
and efficient to make it practically viable. Tom Reps notes that “There are some interesting
precision/efficiency trade-offs: for instance, it can be the case that a more precise pointer
analysis runs more quickly than a less precise one” [32]. Various implementations [42, 54, 84]
show that this top-down approach does not hinder efficiency. In fact increased precision in
pointer information not only causes a subsequent (dependent) analysis to produce more
precise results, it also causes the subsequent analysis to run faster [81].

10

Related Surveys

We list below some investigations that survey heap abstractions, either as the main goal or as
one of the important subgoals of the paper.
Hind [32], Ryder [74], and Smaragdakis and Balatsouras [83] present a theoretical discussion
on some selective pointer analysis metrics like efficiency, precision, client requirements, demand
driven approaches, handling of incomplete programs, and others. They also discuss some chosen
dimensions that influence the precision of heap analyses like flow-sensitivity, context-sensitivity,
field-sensitivity, heap modeling, and others. Smaragdakis and Balatsouras [83] present some of
these aspects in the form of a tutorial. Hind [32] provide an excellent compilation of literature
on pointer analysis which are presented without describing their algorithms.
Sridharan et al. [85] present a high-level survey of alias analyses that they have found useful
from their industrial experiences. Hind and Pioli [33] give an empirical comparison of precision
and efficiency of five pointer analysis algorithms. Ghiya [23] provides a collection of literature
on stack and heap pointer analyses and highlights their key features. Sagiv et al. [78] and
Nielson et al. [64] have a detailed chapter on shape analysis and abstract interpretation.
There are short sections on literature surveys [14, 71], which categorize a variety of heap
analyses into storeless and store based models. Chakraborty [14] points out that heap models
cannot always be partitioned into storeless and store based only; some literature use hybrid
model.
May 2015

39

We have not come across a comprehensive survey which seeks a unifying theme among a
plethora of heap abstractions.

11

Conclusions

A simplistic compile time view of heap memory consists of an unbounded number of
unnamed locations relating to each other in a seemingly arbitrary manner. On the theoretical
side, this offers deep intellectual challenges for building suitable abstractions of heap for more
sophisticated compile time views of the heap memory. On the practical side, the quality of
the result of a heap analysis is largely decided by the heap abstraction used. It is not
surprising, therefore, that heap abstraction is a fundamental and vastly studied component of
heap analysis. What is surprising, however, is that a quest of a unifying theme in heap
abstractions has not received adequate attention which, in our opinion, it deserves.
This paper is an attempt to fill this void by separating the heap model as a representation
of heap memory, from a summarization technique used for bounding it. This separation has
allowed us to explore and compare a comprehensive list of algorithms used in the literature
making it accessible to a large community of researchers. We observe that the heap models
can be classified as storeless, store based, and hybrid. The summarization techniques use
k-limiting, allocation sites, patterns, variables, other generic instrumentation predicates, and
higher-order logics.
We have also studied the design choices in heap abstractions by comparing and
contrasting various techniques used in literature with respect to client requirements like
efficiency, precision, expressiveness, automatability, dimensions of the underlying analysis,
and user program properties. We hope that these comparisons can be helpful for a client to
decide which abstraction to use for designing a heap analysis. It is also expected to pave way
for creating new abstractions by mix-and-match of models and summarization techniques.
We observe in passing that, as program analysts, we still face the challenge of creating
summarizations that are efficient, scale to large programs, and yield results that are precise
enough to be practically useful.

Acknowledgements
An invigorating discussion in the Dagstuhl Seminar on Pointer Analysis [55] sowed the seeds
of this survey paper. We would like to thank Amitabha Sanyal, Supratik Chakraborty, and
Alan Mycroft for their comments on this paper as also for enlightening discussions related to
heap analysis from time to time. Anders Møller helped us in improving the description of
Pointer Assertion Logic Engine. Rohan Padhye, Alefiya Lightwala, and Prakash Agrawal gave
valuable feedback on the paper, helped in rewording some text, and pointed out some errors
in the examples. We would also like to thank the anonymous reviewers for their rigorous and
extensive reviews and thought-provoking questions and suggestions.
Vini Kanvar is partially supported by TCS Fellowship.

References
[1] Gilad Arnold, Roman Manevich, Mooly Sagiv, and Ran Shaham. Combining shape
analyses by intersecting abstractions. In Proceedings of the 7th International Conference
on Verification, Model Checking, and Abstract Interpretation, VMCAI’06, pages 33–48.
Springer-Verlag, 2006.
40

Heap Abstractions

REFERENCES

[2] Rahul Asati, Amitabha Sanyal, Amey Karkare, and Alan Mycroft. Liveness-based garbage
collection. In Proceedings of the 23rd International Conference on Compiler Construction,
CC’14. Springer-Verlag, 2014.
[3] Uwe Aßmann and Markus Weinhardt. Interprocedural heap analysis for parallelizing
imperative programs. In Proceedings of Programming Models for Massively Parallel
Computers, pages 74–82. IEEE Computer Society, September 1993.
[4] Gogul Balakrishnan and Thomas Reps. Recency-abstraction for heap-allocated storage.
In Proceedings of the 13th International Conference on Static Analysis, SAS’06, pages
221–239. Springer-Verlag, 2006.
[5] Barnali Basak, Sandeep Dasgupta, and Amey Karkare. Heap dependence analysis for
sequential programs. In PARCO, pages 99–106, 2011.
[6] Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. Thresher: Precise
refutations for heap reachability. In Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation, PLDI ’13, pages 275–286. ACM,
2013.
[7] Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, and Tomáš
Vojnar. Programs with lists are counter automata. In Proceedings of the 18th International
Conference on Computer Aided Verification, CAV’06, pages 517–531. Springer-Verlag,
2006.
[8] Marius Bozga, Radu Iosif, and Yassine Lakhnech. On logics of aliasing. In SAS, pages
344–360, 2004.
[9] Marius Bozga, Radu Iosif, and Yassine Laknech. Storeless semantics and alias logic.
SIGPLAN Not., 38(10):55–65, June 2003.
[10] Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang.
Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26:1–26:66,
December 2011.
[11] Cristiano Calcagno, Hongseok Yang, and Peter W. O’Hearn. Computability and
complexity results for a spatial assertion language for data structures. In Proceedings
of the 21st Conference on Foundations of Software Technology and Theoretical Computer
Science, FST TCS ’01, pages 108–119, London, UK, UK, 2001. Springer-Verlag.
[12] R. Castillo, A. Tineo, F. Corbera, A. Navarro, R. Asenjo, and E. L. Zapata. Towards a
versatile pointer analysis framework. In Proceedings of the 12th International Conference
on Parallel Processing, Euro-Par’06, pages 323–333. Springer-Verlag, 2006.
[13] Venkatesan T. Chakaravarthy. New results on the computability and complexity of points–
to analysis. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL ’03, pages 115–125. ACM, 2003.
[14] Supratik Chakraborty. Reasoning about Heap Manipulating Programs using Automata
Techniques. In Deepak D’Souza and Priti Shankar, editors, Modern Applications of
Automata Theory. IISc-World Scientific Review Volume, May 2012.
[15] David R. Chase, Mark Wegman, and F. Kenneth Zadeck. Analysis of pointers and
structures. In Proceedings of the ACM SIGPLAN 1990 Conference on Programming
Language Design and Implementation, PLDI ’90, pages 296–310. ACM, 1990.
May 2015

41

REFERENCES

[16] Arnab De and Deepak D’Souza. Scalable flow-sensitive pointer analysis for java with
strong updates. In Proceedings of the 26th European Conference on Object-Oriented
Programming, ECOOP’12, pages 665–687. Springer-Verlag, 2012.
[17] Alain Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In
Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design
and Implementation, PLDI ’94, pages 230–241. ACM, 1994.
[18] Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. A local shape analysis based
on separation logic. In Proceedings of the 12th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, TACAS’06, pages 287–302,
Berlin, Heidelberg, 2006. Springer-Verlag.
[19] Amer Diwan, J. Eliot B. Moss, and Kathryn S. McKinley. Simple and effective analysis of
statically-typed object-oriented programs. In Proceedings of the 11th ACM SIGPLAN
Conference on Object-oriented Programming, Systems, Languages, and Applications,
OOPSLA ’96, pages 292–305, New York, NY, USA, 1996. ACM.
[20] Nurit Dor, Michael Rodeh, and Mooly Sagiv. Detecting memory errors via static pointer
analysis (preliminary experience). In Proceedings of the 1998 ACM SIGPLAN-SIGSOFT
Workshop on Program Analysis for Software Tools and Engineering, PASTE ’98, pages
27–34. ACM, 1998.
[21] Stephen J. Fink, Kathleen Knobe, and Vivek Sarkar. Unified analysis of array and object
references in strongly typed languages. In Proceedings of the 7th International Symposium
on Static Analysis, SAS ’00, pages 155–174, London, UK, UK, 2000. Springer-Verlag.
[22] Manuel Geffken, Hannes Saffrich, and Peter Thiemann. Precise interprocedural sideeffect analysis. In Theoretical Aspects of Computing - ICTAC 2014 - 11th International
Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings, pages 188–205,
2014.
[23] Rakesh Ghiya. Putting Pointer Analysis to Work.
Montreal, 1998.

PhD thesis, McGill University,

[24] Rakesh Ghiya and Laurie J. Hendren. Is it a tree, a dag, or a cyclic graph? a shape
analysis for heap-directed pointers in C. In Proceedings of the 23rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’96, pages 1–15.
ACM, 1996.
[25] Rakesh Ghiya and Laurie J. Hendren. Putting pointer analysis to work. In Proceedings of
the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’98, pages 121–133. ACM, 1998.
[26] Alexey Gotsman, Josh Berdine, and Byron Cook. Interprocedural shape analysis with
separated heap abstractions. In Proceedings of the 13th International Conference on Static
Analysis, SAS’06, pages 240–260. Springer-Verlag, 2006.
[27] Samuel Z. Guyer and Calvin Lin. Client-driven pointer analysis. In Proceedings of the
10th International Conference on Static Analysis, SAS’03, pages 214–236. Springer-Verlag,
2003.
[28] L. Hendren, C. Donawa, M. Emami, G. Gao, Justiani, and B. Sridharan. Designing
the mccat compiler based on a family of structured intermediate representations. In
42

Heap Abstractions

REFERENCES

Utpal Banerjee, David Gelernter, Alex Nicolau, and David Padua, editors, Languages and
Compilers for Parallel Computing, volume 757 of Lecture Notes in Computer Science,
pages 406–420. Springer Berlin Heidelberg, 1993.
[29] L. J. Hendren and A. Nicolau. Parallelizing programs with recursive data structures.
IEEE Trans. Parallel Distrib. Syst., 1(1):35–47, January 1990.
[30] Laurie J. Hendren. Parallelizing Programs with Recursive Data Structures. PhD thesis,
Cornell University, January 1990.
[31] Laurie J. Hendren and Alexandru Nicolau. Intererence analysis tools for parallelizing
programs with recursive data structures. In Proceedings of the 3rd International
Conference on Supercomputing, ICS ’89, pages 205–214. ACM, 1989.
[32] Michael Hind. Pointer analysis: Haven’t we solved this problem yet? In Proceedings of
the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools
and Engineering, PASTE ’01, pages 54–61. ACM, 2001.
[33] Michael Hind and Anthony Pioli. Which pointer analysis should i use? SIGSOFT Softw.
Eng. Notes, 25(5):113–123, August 2000.
[34] C. A. R. Hoare. An axiomatic basis for computer programming.
12(10):576–580, October 1969.

Commun. ACM,

[35] Susan Horwitz. Precise flow-insensitive may-alias analysis is np-hard.
Program. Lang. Syst., 19(1):1–6, January 1997.

ACM Trans.

[36] David Hovemeyer, Jaime Spacco, and William Pugh. Evaluating and tuning a static
analysis to find null pointer bugs. In Proceedings of the 6th ACM SIGPLAN-SIGSOFT
Workshop on Program Analysis for Software Tools and Engineering, PASTE ’05, pages
13–19. ACM, 2005.
[37] Katsuro Inoue, Hiroyuki Seki, and Hikaru Yagi. Analysis of functional programs to detect
run-time garbage cells. ACM Trans. Program. Lang. Syst., 10(4):555–578, October 1988.
[38] Jakob L. Jensen, Michael E. Jørgensen, Michael I. Schwartzbach, and Nils Klarlund.
Automatic verification of pointer programs using monadic second-order logic. In
Proceedings of the ACM SIGPLAN 1997 Conference on Programming Language Design
and Implementation, PLDI ’97, pages 226–234. ACM, 1997.
[39] Neil D. Jones and Steven S. Muchnick. Flow analysis and optimization of lisp-like
structures. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles
of Programming Languages, POPL ’79, pages 244–256. ACM, 1979.
[40] H. B. M. Jonkers. Abstract storage structures. In De Bakker and Van Vliet, editors,
Algorithmic Languages, pages 321–343. IFIP, 1981.
[41] Uday P. Khedker. The approximations vs. abstractions dilemma in pointer analysis. In
Ondřej Lhoták, Yannis Smaragdakis, and Manu Sridharan, editors, Pointer Analysis,
volume 3 of Dagstuhl Reports, pages 91–113. Schloss Dagstuhl – Leibniz-Zentrum für
Informatik, Dagstuhl Publishing, April 2013.
[42] Uday P. Khedker, Alan Mycroft, and Prashant Singh Rawat. Liveness-based pointer
analysis. In Proceedings of the 19th International Conference on Static Analysis, SAS’12,
pages 265–282. Springer-Verlag, 2012.
May 2015

43

REFERENCES

[43] Uday P. Khedker, Amitabha Sanyal, and Amey Karkare. Heap reference analysis using
access graphs. ACM Trans. Program. Lang. Syst., 30(1), November 2007.
[44] Raghavan Komondoor. Precise slicing in imperative programs via term-rewriting and
abstract interpretation. In SAS, pages 259–282, 2013.
[45] Thomas Kotzmann and Hanspeter Mössenböck. Escape analysis in the context of dynamic
compilation and deoptimization. In Proceedings of the 1st ACM/USENIX International
Conference on Virtual Execution Environments, VEE ’05, pages 111–120. ACM, 2005.
[46] Viktor Kuncak, Patrick Lam, Karen Zee, and Martin C. Rinard. Modular pluggable
analyses for data structure consistency. IEEE Trans. Softw. Eng., 32(12):988–1005,
December 2006.
[47] Patrick Lam, Viktor Kuncak, and Martin Rinard. Generalized typestate checking
for data structure consistency. In Proceedings of the 6th International Conference on
Verification, Model Checking, and Abstract Interpretation, VMCAI’05, pages 430–447,
Berlin, Heidelberg, 2005. Springer-Verlag.
[48] Patrick Lam, Viktor Kuncak, and Martin Rinard. Hob: A tool for verifying data
structure consistency. In Proceedings of the 14th International Conference on Compiler
Construction, CC’05, pages 237–241, Berlin, Heidelberg, 2005. Springer-Verlag.
[49] William Landi and Barbara G. Ryder. A safe approximate algorithm for interprocedural
aliasing. In Proceedings of the ACM SIGPLAN 1992 Conference on Programming
Language Design and Implementation, PLDI ’92, pages 235–248. ACM, 1992.
[50] J. R. Larus and P. N. Hilfinger. Detecting conflicts between structure accesses. In
Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design
and Implementation, PLDI ’88, pages 24–31. ACM, 1988.
[51] Chris Lattner and Vikram Adve. Data structure analysis: A fast and scalable contextsensitive heap analysis. Technical report, University of Illinois at Urbana Champaign,
2003.
[52] Chris Lattner, Andrew Lenharth, and Vikram Adve. Making context-sensitive points-to
analysis with heap cloning practical for the real world. In Proceedings of the 2007 ACM
SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07,
pages 278–289, New York, NY, USA, 2007. ACM.
[53] Tal Lev-Ami, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm. Putting static analysis
to work for verification: A case study. In Proceedings of the 2000 ACM SIGSOFT
International Symposium on Software Testing and Analysis, ISSTA ’00, pages 26–38.
ACM, 2000.
[54] Ondřej Lhoták and Kwok-Chiang Andrew Chung. Points-to analysis with efficient strong
updates. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’11, pages 3–16. ACM, 2011.
[55] Ondřej Lhotak, Yannis Smaragdakis, and Manu Sridharan. Pointer Analysis (Dagstuhl
Seminar 13162). Dagstuhl Reports, 3(4):91–113, 2013.
[56] Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson
Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and
Dimitrios Vardoulakis. In defense of soundiness: A manifesto. Commun. ACM, 58(2):44–
46, January 2015.
44

Heap Abstractions

REFERENCES

[57] Ravichandhran Madhavan and Raghavan Komondoor. Null dereference verification
via over-approximated weakest pre-conditions analysis. In Proceedings of the 2011
ACM International Conference on Object Oriented Programming Systems Languages and
Applications, OOPSLA ’11, pages 1033–1052. ACM, 2011.
[58] Ravichandhran Madhavan, Ganesan Ramalingam, and Kapil Vaswani. Purity analysis: An
abstract interpretation formulation. In Proceedings of the 18th International Conference
on Static Analysis, SAS’11, pages 7–24, Berlin, Heidelberg, 2011. Springer-Verlag.
[59] Mark Marron, Cesar Sanchez, Zhendong Su, and Manuel Fahndrich. Abstracting runtime
heaps for program understanding. IEEE Trans. Softw. Eng., 39(6):774–786, June 2013.
[60] Ivan Matosevic and Tarek S. Abdelrahman. Efficient bottom-up heap analysis for symbolic
path-based data access summaries. In Proceedings of the Tenth International Symposium
on Code Generation and Optimization, CGO ’12, pages 252–263. ACM, 2012.
[61] Ana Milanova, Atanas Rountev, and Barbara G. Ryder. Parameterized object sensitivity
for points-to and side-effect analyses for java. SIGSOFT Softw. Eng. Notes, 27(4):1–11,
July 2002.
[62] Anders Møller. Mona project home page, 2014.
[63] Anders Møller and Michael I. Schwartzbach. The pointer assertion logic engine. In
Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design
and Implementation, PLDI ’01, pages 221–231. ACM, 2001.
[64] Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program Analysis.
Springer-Verlag New York, Inc., 1999.
[65] Erik M. Nystrom, Hong-Seok Kim, and Wen-mei W. Hwu. Importance of heap
specialization in pointer analysis. In Proceedings of the 5th ACM SIGPLAN-SIGSOFT
Workshop on Program Analysis for Software Tools and Engineering, PASTE ’04, pages
43–48, New York, NY, USA, 2004. ACM.
[66] Rohan Padhye and Uday P. Khedker. Interprocedural data flow analysis in soot using
value contexts. In Proceedings of the 2Nd ACM SIGPLAN International Workshop on
State Of the Art in Java Program Analysis, SOAP ’13, pages 31–36. ACM, 2013.
[67] G. Ramalingam. The undecidability of aliasing. ACM Trans. Program. Lang. Syst.,
16(5):1467–1471, September 1994.
[68] Thomas Reps. Program analysis via graph reachability. In Proceedings of the 1997
International Symposium on Logic Programming, ILPS ’97, pages 5–19. MIT Press, 1997.
[69] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In
Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS
’02, pages 55–74. IEEE Computer Society, 2002.
[70] H. G. Rice. Classes of recursively enumerable sets and their decision problems.
Transactions of the American Mathematical Society, 74(2):pp. 358–366, 1953.
[71] Noam Rinetzky. Interprocedural and Modular Local Heap Shape Analysis. PhD thesis, Tel
Aviv University, June 2008.
May 2015

45

REFERENCES

[72] Noam Rinetzky, Jörg Bauer, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm. A
semantics for procedure local heaps and its abstractions. In Proceedings of the 32Nd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
’05, pages 296–309. ACM, 2005.
[73] Atanas Rountev, Barbara G. Ryder, and William Landi. Data-flow analysis of program
fragments. In Proceedings of the 7th European Software Engineering Conference Held
Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software
Engineering, ESEC/FSE-7, pages 235–252. Springer-Verlag, 1999.
[74] Barbara G. Ryder. Dimensions of precision in reference analysis of object-oriented
programming languages. In Proceedings of the 12th International Conference on Compiler
Construction, CC’03, pages 126–137, Berlin, Heidelberg, 2003. Springer-Verlag.
[75] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in
languages with destructive updating. In Proceedings of the 23rd ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL ’96, pages 16–31. ACM, 1996.
[76] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems
in languages with destructive updating. ACM Trans. Program. Lang. Syst., 20(1):1–50,
January 1998.
[77] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via
3-valued logic. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’99, pages 105–118. ACM, 1999.
[78] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Shape analysis and applications. In
Y. N. Srikant and P. Shankar, editors, Compiler Design Handbook: Optimizations and
Machine Code Generation, chapter 12. CRC Press, Inc, 2007.
[79] Damien Sereni. Termination analysis of higher-order functional programs. PhD thesis,
Oxford University, 2006.
[80] Ran Shaham, Eran Yahav, Elliot K. Kolodner, and Mooly Sagiv. Establishing local
temporal heap safety properties with applications to compile-time memory management.
In Proceedings of the 10th International Conference on Static Analysis, SAS’03, pages
483–503. Springer-Verlag, 2003.
[81] II Marc Shapiro and Susan Horwitz. The effects of the precision of pointer analysis. In
Proceedings of the 4th International Symposium on Static Analysis, SAS ’97, pages 16–34.
Springer-Verlag, 1997.
[82] Elodie-Jane Sims.
University, 2007.

Pointer analysis and separation logic.

PhD thesis, Kansas State

[83] Yannis Smaragdakis and George Balatsouras. Pointer analysis. Foundations and Trends
in Programming Languages, 2(1), 2015.
[84] Yannis Smaragdakis, Martin Bravenboer, and Ondřej Lhoták. Pick your contexts well:
Understanding object-sensitivity. In Proceedings of the 38th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’11, pages 17–30.
ACM, 2011.
46

Heap Abstractions

[85] Manu Sridharan, Satish Chandra, Julian Dolby, Stephen J. Fink, and Eran Yahav.
Aliasing in object-oriented programming. In Dave Clarke, James Noble, and Tobias
Wrigstad, editors, Alias Analysis for Object-oriented Programs, pages 196–232. SpringerVerlag, 2013.
[86] Bjarne Steensgaard. Points-to analysis in almost linear time. In Proceedings of the 23rd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
’96, pages 32–41, New York, NY, USA, 1996. ACM.
[87] Vijay Sundaresan, Laurie Hendren, Chrislain Razafimahefa, Raja Vallée-Rai, Patrick Lam,
Etienne Gagnon, and Charles Godin. Practical virtual method call resolution for java.
In Proceedings of the 15th ACM SIGPLAN Conference on Object-oriented Programming,
Systems, Languages, and Applications, OOPSLA ’00, pages 264–280, New York, NY, USA,
2000. ACM.
[88] Frédéric Vivien and Martin Rinard. Incrementalized pointer and escape analysis. In
Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design
and Implementation, PLDI ’01, pages 35–46. ACM, 2001.
[89] John Whaley and Monica S. Lam. Cloning-based context-sensitive pointer alias analysis
using binary decision diagrams. In Proceedings of the ACM SIGPLAN 2004 Conference
on Programming Language Design and Implementation, PLDI ’04, pages 131–144. ACM,
2004.
[90] Reinhard Wilhelm, Shmuel Sagiv, and Thomas W. Reps. Shape analysis. In Proceedings of
the 9th International Conference on Compiler Construction, CC ’00, pages 1–17. SpringerVerlag, 2000.
[91] Guoqing Xu and Atanas Rountev. Merging equivalent contexts for scalable heap-cloningbased context-sensitive points-to analysis. In Proceedings of the 2008 International
Symposium on Software Testing and Analysis, ISSTA ’08, pages 225–236, New York, NY,
USA, 2008. ACM.

A

Heap and Stack Memory in C/C++ and Java

In this section, we briefly compare the programming constructs related to pointer variables in
C/C++ and Java programs.
Referencing variables on stack and heap. In C/C++, both stack and heap allow pointer
variables. Java does not allow stack directed pointers. C/C++ allows pointers to variables
on the stack through the use of addressof operator &; Java does not have this operator. Both
C/C++ and Java allow pointers/references to objects on the heap using malloc function (in
C/C++) and new operator (in C++ and Java).
Dereferencing pointers. Every variable on the stack, whether it contains a reference or a
value, always has a name because all the objects allocated on the stack have compile time
names associated with them. Heap allocated data items do not possess names and are all
anonymous. The only way to access heap items is using pointer dereferences. C/C++ has
explicit pointers. Pointer variables in C/C++ are dereferenced using star operator (∗), for
example, y := ∗x. Fields of a pointer to an aggregate data type (struct, union, or class) can
be accessed using star operator (∗) and dot operator (.), for example, (∗x).f, or using arrow
operator (->), for example, x->f; both are equivalent pointer dereferences of the member field
f of pointer variable x. In Java, fields are dereferenced using the dot operator (.), for example,
x.f.
May 2015

47

C/C++
Heap

C/C++
Stack

A

lp

w

tr

rp

tr

lp

lp
B

tr

x
rp

C

y

D

z

Java Stack

tr

rp

tr

tr

Java Heap

Figure 20. C/C++ memory framework modeled as a Java memory framework.

Analysis of scalar and aggregate pointers. In Java, a pointer variable cannot point to an
object of scalar data type such as integer or floating point number; pointer variables point to an
object of only aggregate data types in Java such as structures, classes etc. However, C/C++
allows pointers to both scalars and aggregate structures. In C++, pointer analysis of scalar
variables is comparatively straightforward (due to type restrictions) as compared to the pointer
analysis of aggregate variables. For example, a program statement x := ∗x is syntactically
invalid—the scalar pointer x cannot advance to a location of a different data type. On the
other hand an aggregate pointer can be advanced subject to its type compatibility making it
difficult to find properties of such pointers. For example, program statement x := x->f in a loop
allows the aggregate pointer x to point to any location after x through field f. Further, cycles
in recursive data structures, cause infinite number of paths that refer to the same memory
location. This makes the analysis of an aggregate pointer challenging over a scalar pointer.
Mapping C/C++ memory to the Java memory. As explained before, C/C++ heap and
stack pointers can point to locations on both stack and heap. On the other hand, Java
stack pointers can point only to Java heap locations. In spite of this difference in memory
modeling, stack and heap memory in C/C++ can be modeled like a Java memory. To achieve
this, C/C++ memory is viewed as consisting of two partitions of the memory—addresses of
variables and the rest of the memory (stack and heap together) [43]. Here, the first partition
of the C/C++ memory (i.e. the addresses of variables) works like the Java stack. The second
partition of the C/C++ memory consisting of the rest of the memory (stack and heap together)
works like the Java heap.
Figure 20 illustrates a C/C++ memory snapshot, which has been modeled as Java memory
(in dotted lines). Pointer variables w, x, y, and z are on the C/C++ stack and pointer variables
A, B, C, and D are on the Java stack. C/C++ pointers point to stack variables x and z in the
figure. The stack and heap of C/C++ are represented as the Java heap. Java stack is the set
of addresses of C/C++ locations (viz. w, x, y, and z) stored in A, B, C, and D, respectively.
To overcome the difference of pointer dereferences (∗) and addressof (&) operator in C/C++
which are absent in Java, Khedker et al. [43] model these two C/C++ constructs as follows:
48

Heap Abstractions

• Pointer dereference (∗) is considered as a field dereference deref, which has not been used
elsewhere in the program. For example [43], (∗x).f in C/C++ is viewed as x.deref.f in
Java.
• The addresses of C/C++ variables are represented by the Java stack (as shown in
figure 20, where A denotes &w, B denotes &x, C denotes &y, and D denotes &z). For
example [43], y.f in Java is modeled as &y.deref.f in C/C++.

May 2015

49

