Lesson 8.6 — Functional IRs: CPS, ANF, and SSA as functional programming¶
Techniques: continuation-passing style (Steele, Appel; SML/NJ, Chicken Scheme), A-normal form (Flanagan–Sabry–Duba–Felleisen; GHC's CorePrep), and the correspondence SSA ≡ ANF (Kelsey 1995, Appel 1998) · Pebble uses: nothing directly; the lab's
anfform is ANF with join points, and the lab's SSA and ANF lowerings are the same algorithm in two notations · Lab: theanfform of labs/ch08-forms; drilltac-to-anf· Prerequisites: Lesson 8.4 · Time: 5–7 hours
Functional-language compilers took another route to an optimizable IR: make every intermediate result a named, immutable binding and every control transfer a call. The result looks nothing like a CFG, yet it is the same thing. Lesson 8.4 already hinted at it: a block with parameters is a function, and a branch with arguments is a tail call. This lesson makes the claim a theorem.
1. Problem and motivation¶
The problem. Represent a program in a lambda-calculus-like language in which (a) evaluation order is explicit, (b) every intermediate value is named, and (c) control transfer is explicit, so that ordinary β-reduction and inlining are valid optimizations and code generation is straightforward.
Continuation-passing style¶
In continuation-passing style (CPS) no function returns. Each function takes an extra argument, its continuation, and calls it with the result. Every call is then a tail call, and evaluation order, intermediate values and control are all explicit. Plotkin used the CPS transform to relate call-by-name and call-by-value [Plo75]. Steele's Rabbit compiler for Scheme compiled through CPS [Ste78]. Appel's SML/NJ used CPS as its main optimization IR, as described in Compiling with Continuations [App92]. Chicken Scheme still compiles every program to CPS and then to C (the real-world box in §7). A naive CPS transform introduces many administrative redexes, trivial λs that exist only because of the transform. Danvy and Filinski's one-pass transform avoids creating them [DF92].
A-normal form¶
Flanagan, Sabry, Duba and Felleisen observed that CPS compilers undo most of the transform again: after administrative reductions and a final "un-CPS" step, the result is a direct-style program in which every operand is a variable or constant and every intermediate result is let-bound. They called that form A-normal form (ANF) and showed that it can be produced directly, without the detour through continuations [FSDF93]. GHC's CorePrep pass converts Core to ANF before code generation (§7). Without join points, ANF must either duplicate the code after an if or use a closure. Kennedy [Ken07] and Maurer et al. [MDAJ17] showed that second-class local functions, called only in tail position, solve this. The lab's anf form has them (join, loop, jump).
SSA as functional programming¶
Kelsey showed that SSA programs and CPS programs in which continuations are never escaping correspond one to one: a block becomes a local continuation, and a phi becomes that continuation's parameter [Kel95]. Appel explained the same correspondence under the title "SSA is functional programming" [App98]: "one of the rules of SSA—a definition must dominate its uses—is exactly the lexical scoping rule of a functional language" when the local functions are nested according to the dominator tree. The practical consequence is that the two communities' optimizations transfer. MLton's SSA IR (blocks with arguments and Goto {dst, args}), GHC's join points and MLIR's block arguments are three points in this design space.
2. Definitions and algorithms¶
Continuation-passing style¶
Definition 8.6.1 (CPS terms)
Let atoms be \(a ::= x \mid k \in \mathbb{Z}_{64}\) and continuation variables \(\kappa\). A CPS term is
(First-order CPS for Tiny: primitives are pure, and the only calls are to continuations.) In a higher-order language, functions also take a continuation parameter, \(f(a_1, \dots, a_n, \kappa)\). A continuation is second-class if it is only called, never stored or passed as a value. Then it compiles to a jump.
Definition 8.6.2 (Administrative redex)
A meta-level CPS transform \(\mathcal{C}[\![e]\!]\,\kappa\) builds terms by applying translations of subterms to continuations. An administrative redex is a β-redex \((\lambda x.\,M)\,a\) in the output that the transform itself created (not one present in the source). The naive (Plotkin) transform translates \(e_1 \oplus e_2\) to \(\lambda \kappa.\,\mathcal{C}[\![e_1]\!]\,(\lambda a.\,\mathcal{C}[\![e_2]\!]\,(\lambda b.\,\mathsf{let}\ t = a \oplus b\ \mathsf{in}\ \kappa\,t))\) and an atom \(a\) to \(\lambda\kappa.\,\kappa\,a\). Each application of a translated subterm to a continuation is then an administrative redex.
Algorithm 8.6.3 (One-pass CPS transform, Danvy–Filinski style)
- Input: a Tiny expression \(e\) and a meta-level continuation \(K\) (a function from atoms to CPS terms).
- Output: a CPS term (Definition 8.6.1) with no administrative redexes.
- Precondition: fresh names for temporaries and continuation variables.
- Postcondition: the output evaluates to \(K\) applied to the value of \(e\) (Theorem 8.6.8).
- Invariant: \(K\) is called exactly once per control path, with an atom that holds the value of the current subexpression.
function C(e, K): # K: atom -> term, a function of the compiler
case e of
k or x: return K(e) # no λk.k x redex
op1 e1: return C(e1, λa. let t = op1(a) in K(t))
e1 ⊕ e2: return C(e1, λa. C(e2, λb. let t = ⊕(a, b) in K(t)))
e1 && e2: κ ← NewCont(); r ← NewVar()
return letcont κ(r) = K(r) in # K used once
C(e1, λa. letcont κt() = C(e2, λb. let t = ne(b, 0) in κ(t)) in
letcont κf() = κ(0) in
if a then κt() else κf())
A-normal form¶
Definition 8.6.4 (A-normal form with join points)
ANF terms are
with \(P ::= a \mid \mathit{op}\ a \mid \mathit{op}\ a, a\). A term is well scoped if
every atom \(x\) is bound by an enclosing let or join parameter, and every jump j occurs
in the in part of the definition of \(j\), or, for loop, also in its body, with the
right number of arguments. This is exactly the lab's anf format
(SPEC). By construction every operand is an atom,
and every jump is in tail position.
Algorithm 8.6.5 (A-normalization of Tiny with join points)
- Input: a Tiny program with source variables \(V\).
- Output: a well-scoped ANF term (Definition 8.6.4) of size linear in the program.
- Precondition: fresh names.
- Postcondition: the term returns the program's value (Theorem 8.6.9).
- Invariant:
S(ss, env, K)returns the term for the statements \(ss\) followed by \(K(\mathit{env}')\), where \(\mathit{env}'\) maps each \(v \in V\) to an atom in scope holding its value after \(ss\). Every meta-continuation \(K\) is used exactly once, except insideif, where the join point \(j\) is used instead.
function E(e, env, K): # expressions: exactly Algorithm 8.6.3,
k: K(k); x: K(env[x]) # with `join` for letcont and `jump` for calls
op1 e1: E(e1, env, λa. let t = op1 a in K(t))
e1 ⊕ e2: E(e1, env, λa. E(e2, env, λb. let t = ⊕ a, b in K(t)))
e1 && e2: E(e1, env, λa. join j(r) = K(r) in
if a then E(e2, env, λb. let t = ne b, 0 in jump j(t))
else jump j(0)) # || is dual
function S(ss, env, K):
if ss is empty: return K(env)
s, rest ← head, tail of ss
case s of
x = e: E(e, env, λa. S(rest, env[x ↦ a], K))
while c {b}: ps ← fresh parameters for V; envH ← (V ↦ ps)
return loop h(ps) =
E(c, envH, λa. if a then S(b, envH, λe'. jump h(e'[V]))
else S(rest, envH, K)) # rest used once
in jump h(env[V])
if c {b1} else {b0}:
ps ← fresh parameters; J ← λe'. jump j(e'[V])
return join j(ps) = S(rest, (V ↦ ps), K) in
E(c, env, λa. if a then S(b1, env, J) else S(b0, env, J))
function Translate(ss return e): S(ss, (V ↦ 0), λenv. E(e, env, λa. return a))
SSA as functional programming¶
Definition 8.6.6 (Dominator nesting)
Let \(F\) be a valid block-argument SSA function (Definition 8.4.4) with reachable blocks
\(N\), dominator tree \(\mathcal{D}\), and reverse postorder \(\mathrm{rpo}\) (Definition 8.2.7).
Block \(B\) is a loop header if some edge \(u \to B\) with \(\mathrm{rpo}(u) \ge \mathrm{rpo}(B)\)
exists. The Kelsey term \(K(B)\) of block \(B\) is the ANF term:
the instructions of \(B\) as lets; then, for every child \(C\) of \(B\) in \(\mathcal{D}\), in
decreasing \(\mathrm{rpo}\), the definition loop/join \(C(\mathit{params}(C)) = K(C)\)
in (loop iff \(C\) is a loop header); then \(B\)'s terminator, with br C(args) as
jump C(args), cbr a, C_1(…), C_2(…) as if a then jump … else jump …, and ret a
as return a. The translation of \(F\) is \(K(\mathit{entry})\).
Algorithm 8.6.7 (SSA to ANF, Kelsey 1995)
- Input: a valid block-argument SSA function \(F\) with a reducible CFG.
- Output: the Kelsey term \(K(\mathit{entry})\) (Definition 8.6.6).
- Precondition: dominator tree and RPO computed (Ch 15, Lesson 8.2).
- Postcondition: the term is well scoped and behaves like \(F\) (Theorem 8.6.12).
- Invariant: when \(K(B)\) is emitted, the names in scope are exactly the parameters and instruction results of the blocks on the dominator-tree path from the entry to \(B\), and the join points in scope are those of the children, already emitted, of the blocks on that path.
function Kelsey(F):
idom, rpo ← dominators and reverse postorder of F
headers ← { v : some edge u → v with rpo(u) ≥ rpo(v) }
function K(B):
out ← [ "let x = rhs in" for each instruction x = rhs of B ]
for C in children_D(B) sorted by decreasing rpo(C):
kw ← "loop" if C ∈ headers else "join"
out += [ kw C(params(C)) = K(C) in ]
out += Terminator(B) # br → jump, cbr → if/jump, ret → return
return out
return K(entry)
# The reverse direction flattens: each join/loop becomes a block with its parameters,
# each let an instruction, each `if a then M1 else M2` a cbr to two new blocks for M1, M2.
3. Worked example¶
Continuation-passing style on a small expression¶
Take \(e = x \ast (y + 1)\) with continuation \(\kappa\) (return). The naive transform (Definition 8.6.2) gives
with four administrative redexes: the applications of \(\lambda\kappa_1\), \(\lambda\kappa_2\), \(\lambda\kappa_3\) and \(\lambda\kappa_4\). Reducing them, one per step:
| step | redex reduced | remaining administrative redexes |
|---|---|---|
| 0 | — | 4 |
| 1 | \((\lambda\kappa_1.\,\kappa_1\,x)(\lambda a.\,\dots)\) → substitutes \(x\) for \(a\) | 3 |
| 2 | \((\lambda\kappa_2.\,\dots)(\lambda b.\,\dots)\) → \(\kappa_2\) becomes the \(b\)-continuation | 2 |
| 3 | \((\lambda\kappa_3.\,\kappa_3\,y)(\lambda c.\,\dots)\) → \(c := y\) | 1 |
| 4 | \((\lambda\kappa_4.\,\kappa_4\,1)(\lambda d.\,\dots)\) → \(d := 1\) | 0 |
The result, \(\lambda\kappa.\,\mathsf{let}\ t_1 = y + 1\ \mathsf{in}\ (\lambda b.\,\mathsf{let}\ t_2 = x \ast b\ \mathsf{in}\ \kappa\,t_2)\,t_1\), still has one redex: the continuation of \(y + 1\) applied to \(t_1\). It is administrative too (the transform built both the \(\lambda b\) and the call \(\kappa_2\,t_1\)), but it only became a redex when step 2 substituted \(\lambda b\) for \(\kappa_2\). A fifth step reduces it to \(\lambda\kappa.\,\mathsf{let}\ t_1 = y + 1\ \mathsf{in}\ \mathsf{let}\ t_2 = x \ast t_1\ \mathsf{in}\ \kappa\,t_2\). Algorithm 8.6.3 produces the fully reduced term in one pass: C is called with meta-level functions, so no \(\lambda\kappa_i\) is ever built. It emits let t1 = add y, 1 in let t2 = mul x, t1 in κ(t2), and with \(\kappa\) = "return", exactly the ANF let t1 = add y, 1 in let t2 = mul x, t1 in return t2. That is Theorem 8.6.10 on a small case.
A-normal form on the running example¶
Algorithm 8.6.5 on euler1.tiny (the reference solution, ch08-lower --form=anf labs/ch08-forms/inputs/euler1.tiny; the oracle lower_anf prints the same):
anf
loop loop.0(n.0, s.0, i.0) =
let t.0 = le i.0, n.0 in
if t.0 then
join j.0(n.1, s.1, i.1) =
let t.1 = add i.1, 1 in
jump loop.0(n.1, s.1, t.1)
in
let t.2 = rem i.0, 3 in
let t.3 = eq t.2, 0 in
join j.1(t.4) =
if t.4 then
let t.8 = add s.0, i.0 in
jump j.0(n.0, t.8, i.0)
else
jump j.0(n.0, s.0, i.0)
in
if t.3 then
jump j.1(1)
else
let t.5 = rem i.0, 5 in
let t.6 = eq t.5, 0 in
let t.7 = ne t.6, 0 in
jump j.1(t.7)
else
return s.0
in
jump loop.0(10, 0, 1)
Eighteen let/if/jump/return nodes (the lab counts join and loop definitions as zero, like block headers) and 130 executed steps (ch08-run --form=anf --stats). How the four constructs map:
| source | ANF | why |
|---|---|---|
n = 10; s = 0; i = 1 |
nothing; env = {n: 10, s: 0, i: 1} |
an assignment of an atom only updates the environment |
while i <= n |
loop loop.0(n.0, s.0, i.0) = … in jump loop.0(10, 0, 1) |
a recursive join point; its parameters are the loop-carried values |
if … { s = s + i } |
join j.0(n.1, s.1, i.1) = <rest of the body> in … |
the code after the if would otherwise be duplicated in both branches |
the short-circuit or |
join j.1(t.4) = <the if on t.4> in if t.3 then jump j.1(1) else … |
the value of the or is the join point's parameter |
return s |
else return s.0 in the loop's test |
the rest after a while is used once, so it is placed inline |
SSA as functional programming on gcd¶
gcd.tiny in the lab's SSA form (Algorithm 8.4.7) and its Kelsey term (Algorithm 8.6.7, ssa_to_anf in the oracle):
ssa anf
entry: loop b.0(a.0, b.3, t.0) =
br b.0(1071, 462, 0) let t.1 = ne b.3, 0 in
b.0(a.0, b.3, t.0): join b.1() =
t.1 = ne b.3, 0 let t.2 = rem a.0, b.3 in
cbr t.1, b.1(), b.2() jump b.0(b.3, t.2, t.2)
b.1: in
t.2 = rem a.0, b.3 join b.2() =
br b.0(b.3, t.2, t.2) return a.0
b.2: in
ret a.0 if t.1 then jump b.1() else jump b.2()
in
jump b.0(1071, 462, 0)
The trace of the translation (RPO: entry, b.0, b.2, b.1; dominator tree: entry → b.0 → {b.1, b.2}; back edge b.1→b.0, so b.0 is a loop header):
| step | block emitted | enclosing term | defined children (decreasing RPO) | terminator |
|---|---|---|---|---|
| 1 | entry | — | b.0 as loop |
jump b.0(1071, 462, 0) |
| 2 | b.0 | entry | b.1 (rpo 3) as join, then b.2 (rpo 2) as join |
if t.1 then jump b.1() else jump b.2() |
| 3 | b.1 | b.0 | none | jump b.0(b.3, t.2, t.2), visible because b.0 is a loop |
| 4 | b.2 | b.0 | none | return a.0 |
The SSA side needed the validator's dominance check (rule S2) to know that a.0 may be used in b.2. The ANF side gets the same fact from scoping alone: b.2's body is nested inside b.0's loop, where a.0 is a parameter. The lab's direct A-normalization of gcd (Algorithm 8.6.5) produces the same term with b.1 and b.2 inlined, since each is used once: loop loop.0(a.0, b.0, t.0) = let t.1 = ne b.0, 0 in if t.1 then … jump loop.0(b.0, t.2, t.2) else return a.0 in jump loop.0(1071, 462, 0). Both run in 16 steps.
Try it
./course drill tac-to-anf --seed 2 --difficulty hard --solution: TAC → blocks → pruned SSA →
dominator tree → the nested ANF term, and your own ANF graded by running it on 24 inputs.
4. Invariants and correctness¶
Continuation-passing style¶
Theorem 8.6.8 (Correctness of the CPS transform)
For every expression \(e\) and state \(\sigma\) with \(\langle e, \sigma \rangle \Downarrow v\), and every meta-continuation \(K\) that maps atoms to terms and is parametric (it uses its argument only as an atom): evaluating \(C(e, K)\) in an environment extending \(\sigma\) behaves like evaluating \(K(a)\) in an environment where the atom \(a\) holds \(v\). The output contains no administrative redexes.
Proof sketch (full proofs: [Plo75] for the naive transform; [DF92] for the one-pass transform and the absence of administrative redexes)
By structural induction on \(e\). Atoms: \(C(k, K) = K(k)\) trivially. Binary operators: by
the induction hypothesis for \(e_1\) with continuation \(K_1 = \lambda a.\,C(e_2, K_2)\), the
term behaves like \(K_1(a)\) with \(a\) holding \(v_1\). By the induction hypothesis for \(e_2\)
and \(K_2 = \lambda b.\,\mathsf{let}\ t = a \oplus b\ \mathsf{in}\ K(t)\), it behaves like
\(K(t)\) with \(t\) holding \(v_1 \mathbin{\hat{\oplus}} v_2 = v\). Short circuit: the two
branches call the join continuation \(\kappa\) with \(0\) or \([v_2 \ne 0]\), matching
Definition 0.2.2, and \(\kappa\)'s body is \(K(r)\). The absence of administrative redexes
holds because C never builds a λ that is applied immediately: every continuation it
passes is a meta-level function, reduced when the compiler runs.
A-normal form¶
Theorem 8.6.9 (A-normalization is correct, well scoped and linear)
For every Tiny program \(p\), Algorithm 8.6.5 returns a well-scoped ANF term (Definition 8.6.4) of size \(O(\lvert p \rvert \cdot (1 + \lvert V \rvert))\) that returns the value of \(p\) whenever \(p\) terminates.
Proof
Scoping: every atom that \(E\) or \(S\) emits is either a constant or taken from
\(\mathit{env}\). \(\mathit{env}\) contains only names bound by an enclosing let (from
E), or the parameters of the innermost enclosing loop/join (loop and if cases). Each
jump j is emitted by the continuation passed into the scope of \(j\): the join \(J\) of
if is called in the branches, which lie in \(j\)'s in part, and jump h in a loop body
lies in the body of loop h. Linearity: each meta-continuation is invoked once, except
\(J\) in the if case, which only emits a jump of \(\lvert V \rvert\) atoms. So no subterm
is duplicated, and each construct emits \(O(1 + \lvert V \rvert)\) syntax. Value: by
induction on the big-step derivation, as for Theorem 8.4.9. A jump j(args) binds \(j\)'s
parameters to the current values of all variables, which is exactly the state in which
the rest of the program runs. Tiny's while unrolling rule corresponds to one jump h.
Theorem 8.6.10 (ANF is CPS after administrative reduction)
For every expression \(e\) (without short-circuit operators), let \(\mathcal{C}\) be the naive CPS transform, \(\beta_{\mathrm{adm}}\) the normalization of administrative redexes, and \(\mathcal{U}\) the inverse transform that maps \(\mathsf{let}\ t = P\ \mathsf{in}\ \kappa\,t\) back to direct style with a final return. Then \(\mathcal{U}(\beta_{\mathrm{adm}}(\mathcal{C}[\![e]\!]))\) equals the A-normal form of \(e\) (Algorithm 8.6.5's expression part), up to renaming of temporaries.
Proof sketch (full proof: [FSDF93], where the three steps are shown to compose to the A-reductions)
By induction on \(e\). For an atom both sides are return a. For \(e_1 \oplus e_2\), the
administrative normal form of \(\mathcal{C}[\![e]\!]\) is the normal form for \(e_1\) with its
continuation hole filled by the normal form for \(e_2\), whose hole is filled by
\(\mathsf{let}\ t = a \oplus b\ \mathsf{in}\ \kappa\,t\). Reducing the administrative redexes
is exactly what the one-pass transform does at compile time (Theorem 8.6.8), so this equals
\(C(e, \lambda a.\,\kappa\,a)\). \(\mathcal{U}\) replaces the final \(\kappa\,t\) by return t,
which gives the same nesting of lets that \(E(e, \dots, \lambda a.\,\mathsf{return}\ a)\)
emits. §3 shows the four reduction steps for \(x \ast (y + 1)\).
SSA as functional programming¶
Lemma 8.6.11 (Where jumps land in the Kelsey term)
In a valid block-argument function, let \(u \to v\) be an edge with both ends reachable and \(v\) not the entry. Then (a) \(\mathrm{idom}(v)\) dominates \(u\). (b) If \(u \ne \mathrm{idom}(v)\), let \(c\) be the child of \(\mathrm{idom}(v)\) whose subtree contains \(u\). Then either \(c = v\) (and \(u \to v\) is a back edge, \(v\) a loop header), or \(\mathrm{rpo}(c) < \mathrm{rpo}(v)\), provided that the CFG is reducible.
Proof
(a) If some path \(r \leadsto u\) avoided \(\mathrm{idom}(v)\), extending it by \(u \to v\) would give a path to \(v\) avoiding a strict dominator of \(v\). (b) \(c\) dominates \(u\) (it is an ancestor in \(\mathcal{D}\)), so \(\mathrm{rpo}(c) \le \mathrm{rpo}(u)\): in RPO a dominator comes before every block it dominates, since each path from the entry passes it and RPO respects tree edges (Theorem 8.2.14). If \(u \to v\) is not a back edge, \(\mathrm{rpo}(u) < \mathrm{rpo}(v)\) (Theorem 8.2.14), hence \(\mathrm{rpo}(c) < \mathrm{rpo}(v)\). If it is a back edge in a reducible CFG, \(v\) dominates \(u\) (Theorem 15.6.4), so \(v\) lies on the dominator-tree path from \(\mathrm{idom}(v)\) to \(u\) and is therefore the child \(c\).
Theorem 8.6.12 (SSA ≡ ANF: strict SSA with block arguments and well-scoped ANF with join points correspond)
(a) For every valid block-argument SSA function \(F\) with a reducible CFG, the Kelsey term
\(K(\mathit{entry})\) (Algorithm 8.6.7) is well scoped (Definition 8.6.4) and behaves like \(F\):
the same instructions are executed on the same values, in the same order.
(b) Conversely, flattening a well-scoped ANF term (each join/loop a block with its
parameters, each let an instruction, each jump a br, each if a cbr to two new
parameterless blocks holding its arms) yields a block-argument function
that satisfies S1 after renaming bound names apart, and S2: lexical scope implies dominance.
Hence the SSA rule "definitions dominate uses" and the ANF rule "names are used in their
scope" are the same constraint.
Proof
(a) Variables. A use of \(x\) in block \(B\) is dominated by \(x\)'s definition in block \(D\)
(rule S2). \(D\) is therefore \(B\) or an ancestor of \(B\) in \(\mathcal{D}\). \(K(B)\) is nested
inside \(K(D)\), and in \(K(D)\) the lets and the parameters of \(D\) enclose every child
definition and the terminator. So \(x\) is in scope at the use. A use earlier in the same
block is impossible by S2. Arguments of \(B\)'s terminator are uses at the end of \(B\), and
they are in scope because the terminator is emitted last in \(K(B)\). Jumps. For a jump in
\(K(u)\) to \(v\): by Lemma 8.6.11(a), \(K(u)\) is nested in \(K(\mathrm{idom}(v))\). If
\(u = \mathrm{idom}(v)\), the terminator comes after all child definitions, so \(v\) is in scope.
Otherwise, by Lemma 8.6.11(b), \(K(u)\) lies in \(K(c)\) for a child \(c\) with \(c = v\), in which
case \(v\) is a loop header and was emitted as loop, whose body may jump to it, or with
\(\mathrm{rpo}(c) < \mathrm{rpo}(v)\). In the latter case \(v\)'s definition was emitted before \(c\)'s
(decreasing RPO), so \(K(c)\) lies in \(v\)'s in part. Arity is rule S3. Behavior.
Both have the same instructions. jump v(args) binds \(v\)'s parameters to the arguments'
values and continues in \(K(v)\), which is exactly the parallel copy of Definition 8.4.4. By
induction on the number of executed edges, both run the same blocks with the same values.
(b) After renaming apart, every name is bound once, which is S1. For S2, take a use of \(x\)
at a point \(p\) in the term. \(p\) is lexically inside the scope of \(x\)'s binder \(\beta\), which
is a let or the parameter list of a join point \(J\). Consider any execution path from the
start to \(p\). Control can only enter a term by falling through from its enclosing term, or by
a jump to a join point, and a jump to \(J'\) is only possible from inside \(J'\)'s scope (its
in part, or its body for loop), which by induction on the path has already executed the
code that encloses \(J'\)'s definition. So every path to \(p\) executes \(\beta\) (for a let) or
enters \(J\) (for a parameter) first. That is dominance of the definition over the use in the
flattened CFG.
Corollary 8.6.13 (One environment suffices)
An ANF term in which every binder has a distinct name (or slot) can be executed with a
single mutable environment, without closures: the most recent value of each slot is always
the one in scope. The lab's provided ANF interpreter relies on this
(labs/ch08-forms/provided/Forms.cpp, runANF), and so does every SSA interpreter.
Proof
By Theorem 8.6.12(b), the flattened function is strict SSA. In an execution of strict SSA
code, when a use of \(x\) runs, the most recent execution of \(x\)'s definition is the one
that dominates it on the current path, since every path passes the definition and no other
definition of \(x\) exists. So reading the current slot gives the right value. The
Python oracle uses closures instead (run_anf_term), and test_ch08.py checks that the
two agree on 120 random programs.
5. Complexity¶
Variables: \(\lvert p \rvert\) = program size, \(V\) = source variables, \(m\) = blocks.
| Technique | Time (worst) | Time (typical) | Space | Justification |
|---|---|---|---|---|
| CPS (Alg. 8.6.3) | \(O(\lvert e \rvert)\) | same | output \(O(\lvert e \rvert)\) | one emission per node; the naive transform first builds \(O(\lvert e \rvert)\) administrative redexes |
| ANF (Alg. 8.6.5) | \(O(\lvert p \rvert (1 + V))\) | same | same | Theorem 8.6.9 |
| SSA → ANF (Alg. 8.6.7) | \(O(n + m \log m)\) plus the dominator tree | near-linear | output = input size | each block emitted once; children sorted by RPO |
Pathological family. ANF without join points duplicates the continuation of every if. For a chain \(\mathsf{if}\ c_1\ \{\}\ \mathsf{else}\ \{\};\ \dots;\ \mathsf{if}\ c_k\ \{\}\ \mathsf{else}\ \{\};\ \mathsf{return}\ x\), the term for the rest after \(\mathsf{if}_1\) appears in both branches, and so on recursively. That gives \(2^k\) copies of return x, a term of size \(\Theta(2^k)\). With join points (Algorithm 8.6.5) the size is \(\Theta(k \cdot V)\). This is the observation behind Kennedy's and Maurer et al.'s arguments for second-class continuations [Ken07; MDAJ17].
At scale. SML/NJ compiled its whole implementation through CPS for decades [App92]. GHC has used join points in its optimizer since version 8.2; Maurer et al. describe the design and its effect on the simplifier [MDAJ17].
6. Variants and refinements¶
Continuation-passing style¶
- Second-class continuations (Kennedy's CPS with
letcont, the form of Definition 8.6.1) compile to jumps and stack frames, so the CPS IR needs no closure for every return point [Ken07]. - Higher-order vs first-order transforms: Danvy and Filinski's higher-order one-pass transform avoids administrative redexes. A first-order transform plus a simplifier is easier to write but slower [DF92].
- CPS with a stack (Chicken's Cheney-on-the-MTA): C functions never return, the C stack is the nursery of the garbage collector, and it is collected when full. This trades portable C for unusual runtime machinery.
A-normal form¶
- Monadic normal form generalizes ANF by letting
letbind any computation, which allows nestedlets. It is used in some typed intermediate languages. - Join points (GHC's
join/joinrec, Kotlin-style local jumps) remove ANF's duplication problem and make ANF equivalent to a CFG [MDAJ17]. - Delimited ANF with exceptions:
letof a call that may throw needs an extra handler continuation, which makes ANF closer to CPS again.
SSA as functional programming¶
- Mutually recursive join groups handle irreducible CFGs: define all children of a block in one
letrecgroup, so that siblings may jump to each other in both directions [Kel95]. - Nesting by loops instead of dominance (RVSDG, Lesson 8.5) makes scopes coincide with loop bodies and conditionals, which requires restructuring.
- Type systems on SSA transfer from the functional side: typed assembly languages and dependent types over SSA use the lexical view [App98].
7. In real compilers¶
Continuation-passing style¶
SML/NJ: the CPS datatype cexp (constructors APP for calls, FIX for mutually recursive local functions) in compiler/CPS/cps/cps.sig (tag v2025.1) [SMLNJ-CPS]. Chicken Scheme 5.3.0 CPS-converts every program before generating C. There is no CPS IR in LLVM, GCC or rustc.
Chicken Scheme's CPS conversion of the running example
Reproduce (CHICKEN 5.3.0, Ubuntu package chicken-bin):
cat > euler1.scm <<'EOF'
(define (euler1 n)
(let loop ((i 1) (s 0))
(if (> i n)
s
(loop (+ i 1)
(if (or (= 0 (remainder i 3)) (= 0 (remainder i 5))) (+ s i) s)))))
(display (euler1 10))
(newline)
EOF
chicken euler1.scm -debug 3 -optimize-level 0 -output-file /dev/null
Output (complete):
[cps]
(lambda (k24)
(let ((k25 (##core#lambda
(r26)
(let ((t18 r26))
(let ((k28 (##core#lambda
(r29)
(let ((t19 r29))
(let ((t31 (set! euler1
#f
(lambda (k33 n10)
(let ((k34 (##core#lambda (r35) (k33 r35))))
(let ((loop11 (##core#undefined)))
(let ((t37 (set! loop11
#f
(lambda (k39 i12 s13)
(let ((k40 (##core#lambda (r41) (k39 r41))))
(let ((k43 (##core#lambda
(r44)
(if r44
(k40 s13)
(let ((k46 (##core#lambda (r47) (k40 r47))))
(let ((k50 (##core#lambda
(r51)
(let ((a49 r51))
(let ((k54 (##core#lambda
(r55)
(let ((a53 r55)) (loop11 k46 a49 a53)))))
(let ((k57 (##core#lambda
(r58)
(let ((tmp1416 r58))
(let ((k60 (##core#lambda
(r61)
(if r61
(let ((k63 (##core#lambda (r64) (k54 r64))))
(scheme#+ k63 s13 i12))
(k54 s13)))))
(if tmp1416
(k60 tmp1416)
(let ((k66 (##core#lambda (r67) (k60 r67))))
(let ((k70 (##core#lambda
(r71)
(let ((a69 r71)) (scheme#= k66 0 a69)))))
(scheme#remainder k70 i12 5)))))))))
(let ((k74 (##core#lambda
(r75)
(let ((a73 r75)) (scheme#= k57 0 a73)))))
(scheme#remainder k74 i12 3))))))))
(scheme#+ k50 i12 1)))))))
(scheme#> k43 i12 n10)))))))
(let ((t17 t37)) (loop11 k34 1 0)))))))))
(let ((t20 t31))
(let ((k77 (##core#lambda
(r78)
(let ((t21 r78))
(let ((k80 (##core#lambda
(r81)
(let ((t22 r81))
(let ((k83 (##core#lambda (r84) (k24 r84))))
(let ((k86 (##core#lambda (r87) (r87 k83))))
(chicken.base#implicit-exit-handler k86)))))))
(scheme#newline k80))))))
(let ((k90 (##core#lambda
(r91)
(let ((a89 r91)) (scheme#display k77 a89)))))
(euler1 k90 10)))))))))
(##core#callunit eval k28))))))
(##core#callunit library k25)))
What to notice: every call takes a continuation as its first argument (scheme#+ k63 s13
i12 means "add, then call k63 with the sum"), and every call is a tail call. The loop
loop11 takes its continuation k39 plus i12, s13, the loop-carried values, and the
recursive call (loop11 k46 a49 a53) passes the new values. The ##core#lambdas are
second-class continuations (Definition 8.6.1): they are only called. The trivial ones such
as (##core#lambda (r35) (k33 r35)) are administrative (η-)redexes that Chicken's
optimizer removes at -optimize-level 1 and above.
A-normal form¶
GHC: CorePrep puts Core into A-normal form; the module comment of compiler/GHC/CoreToStg/Prep.hs lists "Convert to A-normal form; that is, function arguments are always variables" (corePrepPgm; tag ghc-9.4.7-release) [GHC-Prep]. The lab's anf reader and interpreter are ANFParser and runANF in labs/ch08-forms/provided/Forms.cpp.
GHC's CorePrep: A-normal form with join points
Reproduce (GHC 9.4.7, Ubuntu package ghc; unique suffixes such as _sYE are stable for a given compiler and input):
cat > Euler1.hs <<'EOF'
module Euler1 (euler1) where
euler1 :: Int -> Int
euler1 n = go 1 0
where
go i s
| i > n = s
| i `rem` 3 == 0 || i `rem` 5 == 0 = go (i + 1) (s + i)
| otherwise = go (i + 1) s
EOF
ghc -O1 -fforce-recomp -dsuppress-all -dno-typeable-binds -ddump-prep -c Euler1.hs \
| sed -n '/^euler1/,$p'
Output (complete):
euler1
= \ n_sYE ->
case n_sYE of { I# ww_sYG ->
join { $j_sYH ww1_sYI = I# ww1_sYI } in
joinrec {
$wgo_sYJ ww1_sYK ww2_sYL
= case ># ww1_sYK ww_sYG of {
__DEFAULT ->
case remInt# ww1_sYK 3# of {
__DEFAULT ->
case remInt# ww1_sYK 5# of {
__DEFAULT ->
case +# ww1_sYK 1# of sat_sYP { __DEFAULT ->
jump $wgo_sYJ sat_sYP ww2_sYL
};
0# ->
case +# ww2_sYL ww1_sYK of sat_sYR { __DEFAULT ->
case +# ww1_sYK 1# of sat_sYQ { __DEFAULT ->
jump $wgo_sYJ sat_sYQ sat_sYR
}
}
};
0# ->
case +# ww2_sYL ww1_sYK of sat_sYT { __DEFAULT ->
case +# ww1_sYK 1# of sat_sYS { __DEFAULT ->
jump $wgo_sYJ sat_sYS sat_sYT
}
}
};
1# -> jump $j_sYH ww2_sYL
}; } in
jump $wgo_sYJ 1# 0#
}
What to notice: every argument of jump and of the primitive operations is a variable
or a literal. The compound +# ww1_sYK 1# of the simplifier's output (next box) has been
bound by case +# ww1_sYK 1# of sat_sYP { __DEFAULT -> … }, which is a strict let in
Definition 8.6.4's sense. join { $j_sYH … } and joinrec { $wgo_sYJ … } are exactly the
lab's join and loop.
SSA as functional programming¶
GHC: join points are ordinary Core bindings whose identifier has a join arity (type JoinArity in compiler/GHC/Types/Basic.hs), and Core Lint checks that jumps are saturated tail calls [MDAJ17]. MLton turns its CPS-like intermediate language into an SSA IR whose blocks take arguments and whose transfers are Goto {dst, args} (mlton/ssa/ssa-tree.sig, tag on-20210117-release) [MLTON-SSA]. MLIR and Cranelift are the SSA-side view of the same design (Lesson 8.4).
GHC's joinrec is a loop header with block arguments
Reproduce (GHC 9.4.7; Euler1.hs from the previous box):
ghc -O1 -fforce-recomp -dsuppress-all -dsuppress-uniques -dno-typeable-binds -ddump-simpl -c Euler1.hs \
| sed -n '/^euler1/,$p'
Output (complete):
euler1
= \ n ->
case n of { I# ww ->
join { $j ww1 = I# ww1 } in
joinrec {
$wgo ww1 ww2
= case ># ww1 ww of {
__DEFAULT ->
case remInt# ww1 3# of {
__DEFAULT ->
case remInt# ww1 5# of {
__DEFAULT -> jump $wgo (+# ww1 1#) ww2;
0# -> jump $wgo (+# ww1 1#) (+# ww2 ww1)
};
0# -> jump $wgo (+# ww1 1#) (+# ww2 ww1)
};
1# -> jump $j ww2
}; } in
jump $wgo 1# 0#
}
What to notice: read it as SSA with block arguments (Theorem 8.6.12).
joinrec { $wgo ww1 ww2 = … } is the loop header block $wgo(ww1, ww2), the analogue of
MLIR's ^bb1(%1, %2) in Lesson 8.4. jump $wgo 1# 0# is br $wgo(1, 0). The three
jump $wgo … sites are the back edges with their arguments, and join { $j ww1 = I# ww1 }
is the exit block, which boxes the result. Unlike the C and MLIR versions, GHC duplicated
the s + i path into the two 0# alternatives instead of merging it: in the functional
view, merging would introduce another join point, and inlining a small one is a normal
simplification.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Continuation-passing style | control fully explicit, including exceptions and call/cc; every call a tail call | \(O(\lvert e \rvert)\) one-pass · administrative redexes if naive | verbose: 68 lines for euler1 in Chicken | moderate (one-pass transform; closure representation for escaping continuations) | Scheme and ML compilers (Chicken, SML/NJ), compiling first-class control |
| A-normal form | same optimizations as CPS for direct-style programs; with join points, same as a CFG | \(O(\lvert p \rvert(1 + V))\) · lab: 18 nodes, 130 steps on the running example | readable direct style; scoping errors are static ("not in scope") | low (Algorithm 8.6.5) | GHC CorePrep, many functional-language compilers, the lab's anf |
| SSA as functional programming | a bijection: strict SSA ≡ well-scoped ANF (Theorem 8.6.12) | translation \(O(n + m \log m)\) given dominators | lets you use lexical-scope reasoning (and type systems) on SSA | low given a dominator tree | MLton's SSA from CPS, GHC's join points, MLIR/SIL block arguments |
Choose CPS when the source language has first-class control (call/cc, generators, effect handlers) that should be compiled away. Choose ANF with join points for a functional language whose control flow is ordinary. It keeps direct style and is a CFG in disguise. Use the correspondence whenever you move between a functional front end and an SSA back end (MLton, GHC's Cmm/LLVM path), and when you want an easy proof that a transformation preserves SSA's dominance property: show that it preserves scoping.
9. Assessment¶
| Technique | Quiz ids (solutions/quizzes/ch08.yaml) |
Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Continuation-passing style | cps-admin-redexes, cps-tail-calls |
none: the one-pass transform has a unique answer per expression, which the quiz computes; the ANF drill covers the same skill | cps |
— |
| A-normal form | anf-join-why, anf-size-chain |
./course drill tac-to-anf |
anf |
L1 (anf form) |
| SSA as functional programming | kelsey-nesting, scope-is-dominance |
./course drill tac-to-anf --difficulty hard (worked solution goes through SSA) |
ssa-anf |
L1 |
Nest by the dominator tree, not by the CFG's successors
A tempting translation defines each block's successors inside it. For a join block with two predecessors, that puts its definition in two places, or in the scope of only one of them. The only place from which both predecessors can see it is their common dominator, which is Kelsey's rule and the reason Definition 8.6.6 uses \(\mathcal{D}\).
References¶
See the chapter references.