figure 5. abstraction map, a : ÂCESK*t → ÂCESKt.
α(e, ρ, σ, a, t) = (e, α(ρ), α(σ), α(a), α(t))
α(ρ) = λx.α(ρ(x))
α(σ) = λa. ˆ
α((λx.e), ρ) = ((λx.e), α(ρ))
α(mt) = mt
α(ar(e, ρ, a)) = ar(e, α(ρ), α(a))
α(fn(v, ρ, a)) = fn(v, α(ρ), α(a))
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;
;#f, ρ,ˆ σ, a, t;
if κ = if(e0, e1, ρ;, c)
;v, ρ,ˆ σ, a, t;
if κ = if(e0, e1, ρ;, c),
;(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