Verification of Code Generators via
Higher-Order Model Checking
Takashi Suwa
Takeshi Tsukada
Naoki Kobayashi

Atsushi Igarashi
Kyoto University

The University of Tokyo

Abstract

uated to a positive integer; to guarantee such a property, one has toredesign the type system of the language.
We propose an alternative approach to safe code generation,
based on higher-order model checking [15, 21]. We provide programmers with a simple functional language equipped with primitives for generating symbols and constructing code fragments. The
programs in our language must be simply-typed, but unlike λand other typed multi-stage languages, the generated code is dynamically typed; we have only a single type code for code andsymbols. Thus, programs may generate ill-typed programs, or eventhose that do not respect variable bindings (like λx.y, which contains an unbound variable). To reject those invalid code generators, we transform a code generator to a tree-generating program,which produces a certain tree representation of the generated code.
By appropriately instrumenting the trees, various notions of “validity” (such as closedness and well-typedness) of the generated codeare reduced to regular properties on the corresponding trees, which
can be checked by using higher-order model checking. Higherorder model checking [21] is a higher-order extension of finite-statemodel checking, which can decide whether the tree generated by agiven simply-typed tree grammar satisfies a given regular tree property.
We explain our approach through an example. Let us consider
the following OCaml-like program, where the function main takes
an integer n as an argument and generates code for the function thattakes x and returns xn .

Dynamic code generation is useful for optimizing code with respect
to information available only at run-time. Writing a code generator is, however, difficult and error prone. We consider a simple
language for writing code generators and propose an automatedmethod for verifying code generators. Our method is based onhigher-order model checking, and can check that a given code generator can generate only closed, well-typed programs. Comparedwith typed multi-stage programming languages, our approach isless conservative on the typability of generated programs (i.e. canaccept valid code generators that would be rejected by typicalmulti-stage languages) and can check a wider range of propertiesof code generators. We have implemented the proposed method andconfirmed its effectiveness through experiments.

1.

Introduction

Dynamic code generation, where code is generated by running a
program (called a code generator), is useful for specializing a program with respect to information available at runtime. Writing acode generator is often difficult and error prone, however. A number of multi-stage languages have been introduced [3, 5, 8, 10, 13,
20, 30–33, 36] to make it easier to write program generators. Those
languages are usually equipped with type systems to ensure that
only “valid” programs can be generated. A drawback of such typed
multi-staged languages is that the type systems are sometimes tooconservative on the typability of generated programs. For example,
λ [9] expresses the type of a program for generating a value oftype τ as τ . But then the following program:let rec genpower n x =if n=0 then One else Times(x, genpower (n-1) x)
let main n =let x = gensym() in Abs(x, genpower n x)

if mode = "int" then next(0) else next(0.0)

Here, One, Times, and Abs are code constructors of arities 0, 2,
and 2 respectively; they represent the code for constant 1, multiplication, and a λ-abstraction respectively. The function main takes
an integer n, generates a fresh symbol and then passes n and thesymbol to the function genpower, which returns a code fragment
e of the form Times(x, · · · Times(x, One) · · · ). The main function
then returns the whole code Abs(x, e) (which represents the function λx.xn ).
We convert the above program to the following, non-deterministic
program for generating trees.

will be rejected as ill-typed, because the then-part has type int
whereas the else-part has typefloat. (Here, suppose thatnext M generates the code for evaluating M at the next stage.)
The type systems of multi-stage languages are also not flexible
enough on the guaranteed properties; for example, while the typesystem for λ can guarantee that an expression of type int
only generates a code fragment evaluated to an integer, it does notguarantee that the expression generates only a code fragment eval-let gensym() = ...
let rec genpower x =if * then One else Times(x, genpower x)
let main() =let x = gensym() in Abs(x, genpower x)
Here, we have removed integer arguments and replaced the condition n = 0 with a non-deterministic Boolean *. The code construc-[Copyright notice will appear here once ’preprint’ option is removed.]1

2016/10/1

tors have been replaced by tree constructors of the same name. The
definition of gensym depends on the property to be verified. If wewish to verify that the code produced by the original program isAbs(x, M ), where M is of the form

ments on the verification methods propopsed in Section 3. Section 5
introduces a relaxed version of λ and provides a translation fromit into the gensym language, so that we can apply our verification
method to programs written in the relaxed λ . Section 6 discusses
limitations of our method and related work. Section 7 concludes
the paper.

Times(x1 , Times(x2 , · · · Times(xn , One) · · · )),then we can simply define gensym as a constant function thatalways returns a singleton tree Var:

Notationslet gensym() = Var

We write N for the set of natural numbers. For a natural numbern ∈ N, we write [n] for {k ∈ N | 1 ≤ k ≤ n}. For a binary
relation R ⊆ A × B, we write dom(R) and im(R) for {a ∈A | ∃b ∈ B. (a, b) ∈ R} and {b ∈ B | ∃a ∈ A. (a, b) ∈ R}
respectively. For a (partial) map f from A to B, dom(f ) and im(f )are defined as special cases. For a map f , we write f [a 7→ b] forthe map f 0 such that dom(f 0 ) = dom(f ) ∪ {a}, f 0 (a) = b, andf 0 (x) = f (x) for x ∈ dom(f 0 ) \ {a}.

Then, the transformed program generates
Abs(Var, One),
Abs(Var, Times(Var, One)),Abs(Var, Times(Var, Times(Var, One))), . . .
in a non-deterministic manner. Therefore, it suffices to check that
all the generated trees belong to the regular tree language describedby the grammar:
S → Abs(Var, A)
A → OneA → Times(Var, A),

2.

The Language for Code Generation

This section introduces a language for writing code generatorsthat we call the gensym language. To clairfy the essence of ourverification method, the language is kept minimal; it is a callby-name functional programming language with code constructors
and primitives for generating fresh symbols, having only code asbase type values. All the functions are named and defined at the
top level. The language should be considered a core language, towhich actual programs written by programmers are transformed
before applying our verification method. For dealing with call-byvalue programs (like the examples in Section 1), it suffices to apply
the CPS transformation. For dealing with programs using othervalues such as integers, we can use predicate abstraction [17], andthen encode Booleans as functions, code and functions as primitive
values.
We assume a finite set of code constructors, and write P for themap from the set of code constructors to the set of natural numbers,
representing the arities of code constructors. We assume that P
contains at least the following bindings:

by using higher-order model checking.
To verify that the above program generates only closed programs (where Abs is considered a variable binder), one can instead
define gensym by:let gensym() = if * then Var else Ig
It returns either Var or Ig. Intuitively, Var represents variables
whose binding information should be tracked, whereas Ig represents those that should be ignored. Then, to check the closedness, itsuffices to check that whenever Var occurs in the generated code,
it is in the scope of Abs(Var, . . .). Indeed, the trees generated by
the transformed program are:Abs(Var, One), Abs(Ig, One),
Abs(Var, Times(Var, One)), Abs(Ig, Times(Ig, One)),Abs(Var, Times(Var, Times(Var, One))),Abs(Ig, Times(Ig, Times(Ig, One))), . . . ,all of which satisfy the condition above. If the main function were
wrongly defined by:

APP 7→ 2,

let main n =let x = gensym() in let y = gensym() inAbs(x, genpower n y),

ABS 7→ 2,

FIX 7→ 2,

IFTE 7→ 3.

then, the set of the trees generated by the transformed program
would contain:

They are constructors for function applications, abstractions, recursions, and conditional expressions (if-then-else). In examples, we
use other constructors such as TIMES (of arity 2) and ’n (of arity 0)
for each integer n. We use the meta-variable P for code costructors.
A function definition is a pair:Abs(Ig, Times(Var, One)),(F, λx1 . · · · λxk . e),which indicates that open code may be generated. In this manner,with an appropriate instantiation of the gensym function, we canverify various properties of the programs generated by code generators.
We formalize the above idea and show how the closedness
and well-typedness of the generated code can be verified by using
higher-order model checking. Since it may be too low-level todirectly write a program generator in the gensym language, we
also design a simple two-stage programming language, which issimilar to λ , but does not require expressions of the next stage
to be simply-typed, and formalize the translation from λ to thegensym language, so that our verification method can be applied.
We have implemented a prototype verification tool based on our
method, and confirmed its effectiveness.
The rest of this paper is structured as follows: Section 2 introduces the gensym language, the source language for describing
code generators. Section 3 formalizes our verification methods forcode generators. Section 4 reports an implementation and experi-

where F is a function symbol and e ranges over the set of applicative terms, defined by:e ····= F | x | e e | P | gensym/cont.
Here, F and x are meta-variables for function symbols and variables respectively. The primitive gensym/cont e is a fresh symbol generator in continuation passing style; it takes an expression e as an argument, creates a fresh symbol, and passes it toe. We often write F x1 · · · x` = e for the function definition(F, λx1 . · · · λx` . e). We also often abbreviate a finite sequence ofvariables x1 , . . . , x` to x̃, and write (F, λx̃. e) or F x̃ = e for thefunction definition.
A (source) program is a pair (D, S ) where D is a finite set offunction definitions, and S, called the main function, is one of thefunction symbols defined in D. We allow D to contain more than
one function definition for each function symbol. That is for the
purpose of modelling non-determinism that would be introduced
when predicate abstraction is used.

2

2016/10/1

The operational semantics of the language is given as follows.
We assume a countably infinite set Symbol of symbols that may
be generated by gensym/cont, ranged over by α. The set ofruntime terms, the set of code values, and the set of evaluation
contexts, ranged over respectively by ê, v, and C, are defined by:Γ ` P : code
→ · ·{z· → code →|} codeP (P )

The following is a standard property of the simple type system.

ê ····= α | F | ê ê | P | gensym/cont ,v ····= α | P | v v ,C ····= [ ] | P v · · · v C ê · · · ê .

Theorem 2. Let (D, S ) be a well-typed program of the gensym
language. If S ,→D ∗ ê, then (i) ê is a value and ∅ ` ê : code; or(ii) there exists a run-time term ê0 such that ê ,→D ê0 .

We write C[ê] for the term obtained by replacing the sole occurrence [ ] in the evaluation context C with the term ê. The reduction
relation ,→D of the gensym language is defined as the least relationthat satisfies the following rules:

3.

This section describes methods to verify the code generated bya program of the gensym language. As mentioned in the introduction, we reduce verification problems to the decision problem
called higher-order model checking [15, 21]. We shall briefly review (a variant of) higher-order model checking in Section 3.1 andthen describe methods to verify closedness (Section 3.2) and welltypedness (Section 3.3) of the generated code.

C[F ê1 · · · ê` ] ,→D C[[ê` /x` ] · · · [ê1 /x1 ]e]if (F x1 · · · x` = e) ∈ D
C[gensym/cont ê] ,→D C[ê α]
if α ∈ Symbol does not occur in C[gensym/cont ê]3.1

If S ,→D ∗ v, we say v is a code value generated by (D, S ). We
write C (D, S ) for the set of code values that the program generates.
D ··= {GenPower x = ’1,

Remark 3. The definition of higher-order model checking given
below is actually a variant of the original problem in [21], which
properly subsumes ours. The differences are: (1) in the original
setting, a higher-order recursion scheme is deterministic and generates a possibly infinite tree, whereas in our setting, it is nondeterministic and generates a set of finite trees, and (2) a property inthe original setting is ω-regular, whereas in our setting it is regular(since we do not handle infinite trees in our setting).

GenPower x = TIMES x (GenPower x),
S = gensym/cont K,
K x = ABS x (GenPower x)}
corresponds to the genpower example in Section 1. The following
is a reduction process of (D, S ):S ,→D gensym/cont K ,→D K α ,→D ABS α (GenPower α),→D ABS α (TIMES α (GenPower α)),→D ABS α (TIMES α (TIMES α (GenPower α))),→D ABS α (TIMES α (TIMES α (TIMES α (GenPower α))))Higher-order recursion schemes Intuitively, a higher-order recursion scheme is a call-by-name, simply-typed, and non-deterministic
functional program for generating a tree.
A ranked alphabet Σ is a finite collection of symbols equippedwith their arities. Formally it is a map Σ : dom(Σ) → N from afinite set of symbols (called terminal symbols) to natural numbers.
A (non-deterministic) higher-order recursion scheme (a HORS
for short) on a ranked alphabet Σ is a triple G = (Σ, R, S )consisting of,→D ABS α (TIMES α (TIMES α (TIMES α ’1)))
We require that programs are simply-typed. The set of types,
ranged over by τ , is defined by:τ ····= code | τ → τ
where the type code describes the type of generated code. Notethat every code fragment has the same type code and we do not
aim to infer (more detailed) types for generated code fragments bythis simple-type system, unlike typed multi-stage calculi such as
λ [9]. A program (D, S ) is well-typed if there exists a type environment Γ of the form {Fi 7→ τi | Fi ∈ dom(D)} that satisfies
Γ (S ) = code and Γ ` (λx̃. e) : Γ (F ) for each (F x̃ = e) ∈ D,
where the typing rules for (runtime) terms are given as follows:• the ranked alphabet Σ;• a finite set R of rewriting rules of the form:

F x̃ → t,
where F is a symbol called a nonterminal, x̃ is a (possibly
empty) finite sequence of variables and t is an applicative term
given by the grammar t ····= a | F | x | t t (where a, F , andx range over dom(Σ), the set of non-terminals, and the set {x̃}of variables);Γ [x1 7→ τ1 ] · · · [x` 7→ τ` ] ` e : codeΓ ` λx1 . · · · λx` . e : τ1 → · · · → τ` → code(Γ (F ) = τ )Γ ` x:τΓ ` F :τPreliminaries: higher-order model checking

Higher-order model checking [15, 21] is the problem to decide
whether, given a higher-order tree grammar (called a higher-orderrecursion scheme) G and a regular tree property A, the trees generated by G satisfy A.

Example 1. The program (D, S ), where(Γ (x) = τ )Verification Method• a special non-terminal S called the start symbol.

We write dom(R) for the set of nonterminals occurring on the lefthand side of a rule. Each non-terminal may have more than one
rewriting rule, as in the language in Section 2. We require that the
HORS be simply-typed in the following sense. Let Sort be theset of sorts (i.e. simple types for HORSs) defined by κ ····= o |κ → κ, where o is the sort of trees. The HORS G = (Σ, R, S )is well-typed if there exists a map K : dom(R) → Sort from
nonterminals to sorts such thatΓ ` α : codeΓ ` ê1 : τ2 → τΓ ` ê2 : τ2Γ ` ê1 ê2 : τΓ ` gensym/cont : (code → code) → code3

2016/10/1

• for every rule (F x1 . . . x` → t) ∈ R, there exist sorts• K(S ) = o holds for the start symbol S,

q J r is inductively defined by: (a t1 · · · tm ) a∆ q J r if r is of
the form (q r1 · · · rm ) and there exists (q a → q1 · · · qm ) ∈ ∆such that ti a∆ qi J ri for each i ∈ [m]. A Q-labeled tree r iscalled a run-tree of A over t if t a∆ q INI J r holds.

where each terminal a ∈ dom(Σ) has the type o·→o→| → · ·{z} o.

Example 5. Let Σ be a ranked alphabet in Example 4. Consider
the automaton A1 = (Σ, {q0 , q1 }, ∆, q0 ) where:κ1 , . . . , κ` that satisfy K[x1 7→ κ1 ] · · · [x` 7→ κ` ] `Σ t : oand K(F ) = κ1 → · · · → κ` → o, andΣ (a)∆ ··= {q0 a → q1 q1 ,q0 c → ε,Given a HORS G = (Σ, R, S ), we define the reduction relation−→G as the least relation that satisfies:• (F t1 · · · t` ) −→G [t` /x` ] · · · [t1 /x1 ]t

q0 d → ε,if (F x1 · · · x` → t) ∈ R,

We write −→∗G for the reflexive and transitive closure of −→G .
A (finite) Σ-labeled ranked tree (or simply a tree) is an applicative term consisting only of terminal symbols. As usual, we often
depict the tree a t1 · · · tn as follows.

q0
q1

a

c

···

c
tm

A value tree of a HORS G is a tree t such that S −→∗G t. We write
L(G) for the set of value trees generated by G.

a∆ q 0 J
b

q1
q1

q1

a

b
···

q1 d → ε}.

a

a

t2

q1 b → q1 ,Intuitively, A1 accepts a tree t if every b-labeled node of t has anancestor node labeled with a. For example, the tree on the lefthand side of Example 4 (as well as the one on the right-hand side)is accepted by A1 , as witnessed by the following relation.

• (a t1 · · · ti · · · tm ) −→G (a t1 · · · t0i · · · tm )if Σ (a) = m and ti −→G t0i .

t1

q1 a → q1 q1 ,q1 c → ε,

d

q1

q1

b

q1

c

q1

q1

For another example of automata, let A2 = (Σ, {q }, ∆, q ) where∆ ··= {q a → q q, q b → q, q c → ε}. This automaton checks
whether every leaf of a given tree is labeled with c. The tree above
is not accepted by A2 .


Example 4. Consider the HORS G = (Σ, R, S ) where:Σ ··= {a 7→ 2, b 7→ 1, c 7→ 0, d 7→ 0},
R ··= {S → F c, F x → a x (F (b x)), F x → d}.

Higher-order model checking We say that a HORS G is acceptedby a tree automaton A if all the value trees of G are accepted by A.
Higher-order model checking is the following decision problem:

The following are value trees of G:
a
a

c
a
a

c

c
a

b
c

b

d

Given a HORS G and a tree automaton A on a common
ranked alphabet Σ, is G accepted by A?

ab

Example 6. Let G0 = (Σ, R, S ) be a HORS in Example 4 andA1 and A2 be automata in Example 5. The HORS G0 is acceptedby A1 , whereas G1 is not.


a

b
b

b

c

b

b

b

c

c

d

Higher-order model checking is decidable [21]. Despite its
extremely high computational complexity, practical higher-ordermodel checkers [2, 15, 24] are available that run fast for typicalinputs.
3.2

Verifying closedness of generated code

Since the gensym language defined in Section 2 has independent
mechanisms for generating (i.e. gensym/cont) and binding (i.e.
ABS e1 e2 and FIX e1 e2 ) a symbol, it is possible for users to write
mistakenly a program that can generate code with an unbound variable. In this section, we propose a method to check that every code
generated by a given source program is closed. As sketched in the
introduction, given a source program (D, S ), we convert (D, S ) toa HORS Gcls (D, S ), and check whether Gcls (D, S ) is accepted byan automaton Acls using higher-order model checking.
A code value v is closed if so is the obvious corresponding
λ-term. This notion is formally defined as follows. A code value
v is well-formed if, for every subterm of the form ABS v1 v2 or
FIX v1 v2 , v1 ∈ Symbol. We say that the occurrences of α
in ABS α v2 and FIX α v2 are binding occurrences and every
occurrence of the symbol α in v2 is bound. An occurrence of asymbol is unbound if it is neither binding nor bound. A well-formed
code value is closed if it has no unbound occurrence of a symbol.

Tree automata We use a tree automaton to specify a propertyof the trees generated by a HORS. A (non-deterministic, topdown) tree automaton on a ranked alphabet Σ is a quadruple
A = (Σ, Q, ∆, q INI ) consisting of• the ranked alphabet Σ;• a finite set Q of states;• a finite set ∆ ⊆ Q × Σ × Q∗ of transition rules such that(q, a, q1 · · · qm ) ∈ ∆ implies m = Σ (a);• a special state q INI ∈ Q called the initial state.

We write q a → q1 · · · qm for a transition rule (q, a, q1 · · · qm ).
The set of Q-labeled trees is given by: r ····= q r1 · · · rm
where q ranges over Q and m ≥ 0. A Σ-labeled ranked tree t issaid to be accepted by A = (Σ, Q, ∆, q INI ) if there exists a (finite)
Q-labeled tree r such that t a∆ q INI J r, where the relation t a∆4

2016/10/1

2. hvi{α} is well-formed and closed for all α ∈ Symbol.

Example 7. Let v :≡ ABS α (ABS β (ABS α (APP α β))) be acode value. It has two binding occurrences of α, one binding occurrence of β, one bound occurrence of α and one bound occurrence of β. This is well-formed and closed. The code value v 0 :≡ABS α (APP α β) is well-formed but not closed since the unique occurrence of β is unbound. The code value v 00 :≡ ABS (APP α β) γ
and v 000 :≡ ABS ’1 ’2 are not well-formed.

3. hviX is well-formed and closed for all X ⊆ Symbol.
Proof. (1 ⇒ 3) If hviX is not well-formed, then v is not wellformed. Assume that hviX is not closed, i.e. it has an unboundoccurrence of var. Let α be the symbol in v occurring at thisposition. Then this occurrence of α is unbound. (3 ⇒ 2) Obvious.
(2 ⇒ 1) If v is not well-formed, then hvi{α} is not well-formed(for any α). Assume that v is not closed. Let α be a symbol which
has an unbound occurrence. Then the corresponding occurrence ofvar in hvi{α} is unbound.


The main obstacles in the static verification of closedness ofgenerated code are (i) the set of code values generated by the
program may be infinite and (ii) the number of symbols occurringin a code value has no a priori bound. We can easily overcome
the first problem by modeling a code generator as a HORS thatgenerates the tree representation of code values. An additional
trick is, however, required to address the second problem. Notethat the set of terminal symbols occurring in a HORS and a tree
automaton must be finite; thus, we need to properly model a codevalue containing an unbounded number of symbols with a finite setof terminals.
An important observation here is that whether an occurrence of
α is bound is completely irrelevant to the usage of other symbols.
Hence, for the purpose of checking if there is an unbound occurrence of α, the code value v :≡ ABS α (APP α (ABS β γ)) has thesame information as hvi{α} ≡ ABS var (APP var (ABS ig ig)),
where var represents the symbol that we currently focus on (that is
α here) and ig represents the other symbols. Note that hvi{α} uses
only a bounded number of symbols; in fact, it is a Σcls -labeled tree,
where Σcls = P ∪ {var 7→ 0, ig 7→ 0}. The notions of wellformedness and closedness are extended to hvi{α} ; we say that a
Σcls -labeled tree is closed if it has no unbound var. Now closedness of v is reduced to that of hvi{α} for every α ∈ Symbol.
We formalize the above idea. Given a code value v and a subset
X ⊆ Symbol, the operation hviX replacing α ∈ X with var andβ∈/ X with ig is defined by:hαiX :≡

varig(if α ∈ X )(otherwise)

It is easy to see that the set of Σcls -labeled trees representing
well-formed and closed code values is a regular tree language. Let
Acls be the automaton that recognizes this language; the definitionof Acls is given in Appendix.
Now what remains is to construct a HORS Gcls (D, S ) for agiven program (D, S ) such that
L(Gcls (D, S )) = {hviX | S ,→D ∗ v, X ⊆ Symbol}.
Given a program (D, S ), we define the HORS Gcls (D, S ) =(Σcls , R, S ) by:
R ··= {F x̃ → hei | (F x̃ = e) ∈ D}
∪ {Gensym k → k var, Gensym k → k ig}
where the transformation h–i of terms into applicative terms of the
HORS is given by:hxi :≡ x,

hF i :≡ F,

hP i :≡ P,

he1 e2 i :≡ he1 i he2 i,hgensym/conti :≡ Gensym.

The HORS Gcls (D, S ) basically simulates the program (D, S )except for gensym/cont. The nonterminal Gensym of the
HORS (that corresponds to gensym/cont) non-deterministicallychooses whether or not the newly generated symbol should belong
to X ⊆ Symbol, and passes var or ig to the continuation accordingly. The enumeration of all the possible behaviours of Gensym
corresponds to that of X ⊆ Symbol in h–iX .

hP iX :≡ P
hv1 v2 iX :≡ hv1 iX hv2 iX .

As discussed above, given a code value v, it is well-formed andclosed if and only if hvi{α} is well-formed and closed for everyα ∈ Symbol. As we shall see in Lemma 9, this is equivalent
to the condition that hviX is well-formed and closed for every
X ⊆ Symbol. (The latter is technically more convenient.)

Example 10. Consider the following variation of the genpower
example in Section 1:

Example 8. Let

letrec genpower_fake n x =if n ≤ 0 then ’1 else
TIMES x (genpower_fake (n − 1) x) inv :≡ ABS α (ABS β (ABS α (APP α β)))be a closed code value. There are essentially four choices of X ⊆Symbol, namely X0 ··= ∅, X1 ··= { α }, X2 ··= { β } and
X3 ··= { α, β }. We have
hviX0 ≡ ABS ig (ABS ig (ABS ig (APP ig ig)))
hviX1 ≡ ABS var (ABS ig (ABS var (APP var ig)))

λn. let x = gensym () inlet y = gensym () in ABS y (genpower_fake n x)
and its corresponding program (D, S ) in the gensym language:
D = {GenPowerFake x = ’1,

hviX2 ≡ ABS ig (ABS var (ABS ig (APP ig var)))

GenPowerFake x = TIMES x (GenPowerFake x),
S = gensym/cont K1 ,hviX3 ≡ ABS var (ABS var (ABS var (APP var var))),all of which are closed. Consider a non-closed code value

K1 x = gensym/cont (K2 x),
K2 x y = ABS y (GenPowerFake x)}.

v 0 :≡ ABS α (APP α β),in which β is unbound. Setting X ··= { β }, we have

Clearly this program can produce a target code that is not closed.
It is transformed to the following HORS consisting of the following rules:

hv 0 iX ≡ ABS ig (APP ig var)in which var is unbound.
Lemma 9. For every code value v, the following conditions areequivalent:

GenPowerFake x → ’1,
GenPowerFake x → TIMES x (GenPowerFake x),

1. v is well-formed and closed.

S → Gensym K1 ,5

2016/10/1

K1 x → Gensym (K2 x),

Given a program (D, S ) of the gensym language, are all thecode values generated by (D, S ) well-typed?

K2 x y → ABS y (GenPowerFake x),
Gensym k → k var, Gensym k → k ig.

Example 13. Consider the following function generating a specialized power function for integers or floating numbers dependingon the value of option:

The HORS generates ABS ig (TIMES var · · ·) if the first rule for
Gensym is chosen in the body of K1 and the second rule is chosen
in the body of K2 . Thus, the HORS is rejected by Acls as expected.
letrec genpower_opt init n x =if n ≤ 0 then init
else TIMES x (genpower_opt init (n − 1) x) in

We prove the correctness of our method below.

λoption. λn. let x = gensym () inif option then genpower_opt ’1 n x

Lemma 11. For every program (D, S ) of the gensym language,
we have
L(Gcls (D, S )) = {hviX | S ,→D ∗ v, X ⊆ Symbol}.

else genpower_opt ’1.0 n x∗This function returns a well-typed code value for every pair ofarguments but this is ill-typed under type systems for multi-stage
languages such as λ [9]. In order to ensure well-typedness ofgenerated code, it suffices to check well-typedness of all codevalues generated by the following program of the gensym language,
which is an abstraction of the above function applied to random
arguments:

Proof sketch. (⊇) Given a reduction sequence S ,→D v anda subset X ⊆ Symbol, we construct a reduction sequence
S −→Gcls (D,S ) ∗ t which simulates the reduction sequence of the
program. A reduction step gensym/cont ê ,→D ê α corresponds to Gensym t −→Gcls (D,S ) t var if α ∈ X and otherwise
Gensym t −→Gcls (D,S ) t ig.
(⊆) Assume a reduction sequence S −→Gcls (D,S ) ∗ t. By using
the bijective correspondence between rewriting rules in Gcls (D, S )and function definitions in (D, S ), we can construct a reduction
sequence S ,→D ∗ v in which gensym/cont does not generate
the same symbol twice. The set X ⊆ Symbol is defined byα ∈ X if and only if gensym/cont ê0 ,→D ê0 α appears in the
reduction sequence and the corresponding rewriting in the HORS
is Gensym t0 −→Gcls (D,S ) t0 var. Then hviX ≡ t.


D ··= {S = gensym/cont (PowerOpt ’1),
S = gensym/cont (PowerOpt ’1.0),
PowerOpt init x = init,
PowerOpt init x = TIMES x (PowerOpt init x)}.
As we shall see, our method automatically proves this.
Let T ⊆fin TgType be a finite subset of types that satisfies

The next theorem is a consequence of Lemmas 9 and 11.

(T1 → T2 ) ∈ T

Theorem 12. Let (D, S ) be a source program of the gensym
language. Then the following are equivalent:(1) All code values generated by (D, S ) are well-formed andclosed.
(2) L(Gcls (D, S )) is accepted by Acls .
3.3⇒{T1 , T2 } ⊆ T .

We call an element of T a candidate type. Our method is paramaterized by T and checks whether a code value v has a type derivationthat uses only types in T . Let us fix T in the rest of this section.
Let v be a code value of which we would like to check welltypedness. Similarly to the idea in the previous subsection, we
replace symbols in v with some elements of a finite set in sucha way that the resulting tree has enough information to check thewell-typedness of v. The key observation is that, once closednessof v has been established, it is sufficient to know the type of eachsymbol to check well-typedness. Let varT be a tree constructor ofarity 0 for each T ∈ T . Given a map θ : Symbol → T , weT
define [v]Tθ as the Σwt-labelled tree obtained by replacing α in v
to varθ(α) . The resulting trees are (P ∪ {varT 7→ 0 | T ∈ T })labelled trees.
We then give a type system for (P ∪ {varT 7→ 0 | T ∈ T })labelled trees as follows.

Verifying well-typedness of generated code

This section presents a method for checking that all the codevalues that can be generated by a given program are simply-typed.
The set TgType of types of generated code fragments, ranged
over by T , is defined by:
T ····= Int | Float | Bool | T → T.
We assume every code constructor P in P (except ABS and FIX) is
associated with a set of types:
P type : (dom(P) \ {ABS, FIX}) → 2TgType .
For example,
P type (APP) ··= {(T1 → T2 ) → T1 → T2 | (T1 → T2 ) ∈ TgType}

varT : T

P type (IFTE) ··= {Bool → T → T → T | T ∈ TgType}(T1 → · · · → Tn → T ) ∈ P type (P )t1 : T1 · · · tn : Tn T ∈ T
P t1 · · · tn : T

v : T2(T1 → T2 ) ∈ T
ABS varT1 v : T1 → T2

P type (TIMES) ··= {Int → Int → Int, Float → Float → Float}.

Note that each constant may have more than one type. A code value
v is well-typed (and has type T ) if ∅ ` v : T is derivable using therule for constants:

v : T1 → T2
FIX varT1 →T2 v : T1 → T2∅`P :T

Thanks to the conditions T ∈ T and (T1 → T2 ) ∈ T in the second
and third rules, v : T implies T ∈ T . Since T is a finite set, one
can construct an automaton that recognizes the set of all well-typed(P ∪ {varT 7→ 0 | T ∈ T })-labelled trees. We write WT for thisregular tree language.

and the standard typing rules for the simply-typed λ-calculus andrecursion.
The problem that we address in this section is as follows:

Lemma 14. Let v be a well-formed and closed code value. If there
exists θ : Symbol → T such that [v]Tθ ∈ WT , then v is welltyped.

(T ∈ P type (P ))62016/10/1

Example 15. Let v :≡ ABS α (ABS β (IFTE α β ’1)) and assume
that P type (’1) = {Int}. For a map θ such that θ(α) ≡ Float andθ(β ) ≡ Bool, we have[v]Tθguesses a correct type for the newly generated symbol. The next
lemma shows that the HORS generates an expected tree language.
T
Lemma 17. For every v ∈ C (D, S ), there exists t ∈ L(Gwt(D, S ))
such that v ∼ t.

≡ ABS varFloat (ABS varBool (IFTE varFloat varBool ’1)),

which is not well-typed. For a map θ0 such that θ0 (α) ≡ Bool andθ0 (β ) ≡ Int, we have

Proof sketch. First we extend [–]Tθ to expressions and k–k to applicative terms. For an expression ê and an applicative term t (thatis not necessarily a tree), the relation ê ∼ t is defined by the obvious way. The claim extended to arbitrary expressions and applicative terms can be proved by induction on the length of reduction
sequences.
[v]Tθ0 = ABS varBool (ABS varInt (IFTE varBool varInt ’1)),
which has type Bool → Int → Int. Hence v has the same type andin particular well-typed.

Now the following proposition is a sufficient condition for thewell-typedness of all the code values generated by (D, S ):As a consequence of Lemmas 14, 16 and 17, we have thefollowing theorem.

∀v ∈ C (D, S ). ∃θ : Symbol → T . [v]Tθ ∈ WT .

Theorem 18 (Soundness). Let (D, S ) be a program of the gensym language generating well-formed and closed code values. If
T
L(Gwt(D, S )) is accepted by ATwt , then all code values generatedby (D, S ) are well-typed.

We reduce this proposition to higher-order model checking. An
important difference from the problem in Section 3.2 is that wehave to handle the existential quantification. (Recall that higherorder model checking is a problem to decide if every value treesatisfies a certain property.)
We embed all possible choices of θ into a tree by the following
technique. Let

T
Note that whether L(Gwt(D, S )) is accepted by ATwt is an
instance of higher-order model checking and thus decidable.
Unfortunately, our method is incomplete, as discussed below.
The first source of incompleteness comes from the choice of T ,which must be finite to keep WT regular. There is a program of thegensym language such that every generated code value has a typebut the set of all types of the generated code values are infinite. An
example is the program (D, S ) defined by:TΣwt··= P ∪ {varT 7→ 0 | T ∈ T } ∪ {oneof 7→ #T }where #T is the number of elements in T . The tree constructor
oneof means that at least one child should be well-typed. Hence it
has the typing rule

D ··= {S = ’1, S = gensym/cont T, T x = ABS x S}

ti : T for some i ∈ [n]oneof t1 · · · tn : T

which generates a code value λα1 . . . . λα` . 1 (written in thestandard syntax) for every ` ∈ N.
The second source of incompleteness comes from the fact that
we assign a type to each symbol. Consider a code value

T
Again well-typedness of Σwt-labelled trees is a regular property.
T
We write Awt for an automaton that recognizes the language; aconstruction of ATwt is given in Appendix.
T
T
A Σwt
-labelled tree can be seen as a set of (Σwt
\ {oneof})labelled tree. We write ktk for the set of trees defined by:koneof t1 · · · tn k ··=[v :≡ ABS α (APP α (ABS α (TIMES α ’1))),
which can be written in the standard syntax as λα. α (λα. α ∗1). This code value is well-typed: an example of a correct type
annotation is:

kti k,λα(Int→Int)→Int . α (λαInt . α ∗ 1).

i∈[n]

kP t1 · · · t` k ··= {P u1 · · · u` | ∀i ∈ [`]. ui ∈ kti k}.

Observe that different occurrences of α have different types. This isinevitable to type v. Hence all elements of {[v]Tθ | θ : Symbol → T }are ill-typed, whatever T is.

The next lemma justifies the intuition that oneof describes anexistential quantification.

Remark 19. The method above can be extended to intersection
types and/or refinement types, as long as the set T of type candidates is finite. For example, with intersection types, the first two
rules for typing labeled trees would become:T
Lemma 16. A Σwt-labelled tree t is accepted by ATwt if and only∃
if u ∈ ktk. u ∈ WT .
T
For a code value v and a Σwt-labelled tree t, we write v ∼ t if
ktk = {[v]Tθ | θ : Symbol → T }. Provided that v ∼ t, then by
Lemmas 14 and 16, a code value v is well-typed if t is accepted by
ATwt .
T
Given a program (D, S ), we define a HORS Gwt(D, S ) =T(Σwt , R, S) such that, for every v ∈ C (D, S ), there exists t ∈T
L(Gwt(D, S )) such that v ∼ t. The rewriting rules are definedby:varT1 ∧···∧Tk : Ti
(T1,1 ∧ · · · ∧ T1,k1 ) → · · · → (Tn,1 ∧ · · · ∧ Tn,kn ) → T∈ P type (P ) ∩ T
ti : Ti,j for each i ∈ [n], j ∈ [ki ]P t1 · · · tn : T

R ··= {F x̃ → hei | (F x̃ = e) ∈ D}
∪ {Gensym k → oneof (k varT1 ) · · · (k varTn )},As long as T , the above rules can be expressed as transition rules ofan alternating tree automaton. (The observation that the typability
in intersection types can be captured by a tree automaton is notnovel; see, e.g., [25].) Using intersection types and/or refinement
types, we can check more complex properties of generated code.

where T1 , . . . , Tn is an enumeration of T . The operation hei isdefined in Section 3.2, which replaces gensym/cont in e toT
Gensym. The HORS Gwt(D, S ) basically simulates the programD,
S
exceptfor
gensym/cont.
The nonterminal Gensym()

7

2016/10/1

Program
genpower
genpower_fake
genpower_option

effgenpower

geniprod

gentranspose

#T
2
10
16
2
4
10
16
2
10
16
4
10
16
5
10
16

Answer
C
WT
Yes

Yes

No

–

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

5.

Time [s]C
WT
0.004
0.004 0.012
0.016
0.004
–
0.008
0.004 0.014
0.098
0.006
0.004 0.025
0.032
0.008
0.008 0.018
0.069
0.012
0.008 0.022
0.091

Since it may be cumbersome to write code generators in the gensym language in Section 2, we introduce in this section a two-stage
programming language called Relaxed λ and formalize a translation to (a variant of) the gensym language. Our two-stage programming language lies somewhere between the untyped multi-stage
language λU [29] and the typed multi-stage language λ [9]. It
has only quasiquotation and unquote as constructs for staging (likeλ ). Typing is more relaxed, however, than λ proper in that it
is applied only for stage 0; the types of terms at the next stage
are collapsed to a single type code. The translation is essentiallythe one presented in Calcagno et al. [4]1 , who study compilationfrom λU [29] to a single-stage language with a special datatype
for ASTs, gensym, and reflection. We show that the translation
preserves typing, which is not studied in [4] (because the source
language is untyped). This property is important for our verification methods to be applicable to Relaxed λ . We do not discuss indetail another important property that the translation preserves semantics but it should straightforwardly be adapted from the resultsin [4].
The sets of terms and types, ranged over by M and τ respectively, are defined by:

Table 1. The Result of Preliminary Experiments

4.

Verification of Two-Stage Programs

Experiments

M ····= c(M, . . . , M ) | x | M M | λx. M | fix x. λx. M| if M then M else M | M | ˜M ,
τ ····= int | float | bool | code | τ → τ.

Based on the verification methods described in Section 3, we have
implemented a prototype verification tool for code generators andcarried out preliminary experiments. The tool supports a call-byvalue language with OCaml-like syntax and the gensym primitive.
A source program is converted to a program in Section 2 by replacing all the conditionals with non-deterministic branches; we havenot integrated predicate abstraction yet and applying the CPS transformation. The program is then transformed to HORS, based on thetransformations described in Sections 3.2 and 3.3. H OR S AT 2 [2] isused as the backend higher-order model checker.
We have tested the tool on a machine with an Intel Core-i5 CPUwith 2.60GHz and 4.00GB memory. The result is shown in Table 1,
where “C” and “WT” mean the closedness check and the welltypedness check, respectively, and the column “#T ” shows thenumber of types considered as candidates of the types of generated
symbols in the well-typedness check. The benchmark programs
used in the experiments are the following ones:

Here, c and x range over the sets of constants (such as integers,
booleans, and primitive operations on them) and variables, respectively. The expression c(M1 , . . . , Mm ) applies the m-ary
constant c to arguments M1 , . . . , Mm . We often write c for c().
When c = ⊕ is binary, we sometimes use the infix notation andwrite M1 ⊕ M2 for ⊕(M1 , M2 ). The term M corresponds toquasiquote in Lisp and represents (quoted) code of M ; the term
˜M —which should appear inside quasiquotation—escapes fromthe quote, evaluates M , and embeds the value of M , which is expected to be a code value, into the surrounding quotation. We omit
the operational semantics, which we assume to be call-by-value, as
it is basically the same as that of λU [4, 29].
Example 20. The program in Example 1 can be written in Relaxed
λ as follows:

genpower: a function that takes a nonnegative integer n and returns code for λx. xn , described in Section 1 and Example 1.
genpower_fake: a buggy version of genpower, which is described in Example 10.

letrec power n x =genpower_option: an extended version of genpower, which isshown in Example 13.

λn. λx. ˜(power n x )if n = 0 then 1 else ˜x ∗˜(power (n − 1) x) in
where letrec x0 x1 · · · x` = M1 in M2 is a shorthand for(λx0 . M2 ) (fix x0 . λx1 . · · · λx` . M1 ).
effgenpower: a variant of genpower, which generates code for afunction that takes an integer x as an input and computes xn intime O(log n).

We present a type system for Relaxed λ . As we mentioned,
we will restrict the set of stages to {0, 1}. The type judgmentsΓ `0 M : τ for stage 0 and Γ `1 M :for stage 1 are defined
as follows:

geniprod: a function that takes a nonnegative integer n and returns code that takes a couple of n-dimentional vectors u, v
(represented by lists of length n) as inputs and computes theinner product u>v.

(C (c) = τ1 → · · · → τm → τ )gentranspose: a function that takes nonnegative integers m, n
and returns code that transposes matrices of size m × n.

Γ `0 Mi : τi for each i ∈ [m]Γ `0 c(M1 , . . . , Mm ) : τ

Here, the types of code values have been extended with list types:
T ····= · · · | T List, and we have added code costructors forlists: (NIL 7→ 0), (CONS 7→ 2), (CAR 7→ 1), (CDR 7→ 1) ∈ P.
The benchmark programs are available at http://www-kb.is.s.
u-tokyo.ac.jp/~suwa/benchmark1.zip.
For all the programs, the tool terminated quickly and output
expected answers.

(Γ (x) = τ )Γ `0 x : τΓ `0 M1 : τ1 → τ2
Γ `0 M2 : τ1
Γ `0 M1 M2 : τ2

1 in fact, a degenerated case of theirs

8

2016/10/1

Γ [x 7→ τ1 ] `0 M : τ2
Γ `0 λx. M : τ1 → τ2

Note that type environments for Relaxed λ possibly map a variable to the symbol , while those for the intermediate language donot. The translation b–ciΨ of Relaxed λ to the intermediate language with a map Ψ from variables to the set {0, 1} of stages isdefined by:Γ [x 7→ τ ] `0 M : τΓ `0 fix x. M : τΓ `0 M0 : boolΓ `0 M1 : τΓ `0 M2 : τΓ `0 if M0 then M1 else M2 : τbc(M1 , . . . , Mm )c0Ψ :≡ c bM1 c0Ψ · · · bMm c0Ψ ,bxc0Ψ :≡ x

10

Γ ` M:
Γ `0 M : codeΓ ` M : codeΓ `1 ˜M :(C (c) = τ1 → · · · → τm → τ ) Γ `1 Mi :for each i ∈ [m]1Γ ` c(M1 , . . . , Mm ) :(Γ (x) =Γ `1 M1 :Γ `1 M2 :1Γ ` M1 M2 :)1

Γ ` x:

Γ [x 7→ ] `1 M :Γ `1 λx. M :Γ [x 7→ ] `1 M :Γ `1 fix x. M :Γ `1 M0 :Γ `1 M1 :Γ `1 M2 :Γ `1 if M0 then M1 else M2 :Here, C maps each constant to its type. In Relaxed λ , terms are
simply-typed at stage 0, while only the occurrence of variables iscontrolled by types at stage 1.
The target language of the translation is actually an intermediate
language, which was already used in Examples 1 and 10, between
Relaxed λ and the gensym language. We first set PC to be themap defined by:Here, we write let x = M1 in M2 as a shorthand for (λx. M2 ) M1 .
Example 21. The program in Example 20 is translated as follows:
bfix power. λn. λx. if n = 0 then 1 else . . .c0∅

PC ··= {’c 7→ m | C (c) ≡ τ1 → · · · → τm → τ }≡ fix power. λn. λx. if n = 0 then b 1 c0Ψ1 elseb (˜x) ∗˜(power (n − 1) x) c0Ψ1∪ {APP 7→ 2, ABS 7→ 2, FIX 7→ 2, IFTE 7→ 3}.
For example, if C (+) ≡ int → int → int, then PC (’+) = 2.
The set of terms, ranged over by N , is defined by:≡ fix power. λn. λx. if n = 0 then ’1 else
TIMES b˜xc1Ψ1 b˜(power (n − 1) x)c1Ψ1

N ····= c | x | N N | λx. N | fix x. N

≡ fix power. λn. λx. if n = 0 then ’1 else
TIMES x (power (n − 1) x)| if N then N else N | P | gensym ()where c and P range over the set of constants and dom(PC ),respectively. The type judgment Γ `m N : τ for the intermediate
language is defined by the following typing rules:(C (c) = τ )(Γ (x) = τ )Γ `m c : τΓ `m x : τ

if Ψ (x) = 0,

bM1 M2 c0Ψ :≡ bM1 c0Ψ bM2 c0Ψ ,bλx. M c0Ψ :≡ λx. bM c0Ψ [x7→0] ,bfix x. M c0Ψ :≡ fix x. bM c0Ψ [x7→0] ,bif M0 then M1 else M2 c0Ψ :≡if bM0 c0Ψ then bM1 c0Ψ else bM2 c0Ψ ,b M c0Ψ :≡ bM c1Ψ ,bc(M1 , . . . , Mm )c1Ψ :≡ ’c bM1 c1Ψ · · · bMm c1Ψ ,bxc1Ψ :≡ x
if Ψ (x) = 1,
bM1 M2 c1Ψ :≡ APP bM1 c1Ψ bM2 c1Ψ ,bλx. M c1Ψ :≡let x = gensym () in ABS x bM c1Ψ [x7→1] ,bfix x. M c1Ψ :≡let x = gensym () in FIX x bM c1Ψ [x7→1] ,bif M0 then M1 else M2 c1Ψ :≡ IFTE bM0 c1Ψ bM1 c1Ψ bM2 c1Ψ ,b˜M c1Ψ :≡ bM c0Ψ .

where Ψ1 ··= {power 7→ 0, n 7→ 0, x 7→ 0}, and:bλn. λx. ˜(power n x ) c0{power7→0}≡ λn. let x = gensym () inb˜(power n x )c1{power7→0,n7→0,x7→1}≡ λn. let x = gensym () in power n x .

Γ `m N1 : τ1 → τ2
Γ `m N2 : τ1
Γ `m N1 N2 : τ2
Γ [x 7→ τ1 ] `m N : τ2
Γ `m λx. N : τ1 → τ2

The following theorem asserts the validity of the translation:
Theorem 22. Let Γ be a type environment, M be a term and τ bea type of Relaxed λ . Then the following hold:Γ [x 7→ τ ] `m N : τΓ `m fix x. N : τ(1) If Γ `0 M : τ , then bΓ c `m bM c0ΨΓ : τ .
(2) If Γ `1 M :Γ `m N0 : boolΓ `m N1 : τΓ `m N2 : τΓ `m if N0 then N1 else N2 : τ, then bΓ c `m bM c1ΨΓ : code.

where, for a type environment Γ , the map ΨΓ : dom(Γ ) → {0, 1}
and the type environment bΓ c are defined by:ΨΓ (x) ··=Γ `m P : code
→ · ·{z· → code →|} codeP C (P )10(if Γ (x) ≡(otherwise) ,)bΓ c(x) ··=codeΓ (x )(if Γ (x) ≡(otherwise) .

Thanks to the theorem above, we can apply the verification methods proposed in Section 3 to programs written in Relaxed λ ; notethat well-typed programs of the intermediate language can be trans-Γ `m gensym () : code9

2016/10/1)

lated to those of the gensym language of Section 2. The proof of
Theorem 22 is given in Appendix.

6.

In their translation, a code value is represented by a function fromthe values of its free variables to the execution result of the code.
So, syntactic information is lost. In fact, they assume a certain typesystem similar to [13], which can check well-typedness of generated code and translation is type-based. In some sense, their focus
is more on semantic properties of generated code. Rather, our technique is closer to string analysis such as [19] in the sense that data
structures to be generated by a program are checked against a grammar. Our technique is more powerful than grammar-based string
analysis because of the use of more powerful grammars, namely
higher-order recursion schemes; indeed, we can extend our technique to checking more semantic properties as well, by encoding amore refined type system such as an intersection type system into atree automaton (recall Remark 19 at the end of Section 3).
Other frameworks for verification of multi-stage languages
have been also studied. Berger and Tratt [1] have developed aHoare logic for a variant of MiniMLe [10]; Concoqtion [11] andΩmega [27] have introduced very expressive type systems withindexed types into multi-stage languages. Although they can also
verify complex semantic properties of code generators, they require
a lot of human assistance to verify.
Our translation from the staged language to the gensym language is very similar to the compilation scheme for multi-stage languages [4], where code values are represented by a special datatype
for ASTs. Our setting is much simpler because we do not deal witheval and cross-stage persistence.

Discussions

We discuss limitations of our approach in Section 6.1 and related
work in Section 6.2.
6.1

Limitations

There are some fundamental limitations of our approach that comefrom the use of higher-order model checking. The first limitationis that the gensym language must be simply-typed; this is due tothe limitation of higher-order model checking that models (calledhigher-order recursion schemes) must be simply typed in order forthe model checking problem to be decidable. There are a few ways
to relax the restriction, however. First, the let-polymorphism (without polymorphic recursion) can be allowed in the gensym language,
because programs can be converted to simply-typed programs by
inlining all the let-definitions. Second, a certain class of recursive data structures (like lists) can be encoded as functions [26].
Third, if we give up the decidability, we can replace higher-ordermodel checking with µHORS model checking [16], an extensionof higher-order model checking with recursive types.
Another limitation of our approach is that we cannot support
the so-called Run primitive, the primitive for running target codeat the current stage. With the run primitive, for example, we could
express the following computation:

6.2.2(run (let x = gensym () in ABS x (genpower 2 x))) 3∗

Model checking of HORS and its application to program verification has been studied extensively [14, 15, 17, 18, 21, 22]. Verification of higher-order tree transducers studied by Kobayashi, Unno,
and Tabuchi [18] is closely related to the present work in that it isa technique to verify the shape of trees output by a certain class offunctional programs. One notable difference is that our work deals
with binding structure in output trees. Kobayashi [14] showed reduction of the resource usage problem [12] to higher-order model
checking. The way how multiple variable are treated in this work
has been inspired by his method (which itself was inspired by [7])to track the usages of mulitiple resources. As already mentioned
above, we can use techniques for higher-order model checking torefine our analysis.

→ (run (ABS X (TIMES X (TIMES X ’1)))) 3∗→ (λx. x ∗ (x ∗ 1)) 3 → 9
where genpower is the function defined in Section 1. The lackof the run-primitive comes from the limitation of higher-ordermodel checking that trees cannot be deconstructed in higher-orderrecursion schemes. One way to remedy the problem would be to use
EHMTT verification methods [34], instead of higher-order model
checking.
6.2
6.2.1

Higher-order model checking

Related WorkMulti-stage programming

Since the seminal work by Davies and Pfenning [10], a lot oftype systems for safe dynamic code generation have been studied [3, 5, 8, 13, 20, 30–33, 36]. Although they differ in the choicesof language primitives for code generation (and, in some cases, execution), most of them aim at checking validity of generated codewhen the code generator is typechecked2 . As the line of those studies shows, it is not very easy to design a type system that is both
flexible and safe. Also, the property we would like to check is hardcoded into the type system. With our approach, code values are
given a single type, which gives much flexibility, and properties
to check are not hard-coded. We can also make good use of standard techniques for model checking such as predicate abstraction.
One drawback of our approach would be the lack of modularity:
the whole code generator has to be available to check its property,
whereas type systems usually allow for separate checking (if thetypes of free variables are given).
Static analysis for multi-stage languages has been studied by
Choi et al. [6]. They give a translation from a multi-stage language
to an ordinary, single-stage language, where their semantics correspondence enables static analysis on a multi-stage program by analyzing the translated program by standard abstract interpretation.

7.

Conclusion

We have proposed an automated method for verifying code generators written in a gensym language, based on higher-order model
checking. Our method can check that all the generated code values
are closed and well-typed, while maintaining the flexibility of programming in the gensym language. We have implemented a prototype verification tool based on the proposed method. We have also
designed a two-stage programming language and a translation to
the gensym language, so that our verification method can also be
applied to two-stage programs.

References[1] M. Berger and L. Tratt. Program logics for homogeneous generative
run-time meta-programming. Logical Methods in Computer Science,
11(1), 2015.
[2] C. H. Broadbent and N. Kobayashi. Saturation-based model checkingof higher-order recursion schemes. In Proceedings of CSL 2013,
volume 23 of LIPIcs, pages 129–148, 2013.
[3] C. Calcagno, E. Moggi, and T. Sheard. Closed types for a safe
imperative MetaML. J. Funct. Program., 13(3):545–571, May 2003.

2 One notable exception is Shields et al.[28], in which typechecking of[4] C. Calcagno, W. Taha, L. Huang, and X. Leroy. Implementing multistage languages using ASTs, gensym, and reflection. In International

generated code is deferred until the execution of the generated code starts.

10

2016/10/1

[27] T. Sheard and N. Linger. Programming in Ωmega. In Central European Functional Programming School, Second Summer School, CEFP
2007, pages 158–227, 2007.
[28] M. Shields, T. Sheard, and S. L. Peyton Jones. Dynamic typing asstaged type inference. In Proc.ACM SIGPLAN/SIGACT Symposiumon Principles of Programming Languages (POPL’98), pages 289–302,
1998.
[29] W. Taha. A sound reduction semantics for untyped CBN multistage computation. Or, the theory of MetaML is non-trivial. In
Proc.Proceedings of Workshop on Partial Evaluation and Program
Manipulation (PEPM2000), 2000.
[30] W. Taha, Z. E.-A. Benaissa, and T. Sheard. Multi-stage programming:
Axiomatization and type-safety. In Proc.25th International Colloquium on Automata, Languages and Programming (ICALP’98), volume 1443 of LNCS, pages 918–929, Aalborg, Denmark, July 1998.
Springer.
[31] W. Taha and M. F. Nielsen. Environment classifiers. In ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages(POPL’03), pages 26–37, 2003.
[32] W. Taha and T. Sheard. Multi-stage programming with explicit annotations. In Proceedings of Workshop on Partial Evaluation and Program
Manipulation (PEPM’97), pages 203–217, Amsterdam, Netherlands,
1997.
[33] T. Tsukada and A. Igarashi. A logical foundation for environment
classifiers. Logical Methods in Computer Science, 6(4:8):1–43, Dec.
2010.
[34] H. Unno, N. Tabuchi, and N. Kobayashi. Verification of treeprocessing programs via higher-order model checking. In Proceedings of APLAS 2010, volume 6461 of LNCS, pages 312–327. Springer,
2010.
[35] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Info. Comput., 115(1):38–94, 1994.
[36] Y. Yuse and A. Igarashi. A modal type system for multi-level generating extensions with persistent code. In Proc.8th ACM SIGPLAN
Symposium on Principles and Practice of Declarative Programming(PPDP’06), pages 201–212, Venice, Italy, July 2006.

Conference on Generative Programming and Component Engineering, pages 57–76, 2003.
[5] C. Chen and H. Xi. Meta-programming through typeful code representation. In Proc. of ICFP, pages 275–286, 2003.
[6] W. Choi, B. Aktemur, K. Yi, and M. Tatsuta. Static analysis of multistaged programs via unstaging translation. In ACM SIGPLAN/SIGACT
Symposium on Principles of Programming Languages, pages 81–92,
Jan. 2011.
[7] B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi.
Proving that programs eventually do something good. In Proc. of
POPL, pages 265–276. ACM Press, 2007.
[8] R. Davies. A temporal-logic approach to binding-time analysis. In
IEEE Symposium on Logic in Computer Science (LICS’96), pages
184–195, July 1996.
[9] R. Davies. A temporal-logic approach to binding-time analysis. In
Proceedings, 11th Annual IEEE Symposium on Logic in Computer
Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages
184–195. IEEE Computer Society, 1996.
[10] R. Davies and F. Pfenning. A modal analysis of staged computation.
JACM, 48(3):555–604, 2001.
[11] S. Fogarty, E. Pasalic, J. Siek, and W. Taha. Concoqtion: Indexed
types now! In Proc.Proceedings of Workshop on Partial Evaluation
and Program Manipulation (PEPM2007), pages 112–121, 2007.
[12] A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Trans.
Prog. Lang. Syst., 27(2):264–313, 2005.
[13] I.-S. Kim, K. Yi, and C. Calcagno. A polymorphic modal type system
for lisp-like multi-staged languages. In ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL’06), pages
257–269, Jan. 2006.
[14] N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proc. of POPL, pages 416–428.
ACM Press, 2009.
[15] N. Kobayashi. Model checking higher-order programs. Journal of theACM, 60(3), 2013.
[16] N. Kobayashi and A. Igarashi. Model checking higher-order programswith recursive types. In Proceedings of ESOP 2013, volume 7792 of
LNCS. Springer, 2013.
[17] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In Proc. of PLDI, pages 222–
233. ACM Press, 2011.
[18] N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multiparameter tree transducers and recursion schemes for program verification. In Proc. of POPL, pages 495–508. ACM Press, 2010.
[19] Y. Minamide. Static approximation of dynamically generated WWW
pages. In Proc.International Conference on World Wide Web, pages
432–441, 2005.
[20] A. Nanevski and F. Pfenning. Staged computation with names andnecessity. J. Funct. Program., 15(5):893–939, 2005.
[21] C.-H. L. Ong. On model-checking trees generated by higher-orderrecursion schemes. In LICS 2006, pages 81–90. IEEE Computer
Society Press, 2006.
[22] C.-H. L. Ong and S. Ramsay. Verifying higher-order programs withpattern-matching algebraic data types. In Proc. of POPL, pages 587–
598. ACM Press, 2011.
[23] B. C. Pierce. Types and Programming Languages. The MIT Press,
2002.
[24] S. Ramsay, R. Neatherway, and C.-H. L. Ong. An abstraction refinement approach to higher-order model checking. In Proceedings of
POPL 2014, 2014.
[25] J. Rehof and P. Urzyczyn. Finite combinatory logic with intersection
types. In Typed Lambda Calculi and Applications - 10th International
Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690, pages 169–183. Springer, 2011.
[26] R. Sato, H. Unno, and N. Kobayashi. Towards a scalable softwaremodel checker for higher-order programs. In Proceedings of PEPM
2013, pages 53–62. ACM Press, 2013.

11

2016/10/1

• The case M ≡ M1 M2 : assume Γ `0 M1 M2 : τ holds. By the

Appendixderivation rules we have Γ `0 M1 : τ1 → τ and Γ `0 M2 : τ1
for some τ1 . Then by IH we can derive:

Proof of Theorem 2
Lemma 23. Let Γ be a type environment, ê be a term, and C be anevaluation context. Then we have Γ ` C[ê] : code if and only ifΓ ` ê : code.
Proof. By straightforward induction on the structure of C.

bΓ c `m bM1 c0ΨΓ : τ1 → τbΓ c `mbΓ c `m APP :code → code → codebM1 c1ΨΓ : codebΓ c `m APP bM1 c1ΨΓ : code → code

Proof. By straightforward induction on the derivation of Γ [x 7→τA ] ` eB : τB . Intuitively we can deduce Γ ` [êA /x]eB : τB
by replacing every leaf of the form Γ [x 7→ τA ] ` x : τA in thederivation tree of Γ [x 7→ τA ] ` eB : τB with the derivation treeof Γ ` êA : τA .
.

bΓ c `mbM2 c1ΨΓ : codebΓ c `m APP bM1 c1ΨΓ bM2 c1ΨΓ : codei.e. we have bΓ c `m bM c1ΨΓ : code.

Lemma 25. If Γ ` v : code, then ∅ ` v : code.

• The case M ≡ λx. M 0 : assume Γ `0 λx. M 0 : τ holds.

By the derivation rules, τ is of the form τ1 → τ2 and satisfies
Γ [x 7→ τ1 ] `0 M 0 : τ2 . Since bΓ [x 7→ τ1 ]c = bΓ c[x 7→ τ1 ]and ΨΓ [x7→τ1 ] = ΨΓ [x 7→ 0], by IH we can derive:Proof of Theorem 2. It is proved in two steps (namely, by showing
Preservation and Progress [23, 35]). We first show that, if Γ `ê : τ and ê ,→D ê0 , then Γ ` ê : τ . Second, we show that ifΓ ` ê : τ , then either (i) ê is a value and ∅ ` ê : code; or (ii)there exists a run-time term ê0 such that ê ,→D ê0 .
The first property is proved by induction on the definition of,→D , it suffices for us to consider the following two cases:• The case (F x1 · · · x` = e) ∈ D, êA ≡ C F ê1 · · · ê`[:τ

On the other hand, assume Γ `1 M1 M2 : . By the derivation
rules we have Γ `1 M1 :and Γ `1 M2 : , and by IH we
can derive:

Lemma 24. Let Γ be a type environment, êA be an applicative
term, eB be a run-time term, and τA , τB be types. If Γ ` êA : τAand Γ [x 7→ τA ] ` eB : τB , then Γ ` [êA /x]eB : τB

Proof. By induction on Γ ` v : code.

bΓ c `m bM2 c0ΨΓ : τ1bΓ c `m bM c0ΨΓbΓ c[x 7→ τ1 ] `m bM 0 c0ΨΓ [x7→0] : τ2bΓ c `m λx. bM 0 c0ΨΓ : τ1 → τ2
i.e. we have bΓ c `m bM c0ΨΓ : τ . On the other hand, if we haveΓ `1 λx. M 0 : , by the derivation rules Γ [x 7→ ] `1 M 0 :holds. Since we have bΓ [x 7→ ]c = bΓ c[x 7→ code] andΨΓ [x7→ ] = ΨΓ [x 7→ 1], by IH bΓ c `m bM c1ΨΓ : code can bederived; its derivation is shown in Figure 7.

]

and êB ≡ C[[ê` /x` ] · · · [ê1 /x1 ]e]: since (D, S ) is simplytyped by the definition of the gensym language, there exist types
τ1 , . . . , τ` such that Γ [x1 7→ τ1 ] · · · [x` 7→ τ` ] ` e : code andΓ (F ) = τ1 → · · · → τ` → code. By Lemma 23 we have Γ `F ê1 · · · ê` : code, and considering the derivation of it we haveΓ ` êi : τi for each i ∈ [`]. Thus, by repeated application ofLemma 24, we have Γ ` [ê` /x` ] · · · [ê1 /x1 ]e : code. Again
by Lemma 23 we have Γ ` C[[ê` /x` ] · · · [ê1 /x1 ]e] : code.

• The case M ≡ fix x. M 0 : if we have Γ `0 fix x. M 0 : τ , thenby the derivation rules Γ [x 7→ τ ] `0 M 0 : τ holds. Similarly
to the previous case, by IH we can derive:bΓ c[x 7→ τ ] `m bM 0 c0ΨΓ [x7→0] : τbΓ c `m fix x. bM 0 c0ΨΓ : τ• The case êA ≡ C gensym/cont ê

[] and êB ≡ C[ê α]:
by Lemma 23 we have Γ ` gensym/cont ê : code, andconsidering the derivation for it Γ ` ê : code → code holds.
Therefore, we can derive Γ ` ê α : code, and by Lemma 23
we have Γ ` C[ê α] : code.

.

The subcase for Γ `1 fix x. M 0 : τ is also similar to theprevious case.
• The case where M ≡ if M0 then M1 else M2 is easy.
• The case M ≡ M 0 : assume Γ `0 M 0 : τ . Then τ ≡ codeand Γ `1 M 0 :hold by the derivation rules, and by IH wehave bΓ c `m bM 0 c1ΨΓ : code. Since bM 0 c1ΨΓ ≡ b M 0 c0ΨΓ ≡bM c0ΨΓ , we have bΓ c `m bM c0ΨΓ : code.

The second property is shown by induction on Γ ` ê : code,using Lemma 25.
Proof of Theorem 22• The case M ≡ ˜M 0 : assume Γ `1 ˜M 0 :. Then Γ `0 M 0 :code holds by the derivation rules, and by IH we have bΓ c `m
bM 0 c0ΨΓ : code. Since bM 0 c0ΨΓ ≡ b˜M 0 c1ΨΓ ≡ bM c1ΨΓ , wehave bΓ c `m bM c1ΨΓ : code.

Proof. We show (1) and (2) at the same time by induction on the
structure of M .
• The case where M ≡ x is trivial.
• The case M ≡ c(M1 , . . . , Mm ): assume Γ `0 M : τ . By
the derivation rules we have C (c) = τ1 → · · · → τm → τand Γ `0 Mi : τi for each i ∈ [m]. Then by IH we havebΓ c `m bMi c0ΨΓ : τ for each i ∈ [m], and by bΓ c `m c : C (c)
The definition of the automaton Acls

we can derive bΓ c `m c bM1 c0ΨΓ · · · bMm c0ΨΓ : τ . On theother hand, assume Γ `1 M : , then by the derivation rules
we have Γ `1 Mi :for each i ∈ [m], and by IH we havebΓ c `m bMi c1ΨΓ : code for each i ∈ [m]. By the assumptionm = PC (’c) and bΓ c `m ’c : code
→ · ·{z· → code →} code,|INIThe automaton Acls = (Σcls , Qcls , ∆cls , qcls
) for the wellformedness and closedness check is defined as follows.

Qcls ··= {q0 , q1 , q var , q ig },INI
qcls··= q0 ,m

we can derive bΓ c `m ’c bM1 c1ΨΓ · · · bMm c1ΨΓ : code.

∆cls ··= {12

q1 var → ε,2016/10/1

bΓ c[x 7→ code] `mbΓ c[x 7→ code] `mbΓ c[x 7→ code] `m
ABS : code → code → codex : codebM 0 c1ΨΓ [x7→1] : codebΓ c[x 7→ code] `m ABS x : code → codebΓ c[x 7→ code] `m ABS x bM 0 c1ΨΓ [x7→1] : codebΓ c `m λx. ABS x bM 0 c1ΨΓ : code → codebΓ c `m gensym () : codebΓ c `m (λx. ABS x bM 0 c1ΨΓ ) gensym () : code
Figure 1. The derivation for bΓ c `m bλx. M 0 c1ΨΓ : code in the proof of Theorem 22
q0 ig → ε,q0 ABS → q var q1 ,q0 ABS → q ig q0 ,q0 FIX → q var q1 ,q0 FIX → q ig q0 ,q1 ig → ε,q1 ABS → q var q1 ,q1 ABS → q ig q1 ,q1 FIX → q var q1 ,q1 FIX → q ig q1 }∪ {q ig ig → ε,

∪ {q some FIX → qT qT | T ∈ T }∪{q some P → qT1 · · · qTP (P )|T1 → · · · → TP (P ) → T ∈ P type (P )q var var → ε}

{T1 , . . . , TP (P ) , T } ⊆ T∪ {q0 P → q0 · · · q0 | P ∈ (dom P ) \ {ABS, FIX}}}

Here A RRAY(i, q ) is a sequence of length #T consisting ofq any except for q at the i-th position. The sate q any accepts all trees
and q some accepts a tree if it is accepted by qT for some T ∈ T .

| {z }P (P )∪ {q1 P → q1 · · · q1 | P ∈ (dom P ) \ {ABS, FIX}}.

| {z }P (P )The state q1 means that var is currently not bound and q0 means it
is bound. The states q var and q ig only accept var and ig, respectively.
The definition of the automaton ATwt
T
INI
The automaton ATwt = (Σwt
, QTwt , ∆Twt , qwt) for the welltypedness check is defined as follows.

QTwt ··= {qT | T ∈ T } ∪ {q any , q some },
INI
some
qwt
,
··= q

∆Twt ··= {qT varT → ε | T ∈ T }∪ {qT oneof → A RRAY(i, qT ) | i ∈ [#T ] ∧ T ∈ T }∪ {qT1 →T2 ABS → qT1 qT2 | (T1 → T2 ) ∈ T }∪ {qT FIX → qT qT | T ∈ T }∪{|qT P → qT1 · · · qTP (P )(P, T1 → · · · → TP (P ) → T ) ∈ P type
{T1 , . . . , TP (P ) , T } ⊆ T}∪ {q any varT → ε | T ∈ T }∪ {q any oneof → q any · · · q any }

|

{z

#T
any

∪ {q any P → q any · · · q|{z

P (P )}| P ∈ dom P }}∪ {q some varT → ε | T ∈ T }∪ {q some oneof → A RRAY(i, q some ) | i ∈ [#T ]}∪ {q some ABS → qT1 qT2 | (T1 → T2 ) ∈ T }13

2016/10/1