figure 5. abstraction map, a : ÂCESK*t → ÂCESKt.

 

α(e, ρ, σ, a, t) = (e, α(ρ), α(σ), α(a), α(t)) α(ρ) = λx.α(ρ(x))

α(σ) = λa. ˆ

;

α(a)=â

{α(σ(a))}

α((λx.e), ρ) = ((λx.e), α(ρ))

α(mt) = mt α(ar(e, ρ, a)) = ar(e, α(ρ), α(a)) α(fn(v, ρ, a)) = fn(v, α(ρ), α(a))

[states] [environments] [stores] [closures] [continuations]

calculation. For the remaining (nondeterministic) cases, we must show an abstract state exists such that the simulation is preserved. By examining the rules for these cases, we see that all three hinge on the abstract store in ς ˆ soundly approximating the concrete store in ς, which follows from the assumption that a (ς )  ς ˆ.

 

Theorem 2 (Decidability) Membership of ς ˆ in CESK*t (e) is decidable.

Proof. The state space of the machine is non-recur-sive with finite sets at the leaves on the assumption that addresses are finite. Hence reachability is decidable since the abstract state space is finite.

3. aBstRaCt state anD ContRoL

We have shown that store-allocated continuations make abstract interpretation of the CESK* machine straightforward. In this section, we want to show that the tight correspondence between concrete and abstract persists after the addition of language features such as conditionals, side effects, and first-class continuations. We tackle each feature, and present the additional machinery required to handle each one. In most cases, the path from a canonical concrete machine to pointer-refined abstraction of the machine is so simple we only show the abstracted system. In doing so, we are arguing that this abstract machine-oriented approach to abstract interpretation represents a flexible and viable framework for building program analyses.

To handle conditionals, we extend the language with a new syntactic form, (if e e e), and introduce a base value #f, representing false. Conditional expressions induce a new continuation form: if (e0¢, e1¢, r, a), which represents the evaluation context E[(if [ ] e0 e1)] where r closes e0¢ to represent e0, r closes e1¢, to represent e1, and a is the address of the representation of E.

Side effects are fully amenable to our approach; we introduce Scheme’s set! for mutating variables using the (set! x e) syntax. The set! form evaluates its subexpression e and assigns the value to the variable x. Although set! expressions are evaluated for effect, we follow Felleisen et al. and specify set! expressions evaluate to the value of x before it was mutated (p. 166 of Felleisen et al. 7). The evaluation

figure 6. abstract extended CesK* machine.

ˆ ˆ ; ; ς ;−→CESK∗ ς ;, where κ ∈ ˆ σ (a), b = alloc (ˆ ς , κ ), u = tick (ˆ ς , κ ) t ;

;c, ρ, σ, a, t;
;v, ρ,ˆ σ, a, t;
;(ife0e1e2),ρ,σ,a,t; ˆ
ˆ
;#f, ρ,ˆ σ, a, t;
if κ = if(e0, e1, ρ;, c)
;v, ρ,ˆ σ, a, t;
if κ = if(e0, e1, ρ;, c),
and v;=#f
;(set x e), ρ, ˆ σ , a, t;
;v, ρ,ˆ σ, a, t;
if κ = set(a;, c)
;(λx.e), ρ, ˆ σ , a, t;
if κ = fn(callcc, ρ;, c)

if κ = fn(callcc, ρ;, a; )

if κ = fn(c, ρ;, a;)

ˆ ;e0, ρ, σ ; [b ;→ if(e1, e2, ρ, a)], b, u; ;e1, ρ;, σ , c, u; ;e0, ρ;, ˆ σ , c, u; ;e, ρ, ˆ σ ; [b ;→ set(ρ(x), a)], b, u; ;v;, ρ, ˆ σ ; [a; ;→ v], c, u;

;v , ρ, ˆ σ , c, u;

context E[(set! x [ ])] is represented by set(a0, a1), where a0 is the address of x’s value and a1 is the address of the representation of E.

First-class control is introduced by adding a new base value callcc which reifies the continuation as a new kind of applicable value. Denoted values are extended to include representations of continuations. Since continuations are store-allocated, we choose to represent them by address. When an address is applied, it represents the application of a continuation (reified via callcc) to a value. The continuation at that point is discarded and the applied address is installed as the continuation.

The resulting grammar is

e ∈ Exp = . . . | (if e e e) | (set! x e)
k ∈ Cont = . . . | if (e, e, r, a) | set(a, a)
v ∈ Val = . . . | #f | callcc | a.

We show only the abstract transitions (Figure 6), which result from store-allocating continuations, time-stamping, and abstracting the concrete transitions for conditionals, mutation, and control. The first three machine transitions deal with conditionals; here we follow the Scheme tradition of considering all non-false values as true. The fourth and fifth transitions deal with mutation.

The remaining three transitions deal with first-class control. In the first of these, callcc is being applied to a closure value v. The value v is then “called with the current continuation,” i.e., v is applied to a value that represents the continuation at this point. In the second, callcc is being applied to a continuation (address). When this value is applied to the reified continuation, it aborts the current computation, installs itself as the current continuation, and puts the reified continuation “in the hole.” Finally, in the third, a continuation is being