JAIST Repository
https://dspace.jaist.ac.jp/

Title

Stacking‑based context‑sensitive points‑toanalysis for java

Author(s)Li, Xin; Ogawa, Mizuhito

Citation

Lecture Notes in Computer Science, 6405/2011:
133‑149

Issue Date

2009/10/20

Type

Journal Article

Text version

author

URL

http://hdl.handle.net/10119/9784

RightsThis is the author‑created version of Springer,
Xin Li, Mizuhito Ogawa, Lecture Notes in Computer
Science, 6405/2011, 2009, 133‑149. The original
publication is available at www.springerlink.com,
http://dx.doi.org/10.1007/978‑3‑642‑19237‑1̲14

Description

Hardware and Software: Verification and Testing,
5th International Haifa Verification Conference,
HVC 2009, Haifa, Israel, October 19‑22, 2009,
Revised Selected Papers

Japan Advanced Institute of Science and Technology

Stacking-based Context-Sensitive Points-to
Analysis for Java
Xin Li and Mizuhito Ogawa
School of Information Science,
Japan Advanced Institute of Science and Technology, Nomi, Japan

Abstract. Points-to analysis for Java infers heap objects that a reference variable can point to. Existing practiced context-sensitive points-to
analyses are cloning-based, with an inherent limit to handle recursive
procedure calls and being hard to scale under deep cloning. This paper
presents a stacking-based context-sensitive points-to analysis for Java, byderiving the analysis as weighted pushdown model checking problems. To
generate a tractable model for model checking, instead of passing global
variables as parameters along procedure calls and returns, we model theheap memory with a global data structure that stores and loads global
references with synchronized points-to information on-demand. To accelerate the analysis, we propose a two-staged iterative procedure thatcombines local exploration for lightening most of iterations and global
update for guaranteeing soundness. In particular, summary transition
rules that carry cached data flows are carefully introduced to trigger
each local exploration, which boosts the convergence with retaining the
precision. Empirical studies show that, our analysis scales well to Javabenchmarks of significant size, and achieved in average 2.5X speedup in
the two-staged analysis framework.

1

Introduction

The notion of context-sensitivity bears a similarity to inline expansion, as if
method calls are replaced with bodies of the callees. As such, the typical cloningbased program analysis [17] creates a separate copy of a method call within abounded call depth or with collapsing recursive procedure calls. The cloningbased approach has an inherit limit to handle (recursive) procedure calls. An
alternative to obtaining context-sensitivity in terms of valid call paths is to model
the program’s call stack with the pushdown stack. Since the stack can growunboundedly, no restriction is placed on the call depth and recursions. By valid,
it means a procedure call always returns to the most recent call site.
Points-to analysis (PTA) infers the set of heap objects that a reference variable may point to. PTA for Java is featured for being interdependent of callgraph construction, due to dynamic language features like late binding. The longstanding challenge is to design a scalable yet precise PTA. Context-sensitivity isshown to be crucial to the precision of PTA for Java. To the best of our knowledge, existing practiced PTA for Java are all cloning-based [17, 13]. However,empirical study recently shows that, more than one thousand of methods are
typically contained within recursive procedure calls in practice [18], and approximating recursions potentially threatens the analysis precision [6].
This paper presents a stacking-based context-sensitive PTA for Java, by encoding the analysis as model checking problems on WPDSs [11]. Our analysis
is context-sensitive, field-sensitive, and flow-insensitive, with the call graph constructed on-the-fly. In contrast to the cloning-based approach, there is a single
copy for each procedure in the analysis, while calling contexts are entirely characterized as (regular) configurations over the pushdown stack. Our first step toscalability is that, instead of passing global variables explicitly as parameters
along procedure calls and returns (that is hopeless to scale from our empirical
study) [10], we model the heap memory with a global data structure during theanalysis, which loads intermediate points-to information of global references, andstores cached values to global references on-demand when they are referred toinside procedures. This encoding dramatically reduces the number of pushdown
transitions and generates a tractable model for model checking.
To further accelerate the analysis, we propose a two-staged iterative procedure, denoted by (LE ◦ GU)∗ as opposed to the traditional iterative procedure
denoted by GU∗ , which combines local exploration (LE) for lightening most of
iterative cycles and global update (GU) for guaranteeing the completeness. Our
insight is, to localize most of iterative cycles on the partial program models in
LEs, and perform GUs on the entire program model as few times as possible. In
particular, summary transition rules that carry previously computed data flows
are introduced to effectively trigger each LE and boost the convergence. In effect, the computation of data flows to some program point in the partial program
model is divided into independent phases via frontiers: the computation of dataflows from the program entry to frontiers and the computation of data flows
from frontiers to the concerned program point. By carefully adding summarytransition rules to frontiers, the analysis by (LE ◦ GU)∗ retains the same precision
as the analysis by GU∗ . Empirical studies show that, a substantial speedup inpractice can be achieved by the two-staged analysis.
This paper primarily makes the following contributions.
– We present a scalable stacking-based context-sensitive PTA for Java bymodel checking WPDSs, with no restriction on (recursive) procedure calls.
– We propose a two-staged iteration procedure, supported by carefully introducing summary transition rules, to effectively accelerate the analysis.
– We implemented the analysis algorithms as a tool named Japot. Empirical
study shows that Japot scales well to Java benchmarks of significant size.
The rest of the paper is organized as follows. Section 2 briefly reviews weighted
pushdown model checking. Section 3 presents Java semantics and abstractions.
Detection of points-to information by model checking is in Section 4. Section
5 presents a two-staged iteration procedure. Section 6 gives experiments andSection 7 discusses related work. Section 8 concludes the paper.

2

Weighted Pushdown Model Checking

Definition 1. Define a pushdown system P = (Q, Γ, ∆, q0 , ω0 ), where Q isa finite set of states called control locations, Γ is a finite stack alphabet, and∆ ⊆ Q × Γ × Q × Γ ∗ is a finite set of transition rules. q0 ∈ Q and ω0 ∈ Γ ∗are the initial control location and stack contents respectively. A transition rule(p, γ, q, ω) ∈ ∆ is denoted by hp, γi ,→ hq, ωi. A configuration of P is a pairhq, ωi for q ∈ Q and ω ∈ Γ ∗ . ∆ defines a transition relation ⇒ on configurations
such that hp, γω 0 i ⇒ hq, ωω 0 ifor each ω 0 ∈ Γ ∗ if hp, γi ,→ hq, ωi.
Definition 2. S = (D, ⊕, ⊗, 0, 1) with 0, 1 ∈ D is a bounded idempotent
semiring if
1. (D, ⊕) is a commutative monoid with 0 as its unit element, and ⊕ is idempotent, i.e., a ⊕ a = a for a ∈ D;
2. (D, ⊗) is a monoid with 1 as the unit element;
3. ⊗ distributes over ⊕;4. ∀a ∈ D, a ⊗ 0 = 0 ⊗ a = 0;
5. The partial ordering v is defined on D such that ∀a, b ∈ D, a v b iff a⊕b = a.
By Def. 2, it is guaranteed there are no infinite descending chains in D wrt
v, and 0 is the greatest element.
Definition 3. Define a weighted pushdown system (WPDS) W = (P, S, f),where P = (Q, Γ, ∆, q0 , ω0 ) is a pushdown system, S = (D, ⊕, ⊗, 0, 1) is abounded idempotent semiring, and f : ∆ → D is a weight assignment function.
When encoding the program as a WPDS, the bounded idempotent semiringmodels program data flows. A weight element encodes traditional program transformers; f ⊕ g combines data flows at the meet of control flows; f ⊗ g composessequential control flows; 1 is identity function, and 0 implies program errors.
Definition 4. Given a weighted pushdown system W = (P, S, f), where P =(Q, Γ, ∆, q0 , w0 ). Assume σ = [r0 , ..., rk ] for ri ∈ ∆(0 ≤ i ≤ k) to be a sequenceof pushdown transition rules, and v(σ) = f (r0 )⊗...⊗f (rk ). Let path(c,c0 ) be theset of all transition sequences that transform configurations from c into c0 . Givensets of regular configurations C, C 0 ⊆ Q × Γ ∗ , for each configuration c ∈ Q × Γ ∗ ,– L
the Generalized Pushdown Successor (GPS) problem is to find gps(c) ={v(σ) | σ ∈ path(c0 , c), c0 ∈ C}.
– L
the Generalized Pushdown Predecessor (GPP) problem is to find gpp(c) ={v(σ) | σ ∈ path(c, c0 ), c0 ∈ C 0 }.
– L
The Meet-Over-All-Valid-Path (MOVP) problem is to find MOVP(C, C 0 , W ) ={v(σ) | σ ∈ path(c, c0 ), c ∈ C, c0 ∈ C 0 }.
Given p ∈ Q, γ ∈ Γ and c ∈ Q × Γ ∗ , and let conf(p, γ) = {hp, γωi | ω ∈ Γ ∗ },[ hp, γi, W ) = MOVP({c}, conf(p, γ), W ).
further define MOVP(c,Efficient algorithms for solving the GPS and GPP problems are proposed
based on the fact that a regular set of configurations is closed under forward andbackward reachability [11]. Then, MOVP is solved based on the results of either
GPS or GPP. There are two off-the-shelf implementations of weighted pushdown
model checking, Weighted PDS Library 1 and WPDS++ [3, 4]. We exploit theformer as the back-end analysis engine.
Example 1. As shown in Table 1, a context-sensitive PTA is able to distinguishthat, x1 and x2 points to objects created at line 2 and 3, respectively. In contrast,
an imprecise analysis may mix them.
Table 1. A Java Code Snippet
0. public class Main {1. public static void main(String[] args){
2.
Object y1 = new String();
3.
Object y2 = new Object();
4.
Object x1 = f1 (y1 );5.
Object x2 = f1 (y2 );6.
System.out.println(x1 .equals(x2 ));7. }8. public static Object f1 (Object a){9.
return f2 (a);10. }11. public static Object f2 (Object b){
12.
return b;
13. }
14. }

3

Semantics and Abstraction

3.1

Java Semantics on the Heap and Call Stack

Definition 5. A method signature consists of method name, parameter types,
and return type. We denote by C the set of classes, and denote by Ψ the set of
method signatures. A method is identified by a pair of its enclosing class C ∈ C
and its method signature ψ ∈ Ψ , denoted by C.ψ. The set of method identifiersis denoted by C.Ψ ⊆ C × Ψ . We denote by Θ the class environment, including allclasses, type representations of classes, and the type hierarchy.
In Java, a heap object is a dynamically created instance of either a class oran array. Reference variables are typically local variables, method parameters,array references, and static or instance fields that hold reference types. Fields
and array references can be regarded as global variables. A local variable v fromits enclosing method C.ψ is denoted by indexing with the scope as v C.ψ . If C.ψ
is clear from the context, we often simply write v.
Definition 6. The set of references is denote by V, and the set of heap objects
is denoted by O. An abstract heap environment henv is a mapping, denotedby 7→, from V to O. The set of abstract heap environments is denoted by Λ,on which the update operation
is defined such that for r, r0 ∈ V, o ∈ O,00(henv [r 7→ o])r = o if r = r and (henv [r 7→ o])r0 = henv(r0 ) otherwise.
1

http://www.fmi.uni-stuttgart.de/szs/tools/wpds/

Definition 7. We denote by L the set of program line numbers and denote by S
the set of program statements. Let Stmt : L → S be the function that returns thestatement at a given line number. S ⊆ S denotes the set of statements that do
not contain explicit method invocations and operate on the heap memory, and by
SI ⊆ S denotes the set of statements that contains explicit method invocations.
Definition 8. Let Elem = L × (O ∪ {∗}) × C.Ψ . Let Π = Elem∗ .{⊥} be theset of calling histories over the call stack. Define push(stack, e) = e.stack forstack ∈ Π; and pop(e.stack) = stack, top(e.stack) = e for e ∈ Elem andstack ∈ Π; and pop(⊥) = top(⊥) = ⊥.
A call stack symbol hl, o, C.ψi ∈ Elem denotes the program execution point atline l of the instance method C.ψ that is invoked on the object o, and hl, ∗, C.ψi ∈Elem represents an execution point inside a static method C.ψ.
Table 2. Transition Rules on the Heap and Call Stackstmt(l) from C.ψ
henv’
x = new T
henv
x=y
henv
x := (T)yhenv
x := @this : T
henv
x := @parameterk : T henv
henv
x = y[i]y[i] = xhenvx = y.fhenv
y.f = xhenv
return yhenv
z = r0 .m(r1 , ..., rn )henv

z = C 0 .m(r1 , ..., rn )stack’[x 7→ ν(henv)][x 7→ henv(y)]push(s, e) where[x 7→ henv(y)]s = pop(stack)[x 7→ henv(this)]e = hnext(l), o, C.ψi[x 7→ henv(argk )]o =0 ∗0 if C.ψ is static[x 7→ henv(y)[i]]o ∈ henv(thisC.ψ ) o.w.
[henv(y)[i] 7→ henv(x)][x 7→ henv(henv(y).f )][henv(y).f 7→ henv(x)][ret 7→ henv(y)]pop(stack)00[thisC .ψ 7→ henv(r0 )]push(s0 , e0 ) where
C 0 .ψ 0[arg1
7→ henv(r1 )] · · ·s0 = push(s, e)
C 0 .ψ 0
7→ henv(rn )][argn
s = pop(stack)00[z 7→ retC .ψ ]e = hnext(l), o, C.ψi00where ψ 0 ∈ Ψ is the method signature of m, e0 = hl0C .ψ , o0 , C 0 .ψ 0 i
0000
and C .ψ = resolve(TypeOf(o ), ψ , Θ)for o0 = henv(r0 ).
0.ψ 0henv [argC
7→ henv(r1 )] · · ·push(s, e0 ) where1
C 0 .ψ 0[arg1
7→ henv(r1 )]s = push(pop(stack), e)00[z 7→ retC .ψ ]e = hnext(l), o, C.ψi000where ψ ∈ Ψ is the method signature of m, e0 = hl0C .ψ , ∗, C 0 .ψ 0 i
0000
and C .ψ = resolve(C , ψ , Θ).

We use a transition system (states, sinit , →) to represent the operational
Java semantics on the heap and call stack, where states ⊆ L × Θ × Λ × Π isthe set of program states, each of which is a tuple of program locations, classenvironment, heap environments and calling histories, and sinit ∈ states is theinitial state; →⊆ states × states is the set of transition rules.

As far as single-threaded Java programs are concerned, the next program
location after each execution step at l (∈ L) is uniquely determined, and is denoted by next(l). As given in Table 2, for the program execution of the statement
stmt(l) at l ∈ L from the method C.ψ, the transition rule is hl, Θ, henv, stacki→ hnext(l), Θ, henv0 , stack0 i. Here, ν is a function that generates a fresh heap
object. this, argk and ret are fresh variables to denote the this reference of aclass instance, the k th method argument, and the return variable, respectively.
TypeOf : O → C is the function that returns the runtime type of a heap object.
resolve : C × Ψ × Θ → C.Ψ is the function implements how JVM resolves andthe method to be invoked at runtime according to its method signature and00possible enclosing class. l0C .ψ refers to the entry point of the method C 0 .ψ 0 .
3.2

Abstraction

We apply the following abstractions to abstract away various sources of infinities.
– A unique abstract heap object models concrete heap objects created at thesame allocation site (a.k.a., the context-insensitive heap abstraction). Thus,
the number of abstract heap objects are syntactically bounded to be finite.
An abstract heap object is a pair of its allocation site and runtime type.
– The indices of arrays are ignored, such that members of an array are notdistinguished. We denote by [[o]] the unique representative for all membersof the array instance o (∈ O). After abstracting the set of heap objects to be
finite, the nesting of array and field reference become finite correspondingly.
Definition 9. The set of abstract heap objects is Obj = (L ∪ { }) × C, whereis a fresh symbol for indicating nowhere. Let TypeOf : Obj → C be the function
returns the second projection of an abstract heap object.
Definition 10. Let RetPoint ⊆ L × C.Ψ be the set of return points for method
invocations. Define abstractions αt : Elem → { } × C.Ψ , αr : Elem → RetPoint,and αo : Elem → Obj × C.Ψ such that, for hl, o, C.ψi ∈ Elem,– αt (hl, o, C.ψi) = ( , C.ψ),– αr (hl, o, C.ψi) = (l, C.ψ), and– αo (hl, o, C.ψi) = (o, C.ψ).
αr and αo are extended to the call stack in an element-wise manner.
Definition 11. Let C = ({ } × (C.Ψ )).RetPoint∗ be the set of abstract calling
contexts. Define a calling context abstraction α : Π → C such that α(⊥) =  andα(e.stack) = αt (e).αr (stack) for e ∈ Elem, and stack ∈ Π.
By Def. 10, αt abstracts the topmost stack symbol for flow-insensitivity. αrabstracts the return points of method invocations, which results in calling contexts in terms of call site strings. Our choice of αr indicates, method invocations
to the same method from different places of the same caller is still distinguished.
An alternative of αr is αo , which abstracts calling contexts as sequences of heap
objects on which methods are invoked, also known as object-sensitivity [9].

Definition 12. We denote by Ref the set of abstract reference variables, andby cc(v) all possible abstract calling contexts for a reference variable v ∈ Ref.
Note that, cc(v) are exactly all possible calling contexts for the method whichv belongs to, and cc(v) is automatically computed as the set of reachable regularconfigurations during model checking (Section 4).
Definition 13. Let R : Ref×C → P(Obj) be the function that stores the pointsto relation, where P denotes the powerset operator. R ↓V : V × C → P(Obj) is
the restriction of R to V ⊆ Ref. Define  : R × R → R, such that for any
r ∈ Ref and cc ∈ C, (R1  R2 )(r, cc) = R1 (r, cc) \ R2 (r, cc).

4

Detecting Points-to Information by Model Checking

This section presents, given points-to information and a call graph, how to detect
new points-to information and enlarge a call graph in a context/field-sensitiveand flow-insensitive way.
Definition 14. G = (M, E) is a call graph of a program if M ⊆ C.Ψ and E ⊆M × L × M . An element in E is called a call edge.
We call P ⊆ C.Ψ a program coverage, and denote the program coverage
consisting of enclosing methods of program entries by P0 .
Definition 15. Let Henv, sp be fresh symbols. Define a weighted pointer assignment graph (WPAG) G = (N, L, , n0 ), where N ⊆ (Ref ∪ {Henv}) × (C.Ψ ∪RetPoint) is the set of nodes, L ⊆ {λx.{o} | o ∈ Obj} ∪ {λx.x} is the set oflabels, ⊆ N × L × N is the set of edges, and n0 = (Henv, sp) ∈ N is the root.
A WPAG G is a directed labeled graph to represent data flow of heap objects.
Henv and sp indicate the program environment that provides new abstract heap
objects and program inputs, and the dummy program entry, respectively. The
first projection of N represents abstract references, and the second projection
represents their program scopes. Edges of G are classified into inter-edges ( i ,defined in Table 3) and intra-edges ( c , r , t , defined in Table 4). An edge(v, m)(v 0 , m0 ) is denoted by((
if m = m0 ∈ C.Ψ
if m0 ∈ RetPointir
00
if m ∈ RetPointc if m 6= m and m, m ∈ C.Ψ
t
The procedure of finding new points-to information consists of the following
steps. Step 1 builds intra-edges of a WPAG G given R. Step 2 builds inter-edgesof G given E. During Step 2, the set of return points associated with each method
invocation is recorded as a mapping M : c → P(RetPoint). Initially, M is theconstant function to the empty set. Step 3 encodes G as a WPDS W and detects
b by model checking.
new points-to information, denoted by R,

Table 3. A[[ ]] : S → P(i)λx.{(l,T)}

A[[x = new T]] = {(Henv, C.ψ)(x, C.ψ)}i
A[[x = y]] = {(y, C.ψ) i (x, C.ψ)}A[[x := (T)y]] = {(y, C.ψ) i (x, C.ψ)}A[[x := @this : T]] = {(this, C.ψ) i (x, C.ψ)} ∪ Ae
λx.{( ,T)}

where Ae = {(Henv, C.ψ)(this, C.ψ)} if C.ψ ∈ P0 and Ae = ∅ otherwiseiA[[x := @parameterk : T]] = {(argk , C.ψ) i (x, C.ψ)} ∪ Ap
λx.{( ,T)}

where Ap = {(Henv, C.ψ)(argk , C.ψ)} if C.ψ ∈ P0 and Ap = ∅ otherwiseiA[[return x]] = {(x, C.ψ) i (ret, C.ψ)}A[[x = y[i]]] = {([[o]], C.ψ) i (x, C.ψ) | o ∈ R(y, cc(y))} ∪ Ag
A[[y[i] = x]] = {(x, C.ψ) i ([[o]], C.ψ) | o ∈ R(y, cc(y))} ∪ Ag
λx.s

where Ag = {(Henv, C.ψ) i ([[o]], C.ψ) | o ∈ R(y, cc(y)), s = R([[o]], cc([[o]]))}
A[[x = y.f ]] = {(o.f, C.ψ) i (x, C.ψ) | o ∈ R(y, cc(y))} ∪ Af
A[[y.f = x]] = {(x, C.ψ) i (o.f, C.ψ) | o ∈ R(y, cc(y))} ∪ Af
where Af = {(Henv, C.ψ)λx.si (o.f, C.ψ) | o ∈ R(y, cc(y)), s = R(o.f, cc(o.f ))}Step 1: Building Intra-procedural Data Flows
Table 3 gives rules that translate statements from S at line l(∈ L) of the method
C.ψ to intra-edges of G, denoted by A[[ ]] : S → P( i ). For simplicity, we omit
a weight associated to
if it is λx.x. Our modeling is featured as follows.
– In contrast to cloning-based approach, there is the unique abstract referenceof each local reference variable. Global references are cloned only for methods
inside which they are referred.
– Instead of passing global variables explicitly as parameters along procedure
calls and returns, the heap memory is modelled with the global data structure
R and provides global references with cached data flows (i.e., Ag , Af ) when
they are locally referred (only necessary for field read).
Step 2: Building Inter-procedural Data Flows
Table 4 gives rules that translate statements from SI that contains explicit
method invocations to inter-edges of G, denoted by A[[ ]] : SI → c ∪ r ∪ t ,where Ac denotes call edges, Ar denotes return edges, and At denotes data flows
from return points to the calling procedure. Note that, Henv as the program
environment is explicitly passed as a parameter among calls and returns. During generation of inter edges, the mapping M is updated with newly produced
return points. The translation rules for static method invocations can be definedsimilarly. Finally, new edges {n0(Henv, C.ψ) | n0 = (Henv, sp), C.ψ ∈ P0 }are added to G that lead from the dummy root node n0 to the program entries.
Step 3: Building the WPDS W from G and Model Checking
Definition 16. Let D1 = {λx.s | s ∈ P(Obj)} and D2 = {λx.x ∪ s | s ∈P(Obj)}. Define a bounded idempotent semiring S = (D, ⊕, ⊗, 0, 1), such that

Table 4. A[[ ]] : SI →

c ∪

r ∪

t

A[[z = r0 .f (r1 , ..., rn )]] = Ac ∪ Ar ∪ At
00
where Ac = {(r0 , C.ψ) c (thisC .ψ , C 0 .ψ 0 )} ∪ {(Henv, C.ψ) c (Henv, C 0 .ψ 0 )}00∪ ri ∈Ref {(ri , C.ψ) c (argi C .ψ , C 0 .ψ 0 )}0000
Ar = {(retC .ψ , C 0 .ψ 0 ) r (retC .ψ , rp)} ∪ {(Henv, C 0 .ψ 0 ) r (Henv, rp)}00
At = {(retC .ψ , rp) t (z, C.ψ)} ∪ {(Henv, rp) t (Henv, C.ψ)}ψ 0 is the method signature of the method f , and(C.ψ, l, C 0 .ψ 0 ) ∈ E, and rp = (l, C.ψ), andfor all r ∈ Ac , M(r) = M(r) ∪ {rp}S

– The weighted domain D = D1 ∪ D2 ∪ {0}, and 1 = λx.x;– d1 ⊗ d2 = d1 ⊕ d2 = λx. d1 (x) ∪ d2 (x) for d1 , d2 ∈ D \ {0}– d ⊗ 0 = 0 ⊗ d = 0 for d ∈ D;
It is easy to see that both the distributivity of ⊗ over ⊕ and the associativityof ⊗ hold. D1 consists of constant functions, and λx.s ∈ D1 is that a reference
points to the set of abstract heap objects s; and λx.x ∪ s ∈ D2 is that a reference
may keep unchanged along a path and be updated to point to s along another.
Given a WPAG G from Definition 15, a WPDS W = (P, S, f) with P =(Q, Γ, ∆, q0 , w0 ) is encoded G as follows,– The set of control locations Q is the first projection of N , i.e., Ref ∪ {Henv};– The stack alphabet Γ is the second projection of N , i.e., C.Ψ ∪ RetPoint;– S is from Definition 16;– q0 = Henv and w0 = sp;– For each edge r represented as (v1 , m1 )l(v2 , m2 ) such that f (r) = l and• hv1 , m1 i ,→ hv2 , m2 i if r ∈ i or t ;• hv1 , m1 i ,→ hv2 , m2 mr i for each mr ∈ M(
• hv1 , m1 i ,→ hv2 , i if r ∈ r .

c ) if r ∈c;Definition 17. Let W = (P, S, f) be a weighted pushdown system with P =b(Q, Γ, ∆, q0 , γ0 ). For any reference v ∈ Ref from the method C.ψ, R(v,cc(v)) =[MOVP(c, hv, C.ψi, W ) (Hinit (v)), where c = hq0 , γ0 i and Hinit denotes the initial
abstract heap environment such that Hinit (v) = ∅ for any v ∈ Ref.
To solve MOVP(Cs , Ct , W ), we (i) first compute gps(c) for each c ∈ Ct given
Cs , and then (ii) read out and combine the value of all paths between Cs and
Ct . We denote by H = 2|Obj| the length of the longest descending chain of theweighted domain, and by T the time to perform either ⊗ or ⊕. In our case,the time required to perform step (ii) can be ignored, and the worst case timecomplexity of performing step (i) is O(|Q|2 |∆| |Γ | H T ).

5

Acceleration by Lightening Iterative Cycles

5.1

A Traditional Iterative Procedure Scheme

Algo. OnTheFlyPTA in Fig. 1 sketches a procedure scheme for on-the-fly Java
PTA. It starts with analyzing the program entry points P0 , and computes thecall graph E and points-to relation R until convergence. For each iterative cycle,b– FindPointsTo : P × E × R → R (line 3) detects points-to information R
on the partial program P, according to updated information in the previous
iteration. The updated points-to information ∆R is derived at line 4.
b according– FindCallEdges : P × R × Θ → E (line 5) resolves call relation Eb
to R, obeying to the standard JVM semantics. The updated call relation∆E is derived at line 6.
– TakeReachables : E → P (line 8) returns the set of methods (reachable
from program entries) to be analyzed in the next iteration. It can be definedas the union of the first and third projection of E.

Algorithm OnTheFlyPTA
Input: the program entry points P0 and the class environment Θ
Output: G = (M, E) and R
0. E := ∅; R := ∅; P := P0
1. do
2.
R = FindPointsTo(P, E, R)
3.
∆R := R  R
4.
R := R t ∆R
5.
E := FindCallEdges(P, R, Θ)
6.
∆E := E \ E
7.
E := E ∪ ∆E
8.
P := TakeReachables(E)9. while ∆E 6= ∅ or ∆R 6= ∅

b

b

b

b

Fig. 1. A Procedure for On-the-fly Java Points-to Analysis

Theorem 1. The algorithm OnTheFlyPTA terminates if (i) the domain of P, E
and R are finite, and (ii) each of these functions FindPointsTo, FindCallEdges
and TakeReachables is monotonic wrt the set inclusion on P, E and the elementwise extension on R of the set inclusion.
FindPointsTo is the core procedure of PTA for Java. For most cloningbased algorithms, FindPointsTo corresponds to the propagation of points-to
sets, which is typically reduced to constraint solving problems. In contrast, wederive the analysis algorithm as model checking problems on WPDSs (Section 4).
Since the abstraction given in Section 3.2 is an over approximation, soundnessof our analysis is straightforward.

5.2

A Two-Staged Iterative Procedure Scheme

For an on-the-fly points-to analysis, the program coverage is enlarged whenpoints-to analysis proceeds. However, we found that only part of the whole program would effectively contribute to the enlargement of the program coverage.
To boost on-the-fly PTA, we propose a two-staged iterative procedure, denotedby (LE ◦ GU)∗ , which combines two phases of LE (local exploration) and GU (global
update). Generally, an LE iteration localizes the analysis on small parts of the
program, which is more likely to enlarge the program coverage, and GU is performed on-demand for guaranteeing completeness. Line 9 switches LE and GU
when conditions defined by SwitchCond are satisfied. Otherwise, a GU iteration
will be triggered to check sound convergence.

Algorithm TwoStaged OnTheFlyPTA
Input: the program entry points P0 and the class environment Θ
Output: G = (M, E) and R
0. E := ∅; R := ∅; P := P0 ; NotDone = NotDone’ := true
1. do
2.
NotDone := NotDone’
3.
R = FindPointsTo(P, E, R)
4.
∆R := R R
5.
R := R t ∆R
6.
E := FindCallEdges(P, R, Θ)
7.
∆E := E \ E
8.
E := E ∪ ∆E
9.
if SwitchCond(∆E, ∆R) = true then10.
P := TakeCoverage(E, ∆E, ∆R)
11.
NotDone’ := true
12.
else
13.
P := TakeReachables(E)14.
NotDone’ := false
15. while ∆E 6= ∅ or ∆R 6= ∅ or NotDone = true

b

b

b

b

Fig. 2. A Two-Staged Procedure for On-the-fly Java Points-to Analysis

Definition 18. SwitchCond(∆E, ∆R) = (∆E 6= ∅) ∨ (∆R ↓Reff 6= ∅), where
Reff ⊆ Ref is the set of base references of instance fields.
Def. 18 means that, an LE is triggered when either new call edges are detected
or new global references are found. Both indicates that the underlying model formodel checking is extended with new pushdown transitions.

Definition 19. TakeCoverage(E, ∆E, ∆R) = M1 ∪M2 ∪M3 ∪TakeReachables(∆E),
∃m, m0 ∈ C.Ψ ∃l, l0 ∈ L. (m, l, m0 ) ∈ ∆E, (m, l0 , m00 ) ∈ E,
M1 = m00 |and the return type of m00 is a reference type
M2 = {C.ψ | v C.ψ ∈ Reff and ∆R(v C.ψ , cc(v C.ψ )) 6= ∅}M3 = {m, C.ψ | ∆R(retC.ψ , cc(retC.ψ )) 6= ∅ and ∃l ∈ L.(m, l, C.ψ) ∈/ E}
A partial model is taken in the ways defined in TakeCoverage, where M1 says
that, if a new call relation found from m to m0 , other callees of m that returns
values of reference type are collected. M2 says that, if the points-to informationof base variables of instance fields are updated, their enclosing methods arecollected. M3 says that, if the points-to information of return variables of C.ψ
is updated, C.ψ and methods that call C.ψ and are not included in the previous
LE are collected. Note that, our choice of TakeCoverage is inspired and decided
by empirical studies on practiced Java benchmarks regarding efficiency.
Theorem 2. The algorithm TwoStaged OnTheFlyPTA terminates if (i) the domain of P, E and R are finite, and (ii) each of these functions FindPointsTo,
FindCallEdges, TakeCoverage and TakeReachables is monotonic on all arguments from their domains, and (iii) SwitchCond(∅, ∅) = false.
5.3

Adding Summary Transition Rules in LE

As given in Table 5 that extends translation rules Table 5, to make the two-staged
iterative procedure work effectively, summary transition rules (i.e., Ac ) thatcarry cached data flows to PE (Def. 20) are introduced, when building a WPAG
in an LE iteration. Translation rules leading from the dummy root node n0 to theprogram entries are lifted to {n0(Henv, C.ψ) | n0 = (Henv, sp), C.ψ ∈ PE }.
Definition 20. Given a program coverage P and the call relation E, PE ={m ∈ P | m0 ∈/ P if (m0 , m) ∈ E}.

Table 5. B[[ ]] : S → P(i)

B[[x := @this : T]] = A[[x := @this : T]] ∪ Ac
λx.s

where Ac = {(Henv, C.ψ)i (this, C.ψ) | s = R(this, cc(this))}if C.ψ ∈ PE and Ac = ∅ otherwise
B[[x := @parameterk : T]] = A[[x := @parameterk : T]] ∪ Ac
λx.s

where Ac = {(Henv, C.ψ)i (argk , C.ψ) | s = R(argk , cc(this))}if C.ψ ∈ PE and Ac = ∅ otherwise

In sequel, we show that adding summary transitions to arguments (i.e.,argi , this) of methods from PE will not cause any loss of precision.

Definition 21. For a pushdown system P = (Q, Γ, ∆, q0 , ω0 ), define D ⊆ Q ×
Γ × Q × Γ , such that hp, γi D hp0 , γ 0 i if there exists hp, γi ⇒∗ hp0 , γ 0 ω 0 i for some
ω 0 ∈ Γ ∗ . Define Ds ⊆ D such that hp, γi Ds hp0 , γ 0 i if (i) hp, γi D hp0 , γ 0 i and(ii) for each ω ∈ Γ ∗ and all transition sequence of σ : hp, γωi ⇒∗ hp0 , γ 0 ω 0 ωi forsome ω 0 ∈ Γ ∗ , and any hp00 , ω 00 i appearing in σ satisfies |w00 | > |w|. hp, γi is adominator of hp0 , γ 0 i if hp, γi Ds hp0 , γ 0 i.
Definition 22. Let W = (P, S, f) be a WPDS with P = (Q, Γ, ∆, q0 , γ0 ). For
p ∈ Q, γ ∈ Γ , {hpi , γi i | 0 ≤ i ≤ k} is a dominator set of hp, γi if (1), foreach i with 0 ≤ i ≤ k, hpi , γi i Ds hp, γi, and (2), for each transition sequence
σ : hq0 , γ0 i ⇒∗ hp, γwi with w ∈ Γ ∗ , there uniquely exists hpj , γj i such that
hpj , γj w0 i for some w0 ∈ Γ ∗ appears in σ.
Lemma 1. Given a WPDS W = (P, S, f) where P = (Q, Γ, ∆, q0 , γ0 ). For p ∈Q, γ ∈ Γ , let H be a dominator set of hp, γi and let c = hq0 , γ0 i, we haveL
[ hp, γi, W ) = hp ,γ i∈H MOVP(c,[ hpi , γi i, W ) ⊗ MOVP(hp[ i , γi i, hp, γi, W ).
MOVP(c,i i
Proof. Straightforward by definitions of frontiers and MOVP problems.
By Lemma 1, the computation of MOVP problems can be soundly divided
into two independent phases via dominators.
Definition 23. Given a WPDS W = (P, S, f) with P = (Q, Γ, ∆, q0 , γ0 ). For
p ∈ Q \ {q0 }, γ ∈ Γ \ {γ0 }, hp, γi is a frontier of W if either hp, γi Ds hp0 , γ 0 i or
hp, γi 4 hp0 , γ 0 i for any p0 ∈ Q, γ 0 ∈ Γ . A frontier set of W , denoted by FW , isa set of frontiers and hp, γi ∈ FW implies hp0 , γ 0 i ∈/ FW if hp, γi Ds hp0 , γ 0 i.
Theorem 3. Given a WPDS W = (P, S, f) with P = (Q, Γ, ∆, q0 , γ0 ). Let W0 =(P0 , S, f0 ) with P0 = (Q0 , Γ 0 , ∆0 ∪ δ, q0 , γ0 ), where Q0 ⊆ Q, Γ 0 ⊆ Γ , ∆0 ⊆ ∆, and[ hpi , γi i, W ) ⊕ f (r) | hpi , γi i ∈ FW 0 }.
δ = {r = hq0 , γ0 i ,→ hpi , γi i, f 0 (r) = MOVP(c,[ hp, γi, W 0 ) w MOVP(c,[ hp, γi, W ).
For p ∈ Q0 , γ ∈ Γ 0 , let c = hq0 , γ0 i, MOVP(c,Proof. By Definition 23, given p ∈ Q, γ ∈ Γ , any frontier set FW 0 of W 0 canbe decomposed into disjoint union FW 0 = F1 ] F2 , where F1 is some collection[ 0 , γ 0 i, hp, γi, W 0 ) = 0}. Theof dominators of hp, γi and F2 ⊆ {hp0 , γ 0 i | MOVP(hpproof is done according to Lemma 1 and the fact that F1 may not contain adominator set of hp, γi.
By Theorem 3, the analysis of LEs with introducing summary transition rules
will never cause any loss of precision, but can be not complete. The completenessis guaranteed by analysis of GUs.
Note that, the set of arguments CE = {(argk , C.ψ), (this, C.ψ) | C.ψ ∈ PE }from PE is a witness of the frontier set FW 0 , where W 0 is the WPDS encodedfrom methods of P augmented with cached transition rules. Recall the example
in Table 1, assume the partial model P taken in an LE consists of methods f1
and f2 . We know PE consists of f1 only by definition. A loss of precision would
be incurred, if summary transition rules Ac are introduced to arguments in f2 .

6Empirical Studies

We developed our analysis algorithms as a tool named Japot 2 , which exploits
Soot2.3.0 [16] for preprocessing from Java programs to Jimple codes, and theWeighted PDS Library as the model checking engine. We perform experiments
on Java applications from the Ashes benchmark suite [15] and the influential DaCapo benchmark suite [2] (Table 6). These applications are de facto benchmarks
when investigating Java points-to analysis. We target on the newest version of
DaCapo benchmark which requires JDK 1.5 or above, and stable Ashes benchmarks for which JDK 1.3 suffices. In sequel, the performance of Japot is measured
by call graph generation in terms of the number of reachable methods, which
is given in the “# Reachable Methods” column and these numbers take into
account libraries used by each benchmark. Benchmarks on which the back-end
model checker runs out of memory are not shown. All experiments were performed on a Mac OS X v.10.5.2 with a Xeon 2×2.66 GHz Dual-Core processor,and 4GB RAM. Only one processor is used in the following experiments.
Table 6. Benchmark Statistics and Call Graph Generation
Benchmark # Reachable Methods # Statements # Suite
# JDK
CHA
Japot Prec.↑Japot
soot-c
5460
5079
7%
83936
sablecc-j
13,0559004
31%143140 Ashes JDK 1.3.1 01
antlr
10,728×bloat
12,928 11090
14%
194063
chart
30,831×jython14,603×pmd
12,485×
Dacapo JDK 1.5.0 13
hsqldb
9983
8394
16%
142629
xalan
9977
8392
16%
141405
luindex
10,5968961
15%152592
lusearch
11,1909580
14%163958
eclipse12,703×

The sub-column titled CHA gives the number of reachable methods by the
CHA (Class Hierarchy Analysis) of Spark in soot-2.3.0. The sub-column titled
Japot gives results computed by our context-sensitive PTA and the “# Statements” column gives the number of Jimple statements that Japot analyzed. The“Prec.↑” sub-column shows how much improvement on precision can be obtainedby Japot over CHA. Our proposals regarding program modelling alone does notyield high scalability. Applying type filtering on-the-fly as usual and ignoring
differences of string constants are also essential to the scalability.
2

As an approximation, return variables from any native methods and reflection calls
can point to objects whose type allows, and a throw exception can be handled byany exception handler whose declared type allows as an over-approximation.

Table 7. An Acceleration on Efficiency
Benchmark # (LE ◦ GU)∗ (sec.) # GU∗ (sec.) # Accelerationsoot-csablecc-j
bloat
hsqldbxalan
luindexlusearch

656
1547
12339
1205
1321
1514
1757

1591
2785
41434
2910
2926
3880
4057

59%
44%
70%
59%
55%
61%
57%

We studied the efficiency improvement of (LE ◦ GU)∗ over GU∗ , and initial
results are given in Table 7 3 . The “# (LE◦GU)∗ ” column and the “# GU∗ ” column
gives the time in seconds of performing these iterative schemes respectively.
∗∗|
The “# Acceleration” column shows an acceleration in terms of |GU |−|(LE◦GU),|GU∗ |∗∗
which shows that (LE ◦ GU) is 2.5X faster in average than GU . We expect novel
strategies of taking LEs can improve the practical efficiency even more.

7

Related WorkOne of the pioneer work is Andersen’s PTA for C [1]. It is a subset-based, flowinsensitive analysis encoded as constraint solving problems, such that object
allocations and pointer assignments are described by subset constraints, e.g.
x = y induces pta(y) ⊆ pta(x). The scalability of Andersen’s analysis has been
greatly improved by more efficient constraint solvers. Andersen’s analysis wasintroduced to Java by using annotated constraints [12].
The first scalable cloning-based context-sensitive Java PTA is presented in[17], in which programs and analysis problems are encoded as rules in logic
program Datalog. Calling contexts are cloned after merging loops as equivalentclasses. The BDD (Binary Decision Diagram) based implementation, as well as
approximation by collapsing recursions, enable the analysis to scale. As discussed
in [6], there are usually rich and large loops within the call graph, and the lossof precision is potentially incurred after approximating recursions.
Reps, et al. present a general framework for program analysis based on CFLreachability [10], in which a PTA for C is shown by formulating pointer assignments as productions of context-free grammars. Inspired by this work, Sridharan, et al. formulated Andersen’s analysis for Java [14] as balanced-parentheses
problems regarding field read and write. A novel refinement-based analysis [13]is based on context-insensitive analysis and recovers the precision on-demandby removing imprecise propagation of points-to sets as violating a grammar for
3

Note that,data structures and program states cannot be shared between soot (inJava) and the back-end model checker (in C). These numbers include DISK IO timefor exchanging information between these two parts via files.

balanced parentheses, regarding both heap access and method calls. It shows
good precision and scalability with respect to downcast safety analysis.
Spark[5] is a widely-used test-bed for experimenting with Java PTA. It supports both equality and subset-based analysis, provides various algorithms forcall graph construction, such as CHA, RTA(Rapid Type Analysis), and on-the-fly
algorithms, as well as variations on field-sensitivity. The BDD-based implementation of the subset-based algorithms further improves the efficiency
One stream of research examines calling contexts in terms of sequences ofobjects on which methods are invoked, called object-sensitivity [9]. Similar tocall-site strings based approach, the sequence of receiver objects can be unbounded and demands proper approximations, like k-CFA. [6] indicates that
object-sensitivity excels at precision and is more likely to scale. Last but not
the least, existing practiced Java PTA as discussed above, are cloning-based forcontext-sensitivity and have restrictions on handling recursive procedure calls.
In contrast to points-to analysis with call graph constructed on-the-fly, anahead-of-time points-to analysis is proposed as one run of weighted pushdown
model checking [7]. The notion of valid paths are enriched with further obeying
to the Java semantics on dynamic dispatch. In particular, invalid control flowsthat violate Java semantics on dynamic dispatch are detected as those carrying
conflicted data flows. The analysis enjoys context-sensitivities regarding bothcall graph construction and valid paths.
Last but not least, WPDSs are extended to conditional weighted pushdown
systems (CWPDSs), by further associating each transition rule with a regular language that specifies conditions under which the transition rule can beapplied [8]. There are wider applications of CWPDs when analyzing programswith objected-oriented features, for which WPDSs are not precise enough under a direct application. It is also shown that, the model checking problem on
CWPDSs can be reduced to model checking problems on WPDSs.

8

Conclusions

We presented a scalable stacking-based context-sensitive points-to analysis forJava. The algorithm is derived as model checking problems on WPDSs, andno restriction is placed on (recursive) procedure calls. A two-staged iterative
procedure is further proposed to effectively accelerate the analysis, supported
by introducing summary transition rules. Our new iteration schemes shows thepotential of an incremental points-to analysis, and we are extending the current
setting with performing local explorations only.

9

Acknowledgments

This research is supported by STARC (Semiconductor Technology Academic
Research Center). We thank Dr. Stefan for help us using the Weighted PDS
Library. We also thank anonymous reviewers for their valuable comments.

References
1. L. Andersen. Program analysis and specialization for the c programming language.
PhD thesis, 1994.
2. S. M. Blackburn, R. Garner, C. Hoffman, and et.al. The DaCapo benchmarks:
Java benchmarking development and analysis. In OOPSLA ’06: Proceedings of the
21st annual ACM SIGPLAN conference on Object-Oriented Programing, Systems,
Languages, and Applications, pages 169–190, New York, NY, USA, Oct. 2006.
3. A. Lal and T. W. Reps. Improving pushdown system model checking. In 18th
International Conference on Computer Aided Verification, CAV06, volume 4144 of
Lecture Notes in Computer Science, pages 343–357. Springer, 2006.
4. A. Lal and T. W. Reps. Solving multiple dataflow queries using wpdss. In 15th
International Symposium on Static Analysis, SAS 2008, volume 5079 of Lecture
Notes in Computer Science, pages 93–109. Springer, 2008.
5. O. Lhoták and L. Hendren. Scaling java points-to analysis using spark. In Proceedings of the 12th International Conference on Compiler Construction.
6. O. Lhoták and L. Hendren. Context-sensitive points-to analysis: is it worth it?
In A. Mycroft and A. Zeller, editors, Compiler Construction, 15th International
Conference, volume 3923 of LNCS, pages 47–64, Vienna, Mar. 2006. Springer.
7. X. Li and M. Ogawa. An ahead-of-time yet context-sensitive points-to analysis forJava. In Proceedings of BYTECODE’09. ENTCS17798, York, Mar. 2009. Elsevier.
8. X. Li and M. Ogawa. Conditional weighted pushdown systems and applications.
In Proceedings of PEPM’10, to appear.
9. A. Milanova, A. Rountev, and B. G. Ryder. Parameterized object sensitivity forpoints-to analysis for java. ACM Trans. Softw. Eng. Methodol., 14(1):1–41, 2005.
10. T. Reps. Program analysis via graph reachability. In ILPS ’97: Proceedings ofthe 1997 international symposium on Logic programming, pages 5–19, Cambridge,
MA, USA, 1997. MIT Press.
11. T. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems andtheir application to interprocedural dataflow analysis. Sci. Comput. Program.,58(1-2):206–263, 2005.
12. A. Rountev, A. Milanova, and B. G. Ryder. Points-to analysis for java using
annotated constraints. SIGPLAN Not., 36(11):43–55, 2001.
13. M. Sridharan and R. Bodı́k. Refinement-based context-sensitive points-to analysis
for Java. volume 41, pages 387–400, New York, NY, USA, 2006. ACM.
14. M. Sridharan, D. Gopan, L. Shan, and R. Bodı́k. Demand-driven points-to analysis
for java. SIGPLAN Not., 40(10):59–76, 2005.
15. R. Vallée-Rai. Ashes suite collection. http://www.sable.mcgill.ca/ashes.
16. R. Vallée-Rai, E. Gagnon, L. J. Hendren, P. Lam, P. Pominville, and V. Sundaresan. Optimizing Java bytecode using the Soot framework: Is it feasible? In Compiler
Construction, 9th International Conference (CC 2000), pages 18–34, 2000.
17. J. Whaley and M. Lam. Cloning-based context-sensitive pointer alias analysis
using binary decision diagrams. In ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI 2004), pages 131–144, 2004.
18. G. Xu and A. Rountev. Merging equivalent contexts for scalable heap-cloningbased context-sensitive points-to analysis. In ISSTA ’08: Proceedings of the 2008
international symposium on Software testing and analysis, pages 225–236, New
York, NY, USA, 2008. ACM.