Pushdown Control-Flow Analysis of Higher-Order Programs
Christopher Earl

David Van Horn ∗

Matthew Might

Northeastern University
dvanhorn@ccs.neu.edu

arXiv:1007.4268v1 [] 24 Jul 2010

University of Utah
{cwearl,might}@cs.utah.edu

Abstract
Context-free approaches to static analysis gain precision over classical approaches by perfectly matching returns to call sites—
a property that eliminates spurious interprocedural paths. Vardoulakis and Shivers’s recent formulation of CFA2 showed that it
is possible (if expensive) to apply context-free methods to higherorder languages and gain the same boost in precision achieved over
first-order programs.
To this young body of work on context-free analysis of higherorder programs, we contribute a pushdown control-flow analysis framework, which we derive as an abstract interpretation of a
CESK machine with an unbounded stack. One instantiation of this
framework marks the first polyvariant pushdown analysis of higherorder programs; another marks the first polynomial-time analysis. In the end, we arrive at a framework for control-flow analysis
that can efficiently compute pushdown generalizations of classical
control-flow analyses.

1. Introduction
Static analysis is bound by theory to accept diminished precision as
the price of decidability. The easiest way to guarantee decidability
for a static analysis is to restrict it to a finite state-space. Not
surprisingly, finite state-spaces have become a crutch.
Whenever an abstraction maps an infinite (concrete) state-space
down to the finite state-space of a static analysis, the pigeon-hole
principle forces merging. Distinct execution paths and values can
and do become indistinguishable under abstraction, e.g., 3 and 4
both abstract to the same value: positive.
Our message is that finite abstraction goes too far: we can abstract into an infinite state-space to improve precision, yet remain
decidable. Specifically, we can abstract the concrete semantics of
a higher-order language into a pushdown automaton (PDA). As an
infinite-state system, a PDA-based abstraction preserves more information than a classical finite-state analysis. Yet, being less powerful than a Turing machine, properties important for computing
control-flow analysis (e.g. emptiness, intersection with regular languages, reachability) remain decidable.

0CFA says that the flow set for the variable a contains both 3
and 4. In fact, so does the flow set for the variable b. For returnflow,1 0CFA says that the invocation of (id 4) may return to the
invocation of (id 3) or (id 4) and vice versa; that is, according
to Shivers’s 0CFA, this program contains a loop.
To combat merging, control-flow analyses have focused on
increasing context-sensitivity [Shivers 1991]. Context-sensitivity
tries to qualify any answer that comes back from a CFA with a
context in which that answer is valid. That is, instead of answering “λ42 may flow to variable v13 ,” a context-sensitive analysis
might answer “λ42 may flow to variable v13 when bound after calling f .” While context-sensitivity recovers some lost precision, it is
no silver bullet. A finite-state analysis stores only a finite amount
of program context to discriminate data- and control-flows during
analysis. Yet, the pigeon-hole principle remains merciless: as long
as the state-space is finite, merging is inevitable for some programs.
Of all the forms of merging, the most pernicious is the merging of return-flow information. As the example shows, a finite-state
control-flow analysis will lose track of where return-points return
once the maximum bound on context is exceeded. Even in programs with no higher-order functions, return-flow merging will still
happen during control-flow analysis.
1.2 A first shot: CFA2
Vardoulakis and Shivers’s recent work on CFA2 [Vardoulakis and
Shivers 2010] constitutes an opening salvo on ending the returnflow problem for the static analysis of higher-order programs.
CFA2 employs an implicit pushdown system that models the stack
of a program. CFA2 solves the return-flow problem for higher-order
programs, but it has drawbacks:
1. CFA2 allows only monovariant precision.
2. CFA2 has exponential complexity in the size of the program.
3. CFA2 is restricted to continuation-passing style.
Our solution overcomes all three drawbacks: it allows polyvariant precision, we can widen it to O(n6 )-time complexity in the
monovariant case and we can operate on direct-style programs.

1.1 The problem with merging
A short example provides a sense of how the inevitable merging
that occurs under a finite abstraction harms precision. Shivers’s
0CFA [Shivers 1991] produces spurious data-flows and returnflows in the following example:
(let* ((id (lambda (x) x))
(a (id 3))
(b (id 4)))
a)
∗ Supported

by the National Science Foundation under grant 0937060 to the
Computing Research Association for the CIFellow Project.

1.3 Our solution: Abstraction to pushdown systems
To prevent return-flow merging during higher-order control-flow
analysis, we abstract into an explicit pushdown system instead of a
finite-state machine. The program stack, which determines returnflow, will remain unbounded and become the pushdown stack. As a
result, return-flow information will never be merged: in the abstract
semantics, a function returns only whence it was called.
1 “Return-flow”

analysis asks to which call sites a given return point may
return. In the presence of tail calls, which break the balance between calls
and returns, return-flow analysis differs from control-flow analysis.

1.4 Overview
This paper is organized as follows: first, we define a variant of the
CESK machine [Felleisen and Friedman 1987] for the A-Normal
Form λ-calculus [Flanagan et al. 1993]. In performing analysis, we
wish to soundly approximate intensional properties of this machine
when it evaluates a given program. To do so, we construct an abstract interpretation of the machine. The abstracted CESK machine
operates much like its concrete counterpart and soundly approximates its behavior, but crucially, many properties of the concrete
machine that are undecidable become decidable when considered
against the abstracted machine (e.g. “is a given machine configuration reachable?” becomes a decidable property).
The abstract counterpart to the CESK machine is constructed
by bounding the store component of the machine to some finite
size. However, the stack component (represented as a continuation)
is left unabstracted. (This is in contrast to finite-state abstractions
that store-allocate continuations [Van Horn and Might 2010].) Unlike most higher-order abstract interpreters, the unbounded stack
implies this machine has a potentially infinite set of reachable machine configurations, and therefore enumerating them is not a feasible approach to performing analysis.
Instead, we demonstrate how properties can be decided by transforming the abstracted CESK machine into an equivalent pushdown automaton. We then reduce higher-order control-flow analysis to deciding the non-emptiness of a language derived from the
PDA. (This language happens to be the intersection of a regular language and the context-free language described by the PDA.) This
approach—though concise, precise and decidable—is formidably
expensive, with complexity doubly exponential in the size of the
program.
We simplify the algorithm to merely exponential in the size of
the input program by reducing the control-flow problem to pushdown reachability [Bouajjani et al. 1997]. Unfortunately, the abstracted CESK machine has an exponential number of control states
with respect to the size of the program. Thus, pushdown reachability for higher-order programs appears to be inherently exponential.
Noting that most control states in the abstracted CESK machine
are actually unreachable, we present a fixed-point algorithm for deciding pushdown reachability that is polynomial-time in the number of reachable control states. Since the pushdown systems produced by abstracted CESK machines are sparse, such algorithms,
though exponential in the worst case, are reasonable options. Yet,
we can do better.
Next, we add an ǫ-closure graph (a graph encoding no-stackchange reachability) and a work-list to the fixed-point algorithm.
Together, these lower the cost of finding the reachable states of a
pushdown system from O(|Γ|4 m5 ) to O(|Γ|2 m4 ), where Γ is the
stack alphabet and m is the number of reachable control states.
To drop the complexity of our analysis to polynomial-time in
the size of the input program, we must resort to both widening and
monovariance. Widening with a single-threaded store and using
a monovariant allocation strategy yields a pushdown control-flow
analysis with polynomial-time complexity, at O(n6 ), where n is
the size of the program.
Finally, we briefly highlight applications of pushdown controlflow analyses that are outside the reach of classical ones, discuss
related work, and conclude.

[Sipser 2005]. Even those familiar with pushdown theory may want
to skim this section to pick up our notation.
2.1 Syntactic sugar
When a triple (x, ℓ, x′ ) is an edge in a labeled graph, a little
syntactic sugar aids presentation:
ℓ

x ֌ x′ ≡ (x, ℓ, x′ ).
Similarly, when a pair (x, x′ ) is a graph edge:
x ֌ x′ ≡ (x, x′ ).
We use both string and vector notation for sequences:
a1 a2 . . . an ≡ ha1 , a2 , . . . , an i ≡ ~a.
2.2 Stack actions, stack change and stack manipulation
Stacks are sequences over a stack alphabet Γ. Pushdown systems
do much stack manipulation, so to represent this more concisely,
we turn stack alphabets into “stack-action” sets; each character
represents a change to the stack: push, pop or no change.
For each character γ in a stack alphabet Γ, the stack-action set
Γ± contains a push character γ+ and a pop character γ− ; it also
contains a no-stack-change indicator, ǫ:
g ∈ Γ± ::= ǫ
| γ+
| γ−

for each γ ∈ Γ
for each γ ∈ Γ

[stack unchanged]
[pushed γ]
[popped γ].

In this paper, the symbol g represents some stack action.
2.3 Pushdown systems
A pushdown system is a triple M = (Q, Γ, δ) where:
1. Q is a finite set of control states;
2. Γ is a stack alphabet; and
3. δ ⊆ Q × Γ± × Q is a transition relation.
We use PDS to denote the class of all pushdown systems.
Unlike the more widely known pushdown automaton, a pushdown system does not recognize a language.
For the following definitions, let M = (Q, Γ, δ).
• The configurations of this machine—Configs (M )—are pairs

over control states and stacks:
Configs(M ) = Q × Γ.∗
• The labeled transition relation (7−→M ) ⊆ Configs(M ) ×

Γ± × Configs(M ) determines whether one configuration may
transition to another while performing the given stack action:
ǫ

ǫ

(q, ~γ ) 7−→ (q ′ , ~γ ) iff q ֌ q ′ ∈ δ
M

γ−

γ−

(q, γ : ~γ ) 7−→ (q ′ , ~γ ) iff q ֌ q ′ ∈ δ
M

γ+

γ+

(q, ~γ ) 7−→ (q ′ , γ : ~γ ) iff q ֌ q ′ ∈ δ
M

[no change]
[pop]
[push].

• If unlabelled, the transition relation (7−→) checks whether any

stack action can enable the transition:
g

c 7−→ c′ iff c 7−→ c′ for some stack action g.

2. Pushdown preliminaries
In this work, we make use of both pushdown systems and pushdown automata. (A pushdown automaton is a specific kind of pushdown system.) There are many (equivalent) definitions of these
machines in the literature, so we adapt our own definitions from

M

M

• For a string of stack actions g1 . . . gn :
g ...gn

g

g

gn−1

gn

M

M

M

M

M

2
1
· · · 7−→ cn−1 7−→ cn ,
c1 7−→
c0 1−
7 → cn iff c0 7−→

for some configurations c0 , . . . , cn .

• For the transitive closure:
∗

~
g

M

M

requires that all arguments to a function be atomic:
e ∈ Exp ::= (let ((v call)) e)
| call

c 7−→ c′ iff c 7−→ c′ for some action string ~g .
Note Some texts define the transition relation δ so that δ ⊆
Q×Γ×Q×Γ∗ . In these texts, (q, γ, q ′ , ~γ ) ∈ δ means, “if in control
state q while the character γ is on top, pop the stack, transition
to control state q ′ and push ~γ .” Clearly, we can convert between
these two representations by introducing extra control states to our
representation when it needs to push multiple characters.
2.4 Rooted pushdown systems
A rooted pushdown system is a quadruple (Q, Γ, δ, q0 ) in which
(Q, Γ, δ) is a pushdown system and q0 ∈ Q is an initial (root) state.
RPDS is the class of all rooted pushdown systems.
For a rooted pushdown system M = (Q, Γ, δ, q0 ), we define a
the root-reachable transition relation:
g

∗

g

M

M

M

c 7−−→
→ c′ iff (q0 , hi) 7−→ c and c 7−→ c′ .
In other words, the root-reachable transition relation also makes
sure that the root control state can actually reach the transition.
We overload the root-reachable transition relation to operate on
control states as well:

| æ
f, æ ∈ Atom ::= v | lam
lam ∈ Lam ::= (λ (v) e)
call ∈ Call ::= (f æ)
v ∈ Var is a set of identifiers

[non-tail call]
[tail call]
[return]
[atomic expressions]
[lambda terms]
[applications]
[variables].

We use the CESK machine of Felleisen and Friedman [1987] to
specify the semantics of ANF. We have chosen the CESK machine
because it has an explicit stack, and under abstraction, the stack
component of our CESK machine will become the stack component
of a pushdown system.
First, we define a set of configurations (Conf ) for this machine:
c ∈ Conf
ρ ∈ Env
σ ∈ Store
clo ∈ Clo

= Exp × Env × Store × Kont
= Var ⇀ Addr
= Addr → Clo
= Lam × Env

κ ∈ Kont = Frame ∗

[continuations]

q 7−−→
→ q ′ iff (q, ~γ ) 7−−→
→ (q ′ , ~γ ′ ) for some stacks ~γ , ~γ ′ .

φ ∈ Frame = Var × Exp × Env
a ∈ Addr is an infinite set of addresses

For both root-reachable relations, if we elide the stack-action label,
then, as in the un-rooted case, the transition holds if there exists
some stack action that enables the transition:

To define the semantics, we need five items:

g

g

M

M

[stack frames]
[addresses].

1. I : Exp → Conf injects an expression into a configuration.

g

2. A : Atom×Env ×Store ⇀ Clo evaluates atomic expressions.

M

3. E : Exp → P (Conf ) computes the set of reachable machine
configurations for a given program.

q 7−−→
→ q ′ iff q 7−−→
→ q ′ for some action g.
M

[configurations]
[environments]
[stores]
[closures]

2.5 Pushdown automata
A pushdown automaton is a generalization of a rooted pushdown
system, a 7-tuple (Q, Σ, Γ, δ, q0 , F, ~γ ) in which:
1. Σ is an input alphabet;

4. (⇒) ⊆ Conf × Conf transitions between configurations.
5. alloc : Var × Conf → Addr chooses fresh store addresses for
newly bound variables.
Program injection The program injection function pairs an expression with an empty environment, an empty store and an empty
stack to create the initial configuration:

2. δ ⊆ Q × Γ± × (Σ ∪ {ǫ}) × Q is a transition relation;
3. F ⊆ Q is a set of accepting states; and
4. ~γ ∈ Γ∗ is the initial stack.

c0 = I(e) = (e, [], [], hi).

We use PDA to denote the class of all pushdown automata.
Pushdown automata recognize languages over their input alphabet. To do so, their transition relation may optionally consume an input character upon transition. Formally, a PDA M =
(Q, Σ, Γ, δ, q0 , F, ~γ ) recognizes the language L(M ) ⊆ Σ∗ :
ǫ ∈ L(M ) if q0 ∈ F
aw ∈ L(M ) if δ(q0 , γ+ , a, q ′ ) and w ∈ L(Q, Σ, Γ, δ, q ′ , F, γ : ~γ )
aw ∈ L(M ) if δ(q0 , ǫ, a, q ′ ) and w ∈ L(Q, Σ, Γ, δ, q ′ , F, ~γ )
′

′

Atomic expression evaluation The atomic expression evaluator,
A : Atom × Env × Store ⇀ Clo, returns the value of an atomic
expression in the context of an environment and a store:
A(lam, ρ, σ) = (lam, ρ)
A(v, ρ, σ) = σ(ρ(v))

[closure creation]
[variable look-up].

Reachable configurations The evaluator E : Exp → P (Conf )
returns all configurations reachable from the initial configuration:
E (e) = {c : I(e) ⇒∗ c} .

′

aw ∈ L(M ) if δ(q0 , γ− , a, q ) and w ∈ L(Q, Σ, Γ, δ, q , F, ~γ )
′

where ~γ = hγ, γ2 , . . . , γn i and ~γ = hγ2 , . . . , γn i,
where a is either the empty string ǫ or a single character.

Transition relation To define the transition c ⇒ c′ , we need three
rules. The first rule handles tail calls by evaluating the function into
a closure, evaluating the argument into a value and then moving to
the body of the λ-term within the closure:
c

3. Setting: A-Normal Form λ-calculus
Since our goal is to create pushdown control-flow analyses of
higher-order languages, we choose to operate on the λ-calculus.
For simplicity of the concrete and abstract semantics, we choose
to analyze programs in A-Normal Form, however this is strictly a
cosmetic choice; all of our results can be replayed mutatis mutandis
in a direct-style setting. ANF enforces an order of evaluation and it

c′

z
}|
{
z
}|
{
([[(f æ)]], ρ, σ, κ) ⇒ (e, ρ′′ , σ ′ , κ) , where
([[(λ (v) e)]], ρ′ ) = A(f, ρ, σ)
a = alloc(v, c)
ρ′′ = ρ′ [v 7→ a]
σ ′ = σ[a 7→ A(æ, ρ, σ)].

Non-tail call pushes a frame onto the stack and evaluates the call:
c′

c

}|
{
z
}|
{
z
([[(let ((v call)) e)]], ρ, σ, κ) ⇒ (call, ρ, σ, (v, e, ρ) : κ) .

Function return pops a stack frame:
c

c

′

}|
{
}|
{
z
z
(æ, ρ, σ, (v, e, ρ′ ) : κ) ⇒ (e, ρ′′ , σ ′ , κ) , where
a = alloc(v, c)
ρ′′ = ρ′ [v 7→ a]
σ ′ = σ[a 7→ A(æ, ρ, σ)].
Allocation The address-allocation function is an opaque parameter in this semantics. We have done this so that the forthcoming
abstract semantics may also parameterize allocation, and in so doing provide a knob to tune the polyvariance and context-sensitivity
of the resulting analysis. For the sake of defining the concrete semantics, letting addresses be natural numbers suffices, and then the
allocator can choose the lowest unused address:
Addr = N
alloc(v, (e, ρ, σ, κ)) = 1 + max(dom(σ)).

4. An infinite-state abstract interpretation
Our goal is to statically bound the higher-order control-flow of the
CESK machine of the previous section. So, we are going to conduct
an abstract interpretation.
Since we are concerned with return-flow precision, we are going to abstract away less information than we normally would.
Specifically, we are going to construct an infinite-state abstract interpretation of the CESK machine by leaving its stack unabstracted.
(With an infinite-state abstraction, the usual approach for computing the static analysis—exploring the abstract configurations reachable from some initial configuration—simply will not work. Subsequent sections focus on finding an algorithm that can compute a
finite representation of the reachable abstract configurations of the
abstracted CESK machine.)
For the abstract interpretation of the CESK machine, we need
an abstract configuration-space (Figure 1). To construct one, we
force addresses to be a finite set, but crucially, we leave the stack
untouched. When we compact the set of addresses into a finite
set, the machine may run out of addresses to allocate, and when
it does, the pigeon-hole principle will force multiple closures to
reside at the same address. As a result, we have no choice but to
force the range of the store to become a power set in the abstract
configuration-space. To construct the abstract transition relation,
we need five components analogous to those from the concrete
semantics.
Program injection The abstract injection function Î : Exp →
\ pairs an expression with an empty environment, an empty
Conf
store and an empty stack to create the initial abstract configuration:
ĉ0 = Î(e) = (e, [], [], hi).
Atomic expression evaluation The abstract atomic expression
d returns the value
d × Store
\ → P(Clo),
evaluator, Â : Atom × Env
of an atomic expression in the context of an environment and a
store; note how it returns a set:
Â(lam, ρ̂, σ̂) = {(lam, ρ)}

[closure creation]

Â(v, ρ̂, σ̂) = σ̂(ρ̂(v))

[variable look-up].

Reachable configurations The abstract program evaluator Ê :
\) returns all of the configurations reachable from
Exp → P(Conf

d × Store
\ = Exp × Env
\ × Kont
[
ĉ ∈ Conf

d = Var ⇀ Addr
[
ρ̂ ∈ Env


d
[ → P Clo
\ = Addr
σ̂ ∈ Store

[environments]
[stores]

c ∈ Clo
d = Lam × Env
d
clo

[ = Frame
\
κ̂ ∈ Kont

[configurations]

[closures]

∗

[continuations]

d
\ = Var × Exp × Env
φ̂ ∈ Frame

[stack frames]

[ is a finite set of addresses
â ∈ Addr

[addresses].

Figure 1. The abstract configuration-space.
the initial configuration:

n
o
Ê(e) = ĉ : Î(e) ;∗ ĉ .

Because there are an infinite number of abstract configurations,
a naı̈ve implementation of this function may not terminate. In
Sections 5 through 8, we show that there is a way to compute a
finite representation of this set.
Transition relation The abstract transition relation (;) ⊆
\ × Conf
\ has three rules, one of which has become nonConf
deterministic. A tail call may fork because there could be multiple
abstract closures that it is invoking:
ĉ′

ĉ

z
}|
{
}|
{
z
([[(f æ)]], ρ̂, σ̂, κ̂) ; (e, ρ̂′′ , σ̂ ′ , κ̂) , where
([[(λ (v) e)]], ρ̂′ ) ∈ Â(f, ρ̂, σ̂)

[
â = alloc(v,
ĉ)
ρ̂′′ = ρ̂′ [v 7→ â]
σ̂ ′ = σ̂ ⊔ [â 7→ Â(æ, ρ̂, σ̂)].
We define all of the partial orders shortly, but for stores:
(σ̂ ⊔ σ̂ ′ )(â) = σ̂(â) ∪ σ̂ ′ (â).
A non-tail call pushes a frame onto the stack and evaluates the call:
ĉ′

ĉ

}|
{
z
}|
{
z
([[(let ((v call)) e)]], ρ̂, σ̂, κ̂) ; (call, ρ̂, σ̂, (v, e, ρ̂) : κ̂) .

A function return pops a stack frame:
ĉ

ĉ′

z
z
}|
{
}|
{
(æ, ρ̂, σ̂, (v, e, ρ̂′ ) : κ̂) ; (e, ρ̂′′ , σ̂ ′ , κ̂) , where
[
â = alloc(v,
ĉ)

ρ̂′′ = ρ̂′ [v 7→ â]
σ̂ ′ = σ̂ ⊔ [â 7→ Â(æ, ρ̂, σ̂)].
Allocation, polyvariance and context-sensitivity In the abstract
[ : Var × Conf
\→
semantics, the abstract allocation function alloc
[ determines the polyvariance of the analysis (and, by extenAddr
sion, its context-sensitivity). In a control-flow analysis, polyvariance literally refers to the number of abstract addresses (variants)
there are for each variable. By selecting the right abstract allocation
function, we can instantiate pushdown versions of classical flow
analyses.
Monovariance: Pushdown 0CFA Pushdown 0CFA uses variables
themselves for abstract addresses:

[ = Var
Addr
alloc(v, ĉ) = v.

\
PDA(e)
= (Q, Σ, Γ, δ, q0 , F, hi), where
d × Store
\
Q = Exp × Env
Σ=Q

Context-sensitive: Pushdown 1CFA Pushdown 1CFA pairs the
variable with the current expression to get an abstract address:

\
Γ = Frame

′

[ = Var × Exp
Addr
alloc(v, (e, ρ̂, σ̂, κ̂)) = (v, e).
Polymorphic splitting: Pushdown poly/CFA Assuming we compiled the program from a programming language with let-bound
polymorphism and marked which functions were let-bound, we can
enable polymorphic splitting:
[ = Var + Var × Exp
Addr
(
(v, [[(f æ)]]) f is let-bound
alloc(v, ([[(f æ)]], ρ̂, σ̂, κ̂)) =
v
otherwise.
Pushdown k-CFA For pushdown k-CFA, we need to look beyond
the current state and at the last k states. By concatenating the
expressions in the last k states together, and pairing this sequence
with a variable we get pushdown k-CFA:
[ = Var × Expk
Addr
[
alloc(v,
h(e1 , ρ̂1 , σ̂1 , κ̂1 ), . . .i) = (v, he1 , . . . , ek i).
4.1 Partial orders
For each set X̂ inside the abstract configuration-space, we use the
natural partial order, (⊑X̂ ) ⊆ X̂ × X̂. Abstract addresses and
syntactic sets have flat partial orders. For the other sets:
• The partial order lifts point-wise over environments:

ρ̂ ⊑ ρ̂′ iff ρ̂(v) = ρ̂′ (v) for all v ∈ dom(ρ̂).
• The partial orders lifts component-wise over closures:

(lam, ρ̂) ⊑ (lam, ρ̂′ ) iff ρ̂ ⊑ ρ̂′ .
• The partial order lifts point-wise over stores:
′

′

σ̂ ⊑ σ̂ iff σ̂(â) ⊑ σ̂ (â) for all â ∈ dom(σ̂).
• The partial order lifts component-wise over frames:

(v, e, ρ̂) ⊑ (v, e, ρ̂′ ) iff ρ̂ ⊑ ρ̂′ .
• The partial order lifts element-wise over continuations:

hφ̂1 , . . . , φ̂n i ⊑ hφ̂′1 , . . . , φ̂′n i iff φ̂i ⊑ φ̂′i .
• The partial order lifts component-wise across configurations:

(e, ρ̂, σ̂, κ̂) ⊑ (e, ρ̂′ , σ̂ ′ , κ̂′ ) iff ρ̂ ⊑ ρ̂′ and σ̂ ⊑ σ̂ ′ and κ̂ ⊑ κ̂′ .
4.2 Soundness
To prove soundness, we need an abstraction map α that connects
the concrete and abstract configuration-spaces:
α(e, ρ, σ, κ) = (e, α(ρ), α(σ), α(κ))
α(ρ) = λv.α(ρ(v))
G
{α(σ(a))}
α(σ) = λâ.
α(a)=â

αhφ1 , . . . , φn i = hα(φ1 ), . . . , α(φn )i
α(v, e, ρ) = (v, e, α(ρ))
α(a) is determined by the allocation functions.

′

(q, ǫ, q , q ) ∈ δ iff (q, κ̂) ; (q ′ , κ̂) for all κ̂
(q, φ̂− , q ′ , q ′ ) ∈ δ iff (q, φ̂ : κ̂) ; (q ′ , κ̂) for all κ̂
(q, φ̂′+ , q ′ , q ′ ) ∈ δ iff (q, κ̂) ; (q ′ , φ̂′ : κ̂) for all κ̂
(q0 , hi) = Î(e)
F = Q.
\ : Exp → PDA.
Figure 2. PDA
It is easy to prove that the abstract transition relation simulates
the concrete transition relation:
Theorem 4.1. If:
α(c) ⊑ ĉ and c ⇒ c′ ,
\ such that:
then there must exist ĉ′ ∈ Conf
α(c′ ) ⊑ ĉ′ and ĉ ⇒ ĉ′ .
Proof. The proof follows by case-wise analysis on the type of the
expression in the configuration. It is a straightforward adaptation of
similar proofs, such as that of Might [2007] for k-CFA.

5. From the abstracted CESK machine to a PDA
In the previous section, we constructed an infinite-state abstract
interpretation of the CESK machine. The infinite-state nature of the
abstraction makes it difficult to see how to answer static analysis
questions. Consider, for instance, a control flow-question:
At the call site (f æ), may a closure over lam be called?
If the abstracted CESK machine were a finite-state machine, an
algorithm could answer this question by enumerating all reachable configurations and looking for an abstract configuration
([[(f æ)]], ρ̂, σ̂, κ̂) in which (lam, ) ∈ Â(f, ρ̂, σ̂). However, because the abstracted CESK machine may contain an infinite number
of reachable configurations, an algorithm cannot enumerate them.
Fortunately, we can recast the abstracted CESK as a special
kind of infinite-state system: a pushdown automaton (PDA). Pushdown automata occupy a sweet spot in the theory of computation:
they have an infinite configuration-space, yet many useful properties (e.g. word membership, non-emptiness, control-state reachability) remain decidable. Once the abstracted CESK machine becomes a PDA, we can answer the control-flow question by checking whether a specific regular language, when intersected with the
language of the PDA, turns into the empty language.
The recasting as a PDA is a shift in perspective. A configuration has an expression, an environment and a store. A stack character is a frame. We choose to make the alphabet the set of control
states, so that the language accepted by the PDA will be sequences
of control-states visited by the abstracted CESK machine. Thus,
every transition will consume the control-state to which it transitioned as an input character. Figure 2 defines the program-to-PDA
\ : Exp → PDA. (Note the implicit use
conversion function PDA
\.)
[ ∼
of the isomorphism Q × Kont
= Conf
At this point, we can answer questions about whether a specified control state is reachable by formulating a question about the

intersection of a regular language with a context-free language described by the PDA. That is, if we want to know whether the control
state (e′ , ρ̂, σ̂) is reachable in a program e, we can reduce the problem to determining:

\
Σ∗ · (e′ , ρ̂, σ̂) · Σ∗ ∩ L(PDA(e))
6= ∅,

where L1 · L2 is the concatenation of formal languages L1 and L2 .

1. S is a finite set of nodes;
2. Γ is a set of frames;
3. E ⊆ S × Γ± × S is a set of stack-action edges; and
4. s0 is an initial state;
such that for any node s ∈ S, it must be the case that:
∗

(s0 , hi) 7−→ (s, ~γ ) for some stack ~γ .

Theorem 5.1. Control-state reachability is decidable.

G

Proof. The intersection of a regular language and a context-free
language is context-free. The emptiness of a context-free language
is decidable.

In other words, a Dyck state graph is equivalent to a rooted pushdown system in which there is a legal path to every control state
from the initial control state.2
We use DSG to denote the class of Dyck state graphs. Clearly:

Now, consider how to use control-state reachability to answer
the control-flow question from earlier. There are a finite number of
possible control states in which the λ-term lam may flow to the
function f in call site (f æ); let’s call the this set of states Ŝ:
n
o
Ŝ = ([[(f æ)]], ρ̂, σ̂) : (lam, ρ̂′ ) ∈ Â(f, ρ̂, σ̂) for some ρ̂′ .

DSG ⊂ RPDS.

What we want to know is whether any state in the set Ŝ is reachable
in the PDA. In effect what we are asking is whether there exists a
control state q ∈ Ŝ such that:
\
Σ∗ · {q} · Σ∗ ∩ L(PDA(e))
6= ∅.
If this is true, then lam may flow to f ; if false, then it does not.
Problem: Doubly exponential complexity The non-emptinessof-intersection approach establishes decidability of pushdown
control-flow analysis. But, two exponential complexity barriers
make this technique impractical.
First, there are an exponential number of both environments
d
\
Addr |
[ ||Var| ) and stores (2|Clo|×|
(|Addr
) to consider for the set Ŝ. On
top of that, computing the intersection of a regular language with a
context-free language will require enumeration of the (exponential)
control-state-space of the PDA. As a result, this approach is doubly
exponential. For the next few sections, our goal will be to lower the
complexity of pushdown control-flow analysis.

6. Focusing on reachability
In the previous section, we saw that control-flow analysis reduces
to the reachability of certain control states within a pushdown system. We also determined reachability by converting the abstracted
CESK machine into a PDA, and using emptiness-testing on a language derived from that PDA. Unfortunately, we also found that
this approach is deeply exponential.
Since control-flow analysis reduced to the reachability of
control-states in the PDA, we skip the language problems and go
directly to reachability algorithms of Bouajjani et al. [1997], Kodumal and Aiken [2004], Reps [1998] and Reps et al. [2005] that
determine the reachable configurations within a pushdown system.
These algorithms are even polynomial-time. Unfortunately, some
of them are polynomial-time in the number of control states, and
in the abstracted CESK machine, there are an exponential number
of control states. We don’t want to enumerate the entire control
state-space, or else the search becomes exponential in even the best
case.
To avoid this worst-case behavior, we present a straightforward
pushdown-reachability algorithm that considers only the reachable
control states. We cast our reachability algorithm as a fixed-point
iteration, in which we incrementally construct the reachable subset
of a pushdown system. We term these algorithms “iterative Dyck
state graph construction.”
A Dyck state graph is a compacted, rooted pushdown system
G = (S, Γ, E, s0 ), in which:

A Dyck state graph is a rooted pushdown system with the “fat”
trimmed off; in this case, unreachable control states and unreachable transitions are the “fat.”
We can formalize the connection between rooted pushdown
systems and Dyck state graphs with a map:
DSG : RPDS → DSG.
Given a rooted pushdown system M = (Q, Γ, δ, q0 ), its equivalent
Dyck state graph is DSG(M ) = (S, Γ, E, q0 ), where the set S
contains reachable nodes:
n
o
∗
S = q : (q0 , hi) 7−→ (q, ~γ ) for some stack ~γ ,
M

and the set E contains reachable edges:
n g
o
g
E = q ֌ q ′ : q 7−−→
→ q′ ,
M

and s0 = q0 .
In practice, the real difference between a rooted pushdown system and a Dyck state graph is that our rooted pushdown system will
be defined intensionally (having come from the components of an
abstracted CESK machine), whereas the Dyck state graph will be
defined extensionally, with the contents of each component explicitly enumerated during its construction.
Our near-term goals are (1) to convert our abstracted CESK
machine into a rooted pushdown system and (2) to find an efficient
method for computing an equivalent Dyck state graph from a rooted
pushdown system.
To convert the abstracted CESK machine into a rooted push\ : Exp → RPDS:
down system, we use the function RPDS
\
RPDS(e)
= (Q, Γ, δ, q0 )
d × Store
\
Q = Exp × Env
\
Γ = Frame

ǫ

′

q ֌ q ∈ δ iff (q, κ̂) ; (q ′ , κ̂) for all κ̂
φ̂−

q ֌ q ′ ∈ δ iff (q, φ̂ : κ̂) ; (q ′ , κ̂) for all κ̂
φ̂+

q ֌ q ′ ∈ δ iff (q, κ̂) ; (q ′ , φ̂ : κ̂) for all κ̂
(q0 , hi) = Î(e).

7. Compacting rooted pushdown systems
We now turn our attention to compacting a rooted pushdown system
(defined intensionally) into a Dyck state graph (defined extension2 We

chose the term Dyck state graph because the sequences of stack
actions along valid paths through the graph correspond to substrings in
Dyck languages. A Dyck language is a language of balanced, “colored”
parentheses. In this case, each character in the stack alphabet is a color.

ally). That is, we want to find an implementation of the function
DSG. To do so, we first phrase the Dyck state graph construction
as the least fixed point of a monotonic function. This will provide a
method (albeit an inefficient one) for computing the function DSG.
In the next section, we look at an optimized work-list driven algorithm that avoids the inefficiencies of this version.
The function F : RPDS → (DSG → DSG) generates the
monotonic iteration function we need:
F(M ) = f , where
M = (Q, Γ, δ, q0 )
f (S, Γ, E, s0 ) = (S ′ , Γ, E ′ , s0 ), where
n
o
S ′ = S ∪ s′ : s ∈ S and s 7−−→
→ s′ ∪ {s0 }
M
n g
o
g
E ′ = E ∪ s ֌ s′ : s ∈ S and s 7−−→
→ s′ .
M

Given a rooted pushdown system M , each application of the function F(M ) accretes new edges at the frontier of the Dyck state
graph. Once the algorithm reaches a fixed point, the Dyck state
graph is complete:
Theorem 7.1. DSG(M ) = lfp(F(M )).
Proof. Let M = (Q, Γ, δ, q0 ). Let f = F(M ). Observe that
lfp(f ) = f n (∅, Γ, ∅, q0 ) for some n. When N ⊆ M , then it easy
to show that f (N ) ⊆ M . Hence, DSG(M ) ⊇ lfp(F(M )).
To show DSG(M ) ⊆ lfp(F(M )), suppose this is not the case.
Then, there must be at least one edge in DSG(M ) that is not in
lfp(F(M )). Let (s, g, s′ ) be one such edge, such that the state s
is in lfp(F(M )). Let m be the lowest natural number such that s
appears in f m (M ). By the definition of f , this edge must appear in
f m+1 (M ), which means it must also appear in lfp(F(M )), which
is a contradiction. Hence, DSG(M ) ⊆ lfp(F(M )).
7.1 Complexity: Polynomial and exponential
To determine the complexity of this algorithm, we ask two questions: how many times would the algorithm invoke the iteration
function in the worst case, and how much does each invocation cost
in the worst case? The size of the final Dyck state graph bounds the
run-time of the algorithm. Suppose the final Dyck state graph has
m states. In the worst case, the iteration function adds only a single
edge each time. Since there are at most 2|Γ|m2 + m2 edges in the
final graph, the maximum number of iterations is 2|Γ|m2 + m2 .
The cost of computing each iteration is harder to bound. The
cost of determining whether to add a push edge is proportional to
the size of the stack alphabet, while the cost of determining whether
to add an ǫ-edge is constant, so the cost of determining all new push
and pop edges to add is proportional to |Γ|m + m. Determining
whether or not to add a pop edge is expensive. To add the pop edge
s ֌γ− s′ , we must prove that there exists a configuration-path to
the control state s, in which the character γ is on the top of the
stack. This reduces to a CFL-reachability query [Melski and Reps
2000] at each node, the cost of which is O(|Γ± |3 m3 ) [Kodumal
and Aiken 2004].
To summarize, in terms of the number of reachable control
states, the complexity of the most recent algorithm is:
O((2|Γ|m2 + m2 ) × (|Γ|m + m + |Γ± |3 m3 )) = O(|Γ|4 m5 ).
While this approach is polynomial in the number of reachable
control states, it is far from efficient. In the next section, we provide
an optimized version of this fixed-point algorithm that maintains a
work-list and an ǫ-closure graph to avoid spurious recomputation.

8. Efficiency: Work-lists and ǫ-closure graphs
We have developed a fixed-point formulation of the Dyck state
graph construction algorithm, but found that, in each iteration, it
wasted effort by passing over all discovered states and edges, even
though most will not contribute new states or edges. Taking a cue
from graph search, we can adapt the fixed-point algorithm with a
work-list. That is, our next algorithm will keep a work-list of new
states and edges to consider, instead of reconsidering all of them.
In each iteration, it will pull new states and edges from the work
list, insert them into the Dyck state graph and then populate the
work-list with new states and edges that have to be added as a
consequence of the recent additions.
8.1 ǫ-closure graphs
Figuring out what edges to add as a consequence of another edge
requires care, for adding an edge can have ramifications on distant
control states. Consider, for example, adding the ǫ-edge q ֌ǫ q ′
into the following graph:
q0

γ+

q′

/q

γ−

/ q1

As soon this edge drops in, an ǫ-edge “implicitly” appears between
q0 and q1 because the net stack change between them is empty; the
resulting graph looks like:
ǫ
e b _ \ Y VQ
mh


q0

γ+

/q

ǫ

/q

′

γ−

<


/ q1

where we have illustrated the implicit ǫ-edge as a dotted line.
To keep track of these implicit edges, we will construct a second graph in conjunction with the Dyck state graph: an ǫ-closure
graph. In the ǫ-closure graph, every edge indicates the existence of
a no-net-stack-change path between control states. The ǫ-closure
graph simplifies the task of figuring out which states and edges are
impacted by the addition of a new edge.
Formally, an ǫ-closure graph, is a pair Gǫ = (N, H), where N
is a set of states, and H ⊆ N × N is a set of edges. Of course, all
ǫ-closure graphs are reflexive: every node has a self loop. We use
the symbol ECG to denote the class of all ǫ-closure graphs.
We have two notations for finding ancestors and descendants of
a state in an ǫ-closure graph Gǫ = (N, H):

←
−
G ǫ [s] = s′ : (s′ , s) ∈ H
[ancestors]
 ′
→
−
′
G ǫ [s] = s : (s, s ) ∈ H
[descendants].
8.2 Integrating a work-list

Since we only want to consider new states and edges in each
iteration, we need a work-list, or in this case, two work-graphs.
A Dyck state work-graph is a pair (∆S, ∆E) in which the set ∆S
contains a set of states to add, and the set ∆E contains edges to be
added to a Dyck state graph.3 We use ∆DSG to refer to the class
of all Dyck state work-graphs.
An ǫ-closure work-graph is a set ∆H of new ǫ-edges. We use
∆ECG to refer to the class of all ǫ-closure work-graphs.
8.3 A new fixed-point iteration-space
Instead of consuming a Dyck state graph and producing a Dyck
state graph, the new fixed-point iteration function will consume and
produce a Dyck state graph, an ǫ-closure graph, a Dyck state workgraph and an ǫ-closure work graph. Hence, the iteration space of
3 Technically,

a work-graph is not an actual graph, since ∆E 6⊆ ∆S ×
Γ± × ∆S; a work-graph is just a set of nodes and a set of edges.

checks whether a new state could produce any new push edges or
no-change edges. We can represent its behavior diagrammatically:

F ′ (M ) = f , where
M = (Q, Γ, δ, q0 )
′

f (G, Gǫ , ∆G, ∆H) = (G

, G′ǫ , ∆G′ , ∆H ′

− H), where

δ

(S, Γ, E, s0 ) = G
q′

(S, H) = Gǫ
(∆S, ∆E) = ∆G
[
(∆E0 , ∆H0 ) =
sprout M (s)
(∆E1 , ∆H1 ) =

[

[

addPush M (G, Gǫ )(s, γ+ , s )
addPop M (G, Gǫ )(s, γ− , s′ )
addEmpty M (G, Gǫ )(s, s′ )

(s,ǫ,s′ )∈∆E

(∆E4 , ∆H4 ) =

[



q ′′

add edge s ֌γ+ q ′′ if it exists in δ.
′

(s,γ− ,s′ )∈∆E

(∆E3 , ∆H3 ) =



γ+
δ

add edge s ֌ǫ q ′ if it exists in δ, and
Formally:

(s,γ+ ,s′ )∈∆E

(∆E2 , ∆H2 ) =

ǫ

which means if adding control state s:

s∈∆S

[

 
 s 

addEmpty M (G, Gǫ )(s, s′ )

sprout (Q,Γ,δ) (s) = (∆E, ∆H), where

n ǫ
o  γ+
γ+
ǫ
∆E = s ֌ q : s ֌ q ∈ δ ∪ s ֌ q : s ֌ q ∈ δ
n
o
ǫ
∆H = s ֌ q : s ֌ q ∈ δ .

E ′ = E ∪ ∆E

Considering the consequences of a new push edge Once our
algorithm adds a new push edge to a Dyck state graph, there is
a chance that it will enable new pop edges for the same stack frame
somewhere downstream. If and when it does enable pops, it will
also add new edges to the ǫ-closure graph. The addPush function:

H ′ = H ∪ ∆H

addPush (Q,Γ,δ) : DSG × ECG → δ → (P (δ) × P (Q × Q)),

(s,s′ )∈∆H

S ′ = S ∪ ∆S

∆E ′ = ∆E0 ∪ ∆E1 ∪ ∆E2 ∪ ∆E3 ∪ ∆E4

∆S ′ = s′ : (s, g, s′ ) ∈ ∆E ′

checks for ǫ-reachable states that could produce a pop. We can
represent this action diagrammatically:

∆H ′ = ∆H0 ∪ ∆H1 ∪ ∆H2 ∪ ∆H3 ∪ ∆H4
′

 
 s 

′

G = (S ∪ ∆S, Γ, E , q0 )

γ+

/ 
 q 

G′ǫ = (S ′ , H ′ )
′

′

′

′

Figure 3. The fixed point of the function F ′ (M ) contains the
Dyck state graph of the rooted pushdown system M .

/ q′

γ−
δ

/ q ′′
G

ǫ
ǫ

′

∆G = (∆S − S , ∆E − E ).

ǫ
ǫ

which means if adding push-edge s ֌γ+ q:
if pop-edge q ′ ֌γ− q ′′ is in δ, then
add edge q ′ ֌γ− q ′′ , and
add ǫ-edge s ֌ q ′′ .

the new algorithm is:
IDSG = DSG × ECG × ∆DSG × ∆ECG.
(The I in IDSG stands for intermediate.)
8.4 The ǫ-closure graph work-list algorithm
The function F ′ : RPDS → (IDSG → IDSG) generates the
required iteration function (Figure 3). Please note that we implicitly
distribute union across tuples:
(X, Y ) ∪ (X ′ , Y ′ ) = (X ∪ X, Y ∪ Y ′ ).
The functions sprout , addPush, addPop, addEmpty calculate
the additional the Dyck state graph edges and ǫ-closure graph edges
(potentially) introduced by a new state or edge.
Sprouting Whenever a new state gets added to the Dyck state
graph, the algorithm must check whether that state has any new
edges to contribute. Both push edges and ǫ-edges do not depend
on the current stack, so any such edges for a state in the pushdown
system’s transition function belong in the Dyck state graph. The
sprout function:
sprout (Q,Γ,δ) : Q → (P (δ) × P (Q × Q)),

Formally:
γ+

addPush (Q,Γ,δ) (G, Gǫ )(s ֌ q) = (∆E, ∆H), where


γ−
γ−
−
→
∆E = q ′ ֌ q ′′ : q ′ ∈ G ǫ [q] and q ′ ֌ q ′′ ∈ δ


γ−
−
→
∆H = s ֌ q ′′ : q ′ ∈ G ǫ [q] and q ′ ֌ q ′′ ∈ δ .
Considering the consequences of a new pop edge Once the algorithm adds a new pop edge to a Dyck state graph, it will create at
least one new ǫ-closure graph edge and possibly more by matching
up with upstream pushes. The addPop function:
addPop (Q,Γ,δ) : DSG × ECG → δ → (P (δ) × P (Q × Q)),
checks for ǫ-reachable push-edges that could match this pop-edge.
We can represent this action diagrammatically:
s

γ+

/ s′

ǫ
ǫ

 
/ s′′
 

γ−
δ

/ 
 qI 

ǫ
ǫ

which means if adding pop-edge s′′ ֌γ− q:
if push-edge s ֌γ+ s′ is already in the Dyck state graph, then

Theorem 8.1. lfp(F ′ (M )) = (DSG(M ), Gǫ , (∅, ∅), ∅).

add ǫ-edge s ֌ q.
Formally:

Proof. The proof is similar in structure to the previous one.
′′

γ−

addPop (Q,Γ,δ) (G, Gǫ )(s ֌ q) = (∆E, ∆H), where


γ+
←
−
∆E = ∅ and ∆H = s ֌ q : s′ ∈ G ǫ [s′′ ] and s ֌ s′ ∈ G .
Considering the consequences of a new ǫ-edge Once the algorithm adds a new ǫ-closure graph edge, it may transitively have to
add more ǫ-closure graph edges, and it may connect an old push to
(perhaps newly enabled) pop edges. The addEmpty function:
addEmpty (Q,Γ,δ) :
DSG × ECG → (Q × Q) → (P (δ) × P (Q × Q)),
checks for newly enabled pops and ǫ-closure graph edges: Once
again, we can represent this action diagrammatically:
ǫ
ǫ

s

γ+

/ s′

ǫ
ǫ

ǫ
ǫ

 
/ s′′
 

  
/ s′′′



ǫ

ǫ
ǫ


/ s′′′′
G

γ−
δ

/q
O

ǫ
ǫ

8.6 Complexity: Still exponential, but more efficient
As with the previous algorithm, to determine the complexity of
this algorithm, we ask two questions: how many times would the
algorithm invoke the iteration function in the worst case, and how
much does each invocation cost in the worst case? The run-time of
the algorithm is bounded by the size of the final Dyck state graph
plus the size of the ǫ-closure graph. Suppose the final Dyck state
graph has m states. In the worst case, the iteration function adds
only a single edge each time. There are at most 2|Γ|m2 +m2 edges
in the Dyck state graph and at most m2 edges in the ǫ-closure graph,
which bounds the number of iterations.
Next, we must reason about the worst-case cost of adding an
edge: how many edges might an individual iteration consider? In
the worst case, the algorithm will consider every edge in every
iteration, leading to an asymptotic time-complexity of:
O((2|Γ|m2 + 2m2 )2 ) = O(|Γ|2 m4 ).
While still high, this is a an improvement upon the previous algorithm. For sparse Dyck state graphs, this is a reasonable algorithm.

9. Polynomial-time complexity from widening
@A

ǫ
ǫ

BC

which means if adding ǫ-edge s′′ ֌ s′′′ :
if pop-edge s′′′′ ֌γ− q is in δ, then
add ǫ-edge s ֌ q; and
add edge s′′′′ ֌γ− q;
add ǫ-edges s′ ֌ s′′′ , s′′ ֌ s′′′′ , and s′ ֌ s′′′′ .
Formally:
addEmpty (Q,Γ,δ) (G, Gǫ )(s′′ ֌ s′′′ ) = (∆E, ∆H), where
γ−

←
−
→
−
∆E = s′′′′ ֌ q : s′ ∈ G ǫ [s′′ ] and s′′′′ ∈ G ǫ [s′′′ ] and
γ+

s ֌ s′ ∈ G

←
−
→
−
∆H = s ֌ q : s′ ∈ G ǫ [s′′ ] and s′′′′ ∈ G ǫ [s′′′ ] and
γ+

s ֌ s′ ∈ G
n
o
←
−
∪ s′ ֌ s′′′ : s′ ∈ G ǫ [s′′ ]
n
o
→
−
∪ s′′ ֌ s′′′′ : s′′′′ ∈ G ǫ [s′′′ ]
n
o
←
−
→
−
∪ s′ ֌ s′′′′ : s′ ∈ G ǫ [s′′ ] and s′′′′ ∈ G ǫ [s′′′ ] .

8.5 Termination and correctness

In the previous section, we developed a more efficient fixed-point
algorithm for computing a Dyck state graph. Even with the core
improvements we made, the algorithm remained exponential in the
worst case, owing to the fact that there could be an exponential
number of reachable control states. When an abstract interpretation is intolerably complex, the standard approach for reducing
complexity and accelerating convergence is widening [Cousot and
Cousot 1977]. (Of course, widening techniques trade away some
precision to gain this speed.) It turns out that the small-step variants
of finite-state CFAs are exponential without some sort of widening
as well.
To achieve polynomial time complexity for pushdown controlflow analysis requires the same two steps as the classical case:
(1) widening the abstract interpretation to use a global, “singlethreaded” store and (2) selecting a monovariant allocation function
to collapse the abstract configuration-space. Widening eliminates a
source of exponentiality in the size of the store; monovariance eliminates a source of exponentiality from environments. In this section,
we redevelop the pushdown control-flow analysis framework with
a single-threaded store and calculate its complexity.
9.1 Step 1: Refactor the concrete semantics
First, consider defining the reachable states of the concrete semantics using fixed points. That is, let the system-space of the evaluation function be sets of configurations:
C ∈ System = P (Conf ) = P (Exp × Env × Store × Kont ).

Because the iteration function is no longer monotonic, we have to
prove that a fixed point exists. It is trivial to show that the Dyck state
graph component of the iteration-space ascends monotonically with
each application; that is:

We can redefine the concrete evaluation function:

Lemma 8.1. Given M ∈ RPDS, G ∈ DSG such that G ⊆ M , if
F ′ (M )(G, Gǫ , ∆G) = (G′ , G′ǫ , ∆G′ ), then G ⊆ G′ .

9.2 Step 2: Refactor the abstract semantics

Since the size of the Dyck state graph is bounded by the original
pushdown system M , the Dyck state graph will eventually reach a
fixed point. Once the Dyck state graph reaches a fixed point, both
work-graphs/sets will be empty, and the ǫ-closure graph will also
stabilize. We can also show that this algorithm is correct:

E (e) = lfp(fe ), where fe : System → System and

fe (C) = {I(e)} ∪ c′ : c ∈ C and c ⇒ c′ .

We can take the same approach with the abstract evaluation function, first redefining the abstract system-space:


\
\ = P Conf
Ĉ ∈ System


d × Store
\ × Kont
[ ,
= P Exp × Env

and then the abstract evaluation function:
\ → System
\ and
Ê(e) = lfp(fˆe ), where fˆe : System
n
o n
o
fˆe (Ĉ) = Î(e) ∪ ĉ′ : ĉ ∈ Ĉ and ĉ ; ĉ′ .

What we’d like to do is shrink the abstract system-space with a
refactoring that corresponds to a widening.
9.3 Step 3: Single-thread the abstract store

We can approximate a set of abstract stores {σ̂1 , . . . , σ̂n } with
the least-upper-bound of those stores: σ̂1 ⊔ · · · ⊔ σ̂n . We can
exploit this by creating a new abstract system space in which the
store is factored out of every configuration. Thus, the system-space
contains a set of partial configurations and a single global store:


′
\ × Store
\
\ = P PConf
System
d × Kont
\ = Exp × Env
[.
π̂ ∈ PConf

With a monovariant allocation scheme that eliminates abstract environments, the number of iterations ultimately reduces to:
|Exp| × (2|d
Var| + 1) × |Exp| + |Var| × |Lam|,

which means that, in the worst case, the algorithm makes a cubic
number of iterations with respect to the size of the input program.4
The worst-case cost of the each iteration would be dominated
by a CFL-reachability calculation, which, in the worst case, must
consider every state and every edge:
O(|Var|3 × |Exp|3 ).

Thus, each iteration takes O(n6 ) and there are a maximum of
O(n3 ) iterations, where n is the size of the program. So,total
complexity would be O(n9 ) for a monovariant pushdown controlflow analysis with this scheme, where n is again the size of the
program. Although this algorithm is polynomial-time, we can do
better.
9.5 Step 5: Reintroduce ǫ-closure graphs

We can factor the store out of the abstract transition relation as well,
\ × (PConf
\ × Store
\):
so that (_σ̂ ) ⊆ PConf
σ̂

(e, ρ̂, κ̂) _ ((e′ , ρ̂′ , κ̂′ ), σ̂ ′ ) iff (e, ρ̂, σ̂, κ̂) ; (e′ , ρ̂′ , σ̂ ′ , κ̂′ ),
′

′

\ → System
\ ,
which gives us a new iteration function, fˆe′ : System
fˆe′ (P̂ , σ̂) = (P̂ ′ , σ̂ ′ ), where


σ̂
′
′
′
′′
P̂ = π̂ : π̂ _ (π̂ , σ̂ ) ∪ {π̂0 }

G  ′′
σ̂
σ̂ ′ =
σ̂ : π̂ _ (π̂ ′ , σ̂ ′′ )
(π̂0 , hi) = Î(e).

Replicating the evolution from Section 8 for this store-widened
analysis, we arrive at a more efficient polynomial-time analysis.
An ǫ-closure graph in this setting is a set of pairs of store-less,
continuation-less partial states:


\ × PState
\ .
[ = P PState
ECG

Then, we can set the system space to include ǫ-closure graphs:
\
System

′′′

[ × ECG
[ × Store.
\
= DSG

Before we redefine the iteration function, we need another factored transition relation. The stack- and action-factored transition
\ × PState
\ × Store determines if a tranrelation (⇁σ̂g ) ⊆ PState
sition is possible under the specified store and stack-action:
σ̂

(e, ρ̂) ⇁ ((e′ , ρ̂′ ), σ̂ ′ ) iff (e, ρ̂, σ̂, κ̂) ; (e′ , ρ̂′ , σ̂ ′ , φ̂ : κ̂′ )

9.4 Step 4: Dyck state control-flow graphs

φ̂+

Following the earlier Dyck state graph reformulation of the pushdown system, we can reformulate the set of partial configurations as
a Dyck state control-flow graph. A Dyck state control-flow graph
is a frame-action-labeled graph over partial control states, and a
partial control state is an expression paired with an environment:
′′

\ = DSCFG
\ × Store
\
System
\ = P(PState)
\ × P(PState
\ × Frame
\ ± × PState)
\
DSCFG
d.
\ = Exp × Env
ψ̂ ∈ PState

In a Dyck state control-flow graph, the partial control states are
partial configurations which have dropped the continuation component; the continuations are encoded as paths through the graph.
If we wanted to do so, we could define a new monotonic iteration function analogous to the simple fixed-point formulation of
Section 7:
′′
′′
\ → System
\ ,
fˆe : System
again using CFL-reachability to add pop edges at each step.
A preliminary analysis of complexity Even without defining the
system-space iteration function, we can ask, How many iterations
will it take to reach a fixed point in the worst case? This question
is really asking, How many edges can we add? And, How many
entries are there in the store? Summing these together, we arrive at
the worst-case number of iterations:
DSCFG edges

store entries

}|
{
}|
{ z
z
d .
[ | × |Clo|
\ | × |Frame
\ ± | × |PState
\ | + |Addr
|PState

σ̂

(e, ρ̂) ⇁ ((e′ , ρ̂′ ), σ̂ ′ ) iff (e, ρ̂, σ̂, φ̂ : κ̂) ; (e′ , ρ̂′ , σ̂ ′ , κ̂′ )
φ̂−
σ̂

(e, ρ̂) ⇁ ((e′ , ρ̂′ ), σ̂ ′ ) iff (e, ρ̂, σ̂, κ̂) ; (e′ , ρ̂′ , σ̂ ′ , κ̂′ ).
ǫ

Now, we can redefine the iteration function (Figure 4).
Theorem 9.1. Pushdown 0CFA can be computed in O(n6 )-time,
where n is the size of the program.
Proof. As before, the maximum number of iterations is cubic in
the size of the program for a monovariant analysis. Fortunately, the
cost of each iteration is also now bounded by the number of edges
in the graph, which is also cubic.

10. Applications
Pushdown control-flow analysis offers more precise control-flow
analysis results than the classical finite-state CFAs. Consequently,
pushdown control-flow analysis improves flow-driven optimizations (e.g., constant propagation, global register allocation, inlining [Shivers 1991]) by eliminating more of the false positives that
block their application.
The more compelling applications of pushdown control-flow
analysis are those which are difficult to drive with classical controlflow analysis. Perhaps not surprisingly, the best examples of such
4 In computing the number of frames, we note that in every continuation,
the variable and the expression uniquely determine each other based on
the let-expression from which they both came. As a result, the number of
abstract frames available in a monovariant analysis is bounded by both the
\ = |Var|.
number of variables and the number of expressions, i.e., |Frame|

fˆ((P̂ , Ê), Ĥ, σ̂) = ((P̂ ′ , Ê ′ ), Ĥ ′ , σ̂ ′′ ), where
T̂+ =

(

φ̂+

σ̂

(ψ̂ ֌ ψ̂ ′ , σ̂ ′ ) : ψ̂ ⇁ (ψ̂ ′ , σ̂ ′ )
φ̂+

)

n
o
ǫ
σ̂
T̂ǫ = (ψ̂ ֌ ψ̂ ′ , σ̂ ′ ) : ψ̂ ⇁ (ψ̂ ′ , σ̂ ′ )
ǫ

φ̂−

σ̂
T̂− = (ψ̂ ′′ ֌ ψ̂ ′′′ , σ̂ ′ ) : ψ̂ ′′ ⇁ (ψ̂ ′′′ , σ̂ ′ ) and
φ̂−

φ̂+

′

ψ̂ ֌ ψ̂ ∈ Ê and
ψ̂ ′ ֌ ψ̂ ′′ ∈ Ĥ
T̂ ′ = T̂+ ∪ T̂ǫ ∪ T̂−
n
o
Ê ′ = ê : (ê, ) ∈ T̂ ′
o
Gn ′
σ̂ ′′ =
σ̂ : ( , σ̂ ′ ) ∈ T̂ ′
n
o
Ĥǫ = ψ̂ ֌ ψ̂ ′′ : ψ̂ ֌ ψ̂ ′ ∈ Ĥ and ψ̂ ′ ֌ ψ̂ ′′ ∈ Ĥ

φ̂+

Ĥ+− = ψ̂ ֌ ψ̂ ′′′ : ψ̂ ֌ ψ̂ ′ ∈ Ê and ψ̂ ′ ֌ ψ̂ ′′ ∈ Ĥ
φ̂−

and ψ̂ ′′ ֌ ψ̂ ′′′ ∈ Ê

Ĥ ′ = Ĥǫ ∪ Ĥ+−
n
o
g
P̂ ′ = P̂ ∪ ψ̂ ′ : ψ̂ ֌ ψ̂ ′ .
Figure 4. An ǫ-closure graph-powered iteration function for pushdown control-flow analysis with a single-threaded store.
analyses are escape analysis and interprocedural dependence analysis. Both of these analyses are limited by a static analyzer’s ability to reason about the stack, the core competency of pushdown
control-flow analysis. (We leave an in-depth formulation and study
of these analyses to future work.)
10.1 Escape analysis
In escape analysis, the objective is to determine whether a heapallocated object is safely convertible into a stack-allocated object.
In other words, the compiler is trying to figure out whether the
frame in which an object is allocated outlasts the object itself. In
higher-order languages, closures are candidates for escape analysis.
Determining whether all closures over a particular λ-term lam
may be heap-allocated is straightforward: find the control states in
the Dyck state graph in which closures over lam are being created,
then find all control states reachable from these states over only ǫedge and push-edge transitions. Call this set of control states the
“safe” set. Now find all control states which are invoking a closure
over lam. If any of these control states lies outside of the safe set,
then stack-allocation may not be safe; if, however, all invocations
lie within the safe set, then stack-allocation of the closure is safe.
10.2 Interprocedural dependence analysis
In interprocedural dependence analysis, the goal is to determine, for
each λ-term, the set of resources which it may read or write when
it is called. Might and Prabhu showed that if one has knowledge
of the program stack, then one can uncover interprocedural dependencies [Might and Prabhu 2009]. We can adapt that technique to
work with Dyck state graphs. For each control state, find the set
of reachable control states along only ǫ-edges and pop-edges. The

frames on the pop-edges determine the frames which could have
been on the stack when in the control state. The frames that are live
on the stack determine the procedures that are live on the stack. Every procedure that is live on the stack has a read-dependence on any
resource being read in the control state, while every procedure that
is live on the stack also has a write-dependence on any resource being written in the control state. This logic is the direct complement
of “if f calls g and g accesses a, then f also accesses a.”

11. Related work
Pushdown control-flow analysis draws on work in higher-order
control-flow analysis [Shivers 1991], abstract machines [Felleisen
and Friedman 1987] and abstract interpretation [Cousot and Cousot
1977].
Context-free analysis of higher-order programs The closest related work for this is Vardoulakis and Shivers very recent work
on CFA2 [Vardoulakis and Shivers 2010]. CFA2 is a table-driven
summarization algorithm that exploits the balanced nature of calls
and returns to improve return-flow precision in a control-flow analysis. Though CFA2 alludes to exploiting context-free languages,
context-free languages are not explicit in its formulation in the
same way that pushdown systems are in pushdown control-flow
analysis. With respect to CFA2, pushdown control-flow analysis is
polyvariant, covers direct-style, and the monovariant instatiation is
lower in complexity (CFA2 is exponential-time).
On the other hand, CFA2 distinguishes stack-allocated and
store-allocated variable bindings, whereas our formulation of pushdown control-flow analysis does not and allocates all bindings in
the store. If CFA2 determines a binding can be allocated on the
stack, that binding will enjoy added precision during the analysis
and is not subject to merging like store-allocated bindings.
Calculation approach to abstract interpretation Midtgaard and
Jensen [2009] systematically calculate 0CFA using the CousotCousot-style calculational approach [1999] to abstract interpretation applied to an ANF λ-calculus. Like the present work, Midtgaard and Jensen start with the CESK machine of Flanagan et al.
[1993] and employ a reachable-states model. The analysis is then
constructed by composing well-known Galois connections to reveal a 0CFA incorporating reachability. The abstract semantics approximate the control stack component of the machine by its top
element. The authors remark monomorphism materializes in two
mappings: “one mapping all bindings to the same variable,” the
other “merging all calling contexts of the same function.” Essentially, the pushdown 0CFA of Section 4 corresponds to Midtgaard
and Jensen’s analsysis when the latter mapping is omitted and the
stack component of the machine is not abstracted.
CFL- and pushdown-reachability techniques This work also
draws on CFL- and pushdown-reachability analysis [Bouajjani
et al. 1997, Kodumal and Aiken 2004, Reps 1998, Reps et al. 2005].
For instance, ǫ-closure graphs, or equivalent variants thereof, appear in many context-free-language and pushdown reachability algorithms. For the less efficient versions of our analyses, we implicitly invoked these methods as subroutines. When we found these
algorithms lacking (as with their enumeration of control states), we
developed Dyck state graph construction.
CFL-reachability techniques have also been used to compute
classical finite-state abstraction CFAs [Melski and Reps 2000]
and type-based polymorphic control-flow analysis [Rehof and
Fähndrich 2001]. These analyses should not be confused with
pushdown control-flow analysis, which is computing a fundamentally more precise kind of CFA. Moreover, Rehof and Fahndrich’s
method is cubic in the size of the typed program, but the types may

be exponential in the size of the program. In addition, our technique
is not restricted to typed programs.
Model-checking higher-order recursion schemes There is terminology overlap with work by Kobayashi [2009] on modelchecking higher-order programs with higher-order recursion schemes,
which are a generalization of context-free grammars in which
productions can take higher-order arguments, so that an order0 scheme is a context-free grammar. Kobyashi exploits a result by Ong [2006] which shows that model-checking these recursion schemes is decidable (but ELEMENTARY-complete) by
transforming higher-order programs into higher-order recursion
schemes. Given the generality of model-checking, Kobayashi’s
technique may be considered an alternate paradigm for the analysis
of higher-order programs. For the case of order-0, both Kobayashi’s
technique and our own involve context-free languages, though ours
is for control-flow analysis and his is for model-checking with respect to a temporal logic. After these surface similarities, the techniques diverge. Moreover, there does not seem to be a polynomialtime variant of Kobyashi’s method.
Other escape and dependence analyses We presented escape and
dependence analyses to prove a point: that pushdown control-flow
analysis is more powerful than classical control-flow analysis, in
the sense that it can answer different kinds of questions. We have
not yet compared our analyses with the myriad escape and dependence analyses (e.g., [Blanchet 1998]) that exist in the literature,
though we do expect that, with their increased precision, our analyses will be strongly competitive.

12. Conclusion
Pushdown control-flow analysis is an alternative paradigm for
the analysis of higher-order programs. By modeling the run-time
program stack with the stack of a pushdown system, pushdown
control-flow analysis precisely matches returns to their calls. We
derived pushdown control-flow analysis as an abstract interpretation of a CESK machine in which its stack component is left
unbounded. As this abstract interpretation ranged over an infinite state-space, we sought a decidable method for determining
th reachable states. We found one by converting the abstracted
CESK into a PDA that recognized the language of legal controlstate sequences. By intersecting this language with a specific regular language and checking non-emptiness, we were able to answer
control-flow questions. From the PDA formulation, we refined the
technique to reduce complexity from doubly exponential, to bestcase exponential, to worst-case exponential, to polynomial. We
ended with an efficient, polyvariant and precise framework.
Future work Pushdown control-flow analysis exploits the fact
that clients of static analyzers often need information about control
states rather than stacks. Should clients require information about
complete configurations—control states plus stacks—our analysis is lacking. Our framework represents configurations as paths
through Dyck state graphs. Its results can provide a regular description of the stack, but at a cost proportional to the size of the
graph. For a client like abstract garbage collection, which would
pay this cost for every edge added to the graph, this cost is unacceptable. Our future work will examine how to incrementally summarize stacks paired with each control state during the analysis.
Acknowledgements We thank Dimitrios Vardoulakis for comments and discussions, and reviewers of ICFP and this workshop.

References
Bruno Blanchet. Escape analysis: Correctness proof, implementation and
experimental results. In POPL ’98: Proceedings of the 25th ACM

SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 25–37. ACM, 1998.
Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis
of pushdown automata: Application to model-checking. In CONCUR
’97: Proceedings of the 8th International Conference on Concurrency
Theory, pages 135–150. Springer-Verlag, 1997.
Patrick Cousot. The calculational design of a generic abstract interpreter.
In M. Broy and R. Steinbrüggen, editors, Calculational System Design.
NATO ASI Series F. IOS Press, Amsterdam, 1999.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice
model for static analysis of programs by construction or approximation
of fixpoints. In Conference Record of the Fourth ACM Symposium on
Principles of Programming Languages, pages 238–252. ACM Press,
1977.
Matthias Felleisen and Daniel P. Friedman. A calculus for assignments
in higher-order languages. In POPL ’87: Proceedings of the 14th
ACM SIGACT-SIGPLAN Symposium on Principles of Programming
Languages, pages 314+. ACM, 1987.
Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The
essence of compiling with continuations. In PLDI ’93: Proceedings of
the ACM SIGPLAN 1993 Conference on Programming Language Design
and Implementation, pages 237–247. ACM, June 1993.
Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL ’09: Proceedings of the 36th
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 416–428. ACM, 2009.
John Kodumal and Alex Aiken. The set constraint/CFL reachability connection in practice. In PLDI ’04: Proceedings of the ACM SIGPLAN
2004 conference on Programming language design and implementation,
pages 207–218. ACM, 2004.
David Melski and Thomas W. Reps. Interconvertibility of a class of set constraints and context-free-language reachability. Theoretical Computer
Science, 248(1-2):29–98, October 2000.
Jan Midtgaard and Thomas P. Jensen. Control-flow analysis of function
calls and returns by abstract interpretation. In ICFP ’09: Proceedings
of the 14th ACM SIGPLAN International Conference on Functional
Programming, pages 287–298. ACM, 2009.
Matthew Might. Environment Analysis of Higher-Order Languages. PhD
thesis, Georgia Institute of Technology, June 2007.
Matthew Might and Tarun Prabhu. Interprocedural dependence analysis of
higher-order programs via stack reachability. In Proceedings of the 2009
Workshop on Scheme and Functional Programming, 2009.
C. H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21st Annual IEEE Symposium on Logic in Computer
Science (LICS’06), pages 81–90. IEEE, 2006.
Jakob Rehof and Manuel Fähndrich. Type-based flow analysis: From polymorphic subtyping to CFL-reachability. In POPL ’01: Proceedings of
the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 54–66. ACM, 2001.
Thomas Reps. Program analysis via graph reachability. Information and
Software Technology, 40(11-12):701–726, December 1998.
Thomas Reps, Stefan Schwoon, Somesh Jha, and David Melski. Weighted
pushdown systems and their application to interprocedural dataflow
analysis. Science of Computer Programming, 58(1-2):206–263, 2005.
Olin G. Shivers. Control-Flow Analysis of Higher-Order Languages. PhD
thesis, Carnegie Mellon University, 1991.
Michael Sipser. Introduction to the Theory of Computation. Course
Technology, 2 edition, February 2005.
David Van Horn and Matthew Might. Abstracting abstract machines.
In ICFP ’10: Proceedings of the 15th ACM SIGPLAN International
Conference on Functional Programming. ACM, September 2010.
Dimitrios Vardoulakis and Olin Shivers. CFA2: a Context-Free Approach
to Control-Flow Analysis. In European Symposium on Programming
(ESOP), volume 6012 of LNCS, pages 570–589. Springer, 2010.

