ZU064-05-FPR

paper-jfp

6 February 2018

3:38

Under consideration for publication in J. Functional Programming

1

arXiv:1406.5106v1 [] 19 Jun 2014

Pushdown flow analysis with abstract garbage
collection
J. IAN JOHNSON
Northeastern University
ILYA SERGEY
IMDEA Software Institute
CHRISTOPHER EARL
University of Utah
MATTHEW MIGHT
University of Utah
DAVID VAN HORN
University of Maryland

Abstract

In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection
push the boundaries of what we can learn about programs statically. This work illuminates and poses
solutions to theoretical and practical challenges that stand in the way of combining the power of these
techniques. Pushdown flow analysis grants unbounded yet computable polyvariance to the analysis
of return-flow in higher-order programs. Abstract garbage collection grants unbounded polyvariance
to abstract addresses which become unreachable between invocations of the abstract contexts in
which they were created. Pushdown analysis solves the problem of precisely analyzing recursion in
higher-order languages; abstract garbage collection is essential in solving the “stickiness” problem.
Alone, our benchmarks demonstrate that each method can reduce analysis times and boost precision
by orders of magnitude.
We combine these methods. The challenge in marrying these techniques is not subtle: computing
the reachable control states of a pushdown system relies on limiting access during transition to the
top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to
compute a root set, just as concrete collection does. Conditional pushdown systems were developed
for just such a conundrum, but existing methods are ill-suited for the dynamic nature of garbage
collection.
We show fully precise and approximate solutions to the feasible paths problem for pushdown
garbage-collecting control-flow analysis. Experiments reveal synergistic interplay between garbage
collection and pushdown techniques, and the fusion demonstrates “better-than-both-worlds” precision.

ZU064-05-FPR

paper-jfp

2

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

(define (id x) x)
(define (f n)
(cond [(<= n 1)
[else

1]
(* n (f (- n 1)))]))

(define (g n)
(cond [(<= n 1)
[else

1]
(+ (* n n) (g (- n 1)))]))

(print (+ ((id f) 3) ((id g) 4)))

Fig. 1: A small example to illuminate the strengths and weaknesses of both pushdown
analysis and abstract garbage collection.

1 Introduction
The development of a context-free1 approach to control-flow analysis (CFA2) by Vardoulakis and Shivers (2010) provoked a shift in the static analysis of higher-order programs. Prior to CFA2, a precise analysis of recursive behavior had been a challenge—even
though flow analyses have an important role to play in optimization for functional languages, such as flow-driven inlining (Might and Shivers 2006a), interprocedural constant
propagation (Shivers 1991) and type-check elimination (Wright and Jagannathan 1998).
While it had been possible to statically analyze recursion soundly, CFA2 made it possible
to analyze recursion precisely by matching calls and returns without approximating the
stack as k-CFA does. The approximation is only in the binding structure, and not the control
structure of the program. In its pursuit of recursion, clever engineering steered CFA2 to
a theoretically intractable complexity, though in practice it performs well. Its payoff is
significant reductions in analysis time as a result of corresponding increases in precision.
For a visual measure of the impact, Figure 2 renders the abstract transition graph (a
model of all possible traces through the program) for the toy program in Figure 1. For this
example, pushdown analysis eliminates spurious return-flow from the use of recursion. But,
recursion is just one problem of many for flow analysis. For instance, pushdown analysis
still gets tripped up by the spurious cross-flow problem; at calls to (id f) and (id g) in
the previous example, it thinks (id g) could be f or g. CFA2 is not confused in this due
to its precise stack frames, but can be confused by unreachable heap-allocated bindings.
Powerful techniques such as abstract garbage collection (Might and Shivers 2006b) were
developed to address the cross-flow problem (here in a way complementary to CFA2’s
stack frames). The cross-flow problem arises because monotonicity prevents revoking a
judgment like “procedure f flows to x,” or “procedure g flows to x,” once it’s been made.

1

As in context-free language, not a context-insensitive analysis.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

3

398
250
76

401

607

344

100

369

414

54

304

287
350

218

407

360

453
133
150

79

647

45

47

300

103

186

508

635

382

377

562

495

433

346
58

267

310
122

138

392

145

560

273

329

499

163

340
482

90

406

615

447

68

245

484
596

28
35

338

628

175

631
408

581
332
48

586

40

569

25

526

254

496

306

480

253

603

271

176

233

216

371

529
439

405

213
53

98
134

400

390

200

509

627
217

142

610

410

555

74

244

327

208

240

549

374

432

566

351

320

323

189

541

72

540

474
352

363

42

278

417

430

147

459
489

110

165

367

85

302

498

152

514

305

373

117

201

313

265

99

595

234

604

516

316

443

416
94

5

10

18
543

177

641

112

570

241

551
275

146

512

299

559

645

281

486
108

246

1

17

121

101
455
397

527

450

16

501

442

257
404

523

222

29

599
524

578

162

141

183

235

106

465

358

425
381

114
609

36
468

343

359

477

620
118

418

8

411

536

161

533

178

312

308

435

545

553

283

212

303

84
11

368

438

120

574

629
269

193
479

298

485

567

552

136

614

573

585

347
571
650

255

6

292

554

587

184

215

296

575
148

111

196

317

105

181

621

471
249

355
135

230

137

214

339

258

159

78

606

630

589

409
648

561
440

594

331

263

535

59

451
309

353
539

153

113

444

31
481
372
92
365

494

598

396
488

619
584

556

104

262

341

590

144

274

280

210

384

168
179

272
37

426

89

593

314

95

649

9

515
402

518

46

119

534

276

356

232

446
39

399

15
470

64
483

259

67
191

502

82

558

140

592

188

487

223

293

131

531
572
225
419

463

33

307

23

199

375
57

12

333

457

335

125

167

154

107

319

361

182
14
321
203
616

66

424

376

532

591
88

205
221

170

624

530
83

506
362

456

563

568

420

537

348

580

441
513

602

458
517

421

285

452

336

622

102

252

123

172

242

493
43

600

227

207

391

194

130

427

4

27

55

236

507
143

370

185
237
467
431

260
318
180

224
187

87
290

73

129

546

38

155

49

284

34
202

192

608

190

434

206

415

448

195

636

50

550

460

156

633

476

466

383

2

77
472

63

21

229
605

289

646

115

65

548

547

7

510

387

132

62

149

75

286

139
228

324

625

454
357

279

251

174

490

97

116
429

634

395
579

577
126

297

198

542

60

330

128

612
231

93
52

393

473

642

389

294

436
295
412
475

51

626

525

157

30

582

328

564

337

91

462

504
56

311

261

644

322

70

96

69

379

597

449

611

437

342

288

538

617

544

380

268

211

623

291

325
301

209

428
26
557
423

601
264

413

22

497

588
20

520

19

13
491

500

528

86

511

386
394

226

3

173

81

197

632
613

366

469

270

505

640

326

204

239

583

464

354

219

461

521

277

315

109
24

522

124

334

248
61

639

345
637

71

403

618
638
422

151
385
643

576

32
378

364

349

164

243

565
256

445

80

44

158

282

492

220

388

160

238

127
503

41
519

247

171

166

266

478
169

(1) without pushdown analysis or abstract GC: 653 states
85
60
16

123

110

48

100

50

84

70

94

119

42

59
112
7
43
67

96

105

80

64

4
102

109

69

76

47

18

20

66

82

92

88

65

133

115

56

54

136

45

121

1

74

22

120

78

40

128

57

124

134

19

97

68

55

95

28

93

98

8

139

49

73
26
135

63

17

75

113

13

32

108

11

99

104

36
10

116

3
27

114

77
101

23
2

106

90

33
87

118

107

12

62

9

51

132

15
91

37
81

52
21

5

111

130

29

125

53

83

41

103

14

38

126

58

25

129

31

89

86

72

61

79

39

137

131
24
117

6

71

46

35

138

44

122
30
34
127

(2) with pushdown only: 139 states
3

84

50

94

21

19

102

10

36

55

28

65

74

34

97

98

13

44

24

43

104

72

70

100

1

48

85

78
82

41

103

47

12

18

11

8

15

64

40

52

73

53

58

45

93

81

96

79

105

87

16

59

61

20

60

62

17

88
71

6
99

5

57
83

63

49

7

26

38

32

80

14

66

42

86

69
101

22

35

33

27

54

76
4

67

37

75

89

77

29

9

51

31

46

92

2

25

23

56

91

39

68
90

30

95

(3) with GC only: 105 states
31
26

64

8

47

56

75

24
68

50
28

73

19

15

34

14

63

76

32

20

57

16

38

41

59

52

33
49

3

58

74

12
9

10

39

42

22

5

7

36

48

54

51

35

72

66

44

46

6

43

70

65

18

53

2

11

23

40

77

37

62

29

17

13

61

27

45

69

60

55

4

30

67

25

21
1

71

(4) with pushdown analysis and abstract GC: 77 states

Fig. 2: We generated an abstract transition graph for the same program from Figure 1 four
times: (1) without pushdown analysis or abstract garbage collection; (2) with only abstract
garbage collection; (3) with only pushdown analysis; (4) with both pushdown analysis and
abstract garbage collection. With only pushdown or abstract GC, the abstract transition
graph shrinks by an order of magnitude, but in different ways. The pushdown-only analysis
is confused by variables that are bound to several different higher-order functions, but
for short durations. The abstract-GC-only is confused by non-tail-recursive loop structure.
With both techniques enabled, the graph shrinks by nearly half yet again and fully recovers
the control structure of the original program.

ZU064-05-FPR

paper-jfp

4

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

In fact, abstract garbage collection, by itself, also delivers significant improvements to
analytic speed and precision in many benchmarks. (See Figure 2 again for a visualization
of that impact.)
It is natural to ask: can abstract garbage collection and pushdown analysis work together? Can their strengths be multiplied? At first, the answer appears to be a disheartening “No.”
1.1 The problem: The whole stack versus just the top
Abstract garbage collection seems to require more than pushdown analysis can decidably
provide: access to the full stack. Abstract garbage collection, like its name implies, discards unreachable values from an abstract store during the analysis. Like concrete garbage
collection, abstract garbage collection also begins its sweep with a root set, and like concrete garbage collection, it must traverse the abstract stack to compute that root set. But,
pushdown systems are restricted to viewing the top of the stack (or a bounded depth)—a
condition violated by this traversal.
Fortunately, abstract garbage collection does not need to arbitrarily modify the stack. It
only needs to know the root set of addresses in the stack. This kind of system has been
studied before in the context of compilers that build a symbol table (a so-called “oneway stack automaton” (Ginsburg et al. 1967)),in the context of first-order model-checking
(pushdown systems with checkpoints (Esparza et al. 2003)),and also in the context of
points-to analysis for Java (conditional weighted pushdown systems (CWPDS) (Li and
Ogawa 2010)). We borrow the definition of (unweighted) conditional pushdown system
(CPDS) in this work, though our analysis does not take CPDSs as inputs.
Higher-order flow analyses typically do not take a control-flow graph, or similar preabstracted object, as input and produce an annotated graph as output. Instead, they take a
program as input and “run it on all possible inputs” (abstractly) to build an approximation
of the language’s reduction relation (semantics), specialized to the given program. This
semantics may be non-standard in such a way that extra-semantic information might be
accumulated for later analyses’ consumption. The important distinction between higherorder and first-order analyses is that the model to analyze is built during the analysis,
which involves interpreting the program (abstractly).
When a language’s semantics treats the control stack as an actual stack, i.e., it does not
have features such as first-class continuations, an interpreter can be split into two parts: a
function that takes the current state and returns all next states along with a pushed activation
frame or a marker that the stack is unchanged; and a function that takes the current state, a
possible “top frame” of the stack, and returns the next states after popping this frame. This
separation is crucial for an effective algorithm, since pushed frames are understood from
program text, and popped frames need only be enumerated from a (usually small) set that
we compute along the way.
Control-state reachability for the straightforward formulation of stack introspection ends
up being uncomputable. Conditional pushdown systems introduce a relatively weak regularity constraint on transitions’ introspection: a CPDS may match the current stack against
a choice of finitely many regular languages of stacks in order to transition from one state to
the next along with the stack action. The general solutions to feasible paths in conditional

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

5

pushdown systems enumerate all languages of stacks that a transition may be conditioned
on. This strategy is a non-starter for garbage collection, since we delineate stacks by the
addresses they keep live; this is exponential in the number of addresses. The abstraction
step that finitizes the address space is what makes the problem fall within the realm of
CPDSs, even if the target is so big it barely fits. But abstract garbage collection is special
— we can compute which languages of stacks we need to check against, given the current
state of the analysis. It is therefore possible to fuse the full benefits of abstract garbage
collection with pushdown analysis. The dramatic reduction in abstract transition graph
size from the top to the bottom in Figure 2 (and echoed by later benchmarks) conveys the
impact of this fusion.
Secondary motivations There are four secondary motivations for this work:
1.
2.
3.
4.

bringing context-sensitivity to pushdown analysis;
exposing the context-freedom of the analysis;
enabling pushdown analysis without continuation-passing style; and
defining an alternative algorithm for computing pushdown analysis, introspectively
or otherwise.

In CFA2, monovariant (0CFA-like) context-sensitivity is etched directly into the abstract
“local” semantics, which is in turn phrased in terms of an explicit (imperative) summarization algorithm for a partitioned continuation-passing style. Our development exposes
the classical parameters (exposed as allocation functions in a semantics) that allow one to
tune the context-sensitivity and polyvariance (accomplishing (1)), thanks to the semantics
of the analysys formulated in the form of an “abstracted abstract machine” (Van Horn and
Might 2012).
In addition, the context-freedom of CFA2 is buried implicitly inside an imperative summarization algorithm. No pushdown system or context-free grammar is explicitly identified. Thus, a motivating factor for our work was to make the pushdown system in CFA2
explicit, and to make the control-state reachability algorithm purely functional (accomplishing (2)).
A third motivation was to show that a transformation to continuation-passing style is
unnecessary for pushdown analysis. In fact, pushdown analysis is arguably more natural
over direct-style programs. By abstracting all machine components except for the program
stack, it converts naturally and readily into a pushdown system (accomplishing (3)). In
his dissertation, Vardoulakis showed a direct-style version of CFA2 that exploits the metalanguage’s runtime stack to get precise call-return matching. The approach is promising,
but its correctness remains unproven, and it does not apply to generic pushdown systems.
Finally, to bring much-needed clarity to algorithmic formulation of pushdown analysis,
we have included an appendix containing a reference implementation in Haskell (accomplishing (4)). We have kept the code as close in form to the mathematics as possible, so
that where concessions are made to the implementation, they are obvious.
1.2 Overview
We first review preliminaries to set a consistent feel for terminology and notation, particularly with respect to pushdown systems. The derivation of the analysis begins with a con-

ZU064-05-FPR

paper-jfp

6

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

crete CESK-machine-style semantics for A-Normal Form λ -calculus. The next step is an
infinite-state abstract interpretation, constructed by bounding the C(ontrol), E(nvironment)
and S(tore) portions of the machine. Uncharacteristically, we leave the stack component—
the K(ontinuation)—unbounded.
A shift in perspective reveals that this abstract interpretation is a pushdown system.
We encode it as a pushdown automaton explicitly, and pose control state reachability as
a decidable language intersection problem. We then extract a rooted pushdown system
from the pushdown automaton. For completeness, we fully develop pushdown analysis for
higher-order programs, including an efficient algorithm for computing reachable control
states. We go further by characterizing complexity and demonstrating the approximations
necessary to get to a polynomial-time algorithm.
We then introduce abstract garbage collection and quickly find that it violates the pushdown model with its traversals of the stack. To prove the decidability of control-state
reachability, we formulate introspective pushdown systems, and recast abstract garbage
collection within this framework. We then review that control-state reachability is decidable for introspective pushdown systems as well when subjected to a straightforward
regularity constraint.
We conclude with an implementation and empirical evaluation that shows strong synergies between pushdown analysis and abstract garbage collection, including significant
reductions in the size of the abstract state transition graph.
1.3 Contributions
We make the following contributions:
1. Our primary contribution is an online decision procedure for reachability in introspective pushdown systems, with a more efficient specialization to abstract garbage
collection.
2. We show that classical notions of context-sensitivity, such as k-CFA and poly/CFA,
have direct generalizations in a pushdown setting. CFA2 was presented as a monovariant analysis,2 whereas we show polyvariance is a natural extension.
3. We make the context-free aspect of CFA2 explicit: we clearly define and identify
the pushdown system. We do so by starting with a classical CESK machine and
systematically abstracting until a pushdown system emerges. We also remove the orthogonal frame-local-bindings aspect of CFA2, so as to focus solely on the pushdown
nature of the analysis.
4. (*) We remove the requirement for a global CPS-conversion by synthesizing the
analysis directly for direct-style (in the form of A-normal form lambda-calculus —
a local transformation).
5. We empirically validate claims of improved precision on a suite of benchmarks.
We find synergies between pushdown analysis and abstract garbage collection that
makes the whole greater that the sum of its parts.
2

Monovariance refers to an abstraction that groups all bindings to the same variable together: there
is one abstract variant for all bindings to each variable.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

7

6. We provide a mirror of the major formal development as working Haskell code in the
appendix. This code illuminates dark corners of pushdown analysis and it provides a
concise formal reference implementation.
(*) The CPS requirement distracts from the connection between continuations and stacks.
We do not discuss call/cc in detail, since we believe there are no significant barriers to
adapting the techniques of Vardoulakis and Shivers (2011) to the direct-style setting, given
related work in Johnson and Van Horn (2013). Languages with exceptions fit within the
pushdown model since a throw can be modeled as “pop until first catch.”
2 Pushdown Preliminaries
The literature contains many equivalent definitions of pushdown machines, so we adapt
our own definitions from Sipser (2005). Readers familiar with pushdown theory may wish
to skip ahead.
2.1 Syntactic sugar
When a triple (x, `, x0 ) is an edge in a labeled graph:
`

x  x0 ≡ (x, `, x0 ).
Similarly, when a pair (x, x0 ) is a graph edge:
x  x0 ≡ (x, x0 ).
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 Γ. To reason about stack manipulation concisely, we first 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 γ+ ; a pop character γ− ; and a no-stack-change indicator, ε:
g ∈ Γ± ::= ε

[stack unchanged]

| γ+ for each γ ∈ Γ

[pushed γ]

| γ− for each γ ∈ Γ

[popped γ].

In this paper, the symbol g represents some stack action.
When we develop introspective pushdown systems, we are going to need formalisms
for easily manipulating stack-action strings and stacks. Given a string of stack actions, we
can compact it into a minimal string describing net stack change. We do so through the
operator b·c : Γ∗± → Γ∗± , which cancels out opposing adjacent push-pop stack actions:
b~g γ+ γ− ~g 0 c = b~g ~g 0 c

b~g ε ~g 0 c = b~g ~g 0 c,

ZU064-05-FPR

paper-jfp

8

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

so that b~gc = ~g, if there are no cancellations to be made in the string ~g.
We can convert a net string back into a stack by stripping off the push symbols with the
stackify operator, d·e : Γ∗± * Γ∗ :
(n)

dγ+ γ+0 . . . γ+ e = hγ (n) , . . . , γ 0 , γi,
and for convenience, [~g] = db~gce. Notice the stackify operator is defined for strings containing only push actions.
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.
The set Q × Γ∗ is called the configuration-space of this pushdown system. We use PDS to
denote the class of all pushdown systems.
For the following definitions, let M = (Q, Γ, δ ).
• The labeled transition relation (7−→M ) ⊆ (Q × Γ∗ ) × Γ± × (Q × Γ∗ ) determines
whether one configuration may transition to another while performing the given
stack action:
ε

(q,~γ) 7−→ (q0 ,~γ) iff q  q0 ∈ δ
ε

[no change]

M

γ−

γ−

(q, γ : ~γ) 7−→ (q0 ,~γ) iff q  q0 ∈ δ

[pop]

M

γ+

γ+

(q,~γ) 7−→ (q0 , γ : ~γ) iff q  q0 ∈ δ

[push].

M

• If unlabelled, the transition relation (7−→) checks whether any stack action can
enable the transition:
g

c 7−→ c0 iff c 7−→ c0 for some stack action g.
M

M

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

g

g

gn−1

gn

M

M

M

M

M

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

for some configurations c0 , . . . , cn .
• For the transitive closure:
~g

c 7−→∗ c0 iff c 7−→ c0 for some action string ~g.
M

M

Note Some texts define the transition relation δ so that δ ⊆ Q × Γ × Q × Γ∗ . In these
texts, (q, γ, q0 ,~γ) ∈ δ means, “if in control state q while the character γ is on top, pop the
stack, transition to control state q0 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.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

9

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 the reachable-fromroot transition relation:
g

g

c7−
−→
→ c0 iff (q0 , hi) 7−→∗ c and c 7−→ c0 .
M

M

M

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:
g

g

M

M

q 7−
−→
→ q0 iff (q,~γ) 7−
−→
→ (q0 ,~γ 0 ) for some stacks ~γ,~γ 0 .
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:
g

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

M

2.5 Computing reachability in pushdown systems
A pushdown flow analysis can be construed as computing the root-reachable subset of
control states in a rooted pushdown system, M = (Q, Γ, δ , q0 ):
n
o
q : q0 7−
−→
→ q .
M

Reps et. al and many others provide a straightforward “summarization” algorithm to compute this set (Bouajjani et al. 1997; Kodumal and Aiken 2004; Reps 1998; Reps et al.
2005). We will develop a complete alternative to summarization, and then instrument this
development for introspective pushdown systems. Summarization builds two large tables:
• One maps “calling contexts” to “return sites” (AKA “local continuations”) so that a
returning function steps to all the places it must return to.
• The other maps “calling contexts” to “return states,” so that any place performing a
call with an already analyzed calling context can jump straight to the returns.
This setup requires intimate knowledge of the language in question for where continuations
should be segmented to be “local” and is strongly tied to function call and return. Our
algorithm is based on graph traversals of the transition relation for a generic pushdown
system. It requires no specialized knowledge of the analyzed language, and it avoids the
memory footprint of summary tables.
2.6 Pushdown automata
A pushdown automaton is an input-accepting generalization of a rooted pushdown system, a 7-tuple (Q, Σ, Γ, δ , q0 , F,~γ) in which:
1. Σ is an input alphabet;
2. δ ⊆ Q × Γ± × (Σ ∪ {ε}) × Q is a transition relation;

ZU064-05-FPR

paper-jfp

10

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
3. F ⊆ Q is a set of accepting states; and
4. ~γ ∈ Γ∗ is the initial stack.

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, q0 ) and w ∈ L (Q, Σ, Γ, δ , q0 , F, γ : ~γ)
aw ∈ L (M) if δ (q0 , ε, a, q0 ) and w ∈ L (Q, Σ, Γ, δ , q0 , F,~γ)
aw ∈ L (M) if δ (q0 , γ− , a, q0 ) and w ∈ L (Q, Σ, Γ, δ , q0 , F,~γ 0 )
where ~γ = hγ, γ2 , . . . , γn i and ~γ 0 = hγ2 , . . . , γn i,
where a is either the empty string ε or a single character.

2.7 Nondeterministic finite automata
In this work, we will need a finite description of all possible stacks at a given control state
within a rooted pushdown system. We will exploit the fact that the set of stacks at a given
control point is a regular language. Specifically, we will extract a nondeterministic finite
automaton accepting that language from the structure of a rooted pushdown system. A
nondeterministic finite automaton (NFA) is a quintuple M = (Q, Σ, δ , q0 , F):
• Q is a finite set of control states;
• Σ is an input alphabet;
• δ ⊆ Q × (Σ ∪ {ε}) × Q is a transition relation.
• q0 is a distinguished start state.
• F ⊆ Q is a set of accepting states.
We denote the class of all NFAs as NFA.

3 Setting: A-Normal Form λ -Calculus
Since our goal is analysis of higher-order languages, we operate on the λ -calculus. To
simplify presentation of the concrete and abstract semantics, we choose A-Normal Form
λ -calculus. (This is a strictly cosmetic choice: all of our results can be replayed mutatis
mutandis in the standard direct-style setting as well. This differs from CFA2’s requirement
of CPS, since ANF can be applied locally whereas CPS requires a global transformation.)
ANF enforces an order of evaluation and it requires that all arguments to a function be

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

c ∈ Conf = Exp × Env × Store × Kont

11

[configurations]

ρ ∈ Env = Var * Addr

[environments]

σ ∈ Store = Addr → Clo

[stores]

clo ∈ Clo = Lam × Env

[closures]

κ ∈ Kont = Frame∗

[continuations]

φ ∈ Frame = Var × Exp × Env

[stack frames]

a ∈ Addr is an infinite set of addresses

[addresses].

Fig. 3: The concrete configuration-space.

atomic:
e ∈ Exp ::= (let ((v call)) e)

[non-tail call]

| call

[tail call]

| æ

[return]

f , æ ∈ Atom ::= v | lam

[atomic expressions]

lam ∈ Lam ::= (λ (v) e)

[lambda terms]

call ∈ Call ::= ( f æ)

[applications]

v ∈ Var is a set of identifiers

[variables].

We use the CESK machine of Felleisen and Friedman (1987) to specify a small-step
semantics for ANF. The CESK machine has an explicit stack, and under a structural abstraction, the stack component of this machine directly becomes the stack component of a
pushdown system. The set of configurations (Conf ) for this machine has the four expected
components (Figure 3).
3.1 Semantics
To define the semantics, we need five items:
1. I : Exp → Conf injects an expression into a configuration:
c0 = I (e) = (e, [], [], hi).
2. A : Atom × Env × Store * Clo evaluates atomic expressions:
A (lam, ρ, σ ) = (lam, ρ)
A (v, ρ, σ ) = σ (ρ(v))

[closure creation]
[variable look-up].

3. (⇒) ⊆ Conf × Conf transitions between configurations. (Defined below.)
4. E : Exp → P (Conf ) computes the set of reachable machine configurations for a
given program:
E (e) = {c : I (e) ⇒∗ c} .

ZU064-05-FPR

paper-jfp

6 February 2018

12

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

5. alloc : Var × Conf → Addr chooses fresh store addresses for newly bound variables.
The address-allocation function is an opaque parameter in this semantics, so that the
forthcoming abstract semantics may also parameterize allocation. The nondeterministic nature of the semantics makes any choice of alloc sound (Might and Manolios
2009). This parameterization provides the knob to tune the polyvariance and contextsensitivity of the resulting analysis. For the sake of defining the concrete semantics,
letting addresses be natural numbers suffices. The allocator can then choose the
lowest unused address:
Addr = N
alloc(v, (e, ρ, σ , κ)) = 1 + max(dom(σ )).
Transition relation To define the transition c ⇒ c0 , 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 closure’s λ -term:
c0

c

}|
{
}|
{ z
z
([[( f æ)]], ρ, σ , κ) ⇒ (e, ρ 00 , σ 0 , κ) , where
0

([[(λ (v) e)]], ρ ) = A ( f , ρ, σ )

a = alloc(v, c)
ρ 00 = ρ 0 [v 7→ a]
σ 0 = σ [a 7→ A (æ, ρ, σ )].

Non-tail calls push a frame onto the stack and evaluate the call:
c0

c

z
}|
{ z
}|
{
([[(let ((v call)) e)]], ρ, σ , κ) ⇒ (call, ρ, σ , (v, e, ρ) : κ) .
Function return pops a stack frame:
c

c0

z
}|
{ z
}|
{
(æ, ρ, σ , (v, e, ρ 0 ) : κ) ⇒ (e, ρ 00 , σ 0 , κ) , where

a = alloc(v, c)
ρ 00 = ρ 0 [v 7→ a]
σ 0 = σ [a 7→ A (æ, ρ, σ )].

4 An Infinite-State Abstract Interpretation
Our first step toward a static analysis is an abstract interpretation into an infinite statespace. To achieve a pushdown analysis, we simply abstract away less than we normally
would. Specifically, we leave the stack height unbounded.
Figure 4 details the abstract configuration-space. To synthesize it, 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, to remain sound we change the range of the store to become a power set in the
abstract configuration-space. The abstract transition relation has components analogous to
those from the concrete semantics:

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

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

[configurations]

d = Var * Addr
[
ρ̂ ∈ Env
 
d
[ → P Clo
[ = Addr
σ̂ ∈ Store

[environments]
[stores]

c ∈ Clo
d = Lam × Env
d
clo

[closures]

d = Frame
\
κ̂ ∈ Kont

∗

d
\ = Var × Exp × Env
φ̂ ∈ Frame
[ is a finite set of addresses
â ∈ Addr

13

[continuations]
[stack frames]
[addresses].

Fig. 4: The abstract configuration-space.

[ pairs an expression
Program injection The abstract injection function Iˆ : Exp → Conf
with an empty environment, an empty store and an empty stack to create the initial abstract
configuration:
ĉ0 = Iˆ(e) = (e, [], [], hi).
Atomic expression evaluation The abstract atomic expression evaluator, Aˆ : Atom ×
d returns the value of an atomic expression in the context of an
d × Store
[ → P(Clo),
Env
environment and a store; it returns a set of abstract closures:
Aˆ(lam, ρ̂, σ̂ ) = {(lam, ρ̂)}
Aˆ(v, ρ̂, σ̂ ) = σ̂ (ρ̂(v))

[closure creation]
[variable look-up].

[ ) returns
Reachable configurations The abstract program evaluator Eˆ : Exp → P(Conf
all of the configurations reachable from the initial configuration:

Eˆ (e) = ĉ : Iˆ(e) c
⇒∗ ĉ .
Because there are an infinite number of abstract configurations, a naı̈ve implementation of
this function may not terminate. Pushdown analysis provides a way of precisely computing
this set and both finitely and compactly representing the result.
[ × Conf
[ has three rules,
Transition relation The abstract transition relation (c
⇒) ⊆ Conf
one of which has become nondeterministic. A tail call may fork because there could be
multiple abstract closures that it is invoking:

ĉ

ĉ0

}|
{
}|
{ z
z
([[( f æ)]], ρ̂, σ̂ , κ̂) c
⇒ (e, ρ̂ 00 , σ̂ 0 , κ̂) , where
([[(λ (v) e)]], ρ̂ 0 ) ∈ Aˆ( f , ρ̂, σ̂ )

[ ĉ)
â = alloc(v,
ρ̂ 00 = ρ̂ 0 [v 7→ â]
σ̂ 0 = σ̂ t [â 7→ Aˆ(æ, ρ̂, σ̂ )].

ZU064-05-FPR

paper-jfp

6 February 2018

14

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

We define all of the partial orders shortly, but for stores:
(σ̂ t σ̂ 0 )(â) = σ̂ (â) ∪ σ̂ 0 (â).
A non-tail call pushes a frame onto the stack and evaluates the call:
ĉ0

ĉ

}|
{ z
}|
{
z
([[(let ((v call)) e)]], ρ̂, σ̂ , κ̂) c
⇒ (call, ρ̂, σ̂ , (v, e, ρ̂) : κ̂) .
A function return pops a stack frame:
ĉ

ĉ0

}|
{ z
}|
{
z
(æ, ρ̂, σ̂ , (v, e, ρ̂ 0 ) : κ̂) c
⇒ (e, ρ̂ 00 , σ̂ 0 , κ̂) , where

[ ĉ)
â = alloc(v,
ρ̂ 00 = ρ̂ 0 [v 7→ â]
σ̂ 0 = σ̂ t [â 7→ Aˆ(æ, ρ̂, σ̂ )].

Allocation: Polyvariance and context-sensitivity In the abstract semantics, the abstract
[ : Var × Conf
[ → Addr
[ determines the polyvariance of the analysis.
allocation function alloc
In a control-flow analysis, polyvariance literally refers to the number of abstract addresses
(variants) there are for each variable. An advantage of this framework over CFA2 is that
varying this abstract allocation function instantiates pushdown versions of classical flow
analyses. All of the following allocation approaches can be used with the abstract semantics. Note, though only a technical detail, that the concrete address space and allocation
would change as well for the abstraction function to still work. The abstract allocation
function is a parameter to the analysis.
Monovariance: Pushdown 0CFA Pushdown 0CFA uses variables themselves for abstract
addresses:
[ = Var
Addr
alloc(v, ĉ) = v.
For better precision, a program would be transformed to have unique binders.
Context-sensitive: Pushdown 1CFA Pushdown 1CFA pairs the variable with the current
expression to get an abstract address:
[ = Var × Exp
Addr
alloc(v, (e, ρ̂, σ̂ , κ̂)) = (v, e).
For better precision, expressions are often uniquely labeled so that textually equal expressions at different points in the program are distinguished.
Polymorphic splitting: Pushdown poly/CFA Assuming we compiled the program from
a programming language with let expressions and we marked which identifiers were letbound, we can enable polymorphic splitting:

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

15

[ = 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
∗
[ to Var × Conf
[ → Addr.
[ By
the last k states, necessarily changing the signature of alloc
concatenating the expressions in the last k states together, and pairing this sequence with a
variable we get pushdown k-CFA:
[ = Var × Expk
Addr
[ h(e1 , ρ̂1 , σ̂1 , κ̂1 ), . . .i) = (v, he1 , . . . , ek i).
alloc(v,

4.1 Partial orders
For each set X̂ inside the abstract configuration-space, we use the natural partial order,
(vX̂ ) ⊆ X̂ × X̂. Abstract addresses and syntactic sets have flat partial orders. For the other
sets, the partial order lifts:
• point-wise over environments:
ρ̂ v ρ̂ 0 iff ρ̂(v) = ρ̂ 0 (v) for all v ∈ dom(ρ̂);
• component-wise over closures:
(lam, ρ̂) v (lam, ρ̂ 0 ) iff ρ̂ v ρ̂ 0 ;
• point-wise over stores:
σ̂ v σ̂ 0 iff σ̂ (â) v σ̂ 0 (â) for all â ∈ dom(σ̂ );
• component-wise over frames:
(v, e, ρ̂) v (v, e, ρ̂ 0 ) iff ρ̂ v ρ̂ 0 ;
• element-wise over continuations:
hφ̂1 , . . . , φ̂n i v hφ̂10 , . . . , φ̂n0 i iff φ̂i v φ̂i0 ; and
• component-wise across configurations:
(e, ρ̂, σ̂ , κ̂) v (e, ρ̂ 0 , σ̂ 0 , κ̂ 0 ) iff ρ̂ v ρ̂ 0 and σ̂ v σ̂ 0 and κ̂ v κ̂ 0 .

ZU064-05-FPR

paper-jfp

16

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
4.2 Soundness

To prove soundness, an abstraction map α connects the concrete and abstract configurationspaces:
α(e, ρ, σ , κ) = (e, α(ρ), α(σ ), α(κ))
α(ρ) = λ v.α(ρ(v))
α(σ ) = λ â.

G

{α(σ (a))}

α(a)=â

αhφ1 , . . . , φn i = hα(φ1 ), . . . , α(φn )i
α(v, e, ρ) = (v, e, α(ρ))
α(a) is determined by the allocation functions.
It is then easy to prove that the abstract transition relation simulates the concrete transition
relation:
Theorem 4.1
[ such that α(c0 ) v ĉ0 and ĉ c
If α(c) v ĉ and c ⇒ c0 , then there exists ĉ0 ∈ Conf
⇒ ĉ0 .
Proof
The proof follows by case analysis on 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, accounting for the states of interest, when
intersected with the language of the PDA, is nonempty.
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 controlstates visited by the abstracted CESK machine. Thus, every transition will consume the

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

\ (e) = (Q, Σ, Γ, δ , q0 , F, hi), where
PDA

17

(q, ε, q0 , q0 ) ∈ δ iff (q, κ̂) c
⇒ (q0 , κ̂) for all κ̂

d × Store
[
Q = Exp × Env

(q, φ̂− , q0 , q0 ) ∈ δ iff (q, φ̂ : κ̂) c
⇒ (q0 , κ̂) for all κ̂

Σ=Q

(q, φ̂+0 , q0 , q0 ) ∈ δ iff (q, κ̂) c
⇒ (q0 , φ̂ 0 : κ̂) for all κ̂
(q0 , hi) = Iˆ(e)

\
Γ = Frame

F = Q.

\ : Exp → PDA.
Fig. 5: PDA

control-state to which it transitioned as an input character. Figure 5 defines the program-to\ : Exp → PDA. (Note the implicit use of the isomorphism
PDA conversion function PDA
∼
d
[
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 contextfree language described by the PDA. That is, if we want to know whether the control state
(e0 , ρ̂, σ̂ ) is reachable in a program e, we can reduce the problem to determining:

\ (e)) 6= 0,
Σ∗ · (e0 , ρ̂, σ̂ ) · Σ∗ ∩ L (PDA
/
where L1 · L2 is the concatenation of formal languages L1 and L2 .
Theorem 5.1
Control-state reachability is decidable.
Proof
The intersection of a regular language and a context-free language is context-free (simple
machine product of PDA with DFA). The emptiness of a context-free language is decidable. The decision procedure is easiest for CFGs: mark terminals, mark non-terminals that
reduce to marked (non)terminals until we reach a fixed point. If the start symbol is marked,
then the language is nonempty. The PDA to CFG translation is a standard construction.
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 this set of states Ŝ:

Ŝ = ([[( f æ)]], ρ̂, σ̂ ) : (lam, ρ̂ 0 ) ∈ Aˆ( f , ρ̂, σ̂ ) for some ρ̂ 0 .
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:
\ (e)) 6= 0.
Σ∗ · {q} · Σ∗ ∩ L (PDA
/
If this is true, then lam may flow to f ; if false, then it does not.
Problem: Doubly exponential complexity The non-emptiness-of-intersection approach
establishes decidability of pushdown control-flow analysis. But, two exponential complexity barriers make this technique impractical.

ZU064-05-FPR

paper-jfp

6 February 2018

18

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

[ |Var| ) and stores
First, there are an exponential number of both environments (|Addr|
d [
d [
((2|Clo| )|Addr| = 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. The size of the control-state-space of the
PDA is clearly doubly exponential:
d × Store|
[
|Q| = |Exp × Env
d × |Store|
[
= |Exp| × |Env|
d Addr|
[
[ |Var| × 2|Clo|×|
= |Exp| × |Addr|
d Addr|
[
[ |Var| × 2|Lam×Env|×|
= |Exp| × |Addr|
[ |Var| ×|Addr|
[
[ |Var| × 2|Lam|×|Addr|
= |Exp| × |Addr|

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. A rooted pushdown system M = (Q, Γ, δ , q0 ) is compact if for any
(q, g, q0 ) ∈ δ , it is the case that:
(q0 , hi) 7−→∗ (q,~γ) for some stack ~γ,
M

and the domain of states and stack characters are exactly those that appear in δ :
Q = {{q, q0 } : (q, g, q0 ) ∈ δ }
Γ = {γ : (q, γ+ , q0 ) ∈ δ or (q, γ− , q0 ) ∈ δ }
S

In other words, a rooted pushdown system is compact when its states, transitions and stack
characters appear on legal paths from the initial control state. We will refer to the class of
compact rooted pushdown systems as CRPDS.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

19

We can compact a rooted pushdown system with a map:
C : RPDS → CRPDS
M

z
}|
{
C (Q, Γ, δ , q0 ) = (Q0 , Γ0 , δ 0 , q0 )
n
o
where Q0 = q : (q0 , hi) 7−→∗ (q,~γ)
M
n
o
0
Γ = γi : (q0 , hi) 7−→∗ (q,~γ)
M


~g
g
0
0
0
δ = (q, g, q ) : (q0 , hi) 7−→ (q, [~g]) 7−→ (q , [~gg]) .
M

M

In practice, the real difference between a rooted pushdown system and its compact form
is that our original system will be defined intensionally (having come from the components
of an abstracted CESK machine), whereas the compact system 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 to compact it.
To convert the abstracted CESK machine into a rooted pushdown system, we use the
\ : Exp → RPDS:
function RPDS
\ (e) = (Q, Γ, δ , q0 )
RPDS

ε

q  q0 ∈ δ iff (q, κ̂) c
⇒ (q0 , κ̂) for all κ̂

d × Store
[
Q = Exp × Env
\
Γ = Frame
(q0 , hi) = Iˆ(e)

φ̂−

q  q0 ∈ δ iff (q, φ̂ : κ̂) c
⇒ (q0 , κ̂) for all κ̂
φ̂+

q  q0 ∈ δ iff (q, κ̂) c
⇒ (q0 , φ̂ : κ̂) for all κ̂.

7 Compacting a Rooted Pushdown System
We now turn our attention to compacting a rooted pushdown system (defined intensionally)
into its compact form (defined extensionally). That is, we want to find an implementation
of the function C . To do so, we first phrase the construction as the least fixed point of a
monotonic function. This will provide a method (albeit an inefficient one) for computing
the function C . In the next section, we look at an optimized work-set driven algorithm that
avoids the inefficiencies of this section’s algorithm.
The function F : RPDS → (CRPDS → CRPDS) generates the monotonic iteration
function we need:
F (M) = f , where
M = (Q, Γ, δ , q0 )

f (S, Γ, E, s0 ) = (S0 , Γ, E 0 , s0 ), where
n
o
S0 = S ∪ s0 : s ∈ S and s 7−
−→
→ s0 ∪ {s0 }
M
n g
o
g
0
0
E = E ∪ s  s : s ∈ S and s 7−
−→
→ s0 .
M

Given a rooted pushdown system M, each application of the function F (M) accretes new
edges at the frontier of the system. Once the algorithm reaches a fixed point, the system is
complete:

ZU064-05-FPR

paper-jfp

20

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Theorem 7.1
C (M) = lfp(F (M)).
Proof
Let M = (Q, Γ, δ , q0 ). Let f = F (M). Observe that lfp( f ) = f n (0,
/ Γ, 0,
/ q0 ) for some n.
When N ⊆ C (M), then it easy to show that f (N) ⊆ C (M). Hence, C (M) ⊇ lfp(F (M)).
To show C (M) ⊆ lfp(F (M)), suppose this is not the case. Then, there must be at least
one edge in C (M) that is not in lfp(F (M)). Since these edges must be root reachable, let
(s, g, s0 ) be the first such edge in some path from the root. This means 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, C (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 system bounds the run-time
of the algorithm. Suppose the final system 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 ε 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  s0 , 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-set and an ε-closure graph to avoid spurious recomputation.
Moreover, we have carefully phrased the complexity in terms of “reachable” control
states because, in practice, compact rooted pushdown systems will be extremely sparse,
and because the maximum number of control states is exponential in the size of the input
program. After the subsequent refinement, we will be able to develop a hierarchy of pushdown control-flow analyses that employs widening to achieve a polynomial-time algorithm
at its foundation.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

21

8 An Efficient Algorithm: Work-sets and ε-Closure Graphs
We have developed a fixed-point formulation of the rooted pushdown system compaction
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-set. That is, our next
algorithm will keep a work-set of new states and edges to consider, instead of reconsidering
all of them. We will refer to the compact rooted pushdown system we are constructing as
a graph, since that is how we represent it (Q is the set of nodes, and δ is a set of labeled
edges).
In each iteration, it will pull new states and edges from the work list, insert them into the
graph and then populate the work-set 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 ε q0 into the following graph:
q0

γ+

/q

q0

γ−

/ 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:
ε

q0

γ+

/q

ε

/ q0

γ−

/ q 1

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 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, 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 ε [s] = s0 : (s0 , s) ∈ H ∪ {s}
[ancestors]
0
→
−
G ε [s] = s : (s, s0 ) ∈ H ∪ {s}
[descendants].
8.2 Integrating a work-set
Since we only want to consider new states and edges in each iteration, we need a work-set,
or in this case, three work-sets:

ZU064-05-FPR

paper-jfp

22

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
• ∆S contains states to add,
• ∆E contains edges to add,
• ∆H contains new ε-edges.

Let WS ::= (∆S, ∆E, ∆H) be the space of work-sets.
8.3 A new fixed-point iteration-space
Instead of consuming a graph and producing a graph, the new fixed-point iteration function
will consume and produce a graph, an ε-closure graph, and the work-sets. Hence, the
iteration space of the new algorithm is:
ICRPDS = (℘(Q) ×℘(Q × Γ± × Q)) × ECG × WS.
The I in ICRPDS stands for intermediate.
8.4 The ε-closure graph work-list algorithm
The function F 0 : RPDS → (ICRPDS → ICRPDS) generates the required iteration function (Figure 6). Please note that we implicitly distribute union across tuples:
(X,Y ) ∪ (X 0 ,Y 0 ) = (X ∪ X,Y ∪Y 0 ).
The functions sprout, addPush, addPop, addEmpty (defined shortly) calculate the additional the graph edges and ε-closure graph edges (potentially) introduced by a new state or
edge.
Sprouting Whenever a new state gets added to the 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 graph. The sprout function:
sprout(Q,Γ,δ ,s0 ) : Q → (P (δ ) × P (Q × Q)),
checks whether a new state could produce any new push edges or no-change edges. We
can represent its behavior diagrammatically (as previously, the dotted arrows correspond
to the corresponding additions to the work-graph and ε-closure work graph):
s
γ+

ε
δ

q0

δ



q00

which means if adding control state s:
ε

add edge s  q0 if it exists in δ (hence the arrow subscript δ ), and
γ+

add edge s  q00 if it exists in δ .
Formally:
sprout(Q,Γ,δ ,s0 ) (s) = (∆E, ∆H), where

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

23

F 0 (M) = f , where
M = (Q, Γ, δ , q0 )
f (G, H, (∆S, ∆E, ∆H)) = (G0 , H 0 , (∆S0 − S0 , ∆E 0 − E 0 , ∆H 0 − H)), where
(S, Γ, E, s0 ) = G
(∆E0 , ∆H0 ) =

[

sproutM (s)

s∈∆S

[

(∆E1 , ∆H1 ) =
(s,γ+

(∆E2 , ∆H2 ) =

addPushM (G, H)(s, γ+ , s0 )

,s0 )∈∆E

[

addPopM (G, H)(s, γ− , s0 )

(s,γ− ,s0 )∈∆E

(∆E3 , ∆H3 ) =

[

addEmptyM (G, H)(s, s0 )

(s,ε,s0 )∈∆E

(∆E4 , ∆H4 ) =

[

addEmptyM (G, H)(s, s0 )

(s,s0 )∈∆H

S0 = S ∪ ∆S
E 0 = E ∪ ∆E
H 0 = H ∪ ∆H
∆E 0 = ∆E0 ∪ ∆E1 ∪ ∆E2 ∪ ∆E3 ∪ ∆E4

∆S0 = s0 : (s, g, s0 ) ∈ ∆E 0 ∪ {s0 }
∆H 0 = ∆H0 ∪ ∆H1 ∪ ∆H2 ∪ ∆H3 ∪ ∆H4

∆Γ = γ : (s, γ+ , s0 ) ∈ ∆E 0
G0 = (S ∪ ∆S, Γ ∪ ∆Γ, E 0 , q0 ).

Fig. 6: The fixed point of the function F 0 (M) contains the compact form of the rooted
pushdown system M.


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

Considering the consequences of a new push edge Once our algorithm adds a new push
edge to a 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:
addPush(Q,Γ,δ ,s0 ) : RPDS × ECG → δ → (P (δ ) × P (Q × Q)),

ZU064-05-FPR

paper-jfp

24

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

checks for ε-reachable states that could produce a pop. We can represent this action by the
following diagram (the arrow subscript ε indicates edges in the ε-closure graph):
s

/q

γ+

ε
ε

/ q0

γ−
δ

/ q00
G

ε
ε
γ+

which means if adding push-edge s  q:
γ−

if pop-edge q0  q00 is in δ , then
γ−

add edge q0  q00 , and
add ε-edge s  q00 .
Formally:
γ+

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


γ
γ
→
−
0 − 00
0
0 − 00
∆E = q  q : q ∈ G ε [q] and q  q ∈ δ


γ
→
−
00
0
0 − 00
∆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 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,Γ,δ ,s0 ) : RPDS × ECG → δ → (P (δ ) × P (Q × Q)),
checks for ε-reachable push-edges that could match this pop-edge. This action is illustrated
by the following diagram:
s

γ+

/ s0

ε
ε

/ s00

γ−
δ

/q
I

ε
ε
γ−

which means if adding pop-edge s00  q:
γ+

if push-edge s  s0 is already in the graph, then
add ε-edge s  q.
Formally:
γ−

addPop(Q,Γ,δ ,s0 ) (G, H)(s00  q) = (∆E, ∆H), where


γ+
←
−
∆E = 0/ and ∆H = s  q : s0 ∈ G ε [s00 ] and s  s0 ∈ 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

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

25

an old push to (perhaps newly enabled) pop edges. The addEmpty function:
addEmpty(Q,Γ,δ ,s0 ) : RPDS × 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

γ+

/ s0

ε
ε

ε
ε

/ s00


/ s000

ε

ε
ε


/ s0000
I

γ−
δ

/q
O

ε
ε

ε
ε

which means if adding ε-edge s00  s000 :
γ−

if pop-edge s0000  q is in δ , then
add ε-edge s  q; and
γ−
add edge s0000  q;
add ε-edges s0  s000 , s00  s0000 , and s0  s0000 .
Formally:
addEmpty(Q,Γ,δ ,s0 ) (G, H)(s00  s000 ) = (∆E, ∆H), where

γ−
←
−
→
−
∆E = s0000  q : s0 ∈ G ε [s00 ] and s0000 ∈ G ε [s000 ] and
γ+

γ−

s  s0 ∈ G and s0000  q ∈ δ

←
−
→
−
∆H = s  q : s0 ∈ G ε [s00 ] and s0000 ∈ G ε [s000 ] and
γ+

γ−

s  s0 ∈ G and s0000  q ∈ δ
n
o
←
−
∪ s0  s000 : s0 ∈ G ε [s00 ]
n
o
→
−
∪ s00  s0000 : s0000 ∈ G ε [s000 ]
n
o
←
−
→
−
∪ s0  s0000 : s0 ∈ G ε [s00 ] and s0000 ∈ G ε [s000 ] .
8.5 Termination and correctness
To prove that a fixed point exists, we show the iteration function is monotonic. The key
observation is that ∆G and ∆H drive all additions to, and are disjoint from, G and H. Since
G and H monotonically increase in a finite space, ∆G and ∆H run out of room (full details
in 18.1). Once the graph reaches a fixed point, all work-sets will be empty, and the εclosure graph will also be saturated. We can also show that this algorithm is correct by
defining first E C G : RPDS → ECG as


~g
0
0
E C G (M) = s  s : s 7−
−→
→ s and [~g] = ε
M

ZU064-05-FPR

paper-jfp

26

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

and stating the following theorem:
Theorem 8.1
For all M ∈ RPDS, C (M) = G and E C G (M) = H, where (G, H, (0,
/ 0,
/ 0))
/ = lfp(F 0 (M)).
In the proof of Theorem 8.1, the ⊆ case comes from an invariant lemma we have on F 0 :
Lemma 8.1
g

g

inv((S, E), H, (∆S, ∆E, ∆H)) = ∀s  s0 ∈ E ∪ ∆E.s 7−
−→
→ s0
M

~g

∧ ∀s  s0 ∈ H ∪ ∆H.∃~g.[~g] = ε ∧ ∀κ̂.(s, κ̂) 7−→∗ (s, κ̂)
M

The ⊇ case follows from
Lemma 8.2
~g
~g
−→
→ s, there is both a corresponding path s0 7−
−→
→ s and for all nonFor all traces π ≡ s0 7−
M

G

~g0

empty subtraces of π, sb 7−
−→
→ sa , if [~g0 ] = ε then sb  sa ∈ H.
M

Since all edges in a compact rooted pushdown system must be in a path from the initial
state, we can extract the edges from said paths using this lemma.
8.6 Complexity: Still exponential, but more efficient
As in the previous case (Section 7.1), 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 graph plus the size of the ε-closure graph.
Suppose the final 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 graph (|Γ|m2 push edges,
just as many pop edges, and m2 no-change edges) and at most m2 edges in the ε-closure
graph, which bounds the number of iterations. Recall that m can be exponential in the size
of the program, since m ≤ |Q| (and Section 5 derived the exponential size of |Q|).
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 graphs,
this is a reasonable algorithm.
9 Polynomial-Time Complexity from Widening
In the previous section, we developed a more efficient fixed-point algorithm for computing a compact rooted pushdown system. Even with the core improvements we made,
the algorithm remained exponential in the worst case, owing to the fact that there could

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

27

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 finitestate CFAs are exponential without some sort of widening as well (Van Horn and Mairson
2008).
To achieve polynomial time complexity for pushdown control-flow analysis requires the
same two steps as the classical case: (1) widening the abstract interpretation to use a global,
“single-threaded” 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 singlethreaded 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).
We can redefine the concrete evaluation function:
E (e) = lfp( fe ), where fe : System → System and

fe (C) = {I (e)} ∪ c0 : c ∈ C and c ⇒ c0 .
9.2 Step 2: Refactor the abstract semantics
We can take the same approach with the abstract evaluation function, first redefining the
abstract system-space:


[
\ = P Conf
Ĉ ∈ System


d × Store
d ,
[ × Kont
= P Exp × Env
and then the abstract evaluation function:
\ → System
\ and
Eˆ (e) = lfp( fˆe ), where fˆe : System

 0
fˆe (Ĉ) = Iˆ(e) ∪ ĉ : ĉ ∈ Ĉ and ĉ c
⇒ ĉ0 .
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 t · · · t σ̂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

ZU064-05-FPR

paper-jfp

28

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

set of partial configurations and a single global store:


0
\ × Store
\ = P PConf
[
System
d × Kont.
d
\ = Exp × Env
π̂ ∈ PConf
We can factor the store out of the abstract transition relation as well, so that (_σ̂ ) ⊆
\ × (PConf
\ × Store):
[
PConf
σ̂

(e, ρ̂, κ̂) _ ((e0 , ρ̂ 0 , κ̂ 0 ), σ̂ 0 ) iff (e, ρ̂, σ̂ , κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , κ̂ 0 ),
0

0

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


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


G
σ̂
0
00
0
00
σ̂ =
σ̂ : π̂ _ (π̂ , σ̂ )
(π̂0 , hi) = Iˆ(e).
9.4 Step 4: Pushdown control-flow graphs
Following the earlier graph reformulation of the compact rooted pushdown system, we
can reformulate the set of partial configurations as a pushdown control-flow graph. A
pushdown 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:
00

\ = PDCFG
\ × Store
[
System
\ = P(PState)
\ × P(PState
\ × Frame
\
\ ± × PState)
PDCFG
d
\ = Exp × Env.
ψ̂ ∈ PState
In a pushdown 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.
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:
PDCFG edges

store entries

}|
{
}|
{ z
z
d.
[ × |Clo|
\ × |Frame
\ + |Addr|
\ ± | × |PState|
|PState|
With a monovariant allocation scheme that eliminates abstract environments, the number
of iterations ultimately reduces to:
d + 1) × |Exp| + |Var| × |Lam|,
|Exp| × (2|Var|

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

29

which means that, in the worst case, the algorithm makes a cubic number of iterations with
respect to the size of the input program.3
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
control-flow 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
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:


d = P PState
\ × PState
\ .
ECG
Then, we can set the system space to include ε-closure graphs:
000

d × Store.
\ = CRPDS
\ × ECG
[
System
Before we redefine the iteration function, we need another factored transition relation.
σ̂
\ × PState
\ × Store deterThe stack- and action-factored transition relation (+) ⊆ PState
g

mines if a transition is possible under the specified store and stack-action:
(e, ρ̂) + ((e0 , ρ̂ 0 ), σ̂ 0 ) iff (e, ρ̂, σ̂ , κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , φ̂ : κ̂)
σ̂

φ̂+

(e, ρ̂) + ((e0 , ρ̂ 0 ), σ̂ 0 ) iff (e, ρ̂, σ̂ , φ̂ : κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , κ̂)
σ̂

φ̂−

(e, ρ̂) + ((e0 , ρ̂ 0 ), σ̂ 0 ) iff (e, ρ̂, σ̂ , κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , κ̂).
σ̂
ε

Now, we can redefine the iteration function (Figure 7).
Theorem 9.1
Pushdown 0CFA with single-threaded store (PDCFA) 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.
3

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
\ = |Var|.
the number of variables and the number of expressions, i.e., |Frame|

ZU064-05-FPR

paper-jfp

30

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

fˆe ((P̂, Ê), Ĥ, σ̂ ) = ((P̂0 , Ê 0 ), Ĥ 0 , σ̂ 00 ), where
(
T̂+ =

φ̂+

)
0

0

0

σ̂

0

(ψ̂  ψ̂ , σ̂ ) : ψ̂ + (ψ̂ , σ̂ )
φ̂+

n
o
ε
σ̂
T̂ε = (ψ̂  ψ̂ 0 , σ̂ 0 ) : ψ̂ + (ψ̂ 0 , σ̂ 0 )
ε


φ̂−
σ̂
T̂− = (ψ̂ 00  ψ̂ 000 , σ̂ 0 ) : ψ̂ 00 + (ψ̂ 000 , σ̂ 0 ) and
φ̂−
φ̂+

ψ̂  ψ̂ 0 ∈ Ê and
ψ̂ 0  ψ̂ 00 ∈ Ĥ
T̂ 0 = T̂+ ∪ T̂ε ∪ T̂−

Ê 0 = ê : (ê, ) ∈ T̂ 0
G
σ̂ 00 =
σ̂ 0 : ( , σ̂ 0 ) ∈ T̂ 0

Ĥε = ψ̂  ψ̂ 00 : ψ̂  ψ̂ 0 ∈ Ĥ and ψ̂ 0  ψ̂ 00 ∈ Ĥ

φ̂+
Ĥ+− = ψ̂  ψ̂ 000 : ψ̂  ψ̂ 0 ∈ Ê and ψ̂ 0  ψ̂ 00 ∈ Ĥ
φ̂−

and ψ̂ 00  ψ̂ 000 ∈ Ê
Ĥ 0 = Ĥε ∪ Ĥ+−
n
o
g
P̂0 = P̂ ∪ ψ̂ 0 : ψ̂  ψ̂ 0 ∪ {(e, ⊥)} .

Fig. 7: An ε-closure graph-powered iteration function for pushdown control-flow analysis
with a single-threaded store.

10 Introspection for Abstract Garbage Collection
Abstract garbage collection (Might and Shivers 2006b) yields large improvements in precision by using the abstract interpretation of garbage collection to make more efficient
use of the finite address space available during analysis. Because of the way abstract
garbage collection operates, it grants exact precision to the flow analysis of variables whose
bindings die between invocations of the same abstract context. Because pushdown analysis
grants exact precision in tracking return-flow, it is clearly advantageous to combine these
techniques. Unfortunately, as we shall demonstrate, abstract garbage collection breaks the
pushdown model by requiring a full traversal of the stack to discover the root set.
Abstract garbage collection modifies the transition relation to conduct a “stop-and-copy”
garbage collection before each transition. To do this, we define a garbage collection func[ → Conf
[ on configurations:
tion Ĝ : Conf
ĉ

z }| {
Ĝ(e, ρ̂, σ̂ , κ̂) = (e, ρ̂, σ̂ |Reachable(ĉ), κ̂),

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

31

where the pipe operation f |S yields the function f , but with inputs not in the set S mapped
[ → P(Addr)
[ first
to bottom—the empty set. The reachability function Reachable : Conf
computes the root set, and then the transitive closure of an address-to-address adjacency
relation:
ĉ


z }| {
∗
Reachable(e, ρ̂, σ̂ , κ̂) = â : â0 ∈ Root(ĉ) and â0 _ â ,
σ̂

[ → P(Addr)
[ finds the root addresses:
where the function Root : Conf
Root(e, ρ̂, σ̂ , κ̂) = range(ρ̂) ∪ StackRoot(κ̂),
d → P(Addr)
[ function finds roots down the stack:
and the StackRoot : Kont
StackRoothφ1 , . . . , φn i =

[

T (φi ),

i

[
\ → P(Addr):
using a “touches” function, T : Frame
T (v, e, ρ̂) = range(ρ̂),
[ × Store
[ connects adjacent addresses:
[ × Addr
and the relation (_) ⊆ Addr
â _ â0 iff there exists (lam, ρ̂) ∈ σ̂ (â) such that â0 ∈ range(ρ̂).
σ̂

The new abstract transition relation is thus the composition of abstract garbage collection
with the old transition relation:
(c
⇒GC ) = (c
⇒) ◦ Ĝ.
Problem: Stack traversal violates pushdown constraint In the formulation of pushdown systems, the transition relation is restricted to looking at the top frame, and in less
restricted formulations that may read the stack, the reachability decision procedures need
the entire system up-front. Thus, the relation (c
⇒GC ) cannot be computed as a straightforward pushdown analysis using summarization.
Solution: Introspective pushdown systems To accommodate the richer structure of the
relation (c
⇒GC ), we now define introspective pushdown systems. Once defined, we can
embed the garbage-collecting abstract interpretation within this framework, and then focus
on developing a control-state reachability algorithm for these systems.
An introspective pushdown system is a quadruple M = (Q, Γ, δ , q0 ):
1. Q is a finite set of control states;
2. Γ is a stack alphabet;
3. δ ⊆ Q × Γ∗ × Γ± × Q is a transition relation (where (q, κ, φ− , q0 ) ∈ δ implies κ ≡ φ :
κ 0 ); and
4. q0 is a distinguished root control state.
The second component in the transition relation is a realizable stack at the given controlstate. This realizable stack distinguishes an introspective pushdown system from a general
pushdown system. IPDS denotes the class of all introspective pushdown systems.

ZU064-05-FPR

paper-jfp

32

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Determining how (or if) a control state q transitions to a control state q0 , requires knowing a path taken to the state q. We concern ourselves with root-reachable states. When
M = (Q, Γ, δ , q0 ), if there is a κ̂ such that (q0 , hi) 7−→∗ (q, κ̂) we say q is reachable via κ̂,
M

where
(q, κ̂) 7−→∗ (q0 , κ̂ 0 ) (q0 , κ̂ 0 , g0 , q00 ) ∈ δ
M

(q, κ̂) 7−→∗ (q, κ̂)
M

(q, κ̂) 7−→∗ (q00 , [κ̂+0 g0 ])
M

10.1 Garbage collection in introspective pushdown systems
To convert the garbage-collecting, abstracted CESK machine into an introspective pushdown system, we use the function I \
PDS : Exp → IPDS:
I\
PDS (e) = (Q, Γ, δ , q0 )
d × Store
[
Q = Exp × Env
\
Γ = Frame
(q0 , hi) = Iˆ(e)

(q, κ̂, ε, q0 ) ∈ δ iff Ĝ(q, κ̂) c
⇒ (q0 , κ̂)
(q, φ̂ : κ̂, φ̂− , q0 ) ∈ δ iff Ĝ(q, φ̂ : κ̂) c
⇒ (q0 , κ̂)
(q, κ̂, φ̂+ , q0 ) ∈ δ iff Ĝ(q, κ̂) c
⇒ (q0 , φ̂ : κ̂).

11 Problem: Reachability for Introspective Pushdown Systems is Uncomputable
As currently formulated, computing control-state reachability for introspective pushdown
systems is uncomputable. The problem is that the transition relation expects to enumerate
every possible stack for every control point at every transition, without restriction.
Theorem 11.1
Reachability in introspective pushdown systems is uncomputable.
Proof
Consider an IPDS with two states — searching (start state) and valid — and a singleton
stack alphabet of unit (>). For any first-order logic proposition, φ , we can define a reduction relation that interprets the length of the stack as an encoding of a proof of φ . If the
length encodes an ill-formed proof object, or is not a proof of φ , searching pushes > on
the stack and transitions to itself. If the length encodes a proof of φ , transition to valid.
By the completeness of first-order logic, if φ is valid, there is a finite proof, making the
pushdown system terminate in valid. If it is not valid, then there is no proof and valid
is unreachable. Due to the undecidability of first-order logic, we definitely cannot have a
decision procedure for reachability of IPDSs.
To make introspective pushdown systems computable, we must first refine our definition
of introspective pushdown systems to operate on sets of stacks and insist these sets be
regular.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

33

A conditional pushdown system (CPDS) is a quadruple M = (Q, Γ, δ , q0 ):
1. Q is a finite set of control states;
2. Γ is a stack alphabet;
3. δ ⊆fin Q × RE G (Γ∗ ) × Γ± × Q is a transition relation (same restriction on stacks);
and
4. q0 is a distinguished root control state,
where RE G (S) is the set of all regular languages formable with strings in S.
The regularity constraint on the transition relations guarantees that we can decide applicability of transition rules at each state, since (as we will see) the set of all stacks that reach
a state in a CPDS has decidable overlap with regular languages. Let CPDS denote the set
of all conditional pushdown systems.
The rules for reachability with respect to sets of stacks are similar to those for IPDSs.
(q, κ̂) 7−→∗ (q0 , κ̂ 0 ) κ̂ 0 ∈ K̂ 0
M

(q, κ̂) 7−→∗ (q, κ̂)

(q0 , K̂ 0 , g0 , q00 ) ∈ δ

(q, κ̂) 7−→∗ (q00 , [κ̂+0 g0 ])

M

M

K̂,g

We will write q 7−
−→
→ q0 to mean there are κ̂, K̂ such that q is reachable via κ̂, κ̂ ∈ K̂ and
M

(q, K̂, g, q0 ) ∈ δ . We will omit the labels above if they merely exist.
11.1 Garbage collection in conditional pushdown systems
Of course, we must adapt abstract garbage collection to this refined framework. To convert
the garbage-collecting, abstracted CESK machine into a conditional pushdown system, we
0
use the function I \
PDS : Exp → CPDS:
0

I\
PDS (e) = (Q, Γ, δ , q0 )
d × Store
[
Q = Exp × Env
\
Γ = Frame
[ let K̂ = {κ̂ : StackRoot(κ̂) = A}
For all sets of addresses A ⊆ Addr
(q, K̂, ε, q0 ) ∈ δ iff Ĝ(q, κ̂) c
⇒ (q0 , κ̂) for any κ̂ ∈ K̂
(q, K̂, φ̂− , q0 ) ∈ δ iff Ĝ(q, φ̂ : κ̂) c
⇒ (q0 , κ̂) for any φ̂ : κ̂ ∈ K̂
(q, K̂, φ̂+ , q0 ) ∈ δ iff Ĝ(q, κ̂) c
⇒ (q0 , φ̂ : κ̂) for any κ̂ ∈ K̂
(q0 , hi) = Iˆ(e).
Assuming we can overcome the difficulty of computing with some representation of a
set of stacks, the intuition for the decidability of control-state reachability with garbage
collection stems from two observations: garbage collection operates on sets of addresses,
and for any given control point there is a finite number of sets of sets of addresses. The
finiteness makes the definition of δ fit the finiteness restriction of CPDSs. The regularity of
K̂ (for any given A, which we recall are finite sets) is apparent from a simple construction:
let the DFA control states represent the subsets of A, with 0/ the start state and A the
accepting state. Transition from A0 ⊆ A to A ∪ T (φ̂ ) for each φ̂ (no transition if the result

ZU064-05-FPR

paper-jfp

34

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

is not a subset of A). Thus any string of frames that has a stack root of A (and only A) gets
accepted.
The last challenge to consider before we can delve into the mechanics of computing
reachable control states is how to represent the sets of stacks that may be paired with
each control state. Fortunately, a regular language can describe the stacks that share the
same root addresses, the set of stacks at a control point are recognized by a one-way
non-deterministic stack automaton (1NSA), and, fortuitously, non-empty overlap of these
two is decidable (but NP-hard (Rounds 1973)). The 1NSA describing the set of stacks
at a control point is already encoded in the structure of the (augmented) CRPDS that we
will accumulate while computing reachable control states. As we develop an algorithm for
control-state reachability, we will exploit this insight (Section 13).
12 Reachability in Conditional Pushdown Systems
We will show a progression of constructions that take us along the following line:
specialize

CPDS −−−→ CCPDS −−−−−→ PDCFA with GC → approx. PDCFA with GC
§12.2

§12.3

In the first construction, we show that a CCPDS is finitely constructible in a similar
fashion as in Section 7. The key is to take the current introspective CRPDS and “read off”
an automaton that describes the stacks accepted at each state. For traditional pushdown
systems, this is always an NFA, but introspection adds another feature: transition if the
string accepted so far is accepted by a given NFA. Such power falls outside of standard
NFAs and into one-way non-deterministic stack automata (1NSA)4 . These automata enjoy
closure under finite intersection with regular languages and decidable emptiness checking (Ginsburg et al. 1967), which we use to decide applicability of transition rules. If
the stacks realizable at q have a non-empty intersection with a set of stacks K̂ in a rule
(q, K̂, g, q0 ) ∈ δ , then there are paths from the start state to q that further reach q0 .
The structure of the GC problem allows us to sidestep the 1NSA constructions and more
directly compute state reachability. We specialize to garbage collection in subsection 12.3.
We finally show a space-saving approximation that our implementation uses.
12.1 One-way non-deterministic stack automata
The machinery we use for describing the realizable stacks at a state is a generalized
pushdown automaton itself. A stack automaton is permitted to move a cursor up and down
the stack and read frames (left and right on the input if two-way, only right if one-way),
but only push and pop when the stack cursor is at the top. Formally, a one-way stack
automaton is a 6-tuple A = (Q, Σ, Γ, δ , q0 , F) where
1.
2.
3.
4.
4

Q is a finite nonempty set of states,
Σ is a finite nonempty input alphabet,
Γ is a finite nonempty stack alphabet,
δ ⊆ Q × (Γ ∪ {ε}) × (Σ ∪ {ε}) × {↑, ·, ↓} × Γ± × Q is the transition relation,

The reachable states of a 1NSA is known to be regular, but the paths are not.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

35

5. q0 ∈ Q is the start state, and
6. F ⊆ Q the set of final states
An element of the transition relation, (q, φε , a, d, φ± , q0 ), should be read as, “if at q the
right of the stack cursor is prefixed by φε and the input is prefixed by a, then consume
a of the input, transition to state q0 , move the stack cursor in direction d, and if at the
top of the stack, perform stack action φ± .” This reading translates into a run relation
on instantaneous descriptions, Q × (Γ∗ × Γ∗ ) × Σ∗ . These descriptions are essentially
machine states that hold the current control state, the stack split around the cursor, and the
rest of the input.
(q, φε , a, d, φ± , q0 ) ∈ δ

φε v ΓT

w ≡ aw0

[Γ0B , Γ0T ] = P(φ± , D(d, [ΓB , ΓT ]))

(q, [ΓB , ΓT ], w) 7−→ (q0 , [Γ0B , Γ0T ], w0 )
where
P(φ+ , [ΓB , φε0 ]) = [ΓB φε0 , φ ]

D(↑, [ΓB , φ ΓT ]) = [ΓB φ , ΓT ]

P(φ− , [ΓB φ 0 , φ ]) = [ΓB , φ 0 ]

D(↓, [ΓB φ , ΓT ]) = [ΓB , φ ΓT ]

P(φ− , [ε, φ ]) = [ε, ε]
P(φ± , ΓB,T ) = ΓB,T

D(d, ΓB,T ) = ΓB,T

otherwise

otherwise

The meta-functions P and D perform the stack actions and direct the stack cursor,
respectively. A string w is thus accepted by a 1NSA A iff there are q ∈ F, ΓB , ΓT ∈ Γ∗
such that
(q0 , [ε, ε], w) 7−→∗ (q, [ΓB , ΓT ], ε)
Next we develop an introspective form of compact rooted pushdown systems that use
1NSAs for realizable stacks, and prove a correspondence with conditional pushdown systems.
12.2 Compact conditional pushdown systems
Similar to rooted pushdown systems, we say a conditional pushdown system G = (S, Γ, E, s0 )
is compact if all states, frames and edges are on some path from the root. We will refer to
this class of conditional pushdown systems as CCPDS. Assuming we have a way to decide
overlap between the set of realizable stacks at a state and a regular language of stacks, we
can compute the CCPDS in much the same way as in section 7.
F (M) = f , where
M = (Q, Γ, δ , q0 )
G

z }| {
f (S, Γ, E, s0 ) = (S0 , Γ, E 0 , s0 ), where
n
o
S0 = S ∪ s0 : s ∈ S and s 7−
−→
→ s0 ∪ {s0 }
M


K̂,g
K̂,g 0
0
0
E = E ∪ s  s : s ∈ S and s 7−
−→
→ s and Stacks(G)(s) ∩ K̂ 6= 0/ .
M

ZU064-05-FPR

paper-jfp

36

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

The function Stacks : CCPDS → S → 1NSA performs the stack extraction with a construction that inserts the stack-checking NFA for each reduction rule after it has run the
cursor to the bottom of the stack, and continues from the final states to the state dictated
by the rule (added by meta-function gadget). All the stack manipulations from s0 to s are
ε-transitions in terms of reading input; only once control reaches s do we check if the stack
is the same as the input, which captures the notion of a stack realizable at s. Once control
reaches s, we run down to the bottom of the stack again, and then match the stack against
the input; complete matches are accepted. To determine the bottom and top of the stack,
we add distinct sentinel symbols to the stack alphabet, ¢ and $.

G

z }| {
Stacks(S, Γ, E, s0 )(s) = (S ∪ S0 , Γ, Γ ∪ {¢, $} , δ , sstart , {sfinal }), where
sstart , sdown , scheck , sfinal fresh, and S0 , δ the smallest sets such that
{sstart , sdown , scheck , sfinal } ⊆ S0
(sstart , ε, ε, ·, ¢+ , s0 ) ∈ δ
0

gadget(s , K̂, γ± , s00 ) v (δ , S0 ) if (s0 , K̂, γ± , s00 ) ∈ E
(s, ε, ε, ·, $+ , sdown ) ∈ δ
(sdown , ε, ε, ↓, ε, sdown ) ∈ δ
(sdown , ¢, ε, ↑, ε, scheck ) ∈ δ
(scheck , a, a, ↑, ε, scheck ) ∈ δ , a ∈ Γ ∪ {ε}
(scheck , $, ε, ↑, ε, sfinal ) ∈ δ

The first rule changes the initial state to initialize the stack with the “bottom” sentinel.
Every reduction of the CPDS is given the gadget discussed above and explained below.
The last five rules are what implement the final checking of stack against input. When at
the state we are recognizing realizable stacks for, the machine will have the cursor at the
top of the stack, so we push the “top” sentinel before moving the cursor all the way down
to the bottom. When sdown finds the bottom sentinel at the cursor, it moves the cursor past
it to start the exact matching in scheck . If the cursor matches the input exactly, we consume
the input and move the cursor past the matched character to start again. When scheck finds
the top sentinel, it transitions to the final state; if the input is not completely exhausted, the
machine will get stuck and not accept.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

37

gadget(s, K̂, γ± , s0 ) = (δ 0 , Q ∪ {qdown , qout }) where
Let N = (Q, Σ, δ , q0 , F) be a fresh NFA recognizing K̂, qdown , qout fresh states
(q, a, ε, ↑, ε, q0 ) ∈ δ 0 if (q, a, q0 ) ∈ δ , a ∈ Σ
(q, ε, ε, ·, ε, q0 ) ∈ δ 0 if (q, ε, q0 ) ∈ δ
(q, $, ε, ·, $− , qout ) ∈ δ 0 if q ∈ F
(qout , ε, ε, ·, γ± , s0 ) ∈ δ 0
(s, ε, ε, ·, $+ , qdown ) ∈ δ 0
(qdown , ε, ε, ↓, ε, qdown ) ∈ δ 0
(qdown , ¢, ε, ↑, ε, q0 ) ∈ δ 0
We explain each rule in order. When the NFA that recognizes K̂ consumes a character,
the stack automaton should similarly read the character on the stack and move the cursor
along. If the NFA makes an ε-transition, the stack automaton should also, without moving
the stack cursor. When this sub-machine N is in a final state, the cursor should be at the
top of the stack (if indeed it matched), so we pop off the top sentinel and proceed to do
the stack action the IPDS does when transitioning to the next state. The last three rules
implement the same “run down to the bottom” gadget used before, when matching the
stack against the input.
Finally, we can show that states are reachable in a conditional pushdown system iff they
are reached in their corresponding CCPDS. Consider a map
C C : CPDS → CCPDS
such that given a conditional pushdown system M = (Q, Γ, δ , q0 ), its equivalent CCPDS is
C C (M) = (S, Γ, E, q0 ) where S contains reachable nodes:
o
n
S = q : (q0 , hi) 7−→∗ (q, κ̂)
M

and the set E contains reachable edges:


K̂,g
K̂,g
0
0
E = q  q : q 7−
−→
→ q
M

Theorem 12.1 (Computable reachability)
For all M ∈ CPDS, C C (M) = lfp(F (M))
Proof in Appendix 18.2.
Corollary 12.1 (Realizable stacks of CPDSs are recognized by 1NSAs)
For all M = (Q, Γ, δ , q0 ) ∈ CPDS, and (S, Γ, E, q0 ) = lfp(F (M)), (q0 , hi) 7−→∗ (q, κ̂) iff
M

q ∈ S and Stacks(G)(q) accepts κ̂.
12.3 Simplifying garbage collection in conditional pushdown systems
The decision problems on 1NSAs are computationally intractable in general, but luckily
GC is a special problem where we do not need the full power of 1NSAs. There are equally

ZU064-05-FPR

paper-jfp

6 February 2018

38

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

fˆe ((P̂, Ê), Ĥ) = ((P̂0 , Ê 0 ), Ĥ 0 ), where
(
Ê+ =

φ̂+

)
A

0

(ψ̂, A)  (ψ̂ , A ∪ T (φ̂ )) : ψ̂ + ψ̂

0

φ̂+

n
o
ε
A
Êε = (ψ̂, A)  (ψ̂ 0 , A) : ψ̂ + ψ̂ 0
ε


φ̂+
φ̂−
A
Ê− = (ψ̂ 00 , A)  (ψ̂ 000 , A0 ) : ψ̂ 00 + ψ̂ 000 and (ψ̂, A0 )  (ψ̂ 0 , A) ∈ Ê and (ψ̂ 0 , A)  (ψ̂ 00 , A) ∈ Ĥ
φ̂−
0

Ê = Ê+ ∪ Êε ∪ Ê−

Ĥε = Ω̂  Ω̂00 : Ω̂  Ω̂0 ∈ Ĥ and Ω̂0  Ω̂00 ∈ Ĥ

φ̂+
Ĥ+− = Ω̂  Ω̂000 : Ω̂  Ω̂0 ∈ Ê and Ω̂0  Ω̂00 ∈ Ĥ
φ̂−

and Ω̂00  Ω̂000 ∈ Ê
Ĥ 0 = Ĥε ∪ Ĥ+−
n
o
g
P̂0 = P̂ ∪ Ω̂0 : Ω̂  Ω̂0 ∪ {((e, ⊥, ⊥), 0)}
/ .

Fig. 8: An ε-closure graph-powered iteration function for pushdown garbage-collecting
control-flow analysis

precise techniques at much lower cost, and less precise techniques that can shrink the
explored state space.5 The transition relation we build does not enumerate all sets of
addresses, but instead queries the graph for the sets of addresses it should consider in
order to apply GC. A fully precise method to manage the stack root addresses is to add
the root addresses to the representation of each state, and update it incrementally. The
root addresses can be seen as the representation of K̂ in edge labels, but to maintain the
precision, the set must also distinguish control states. This addition to the state space is an
effective reification of the stack filtering that conditional performs.
An approximative method is to not distinguish control states, but rather to traverse the
graph backward through ε-closure edges and push edges, and collect the root addresses
through the pushed frames. As more paths are discovered to control states, more stacks
will be realizable there, which add more to the stack root addresses to consider as the
relation steps forward. For soundness, edges still must be labeled with the language of
stacks they are valid for, since they can become invalid as more stacks reach control states.
Notice that the root sets of addresses are isomorphic to languages of stacks that have the
given root set, so we can use sets of addresses as the language representation.
We consider both methods in turn, augmenting the compaction algorithm from subsection 9.5. Each have program states that consist of the expression, environment, and store;
d × Store.
\ = Exp × Env
[ Since GC is a non-monotonic operation, stores cannot
ψ̂ ∈ PState
5

The added precision of GC with tighter working sets makes the state space comparison between
the two approaches non-binary. Neither approach is clearly better in terms of performance.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

39

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

be shared globally without sacrificing the precision benefits of GC. For the first method,
program states additionally include the stack root set of addresses; we will call these
[ We show the non-worklist
\ = PState
\ × P(Addr).
ornamented program states, Ω̂ ∈ OPState
solution to computing reachability by employing the function fˆe defined in Figure 8.
A
In order to define the iteration function, we need a refactored transition relation + ⊆
g

\ × PState,
\ defined as follows:
PState
A

(e, ρ̂, σ̂ ) + (e0 , ρ̂ 0 , σ̂ 0 ) iff StackRoot(κ̂) = A and Ĝ(e, ρ̂, σ̂ , κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , φ̂ : κ̂)
φ̂+
A

(e, ρ̂, σ̂ ) + (e0 , ρ̂ 0 , σ̂ 0 ) iff StackRoot(φ̂ : κ̂) = A and Ĝ(e, ρ̂, σ̂ , φ̂ : κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , κ̂)
φ̂−
A
ε

(e, ρ̂, σ̂ ) + (e0 , ρ̂ 0 , σ̂ 0 ) iff StackRoot(κ̂) = A and Ĝ(e, ρ̂, σ̂ , κ̂) c
⇒ (e0 , ρ̂ 0 , σ̂ 0 , κ̂)

Theorem 12.2 (Correctness of GC specialization)
0
lfp( fˆe ) completely abstracts C C (I \
PDS (e))
The approximative method changes
to contain
 the representation of edges in the graph

[ = P PState
[ × Frame
\ × P(Addr)
\ . We also add
\ ± × PState
sets of addresses, Ê ∈ Edge
[ → (PState
[ to
\ → P(Addr))
\ → P(Addr)),
in a sub-fixed-point computation for tˆ : (PState
traverse the graph and collect the union of all stack roots for stacks realizable at a state.
Although we show a non-worklist solution here (in Figure 9) to not be distracting, this
solution will not compute the same reachable states as a worklist solution due to the evergrowing stack roots at each state. Only states in the worklist would need to be analyzed at
the larger stack root sets. In other words, the non-worklist solution potentially throws in
more live addresses at states that would otherwise not need to be re-examined.
This approximation is not an easily described introspective pushdown system since the
root sets it uses depend on the iteration state — particularly what frames have reached a
state so far, regardless of the stack filtering the original CPDS performs. The regular sets
of stacks acceptable at some state can be extracted a posteriori from the fixed point of the
function fˆe0 defined in Figure 9, if so desired. The next theorem follows from the fact that
R(ψ̂) ⊇ A for any represented (ψ̂, A).
Theorem 12.3 (Approximate GC is sound)
lfp( fˆe0 ) approximates lfp( fˆe ).
The last thing to notice is that by disregarding the filtering, the stack root set can get
larger and render previous GCs unsound, since more addresses can end up live than were
previously considered. Thus we label edges with the root set for which the GC was considered, in order to not make false predictions.
13 Implementing Introspective Pushdown Analysis with Garbage Collection
The reachability-based analysis for a pushdown system described in the previous section
requires two mutually-dependent pieces of information in order to add another edge:

ZU064-05-FPR

paper-jfp

6 February 2018

40

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

fˆe0 ((P̂, Ê), Ĥ) = ((P̂0 , Ê 0 ), Ĥ 0 ), where
(

)

A

A

0

ψ̂  ψ̂ : A = R(ψ̂), ψ̂ + ψ̂

Ê+ =

φ̂+

φ̂+



0

A

0

Êε = ψ̂  ψ̂ : A = R(ψ̂), ψ̂
ε

A
+ ψ̂ 0
ε




A
A
Ê− = ψ̂ 00  ψ̂ 000 : A = R(ψ̂ 00 ), ψ̂ 00 + ψ̂ 000 and
φ̂−

φ̂−

A0

ψ̂  ψ̂ 0 ∈ Ê and
φ̂+
0

ψ̂  ψ̂ 00 ∈ Ĥ
Ê 0 = Ê+ ∪ Êε ∪ Ê−

Ĥε = ψ̂  ψ̂ 00 : ψ̂  ψ̂ 0 ∈ Ĥ and ψ̂ 0  ψ̂ 00 ∈ Ĥ

A
Ĥ+− = ψ̂  ψ̂ 000 : ψ̂  ψ̂ 0 ∈ Ê and ψ̂ 0  ψ̂ 00 ∈ Ĥ
φ̂+
A0

and ψ̂ 00  ψ̂ 000 ∈ Ê
φ̂−
0

Ĥ = Ĥε ∪ Ĥ+−


A
P̂0 = P̂ ∪ ψ̂ 0 : ψ̂  ψ̂ 0 ∪ {(e, ⊥, ⊥)}
g
(
tˆ(R) = λ ψ̂.

0

0 A

( T (φ̂ ) ∪ R(ψ̂ ) : ψ̂  ψ̂ ∈ Ê

[

)

∪ R(ψ̂ 0 ) : ψ̂ 0  ψ̂ ∈ Ĥ )

φ̂+

R = lfp(tˆ).

Fig. 9: Approximate pushdown garbage-collecting control-flow analysis.

1. The topmost frame on a stack for a given control state q. This is essential for return
transitions, as this frame should be popped from the stack and the store and the
environment of a caller should be updated respectively.
2. Whether a given control state q is reachable or not from the initial state q0 along
realizable sequences of stack actions. For example, a path from q0 to q along edges
labeled “push, pop, pop, push” is not realizable: the stack is empty after the first pop,
so the second pop cannot happen—let alone the subsequent push.
Knowing about a possible topmost frame on a stack and initial-state reachability is
enough for a classic pushdown reachability summarization to proceed one step further,
and we presented an efficient algorithm to compute those in Section 8. However, to deal
with the presence of an abstract GC in a conditional PDS, we add:
3. For a given control state q, what are the touched addresses of all possible frames that
could happen to be on the stack at the moment the CPDS is in the state q?

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

41

The crucial addition to the algorithm is maintaining for each node q0 in the CRPDS a
~g

set of ε-predecessors, i.e., nodes q, such that q 7−
−→
→ q0 and [~g] = ε. In fact, only two out of
M

three kinds of transitions can cause a change to the set of ε-predecessors for a particular
node q: an addition of an ε-edge or a pop edge to the CRPDS.
One can notice a subtle mutual dependency between computation of ε-predecessors and
top frames during the construction of a CRPDS. Informally:
• A top frame for a state q can be pushed as a direct predecessor (e.g., q follows a
nested let-binding), or as a direct predecessor to an ε-predecessor (e.g., q is in tail
position and will return to a waiting let-binding).
ε
• When a new ε-edge q →
− q0 is added, all ε-predecessors of q become also ε-predecessors
of q0 . That is, ε-summary edges are transitive.
γ−

• When a γ− -pop-edge q −→ q0 is added, new ε-predecessors of a state q1 can be
obtained by checking if q0 is an ε-predecessor of q1 and examining all existing εpredecessors of q, such that γ+ is their possible top frame: this situation is similar to
the one depicted in the example above.
The third component—the touched addresses of all possible frames on the stack for a
state q—is straightforward to compute with ε-predecessors: starting from q, trace out only
the edges which are labeled ε (summary or otherwise) or γ+ . The frame for any action γ+
in this trace is a possible stack action. Since these sets grow monotonically, it is easy to
cache the results of the trace, and in fact, propagate incremental changes to these caches
when new ε-summary or γ+ nodes are introduced. This implementation strategy captures
the approximative approach to performing GC, as discussed in the previous section. Our
implementation directly reflects the optimizations discussed above.

14 Experimental Evaluation
A fair comparison between different families of analyses should compare both precision
and speed. We have implemented a version k-CFA for a subset of R5RS Scheme and
instrumented it with a possibility to optionally enable pushdown analysis, abstract garbage
collection or both. Our implementation source (in Scala) and benchmarks are available:
http://github.com/ilyasergey/reachability
In the experiments, we have focused on the version of k-CFA with a per-state store (i.e.,
without widening), as in the presence of single-threaded store, the effect of abstract GC
is neutralized due to merging. For non-widened versions of k-CFA, as expected, the fused
analysis does at least as well as the best of either analysis alone in terms of singleton flow
sets (a good metric for program optimizability) and better than both in some cases. Also
worthy of note is the dramatic reduction in the size of the abstract transition graph for the
fused analysis—even on top of the already large reductions achieved by abstract garbage
collection and pushdown flow analysis individually. The size of the abstract transition
graph is a good heuristic measure of the temporal reasoning ability of the analysis, e.g.,
its ability to support model-checking of safety and liveness properties (Might et al. 2007).

ZU064-05-FPR

paper-jfp

6 February 2018

42

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Program #e #v k
mj09

19

8

eta

21 13

kcfa2

20 10

kcfa3

25 13

blur

40 20

loop2

41 14

sat

51 23

0
1
0
1
0
1
0
1
0
1
0
1
0
1

k-CFA
83
107
454
812
63
74
33
33
194
236
970
1935
272
327
> 32662 > 88548
4686
7606
123
149
149
163
> 10867 > 16040
3844
5547
> 28432 > 37391

k-CFA + GC

k-PDCFA
4
1
4
8
3
1
4
–
4
10
7
–
4
–

38
38
44
48
32
32
32
31
36
35
87
144
58
63
1761 4046
115
146
94
101
69
73
411
525
545
773
12828 16846

4
36
39
1
34
35
6
28
27
8
28
27
4
35
34
2
35
34
5
53
52
2
53
52
4
90
95
10 76
82
7
43
46
3 151 163
4 1137 1543
4 958 1314

4
1
8
8
4
2
5
2
10
10
7
3
4
5

k-PDCFA + GC
33
32
28
28
35
35
53
53
68
75
34
145
254
71

32
31
27
27
34
34
52
52
76
81
35
156
317
73

4
1
8
8
4
2
5
2
10
10
7
3
4
10

Table 1: Benchmark results for toy programs. The first three columns provide the name
of a benchmark, the number of expressions and variables in the program in the ANF,
respectively. For each of eight combinations of pushdown analysis, k ∈ {0, 1} and garbage
collection on or off, the first two columns in a group show the number of control states
and transitions/CRPDS edges computed during the analysis (for both less is better). The
third column presents the amount of singleton variables, i.e, how many variables have a
single lambda flow to them (more is better). Inequalities for some results of the plain kCFA denote the case when the analysis explored more than 105 configurations (i.e., control
states coupled with continuations) or did not finish within 30 minutes. For such cases we
do not report on singleton variables.

14.1 Plain k-CFA vs. pushdown k-CFA
In order to exercise both well-known and newly-presented instances of CESK-based CFAs,
we took a series of small benchmarks exhibiting archetypal control-flow patterns (see
Table 1). Most benchmarks are taken from the CFA literature: mj09 is a running example
from the work of Midtgaard and Jensen designed to exhibit a non-trivial return-flow behavior (Midtgaard 2007), eta and blur test common functional idioms, mixing closures and
eta-expansion, kcfa2 and kcfa3 are two worst-case examples extracted from the proof of
k-CFA’s EXPTIME hardness (Van Horn and Mairson 2008), loop2 is an example from
Might’s dissertation that was used to demonstrate the impact of abstract GC (Might 2007,
Section 13.3), sat is a brute-force SAT-solver with backtracking.

14.1.1 Comparing precision
In terms of precision, the fusion of pushdown analysis and abstract garbage collection
substantially cuts abstract transition graph sizes over one technique alone.
We also measure singleton flow sets as a heuristic metric for precision. Singleton flow
sets are a necessary precursor to optimizations such as flow-driven inlining, type-check
elimination and constant propagation. It is essential to notice that for the experiments in

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

43

Table 1 our implementation computed the sets of values (i.e., closures) assigned to each
variable (as opposed to mere syntactic lambdas). This is why in some cases the results
computed by 0CFA appear to be better than those by 1CFA: the later one may examine
more states with different environments, which results in exploring more different values,
whereas the former one will just collapse all these values to a single lambda (Might et al.
2010). What is important is that for a fixed k the fused analysis prevails as the best-of- or
better-than-both-worlds.
Running on the benchmarks, we have re-validated hypotheses about the improvements to
precision granted by both pushdown analysis (Vardoulakis and Shivers 2010) and abstract
garbage collection (Might 2007). Table 1 contains our detailed results on the precision of
the analysis. In order to make the comparison fair, in the table we report on the numbers of
control states, which do not contain a stack component and are the nodes of the constructed
CRPDS. In the case of plain k-CFA, control states are coupled with stack pointers to obtain
configurations, whose resulting number is significantly bigger.
The SAT-solving benchmark showed a dramatic improvement with the addition of contextsensitivity. Evaluation of the results showed that context-sensitivity provided enough fuel
to eliminate most of the non-determinism from the analysis.

14.1.2 Comparing speed
In the original work on CFA2, Vardoulakis and Shivers present experimental results with
a remark that the running time of the analysis is proportional to the size of the reachable
states (Vardoulakis and Shivers 2010, Section 6). There is a similar correlation in our fused
analysis, but with higher variance due to the live address set computation GC performs.
Since most of the programs from our toy suite run for less than a second, we do not report
on the absolute time. Instead, the histogram on Figure 10 presents normalized relative
times of analyses’ executions. To our observation the pure machine-style k-CFA is always
significantly worse in terms of execution time than either with GC or push-down system,
so we excluded the plain, non-optimized k-CFA from the comparison.
Our earlier implementation of a garbage-collecting pushdown analysis (Earl et al. 2012)
did not fully exploit the opportunities for caching ε-predecessors, as described in Section 13. This led to significant inefficiencies of the garbage-collecting analyzer with respect
to the regular k-CFA, even though the former one observed a smaller amount of states and
in some cases found larger amounts of singleton variables. After this issue has been fixed,
it became clearly visible that in all cases the GC-optimized analyzer is strictly faster than
its non-optimized pushdown counterpart.
Although caching of ε-predecessors and ε-summary edges is relatively cheap, it is not
free, since maintaining the caches requires some routine machinery at each iteration of
the analyzer. This explains the loss in performance of the garbage-collecting pushdown
analysis with respect to the GC-optimized k-CFA.
As it follows from the plot, fused analysis is always faster than the non-garbage-collecting
pushdown analysis, and about a fifth of the time, it beats k-CFA with garbage collection in
terms of performance. When the fused analysis is slower than just a GC-optimized one, it is
generally not much worse than twice as slow as the next slowest analysis. Given the already

paper-jfp

6 February 2018

44

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

�����������������������������������
�����������������������������������

���
���
����
����

�������
�������
����������
����������
������������
������������

��
���
���
��
��
���
���
��

����
����

���
���

�����
�����

�����
�����

����
����

�����
�����

���
���

�����
�����

�����
�����

����
����

�����
�����

���
���

���
���
�����������������������������������
�����������������������������������

ZU064-05-FPR

����
����

�������
�������
����������
����������
������������
������������

��
���
���
��
��
���
���
��

����
����

���
���

Fig. 10: Analysis times relative to worst (= 1) in class; smaller is better. At the top is
the monovariant 0CFA class of analyses, at the bottom is the polyvariant 1CFA class of
analyses. (Non-GC k-CFA omitted.)

substantial reductions in analysis times provided by collection and pushdown analysis, the
amortized penalty is a small and acceptable price to pay for improvements to precision.

14.2 Analyzing real-world programs with garbage-collecting pushdown CFA
Even though our prototype implementation is just a proof of concept, we evaluated it not
on a suite of toy programs, tailored for particular functional programming patterns, but on a

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION
Program

#e

primtest 155
rsa
211
regex
344
scm2java 1135

#v !#v
44
93
150
460

16
36
44
63

k = 0, GC off
790 955 1400
1267 1507 2300
943 956 5400
376 375 1300

k = 0, GC on
113
355
578
376

k = 1, GC off

127 100 >43146 >54679 ∞
407 600
20746
28895 210
589 4500
1153
1179
8800
375 1300
376
375
1400

45

k = 1, GC on
442 562 1300
926 1166 2800
578 589 5000
376 375 1300

Table 2: Benchmark results of PDCFA on real-world programs. The first four columns
provide the name of a program, the number of expressions and variables in the program in
the ANF, and the number of singleton variables revealed by the analysis (same in all cases).
For each of four combinations of k ∈ {0, 1} and garbage collection on or off, the first two
columns in a group show the number of visited control states and edges, respectively, and
the third one shows absolute time of running the analysis (for both less is better). The
results of the analyses are presented in minutes (0 ) or seconds (00 ), where ∞ stands for an
analysis, which has been interrupted due to the an execution time greater than 30 minutes.

set of real-world programs. In order to set this experiment, we have chosen four programs,
dealing with numeric and symbolic computations:
• primtest – an implementation of the probabilistic Fermat and Solovay-Strassen
primality testing in Scheme for the purpose of large prime generation;
• rsa – an implementation of the RSA public-key cryptosystem;
• regex – an implementation of a regular expression matcher in Scheme using Brzozovski derivatives (Might et al. 2011; Owens et al. 2009);
• scm2java – scm2java is a Scheme to Java compiler;
We ran our benchmark suite on a 2.7 GHz Intel Core i7 OS X machine with 8 Gb
RAM. Unfortunately, k-CFA without global stores timed out on most of these examples
(i.e., did not finish within 30 minutes), so we had to exclude it from the comparison and
focus on the effect of a pushdown analyzer only. Table 2 presents the results of running the
benchmarks for k ∈ {0, 1} with a garbage collector on and off. Surprisingly, for each of the
six programs, those cases, which terminated within 30 minutes, found the same number
of global singleton variables.6 However, the numbers of observed states and runtimes are
indeed different in most of the cases except scm2java, for which all the four versions of
the analysis were precise enough to actually evaluate the program: happily, there was no
reuse of abstract addresses, which resulted in the absence of forking during the CRPDS
construction. In other words, the program scm2java, which used no scalar data but strings
being concatenated and was given a simple input, has been evaluated precisely, which is
confirmed by the number of visited control states and edges.
Time-wise, the results of the experiment demonstrate the general positive effect of the
abstract garbage collection in a pushdown setting, which might improve the analysis performance by more than two orders of magnitude.
6

Of course, the numbers of states explored for each program by different analyses were different,
and there were variations in function parameters cardinalities, which we do not report on here.

ZU064-05-FPR

paper-jfp

46

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
15 Discussion: Applications

Pushdown control-flow analysis offers more precise control-flow analysis results than the
classical finite-state CFAs. Consequently, introspective 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 control-flow analysis. Perhaps not surprisingly, the best
examples of such 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 introspective pushdown control-flow analysis. (We leave an indepth formulation and study of these analyses to future work.)

15.1 Escape analysis
In escape analysis, the objective is to determine whether a heap-allocated 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 compact rooted pushdown system 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.

15.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 (2009) showed
that if one has knowledge of the program stack, then one can uncover interprocedural
dependencies. We can adapt that technique to work with compact rooted pushdown systems. 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 readdependence 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. In control-flow terms, this translates to “if f calls g and g accesses a, then f also
accesses a.”

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

47

16 Related Work
The Scheme workshop presentation of PDCFA (Earl et al. 2010) is not archival, nor were
there rigorous proofs of correctness. The complete development of pushdown analysis from
first principles stands as a new contribution, and it constitutes an alternative to CFA2. It
goes beyond work on CFA2 by specifying specific mechanisms for reducing the complexity
to polynomial time (O(n6 )) as well. Vardoulakis (2012) sketches an approach to regain
polynomial time in his dissertation, but does not give a precise bound. An immediate advantage of the complete development is its exposure of parameters for controlling polyvariance and context-sensitivity. An earlier version of this work appeared in ICFP 2012 (Earl
et al. 2012). We also provide a reference implementation of control-state reachability in
Haskell. We felt this was necessary to shine a light on the “dark corners” in the formalism,
and in fact, it helped expose both bugs and implicit design decisions that were reflected
in the revamped text of this work. The development of introspective pushdown systems is
also more complete and more rigorous. We expose the critical regularity constraint absent
from the ICFP 2012 work, and we specify the implementation of control-state reachability
and feasible paths for conditional pushdown systems in greater detail. More importantly,
this work uses additional techniques to improve the performance of the implementation
and discusses those changes.
Garbage-collecting pushdown control-flow analysis draws on work in higher-order controlflow analysis (Shivers 1991), abstract machines (Felleisen and Friedman 1987) and abstract
interpretation (Cousot and Cousot 1977).

Context-free analysis of higher-order programs The motivating work for our own is
Vardoulakis and Shivers recent discovery of CFA2. 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 exploits context-free languages, contextfree languages are not explicit in its formulation in the same way that pushdown systems
are explicit in our presentation of pushdown flow analysis. With respect to CFA2, our pushdown flow analysis is also polyvariant/context-sensitive (whereas CFA2 is monovariant/contextinsensitive), and it covers direct-style.
On the other hand, CFA2 distinguishes stack-allocated and store-allocated variable bindings, whereas our formulation of pushdown control-flow analysis does not: it 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. While we could incorporate such a feature in our formulation, it
is not necessary for achieving “pushdownness,” and in fact, it could be added to classical
finite-state CFAs as well.
CFA2 has a follow-up that sacrifices its complete abstraction with the machine that only
abstracts bindings in order to handle first-class control (Vardoulakis and Shivers 2011).
We do not have an analogous construction since loss of complete abstraction was an antigoal of this work. We leave an in-depth study of generalizations of CFA2’s method to
introspection, polyvariance and other control operators to future work.

ZU064-05-FPR

paper-jfp

48

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Calculation approach to abstract interpretation Midtgaard and Jensen (2009) systematically calculate 0CFA using the Cousot-style calculational approach to abstract interpretation (Cousot 1999) 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 reachablestates 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 analysis when the latter mapping is
omitted and the stack component of the machine is not abstracted. However, not abstracting
the stack requires non-trivial mechanisms to compute the compaction of the pushdown
system.
CFL- and pushdown-reachability techniques This work also draws on CFL- and pushdownreachability 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 our analysis, we implicitly invoked these methods as subroutines. When we found these algorithms lacking (as
with their enumeration of control states), we developed rooted pushdown system compaction.
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 Fähndrich’s method is cubic in the size of the typed program, but the
types may be exponential in the size of the program. Finally, our technique is not restricted
to typed programs.
Model-checking pushdown systems with checkpoints A pushdown system with checkpoints has designated finite automata for state/frame pairs. If in a given state/frame configuration, and the automaton accepts the current stack, then execution continues. This
model was first created in Esparza et al. (2003) and describes its applications to modelchecking programs that use Java’s AccessController class, and performing better dataflow analysis of Lisp programs with dynamic scope, though the specific applications are
not fully explored. The algorithm described in the paper is similar to ours, but not “on-thefly,” however, so such applications would be difficult to realize with their methods. The
algorithm discussed has multiple loops that enumerate all transitions within the pushdown
system considered. Again this is a non-starter for higher-order languages, since up-front
enumeration would conservatively suggest that any binding called would resolve to any
possible function. This strategy is a sure-fire way to destroy precision and performance.
Meet-over-all-paths for conditional weighted pushdown systems A conditional pushdown system is essentially a pushdown system in which every state/frame pair is a check-

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

49

point. The two are easily interchangeable, but weighted conditional pushdown systems
assign weights to reduction rules from a bounded idempotent semiring in the same manner
as Reps et al. (2005). The work that introduces CWPDSs uses them for points-to analysis
for Java. They solve the meet-over-all-paths problem by an incrementally translating a
skeleton CFG into a WPDS and using WPDS++ (Lal and Reps 2006) to discover more
points-to information to fill in call/return edges. The translation involves a heavy encoding
and is not obviously correct. The killer for its use for GC is that it involves building
the product automaton of all the (minimized) condition automata for the system, and
interleaving the system states with the automaton’s states — there are exponentially many
such machines in our case, and even though the overall solution is incremental, this large
automaton is pre-built. It is not obvious how to incrementalize the whole construction, nor
is it obvious that the precision and performance are not negatively impacted by the repeated
invocation of the WPDS solver (as opposed to a work-set solution that only considers
recently changed states).
The approach to incremental solving using first-order tools is an interesting approach
that we had not considered. Perhaps first-order and higher-order methods are not too far
removed. It is possible that these frameworks could be extended to request transitions —
or even further, checkpoint machines — on demand in order to better support higher-order
languages. As we saw in this article, however, we needed access to internal data structures
to compute root sets of addresses, and the ability to update a cache of such sets in these
structures. The marriage could be rocky, but worth exploring in order to unite the two
communities and share technologies.
Model-checking higher-order recursion schemes There is terminology overlap with
work by Kobayashi (2009) on model-checking 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 order-0 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. In particular, higher-order recursions
schemes are limited to model-checking programs in the simply-typed lambda-calculus with
recursion.

17 Conclusion
Our motivation was to further probe the limits of decidability for pushdown flow analysis
of higher-order programs by enriching it with abstract garbage collection. We found that
abstract garbage collection broke the pushdown model, but not irreparably so. By casting
abstract garbage collection in terms of an introspective pushdown system and synthesizing

ZU064-05-FPR

paper-jfp

50

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

a new control-state reachability algorithm, we have demonstrated the decidability of fusing
two powerful analytic techniques.
As a byproduct of our formulation, it was also easy to demonstrate how polyvariant/contextsensitive flow analyses generalize to a pushdown formulation, and we lifted the need to
transform to continuation-passing style in order to perform pushdown analysis.
Our empirical evaluation is highly encouraging: it shows that the fused analysis provides further large reductions in the size of the abstract transition graph—a key metric for
interprocedural control-flow precision. And, in terms of singleton flow sets—a heuristic
metric for optimizability—the fused analysis proves to be a “better-than-both-worlds”
combination.
Thus, we provide a sound, precise and polyvariant introspective pushdown analysis for
higher-order programs.
Acknowledgments
We thank the anonymous reviewers of ICFP 2012 and JFP for their detailed reviews, which
helped to improve the presentation and technical content of the paper. Tim Smith was
especially helpful with his knowledge of stack automata. This material is based on research
sponsored by DARPA under the programs Automated Program Analysis for Cybersecurity (FA8750-12-2-0106) and Clean-Slate Resilient Adaptive Hosts (CRASH). The U.S.
Government is authorized to reproduce and distribute reprints for Governmental purposes
notwithstanding any copyright notation thereon.
References
Bouajjani, A., J. Esparza, and O. Maler (1997). Reachability analysis of pushdown
automata: Application to Model-Checking. In Proceedings of the 8th International
Conference on Concurrency Theory, CONCUR ’97, pp. 135–150. Springer-Verlag.
Cousot, P. (1999). The calculational design of a generic abstract interpreter. In M. Broy and
R. Steinbrüggen (Eds.), Calculational System Design. NATO ASI Series F. IOS Press,
Amsterdam.
Cousot, P. and R. Cousot (1977). 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, pp.
238–252. ACM Press.
Earl, C., M. Might, and D. Van Horn (2010). Pushdown Control-Flow analysis of HigherOrder programs. In Workshop on Scheme and Functional Programming.
Earl, C., I. Sergey, M. Might, and D. Van Horn (2012). Introspective pushdown analysis
of higher-order programs. In Proceedings of the 17th ACM SIGPLAN International
Conference on Functional Programming (ICFP 2012), ICFP ’12, pp. 177–188. ACM.
Esparza, J., A. Kucera, and S. Schwoon (2003). Model checking LTL with regular
valuations for pushdown systems. Inf. Comput. 186(2), 355–376.
Felleisen, M. and D. P. Friedman (1987). A calculus for assignments in higher-order
languages. In POPL ’87: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium
on Principles of Programming Languages, pp. 314+. ACM.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

51

Flanagan, C., A. Sabry, B. F. Duba, and M. Felleisen (1993, June). The essence of
compiling with continuations. In PLDI ’93: Proceedings of the ACM SIGPLAN 1993
Conference on Programming Language Design and Implementation, pp. 237–247.
ACM.
Ginsburg, S., S. A. Greibach, and M. A. Harrison (1967). One-way stack automata. Journal
of the ACM 14(2), 389–418.
Johnson, J. I. and D. Van Horn (2013). Concrete semantics for pushdown analysis: The
essence of summarization. In HOPA 2013: Workshop on higher-order program analysis.
Kobayashi, N. (2009, January). Types and higher-order recursion schemes for verification
of higher-order programs. SIGPLAN Not. 44(1), 416–428.
Kodumal, J. and A. Aiken (2004, June). The set constraint/CFL reachability connection
in practice. In PLDI ’04: Proceedings of the ACM SIGPLAN 2004 Conference on
Programming Language Design and Implementation, pp. 207–218. ACM.
Lal, A. and T. W. Reps (2006). Improving pushdown system model checking. In T. Ball
and R. B. Jones (Eds.), CAV, Volume 4144 of Lecture Notes in Computer Science, pp.
343–357. Springer.
Li, X. and M. Ogawa (2010). Conditional weighted pushdown systems and applications.
In J. P. Gallagher and J. Voigtländer (Eds.), PEPM, pp. 141–150. ACM.
Melski, D. and T. W. Reps (2000, October). Interconvertibility of a class of set constraints
and context-free-language reachability. Theoretical Computer Science 248(1-2), 29–98.
Midtgaard, J. (2007). Transformation, Analysis, and Interpretation of Higher-Order
Procedural Programs. Ph. D. thesis, University of Aarhus.
Midtgaard, J. and T. P. Jensen (2009). 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, pp. 287–298. ACM.
Might, M. (2007, June). Environment Analysis of Higher-Order Languages. Ph. D. thesis,
Georgia Institute of Technology.
Might, M., B. Chambers, and O. Shivers (2007, January). Model checking via GammaCFA. In Verification, Model Checking, and Abstract Interpretation, pp. 59–73.
Might, M., D. Darais, and D. Spiewak (2011). Parsing with derivatives: a functional
pearl. In ICFP ’11: Proceeding of the 16th ACM SIGPLAN international conference
on Functional Programming, pp. 189–195. ACM.
Might, M. and P. Manolios (2009). A posteriori soundness for non-deterministic abstract
interpretations. In Proceedings of the 10th International Conference on Verification,
Model Checking, and Abstract Interpretation, VMCAI ’09, pp. 260–274. SpringerVerlag.
Might, M. and T. Prabhu (2009). Interprocedural dependence analysis of higher-order
programs via stack reachability. In Proceedings of the 2009 Workshop on Scheme and
Functional Programming.
Might, M. and O. Shivers (2006a). Environment analysis via Delta-CFA. In Conference
Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL 2006), pp. 127–140. ACM.
Might, M. and O. Shivers (2006b). Improving flow analyses via Gamma-CFA: Abstract
garbage collection and counting.
In Proceedings of the 11th ACM SIGPLAN
International Conference on Functional Programming (ICFP 2006), pp. 13–25. ACM.

ZU064-05-FPR

paper-jfp

52

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Might, M., Y. Smaragdakis, and D. Van Horn (2010). Resolving and exploiting the kCFA paradox: Illuminating functional vs. object-oriented program analysis. In PLDI
’10: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language
Design and Implementation, PLDI ’10, pp. 305–315. ACM Press.
Ong, C. H. L. (2006). On Model-Checking trees generated by Higher-Order recursion
schemes. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06),
LICS, pp. 81–90. IEEE.
Owens, S., J. Reppy, and A. Turon (2009). Regular-expression derivatives re-examined.
Journal of Functional Programming 19(02), 173–190.
Rehof, J. and M. Fähndrich (2001). Type-based flow analysis: From polymorphic
subtyping to CFL-reachability. In POPL ’01: Proceedings of the 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 54–66. ACM.
Reps, T. (1998, December). Program analysis via graph reachability. Information and
Software Technology 40(11-12), 701–726.
Reps, T., S. Schwoon, S. Jha, and D. Melski (2005, October). Weighted pushdown
systems and their application to interprocedural dataflow analysis. Science of Computer
Programming 58(1-2), 206–263.
Rounds, W. C. (1973). Complexity of recognition in intermediate level languages. In
Switching and Automata Theory, 1973. SWAT ’08. IEEE Conference Record of 14th
Annual Symposium on, pp. 145–158.
Shivers, O. G. (1991). Control-Flow Analysis of Higher-Order Languages. Ph. D. thesis,
Carnegie Mellon University.
Sipser, M. (2005, February). Introduction to the Theory of Computation (2 ed.). Cengage
Learning.
Van Horn, D. and H. G. Mairson (2008). Deciding kCFA is complete for EXPTIME.
In ICFP ’08: Proceeding of the 13th ACM SIGPLAN International Conference on
Functional Programming, pp. 275–282. ACM.
Van Horn, D. and M. Might (2012). Systematic abstraction of abstract machines. Journal
of Functional Programming 22(Special Issue 4-5), 705–746.
Vardoulakis, D. (2012). CFA2: Pushdown Flow Analysis for Higher-Order Languages. Ph.
D. thesis, Northeastern University.
Vardoulakis, D. and O. Shivers (2010). CFA2: A Context-Free approach to ControlFlow analysis. In A. D. Gordon (Ed.), Programming Languages and Systems, Volume
6012 of Lecture Notes in Computer Science, Chapter 30, pp. 570–589. Springer Berlin
Heidelberg.
Vardoulakis, D. and O. Shivers (2011). Pushdown flow analysis of first-class control.
In Proceedings of the 16th ACM SIGPLAN International Conference on Functional
Programming, ICFP ’11, pp. 69–80. ACM.
Wright, A. K. and S. Jagannathan (1998, January). Polymorphic splitting: An effective
polyvariant flow analysis. ACM Transactions on Programming Languages and
Systems 20(1), 166–207.

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

53

18 Full Proofs
18.1 Pushdown reachability
Proof of Theorem 8.1. The space ICRPDS is further constrained than stated in the main
article:


S
{{s, s0 } : s  s0 ∈ H} ⊆ S,
ICRPDS = ((S, E), H, (∆S, ∆E, ∆H)) :
∆S ∩ S = 0,
/ ∆E ∩ E = 0,
/ and ∆H ∩ H = 0/
For this section we assume
M = (Q, Γ, δ , q0 ) ∈ RPDS
G = ((S, E), H, (∆S, ∆E), ∆H) ∈ CRPDS where (S, E) ⊆ (Q, δ )
and q0 = s0
Let ORD be the class of ordinal numbers. We define a termination measure on the fixedpoint computation of F 0 ((Q, Γ, , )), d : CRPDS → ORD.
2 ·|Γ|

d((S, E), H, (∆S, ∆E, ∆H)) = (2|Q|

2

− |E|)ω + (2|Q| − |H|)

Lemma 18.1 (Termination)
Either G = F 0 (M)(G) or d(F 0 (M)(G)) ≺ d(G)
Proof
If both ∆E and ∆H are empty, there are no additions made to S, E or H, meaning G is a
fixed point. Otherwise, due to the non-overlap condition, one or both of E and H grow,
meaning the ordinal is smaller.
A corollary is that the fixed-point has empty ∆E and ∆H.
Lemma 18.2 (Key lemma for PDS reachability)
If inv(G) then inv(F 0 (M)(G))
Proof
All additional states and edges come from ∆Ei and ∆Hi for i ∈ [0..4], so by cases on the
sources of edges:
g

Case s  s0 ∈ ∆E0 , s00  s000 ∈ ∆H0 .
By definition of sprout and path extension.
g
Case s  s0 ∈ ∆E1 , s00  s000 ∈ ∆H1 .
φ̂+

If g ≡ φ̂− , then by definition of addPush there are q  q0 ∈ ∆E, q0  s ∈ H, such
that (s, φ̂+ , s0 ) ∈ δ .
Let ~g be the witness of the invariant on q0  s given from definition of inv. Let κ̂ be
φ̂+~gφ̂−

arbitrary. We have [φ̂+~gφ̂− ] = ε. We also have (q, κ̂) 7−→∗ (s0 , κ̂). Root reachability
M

φ̂+

follows from path concatenation with the root path from (q, κ̂) 7−→ (q0 , φ̂ κ̂) from
M

inv.
The balanced path for s00  s000 comes from a similar push edge from ∆E and
concatenation with the path from the invariant on H.

ZU064-05-FPR

paper-jfp

6 February 2018

54

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Case s00  s000 ∈ ∆H2 .
φ̂−

By definition of addPop, ∆E2 = 0/ and there are q  s000 ∈ ∆E, q0  q ∈ H such that
φ̂+

s00  q0 ∈ E. Let ~g be the witness of the invariant on q0  q. Let κ̂ be arbitrary. We
φ̂+~gφ̂−

know by the invariant on E, (s00 , κ̂) 7−→∗ (s000 , κ̂) and [φ̂+~gφ̂− ] = ε.
M

g

s0

, s00

s000

Case s  ∈ ∆E3 ∪ ∆E4
 ∈ ∆H3 ∪ ∆H4 .
Follows from definition of inv and path concatenation, following similar reasoning
as above cases.

We define “π is a subtrace of π 0 ,” π v π 0
~g ∗

π v (s, κ̂) 7−→ (s0 , κ̂ 0 ) (s0 , g0 , s00 ) ∈ δ
hi ∗

~g ∗

(s0 , κ̂ 0 ) 7−→ (s0 , κ̂ 0 ) v (s, κ̂) 7−→ (s0 , κ̂ 0 )
M

M

M
~g ∗

g0

M

M

π v (s, κ̂) 7−→ (s0 , κ̂ 0 ) 7−→ (s00 , [κ̂+0 g0 ])
∗
g~00

~g ∗

(s, κ̂) 7−→ (s0 , κ̂ 0 ) v (s000 , κ̂ 00 ) 7−→ (s0 , κ̂ 0 ) (s0 , g0 , s00 ) ∈ δ
M
M
∗
g0
g~00
0
0
00
0
0
(s , κ̂ ) 7−→ (s , [κ̂+ g ]) v (s000 , κ̂ 00 ) 7−→
M
M

~g ∗

(s, κ̂) 7−→
M

g0

(s0 , κ̂ 0 ) 7−→ (s00 , [κ̂+0 g0 ])
M

Theorem 8.1 is a corollary of the following theorem.
Theorem 18.1
lfp(F 0 (M)) = (C (M), E C G (M), (0,
/ 0),
/ 0)
/
Proof
(⊆): Directly from 18.2.

~g ∗

(⊇): Let π ≡ (s0 , hi) 7−→ (s, κ̂) be an arbitrary path in C (M) (the inclusion of root is not
M

a restriction due to the definition of CRPDSs). Let n ∈ Nats be such that lfp(F 0 (M)) =
F 0 (M)n . We show
• the same path through G,
g

g

• for each s ∈ S, s  s0 ∈ E, s  s0 ∈ H, there is an m < n such that s ∈ ∆Sm s  s0 ∈
∆Em s  s0 ∈ ∆Hm respectively, where F 0 (M)m = (Gm , Hm , (∆Sm , ∆Em , ∆Hm )), and
g~ε ∗

• all non-empty balanced subtraces have edges in H: ∀(sb , κ̂) 7−→ (sa , κ̂) v π.~
gε 6=
M

hi ∧ [~
gε ] = ε =⇒ sb  sa ∈ H.
By induction on π,
Case Base: s0 .
Follows by definition of F 0 . No non-empty balanced subtrace.
~g0 ∗

g00

M

M

Case Induction step: (s0 , hi) 7−→ (s0 , κ̂) 7−→ (s, [κ̂+ g00 ]).
~g0 ∗

By IH, (s0 , hi) 7−→
G

(s0 , κ̂).

By cases on g00 :

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

55

Case γ+ .
g00

Let m be the witness for s0 by the IH. By definition of F 0 , (s0 , κ̂) 7−→ (s, [κ̂+ g00 ])
M

is in ∆Em+1 and Em+2 (and thus s ∈ ∆Sm+1 and Sm+2 ). Thus the path is constructible through Gn . All balanced subtraces carry over from IH, since the last
push edge cannot end a balanced path.
Case ε.
The path is constructible the same as γ+ . Let m be the witness used in the path
g~ε ∗

construction. Let π 0 ≡ (sb , κ̂) 7−→ (se , κ̂) be an arbitrary non-empty balanced
M

subtrace. If se 6= s, then the IH handles it. Otherwise, g~ε = g~0ε ε. If sb = s0 , then
the ε-edge is added by sprout (so the witness number is m + 1). If not, then there
∗
g~0

ε
is a balanced subtrace (sb , κ̂) 7−→
(s0 , κ̂), thus sb  s0 ∈ H. Let m0 be the witness

M

for sb  s0 ∈ ∆Hm0 . Then sb  s ∈ ∆max{m,m0 }+1 by definition of addEmpty.
Case γ− .
γ+

Since [~g] is defined, there is a push edge in the trace (call it su 7−→ sv ) with a
M

(possibly empty) balanced subtrace following to s0 . Thus by IH, there are some
γ+

m, m0 such that su  sv ∈ Em , (if the subtrace is non-empty) sv  s0 ∈ Hm0 If
γ−

m ≥ m0 by definition of addPush, s0  s ∈ ∆Em+1 . Otherwise, the edge is in Em0
γ−

and by definition of addEmpty, s0  s ∈ ∆Em0 +1 .
g~ε ∗

Let π 0 ≡ (sb , κ̂) 7−→ (se , κ̂) be an arbitrary non-empty balanced subtrace. If se 6=
M

∗
g~0

γ+

M

M

ε
(su , κ̂) 7−→
s, the IH handles it. Otherwise, g~ε = g~0ε γ+ g~00ε γ− and π 0 ≡ (sb , κ̂) 7−→

∗
g~0ε

γ−

M

M

(sv , γ κ̂) 7−→ (s0 , γ κ̂) 7−→ (s, κ̂). su  s is added to ∆Hmax{m,m0 }+1 and thus sb 
su is in Hmax{m,m0 }+3 .

18.2 RIPDS reachability
We use metafunction •++• : Cont × Cont → Cont to aid proofs:
ε++κ̂ = κ̂
φ : κ̂++κ̂ 0 = φ : (κ̂++κ̂ 0 )

split(ε) = [¢, ε]
split(φ : κ̂) = [¢κ̂, φ ]
Lemma 18.3 (Down spin)
For (q, ε, ε, ↓, ε, q) ∈ δ , (q, [κ̂B ++κ̂B0 , κ̂T ], w) 7−→∗ (q, [κ̂B , κ̂B0 ++κ̂T ], w)
Proof
By induction on κ̂B0 .

ZU064-05-FPR

paper-jfp

6 February 2018

56

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

Case Base: κ̂B = ε.
Reflexivity.
Case Induction step: κ̂B0 = κ̂φ .
By δ , (q, [κ̂B ++κ̂B0 , κ̂T ], w) 7−→ (q, [κ̂B ++κ̂, φ κ̂T ], w). By IH, (q, [κ̂B ++κ̂, φ κ̂T ], w)
7−→∗ (q, [κ̂B , κ̂++φ κ̂T ], w). This final configuration is the same as (q, [κ̂B , κ̂B0 ++κ̂T ], w).

Lemma 18.4 (gadget correctness)
For (δ , S) = gadget(s, K̂, g, s0 ), (s, split(κ̂), w) 7−→∗ (s0 , split([κ̂+ g]), w) iff κ̂ ∈ K̂ and [κ̂+ g]
δ

defined.
Proof
(⇒): By inversion on the rules for δ , the path must go through three stages: the downspin, the middle path, and the pop-off. By 18.3, (s, split(κ̂), w) 7−→ (qdown , [¢κ̂, $], w) 7−→∗
(qdown , [ε, ¢κ̂$], w). Then the (qdown , ¢, ε, ↑, ε, q0 ) rule must apply. We can construct an accepting path in the machine recognizing K̂ from the middle path via the following lemma:
κ̂ 0

κ̂ 0

δ

N

(q0 , [¢, κ̂$], w) 7−→∗ (q, [¢κ̂ 0 , κ̂ 00 $], w) implies (q0 , κ̂) 7−→∗ (q, κ̂ 00 ). Proof by induction.
Then (q, $, ε, ·, $− , qout ) must apply, and then (qout , ε, ε, g, s0 ) must apply, meaning that
[κ̂+ g] is defined.
(⇐): Since K̂ is regular, there must be a path in the chosen NFA N = (Q, Σ, δN , q0 , F)
from q0 to a final state q ∈ F, (q0 , κ̂) 7−→∗ (q, ε).
N

In the first stage, (s, split(κ̂), w) 7−→∗ (q0 , [¢, κ̂$], w).
The follows first by the (s, ε, ε, ·, $+ , qdown ) transition, then by 18.3 (qdown , split(κ̂$), w)
7−→∗ (qdown , [ε, ¢κ̂$], w), finally by the (qdown , ¢, ε, ↑, ε, q0 ) rule.
In the second stage we construct a path (q0 , [¢, κ̂$], w) 7−→∗ (q, [¢κ̂, $], w), from an accepting path in N: (q0 , κ̂) 7−→∗ (q, ε) where q ∈ F. The statement we can induct on to get this
κ̂ 0

κ̂ 0

is (q0 , κ̂) 7−→∗ (q, κ̂ 00 ) implies (q0 , [¢, κ̂$], w) 7−→∗ (q, [¢κ̂ 0 , κ̂ 00 $], w).
N

δ

κ̂ 0

Case Base: = ε, q = q0
Reflexivity.

, κ̂ 00

= κ̂.
κ̂ 000

φε

Case Induction step: κ̂ 0 = κ̂ 000 φε , (q0 , κ̂) 7−→∗ (q0 , κ̂ 0000 ) 7−→ (q, κ̂ 00 ).
N
7 →∗ (q0 , [¢κ̂ 000 , κ̂ 0000 $], w).
−

N

By IH, (q0 , [¢, κ̂$], w)
If φε = ε, then κ̂ 000 = κ̂ 0 , κ̂ 0000 = κ̂ 00
0
and we apply the (q , ε, ε, ·, ε, q) rule to get to (q, [¢κ̂ 0 , κ̂ 00 $], w). Otherwise, κ̂ 0 = κ̂ 000 φ
and we apply the (q0 , φ , ε, ↑, ε, q) rule to get to (q, [¢κ̂ 0 , κ̂ 00 $], w).
In the third and final stage, (qout , [¢κ̂, $], w) 7−→ (qout , split(κ̂), w) and since [κ̂+ g] is defined, we reach the final state by (qout , ε, ε, ·, g, s0 ).
Lemma 18.5 (Checking lemma)
If (q, a, a, ↑, ε, q) ∈ δ and (q, [κ̂B , κ̂T 0 ++κ̂T $], w) 7−→∗ (q, [κ̂B ++κ̂T 0 , κ̂T $], w0 ) (through
the one rule) then w = κ̂T 0 w0 .

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

57

Proof
Simple induction.

Lemma 18.6 (Stack machine correctness)
For all M ∈ CPDS, G ∈ CCPDS, q ∈ G, if G v C C (M) then


−→


K̂,g
L (Stacks(G)(q)) = κ̂ : (q0 , hi) 7−→∗ (q, κ̂) .


G
Proof
(⊆): Let (sstart , [ε, ε], κ̂) 7−→∗ (sfinal , split(κ̂), ε) be an accepting path for κ̂ ∈ L (Stacks(G)(q)).
We inductively construct a corresponding path in G that realizes κ̂. We first see that the
given path is split into three phases: setup, gadgetry, checking. The first step must be
(sstart , ε, ε, ·, ¢+ , s0 ), which we call setup. The only final state must be preceded by scheck ,
sdown , and the final occurrence of s, which we call checking. Thus the middle phase is a
trace from s0 to s. This must be through gadgets, which are disjoint for each rule of the
IPDS, and thus each edge in G.
(sstart , [ε, ε], κ̂) 7−→ (s0 , [ε, ¢], κ̂) 7−→∗ (s, split(κ̂), κ̂) 7−→
(sdown , [¢κ̂, $], κ̂) 7−→∗ (sdown , [ε, ¢κ̂$], κ̂) 7−→
(scheck , [¢, κ̂$], κ̂) 7−→∗ (scheck , [¢κ̂, $], ε) 7−→ (sfinal , split(κ̂), ε)
We induct on the path through gadgets, s0 to s in the above path, invoking 18.4 at each step.
(⊇): Simple induction between setup and teardown, applying 18.4.

Proof of Theorem 12.1

Proof
The finiteness of the state space and monotonicity of F ensures the least fixed point exists.
lfp(F (M)) ⊆ C C (M) follows from 18.6 and the definition of F .
−→ ∗
K̂,g

To prove C C (M) ⊆ lfp(F (M)), suppose not. Then there must be a path (s0 , hi) 7−→
M

K̂ 0 ,g0

(s, κ̂) 7−→ (s0 , [κ̂+ g0 ])
M

where the final edge is the first edge not in lfp(F (M)).

By definition of C C , κ̂ ∈ K̂ 0 and (s, K̂ 0 , g, s0 ) ∈ δ . Since κ̂ is realizable at s in G, by
K̂ 0 ,g

definition of F and 18.6, (s, κ̂) 7−→ (s0 , [κ̂+ g]) contra the assumption. Thus C C (M) ⊆
G

lfp(F (M)) holds by contradiction.

ZU064-05-FPR

paper-jfp

58

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

mon \
\Γ−
\ Γ = ICRPDS×
We first prove an invariant of fˆ : Exp → System
−→ SystemΓ , where System
\ × OPState)
\
P(OPState

IΓ (e) = ((e, ⊥, ⊥), hi)
IΓ0 (e) = (((e, ⊥, ⊥), 0),
/ hi)
hφ̂1 , . . . , φ̂n i+ = φ̂1+ . . . φ̂n+
\ Γ → Prop
invΓ : Exp → System
G

z }| {
o
[ n
g
Ω̂, Ω̂0 : Ω̂  Ω̂0 ∈ Ê )
invΓ (e)((P̂, Ê), Ĥ) = (P̂ =
g

∧ ∀(ψ̂, A)  (ψ̂ 0 , A0 ) ∈ Ê.let K̂ = {κ̂ : StackRoot(κ̂) = A} in

∀κ̂ ∈ κ̂ ∈ K̂ : [κ̂+ g] defined .StackRoot([κ̂+ g]) = A0
K̂,g

∧ (ψ̂, κ̂) 7−→ (ψ̂ 0 , [κ̂+ g])
M

−→ ∗
−−→
K̂,g
∧ ∀(ψ̂, )  (ψ̂ , ) ∈ Ĥ.∃K̂, g.[~g] = ε ∧ (ψ̂, hi) 7−→ (ψ̂ 0 , hi)
0

M

0

where M = I \
PDS (e)
Lemma 18.7 ( fˆ invariant)
For all e, if invΓ (e)(G) then invΓ (e)( fˆe (G))
Proof
Same structure as in Lemma 18.2 without reasoning about worklists.
Proof of Theorem 12.2
Proof
0
Let M = I \
PDS (e), G = C C (M) and G0 = ((P̂, Ê), Ĥ) = lfp( fˆe ).
(G0 approximates G):
−→
K̂,g

We strengthen the statement to π ≡ IΓ (e) 7−→∗ (ψ̂, κ̂) implies
G

~g

• IΓ0 (e) 7−→0 ∗ ((ψ̂, StackRoot(κ̂)), κ̂).
G

−→ ∗
K̂,g

K̂ 0 ,g0

• for all (ψ̂, κ̂) 7−→ (ψ̂ 0 , [κ̂+~g]) 7−→ (ψ̂ 00 , [κ̂+~gg0 ]) v π, if [~gg0 ] = ε, then ∃κ̂ ∈ K̂ and
G

G

(ψ̂, StackRoot(κ̂))  (ψ̂ 00 , StackRoot([κ̂+~gg0 ])) ∈ Ĥ
By induction on π,
Case Base: IΓ (e).
By definition of fˆe , IΓ0 (e) = (Ω̂0 , hi), Ω̂0 ∈ P̂. First goal holds by definition of
StackRoot(hi) and reflexivity. Second goal vacuously true.
Case Induction step:

−−→
K̂ 0 ,g0
((e, ⊥, ⊥), hi) 7−→∗
G

K̂ 00 ,g00

(ψ̂ 0 , [~g0 ]) 7−→ (ψ̂, κ̂).
G

~g0

Let A = StackRoot([~g0 ]). By IH, IΓ0 (e) 7−→0 ∗ ((ψ̂ 0 , A), [~g0 ]).
G

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

59

0

Let K̂root = {κ̂ : StackRoot(κ̂) = A} By definition of I \
PDS and the case assumpK̂ 00 ,g00
0
00
0
0
~
tion, (ψ̂ , K̂root , g , ψ̂) ∈ δ . By cases on (ψ̂ , [g ]) 7−→ (ψ̂, κ̂):
G

K̂ 00 ,φ̂+

Case (ψ̂ 0 , [~g0 ]) 7−→ (ψ̂, κ̂).
G

φ̂

+
By definition of fˆ, (ψ̂ 0 , A)  (ψ̂, A ∪ T (φ̂+ )) ∈ G0 . By definition of StackRoot
and A, StackRoot([~g0 g00 ]) = StackRoot([~g]) = StackRoot(κ̂).
K̂ 00 ,ε
Case (ψ̂ 0 , [~g0 ]) 7−→ (ψ̂, κ̂).

G

Similar to previous case.
K̂ 00 ,φ̂−
Case (ψ̂ 0 , [~g0 ]) 7−→ (ψ̂, κ̂).
G

Since is [~g0 φ̂− ] is defined, there is an i such that gi = φ̂+ , which is witness
K̂ 000 ,φ̂+

to an edge in the trace with that action, ψ̂b 7−
−→
→ ψ̂e By definition of [ ], the
G

actions from ψ̂e to ψ̂ 0 cancel to ε, meaning by IH (ψ̂e , A)  (ψ̂ 0 , A) ∈ H, and
φ̂

+
(ψ̂b , A0 )  (ψ̂e , A) ∈ E. Thus the pop edge is added by definition of fˆ0 . The new
balanced path (ψ̂b , A0 )  (ψ̂, A0 ) is also added, and extended paths get added
with propagation.

Approximation follows by composition with Theorem 12.1.
(G approximates G0 ): Directly from 18.7.
The approximate GC has a similar invariant, except the sets of addresses are with respect
to the tˆ computation.
\ Γ → Prop
invΓ̂ : Exp → System
G



z }| {
[ 
A,g
0
0
invΓ̂ (e)((P̂, Ê), Ĥ) = (P̂ =
ψ̂, ψ̂ : ψ̂  ψ̂ ∈ Ê )
A,g

g

∧ ∀ψ̂0  ψ̂1 ∈ Ê.∃(ψ̂0Γ , AΓ )  (ψ̂1Γ , A0Γ ) ∈ Ê.(∀i.ψ̂iΓ v ψ̂i ) ∧ AΓ ⊆ A
∧ ∀ψ̂0  ψ̂1 ∈ Ĥ.∃(ψ̂0Γ , AΓ )  (ψ̂1Γ , AΓ ) ∈ Ĥ 0 .∀i.ψ̂iΓ v ψ̂i
∧ ∀ψ̂ ∈ P̂.∃(ψ̂ Γ , A) ∈ P̂0 .ψ̂ Γ v ψ̂ ∧ lfp(tˆ)(ψ̂) ⊆ A
where ((P̂0 , Ê 0 ), Ĥ 0 ) = lfp( fˆe )
Lemma 18.8 (Approx GC invariant)
For all e, if invΓ̂ (e)(G) then invΓ̂ (e)( fˆe0 (G))
Proof
Straightforward case analysis.
Proof of Theorem 12.3
Proof
Induct on path in lfp( fˆe ) and apply 18.8.

ZU064-05-FPR

paper-jfp

60

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
19 Haskell implementation of CRPDSs

Where it is critical to understanding the details of the analysis, we have transliterated the
formalism into Haskell. We make use of a two extensions in GHC:
-XTypeOperators -XTypeSynonymInstances
All code is in the context of the following header, and we’ll assume the standard instances
of type classes like Ord and Eq.
import Prelude hiding ((!!))
import Data.Map as Map hiding (map,foldr)
import Data.Set as Set hiding (map,foldr)
import Data.List as List hiding ((!!))
type P s = Set.Set s
type k :-> v = Map k v
(==>) :: a -> b -> (a,b)
(==>) x y = (x,y)
(//) :: Ord a => (a :-> b) -> [(a,b)] -> (a :-> b)
(//) f [(x,y)] = Map.insert x y f
set x = Set.singleton x

19.1 Transliteration of NFA formalism
We represent an NFA as a set of labeled forward edges, the inverse of those edges (for
convenience), a start state and an end state:
type NFA state char =
(NFAEdges state char,NFAEdges state char,state,state)
type NFAEdges state char = state :-> P(Maybe char,state)

19.2 ANF
data Exp

=
|
|
data AExp
=
|
data Lambda =
data Call
=
type Var
=

Ret AExp
App Call
Let1 Var Call Exp
Ref Var
Lam Lambda
Var :=> Exp
AExp :@ AExp
String

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION
-- Abstract
type AConf
type AEnv
type AStore
type AD
data AVal
type AKont
type AFrame

61

state-space:
= (Exp,AEnv,AStore,AKont)
= Var :-> AAddr
= AAddr :-> AD
= (AVal)
= AClo (Lambda, AEnv)
= [AFrame]
= (Var,Exp,AEnv)

data AAddr = ABind Var AContext
type AContext = [Call]
Abstract configuration space transliterated into Haskell. In the code, we defined abstract
addresses to be able to support k-CFA-style polyvariance.
Atomic expression evaluation implementation:
aeval :: (AExp,AEnv,AStore) -> AD
aeval (Ref v, ρ, σ ) = σ !!(ρ!v)
aeval (Lam l, ρ, σ ) = set $ AClo (l, ρ)
We encode the transition relation it as a function that returns lists of states:
astep :: AConf -> [AConf]
astep (App (f :@ ae), ρ, σ , κ) = [(e, ρ’’, σ ’, κ) |
AClo(v :=> e, ρ’) <- Set.toList $ aeval(f, ρ, σ ),
let a = aalloc(v, App (f :@ ae)),
let ρ’’ = ρ’ // [v ==> a],
let σ ’ = σ [a ==> aeval(ae, ρ, σ )] ]
astep (Let1 v call e, ρ, σ , κ) =
[(App call, ρ, σ , (v, e, ρ) : κ)]
astep (Ret ae, ρ, σ , (v, e, ρ’) : κ) = [(e, ρ’’, σ ’, κ)]
where a = aalloc(v, Ret ae)
ρ’’ = ρ’ // [v ==> a]
σ ’ = σ [a ==> aeval(ae, ρ, σ )]

19.3 Partial orders
We define a typeclass for lattices:
class Lattice a where
bot :: a
top :: a
(v) :: a -> a -> Bool
(t) :: a -> a -> a
(u) :: a -> a -> a

ZU064-05-FPR

paper-jfp

62

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn

And, we can lift instances to sets and maps:
instance (Ord s, Eq s) => Lattice (P s) where
bot = Set.empty
top = error "no representation of universal set"
x t y = x ‘Set.union‘ y
x u y = x ‘Set.intersection‘ y
x v y = x ‘Set.isSubsetOf‘ y
instance (Ord k, Lattice v) => Lattice (k :-> v) where
bot = Map.empty
top = error "no representation of top map"
f v g = Map.isSubmapOfBy (v) f g
f t g = Map.unionWih (t) f g
f u g = Map.intersectionWith (u) f g
(t) :: (Ord k, Lattice v) => (k :-> v) -> [(k,v)] -> (k :-> v)
f t [(k,v)] = Map.insertWith (t) k v f
(!!) :: (Ord k, Lattice v) => (k :-> v) -> k -> v
f !! k = Map.findWithDefault bot k f

19.4 Reachability
We can turn any data type to a stack-action alphabet:
data StackAct frame = Push { frame :: frame }
| Pop { frame :: frame }
| Unch
type CRPDS control frame = (Edges control frame, control)
type Edges control frame = control :-> (StackAct frame,control)
We split the encoding of δ into two functions for efficiency purposes:
type Delta control frame =
(TopDelta control frame, NopDelta control frame)
type TopDelta control frame =
control -> frame -> [(control,StackAct frame)]
type NopDelta control frame =
control -> [(control,StackAct frame)]
If we only want to know push and no-change transitions, we can find these with a NopDelta
function without providing the frame that is currently on top of the stack. If we want pop
transitions as well, we can find these with a TopDelta function, but of course, it must have

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

63

access to the top of the stack. In practice, a TopDelta function would suffice, but there
are situations where only push and no-change transitions are needed, and having access to
NopDelta avoids extra computation.
At this point, we must clarify how to embed the abstract transition relation into a pushdown transition relation:

adelta :: TopDelta AControl AFrame
adelta (e, ρ, σ ) γ = [ ((e’, ρ’, σ ’), g) |
(e’, ρ’, σ ’, κ) <- astep (e, ρ, σ , [γ]),
let g = case κ of
[]
-> Pop γ
[γ1 , ] -> Push γ1
[ ]
-> Unch ]
adelta’ :: NopDelta AControl AFrame
adelta’ (e, ρ, σ ) = [ ((e’, ρ’, σ ’), g) |
(e’, ρ’, σ ’, κ) <- astep (e, ρ, σ , []),
let g = case κ of
[γ1] -> Push γ1
[ ]
-> Unch ]

The function crpds will invoke the fixed point solver:

crpds :: (Ord control, Ord frame) =>
(Delta control frame) ->
control ->
frame ->
CRPDS control frame
crpds (δ ,δ ’) q0 0 =
(summarize (δ ,δ ’) etg1 ecg1 [] dE dH, q0) where
etg1 = (Map.empty // [q0 ==> Set.empty],
Map.empty // [q0 ==> Set.empty])
ecg1 = (Map.empty // [q0 ==> set q0],
Map.empty // [q0 ==> set q0])
(dE,dH) = sprout (δ ,δ ’) q0

Figure 11 provides the code for summarize, which conducts the fixed point calculation,
the executable equivalent of Figure 6:

ZU064-05-FPR

paper-jfp

64

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
summarize :: (Ord control, Ord frame) =>
(Delta control frame) ->
(ETG control frame) ->
(ECG control) ->
[control] ->
[Edge control frame] ->
[EpsEdge control] ->
(Edges control frame)

To expose the structure of the computation, we’ve added a few types:
-- A set of edges, encoded as a map:
type Edges control frame =
control :-> P (StackAct frame,control)
-- Epsilon edges:
type EpsEdge control = (control,control)
-- Explicit transition graph:
type ETG control frame =
(Edges control frame, Edges control frame)
-- Epsilon closure graph:
type ECG control =
(control :-> P(control), control :-> P(control))

An explicit transition graph is an explicit encoding of the reachable subset of the transition relation. The function summarize takes six parameters:
1. the pushdown transition function;
2. the current explicit transition graph;
3. the current ε-closure graph;
4. a work-list of states to add;
5. a work-list of explicit transition edges to add; and
6. a work-list of ε-closure transition edges to add.
The function summarize processes ε-closure edges first, then explicit transition edges and
then individual states. It must process ε-closure edges first to ensure that the ε-closure
graph is closed when considering the implications of other edges.
Sprouting

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION
summarize (δ ,δ ’) (fw,bw) (fe,be) [] [] [] = fw
summarize (δ ,δ ’) (fw,bw) (fe,be) (q:dS) [] []
| fe ‘contains‘ q = summarize (δ ,δ ’) (fw,bw) (fe,be) dS [] []
summarize (δ ,δ ’) (fw,bw) (fe,be) (q:dS) [] [] =
summarize (δ ,δ ’) (fw’,bw’) (fe’,be’) dS dE’ dH’ where
(dE’,dH’) = sprout (δ ,δ ’) q
fw’ = fw t [q ==> Set.empty]
bw’ = bw t [q ==> Set.empty]
fe’ = fe t [q ==> set q]
be’ = be t [q ==> set q]
summarize (δ ,δ ’) (fw,bw) (fe,be) dS ((q,g,q’):dE) []
| (q,g,q’) ‘isin’‘ fw = summarize (δ ,δ ’) (fw,bw) (fe,be) dS dE []
summarize (δ ,δ ’) (fw,bw) (fe,be) dS ((q,Push ,q’):dE) [] =
summarize (δ ,δ ’) (fw’,bw’) (fe’,be’) dS’ dE’’ dH’ where
(dE’,dH’) = addPush (fw,bw) (fe,be) (δ ,δ ’) (q,Push ,q’)
dE’’ = dE’ ++ dE’’
dS’ = q’:dS
fw’ = fw t [q ==> set (Push ,q’)]
bw’ = bw t [q’ ==> set (Push ,q) ]
fe’ = fe t [q ==> set q ]
be’ = fe t [q’ ==> set q’]
summarize (δ ,δ ’) (fw,bw) (fe,be) dS ((q,Pop ,q’):dE) [] =
summarize (δ ,δ ’) (fw’,bw’) (fe’,be’) dS’ dE’’ dH’ where
(dE’,dH’) = addPop (fw,bw) (fe,be) (δ ,δ ’) (q,Pop ,q’)
dE’’ = dE ++ dE’
dS’ = q’:dS
fw’ = fw t [q ==> set (Pop ,q’)]
bw’ = bw t [q’ ==> set (Pop ,q) ]
fe’ = fe t [q ==> set q ]
be’ = fe t [q’ ==> set q’]
summarize (δ ,δ ’) (fw,bw) (fe,be) dS ((q,Unch,q’):dE) [] =
summarize (δ ,δ ’) (fw’,bw’) (fe’,be’) dS’ dE [(q,q’)] where
dS’ = q’:dS
fw’ = fw t [q ==> set (Unch,q’)]
bw’ = bw t [q’ ==> set (Unch,q) ]
fe’ = fe t [q ==> set q ]
be’ = fe t [q’ ==> set q’]
summarize (δ ,δ ’) (fw,bw) (fe,be) dS dE ((q,q’):dH)
| (q,q’) ‘isin‘ fe = summarize (δ ,δ ’) (fw,bw) (fe,be) dS dE dH
summarize (δ ,δ ’) (fw,bw) (fe,be) dS dE ((q,q’):dH) =
summarize (δ ,δ ’) (fw,bw) (fe’,be’) dS dE’ dH’ where
(dE’,dH’) = addEmpty (fw,bw) (fe,be) (δ ,δ ’) (q,q’)
fe’ = fe t [q ==> set q ]
be’ = fe t [q’ ==> set q’]

Fig. 11: An implementation of pushdown control-state reachability.

65

ZU064-05-FPR

paper-jfp

66

6 February 2018

3:38

J.I. Johnson, I. Sergey, C. Earl, M. Might, and D. Van Horn
sprout :: (Ord control) =>
Delta control frame ->
control ->
([Edge control frame], [EpsEdge control])
sprout (δ ,δ ’) q = (dE, dH) where
edges = δ ’ q
dE = [ (q,g,q’) | (q’,g) <- edges, isPush g ]
dH = [ (q,q’)
| (q’,g) <- edges, isUnch g ]

Pushing
addPush :: (Ord control) =>
ETG control frame ->
ECG control ->
Delta control frame ->
Edge control frame ->
([Edge control frame], [EpsEdge control])
addPush (fw,bw) (fe,be) (δ ,δ ’) (s,Push γ,q) = (dE,dH) where
qset’ = Set.toList $ fe!q
dE = [ (q’,g,q’’) | q’ <- qset’, (q’’,g) <- δ q’ γ, isPop g ]
dH = [ (s,q’’)
| (q’,Pop ,q’’) <- dE ]

Popping
addPop :: (Ord control) =>
ETG control frame ->
ECG control ->
Delta control frame ->
Edge control frame ->
([Edge control frame], [EpsEdge control])
addPop (fw,bw) (fe,be) (δ ,δ ’) (s’’,Pop γ,q) = (dE,dH) where
sset’ = Set.toList $ be!s’’
dH = [ (s,q) | s’ <- sset’,
(g,s) <- Set.toList $ bw!s’, isPush g ]
dE = []
Clearly, we could eliminate the new edges parameter dE for the function addPop, but we
have retained it for stylistic symmetry.
Adding empty edges The function addEmpty has many cases to consider:

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

PUSHDOWN FLOW ANALYSIS WITH ABSTRACT GARBAGE COLLECTION

67

addEmpty :: (Ord control) =>
ETG control frame ->
ECG control ->
Delta control frame ->
EpsEdge control ->
([Edge control frame], [EpsEdge control])
addEmpty (fw,bw) (fe,be) (δ ,δ ’) (s’’,s’’’) = (dE,dH) where
sset’
= Set.toList $ be!s’’
sset’’’’ = Set.toList $ fe!s’’’
dH’
= [ (s’,s’’’’) | s’ <- sset’, s’’’’ <- sset’’’’ ]
dH’’ = [ (s’,s’’’)
| s’ <- sset’ ]
dH’’’ = [ (s’’,s’’’’) | s’’’’ <- sset’’’’ ]
sEdges = [ (g,s) | s’ <- sset’, (g,s) <- Set.toList $ bw!s’ ]
dE = [ (s’’’’,g’,q) | s’’’’ <- sset’’’’,
(g,s) <- sEdges,
isPush g, let Push γ = g,
(q,g’) <- δ s’’’’ γ,
isPop g’ ]
dH’’’’ = [ (s,q) | ( ,s) <- sEdges, ( , ,q) <- dE ]
dH = dH’ ++ dH’’ ++ dH’’’ ++ dH’’’’

ZU064-05-FPR

paper-jfp

6 February 2018

3:38

