Is Continuation-Passing Useful for Data Flow Analysis?

Amr Sabry^{∗} Matthias Felleisen^{∗}

Department of Computer Science Rice University Houston, TX 77251-1892^{†}

Abstract

The widespread use of the continuation-passing style (CPS) transformation in compilers, optimizers, abstract interpreters, and partial evaluators reflects a common belief that the transformation has a positive effect on the analysis of programs. Investigations by Nielson [13] and Burn/Filho [5, 6] support, to some degree, this belief with theoretical results. However, they do not pinpoint the source of increased abstract information and do not explain the observation of many people that continuation-passing confuses some conventional data flow analyses.

To study the impact of the CPS transformation on program analysis, we derive three canonical data flow analyzers for the core of an applicative higher-order programming language. The first analyzer is based on a direct semantics of the language, the second on a continuation-semantics of the language, and the last on the direct semantics of CPS terms. All analyzers compute the control flow graph of the source program and hence our results apply to a large class of data flow analyses. A comparison of the information gathered by our analyzers establishes the following points:

1. The results of a direct analysis of a source program are incomparable to the results of an analysis of the equivalent CPS program. In other words, the translation of the source program to a CPS version may increase or decrease static information.

The gain of information occurs in non-distributive analyses and is solely due to the duplication of the analysis of the continuation. The loss of information is due to the confusion of distinct procedure returns.

2. The analyzer based on the continuation semantics produces more accurate results than both direct analyzers, but again only in non-distributive analyses due to the duplication of continuations along every execution path. However, when the analyzer explicitly accounts for looping constructs, the results of the semantic-CPS analysis are no longer computable.

In view of these results, we argue that, in practice, a direct data flow analysis that relies on some amount of duplication would be as satisfactory as a CPS analysis.

1 Compiling with CPS

Many compilers for higher-order applicative languages (Scheme, ML, Common Lisp) map source programs to programs in continuation-passing style (CPS) [1, 10, 11, 17]. Compiler writers believe that the intermediate representation based on CPS eases the production of code and facilitates optimizations. Numerous people also argue that the CPS transformation increases the precision of the data flow analysis that is necessary for advanced optimizations [2, 3, 5, 6, 16].^{1}

Even though CPS programs are widely accepted as an advantageous intermediate representation, few compiler writers can pinpoint the advantages of the CPS representation over other intermediate representations.

∗Supported in part by NSF grant CCR 89-17022 and by Texas ATP grant 91-003604014. Also partially supported by Arpa grant 8313, issued by ESD/AVS under Contract No. F196228-91-C-0168 under the direction of Robert Harper and Peter Lee.

†Temporary address: School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213.

1Researchers often express this view in informal discussions as opposed to formal papers. We discussed and re-confirmed this idea with, among others, Charles Consel, and Olivier Danvy at LFP ’92 [June 92], following the presentation of our paper on equational reasoning about programs in CPS [14]; in an email exchange with Geoffrey Burn and Juarez Filho [July 92]; in further discussions at POPL ’93 with Daniel Weise; in email discussions with Kelsey [July 93] and Shivers [May 93]; and in discussions with Burn at FPCA ’93 [June 93].

In an attempt to understand the principles of compiling with continuations and to determine its crucial properties, we recently found two important results:

1. The theory of equational manipulations of programs in CPS based on the β rule of the lambda calculus has a simple counterpart for source programs; in other words, whatever optimizations are expressible via β-steps on CPS programs, can equally well be formulated for source programs [14].

2. The code generation phase of a non-optimizing CPS compiler only requires that the intermediate representation be normalized according to simple transformations. It is unnecessary to perform a full CPS translation [7].

Prompted by conversations with G. Burn [July 92] and with H. Boehm [August 92], and by the observation that the CPS transformation obscures some obvious properties of programs, we started to investigate the exact effect of the CPS program representation on the data flow analysis of programs. Our answer rejects the common belief that the CPS transformation is useful for practical analyses.

The organization of the rest of this paper is as follows. The next section introduces the syntax and semantics of a typical higher-order language. Section 3 presents the CPS transformation. In Section 4, we derive various data flow analyzers from the standard semantics using the method of abstract interpretation. Section 5 presents all the formal theorems, which are discussed from a practical perspective in Section 6. For full proofs, we refer the reader to the technical report version of our paper [15].

2 Λ: Syntax and Semantics

Our source language is a simple extension of the language Λ of the λ-calculus. It corresponds to the core of typical higher-order languages like Scheme, Lisp, and ML. The set of terms includes values, applications, letexpressions, and conditionals; the set of syntactic values contains numerals (n ∈ ), variables (x ∈ Var), primitive procedures, and user-defined procedures:

M ::= V | (M M) | (let (x M) M) | (if0 M M M)
V ::= n | x | add1 | sub1 | (λx.M)

Informally, the semantics of the language is as follows. All procedures are call-by-value, the evaluation of (let (x M_{1}) M_{2}) computes the value of M_{1} and binds it to x in M_{2}, and the conditional if0 branches to the second or third subexpression depending on whether the first subexpression evaluates to 0 or not. Though the language is overly simple, it is rich enough for the primary purpose of the paper.

The analysis of programs assumes that every intermediate result is named, and that all bound variables in a program are unique. The restricted subset is the following language:

M ::= V
| (let (x V) M)
| (let (x (V V)) M)
| (let (x (if0 V M M)) M)
V ::= n | x | add1 | sub1 | (λx.M)

The assumptions simplify the semantics and the derivation of the data flow analyzers without restricting the set of valid programs: every term in Λ has a semantically equivalent normal form in the restricted subset. For example, the code fragment (f (let (x 1) (g x))) becomes:

(let (x_{1} 1) (let (x_{2} (g x_{1})) (let (x_{3} (f x_{2})) x_{3}))).

In general, the normalization process uses the reductions that we identified in previous work as the Areductions [7, 14].^{2}

The semantics of the restricted subset of Λ is specified by the two predicates M and app defined in Figure 1. It is straightforward to show that M is a partial function from terms, environments, and stores to answers. The environment is a finite table that maps the free variables to locations; the store is a finite table that maps locations to values.^{3} An answer is a pair that consists of a run-time value and a store. The set of run-time values consists of numbers and closures. A closure is one of the procedure tags inc and dec, or a data-structure that contains the text of a userdefined procedure and the environment at the point of the creation of the closure. When applying a closure ⟨cl x, M, ρ⟩ to a value u, we extend the enclosed environment at x with a new location and extend the store with the value u at the new location. Thus, the bound variable of a procedure or a block is related to different locations, one for each invocation of the procedure. The function new takes a variable x, a store

2The normalization process does not affect the results of the data flow analyzers. Intuitively, the first phase of Anormalization gives every subexpression a name to which the data flow analyzer can associate information about the expression. Without A-normalization, the analyzer would typically associate a “label” with every expression and attach the information about each expression at the corresponding label [8, 13, 16].

The two treatments are identical but the replacement of labels by variables simplifies the analyzers. The second phase of A-normalization re-orders the expressions to reflect the order in which the interpreters will traverse them. For example, an expression (add1 (let (x V) 0)) would be rewritten as (let (x V) (add1 0)). Again, the change is transparent to the (abstract) interpreters since they evaluate both expressions in the same manner.

3The formulation of the semantics does not require a store, but the presence of the store simplifies the derivation of data flow analyzers.

Domains:  Auxiliary Function:
Ans = Val × Sto
Env = Var ⟶ ∘ Loc
Sto = Loc ⟶ ∘ Val
Val = Num + Clo
Clo = (Var × Λ × Env) + inc + dec

ϕ : Λ(V) × Env × Sto → Val
ϕ(n, ρ, s) = n
ϕ(x, ρ, s) = s(ρ(x))
ϕ(add1, ρ, s) = inc
ϕ(sub1, ρ, s) = dec
ϕ((λx.M), ρ, s) = ⟨cl x, M, ρ⟩

M : (Λ × Env × Sto) → Ans

\frac{u = ϕ(V, ρ, s)}{⟨V, ρ, s⟩ M ⟨u, s⟩}  \frac{u = ϕ(V, ρ, s) ⟨M, ρ[x := new(x)], s[new(x) := u]⟩ M A}{⟨(let (x V) M), ρ, s⟩ M A}

\frac{u_{1} = ϕ(V_{1}, ρ, s) u_{2} = ϕ(V_{2}, ρ, s) ⟨u_{1}, u_{2}, s⟩ app ⟨u_{3}, s_{3}⟩ ⟨M, ρ[x := new(x)], s_{3}[new(x) := u_{3}]⟩ M A}{⟨(let (x (V_{1} V_{2})) M), ρ, s⟩ M A}

\frac{u_{0} = ϕ(V_{0}, ρ, s) ⟨M_{i}, ρ, s⟩ M ⟨u_{1}, s_{1}⟩ ⟨M, ρ[x := new(x)], s_{1}[new(x) := u_{1}]⟩ M A}{⟨(let (x (if0 V_{0} M_{1} M_{2})) M), ρ, s⟩ M A} i = 1 if u_{0} = 0, i = 2 otherwise.

app : (Val × Val × Sto) → Ans

\overline{⟨inc, n, s⟩ app ⟨(n + 1), s⟩}  \overline{⟨dec, n, s⟩ app ⟨(n − 1), s⟩}  \frac{⟨M, ρ[x := new(x)], s[new(x) := u]⟩ M A}{⟨⟨cl x, M, ρ⟩, u, s⟩ app A}

Figure 1: Direct (Store) Interpreter

s, and returns a new location ℓ from which it is possible to recover x, i.e., new(x, s) = ℓ ∉ dom(s) and x = new^{−1}(ℓ). (For brevity, we will often omit the second argument to new.)

3 Continuation-Passing Style

A continuation-passing style transformation may be applied to the interpreter or to the source program. We distinguish the two approaches by referring to the first transformation as the semantic-CPS transformation and to the second as the syntactic-CPS transformation. We discuss both possibilities in this section.

3.1 Continuations

A continuation is the control state of an evaluator. For example, during the evaluation of the procedure call ((λa.N_{1}) 5) in (let (x ((λa.N_{1}) 5)) N_{2}), the evaluator must remember the evaluation context (let (x [ ]) N_{2}) of the call as well as the environment ρ in which to evaluate N_{2}. Typically, this information is packaged in a frame and added to the continuation prior to the procedure call. The evaluation of the body of the procedure N_{1} may itself push frames on the control stack. Thus the continuation κ can in general be represented as a list of frames where each frame consists of an evaluation context and an environment [7]:

κ = ⟨E_{1}, ρ_{1}⟩ :: ⋯:: nil where E_{i} = (let (x_{i} [ ]) M_{i})

3.2 Semantic-CPS Transformation

The CPS interpreter (see Figure 2) maps expressions, environments, continuations, and stores to answers. It employs two auxiliary functions: appk, which is the CPS counterpart of app, and appr, which corresponds to the “return” operation of an abstract machine. The latter operation binds the return value to a variable, restores the environment, pops the control stack, and jumps to the next instruction.

The direct interpreter and the semantic-CPS interpreter produce the same output.

Lemma 3.1 Let M ∈ Λ, then ⟨M, ρ, s⟩ M A iff ⟨M, ρ, nil, s⟩ C A.

3.3 Syntactic-CPS Transformation

The transformation of a source program to a program in CPS uses two mutually recursive functions: F to transform terms and V to transform values. The function F takes an additional argument k, which is a variable that represents the current continuation.

Definition 3.2. (Syntactic-CPS Transformation) Let cps(Λ) be the language:

P ::= (k W)
| (let (x W) P)
| (W W (λx.P))
| (let (k λx.P) (if0 W P P))
W ::= n | x | add1k | sub1k | (λxk.P)

Domains:

Ans = Val × Sto
Env = Var ⟶ ∘ Loc
Sto = Loc ⟶ ∘ Val

Con = (Λ(E) × Env) :: Con + nil
Val = Num + Clo
Clo = (Var × Λ × Env) + inc + dec

C : (Λ × Env × Con × Sto) → Ans

\frac{u = ϕ(V, ρ, s) ⟨κ, ⟨u, s⟩⟩ appr A}{⟨V, ρ, κ, s⟩ C A}  \frac{u = ϕ(V, ρ, s) ⟨M, ρ[x := new(x)], κ, s[new(x) := u]⟩ C A}{⟨(let (x V) M), ρ, κ, s⟩ C A}

\frac{u_{1} = ϕ(V_{1}, ρ, s) u_{2} = ϕ(V_{2}, ρ, s) ⟨u_{1}, u_{2}, ⟨(let (x [ ]) M), ρ⟩ :: κ, s⟩ appk A}{⟨(let (x (V_{1} V_{2})) M), ρ, κ, s⟩ C A}

\frac{u_{0} = ϕ(V_{0}, ρ, s) ⟨M_{i}, ρ, ⟨(let (x [ ]) M), ρ⟩ :: κ, s⟩ C A}{⟨(let (x (if0 V_{0} M_{1} M_{2})) M), ρ, κ, s⟩ C A} i = 1 if u_{0} = 0, i = 2 otherwise.

appk : (Val × Val × Con × Sto) → Ans

\frac{⟨κ, ⟨(n + 1), s⟩⟩ appr A}{⟨inc, n, κ, s⟩ appk A}  \frac{⟨κ, ⟨(n − 1), s⟩⟩ appr A}{⟨dec, n, κ, s⟩ appk A}  \frac{⟨M, ρ[x := new(x)], κ, s[new(x) := u]⟩ C A}{⟨⟨cl x, M, ρ⟩, u, κ, s⟩ appk A}

appr : (Con × Ans) → Ans

\frac{⟨M, ρ[x := new(x)], κ, s[new(x) := u]⟩ C A}{⟨⟨(let (x [ ]) M), ρ⟩ :: κ, ⟨u, s⟩⟩ appr A}  \overline{⟨nil, A⟩ appr A}

Figure 2: Semantic-CPS Interpreter

where x ∈ Vars, k ∈ KVars and KVars ∩ Vars = ∅. The CPS transformation uses the functions F and V:

F : Λ → cps(Λ) F_{k}[[V]] = (k V[[V]]) F_{k}[[(let (x V) M)]] = (let (x V[[V]]) F_{k}[[M]]) F_{k}[[(let (x (V_{1} V_{2})) M)]] = (V[[V_{1}]] V[[V_{2}]] λx.F_{k}[[M]]) F_{k}[[(let (x (if0 V_{0} M_{1} M_{2})) M)]] =

(let (k′ λx.F_{k}[[M]]) (if0 V[[V_{0}]] F_{k′}[[M_{1}]] F_{k′}[[M_{2}]]))

V : Λ(V) → cps(Λ)(W) V[[n]] = n V[[x]] = x V[[add1]] = add1k V[[sub1]] = sub1k V[[(λx.M)]] = (λxk.F_{k}[[M]])

The evaluation for CPS programs is defined by M_{c}, a specialized version of the direct interpreter M [7]. It handles procedures of two arguments and manipulates a larger set of run-time values than the direct interpreter that includes continuations of the form ⟨co x, P, ρ⟩ (see Figure 3). The larger set of run-time values reflects the salient aspect of the CPS transformation: it reifies the continuation of the evaluator to an object that the program explicitly manipulates.^{4}

To establish the formal relationship between the behavior of a direct term and the behavior of its CPStransform, we define the function δ that relates direct run-time values to their CPS counterparts:

δ(n) = n
δ(inc) = inck
δ(dec) = deck
δ(⟨cl x, M, ρ⟩) = ⟨cl xk, F_{k}[[M]], ρ⟩

We extend δ to work on stores by applying it to the value at each location and to answers by applying it to both the value component and the store component.

The following lemma describes the precise relationship between the semantic-CPS interpreter and the syntactic-CPS interpreter. The interpreters yield answers related by δ; the store resulting from the syntactic-CPS interpreter will contain additional entries that correspond to continuations.

Lemma 3.3 Let M ∈ Λ, then:

⟨M, ρ, nil, s⟩ C ⟨u_{1}, s_{1}⟩ iff

⟨F_{k}[[M]], ρ[k := new(k)], δ(s)[new(k) := stop]⟩ M_{c} ⟨δ(u_{1}), δ(s_{1})[new(k_{1}) := κ_{1}, new(k_{2}) := κ_{2},…]⟩.

Together with Lemma 3.1, this result also relates the syntactic-CPS interpreter to the direct one.

4In principle, we could use the direct interpreter M to evaluate CPS programs. However, this choice forces continuations to be represented as procedures, which is (unrealistic and) unnecessarily confusing for data flow analyzers.

Domains:  Auxiliary Function:
Ans = Val × Sto
Env = Var ⟶ ∘ Loc
Sto = Loc ⟶ ∘ Val
Val = Num + Clo + Con
Clo = (Var × KVar × cps(Λ) × Env)

+ inck + deck

Con = (Var × cps(Λ) × Env) + stop

ϕ_{c} : cps(Λ)(W) × Env × Sto → Val
ϕ_{c}(n, ρ, s) = n
ϕ_{c}(x, ρ, s) = s(ρ(x))
ϕ_{c}(add1k, ρ, s) = inck
ϕ_{c}(sub1k, ρ, s) = deck
ϕ_{c}((λxk.P), ρ, s) = ⟨cl xk, P, ρ⟩

M_{c} : (cps(Λ) × Env × Sto) → Ans

\frac{κ = s(ρ(k)) u = ϕ_{c}(W, ρ, s) ⟨κ, ⟨u, s⟩⟩ appr_{c} A}{⟨(k W), ρ, s⟩ M_{c} A}  \frac{u = ϕ_{c}(W, ρ, s) ⟨P, ρ[x := new(x)], s[new(x) := u]⟩ M_{c} A}{⟨(let (x W) P), ρ, s⟩ M_{c} A}

\frac{u_{1} = ϕ_{c}(W_{1}, ρ, s) u_{2} = ϕ_{c}(W_{2}, ρ, s) ⟨u_{1}, u_{2}, ⟨co x, P, ρ⟩, s⟩ app_{c} A}{⟨(W_{1} W_{2} (λx.P)), ρ, s⟩ M_{c} A}

\frac{u_{0} = ϕ_{c}(W_{0}, ρ, s) ⟨P_{i}, ρ[k := new(k)], s[new(k) := ⟨co x, P, ρ⟩]⟩ M_{c} A}{⟨(let (k λx.P) (if0 W_{0} P_{1} P_{2})), ρ, s⟩ M_{c} A} i = 1 if u_{0} = 0, i = 2 otherwise.

app_{c} : (Val × Val × Val × Sto) → Ans

\frac{⟨κ, ⟨(n + 1), s⟩⟩ appr_{c} A}{⟨inck, n, κ, s⟩ app_{c} A}  \frac{⟨κ, ⟨(n − 1), s⟩⟩ appr_{c} A}{⟨deck, n, κ, s⟩ app_{c} A}

\frac{⟨P, ρ[x := new(x), k := new(k)], s[new(x) := u, new(k) := κ]⟩ M_{c} A}{⟨⟨cl xk, P, ρ⟩, u, κ, s⟩ app_{c} A}

appr_{c} : (Val × Ans) → Ans

\frac{⟨P, ρ[x := new(x)], s[new(x) := u]⟩ M_{c} A}{⟨⟨co x, P, ρ⟩, ⟨u, s⟩⟩ appr_{c} A}

⟨stop, A⟩ appr_{c} A

Figure 3: Syntactic-CPS Interpreter

4 Constant Propagation by Abstract Interpretation

Using well-known ideas from the area of abstract interpretation [4, 8, 13, 16], we now derive a data flow analyzer from each of the three interpreters. The first step in the derivation is to associate one location with each variable that holds the potentially infinite set of values to which the variable is bound during the evaluation of the program. Second, we approximate these sets of values so that each label is associated with a finite number of values. Finally, we modify the interpreters to detect and recover from all loops when computing over the universe of approximate values.

4.1 Abstracting Procedures

The first step in the derivation of the data flow analyzers is to limit the number of locations that can be created during the evaluation of a given program. One of the simple approximations, known as 0CFA analysis [16], is to associate one location for each variable and to collect all the values to which the variable is bound at that location. Formally, we approximate environments ρ to \overline{ρ} and stores s to \overline{s} as follows:

• Since each variable is associated with exactly one location, we can choose that location to be the variable itself. Thus, if ρ = {x_{1} ↦ new(x_{1}),…}, \overline{ρ} = \{x_{1} ↦ x_{1},…\}. This approximation of the environment does not provide any information, that is, we can drop it completely. Thus, a closure ⟨cl x, M, ρ⟩ becomes an abstract closure ⟨cl^{⊖} x, M⟩, a continuation ⟨E_{1}, ρ_{1}⟩ :: …:: nil becomes E_{1} :: …:: nil, and a continuation ⟨co x, M, ρ⟩ becomes an abstract continuation ⟨co^{⊖} x, M⟩. It follows that, for each source program, the sets of abstract closures and abstract continuations are finite.

• For stores s = {new(x_{1}) ↦ u_{1},…}, we first recover the variable associated with each of the locations: {x_{1} ↦ u_{1},…}. Then, to obtain the store \overline{s}, we merge all entries of the form x ↦ u_{1}, x ↦ u_{2},… for some x into one entry x ↦ {u_{1}, u_{2},…}.

A “collecting semantics” like the above associates a set with each variable. Intuitively, the larger the set the less information is available at compile time about the variable. To formalize this notion of “precision,” we note that the sets of collected values form a complete lattice ordered by set-inclusion; the least upper bound operation is set-union. Thus, the relation “is more precise than” coincides with the lattice ordering.

4.2 Abstracting Integers

Despite the approximations of environments, stores, closures, and continuations, the “collecting semantics” still associates an unbounded set of values with a variable because the lattice of collected values contains infinite chains of elements of decreasing precision, e.g., ∅ ⊆ {0} ⊆ {0, 1} ⊆ {0, 1, 2}. . .. Since these infinite chains may cause the analysis to diverge, we approximate sets of numbers to abstract numbers [9]:

\overline{∅} = ⊥, \overline{\{n\}} = n, and \overline{\{n_{1}, n_{2},…\}} = ⊤.

At this point, the universe of abstract values consists of abstract numbers and abstract closures. It remains to impose an order ⊑ on the abstract values similar to the order ⊆ on collected values that coincides with the relation “is more precise than.” For the direct and semantic-CPS interpreters, we organize the abstract values in a lattice that is the product of two lattices: the first is the traditional lattice _{⊥}^{⊤} for constant propagation [9], and the second is the power set of abstract closures (ordered by the subset relation) for control flow analysis [16]. The ordering relation ⊑ and the least upper bound operation ⊔ are defined component-wise. It is easy to check that, if S_{1} and S_{2} are sets of collected values, then S_{1} ⊆ S_{2} implies \overline{S_{1}} ⊑ \overline{S_{2}}.

For the syntactic-CPS collecting interpreter, the sets of values include abstract continuations as well. In that case, we use a lattice of abstract values that consists of the product of three lattices: the constant propagation lattice, the power set of abstract closures, and the power set of abstract continuations.

The ordering of abstract values induces an ordering on stores. If σ_{1} and σ_{2} are abstract stores, then σ_{1} ⊑ σ_{2} if for every variable x in the domain of σ_{1}, σ_{1}(x) ⊑ σ_{2}(x). The latter ordering induces a component-wise ordering on abstract answers.

We can now specify collecting interpreters that manipulate abstract values. The interpreters replace add1 and sub1 by add1^{⊖} and sub1^{⊖}:

add1^{⊖}(⊥) = ⊥
add1^{⊖}(n) = (n + 1)
add1^{⊖}(⊤) = ⊤

sub1^{⊖}(⊥) = ⊥
sub1^{⊖}(n) = (n − 1)
sub1^{⊖}(⊤) = ⊤

Figures 4, 5, and 6 contain the direct abstract collecting interpreters, the semantic-CPS abstract collecting interpreter, and the syntactic-CPS abstract collecting interpreter respectively.

4.3 Correctness

The correctness criterion of an abstract collecting interpreter is that its results approximate the actual execution of the program. For example, if the variable x gets bound to 5 along any actual execution path, the abstract collecting interpreter should associate an abstract value u ⊒ ⟨5, ⊥⟩ with the variable x.

Lemma 4.1 If \overline{s} ⊑ σ, \overline{\{u_{1}\}} ⊑ u_{2} and \overline{s_{1}} ⊑ σ_{2}, then:

1. If ⟨M, ρ, s⟩ M ⟨u_{1}, s_{1}⟩, then ⟨M, σ⟩ M^{⊖} ⟨u_{2}, σ_{2}⟩.

2. If ⟨M, ρ, κ, s⟩ C ⟨u_{1}, s_{1}⟩, then ⟨M, \overline{κ}, σ⟩ C^{⊖}

⟨u_{2}, σ_{2}⟩.

3. If ⟨P, ρ, s⟩ M_{c} ⟨u_{1}, s_{1}⟩, then ⟨P, σ⟩ M_{c}^{⊖} ⟨u_{2}, σ_{2}⟩.

4.4 Termination

Interpreted naïvely, the specifications for the abstract collecting interpreters define partial functions that diverge on some inputs, and hence are not data flow algorithms. However, this is not a problem, since it is possible to detect all loops in the derivations. More precisely, assume we have the following fragment of a derivation tree:

…

⟨M_{j}, σ_{j}⟩ M^{⊖} ? … ⟨M_{i}, σ_{i}⟩ M^{⊖} ? … ⟨M_{1}, σ_{1}⟩ M^{⊖} ?

The evaluation of M_{1} in store σ_{1} requires the value of M_{i} in store σ_{i}, which in turn requires the value of M_{j} in store σ_{j}, and so on. If the above fragment of the derivation is indeed infinite, then one of the M’s must be repeated infinitely often as the abstract syntax tree of the program has only a finite number of subtrees. Thus, without loss of generality, let M_{1} = M_{i} = M_{j} = M. By inspection of the direct abstract collecting interpreter, σ_{1} … ⊑ σ_{i}… ⊑ σ_{j} . . .. As the lattice of abstract stores does not have any infinite ascending chains, one of the σ’s in the sequence must be repeated: σ_{i} = σ_{j} = σ. Thus, all loops will result in two identical proof goals. Having detected a loop, we return the least precise value paired with the current store. Thus, if the arguments ⟨M, σ⟩ have already been considered, the direct interpreter returns the answer ⟨⟨⊤, CL^{⊤}⟩, σ⟩ where CL^{⊤} is the set of all abstract closures in the program. Similarly, the semantic-CPS interpreter returns

Domains:  Auxiliary Functions:
\overline{Ans} = \overline{Val} × \overline{Sto}
\overline{Sto} = \overline{Var} ⟶ ∘ \overline{Val}
\overline{Val} = \overline{Num} × P(\overline{Clo})
\overline{Clo} = (Var × Λ) + inc + dec

ϕ^{⊖} : Λ(V) × \overline{Sto} → \overline{Val}
ϕ^{⊖}(n, σ) = ⟨n, ∅⟩
ϕ^{⊖}(x, σ) = σ(x)
ϕ^{⊖}(add1, σ) = ⟨⊥, {inc}⟩
ϕ^{⊖}(sub1, σ) = ⟨⊥, {dec}⟩
ϕ^{⊖}((λx.M), σ) = ⟨⊥, {⟨cl^{⊖} x, M⟩}⟩

M^{⊖} : (Λ × \overline{Sto}) → \overline{Ans}

\frac{u = ϕ^{⊖}(V, σ)}{⟨V, σ⟩ M^{⊖} ⟨u, σ⟩}  \frac{u = ϕ^{⊖}(V, σ)  ⟨M, σ[x := σ(x) ⊔ u]⟩ M^{⊖} A}{⟨(let (x V) M), σ⟩ M^{⊖} A}

\frac{u_{1} = ϕ^{⊖}(V_{1}, σ) u_{2} = ϕ^{⊖}(V_{2}, σ) ⟨u_{1}, u_{2}, σ⟩ app^{⊖} ⟨u_{3}, σ_{3}⟩ ⟨M, σ_{3}[x := σ_{3}(x) ⊔ u_{3}]⟩ M^{⊖} A}{⟨(let (x (V_{1} V_{2})) M), σ⟩ M^{⊖} A}

\frac{u_{0} = ϕ^{⊖}(V_{0}, σ) ⟨M_{i}, σ⟩ M^{⊖} ⟨u_{1}, σ_{1}⟩ ⟨M, σ_{1}[x := σ_{1}(x) ⊔ u_{1}]⟩ M^{⊖} A}{⟨(let (x (if0 V_{0} M_{1} M_{2})) M), σ⟩ M^{⊖} A} i = 1 if u_{0} = ⟨0, ∅⟩, i = 2 if ⟨0, ∅⟩ ⋢ u_{0}.

\frac{⟨0, ∅⟩ u_{0} = ϕ^{⊖}(V_{0}, σ) ⟨M_{1}, σ⟩ M^{⊖} ⟨u_{1}, σ_{1}⟩ ⟨M_{2}, σ⟩ M^{⊖} ⟨u_{2}, σ_{2}⟩ ⟨M, (σ_{1} ⊔ σ_{2})[x := (σ_{1} ⊔ σ_{2})(x) ⊔ (u_{1} ⊔ u_{2})]⟩ M^{⊖} A}{⟨(let (x (if0 V_{0} M_{1} M_{2})) M), σ⟩ M^{⊖} A}

app^{⊖} : (\overline{Val} × \overline{Val} × \overline{Sto}) → \overline{Ans}

\frac{⟨cl_{1}, u, σ⟩ app_{1}^{⊖} A_{1} … ⟨cl_{n}, u, σ⟩ app_{1}^{⊖} A_{n}}{⟨⟨n, \{cl_{1},…, cl_{n}\}⟩, u, σ⟩ app^{⊖} ⨆_{i=1,n} A_{i}}

app_{1}^{⊖} : (\overline{Clo} × \overline{Val} × \overline{Sto}) → \overline{Ans}

\frac{u = ⟨add1^{⊖}(n), ∅⟩}{⟨inc, ⟨n, CL⟩, σ⟩ app_{1}^{⊖} ⟨u, σ⟩}  \frac{u = ⟨sub1^{⊖}(n), ∅⟩}{⟨dec, ⟨n, CL⟩, σ⟩ app_{1}^{⊖} ⟨u, σ⟩}  \frac{⟨M, σ[x := σ(x) ⊔ u]⟩ M^{⊖} A}{⟨⟨cl^{⊖} x, M⟩, u, σ⟩ app_{1}^{⊖} A}

Figure 4: Direct Abstract Collecting Interpreter

⟨⟨⊤, CL^{⊤}⟩, σ⟩ to the continuation κ. If the syntactic-CPS interpreter detects that the arguments ⟨P, σ⟩ have already been considered, it returns ⟨⟨⊤, CL^{⊤}, K^{⊤}⟩, σ⟩ where K^{⊤} is the set of all abstract continuations ⟨co^{⊖} x, P ⟩ in the program.

In the remainder of the paper, we will use “abstract collecting interpreter” or “data flow analysis” to refer to the terminating versions of the interpreters that detect loops as above.

5 Formal Relationships

After deriving the data flow analyzers, we turn our attention to the relationship between them. For the connection between the direct and syntactic-CPS analyses, we need an abstract version of the function δ that maps abstract direct values to abstract CPS values:

δ^{⊖}(⟨n, {cl_{1},…, cl_{i}}⟩) = ⟨n, {V^{⊖}(cl_{1}),…, V^{⊖}(cl_{i})}, ∅⟩ V^{⊖}(⟨cl^{⊖} x_{1}, M_{1}⟩) = ⟨cl^{⊖} x_{1}k_{1}, F_{k_{1}}[[M_{1}]]⟩ V^{⊖}(inc) = inck V^{⊖}(dec) = deck

The application of δ^{⊖} to stores and answers is pointwise and component-wise respectively.

5.1 Direct vs Syntactic-CPS

The first theorem establishes that the direct analysis of M may be more precise than the analysis of F_{k}[[M]].

Theorem 5.1 There exists M ∈ Λ and σ ∈ Sto such that:

• ⟨M, σ⟩ M^{⊖} ⟨u_{1}, σ_{1}⟩,

• ⟨F_{k}[[M]], δ^{⊖}(σ)[k := ⟨⊥, ∅, {stop}⟩]⟩ M_{c}^{⊖} ⟨u_{2}, σ_{2}⟩,

Domains:

\overline{Ans} = \overline{Val} × \overline{Sto}
\overline{Sto} = Var ⟶ ∘ \overline{Val}

\overline{Con} = Λ(E) :: \overline{Con} + nil
\overline{Val} = \overline{Num} × P(\overline{Clo})
\overline{Clo} = (Var × Λ) + inc + dec

C^{⊖} : (Λ × \overline{Con} × \overline{Sto}) → \overline{Ans}

\frac{u = ϕ^{⊖}(V, σ) ⟨κ, ⟨u, σ⟩⟩ appr^{⊖} A}{⟨V, κ, σ⟩ C^{⊖} A} \frac{u = ϕ^{⊖}(V, σ) ⟨M, κ, σ[x := σ(x) ⊔ u]⟩ C^{⊖} A}{⟨(let (x V) M), κ, σ⟩ C^{⊖} A}

\frac{u_{1} = ϕ^{⊖}(V_{1}, σ) u_{2} = ϕ^{⊖}(V_{2}, σ) ⟨u_{1}, u_{2}, (let (x [ ]) M) :: κ, σ⟩ appk^{⊖} A}{⟨(let (x (V_{1} V_{2})) M), κ, σ⟩ C^{⊖} A}

\frac{u_{0} = ϕ^{⊖}(V_{0}, σ) ⟨M_{i}, (let (x [ ]) M) :: κ, σ⟩ C^{⊖} A}{⟨(let (x (if0 V_{0} M_{1} M_{2})) M), κ, σ⟩ C^{⊖} A} i = 1 if u_{0} = ⟨0, ∅⟩, i = 2 if ⟨0, ∅⟩ ⋢ u_{0}.

\frac{⟨0, ∅⟩ u_{0} = ϕ^{⊖}(V_{0}, σ) ⟨M_{1}, (let (x [ ]) M) :: κ, σ⟩ C^{⊖} A_{1} ⟨M_{2}, (let (x [ ]) M) :: κ, σ⟩ C^{⊖} A_{2}}{⟨(let (x (if0 V_{0} M_{1} M_{2})) M), κ, σ⟩ C^{⊖} A_{1} ⊔ A_{2}}

appk^{⊖} : (\overline{Val} × \overline{Val} × \overline{Con} × \overline{Sto}) → \overline{Ans}

\frac{⟨cl_{1}, u, κ, σ⟩ appk_{1}^{⊖} A_{1} … ⟨cl_{n}, u, κ, σ⟩ appk_{1}^{⊖} A_{n}}{⟨⟨n, \{cl_{1},…, cl_{n}\}⟩, u, κ, σ⟩ appk^{⊖} ⨆_{i=1,n} A_{i}}

appk_{1}^{⊖} : (\overline{Clo} × \overline{Val} × \overline{Con} × \overline{Sto}) → \overline{Ans}

\frac{u = ⟨add1^{⊖}(n), ∅⟩ ⟨κ, ⟨u, σ⟩⟩ appr^{⊖} A}{⟨inc, ⟨n, CL⟩, κ, σ⟩ appk_{1}^{⊖} A}  \frac{u = ⟨sub1^{⊖}(n), ∅⟩ ⟨κ, ⟨u, σ⟩⟩ appr^{⊖} A}{⟨dec, ⟨n, CL⟩, κ, σ⟩ appk_{1}^{⊖} A}  \frac{⟨M, κ, σ[x := σ(x) ⊔ u]⟩ C^{⊖} A}{⟨⟨cl^{⊖} x, M⟩, u, κ, σ⟩ appk_{1}^{⊖} A}

appr^{⊖} : (\overline{Con} × \overline{Ans}) → \overline{Ans}

\frac{⟨M, κ, σ[x := σ(x) ⊔ u]⟩ C^{⊖} A}{⟨(let (x [ ]) M) :: κ, ⟨u, σ⟩⟩ appr^{⊖} A}  \overline{⟨nil, A⟩ appr^{⊖} A}

Figure 5: Semantic-CPS Abstract Collecting Interpreter

• δ^{⊖}(u_{1}) ⊑ u_{2}, and for each variable in the domain of σ_{1}, δ^{⊖}(σ_{1}(x)) ⊑ σ_{2}(x).

Proof. Let M be (let (a_{1} (f 1)) (let (a_{2} (f 2)) a_{2})), and let:

σ = {a_{1} ↦ ⟨⊥, ∅⟩,
a_{2} ↦ ⟨⊥, ∅⟩,
f ↦ ⟨⊥, {⟨cl^{⊖} x, x⟩}⟩,
x ↦ ⟨⊥, ∅⟩}.

It is straightforward to calculate that the result of the direct abstract collecting interpreter is A_{1} = ⟨u_{1}, σ_{1}⟩ where:

u_{1} = ⟨⊤, ∅⟩
σ_{1} = {a_{1} ↦ ⟨1, ∅⟩,
a_{2} ↦ ⟨⊤, ∅⟩,
f ↦ ⟨⊥, {⟨cl^{⊖} x, x⟩}⟩,
x ↦ ⟨⊤, ∅⟩}.

For the analysis of the CPS version, we have that:

F_{k}[[M]] = (f 1 (λa_{1}.(f 2 (λa_{2}.(k a_{2})))))
σ′ = {a_{1} ↦ ⟨⊥, ∅, ∅⟩,
a_{2} ↦ ⟨⊥, ∅, ∅⟩,

f ↦ ⟨⊥, {⟨cl^{⊖} xk_{1}, (k_{1} x)⟩}, ∅⟩,

x ↦ ⟨⊥, ∅, ∅⟩,
k ↦ ⟨⊥, ∅, {stop}⟩}.

The syntactic-CPS abstract collecting interpreter produces the answer A_{2} = ⟨u_{2}, σ_{2}⟩ where:

u_{2} = ⟨⊤, CL^{⊤}, K^{⊤}⟩
σ_{2} = {a_{1} ↦ ⟨⊤, ∅, ∅⟩,
a_{2} ↦ ⟨⊤, ∅, ∅⟩,

Domains:  Auxiliary Function:
\overline{Ans} = \overline{Val} × \overline{Sto}
\overline{Sto} = Var ⟶ ∘ \overline{Val}
\overline{Val} = \overline{Num} × P(\overline{Clo}) × P(\overline{Con})
\overline{Clo} = (Var × KVar × cps(Λ))

+ inck + deck

\overline{Con} = (Var × cps(Λ)) + stop

ϕ_{c}^{⊖} : cps(Λ)(W) × \overline{Sto} → \overline{Val}
ϕ_{c}^{⊖}(n, σ) = ⟨n, ∅, ∅⟩
ϕ_{c}^{⊖}(x, σ) = σ(x)
ϕ_{c}^{⊖}(add1k, σ) = ⟨⊥, {inck}, ∅⟩
ϕ_{c}^{⊖}(sub1k, σ) = ⟨⊥, {deck}, ∅⟩
ϕ_{c}^{⊖}((λxk.P), σ) = ⟨⊥, {⟨cl^{⊖} xk, P ⟩}, ∅⟩

M_{c}^{⊖} : (cps(Λ) × \overline{Sto}) → \overline{Ans}

\frac{κ = σ(k) u = ϕ_{c}^{⊖}(W, σ) ⟨κ, ⟨u, σ⟩⟩ appr_{c}^{⊖} A}{⟨(k W), σ⟩ M_{c}^{⊖} A}  \frac{u = ϕ_{c}^{⊖}(W, σ) ⟨P, σ[x := σ(x) ⊔ u]⟩ M_{c}^{⊖} A}{⟨(let (x W) P), σ⟩ M_{c}^{⊖} A}

\frac{u_{1} = ϕ_{c}^{⊖}(W_{1}, σ) u_{2} = ϕ_{c}^{⊖}(W_{2}, σ) ⟨u_{1}, u_{2}, ⟨⊥, ∅, ⟨co^{⊖} x, P ⟩⟩, σ⟩ app_{c}^{⊖} A}{⟨(W_{1} W_{2} (λx.P)), σ⟩ M_{c}^{⊖} A}

\frac{u_{0} = ϕ_{c}^{⊖}(W_{0}, σ) ⟨P_{i}, σ[k := σ(k) ⊔ ⟨⊥, ∅, ⟨co^{⊖} x, P ⟩⟩]⟩ M_{c}^{⊖} A}{⟨(let (k λx.P) (if0 W_{0} P_{1} P_{2})), σ⟩ M_{c}^{⊖} A} i = 1 if u_{0} = ⟨0, ∅, ∅⟩, i = 2 if ⟨0, ∅, ∅⟩ ⋢ u_{0}.

\frac{\begin{matrix}⟨0, ∅, ∅⟩ u_{0} = ϕ_{c}^{⊖}(W_{0}, σ) \\ ⟨P_{1}, σ[k := σ(k) ⊔ ⟨⊥, ∅, ⟨co^{⊖} x, P ⟩⟩]⟩ M_{c}^{⊖} A_{1} ⟨P_{2}, σ[k := σ(k) ⊔ ⟨⊥, ∅, ⟨co^{⊖} x, P ⟩⟩]⟩ M_{c}^{⊖} A_{2} \end{matrix}}{⟨(let (k λx.P) (if0 W_{0} P_{1} P_{2})), σ⟩ M_{c}^{⊖} A_{1} ⊔ A_{2}}

app_{c}^{⊖} : (\overline{Val} × \overline{Val} × \overline{Val} × \overline{Sto}) → \overline{Ans}

\frac{⟨cl_{1}, u, κ, σ⟩ app_{1c}^{⊖} A_{1} … ⟨cl_{n}, u, κ, σ⟩ app_{1c}^{⊖} A_{n}}{⟨⟨n, \{cl_{1},…, cl_{n}\}, K⟩, u, κ, σ⟩ app_{c}^{⊖} ⨆_{i=1,n} A_{i}}

app_{1c}^{⊖} : (\overline{Clo} × \overline{Val} × \overline{Val} × \overline{Sto}) → \overline{Ans}

\frac{u = ⟨add1^{⊖}(n), ∅, ∅⟩ ⟨κ, ⟨u, σ⟩⟩ appr_{c}^{⊖} A}{⟨inck, ⟨n, CL, K⟩, κ, σ⟩ app_{1c}^{⊖} A}  \frac{u = ⟨sub1^{⊖}(n), ∅, ∅⟩ ⟨κ, ⟨u, σ⟩⟩ appr_{c}^{⊖} A}{⟨deck, ⟨n, CL, K⟩, κ, σ⟩ app_{1c}^{⊖} A}

\frac{⟨P, σ[x := σ(x) ⊔ u, k := σ(k) ⊔ κ]⟩ M_{c}^{⊖} A}{⟨⟨cl^{⊖} xk, P ⟩, u, κ, σ⟩ app_{1c}^{⊖} A}

appr_{c}^{⊖} : (\overline{Val} × \overline{Ans}) → \overline{Ans}

\frac{⟨κ_{1}, ⟨u, σ⟩⟩ appr_{1c}^{⊖} A_{1} … ⟨κ_{n}, ⟨u, σ⟩⟩ appr_{1c}^{⊖} A_{n}}{⟨⟨n, CL, \{κ_{1},…, κ_{n}\}⟩, ⟨u, σ⟩⟩ appr_{c}^{⊖} ⨆_{i=1,n} A_{i}}

appr_{1c}^{⊖} : (\overline{Con} × \overline{Ans}) → Ans

\frac{⟨P, σ[x := σ(x) ⊔ u]⟩ M_{c}^{⊖} A}{⟨⟨co^{⊖} x, P ⟩, ⟨u, σ⟩⟩ appr_{1c}^{⊖} A}

⟨stop, A⟩ appr_{1c}^{⊖} A

Figure 6: Syntactic-CPS Abstract Collecting Interpreter

f ↦ ⟨⊥, {⟨cl^{⊖} xk_{1}, (k_{1} x)⟩}, ∅⟩,

x ↦ ⟨⊤, ∅, ∅⟩,

k_{1} ↦ ⟨⊥, ∅, { ⟨co^{⊖} a_{1}, (f 2 (λa_{2}.(k a_{2})))⟩,

⟨co^{⊖} a_{2}, (k a_{2})⟩}⟩

k ↦ ⟨⊥, ∅, {stop}⟩] The analysis of the source program is more precise since it determines that the variable a_{1} is constant (=1), while the analysis of the CPS program fails to produce any information about a_{1}.

Our second theorem states that the direct analysis of a program may also give less information than the syntactic-CPS analysis. Together with the previous theorem, the result establishes that the direct analysis of a source program is incomparable to the syntactic-CPS analysis.

Theorem 5.2 There exists a term M ∈ Λ such that:

• ⟨M, σ⟩ M^{⊖} ⟨u_{1}, σ_{1}⟩,

• ⟨F_{k}[[M]], δ^{⊖}(σ)[k := ⟨⊥, ∅, {stop}⟩]⟩ M_{c}^{⊖} ⟨u_{2}, σ_{2}⟩,

• δ^{⊖}(u_{1}) ⊒ u_{2}, and for each variable x in the domain of σ_{1}, δ^{⊖}(σ_{1}(x)) ⊒ σ_{2}(x).

Proof. To illustrate the principle, we present two cases in which the analysis of the CPS program yields more information than the direct analysis of the source program.

For the first case, take:

M = (let (a_{1} (if0 x 0 1))

(let (a_{2} (if0 a_{1} (+ a_{1} 3) (+ a_{1} 2))) a_{2}))

σ = {a_{1} ↦ ⟨⊥, ∅⟩, a_{2} ↦ ⟨⊥, ∅⟩, x ↦ ⟨⊤, ∅⟩}

where (+ a_{1} 3) and (+ a_{1} 2) are the obvious abbreviations. The direct analysis of the term, not knowing which branch to take, merges the abstract values of 0 and 1 at the variable a_{1} and hence loses all information about a_{2}. In contrast, the analysis of:

F_{k}[[M]] = (let (k′ λa_{1}.F_{k}[[(let (a_{2} (if0 a_{1} (a_{1} + 3) (a_{1} + 2))) a_{2})]]) (if0 x (k′ 0) (k′ 1)))

analyzes both (k′ 0) and (k′ 1) in a store that maps k′ ↦ ⟨co^{⊖} a_{1},…⟩. The analysis of each execution path determines that the abstract value of a_{2} is ⟨3, ∅, ∅⟩, which improves on the direct analysis.

For the second case, take M:

M = (let (a_{1} (f 3))

(let (a_{2} (if0 a_{1} 5 (if0 (sub1 a_{1}) 5 6))) a_{2}))

σ = {a_{1} ↦ ⟨⊥, ∅⟩

a_{2} ↦ ⟨⊥, ∅⟩, f ↦ ⟨⊥, {⟨cl^{⊖} d_{0}, 0⟩, ⟨cl^{⊖} d_{1}, 1⟩}⟩ d_{0} ↦ ⟨⊥, ∅⟩, d_{1} ↦ ⟨⊥, ∅⟩}

where we have not named the results of (sub1 a_{1}) and (if0 (sub1 a_{1}) 5 6) to avoid clutter. The direct analysis of M begins by applying both closures bound to f to the abstract value of 3. The analysis then combines the results of these two applications associating ⟨0, ∅⟩⊔ ⟨1, ∅⟩ = ⟨⊤, ∅⟩ with a_{1}. As a consequence, the analysis loses all information about the value of a_{2}. In contrast, the analysis of the CPS version:

(f 3 (λa_{1}.F_{k}[[(let (a_{2} (if0 a_{1} 5 (if0 (sub1 a_{1}) 5 6))) a_{2})]]))

duplicates the continuation (λa_{1}.. . .) when evaluating the application of each of the closures bound to f. The analysis determines that the value of a_{2} is ⟨5, ∅, ∅⟩ along each execution path and hence improves on the analysis of the source program.

5.2 Direct vs Semantic-CPS

The character of the relationship between the direct and the semantic-CPS analysis depends on a key property of analyses.

Definition 5.3. (Distributivity) An analysis is distributive^{5} if for all κ, A_{i}, and n:

⟨κ, ⨆_{i=1,n} A_{i}⟩ appr^{⊖} A_{f} iff

⟨κ, A_{1}⟩ appr^{⊖} B_{1} … ⟨κ, A_{n}⟩ appr^{⊖} B_{n}

and A_{f} = ⨆_{i=1,n} B_{n}.

When Distributivity does not hold, e.g., for constant propagation [9], the semantic-CPS data flow analyzer may gain information by duplicating the continuation along every execution path as in the right hand side of the condition. Otherwise, the results of the analyses are identical.

Theorem 5.4 Let M ∈ Λ, then ⟨M, κ, σ⟩ C^{⊖} A_{1} if and only if:

• ⟨M, σ⟩ M^{⊖} A_{2}, and ⟨κ, A_{2}⟩ appr^{⊖} A_{3}, and A_{1} ⊑ A_{3}, or

• if the Distributivity condition holds, ⟨M, σ⟩ M^{⊖} A_{2}, and ⟨κ, A_{2}⟩ appr^{⊖} A_{1}.

5.3 Syntactic-CPS vs Semantic-CPS

The semantic-CPS analyzer may yield more precise results than the syntactic-CPS analyzer since the latter may confuse the continuations collected at a given label.

Theorem 5.5 Let M ∈ Λ, then:

⟨M, nil, σ⟩ C^{⊖} A_{1} iff
⟨F_{k}[[M]], δ^{⊖}(σ)[k := ⟨⊥, ∅, {stop}⟩]⟩ M_{c}^{⊖} A_{2}

where δ^{⊖}(A_{1}) ⊑ A_{2}.

5In the traditional framework, the lattice is usually inverted and the Distributivity condition is stated using the greatest lower bound ⊓. In our case, the condition should be called Continuity but, to avoid confusion, we use the standard terminology.

6 Discussion of the Results

In summary, our theorems show that:

1. The syntactic-CPS analyzer may confuse some continuations, i.e., may analyze an infeasible path, and also duplicates the analysis of continuations along every execution path, i.e., may gather more information than the direct analyzer in nondistributive analyses.

2. The semantic-CPS analyzer does not suffer from the false return problem and increases the collected information in non-distributive analyses by the duplication of the analysis of continuations.

In the remainder of this section, we discuss each of the properties of the CPS analyzers in detail.

6.1 False Returns

In practice, many analyses do indeed confuse continuations when applied to CPS programs. For example, Shivers’s 0CFA analysis of CPS programs [16] merges distinct control paths unnecessarily. Shivers did not relate the problem to CPS but his example [16:p.33] is essentially the example for Theorem 5.1.

Given our result, we can explain how the CPS transformation confuses some data flow analyzers that associate (approximate) information with program points. Because the CPS transformation reifies the continuation to a value that the program manipulates explicitly, the analysis of a CPS program is obligated to collect, at each variable k, the set of continuations that k may refer to during the execution of the program. Thus, when considering a return, i.e., a call (k W), the analysis applies each of the continuations bound to k and merges the results. In contrast, the analysis of the source program and the semantic-CPS analysis do not collect continuations, but only consider the current continuation at any program point.

6.2 Duplication

The gain of information in semantic-CPS analyzers is folklore knowledge. Nielson [13] proved that, for a small imperative language, the semantic-CPS analysis computes the MOP (meet over all paths) solution and the direct analysis computes the less precise MFP (maximum fixed point) solution; Filho and Burn [6] improved the abstract interpretations of typed call-by-name languages using the CPS transformation. Our result shows that the gain in all cases is entirely due to the duplication of the analysis of the continuation along different execution paths. In the remainder of this section, we consider the impact of this duplication on the computability and cost of the analysis.

Intuitively, the difference between the direct semantics and the CPS analyses is that the former merges all the values of an expression before analyzing the continuation and the latter apply the continuation to each of the values of an expression and merge the results. Therefore, the duplication of the analysis of the continuation depends on the number of values an expression may have.

Thus far, every expression in our language had only a finite number of values: the analysis of a conditional expression may proceed along two paths, and the analysis of a procedure call may proceed along some finite number of paths, one for each abstract closure that the term in function position evaluates to. Consequently, at each conditional and at each call site, the continuation may be duplicated along each of the possible paths, at an overall exponential cost in the analysis.

In a realistic language, the duplication of the continuation causes the computation of the result of the CPS analysis to become undecidable. To illustrate this point, we assume an extension of the language with an explicit looping construct and a sufficiently rich set of primitives.

Let the construct loop be an infinite loop whose exact collecting semantics returns the infinite set of values {0, 1, 2,…}.^{6} The extensions of the direct and semantic-CPS analyzers are:

\frac{u_{i} = ⟨i, ∅⟩ A_{i} = ⟨u_{i}, σ⟩}{⟨loop, σ⟩ M^{⊖} (⨆_{i=0,∞} A_{i})}

\frac{u_{i} = ⟨i, ∅⟩ A_{i} = ⟨u_{i}, σ⟩ ⟨κ, A_{i}⟩ appr^{⊖} B_{i}}{⟨loop, κ, σ⟩ C^{⊖} (⨆_{i=0,∞} B_{i})}

In the direct interpreter, each u_{i} is an abstract number ⟨i, ∅⟩ and the least upper bound of the set {u_{i} | i ≥ 0} is ⟨⊤, ∅⟩. In the semantic-CPS case, the computation of ⨆_{i=0,∞} B_{i} is undecidable. The proof is an adaptation of Kam and Ullman’s proof [9] that it is undecidable to compute the MOP solution for a general program in an arbitrary monotone framework.

6.3 Conclusion

In conclusion, a practical analysis based on the CPS transformation should not perform any duplication when the analysis is distributive since the duplication would not yield more precise answers. In nondistributive cases, a CPS analysis should limit the amount of duplication for both computability and efficiency reasons. When the analysis of a CPS program does not perform any duplication, the net effect of transforming the program to CPS is to obscure the fact that there is only one control stack at any point during a computation. Hence a more practical alternative is to combine heuristic in-lining algorithms with a direct-style analysis.

6The construct loop corresponds to the following program fragment ‘x := 0; while true x := x + 1’.

Acknowledgements

We thank Hans Boehm for discussions about the undecidability of the semantic-CPS analysis, and Geoffrey Burn, Bruce Duba, Juarez Filho, Cormac Flanagan, John Greiner, Bob Harper, Nevin Heintze, Peter Lee, and Frank Pfenning for comments on an earlier version of this paper and for discussions of the results.

References

[1] Appel, A. Compiling with Continuations. Cambridge University Press (1992).

[2] Bondorf, A. Improving binding times without explicit CPS-conversion. In Proceedings of the ACM Conference on Lisp and Functional Programming (1992) 1–10.

[3] Consel, C. and Danvy, O. For a better support of static data flow. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (1991) 496–519.

[4] Cousot, P. and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (1977) 238–252.

[5] Filho, J. Muylaert. Improving abstract interpretations with CPS-translation. (1993). Unpublished Manuscript.

[6] Filho, J. Muylaert and Burn, G. Continuation passing transformation and abstract interpretation. In Burn, G., Gay, S., and Ryan, M., editors, Proceedings of the First Imperial College, Department of Computing, Workshop on Theory and Formal Methods (1993).

[7] Flanagan, C., Sabry, A., Duba, B. F., and Felleisen, M. The essence of compiling with continuations. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (1993) 237–247.

[8] Hudak, P. and Young, J. Collecting interpretations of expressions. ACM Transactions on Programming Languages and Systems, 13, 2 (April 1991) 269–290.

[9] Kam, J.B. and Ullman, J. D. Monotone data flow analysis frameworks. Acta Informatica, 7 (1977) 305–317.

[10] Kelsey, R. and Hudak, P. Realistic compilation by program transformation. In Conference Record of the 16th ACM Symposium on Principles of Programming Languages (1989) 281–292.

[11] Kranz, D., Kelsey, R., Rees, J., Hudak, P., Philbin, J., and Adams, N. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM Sigplan Symposium on Compiler Construction, Sigplan Notices, 21, 7 (1986) 219–233.

[12] Marlowe, T.J. and Ryder, B.G. Properties of data flow frameworks: A unified model. Acta Informatica (1990).

[13] Nielson, F. A denotational framework for data flow analysis. Acta Informatica, 18 (1982) 265– 287.

[14] Sabry, A. and Felleisen, M. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6, 3/4 (1993) 289–360. Also in Proceedings of the ACM Conference on Lisp and Functional Programming, 1992, and Technical Report 92-180, Rice University.

[15] Sabry, A. and Felleisen, M. Is Continuation-Passing Useful for Data Flow Analysis? Technical Report TR94-223, Rice University (1994).

[16] Shivers, O. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, Carnegie Mellon University (1991).

[17] Steele, G. L. Rabbit: A Compiler for Scheme. MIT AI Memo 474, Massachusetts Institute of Technology (1978).