Jan Midtgaard

Thomas P Jensen
email: thomas.jensen@inria.fr

Control-flow analysis of function calls and returns by abstract interpretation

interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, the analysis computes for each expression an abstract call-stack, effectively approximating where function calls return. The analysis is systematically derived by abstract interpretation of the stack-based C a EK abstract machine of Flanagan et al. using a series of Galois connections. We prove that the analysis is equivalent to an analysis obtained by first transforming the program into continuation-passing style and then performing control flow analysis of the transfored program. We then show how the analysis induces an equivalent constraint-based formulation, thereby providing a rational reconstruction of a constraint-based CFA from abstract interpretation principles.

Introduction

Control-flow analysis (CFA) of functional programs is concerned with determining how the program's functions call each other. In the case of the lambda calculus, this amounts to computing the flow of lambda expressions in order to determine what functions are effectively called in an application (e 1 e 2 ). The result of a CFA can be visualized as an oriented control flow graph (CFG) linking sub-expression e i to sub-expression e j if evaluation of e i may entail the immediate evaluation of e j . A CFA computes an approximation of the actual behaviour of the program and can be more or less accurate depending on the technique employed.

In his seminal work, Jones [START_REF] Jones | Flow Analysis of Lambda Expressions[END_REF][START_REF] Jones | Flow analysis of lambda expressions (preliminary version)[END_REF] proposed to use program analysis techniques to statically approximate the flow of lambda-expressions under both call-byvalue and call-by-name evaluation in the lambda calculus. Since then CFA has been the subject of an immense research effort [START_REF] Ayers | Abstract Analysis and Optimization of Scheme[END_REF][START_REF] Shivers | Control-flow analysis in Scheme[END_REF][START_REF] Sestoft | Replacing function parameters by global variables[END_REF][START_REF] Nielson | Infinitary control flow analysis: a collecting semantics for closure analysis[END_REF]-see the recent survey by Midtgaard [START_REF] Midtgaard | Control-flow analysis of functional programs[END_REF] for a complete list. CFA has been expressed using a variety of formalisms including data flow equations, type systems and constraint-based analysis. Surprisingly, nobody has employed Cousot's programme of calculational abstract interpretation [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF] in which a program analysis is calculated by systematically applying abstraction functions to a formal programming language semantics. The purpose of this article is to show that such a derivation is indeed feasible and that a number of advantages follow from taking this approach:

• The systematic derivation of a CFA for a higher-order functional language from a well-known operational semantics provides the resulting analysis with strong mathematical foundations. Its correctness follows directly from the general theorems of abstract interpretation.

• The approach is easily adapted to different variants of the source language. We demonstrate this by deriving a CFA for functional programs written in continuation-passing style.

• The common framework of these analyses enables their comparison. We take advantage of this to settle a question about the equivalence between the analysis of programs in direct and continuation-passing style.

• The resulting equations can be given an equivalent constraint-based presentation, providing ipso facto a rational reconstruction and a correctness proof of constraint-based CFA.

The article is organized as follows. Section 2 provides a concise enumeration of fundamental notions from abstract interpretation used in the rest of the article. In Section 3 we define the language of study (the lambda calculus in administrative normal form) and its semantics, and give an example of CFA of programs written in this language. Sections 4 and 5 contain the derivation of a 0-CFA from an operational semantics: the C a EK machine of Flanagan et al. [START_REF] Flanagan | The essence of compiling with continuations[END_REF]. In Section 4 we define a series of Galois connections that each specifies one aspect of the abstraction in the analysis. In Section 5 we calculate the analysis as the result of composing the collecting semantics induced by the abstract machine with these Galois connections. Section 6 uses the same technical machinery to derive a CFA for a language in continuation-passing style and sets up a relation between the two abstract domains that enables to prove a lock-step equivalence of the analysis of programs in direct style and the CPS analysis of their CPS counterparts. In Section 7 we show how the recursive equations defining the CFA of a program induce an equivalent formulation of the analysis, where the result of the analysis now is expressed as a solution to a set of constraints. Section 8 compares with related approaches and Section 9 concludes.

Preliminary versions of the results reported in this article were published at SAS 2008 [START_REF] Midtgaard | A calculational approach to control-flow analysis by abstract interpretation[END_REF] and ICFP 2009 [START_REF] Midtgaard | Control-flow analysis of function calls and returns by abstract interpretation[END_REF]. The present article is a revised version of the latter paper, extending the lock-step relation between the direct and continuation-passing style analyses to include integer constants. The paper has furthermore been expanded with proofs and details of derivations of the abstract interpretations.

Abstract interpretation

This section recalls basic notions of lattice theory and abstract interpretation [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF][START_REF] Cousot | Semantic foundations of program analysis[END_REF][START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF][START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF][START_REF] Davey | Introduction to Lattices and Order[END_REF] on which we base our developments in the subsequent sections. In particular, we introduce the notion of Galois connections and provide a list of known Galois connections that will be used to design the abstraction underlying the CFA developed in Section 4.

A partially ordered set (poset) S; ⊑ is a set S equipped with a partial order ⊑. A complete lattice is a poset C; ⊑, ⊥, ⊤, ⊔, ⊓ , such that the least upper bound ⊔S and the greatest lower bound ⊓S exists for every subset S of C. ⊥ = ⊓C denotes the infimum of C and ⊤ = ⊔C denotes the supremum of C. The set of total functions D → C, whose codomain is a complete lattice C; ⊑, ⊥, ⊤, ⊔, ⊓ , is itself a complete lattice D → C; ⊑, ⊥, ⊤, ⊔, ⊓ under the pointwise ordering f ⊑ f ′ ⇐⇒ ∀x.f (x) ⊑ f ′ (x), and with bottom, top, join, and meet extended similarly. The powersets ℘(S) of a set S ordered by set inclusion is a complete lattice ℘(S); ⊆, ∅, S, ∪, ∩ .

Galois connections

A Galois connection is a pair of functions α, γ between two posets C; ⊑ and A; ≤ such that for all a ∈ A, c ∈ C : α(c) ≤ a ⇐⇒ c ⊑ γ(a). Equivalently a Galois connection can be defined as a pair of functions satisfying The following Galois connections will be used in the article:

Elementwise Abstraction [START_REF] Cousot | Abstract interpretation of algebraic polynomial systems[END_REF]:. A function @ : C → A induces a Galois connection:

℘(C); ⊆ ----→ ← ---- α @ γ @ ℘(A); ⊆ α @ (P ) = {@(p) | p ∈ P } γ @ (Q) = {p | @(p) ∈ Q}
Cartesian abstraction [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]. One can approximate a set of tuples by a tuple of sets, by projecting out each component into a separate set:

℘(C 1 × . . . × C n ); ⊆ --→ ← --℘(C 1 ) × . . . × ℘(C n ); ⊆ × α × (r) = π 1 (r), . . ., π n (r) γ × ( X 1 , . . ., X n ) = X 1 × . . . × X n
Componentwise Abstraction [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]:. Assuming a series of Galois connections:

℘(C i ) ---→ ← --- αi γi
A i for i ∈ {1, . . . , n}, their componentwise composition induces a Galois connection on tuples:

℘(C 1 ) × . . . × ℘(C n ); ⊆ × ----→ ← ---- α⊗ γ⊗ A 1 × . . . × A n ; ⊆ ⊗ α ⊗ ( X 1 , . . ., X n ) = α 1 (X 1 ), . . ., α n (X n ) γ ⊗ ( x 1 , . . ., x n ) = γ 1 (x 1 ), . . ., γ n (x n )
We write ∪ ⊗ and ⊆ ⊗ for componentwise join and inclusion, respectively.

Pointwise Encoding of a Relation [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]:. A relation can be isomorphically encoded as a set-valued function by a Galois connection:

℘(A × B); ⊆ ----→ -→ ← ←----- αω γω A → ℘(B); ⊆ α ω (r) = λa. {b | a, b ∈ r} γ ω (f ) = { a, b | b ∈ f (a)}
Pointwise Abstraction of a Set of Functions [START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF]:. A given Galois connection on the co-domain

℘(C); ⊆ ---→ ← --- α γ
C ♯ ; ⊑ induces a Galois connection on a set of functions:

℘(D → C); ⊆ ----→ ← ---- αΠ γΠ D → C ♯ ; ⊑ α Π (F ) = λd. α({f (d) | f ∈ F }) γ Π (A) = {f | ∀d : f (d) ∈ γ(A(d))}
Subset Abstraction [START_REF] Cousot | Abstract interpretation of algebraic polynomial systems[END_REF]:. Given a set C and a strict subset A ⊂ C hereof, the restriction to the subset induces a Galois connection:

℘(C); ⊆ ----→ -→ ← ----- α⊂ γ⊂ ℘(A); ⊆ α ⊂ (X) = X ∩ A γ ⊂ (Y ) = Y ∪ (C \ A)
A(n upper) closure operator ρ is map ρ : S → S on a poset S; ⊑ , that is (a) monotone: (for all s, s ′ ∈ S : s ⊑ s ′ =⇒ ρ(s) ⊑ ρ(s ′ )), (b) extensive (for all s ∈ S : s ⊑ ρ(s)), and (c) idempotent, (for all s ∈ S : ρ(s) = ρ(ρ(s))). A closure operator ρ induces a Galois connection S; ⊑ --→ ←-ρ 1 ρ(S); ⊑ , writing ρ(S) for {ρ(s) | s ∈ S} and 1 for the identity function. Furthermore the image of a complete lattice C; ⊑, ⊥, ⊤, ⊔, ⊓ by an upper closure operator is itself a complete lattice ρ(C); ⊑, ρ(⊥), ⊤, λX. ρ(⊔X), ⊓ .

Abstract interpretation basics

Canonical abstract interpretation approximates the collecting semantics of a transition system [START_REF] Cousot | Semantic foundations of program analysis[END_REF]. A standard example of a collecting semantics is the reachable states from a given set of initial states I. Given a transition function T defined as:

T (Σ) = I ∪ {σ | ∃σ ′ ∈ Σ : σ ′ → σ}
we can compute the reachable states of T as the least fixed-point lfp T of T . The collecting semantics is ideal, in that it is the most precise analysis. Unfortunately it is in general uncomputable. Abstract interpretation therefore approximates the collecting semantics, by instead computing a fixed-point over an alternative and perhaps simpler domain. For this reason, abstract interpretation is also referred to as a theory of fixed-point approximation.

Abstractions are formally represented as Galois connections which connect complete lattices through a pair of adjoint functions α and γ. Galois connectionbased abstract interpretation suggests that one may derive an analysis systematically by composing the transition function with these adjoints: α • T • γ. The function so obtained is called the best correct aproximation with respect to T and α. In this setting Galois connections allow us to gradually refine the collecting semantics into a computable analysis function by mere calculation. Cousot [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF] has shown how to systematically construct a static analyser for a first-order imperative language using calculational abstract interpretation. An alternative "recipe" consists in rewriting the composition of the abstraction function and transition function α • T into something of the form T ♯ • α, from which the analysis function T ♯ can be read off [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. We will use the former approach in Section 4 and the latter approach in Section 5 for deriving a CFA.

An analysis function T ♯ is said to be complete with respect to an abstraction α if T ♯ • α = α • T . Intuitively, this means that the analysis is able to take full advantage of the information present in the abstract domain. The best correct approximation is not always a complete analysis function. The notion of completeness generalizes in a straightforward manner to the setting where T has different domain and codomain that are abstracted by different α'ssee Giacobazzi et al. [START_REF] Giacobazzi | Making abstract interpretations complete[END_REF].

Language and semantics

Our source language is a simple call-by-value core language known as administrative normal form (ANF). The grammar of ANF terms is given in Fig. 1.

P ∋ p ::= s (programs) T ∋ t ::= n | x | fn x => s (trivial expressions) C ∋ s ::= (serious expressions) t (return) | let x=t in s (let-binding) | t 0 t 1 (tail call) | let x=t 0 t 1 in s (non-tail call)
Figure 1: ANF grammar Following Reynolds [START_REF] Reynolds | Definitional interpreters for higher-order programming languages[END_REF], the grammar distinguishes serious expressions, i.e., terms whose evaluation may diverge, from trivial expressions, i.e., terms without risk of divergence. Trivial expressions include constants, variables, and functions, and serious expressions include returns, let-bindings, tail calls, and non-tail calls. Programs are serious expressions. For more explanations about the ANF, we refer to Danvy [START_REF] Danvy | Three Steps for the CPS Transformation[END_REF] and Flanagan et al. [START_REF] Flanagan | The essence of compiling with continuations[END_REF]. Throughout the rest of the paper we implicitly distinguish between syntactically identical sub-terms that occur at different places in an expression. This can be achieved, e.g., through a labelling of all sub-terms as is standard [START_REF] Nielson | Principles of Program Analysis[END_REF].

The analysis is calculated from a simple operational semantics in the form of an abstract machine. We use the environment-based C a EK abstract machine of Flanagan et al. [START_REF] Flanagan | The essence of compiling with continuations[END_REF] given in Fig. 2. The machine represents functional values as closures [START_REF] Landin | The mechanical evaluation of expressions[END_REF], i.e., pairs of a lambda-expression and an environment. The environment-component captures the (values of the) free variables of the lambda. Machine states are triples consisting of a serious expression, an environment and a control stack. The control stack is composed of elements ("stack frames") of the form [x, s, e] where x is the variable receiving the return value w of the current function call, and s is a serious expression whose evaluation in the environment e[x → w] represents the rest of the computation in that stack frame. The empty stack is represented by stop. The machine has a helper function µ for evaluation of trivial expressions. The machine is initialized with the input program, with an empty environment, and with an initial stack, that will bind the result of the program to a special variable x r before halting. Evaluation follows by repeated application of the machine transitions.

For example, the program (which we abbreviate p below)

let f=fn x => x in let a 1 =f 1 in let a 2 =f 2 in a 2
taken from Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF] gives rise to the following sequence of tran-

Val
′ -→ s ′ , e ′ [x → µ(t, e)], k ′ let x=t in s, e, k -→ s, e[x → µ(t, e)], k t 0 t 1 , e, k -→ s ′ , e ′ [x → w], k if [fn x => s ′ , e ′ ] =
eval (p) = w iff p, •, [x r , x r , •] :: stop -→ * x r , •[x r → w], stop (d) Machine evaluation
-→ let a 1 =f 1 in let a 2 =f 2 in a 2 , ef •[f → [fn x => x, •]], k init (let-binding) -→ x, •[x → 1], [a 1 , let a 2 =f 2 in a 2 , e f ] :: k init (non-tail call) -→ let a 2 =f 2 in a 2 , e f [a 1 → 1], k init (return) -→ x, •[x → 2], [a 2 , a 2 , e f [a 1 → 1]] :: k init (non-tail call) -→ a 2 , e f [a 1 → 1][a 2 → 2], k init (return) -→ x r , •[x r → 2], stop (return)
and hence eval (p) = 2 as one would expect. Now consider the example program in Fig. 3. The program contains three functions: two named function g and f and an anonymous function fn x => x. A standard direct-style CFA can determine that the applications of k in each branch of the conditional will call the anonymous function fn x => x at run time. Building a control-flow graph based on the output of a standard direct- 3b, where we have named the main expression of the program main. In addition to the above resolved call, our analysis will determine that the anonymous function returns to the let-binding of y in main upon completion, rather than to its caller. The analysis hence gives rise to the more precise control-flow graph in Figure 3c.

let g z = z in let f k = if b then

Control-flow analysis

As our collecting semantics we consider the reachable states of the C a EK machine, expressed as the least fixed point lfp F p of the following transition function. Proof. By case analysis on t. For constants n, we have

F : P → ℘(C × Env × K ) → ℘(C × Env × K ) F p (S ) = I p ∪ {s | ∃s ′ ∈ S : s ′ -→ s} where I p = { p, •, [x r , x
µ c (n, {e}) = {n} = {µ(n, e)}
For variables x, we have

µ c (x, {e}) = {w | ∃e ′ ∈ {e} : w = e ′ (x)} = {w | w = e(x)} = {µ(x, e)}
For abstractions, we have

µ c (fn x => s, {e}) = {[fn x => s, e ′ ] | ∃e ′ ∈ {e}} = {[fn x => s, e]} = {µ(fn x => s, e)}
The equivalence of the two helper functions follows straightforwardly. This lemma enables us to express an equivalent collecting semantics based on µ c , which appears in Fig. 4.

Lemma 4.2. ∀p, S : F p (S ) = F c p (S )
Proof. The definition of F p (S ) yields

I p ∪ s ′ ∈S {s | s ′ -→
{ s ′ , e ′ [x → w], k ′ }.
The other cases of the proof of this lemma follow similar reasoning.

The abstraction of the collecting semantics is staged in several steps. Figure 5 provides an overview. Intuitively, the analysis extracts three pieces of information from the set of reachable states.

1. An approximation of the set of reachable expressions.

A relation between expressions and control stacks that represents where

the values of expressions are returned to.

3. An abstract environment mapping variables to the expressions that may be bound to that variable. This is standard in CFA and allows to determine which functions are called at a given call site.

Keeping an explicit set of reachable expressions is more precise than leaving it out, once we further approximate the expression-stack pairs. Alternatively the reachable expressions would be approximated by the expressions present in the expression-stack relation. However expressions may be in the expression-stack To formalize this analysis, we first perform a Cartesian abstraction of the machine states, however keeping the relation between expressions and their corresponding control stacks. The next step in the approximation consists in closing the triples by a closure operator, to ensure that (a) any saved environment on the stack or nested within another environment is itself part of the environment set, and (b) that all expression-control stack pairs that appear further down in a control stack are also contained in the expression-stack relation. We explain this in more detail below (Section 4.2). Finally, we approximate stacks by their top element, we merge expressions with the same return point into equivalence classes, and we approximate closure values by their lambda expression.

µ c : T × ℘(Env ) → ℘(Val) µ c (n, E ) = {n} µ c (x, E ) = {w | ∃e ∈ E : w = e(x)} µ c (fn x => s, E ) = {[fn x => s, e] | ∃e ∈ E } (a) Helper function F c : P → ℘(C × Env × K ) → ℘(C × Env × K ) F c p (S ) = I p ∪ t, e, [x, s ′ , e ′ ]::k ′ ∈S w∈µc (t,{e}) { s ′ , e ′ [x → w], k ′ } ∪ let x=t in s, e, k ∈S w∈µc (t,{e}) { s, e[x → w], k } ∪ t0 t1, e, k ∈S [fn x => s ′ , e ′ ]∈µc(t0,{e}) w∈µc (t1,{e}) { s ′ , e ′ [x → w], k } ∪ let x=t0 t1 in s, e, k ∈S [fn y => s ′ , e ′ ]∈µc(t0,{e}) w∈µc (t1,{e}) { s ′ , e ′ [y → w], [x, s, e] :: k } (b) Transition function Figure 4: Collecting semantics ℘(C × Env × K ) α× collecting semantics F c ℘(C ) × ℘(C × K ) × ℘(Env ) γ× O O ρ - F × ρ(℘(C ) × ℘(C × K ) × ℘(Env )) 1 O O α⊗ - F ρ ℘(C ) × (C / ≡ → ℘(K ♯ )) × Env ♯ γ⊗ O O 0-CFA F ♯
In the following sections we provide a detailed explanation of each abstraction in turn. In order to illustrate the systematic calculation and still remain of a manageable size, we only provide the calculations for the return case t. Since we calculate with Galois connections on complete lattices, the abstraction functions are complete join morphisms (CJMs), and hence distribute over each element of a join, permitting us to do such case division. The remaining cases are proved similarly.

Projecting machine states

The mapping that extracts the three kinds of information described above is defined formally as follows.

℘(C × Env × K ) ----→ ← ---- α× γ× ℘(C ) × ℘(C × K ) × ℘(Env ) α × (S ) = π 1 S , { s, k | ∃e : s, e, k ∈ S }, π 2 S γ × ( C, F , E ) = { s, e, k | s ∈ C ∧ s, k ∈ F ∧ e ∈ E } Lemma 4.3. α × , γ × is a Galois connection.
Proof. The projection of a tuple space onto a sub-space of smaller dimension forms a Galois connection with its inverse. The function pair α × , γ × can therefore be characterized as the component-wise abstraction of three Galois connections and thus constitutes a Galois connection itself.

We use the notation ∪ × and ⊆ × for the componentwise join and componentwise inclusion of triples. As traditional [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF][START_REF] Cousot | Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages)[END_REF], we will assume that the abstract product domains throughout this article have been reduced with respect to the empty set, i.e., all triples A, B, C representing the empty set ∅

(γ a (A) = ∅ ∨ γ b (B) = ∅ ∨ γ c (C) = ∅) have been eliminated and replaced by a single bottom element ⊥ a , ⊥ b , ⊥ c .
We now calculate a new transfer function by composing the partly-relational abstraction with the collecting semantics. As explained above, this amounts to applying the abstraction to each of the set expressions that define the collecting semantics. For the return case t, we obtain the following derivation:

Let C, F , E ∈ ℘(C ) × ℘(C × K ) × ℘(Env ) be given. α × ( t, e, [x, s ′ , e ′ ]::k ′ ∈γ×( C, F , E ) w∈µc (t,{e}) { s ′ , e ′ [x → w], k ′ }) = × t, e, [x, s ′ , e ′ ]::k ′ ∈γ×( C, F , E ) w∈µc (t,{e}) α × ({ s ′ , e ′ [x → w], k ′ }) (α × a CJM) = × t, e, [x, s ′ , e ′ ]::k ′ ∈γ×( C, F , E ) w∈µc (t,{e}) {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} (def. α × ) = × α×({ t, e, [x, s ′ , e ′ ]::k ′ })⊆× C, F , E w∈µc (t,{e}) {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} (Galois conn.) = × {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} (def. α × )
By similar calculations, we obtain the transition function given in Fig. 6. Because the transition function has been obtained by equational reasoning, it is the best correct approximation with respect to the partly-relational approximation α × , as stated by the following theorem.

Theorem 4.1. ∀p, C, F , E : α × (F c p (γ × ( C, F , E ))) = F × p ( C, F , E )

A closure operator on machine states

For the final analysis, we are only interested in an abstraction of the information present in an expression-stack pair. More precisely, we aim at only keeping track of the link between an expression and the top stack frame in effect during its evaluation, throwing away everything below. However, we need to make this information explicit for all expressions appearing on the control stack, i.e., for a pair s, [x, s ′ , e] :: k we also want to retain that s ′ will eventually be evaluated with control stack k. Similarly, environments can be stored on the stack or inside other environments and will have to be extracted. We achieve this by defining a suitable closure operator on these nested structures. For environments, we adapt the definition of a constituent relation due to Milner and Tofte [START_REF] Milner | Co-induction in relational semantics[END_REF]. To deal with the control stack, we extend this to a structural order on expression-stack pairs. Definition 4.1 (Milner and Tofte's constituent relation). For each component x i of a tuple x 0 , . . . , x n we say that x i is a constituent of the tuple, written x 0 , . . . , x n ≻ x i . For a partial function 1 f = [x 0 → w 0 , . . . , x n → w n ], we say that each w i is a constituent of the function, written f ≻ w i .

F × : P → ℘(C ) × ℘(C × K ) × ℘(Env ) → ℘(C ) × ℘(C × K ) × ℘(Env ) F × p ( C, F , E ) = {p}, { p, [x r , x r , •] :: stop }, {•} ∪ × × {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ∪ × × {let x=t in s}, { let x=t in s, k }, {e} ⊆× C, F , E w∈µc (t,{e}) {s}, { s, k }, {e[x → w]} ∪ × × {t0 t1}, { t0 t1, k }, {e} ⊆× C, F , E [fn x => s ′ , e ′ ]∈µc(t0,{e}) w∈µc (t1,{e}) {s ′ }, { s ′ , k }, {e ′ [x → w]} ∪ × × {let x=t0 t1 in s}, { let x=t0 t1 in s, k }, {e} ⊆× C, F , E [fn y => s ′ , e ′ ]∈µc(t0,{e}) w∈µc (t1,{e}) {s ′ }, { s ′ , [x, s, e] :: k }, {e ′ [y → w]}
For example, the empty stack stop is a constituent of the non-empty stack [x r , x r , •] :: stop which we write as [x r , x r , •] :: stop ≻ stop. The empty environment is also a constituent thereof: [x r , x r , •] :: stop ≻ •. Similarly the closure w = [fn i => i, •] is a constituent of the extended environment 1 Milner and Tofte define the constituent relation for finite functions. We write ⋗ * for the expression-stack ordering induced by the reflexive, transitive closure of the expression-stack pair relation. The following lemma relates this expression-stack ordering to the constituent relation.

Lemma 4.4. ∀ s, k , s ′ , k ′ : s, k ⋗ * s ′ , k ′ =⇒ k ≻ * k ′ Proof. By induction. Assume that s, k = s 0 , k 0 ⋗ s 1 , k 1 ⋗ . . . ⋗ s n , k n = s ′ , k ′ . If n = 0 then k 0 = k n and hence k ≻ * k ′ .
Otherwise, we use the induction hypothesis to deduce that k 0 ≻ * k n-1 . In addition, we have that condition (a) of Definition 4.2 yields

s n-1 , k n-1 ⋗ s n , k n =⇒ k n-1 ≻ k n . Hence, k 0 ≻ * k n
Next, we define an operator ρ, defined in terms of the constituent relation and the expression-stack pair ordering. This operator takes triples consisting of sets of expressions, sets of expression-stack pairs and sets of environemnts. Its purpose is 1. to "extract" all environments residing on the stacks (condition s, k ≻ * e in the Definition below) or nested within another environment (condition e ′ ≻ * e) and add them to the set of environments, and 2. to ensure that any expression-stack pair that appears inside a control stack is added to the expression-stack relation (condition s ′ , k ′ ⋗ * s, k ).

Definition 4.3. Let ρ be the endo-function

ρ : ℘(C ) × ℘(C × K ) × ℘(Env ) → ℘(C ) × ℘(C × K ) × ℘(Env ) defined by ρ( C, F , E ) = C, { s, k | ∃ s ′ , k ′ ∈ F : s ′ , k ′ ⋗ * s, k }, {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ E : e ′ ≻ * e} Lemma 4.5

. ρ is a closure operator

Proof. There are three properties to prove of ρ: monotonicity, extensiveness and idempotence.

Monotonicity. Assume C, F , E ⊑ C ′ , F ′ , E ′ . Then C ⊆ C ′ , F ⊆ F ′ and E ⊆ E ′ . Hence ρ( C, F , E ) = C, { s, k | ∃ s ′ , k ′ ∈ F : s ′ , k ′ ⋗ * s, k }, {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ E : e ′ ≻ * e} ⊆ C ′ , { s, k | ∃ s ′ , k ′ ∈ F ′ : s ′ , k ′ ⋗ * s, k }, {e | ∃ s, k ∈ F ′ : s, k ≻ * e ∨ ∃e ′ ∈ E ′ : e ′ ≻ * e} = ρ( C ′ , F ′ , E ′ )
Extensiveness. This amounts to proving C, F , E ⊑ ρ( C, F , E ) which is shown by proving the inclusion component-wise. ρ is the identity on the first component, so this inclusion is trivial. For the second component, it suffices to observe that

F ⊆ { s, k | ∃ s ′ , k ′ ∈ F : s ′ , k ′ ⋗ * s, k }
due to the reflexivity of ⋗ * , and for the third component, we have that

E ⊆ {e | ∃e ′ ∈ E : e ′ ≻ * e} ⊆ {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ E : e ′ ≻ * e}. Idempotence. We need to show that ρ(ρ( C, F , E )) = ρ( C, F , E ). As ρ is extensive we have C, F , E ⊑ ρ( C, F , E ), and, as ρ is monotone, therefore also ρ( C, F , E ) ⊑ ρ(ρ( C, F , E ))
. So, it remains to show the other inclusion ⊒.

Since ρ is the identity on the first component, the desired inclusion for this component is immediate. In the following, we write (ρ( C, F , E ))↓2 and (ρ( C, F , E )) ↓ 3 for the second and third component of the triple ρ( C, F , E ). By unfolding the definition of ρ for the second component, we have

{ s, k | ∃ s ′ , k ′ ∈ (ρ( C, F , E ))↓2 : s ′ , k ′ ⋗ * s, k } = { s, k | ∃ s ′ , k ′ ∈ { s ′′ , k ′′ ∈ F : s ′′ , k ′′ ⋗ * s ′ , k ′ } : s ′ , k ′ ⋗ * s, k } = { s, k | ∃ s ′ , k ′ , s ′′ , k ′′ : s ′′ , k ′′ ∈ F ∧ s ′′ , k ′′ ⋗ * s ′ , k ′ ∧ s ′ , k ′ ⋗ * s, k } = { s, k | ∃ s ′′ , k ′′ ∈ F : s ′′ , k ′′ ⋗ * s, k } which is exactly the second component of ρ( C, F , E ).
For the third component, we need to show the inclusion

{e | ∃ s, k ∈ (ρ( C, F , E ))↓2 : s, k ≻ * e ∨ ∃e ′ ∈ (ρ( C, F , E )) ↓ 3 : e ′ ≻ * e} ⊆ (ρ( C, F , E )) ↓ 3
where the left hand side of the inclusion is obtained by unfolding the expression ρ(ρ( C, F , E )). Now, pick an e belonging to the left hand side. There are two cases to consider.

∃ s, k ∈ (ρ( C, F , E ))↓2 : s, k ≻ * e ⇒ ∃ s, k ∈ { s, k | ∃ s ′ , k ′ ∈ F : s ′ , k ′ ⋗ * s, k } : s, k ≻ * e ⇒ ∃ s, k , s ′ , k ′ : s ′ , k ′ ∈ F ∧ s ′ , k ′ ⋗ * s, k ∧ s, k ≻ * e ⇒ ∃ s, k , s ′ , k ′ : s ′ , k ′ ∈ F ∧ k ′ ≻ * k ∧ s, k ≻ * e (Lemma 4.4) ⇒ ∃ s, k , s ′ , k ′ : s ′ , k ′ ∈ F ∧ s ′ , k ′ ≻ * k ∧ s, k ≻ * e ⇒ ∃ s, k , s ′ , k ′ : s ′ , k ′ ∈ F ∧ s ′ , k ′ ≻ * k ∧ k ≻ * e ⇒ ∃ s, k , s ′ , k ′ : s ′ , k ′ ∈ F ∧ s ′ , k ′ ≻ * e ⇒ e ∈ (ρ( C, F , E )) ↓ 3 ∃e ′ ∈ (ρ( C, F , E )) ↓ 3 : e ′ ≻ * e ⇒ ∃e ′ ∈ {e ′′′ | ∃ s, k ∈ F : s, k ≻ * e ′′′ ∨ ∃e ′′ ∈ E : e ′′ ≻ * e ′′′ } : e ′ ≻ * e ⇒ ∃e ′ ∈ {e ′′′ | ∃ s, k ∈ F : s, k ≻ * e ′′′ } ∪ {e ′′′ | ∃e ′′ ∈ E : e ′′ ≻ * e ′′′ } : e ′ ≻ * e ⇒ ∃e ′ : (∃ s, k ∈ F : s, k ≻ * e ′ ∧ e ′ ≻ * e) ∨ (∃e ′′ ∈ E : e ′′ ≻ * e ′ ∧ e ′ ≻ * e) ⇒ (∃ s, k ∈ F : s, k ≻ * e) ∨ (∃e ′′ ∈ E : e ′′ ≻ * e ′ ∧ e ′ ≻ * e) ⇒ e ∈ (ρ( C, F , E )) ↓ 3
In either case, we show that e belongs to the right hand side of the inclusion. This proves the inclusion for the third component, and concludes the proof of idempotence.

We note without proof that ρ preserves least upper bounds, i.e., it is a disjunctive closure. We can now formulate an abstraction on the triples:

℘(C )×℘(C × K )×℘(Env) ---→ ← --- ρ 1 ρ(℘(C )×℘(C × K )×℘(Env))
We use the notation ∪ ρ for the join operation λX. ρ(∪ × X) on the closure operator-induced complete lattice. First observe that in our case:

∪ ρ = λX. ρ( × i X i ) = λX. × i ρ(X i ) = λX. × i X i = ∪ ×
Based on the closure operator-based Galois connection, we calculate a new intermediate transfer function

F ρ . Now let C, F , E ∈ ρ(℘(C ) × ℘(C × K ) × ℘(Env )) be given. ρ( × {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) = ρ {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) (ρ a CJM) = × {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) (by observation)
The resulting transfer function appears in Fig. 7. This transfer function differs only minimally from the one in Fig. 6, in that (a) the signature has changed, (b) the set of initial states has been "closed" and now contains the structurally smaller pair x r , stop , and (c) the four indexed joins now each join "closed" triples in the image of the closure operator.

By construction, the new transition function satisfies the following theorem.

Theorem 4.2. ∀p, C, F , E : ρ • F × p • 1( C, F , E ) = F ρ p ( C, F , E )

Abstracting the expression-stack relation

Since stacks can grow unbounded (for non-tail recursive programs), we need to approximate the stack component and hereby the expression-stack relation. The approximation that we shall be using is simply to keep only the top element of the stack and throw away the rest. We formalize this through a grammar of abstract stacks and an elementwise operator @ : C × K → C × K ♯ operating on expression-stack pairs.

K ♯ ∋ k ♯ ::= stop | [x, s] (abstract stacks) @( s, stop ) = s, stop @( s, [x, s ′ , e] :: k ) = s, [x, s ′ ]
This elementwise operator constitutes an elementwise abstraction that gives rise to a Galois connection as described in Section 2.1. Based hereon we define a second elementwise operator @ ′ : C × K ♯ → C / ≡ × K ♯ mapping the first component of an expression-stack pair to a representative of its corresponding equivalence class:

α @ : ℘(C × K ) → ℘(C × K ♯ ) α @ (F ) = {@( s, k ) | s, k ∈ F } γ @ (F ♯ ) = { s, k | @( s, k ) ∈ F ♯ } ℘(C × K ) ----→ ← ---- α @ γ @ ℘(C × K ♯ ) F ρ : P → ρ(℘(C ) × ℘(C × K ) × ℘(Env )) → ρ(℘(C ) × ℘(C × K ) × ℘(Env )) F ρ p ( C, F , E ) = {p}, { p, [x r , x r , •] :: stop , x r , stop }, {•} ∪ × × {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) ∪ × × {let x=t in s}, { let x=t in s, k }, {e} ⊆× C, F , E w∈µc (t,{e}) ρ( {s}, { s, k }, {e[x → w]} ) ∪ × × {t0 t1}, { t0 t1, k }, {e} ⊆× C, F , E [fn x => s ′ , e ′ ]∈µc (t0,{e}) w∈µc (t1,{e}) ρ( {s ′ }, { s ′ , k }, {e ′ [x → w]} ) ∪ × × {let x=t0 t1 in s}, { let x=t0 t1 in s, k }, {e} ⊆× C, F , E [fn y => s ′ , e ′ ]∈µc (t0,{e}) w∈µc (t1,{e}) ρ( {s ′ }, { s ′ , [x, s, e] :: k }, {e ′ [y → w]} )
@ ′ ( s, k ♯ ) = [s] ≡ , k ♯
We can choose the outermost expression as a representative for each equivalence class by a linear top-down traversal of the input program. By composing the above Galois connection with a Galois connection α ω for pointwise encoding of a relation (Section 2.1) we obtain our abstraction of the expression-stack relation:

℘(C × K ) ----→ ← ---- αst γst C / ≡ → ℘(K ♯ )
where

α st = α ω • α @ ′ • α @ = λF . ˙ s, k ∈F α ω ({@ ′ • @( s, k )}) and γ st = γ @ • γ @ ′ • γ ω .
We can now prove a lemma relating the concrete and abstract expression-stack relations.

C, F , E ∈ ρ(℘(C ) × ℘(C × K ) × ℘(Env )) be given. s, [x, s ′ , e] :: k ∈ F =⇒ e ∈ E ∧ { s ′ , k } ⊆ F ∧ {[x, s ′ ]} ⊆ α st (F )([s] ≡ ) Proof. Assume { s, [x, s ′ , e] :: k } ⊆ F . Now s, [x, s ′ ,
e] :: k ≻ * e and hence e ∈ E by the assumption on E . Furthermore s, [x, s ′ , e] :: k ⋗ s ′ , k hence { s ′ , k } ⊆ F by the assumption on F . For the last part we reason as follows:

=⇒ α st ({ s, [x, s ′ , e] :: k }) ⊆ α st (F ) (α st monotone) ⇐⇒ ˙ s ′′ , k ′′ ∈{ s, [x, s ′ , e]::k } α ω ({@ ′ • @( s ′′ , k ′′ )}) ⊆ α st (F ) (def. α st ) ⇐⇒ α ω ({@ ′ • @( s, [x, s ′ , e] :: k )}) ⊆ α st (F ) (def. ∪) ⇐⇒ α ω ({@ ′ ( s, [x, s ′ ] )}) ⊆ α st (F ) (def. @) ⇐⇒ α ω ({ [s] ≡ , [x, s ′ ] }) ⊆ α st (F ) (def. @ ′ ) ⇐⇒ λ_. ∅[[s] ≡ → {[x, s ′ ]}] ⊆ α st (F ) (def. α ω ) ⇐⇒ {[x, s ′ ]} ⊆ α st (F )([s] ≡ ) (def. ⊆)

Abstracting environments

We also abstract values using an elementwise abstraction. Again we formulate a grammar of abstract values and an elementwise operator @ : Val → Val ♯ mapping concrete to abstract values.

Val ♯ ∋ w ♯ ::= n | [fn x => s] @(n) = n @([fn x => s, e]) = [fn x => s]
The abstraction of environments, which are themselves partial functions, can be obtained by composing the two Galois connections Pointwise Abstraction of a Set of Functions and Subset Abstraction (see Section 2.1) as follows.

A standard trick is to regard partial functions r : D ⇀ C as total functions r ⊥ : D → (C ∪ ⊥) where ⊥ ⊑ ⊥ ⊑ c, for all c ∈ C. Now consider environments e ∈ Var ⇀ Val to be total functions Var → (Val ∪ ⊥) using this idea. In this context the bottom element ⊥ will denote variable lookup failure. Now compose a subset abstraction

℘(Val ∪ ⊥) ----→ -→ ← ----- α⊂ γ⊂ ℘(Val )
with the value abstraction from the previous section, and feed the result to the pointwise abstraction above. The

Putting it all together

We can now calculate the analysis as the abstraction of triplet of sets into abstract triples by a componentwise abstraction.

For the set of expressions ℘(C ) we use the identity abstraction consisting of two identity functions. For the expression-stack relation ℘(C × K ) we use the expression-stack abstraction α st developed in Section 4.3. For the set of environments ℘(Env ) we use the environment abstraction α Π developed in Section 4.4. These can be combined using the Componentwise Abstraction Galois connection into the last abstraction step depicted in Figure 5.

Calculating the analysis

Using the alternative "recipe" we can calculate the analysis by "pushing α's" under the intermediate transition function:

α ⊗ (F ρ p ( C, F , E )) ⊆ ⊗ F ♯ p ( C, α st (F ), α Π (E ) )
from which the final definition of F ♯ p can be read off. We recall that α st was defined in Section 4.4 and α Π in Section 4.4. For space-saving purposes the calculation is divided into a number of observations, on which the derivation relies

. Let C, F , E ∈ ρ(℘(C ) × ℘(C × K ) × ℘(Env )) be given. First observe that: {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ ( {e ′ }⊆E w∈µc (t,E ) {e ′ [x → w]}) : e ′ ≻ * e} = {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ E , w ∈ µ c (t, E ) : e ′ [x → w] ≻ * e} (def. ∪) = {e | ∃ s, k ∈ F : s, k ≻ * e} ∪ {e | ∃e ′ ∈ E , w ∈ µ c (t, E ) : e ′ [x → w] ≻ * e} (def. ∨) ⊆ E ∪ {e | ∃e ′ ∈ E , w ∈ µ c (t, E ) : e ′ [x → w] ≻ * e} (assumption on E ) = E ∪ {e | ∃e ′ ∈ E , w ∈ µ c (t, E ) : e ′ [x → w] = e ∨ e ′ ≻ * e ∨ w ≻ * e} (case analysis) = E ∪ {e | ∃e ′ ∈ E , w ∈ µ c (t, E ) : e ′ [x → w] = e ∨ e ′ ≻ * e} (by Lemma 4.9) = E ∪ {e | ∃e ′ ∈ E , w ∈ µ c (t, E ) : e ′ [x → w] = e} (assumption on E ) = E ∪ {e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )} (def =)
Secondly, observe that:

× { s ′ , k ′ }⊆F {e ′ }⊆E {e}⊆E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) = × { s ′ , k ′ }⊆F {e ′ }⊆E w∈µc (t,E ) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) (def. µ c ) = × {e ′ }⊆E w∈µc (t,E ) ρ( × { s ′ , k ′ }⊆F {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} ) (ρ a CJM) = × {e ′ }⊆E w∈µc (t,E ) ρ( {s ′ }, { s ′ , k ′ }⊆F { s ′ , k ′ }, {e ′ [x → w]} ) (def. ∪ × ) ⊆ × × {e ′ }⊆E w∈µc (t,E ) ρ( {s ′ }, F , {e ′ [x → w]} ) (def. ∪) = ρ( × {e ′ }⊆E w∈µc (t,E ) {s ′ }, F , {e ′ [x → w]} ) (ρ a CJM) = ρ( {s ′ }, F , {e ′ }⊆E w∈µc (t,E ) {e ′ [x → w]} ) (def. ∪ × ) = {s ′ }, { s, k | ∃ s ′ , k ′ ∈ F : s ′ , k ′ ⋗ * s, k }, {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ {e ′ }⊆E w∈µc (t,E ) {e ′ [x → w]} : e ′ ≻ * e} (def. ρ) = {s ′ }, F , {e | ∃ s, k ∈ F : s, k ≻ * e ∨ ∃e ′ ∈ {e ′ }⊆E w∈µc (t,E ) {e ′ [x → w]} : e ′ ≻ * e} (assumption on F ) ⊆ × {s ′ }, F , E ∪ {e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )} (First obs.)
Thirdly, observe that:

α Π (E ∪ {e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )}) = α Π (E ) ∪ α Π ({e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )}) (α Π a CJM) = α Π (E ) ∪ α Π ({λy. if y = x then w else e ′ (y) | e ′ ∈ E , w ∈ µ c (t, E )}) (def. extend) = α Π (E ) ∪ λy. if y = x then α @ ({w | w ∈ µ c (t, E )}) else α @ ({e ′ (y) | e ′ ∈ E }) (def. α Π ) = α Π (E ) ∪ λy. if y = x then α @ (µ c (t, E )) else α Π (E )(y) (def. α Π ) = α Π (E ) ∪ λy. if y = x then µ ♯ (t, α Π (E )) else α Π (E )(y) (by Lemma 4.7) = α Π (E ) ∪ α Π (E )[x → µ ♯ (t, α Π (E ))] (def. extend) = α Π (E ) ∪ [x → µ ♯ (t, α Π (E ))] (def. ∪)
where we have written [x → . . .] as shorthand for λ_. ∅[x → . . .]. Now we can calculate the analysis:

α ⊗ ( × {t}, { t, [x, s ′ , e ′ ]::k ′ }, {e} ⊆× C, F , E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} )) = α ⊗ ( × {t}⊆C { t, [x, s ′ , e ′ ]::k ′ }⊆F {e}⊆E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} )) (def. ⊆ × ) ⊆ ⊗ α ⊗ ( × {t}⊆C {[x, s ′ ]}⊆αst (F )([t]≡) { s ′ , k ′ }⊆F {e ′ }⊆E {e}⊆E w∈µc (t,{e}) ρ( {s ′ }, { s ′ , k ′ }, {e ′ [x → w]} )) (by Lemma 4.6) ⊆ ⊗ α ⊗ ( × {t}⊆C {[x, s ′ ]}⊆αst (F )([t]≡) {s ′ }, F , E ∪ {e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )} ) (Second obs.) = ⊗ {t}⊆C {[x, s ′ ]}⊆αst (F )([t]≡) α ⊗ ( {s ′ }, F , E ∪ {e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )} ) (α ⊗ a CJM) = ⊗ {t}⊆C {[x, s ′ ]}⊆αst (F )([t]≡) {s ′ }, α st (F ), α Π (E ∪ {e ′ [x → w] | e ′ ∈ E , w ∈ µ c (t, E )}) (def. α ⊗ ) = × {t}⊆C {[x, s ′ ]}⊆αst (F )([t]≡) {s ′ }, α st (F ), α Π (E ) ∪ [x → µ ♯ (t, α Π (E ))] (Third obs.)
The resulting analysis appears in Fig. 8. The alert reader may have noticed that this final abstraction is not complete in that the above derivation contains an inequality. The inequality is strict as illustrated by the following example. Consider two environments:

e 1 = •[x → [fn i => i, •], y → [fn j => j, •]] e 2 = •[x → [fn j => j, •], y → [fn i => i, •]]
and a triple containing the two: {x y}, { x y, stop }, {e 1 , e 2 } . Technically this triple is not closed under the closure operator ρ as the two environments

F ♯ : P → ℘(C ) × (C / ≡ → ℘(K ♯ )) × Env ♯ → ℘(C ) × (C / ≡ → ℘(K ♯ )) × Env ♯ F ♯ p ( C, F ♯ , E ♯ ) = {p}, [[p] ≡ → {[x r , x r ]}, [x r ] ≡ → {stop}], λ_. ∅ ∪ ⊗ ⊗ {t}⊆C {[x, s ′ ]}⊆F ♯ ([t]≡) {s ′ }, F ♯ , E ♯ ∪ [x → µ ♯ (t, E ♯ )] ∪ ⊗ ⊗ {let x=t in s}⊆C {s}, F ♯ , E ♯ ∪ [x → µ ♯ (t, E ♯ )] ∪ ⊗ ⊗ {t0 t1}⊆C {[fn x => s ′ ]}∈µ ♯ (t0,E ♯ ) {s ′ }, F ♯ ∪ [[s ′ ] ≡ → F ♯ ([t 0 t 1 ] ≡ )], E ♯ ∪ [x → µ ♯ (t 1 , E ♯ )] ∪ ⊗ ⊗ {let x=t0 t1 in s}⊆C {[fn y => s ′ ]}∈µ ♯ (t0,E ♯ ) {s ′ }, F ♯ ∪ [[s ′ ] ≡ → {[x, s]}], E ♯ ∪ [y → µ ♯ (t 1 , E ♯ )]
} )) = α ⊗ ( {p, i, j}, { p, [x r , x r , •] :: stop , x r , stop , i, stop , j, stop }, {•, •[i → [fn j => j, •]], •[j → [fn i => i, •]]} ) = {p, i, j}, [[p] ≡ → {[x r , x r ]}, [x r ] ≡ → {stop}, [i] ≡ → {stop}, [j] ≡ → {stop}], [i → {[fn j => j]}, j → {[fn i => i]}] whereas F ♯ p ( {x y}, α st ({ x y, stop }), α Π ({•, e 1 , e 2 }) ) = F ♯ p ( {x y}, [[x y] ≡ → stop], [x → {[fn i => i], [fn j => j]}, y → {[fn i => i], [fn j => j]}] ) = {p, i, j}, [[p] ≡ → {[x r , x r ]}, [x r ] ≡ → {stop}, [i] ≡ → {stop}, [j] ≡ → {stop}], [i → {[fn i => i], [fn j => j]}, j → {[fn i => i], [fn j => j]}]
for a program p. This example illustrates the information loss when abstracting the bindings of a set of environments as independent attributes to one global abstract environment: the analysis loses track of which bindings belong to the same environment. Whereas completeness is a desirable goal in an abstract interpretation it is not possible in general without refining the abstract domain [START_REF] Giacobazzi | Making abstract interpretations complete[END_REF]. As traditional [START_REF] Cousot | The calculational design of a generic abstract interpreter[END_REF], we instead limit upward judgements to a minimum. As a corollary of the construction, the analysis safely approximates the reachable states of the abstract machine.

Corollary 5.1. ∀p : α ⊗ • ρ • α × (lfp F p ) ⊆ ⊗ lfp F ♯ p
Proof. The only property that needs to be verified is that the resulting function is monotone (this does not follow automatically because of the upwards judgment in the derivation). The monotonicity follows from the fact that all operations involved in the definition of F ♯ are monotone.

Table 1 in Section 6 contains an example trace of the analysis function and how it calculates an approximation of reachable states.

Characteristics of the derived analysis

First of all the analysis incorporates reachability: it computes an approximate set of reachable expressions and will only analyse those reachable program fragments. Reachability analyses have previously been discovered independently [START_REF] Ayers | Efficient closure analysis with reachability[END_REF][START_REF] Palsberg | Safety analysis versus type inference[END_REF][START_REF] Biswas | A demand-driven set-based analysis[END_REF][START_REF] Gasser | Systematic realisation of control flow analyses for CML[END_REF]. In our case they arise naturally from a projecting abstraction of a reachable states collecting semantics.

Second the formulation materializes monomorphism into two mappings: (a) one mapping merging all bindings to the same variable, and (b) one mapping merging all calling contexts of the same function. Both characteristics are well known, but our presentation literally captures this phenomenon in two approximation functions.

Third the analysis handles returns inside-out ("callee-restore"), in that the called function restores control from the approximate control stack and propagates the obtained return values. This differs from the traditional direct-style presentations [START_REF] Palsberg | Closure analysis in constraint form[END_REF][START_REF] Nielson | Principles of Program Analysis[END_REF] that handle returns outside-in ("caller-restore") where the caller propagates the obtained return values from the body of the function to the call site (typically formulated as conditional constraints). Such caller-restore CFAs typically mimic the recursive nature of a corresponding interpreter, e.g., a big-step or denotational semantics. As a consequence they need not abstract the call stack. In our case the starting point was a callee-restore machine with an explicit call stack. Our systematic derivation of the "abstract interpreter" inherits this callee-restore strategy. We believe that the same strategy should be used by both a semantics and a corresponding analysis -an aspect that goes beyond analysing functional program. E.g., the Java byte code semantics of Cachera et al. [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF] uses a callee-restore strategy, whereas their corresponding flow-logic CFA is caller-restore. The mismatch of control transfer needlessly complicated the induction hypothesis of the machine-checked soundness proof [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF]. In the words of Cachera et al. [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF]: "This is because the effect of the return is simulated by a constraint (. . . ) attached to a different instruction".

In this presentation we did not include an explicit construct for recursive functions. Since our source language is untyped, it is possible to encode recursion through fixed-point operators. Explicit recursion is typically modelled by circular environments. The current formulation extends straight forwardly to handle those, because of our two-staged environment abstraction (closure operator and pointwise extended value abstraction).

Control-flow analysis of programs in continuation-passing style

In this section we present a CFA with reachability for a language in continuationpassing style (CPS). This analysis has been derived in the same way as the ANF CFA was derived in the previous section, using the stack-less CE-machine of Flanagan et al. [START_REF] Flanagan | The essence of compiling with continuations[END_REF] as operational semantics. Details of the derivation can be found in Midtgaard and Jensen [START_REF] Midtgaard | A calculational approach to control-flow analysis by abstract interpretation[END_REF]. We prove that the ANF analysis derived in this article achieves the same precision as obtained by first transforming a program into CPS and then using the CPS analysis. This is done by defining a relation that captures how the direct-style analysis and the CPS analysis operate in lock-step.

The grammar of CPS terms is given in Fig. 9. The grammar distinguishes variables in the original source program x ∈ X , from intermediate variables v ∈ V and continuation variables k ∈ K . We assume the three classes are non-overlapping. Their union constitute the domain of CPS variables Var = X ∪ V ∪ K . Trivial CPS expressions also include constants and functions.

CPS transformation and back again

In order to state the relation between the ANF and CPS analyses we first recall the relevant program transformations. The below presentation is based on Danvy [START_REF] Danvy | Three Steps for the CPS Transformation[END_REF], Flanagan et al. [START_REF] Flanagan | The essence of compiling with continuations[END_REF], and Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF].

The CPS transformation given in Fig. 10(a) is defined by two mutually recursive functions for serious and trivial expressions, respectively. A continuation variable k is provided in the initial call to F . A fresh k is generated in V's lambda abstraction case. To ease the expression of the relation, we choose k unique to the serious expression sk s . It follows that we only need one k per lambda abstraction in the original program + an additional k in the initial case.

It is immediate from the definition of F that the CPS transformation of a let-binding let x=t in s and the CPS transformation of its body s share the same continuation identifier -and similarly for non-tail calls. Hence we shall equate the two:

Definition 6.1. k s ≡ k s ′ iff s ≡ s ′
The direct-style transform given in Fig. 10(b) is defined by two mutually recursive functions over serious and trivial CPS expressions. We define the direct-style transformation of a program fn k => e as the direct-style transformation of its body U[e]. Transforming a program, a serious expression, or a trivial expression to CPS and back to direct style yields the original expression.

Lemma 6.1. D[C[p]] = p ∧ U[F k [s]] = s ∧ P[V[t]] = t
Proof. The proof follows by straightforward (mutual) structural induction on trivial and serious expressions. The definition relies on two special variables k r and v r , the first of which names the initial continuation and the second of which names the result of the program. To ensure the most precise analysis result, variables in the source program can be renamed to be distinct as is traditional in control-flow analysis [START_REF] Nielson | Principles of Program Analysis[END_REF].

CPS analysis

Analysis equivalence

Before formally stating the equivalence of the two analyses we will study an example run. As our example we use the ANF program:

let f=fn x => x in let a 1 =f 1 in let a 2 =f 2 in a 2
taken from Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF]. The analysis trace appears in the left column of Table 1. Similarly we study the CPS analysis of the CPS transformed program. The analysis trace appears in the right column of Table 1. Contrary to Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF] both the ANF and the CPS analyses achieve the same precision on the example, determining that a 1 will be bound to one of the two integer literals. Note that integers are not approximated in either analysis. Doing so would be straightforward by utilizing the isomorphism between a mixed set of tagged elements and two separate sets for each tag [START_REF] Deutsch | On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications[END_REF]:

℘(Val ♯ ) = ℘(Const + Lam) ---→ -→ ← ←---- α γ ℘(Const ) × ℘(Lam)
One can now choose to approximate the set of integer constants further, e.g, by using intervals [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF], or by the constant propagation lattice [START_REF] Kildall | A unified approach to global program optimization[END_REF] as in the analyses of Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF], as long as one applies the same abstraction of integers in both ANF and in CPS.

We are now in position to state our main theorem relating the ANF analysis to the CPS analysis. Intuitively the theorem relates:

• reachability in ANF to CPS reachability

• abstract stacks in ANF to CPS continuation closures • abstract stack bottom in ANF to CPS initial continuation • ANF closures to CPS function closures • ANF constants to CPS constants Theorem 6.1. Let p be given. Let C, F ♯ , E ♯ = lfp F ♯ p and Q ♯ , R ♯ = lfp T ♯ C[p] . Then s ∈ C ⇐⇒ F k s [s] ∈ Q ♯ ∧ [x, s ′ ] ∈ F ♯ ([s] ≡ ) ⇐⇒ [fn x => F k s ′ [s ′ ]] ∈ R ♯ (k s ) ∧ stop ∈ F ♯ ([s] ≡ ) ⇐⇒ stop ∈ R ♯ (k s ) ∧ [fn x => s] ∈ E ♯ (y) ⇐⇒ [fn x, k s => F ks [s]] ∈ R ♯ (y) ∧ n ∈ E ♯ (y) ⇐⇒ n ∈ R ♯ (y)
For the purpose of the equivalence we equate the special variables x r and v r both naming the result of the computations. We prove the theorem by combining an implication in each direction with the identity from Lemma 6.1. We formulate both implications as relations and prove that both relations are preserved by the transfer functions.

ANF-CPS equivalence

We formally define a relation R ANF CPS that relates ANF analysis triples to CPS analysis pairs. i

ANF trace: C i , F ♯ i , E ♯ i CPS trace: Q ♯ i , R ♯ i 0 {let f=fn x => x in let a1=f 1 in let a2=f 2 in a2}   [xr]≡ → {stop}, [let f=fn x => x in let a1=f 1 in let a2=f 2 in a2]≡ → {[xr, xr]}   λ_. ∅ (fn f => f 1 (fn a1 => f 2 (fn a2 => kp a2))) (fn x, kx => kx x)   kr → {stop}, kp → {[fn vr => kr vr]}   1 C0 ∪ {let a1=f 1 in let a2=f 2 in a2} F ♯ 0 E ♯ 0 ∪ f → {[fn x => x]} Q ♯ 0 ∪ f 1 (fn a1 => f 2 (fn a2 => kp a2)) R ♯ 0 ∪ f → {[fn x, kx => kx x]} 2 C1 ∪ {x} F ♯ 1 ∪ [x]≡ → {[a1, let a2=f 2 in a2]} E ♯ 1 ∪ x → {1} Q ♯ 1 ∪ {kx x} R ♯ 1 ∪   kx → {[fn a1 => f 2 (fn a2 => kp a2)]} x → {1}   3 C2 ∪ {let a2=f 2 in a2} F ♯ 2 E ♯ 2 ∪ a1 → {1} Q ♯ 2 ∪ f 2 (fn a2 => kp a2) R ♯ 2 ∪ a1 → {1} 4 C3 F ♯ 3 ∪ [x]≡ → {[a1, let a2=f 2 in a2], [a2, a2]} E ♯ 3 ∪ x → {1, 2} Q ♯ 3 R ♯ 3 ∪   kx → {[fn a1 => f 2 (fn a2 => kp a2)], [fn a2 => kp a2]} x → {1, 2}   5 C4 ∪ {a2} F ♯ 4 E ♯ 4 ∪   a1 → {1, 2} a2 → {1, 2}   Q ♯ 4 ∪ kp a2 R ♯ 4 ∪   a1 → {1, 2} a2 → {1, 2}   6 C5 ∪ {xr} F ♯ 5 E ♯ 5 ∪ xr → {1, 2} Q ♯ 5 ∪ {kr vr} R ♯ 5 ∪ vr → {1, 2} 7
C6 F ♯ 6 E ♯ 6 Q ♯ 6 R ♯ 6
Table 1: Analysis traces of let f=fn x => x in let a 1 =f 1 in let a 2 =f 2 in a 2 and its CPS transformed counterpart

Definition 6.2. C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ iff s ∈ C =⇒ F k s [s] ∈ Q ♯ ∧ [x, s ′ ] ∈ F ♯ ([s] ≡ ) =⇒ [fn x => F k s ′ [s ′ ]] ∈ R ♯ (k s ) ∧ stop ∈ F ♯ ([s] ≡ ) =⇒ stop ∈ R ♯ (k s ) ∧ [fn x => s] ∈ E ♯ (y) =⇒ [fn x, k s => F ks [s]] ∈ R ♯ (y) ∧ n ∈ E ♯ (y) =⇒ n ∈ R ♯ (y)
First we need a small lemma relating the ANF helper function to one of the CPS helper functions. Lemma 6.2.

[fn x => s] ∈ µ ♯ (t, E ♯ ) ∧ C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ =⇒ [fn x, k s => F ks [s]] ∈ µ ♯ t (V[t], R ♯ )
and

n ∈ µ ♯ (t, E ♯ ) ∧ C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ =⇒ n ∈ µ ♯ t (V[t], R ♯ ) Proof.
The proof for each part follows by a simple case analysis on t.

The relation is preserved by the transfer functions. Theorem 6.2.

C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ =⇒ F ♯ p ( C, F ♯ , E ♯ ) R ANF CPS T ♯ C[p] ( Q ♯ , R ♯ ) Proof.
First we name the individual triples of the union in the function body of F ♯ . We name the first triple of results as initial:

C I , F ♯ I , E ♯ I = {p}, [[p] ≡ → {[x r , x r ]}, [x r ] ≡ → {stop}],
λ_. ∅ The results of the second, third, fourth, and fifth joined triples corresponding to return, binding, tail call, and non-tail call are named

C ret , F ♯ ret , E ♯ ret , C bind , F ♯ bind , E ♯ bind , C tc , F ♯ tc , E ♯ tc and C ntc , F ♯ ntc , E ♯ ntc , respectively.
Similarly we name the first result pair in the function body of the CPS analysis as initial:

Q ♯ I , R ♯ I = {e}, [k r → {stop}, k → {[fn v r => k r v r ]}] .
The results of the second and third joined pair corresponding to call and return are named

Q ♯ call , R ♯ call and Q ♯ ret , R ♯ ret ,
respectively. The proof proceeds by verifying five relations:

C I , F ♯ I , E ♯ I R ANF CPS Q ♯ I , R ♯ I (1) C ret , F ♯ ret , E ♯ ret R ANF CPS Q ♯ ret , R ♯ ret (2) C bind , F ♯ bind , E ♯ bind R ANF CPS Q ♯ ret , R ♯ ret (3) C tc , F ♯ tc , E ♯ tc R ANF CPS Q ♯ call , R ♯ call (4) C ntc , F ♯ ntc , E ♯ ntc R ANF CPS Q ♯ call , R ♯ call (5)
We now prove the return case relation (2

): C ret , F ♯ ret , E ♯ ret R ANF CPS Q ♯ ret , R ♯ ret .
The remaining cases follow by similar reasoning.

(2a) Assume s ∈ C ret . Hence there exists x, s ′ , t such that s = s ′ , {t} ⊆ C, and

{[x, s ′ ]} ⊆ F ♯ ([t] ≡ ). From the C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ assumption we have F k t [t] ∈ Q ♯ and [fn x => F k s ′ [s ′ ]] ∈ R ♯ (k t ). Hence k t V[t] ∈ Q ♯ and [fn x => F k s ′ [s ′ ]] ∈ µ ♯ c (k t , R ♯ ). As a consequence F k s ′ [s ′ ] ∈ Q ♯ ret . (2b) Assume [x, s ′ ] ∈ F ♯ ret ([s] ≡ ). Hence there exists x ′′ , s ′′ , t such that {t} ⊆ C, {[x ′′ , s ′′ ]} ⊆ F ♯ ([t] ≡ ), and [x, s ′ ] ∈ F ♯ ret ([s] ≡ ) = F ♯ ([s] ≡ ). From the C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ assumption we have F k t [t] ∈ Q ♯ , [fn x ′′ => F k s ′′ [s ′′ ]] ∈ R ♯ (k t ), and [fn x => F k s ′ [s ′ ]] ∈ R ♯ (k s ). Hence k t V[t] ∈ Q ♯ , [fn x ′′ => F k s ′′ [s ′′ ]] ∈ µ ♯ c (k t , R ♯ ), and [fn x => F k s ′ [s ′ ]] ∈ R ♯ (k s ). Since R ♯ ⊆ R ♯ ret we have [fn x => F k s ′ [s ′ ]] ∈ R ♯ ret (k s ). (2c) Assume stop ∈ F ♯ ret ([s] ≡ ). Hence there exists x ′′ , s ′′ , t such that {t} ⊆ C, {[x ′′ , s ′′ ]} ⊆ F ♯ ([t] ≡ ), and stop ∈ F ♯ ret ([s] ≡ ) = F ♯ ([s] ≡ ). From the C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ assumption we have F k t [t] ∈ Q ♯ , [fn x ′′ => F k s ′′ [s ′′ ]] ∈ R ♯ (k t ), and stop ∈ R ♯ (k s ). Hence k t V[t] ∈ Q ♯ , [fn x ′′ => F k s ′′ [s ′′ ]] ∈ µ ♯ c (k t , R ♯ ), and stop ∈ R ♯ (k s ). Since R ♯ ⊆ R ♯ ret we have stop ∈ R ♯ ret (k s ). (2d) Assume [fn x => s] ∈ E ♯ ret (y). Hence there exists x ′ , s ′ , t such that {t} ⊆ C, {[x ′ , s ′ ]} ⊆ F ♯ ([t] ≡ ), and [fn x => s] ∈ (E ♯ ∪ [x ′ → µ ♯ (t, E ♯ )])(y). From the C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ assumption we have F k t [t] ∈ Q ♯ and [fn x ′ => F k s ′ [s ′ ]] ∈ R ♯ (k t ). Hence k t V[t] ∈ Q ♯ and [fn x ′ => F k s ′ [s ′ ]] ∈ µ ♯ c (k t , R ♯ ).
There are now two subcases:

1. [fn x => s] ∈ E ♯ (y). Hence [fn x, k s => F k s [s]] ∈ R ♯ (y). Since R ♯ ⊆ R ♯ ret we have [fn x, k s => F k s [s]] ∈ R ♯ ret (y). 2. [fn x => s] ∈ [x ′ → µ ♯ (t, E ♯ )](y). If y = x ′ our assumption reads [fn x => s] ∈ ∅. Hence [fn x, k s => F k s [s]] ∈ R ♯ ret (y) is trivially true. If y = x ′ our assumption reads [fn x => s] ∈ µ ♯ (t, E ♯ ). By Lemma 6.2 it now follows that [fn x, k s => F k s [s]] ∈ µ ♯ t (V[t], R ♯ ). As a conse- quence [fn x, k s => F k s [s]] ∈ R ♯ ret (y). (2e) Assume n ∈ E ♯ ret (y). Hence there exists x ′ , s ′ , t such that {t} ⊆ C, {[x ′ , s ′ ]} ⊆ F ♯ ([t] ≡ ), and n ∈ (E ♯ ∪ [x ′ → µ ♯ (t, E ♯ )])(y). From the C, F ♯ , E ♯ R ANF CPS Q ♯ , R ♯ assumption we again have F kt [t] ∈ Q ♯ and [fn x ′ => F k s ′ [s ′ ]] ∈ R ♯ (k t ). Hence k t V[t] ∈ Q ♯ and [fn x ′ => F k s ′ [s ′ ]] ∈ µ ♯ c (k t , R ♯ ).
There are now two subcases:

1. n ∈ E ♯ (y). Hence n ∈ R ♯ (y). Since R ♯ ⊆ R ♯ ret we have n ∈ R ♯ ret (y). 2. n ∈ [x ′ → µ ♯ (t, E ♯ )](y). If y = x ′ our assumption reads n ∈ ∅. Hence n ∈ R ♯ ret (y) is trivially true. If y = x ′ our assumption reads n ∈ µ ♯ (t, E ♯ ). By Lemma 6.2 it now follows that n ∈ µ ♯ t (V[t], R ♯ ). As a consequence n ∈ R ♯ ret (y).
Realizing that the union of related triples and pairs are related we obtain the desired result.

After realizing that the bottom elements are related by the above relation, it follows by fixed point induction that their least fixed points (and hence the analyses) are related.

Corollary 6.1. lfp F ♯ p R ANF CPS lfp T ♯ C[p]

CPS-ANF equivalence

Again we formally define a relation now relating CPS analysis pairs to ANF analysis triples.

Definition 6.3. Q ♯ , R ♯ R CPS ANF C, F ♯ , E ♯ iff e ∈ Q ♯ =⇒ U[e] ∈ C ∧ [fn x => e] ∈ R ♯ (k s ) =⇒ [x, U[e]] ∈ F ♯ ([s] ≡ ) ∧ stop ∈ R ♯ (k s ) =⇒ stop ∈ F ♯ ([s] ≡ ) ∧ [fn x, k s => e] ∈ R ♯ (y) =⇒ [fn x => U[e]] ∈ E ♯ (y) ∧ n ∈ R ♯ (y) =⇒ n ∈ E ♯ (y)
We again need a helper lemma relating the helper functions.

Lemma 6.3.

[fn x, k s => e] ∈ µ ♯ t (t, R ♯ ) ∧ Q ♯ , R ♯ R CPS ANF C, F ♯ , E ♯ =⇒ [fn x => U[e]] ∈ µ ♯ (P[t], E ♯ ) and n ∈ µ ♯ t (t, R ♯ ) ∧ Q ♯ , R ♯ R CPS ANF C, F ♯ , E ♯ =⇒ n ∈ µ ♯ (P[t], E ♯ )
Proof. The proof for each part follows by a simple case analysis on t.

This relation is also preserved by the transfer functions.

Theorem 6.3.

Q ♯ , R ♯ R CPS ANF C, F ♯ , E ♯ =⇒ T ♯ C[p] ( Q ♯ , R ♯ ) R CPS ANF F ♯ p ( C, F ♯ , E ♯ )
Proof. The proof follows a similar structure to the above proof.

The bottom elements are related by the relation and it again follows by fixed point induction that their least fixed points (and hence the analyses) are related.

Corollary 6.2. lfp T ♯ C[p] R CPS ANF lfp F ♯ p 7. Extracting a constraint-based CFA
The resulting analysis may appear complex at first glance. However, we can express the analysis in the popular constraint formulation, extracted from the obtained definition. The formulation shown below is in terms of program-specific conditional constraints.

Constraints have a (possibly empty) list of preconditions and a conclusion [START_REF] Palsberg | Safety analysis versus type inference[END_REF][START_REF] Gasser | Systematic realisation of control flow analyses for CML[END_REF]:

{u 1 } ⊆ rhs 1 ∧ . . . ∧ {u n } ⊆ rhs n ⇒ lhs ⊆ rhs
The constraints operate on the same three domains as the above analysis. Lefthand sides lhs can be of the form {u}, F ♯ ([s] ≡ ), or E ♯ (x), right-hand sides rhs can be of the form C, F ♯ ([s] ≡ ), or E ♯ (x), and singleton elements u can be of the form s, n, [fn x => s], or [x, s]. From Fig. 8 we can directly extract the following constraints that must be satisfied by a valid result of the CFA. More precisely, each set expression in the set union defining the control flow analysis equation gives rise to a set of constraints. For example, one of the expressions in the equation reads:

⊗ {t}⊆C {[x, s ′ ]}⊆F ♯ ([t]≡) {s ′ }, F ♯ , E ♯ ∪ [x → µ ♯ (t, E ♯ )]
Correspondingly, for each return expression t and non-tail call let x=t 0 t 1 in s ′ in p, we generate the constraints:

{t} ⊆ C ∧ {[x, s ′ ]} ⊆ F ♯ ([t] ≡ ) ⇒ {s ′ } ⊆ C ∧ µ sym (t, E ♯ ) ⊆ E ♯ (x)
The other parts of the definition of F ♯ similarly induce a constraint generation scheme, as follows: Theorem 7.1. A solution to the CFA constraints of program p is a safe approximation of the least fixpoint of the analysis function F ♯ induced by p. Furthermore, the least solution to the CFA constraints is equal to the least fixpoint of F ♯ .

Proof. The first part of the theorem is proved by showing that a solution to the CFA constraints C, F , E is a post-fixpoint of F ♯ , i.e., that it satisfies F ♯ ( C, F , E ) ⊆ ⊗ C, F , E and then appeal to the Knaster-Tarski fixpoint theorem that the least fixpoint of a monotone operator F ♯ is the greatest lower bound of the set of post-fixpoints of F ♯ . This reduces to showing that for each of the expressions defining F ♯ in Fig. 8 we have that its value is already included in the solution C, F , E . For example, for the expression

⊗ {t}⊆C {[x, s ′ ]}⊆F ♯ ([t]≡) {s ′ }, F ♯ , E ♯ ∪ [x → µ ♯ (t, E ♯ )]
we must have, for all t satisfying {t} ⊆ C and s

′ satisfying {[x, s ′ ]} ⊆ F ♯ ([t] ≡ ), that {s ′ } ⊆ C and E ♯ ∪ [x → µ ♯ (t, E ♯ )] ⊆ E ♯ .
The latter inequality reduces to µ sym (t, E ♯ ) ⊆ E ♯ (x). and we obtain exactly the constraints for return expressions. The other cases follow by similar reasoning.

For the equality of the least solution and the least fixpoint, it then suffices to prove that the fixpoint is a solution to the CFA constraints. The argumentation is again based on unfolding the definition of F ♯ and using reasoning similar to above.

Implemented naively, a single constraint may take O(n) space alone. However by using a pointer or the implicit label of each sub-expression instead of the sub-expression itself, a single constraint takes only constant space. By linearly determining a representative for each sub-expression, by generating O(n 2 ) constraints, linear post-processing, and iteratively solving them using a well-known algorithm [START_REF] Palsberg | Safety analysis versus type inference[END_REF][START_REF] Gasser | Systematic realisation of control flow analyses for CML[END_REF][START_REF] Nielson | Principles of Program Analysis[END_REF], we can compute the analysis in worst-case O(n 3 ) time.

The extracted constraints bear similarities to existing constraint-based analyses in the literature. Consider, e.g., calls t 0 t 1 , which usually gives rise to two conditional constraints [START_REF] Palsberg | Closure analysis in constraint form[END_REF][START_REF] Nielson | Principles of Program Analysis[END_REF]

: (1) {[fn x => s ′ ]} ⊆ C(t 0 ) ⇒ C(t 1 ) ⊆ E(x) and (2) {[fn x => s ′ ]} ⊆ C(t 0 ) ⇒ C(s ′ ) ⊆ C(t 0 t 1 )
. The first constraint resembles our third constraint for tail calls. The second "return constraint" differs in that it has a inside-out (or caller-restore) nature, i.e., propagation of return-flow from the function body is handled at the call-site. The extracted reachability constraints are similar to Gasser et al. [START_REF] Gasser | Systematic realisation of control flow analyses for CML[END_REF] (modulo an isomorphic encoding ℘(C ) ≃ C → ℘({on}) of powersets).

Related work

We separate the discussion of related analyses in two: direct-style analyses and analyses based on CPS.

Direct-style CFA has a long research history. Jones [START_REF] Jones | Flow analysis of lambda expressions (preliminary version)[END_REF] initially developed methods for approximating the control flow of lambda terms. Since then Sestoft [START_REF] Sestoft | Replacing function parameters by global variables[END_REF] conceived the related closure analysis. Palsberg [START_REF] Palsberg | Closure analysis in constraint form[END_REF] simplified the analysis and formulated an equivalent constraint-based analysis. At the same time Heintze [START_REF] Heintze | Set-based program analysis of ML programs[END_REF] developed a related set-based analysis formulated in terms of set constraints. For a detailed account of related work, we refer to a recent survey of the area [START_REF] Midtgaard | Control-flow analysis of functional programs[END_REF]. It is worth emphasizing that all of the above analyses focus on calls, in that they approximate the source lambdas being called at each call-site. As such they do not directly determine return flow for programs in direct style. Continuation-passing style CFA was pioneered by Shivers [START_REF] Shivers | Control-flow analysis in Scheme[END_REF] who formulated control-flow analysis for Scheme. Since then a number of analyses have been formulated for CPS [START_REF] Ayers | Abstract Analysis and Optimization of Scheme[END_REF][START_REF] Ashley | A practical and flexible flow analysis for higher-order languages[END_REF][START_REF] Might | Environmental analysis via ∆CFA[END_REF]. In CPS all calls are tail calls, and even returns are encoded as calls to the current continuation. By determining "call flow" and hence the receiver functions of such continuation calls, a CPS-based CFA thereby determines return flow without additional effort.

A long-standing question in flow analysis is to characterize the impact of CPS transformation on the precision of program analysis [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF][START_REF] Palsberg | CPS transformation of flow information[END_REF][START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF]. The study of this question originated in binding-time analysis, for which the transformation is known to have a positive effect [START_REF] Consel | For a better support of static data flow[END_REF][START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF]. The following example is due to Damian and Danvy [START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF]. Consider a let binding let x=s in s ′ in which s is dynamic (unknown) and s ′ is static (known at compile time). Since evaluating s may have an effect, e.g, non-termination, the result of the entire expression has to be qualified as dynamic. Now consider its CPS counterpart: fn k => e (fn x => e ′ k) in which e and e ′ represent the CPS transformation of s and s ′ , respectively. In CPS the result of evaluating e ′ (which is sent to k) may now be qualified as static independent of e.

As to the impact of CPS transformation on CFA we separate the previous work on the subject in two:

1. results relating an analysis specialized to the source language to an analysis specialized to the target language (CPS), and 2. results relating the analysis of a program to the same analysis of the CPS transformed program.

Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF] designed and compared specialized analyses and hence falls into the first category as does the present paper. Damian and Danvy [START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF] related the analysis of a program and its CPS counterpart for a standard flowlogic CFA (as well as for two binding-time analyses), and Palsberg and Wand [START_REF] Palsberg | CPS transformation of flow information[END_REF] related the analysis of a program and its CPS counterpart for a standard conditional constraint CFA. Hence the latter two fall into the second category. We paraphrase the relevant theorems of Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF], of Damian and Danvy [START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF], of Palsberg and Wand [START_REF] Palsberg | CPS transformation of flow information[END_REF], and of the present paper in order to underline the difference between the contributions (C refers to non-trivial, 0-CFA-like analyses defined in the cited papers, p ranges over direct-style programs, cps denotes CPS transformation, and ∼ denotes analysis equivalence).

Our formulations should not be read as a formal system, but only as a means for elucidating the difference between the contributions. Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF]: Our work relates to all of the above contributions. The disciplined derivation of specialized CPS and direct-style analyses results in comparable analyses, contrary to Sabry and Felleisen [START_REF] Sabry | Is continuation-passing useful for data flow analysis?[END_REF]. Furthermore our equivalence proof extends the results of Damian and Danvy [START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF] and Palsberg and Wand [START_REF] Palsberg | CPS transformation of flow information[END_REF] in that we relate both call flow, return flow, and reachability, contrary to their relating only the call flow of standard CFAs. In addition, the systematic abstract interpretationbased approach suggests a strategy for obtaining similar equivalence results for other CFAs derived in this fashion.

Formulating CFA in the traditional abstract interpretation framework was stated as an open problem by [START_REF] Nielson | Infinitary control flow analysis: a collecting semantics for closure analysis[END_REF]. It has been a recurring theme in the work of the present authors. In an earlier paper Spoto and Jensen [START_REF] Spoto | Class analyses as abstract interpretations of trace semantics[END_REF] investigated class analysis of object-oriented programs as a Galois connection-based abstraction of a trace semantics. In a recent article [START_REF] Midtgaard | A calculational approach to control-flow analysis by abstract interpretation[END_REF], the authors systematically derived a CPS-based CFA from the collecting semantics of a stack-less machine. While investigating how to derive a corresponding direct-style analysis we discovered the mismatch between the computed return information.

As tail calls are identified syntactically, the additional information could also have been obtained by a subsequent analysis after a traditional direct-style CFA. However we view the need for such a subsequent analysis as a strong indication of a mismatch between the two analysis formulations. Debray and Proebsting [START_REF] Debray | Interprocedural control flow analysis of first-order programs with tail-call optimization[END_REF] have investigated such a "return analysis" for a first-order language with tail-call optimization. The present paper builds a semantics-based CFA that determines such information, and for a higher-order language.

The systematic design of constraint-based analyses is a goal shared with the flow logic framework of Nielson and Nielson [START_REF] Nielson | Flow logic: a multi-paradigmatic approach to static analysis[END_REF]. In flow logic an analysis specification can be systematically transformed into a constraint-based analysis. The present paper instead extracts a constraint-based analysis from an analysis developed in the original abstract interpretation framework.

Conclusions

We have presented a control-flow analysis determining interprocedural controlflow of both calls and returns for a direct-style language. Existing CFAs have focused on analysing which functions are called at a given call site. In contrast, the systematic derivation of our CFA has lead to an analysis that provides extra information about where a function returns to at no additional cost. In the presence of tail-call optimization, such information enables the creation of more precise call graphs.

The analysis was developed systematically using Galois connection-based abstract interpretation of a standard operational semantics for that language: the C a EK abstract machine of Flanagan et al. In addition to being more principled, such a formulation of the analysis is pedagogically pleasing since monomorphism of the analysis is made explicit through two Galois connections: one literally merges all bindings to the same variable and one merges all calling contexts of the same function.

The analysis has been shown to provide a result equivalent to what can be obtained by first CPS transforming the program and then running a controlflow analysis derived from a CPS-based operational semantics. This extends previous results obtained by Damian and Danvy, and Palsberg and Wand. The close correspondence between the way that the analyses operate (as illustrated by the analysis trace in Table 1) leads us to conjecture that such equivalence results can be obtained for other CFAs derived using abstract interpretation.

The functional, derived by abstract interpretation, that defines the analysis may appear complex at first glance. As a final result, we have shown how to extract from the analysis an equivalent constraint-based formulation expressed in terms of the more familiar conditional constraints. Nevertheless, we stress that the derived functional can be used directly to implement the analysis. We have developed a prototype implementation of the resulting analysis in OCaml. 2The analysis has been developed for a minimalistic functional language in order to be able to focus on the abstraction of the control structure induced by function calls and returns. An obvious extension is to enrich the language with numerical operators and study how our Galois connections interact with abstractions such as the interval or polyhedral abstraction of numerical entities.

The calculations involved in the derivation of a CFA are lengthy and would benefit from some form of machine support. Certified abstract interpretation [START_REF] Pichardie | Interprétation abstraite en logique intuitioniste: extraction d'analyseurs Java certifiés[END_REF][START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF] has so far focused on proving the soundness of the analysis inside a proof assistant by using the concretization (γ) component of the Galois connection to prove the correctness of an already defined analysis. Further work should investigate whether proof assistants such as Coq are suitable for conducting the kind of reasoning developed in this paper in a machine-checkable way.

  (a) α and γ are monotone. (b) α • γ is reductive (for all a ∈ A : α • γ(a) ≤ a),(c) γ • α is extensive (for all c ∈ C : c ⊑ γ • α(c)).Galois connections are typeset asC; ⊑ ---→ ← --α γA; ≤ . We omit the orderings when they are clear from the context. For a Galois connection between two complete lattices C;⊑, ⊥ c , ⊤ c , ⊔, ⊓ and A; ≤, ⊥ a , ⊤ a , ∨, ∧ , α is a complete join-morphism (CJM) (for all S c ⊆ C : α(⊔S c ) = ∨α(S c ) = ∨{α(c) | c ∈ S c }) and γ is a complete meet morphism (for all S a ⊆ A : γ(∧S a ) = ⊓γ(S a ) = ⊓{γ(a) | a ∈ S a }). The composition of two Galois connections C; ⊑ ---→ ←---α1 γ1 B; ⊆ and B; ⊆ ---→ ←---α2 γ2 A; ≤ is itself a Galois connection C; ⊑ ------→ ← ------α2•α1 γ1•γ2A; ≤ . Galois connections in which α is surjective (or equivalently γ is injective) are typeset as: C; ⊑ ---→ -→ ← ---α γ A; ≤ . Galois connections in which γ is surjective (or equivalently α is injective) are typeset as: C; ⊑ --. When both α and γ are surjective, the two domains are isomorphic.

  ∋ w ::= n | [fn x => s, e] Env ∋ e ::= • | e[x → w] K ∋ k ::= stop | [x, s, e] :: k (a) Values, environments, and stacks µ : T × Env ⇀ Val µ(n, e) = n µ(x, e) = e(x) µ(fn x => s, e) = [fn x => s, e]

  (b) Helper function t, e, [x, s ′ , e ′ ] :: k

Figure 2 :

 2 Figure 2: The C a EK abstract machine

Figure 3 :

 3 Figure 3: The corresponding call graphs

  r , •] :: stop } First we formulate in Fig. 4(a) an equivalent helper function µ c extended to work on sets of environments.

Lemma 4 . 1 .

 41 ∀t, e : {µ(t, e)} = µ c (t, {e})

Figure 5 :

 5 Figure 5: Overview of abstraction

Figure 6 :

 6 Figure 6: Abstract transition function

•

  [x → w]: •[x → w] ≻ w of which the empty environment is a constituent: w ≻ •. We write ≻ * for the reflexive, transitive closure of the constituent relation. For example, •[x → w] ≻ * •.

Definition 4 . 2 (

 42 Relation on expression-stack pairs). Let the binary relation ⋗ on expression-stack pairs be defined by s, [x, s ′ , e] :: k ⋗ s ′ , k . Informally, expression-stack pairs are related iff (a) the stack component of the second pair is the tail of the first pair's stack component, and (b) the expression component of the second, resides on the top stack frame of the stack component of the first pair.

Figure 7 :

 7 Figure 7: The second abstract transition function

Lemma 4 . 6 .

 46 Control stack and saved environments Let

Figure 8 :

 8 Figure 8: The resulting analysis function

CProgFigure 9 :

 9 Figure 9: BNF of CPS language

Fig. 11

 11 Fig. 11 defines a CFA for CPS programs. It is defined as the least fixed point of a program specific transfer function T ♯ p . The definition relies on two helper functions µ ♯ t and µ ♯ c for trivial and continuation expressions, respectively. The analysis computes a pair consisting of (a) a set of serious expressions (the reachable expressions) and (b) an abstract environment. Abstract environments map variables to abstract values. Abstract values can be either constants, the initial continuation stop, function closures [fn x, k => e], or continuation closures [fn v => e].The definition relies on two special variables k r and v r , the first of which names the initial continuation and the second of which names the result of the program. To ensure the most precise analysis result, variables in the source program can be renamed to be distinct as is traditional in control-flow analysis[START_REF] Nielson | Principles of Program Analysis[END_REF].

exists analyses C 1 ,

 1 C 2 : exists p, C 1 (p) ≁ C 2 (cps(p))Damian and Danvy[START_REF] Damian | Syntactic accidents in program analysis: On the impact of the CPS transformation[END_REF], Palsberg and Wand[START_REF] Palsberg | CPS transformation of flow information[END_REF]:exists analysis C : for all p, C(p) ∼ C(cps(p))Present paper, Theorem 6.1:exists analyses C 1 , C 2 : for all p, C 1 (p) ∼ C 2 (cps(p))

  µ(t 0 , e) and w = µ(t 1 , e)let x=t 0 t 1 in s, e, k -→ s ′ , e ′ [y → w], [x,s, e] :: k if [fn y => s ′ , e ′ ] = µ(t 0 , e) and w = µ(t 1 , e)

	(c) Machine transitions

  s} which can be specialized into the four set expressions defining F c by case analysis of the transition relation -→. For example, if the state is of the form t, e, [x, s ′ , e ′ ]::k ′ then the resulting state after a -→ transition will be of the form s ′ , e ′ [x → µ(t, e)], k ′ . This state belongs to the set expression

	{ s ′ , e ′ [x → w], k ′ }
	w∈{µ(t,e)}
	which by Lemma 4.1 is equivalent to
	w∈µc (t,{e})

available at http://www.cs.au.dk/~jmi/ANF-CFA/

Acknowledgement:. The authors thank Matthew Fluet, Amr Sabry, Matthias Felleisen, Mitchell Wand, Daniel Damian, Olivier Danvy, Casey Klein, and Robby Findler for comments on earlier versions of this paper. Part of this work was done with the support of the Carlsberg Foundation and an INRIA post-doc grant.

result is a pointwise abstraction of a set of environments, that does not explicitly model variable lookup failure:

By considering only closed programs, we statically ensure against failure of variable-lookup, hence disregarding ⊥ loses no information.

Given the abstraction of environments, we can calculate the corresponding abstract versions of the helper function used in the semantics, by "pushing α's" under the function definition, and reading off a resulting abstract definition. The resulting helper function reads:

where we write Env ♯ as shorthand for Var → ℘(Val ♯ ). The calculation can be done without introducing any additional approximations and leads to a complete abstraction of the helper function µ ♯ . Lemma 4.7. Completeness of abstract helper function

Proof. By a simple case analysis on t and an unfolding of the remaining definitions.

We shall need a lemma relating the two helper function definitions on closed environments.

Proof. By a simple case analysis on t. The constant and variable cases are straightforward. For the lambda case t = fn x ′ => s ′ there are two subcases to consider: fn x ′ => s ′ = fn x => s in which case we reach a contradiction, and fn x ′ => s ′ = fn x => s which follows straightforwardly.

The above lemma is easily extended to capture nested environments in all values returned by the helper function:

Proof. By a simple case analysis on w. In case w is a closure we apply the above lemma and the closed environment assumption.

(abstract values)

• For each let-binding let x=t in s in p:

• For each tail call t 0 t 1 and function fn x => s ′ in p:

• For each non-tail call let x=t 0 t 1 in s and function fn y => s ′ in p:

where we partially evaluate the helper function µ sym , i.e., interpret the helper function symbolically at constraint-generation time, to generate a lookup for variables, and a singleton for constants and lambda expressions. The definition of the symbolic helper function otherwise coincides with the abstract helper function µ ♯ :

We may generate constraints {[fn x => s]} ⊆ {[fn y => s ′ ]} of a form not covered by the above grammar. We therefore first pre-process the constraints in linear time, The resulting constraint system is formally equivalent to the control flow analysis in the sense that all solutions yield correct control flow information and that the best (smallest) solution of the constraints is as precise as the information computed by the analysis. More formally: