1
Bonsai: Synthesis-Based Reasoning for Type Systems

arXiv:1708.00551v1 [] 1 Aug 2017

KARTIK CHANDRA, Stanford University
RASTISLAV BODIK, University of Washington

We describe algorithms for symbolic reasoning about executable models of type systems, supporting three
queries intended for designers of type systems. First, we check for type soundness bugs and synthesize
a counterexample program if such a bug is found. Second, we compare two versions of a type system,
synthesizing a program accepted by one but rejected by the other. Third, we minimize the size of synthesized
counterexample programs.
These algorithms symbolically evaluate typecheckers and interpreters, producing formulas that characterize
the set of programs that fail or succeed in the typechecker and the interpreter. However, symbolically
evaluating interpreters poses efficiency challenges, which are caused by having to merge execution paths of
the various possible input programs. Our main contribution is the Bonsai tree, a novel symbolic representation
of programs and program states which addresses these challenges. Bonsai trees encode complex syntactic
information in terms of logical constraints, enabling more efficient merging.
We implement these algorithms in the Bonsai tool, an assistant for type system designers. We perform
case studies on how Bonsai helps test and explore a variety of type systems. Bonsai efficiently synthesizes
counterexamples for soundness bugs that have been inaccessible to automatic tools, and is the first automated
tool to find a counterexample for the recently discovered Scala soundness bug SI-9633 [2].

1

INTRODUCTION

Today’s type system designers strive to develop typecheckers that balance expressiveness and
convenience with powerful static guarantees. This has led to a variety of innovations, such as
polymorphism, path-dependent types, and ownership types. On their own, these features promise
programmers strong static guarantees on their programs. Unfortunately, combining such features
often creates intricate soundness bugs, some of which have gone unnoticed for many years. For
example, soundness bugs were caused by the confluence of assignment and polymorphism in
ML [55, 61], and of path-dependent types and nullable values in Scala [2].
To automate checking of type systems, we present a set of symbolic algorithms that aid type
system designers in reasoning about executable language models. Using bounded program synthesis
techniques, we demonstrate how users can compute answers to queries such as these:
• Soundness. If the type system is not sound, synthesize a counterexample, a program that
passes the typechecker but fails in the interpreter.
• Comparison. Given two versions of a typechecker, synthesize a program accepted by one
version but rejected by the other, elucidating the impact of changes to a type system.
• Minimization. For either of the above queries, produce the smallest possible counterexample.
Successfully answering these queries requires us to efficiently explore the extremely large space
of candidate programs that are complex enough to demonstrate a harmful interaction. Fuzzers,
which are commonly used to answer the first query, attempt to search these large spaces by
avoiding programs that would be rejected somewhere along the parser-typechecker-interpreter
pipeline (see Figure 1). Early fuzzers explored the space of all programs, some of which may have
failed in the parser [63]. More recent “syntax fuzzers” such as Redex [28] generate only syntactically
correct programs, thus shrinking the candidate space. Further advancements allow us to generate
only type-safe programs [14, 15, 19, 43]. These “type fuzzers” use constraint solvers to search for a
Pre-print. 2017.

1:2

Kartik Chandra and Rastislav Bodik
syntactically
correct programs
random
program

Random fuzzer
samples all programs

well-typed
programs

✓
Parser

✓
Typechecker

✘
Interpreter

counterexample!

Syntactic fuzzer
samples grammar derivations

Type fuzzer
samples typesafe programs

Bonsai checker
reasons from runtime failures

syntax rules

syntax + type rules

syntax + typechecker +
interpreter

Fig. 1. Searching for a counterexample using various combinations of goal-directed search and forward
execution. For example, the type fuzzer composes type judgments with the goal of generating a random
type-safe program P. It then executes P forward on the interpreter, hoping that P will fail.

typesafe program in a goal-directed fashion; only the interpreter is executed forward. However,
even among type-safe programs, counterexamples are scarce.
The natural next step, then, is to reason about the entire pipeline in a goal-directed fashion, so
that a counterexample can be directly constructed by the constraint solver by reasoning backwards
from the possible failure points in the interpreter. We develop such goal-directed algorithm by
symbolically compiling the entire parser-typechecker-interpreter pipeline into a single logical
formula. This reduction also allows us to make the other queries mentioned above by modifying
the structure of the formula.
Our contributions are:
• The Bonsai tree (Sections 2 and 3): We describe Bonsai trees, a symbolic representation
of a bounded space of input programs and tree-shaped program states. Bonsai trees enable
symbolic evaluation of language models into logical formulas. Symbolic evaluation can be
performed on standard trees, of course, but Bonsai-powered symbolic evaluation is more
efficient and more effective, generating formulas that are smaller and easier to solve. Bonsai
trees reduce formula sizes by encoding the syntactic information in logical constraints
rather than in the shape of the data structure.
We demonstrate several interesting properties of Bonsai trees (Sections 3 and 4). First,
Bonsai trees make it easier to avoid symbolically evaluating the parser-typecheckerinterpreter pipeline as a monolithic composition of the three components. Instead, we
evaluate them separately, producing three simpler formulas that in turn represent syntactically correct programs; programs that pass the typechecker even though they may not be
syntactically correct; and programs that succeed (or fail) in the interpreter even though
they may syntactically incorrect or not typesafe. These three sets, illustrated in Figure 2,
are then intersected by conjuncting the formulas, to obtain the set of counterexamples.
Second, depending on what sets we intersect, we can formulate other queries. For
example, synthesis of correct programs that are rejected by the typechecker is also shown
in Figure 4. The Compare query is formed analogously (see the bullet “Case studies” below
for more details). The Minimize query simply adds the requirement that the solver returns
a solution that minimizes some user-supplied metric, such as the tree size.
Third, Bonsai trees can be added to standard symbolic evaluators. In particular, we
formalize symbolic evaluation of Bonsai trees on a small core language (Section 3) and
outline how we added this functional core language to Rosette [58], a symbolic evaluator for
a subset of Racket with assignments, objects, and other features (Section 4). This integration
of Bonsai symbolic evaluation into Rosette is at the heart of the Bonsai tool.

Bonsai: Synthesis-Based Reasoning for Type Systems

1:3
rejected good programs

Parser

symbolic tree
represents all programs
up to depth d
(define p
(make-symbolic-program!))

✓

(assert (parser p))

✓
Type Checker

Interpreter

syntactically correct programs

well-typed programs
(assert (typechecker p))

✘

programs failing in interpreter
(assert-not (interpreter p))

counterexamples
(define cex (solve))
(display cex)

Fig. 2. Bonsai performs three independent symbolic evaluations, executing the interpreter on trees that are
both syntactically and type-incorrect.

• Case studies (Section 5): We study a variety of type systems with Bonsai, gauging its
utility during a type system design. We perform three case studies, with Featherweight
Java [26], Ownership Java [11], and DOT, the dependently-typed model of Scala [5].
We first examine how counterexamples can provide a clear explanation of soundness
bugs. We demonstrate that by understanding how a counterexample fails in the interpreter,
in our case by examining a stack trace of a program crash, we can better understand the
cause of a soundness bug.
Second, we investigate what language specification patterns are friendly to symbolic
evaluation. Interestingly, we find that Bonsai trees can be efficiently used to represent not
only ASTs, but also other auxiliary data structures such as environments and class tables.
Third, we experiment with the Compare query: we ask Bonsai to explain a static type rule
that appeared to us unnecessary (subsumed by other checks) or unnecessarily restrictive
(rejecting correct programs). We removed the rule, creating a more permissive version of
the type system and asked Bonsai “Is there a program (i) rejected by the old type system,
(ii) accepted by the new type system, and (iii) that nevertheless runs without error?” Bonsai
synthesized such a program, suggesting that it may be useful to design a less restrictive
type system.
Finally, we use the DOT model to stress Bonsai’s expressiveness. DOT is a rich calculus
with dependent types, function types, records, intersection types, and recursive types. We
find DOT easy to reformulate to Bonsai patterns. We were able to express all features of
DOT except for recursive types: early on we decided to use call-by-value semantics, only to
realize later that DOT’s definition of recursive types is only compatible with call-by-name
semantics. Overall, implementing DOT features did not hamper symbolic evaluation. In
fact, in minutes, we synthesize on DOT a counterexample for the Scala soundness error
SI-9633 [2].
• Performance evaluation (Section 6): First, in under an hour, we synthesize a counterexample for the language with assignments and polymorphic references [54], which has been
inaccessible to automatic tools [19]. Second, we show that Bonsai trees allow exploration
of vastly larger spaces than the standard symbolic tree. In our experiments with lambda
calculus, Bonsai explores 1050 vs. 1025 candidate programs in 20 seconds. Third, on a subset
of Redex benchmarks, Bonsai is about 600-times faster than a syntactic fuzzer and 12-times
faster than a type fuzzer. We also find Bonsai superior in the size of counterexamples,
synthesizing counterexamples about 10-times smaller, on average, than the type fuzzer.
Implementations of many of the case studies and evaluations can be found at https://bitbucket.org/
bonsai-checker/.

1:4

Kartik Chandra and Rastislav Bodik

; syntax
; type rules
(define arithmetic-syntax
(define (check t)
'([exp zero (succ exp) (if exp exp exp) (zero? exp)
(tree-match t
]))
'zero (lambda () 'nat)
; evaluator
'(succ _) (lambda (x)
(define (execute t)
(assert (eq? (check x) 'nat))
(tree-match t
'nat)
'zero (lambda () 0)
'(succ _) (lambda (x) (+ (execute x) 1))
'(if _ _ _) (lambda (c t f)
(if (execute c)
(execute t)
(execute f)))
'(zero? _) (lambda (x) (= 0 (execute x)))))

'(if _ _ _) (lambda (c t f)
(assert (eq? (check c) 'bool))
(define t+ (check t))
(define f+ (check f))
;; (assert (eq? t+ f+))
;; omitted!
t+)
'(zero? _) (lambda (x)
(assert (eq? (check x) 'nat))
'bool)))

Fig. 3. An executable specification of the arithmetic language [41] that we would like to check for soundness.
tree-match is a pattern-matching macro, which checks an input AST against the given patterns, and, upon
finding a match, executes the accompanying lambda with the contents of the blanks as arguments.

Overall, we believe that Bonsai complements the theorem-prover-based mechanization of a
soundness proof, especially during design space exploration. Bonsai’s strengths are automation and
queries that go beyond soundness checking. Among weaknesses is the inability to guarantee absence
of bugs. This limitation is somewhat compensated by the Bonsai’s efficiency: we observe that during
an overnight run, it exhaustively explores candidates 2- to 4-times larger than the counterexamples
constructed by human experts (Table 3), providing a safety margin. The relationship with other
tools is given in Section 7.
2

BACKGROUND AND MOTIVATION

Figure 3 shows a simple executable specification of the simply-typed arithmetic language [41]. This
particular specification has an unsound typechecker, due to an omitted type rule—it does not verify
that the two branches of an “if” term have the same type. We would like to automatically synthesize
a counterexample to soundness for this language by symbolically translating the typechecker and
interpreter to SMT formulas, and then querying a solver for a program that passes “check” but
fails in “execute.” In this section, we explain the scalability challenges presented by this strategy,
motivating a new symbolic representation of abstract syntax trees. In the following section, we
address those challenges by designing such a symbolic representation, the Bonsai Tree. Finally,
equipped with the Bonsai Tree, we return to the example above and demonstrate how to synthesize
a counterexample.
We begin with a brief overview of symbolic evaluation techniques, focusing in particular on the
“branch-and-merge” strategy for evaluating conditional statements. We then explain how currentlyused symbolic data structures like ASTs are created by representing “symbolic unions” of concrete
trees, and why this structure makes branch-and-merge operations prohibitively expensive. Finally,
we introduce the key idea behind our new tree encoding, “Bonsai,” which allows the symbolic

Bonsai: Synthesis-Based Reasoning for Type Systems

1:5

evaluator to efficiently branch and merge, dramatically decreasing the time needed to create the
SMT formula.
2.1

Background: Symbolic Evaluation

Symbolic evaluation was first described by King [27]: the goal is to translate a program P with
inputs x 1 , x 2 , . . . , x n into an equivalent SMT formula f (x 1 , x 2 , . . . , x n ), which can then be processed
using an SMT solver. The inputs x i are called symbolic constants; they can be booleans, integers,
bitvectors, or members of any other theory supported by the SMT solver. Importantly, substituting
a concrete value vi for each x i in the formula should simplify to the same result as evaluating P
with arguments vi directly. For example, the symbolic evaluation of the program
P(x1 : int) : int {
int k = 0;
for (int i=0; i<3; i++) { k += x1; }
return k;
}

yields the formula (((0 + x 1 ) + x 1 ) + x 1 ).
A program may also make assertions about its symbolic constants. For example, the statement
assert P(x1) = 9 would create the formula (((0 + x 1 ) + x 1 ) + x 1 ) = 9. Such an assertion can
then be sent as part of a query to the SMT solver, which would report the solution model {x 1 = 3}.
Symbolic evaluators generally collect all assertions encountered during the program’s execution in
a set called the assertion store. The final query is the conjunction of all assertions in the store.
The symbolic evaluation of most terms is a straightforward application of partial evaluation.
However, branching statements require some care. Consider the program below.
P(x1 : int) : string {
if (x1 > 5) { return "big"; }
else
{ return "small"; }
}

Notice that the value of the condition x1 > 5 is not known to the symbolic evaluator. Thus, the
symbolic evaluator must branch to try both paths, and then merge the results to create a formula
expressing both alternatives. Such a formula is known as an ite for if-then-else, and the entire
process is known as a “branch-and-merge operation.” Here, the branch-and-merge operation yields
ite(x 1 > 5, "big", "small"). The conditions x 1 > 5 and ¬(x 1 > 5) are called the path conditions of
their respective values "big" and "small".
Operations on an ite are mapped over its branches. For example, the program strLen P(x1)
produces ite(x 1 > 5, strLen "big", strLen "small"), which is then simplified to ite(x 1 > 5, 3, 5).
Thus, one could query the solver for x 1 such that assert strLen P(x1) = 5. The solver may
report ‘2’ as a solution. Following Torlak and Bodik [58], we generalize the ite to the symbolic
union, which represents a sequence of n chained ites. We represent ite(ϕ 1 , v 1 , ite(ϕ 2 , v 2 , . . . )) as the
symbolic union {ϕ 1 → v 1 , ϕ 2 → v 2 , . . . , ϕ n → vn }. Each ϕ i is a path condition to its corresponding
value vi ; as with ites, operations on symbolic unions are mapped over each such value.
One final nuance lies in assertions made in the bodies of conditionals. Consider the program
P(x1 : int) : void {
if (x1 > 5) { assert x1 = 10; } // A
else
{ assert x1 = 0; } // B
}

A naive execution of this program creates the unsatisfiable assertion store x 1 = 10∧x 1 = 0. However,
both 10 and 0 should be valid values for x 1 . To allow this, the symbolic evaluator maintains a global
path condition, which reflects the conditions under which an assertion is made. The path condition

1:6

Kartik Chandra and Rastislav Bodik
join

𝑥

abs

𝑦
𝑥

𝜙1

app
𝑥

𝜆𝑦. 𝑥

𝑥

abs

𝑦
𝑥𝑦

𝜙3

𝜙2

app
𝑥

𝑦

share subtrees

Fig. 4. The symbolic union of three syntax trees G[x], G[λy.x], and G[(x y)] under their respective path
conditions ϕ 1 , ϕ 2 , and ϕ 3 . The “join” node represents a symbolic union. Notice that since members of a
symbolic union are disjoint, we can optimize for space by sharing subtrees across the merge.

is updated every time the program branches with a symbolic condition. For example, when the
first assertion (“A”) is made, x 1 > 5 must hold. Thus, the path condition is x 1 > 5, and the actual
assertion recorded by the symbolic evaluator is the implication x 1 > 5 =⇒ (x 1 = 10). Similarly,
the second assertion (“B”) is recorded as ¬(x 1 > 5) =⇒ (x 1 = 0). Thus, the query to the solver
becomes (x 1 > 5 =⇒ x 1 = 10) ∧ (¬(x 1 > 5) =⇒ x 1 = 0), which is satisfiable with both 10 and 0
as solutions for x 1 .
2.2

Symbolic Syntax Trees

To symbolically evaluate typecheckers and interpreters, we must represent programs in terms of a
set of symbolic constants. The classical approach to representing symbolic ASTs uses symbolic
unions to represent choosing between production rules. For the remainder of this section, we will
consider a simple grammar for the lambda calculus, with the production rules e → x | λx .e | (e e),
where x ranges over variable names.
Structure. To construct a symbolic AST, one might begin by creating a symbolic union over a
symbolic constant c, which chooses among the three types of depth-1 trees, i.e. the three production
rules: {c = 1 → x, c = 2 → λy.x, c = 3 → (x y)}. This symbolic union is depicted in Figure 4.
Larger ASTs can then be created recursively using the same process, using smaller ASTs as subtrees.
Notice that the structure of these trees depends on the syntax of the language. We thus call such
trees “syntax trees.” Syntax trees are appealing because of their simplicity: indeed, they are the
most commonly-used symbolic representations of ASTs. However, they can become extremely
inefficient when symbolically evaluated.
Scalability challenges. The inefficiency of symbolic syntax trees can be revealed by analyzing
their “branch-and-merge” operations. Recall that the “branch” operation takes place on a symbolic
condition: in the case of an operation on ASTs, this condition determines whether a tree matches
a given pattern. To perform a pattern-match on a symbolic syntax tree, the symbolic evaluator
must examine the members of the symbolic union and individually check whether each member
matches. Furthermore, when pattern-matching, we usually wish to extract subtrees that match
our pattern’s metavariables. The symbolic evaluator must therefore perform this extraction on
each member of the symbolic union and then merge the results into a fresh symbolic union. This
situation is depicted in Figure 5 on the left. For a symbolic union with n members, this operation
takes at least O(n) time.
Analyzing the “merge” operation reveals that such a merge often grows the size of the symbolic
union. To merge two symbolic unions, a symbolic evaluator must add together the members of
each symbolic union, updating the respective path conditions as required. In the worst case, this
can double the size of the symbolic union. This is depicted in Figure 5 on the right. Over the course
of many branch-and-merge operations, the symbolic unions that represent symbolic syntax trees
grow. Over time, symbolic evaluation slows down, and ultimately becomes impractically inefficient.

Bonsai: Synthesis-Based Reasoning for Type Systems
join
𝜙11

𝜙21

𝜙11

…

𝜆

𝜆

app

𝛼11 𝛽11

𝛼21 𝛽21

𝛼2𝑘 𝛽2𝑘

join
𝜙21

match(𝑛, λ 𝒗 . 𝒆) =
𝒗 ↦ 𝛼11
𝒗 ↦ 𝛼21
𝒆 ↦ 𝛽11 , 𝒆 ↦ 𝛽21 , …
pc ↦ 𝜙11 pc ↦ 𝜙21

1:7
𝐺1

𝜙11

join
… 𝜙1𝑘

𝐺2
𝜙21

join
… 𝜙2𝑘

𝜆

app

𝜆

app

𝛼11 𝛽11

𝛼1𝑘 𝛽1𝑘

𝛼21 𝛽21

𝛼2𝑘 𝛽2𝑘

merge(𝜙1 ⇒ 𝐺1 , 𝜙2 ⇒ 𝐺2 ):
join
𝜙1 ∧ 𝜙11
…
𝜙2 ∧ 𝜙21
𝜆
𝜆
app

𝛼11 𝛽11

𝛼21 𝛽21

𝛼2𝑘 𝛽2𝑘

Fig. 5. Left: A “match” operation on a symbolic syntax tree. Right: A “merge” operation on two symbolic
syntax trees.

Possible solutions. A crucial insight is that syntax trees are inefficient because their structure
depends on the grammar of the language. Representing a set of differently-shaped trees requires us
to create a symbolic union, which is expensive to match against. This intuition guides us to the key
idea behind the Bonsai tree: maintain a single tree that may or may not be syntactically-valid, and
push the constraints of the syntax to assertions in the assertion store. Such a “clean” data structure,
unencumbered by syntactic constraints, should be efficiently manipulable by a symbolic evaluator.
In the remainder of this paper, we demonstrate that this is indeed the case.
3

BONSAI TREES

We now formalize the intuition above in terms of the Bonsai Tree, an efficient alternative to the
syntax tree. Our discussion is guided by the Bonsai Core language, a minimal calculus that describes
programs that manipulate symbolic Bonsai trees via “match” and “merge” operations (Figure 6). An
empirical evaluation of the Bonsai encoding is presented in Section 6.3.
Structure. Bonsai trees are embedded in perfect binary trees. Figure 7 depicts three such “concrete”
trees, and their embeddings in perfect binary trees. As shown in the Bonsai Core rule SE-Tree, the
embedding is represented by assigning two symbolic constants to each node of the binary tree. The
first determines whether the node is internal or a leaf, and the second determines the terminal in
case it is a leaf. Figure 8 depicts one such representation.
More formally, a Bonsai tree G is a tuple hT , L, m, internal, leafi where T = hN , Ei is a perfect
binary tree of depth d and size m = 2d − 1, such that N is the set of nodes {n 1 , . . . , nm } and L is
the set of potential leaf symbols. The predicates internal : N → Bool and leaf : (N × L) → Bool
specify what tree is embedded in G. In a symbolic Bonsai tree, these guards are logical formulas
composed of symbolic constants.
Branch-and-merge operations. Bonsai carefully maintains the following invariant: each ite created
in the language has the property that if its condition is true, the result is a leaf, else it is an inner
node. This invariant can easily be verified for the rules SE-Tree and SE-Merge, the only sources of
ites in Bonsai Core.
A useful result of this invariant is that a pattern matcher need not branch when matching against
an ite: depending on whether the pattern is a leaf or an inner node, it is clear which path of the
ite must be taken. Thus, symbolic Bonsai trees can be matched in a single operation. In contrast,
recall that symbolic syntax trees required a match operation for each member of their symbolic
unions. Pattern-matching a Bonsai tree is depicted in Figure 9 on the left. The path condition ϕ
represents the conditions required for that Bonsai tree to match the pattern. Notice that since the
pattern-matcher never branches, any subtree can be extracted directly. In contrast, the symbolic
syntax tree must merge the extracted subtrees from each individual match into another, larger
symbolic union.
A merge of two Bonsai trees under path conditions ϕ 1 , ϕ 2 := ¬ϕ 1 is depicted in Figure 9 on the
right. No matter what the guards for these individual trees are, we can merge them by joining them

1:8

Kartik Chandra and Rastislav Bodik

hterm i ::= [ hterm i , hterm i ]
New inner node with subtrees
| tree d
Fresh tree of depth d ≥ 0
| c
Constant ranging over L
| match hterm i on ( hpat i for hterm i )* end Pattern matching
| x, y, . . .
Variable bound by a match

hval i ::= [ hval i , hval i ]
| c
| e
c
| fail
| ite( hfrm i , hval i , hval i )

hpat i ::= x, y, . . .
| c
| [ hpat i , hpat i ]

hfrm i ::= T | F
| e
c =c
| hfrm i ∧ hfrm i | hfrm i ∨ hfrm i | hfrm i =⇒ hfrm i | ¬ hfrm i

Pattern variable
Constant ranging over L
Inner node

Inner node with subtrees
Constant
Symbolic constant
Failure
If-then-else

SE-Tree

htree d − 1, π, ϕ i → ht 1, π, ϕ i
htree d − 1, π, ϕ i → ht 2, π, ϕ i
d >0
e
c 1 = fresh({Inner, Leaf})
e
c 2 = fresh(L)
c 1 = Leaf, e
c 2, [t 1, t 2 ]), π, ϕ i
htree d, π, ϕ i → hite(e

SE-Inner-Node
he, π, ϕ i → he 0, π 0, ϕ 0 i
hf , π, ϕ i → hf 0, π 00, ϕ 00 i

h[e, f ], π, ϕ i → h[e 0, f 0 ], π 0 ∧ π 00, ϕ 0 ∧ ϕ 00 i

SE-Match-Empty
hmatch t on [] end, π, ϕ i → hfail, π, ϕ ∧ ¬π i

SE-Leaf
v L , π, ϕ i
htree 0, π, ϕ i → he
SE-Match-Nonempty
htest p on t for e, π, ϕ i → he 0, π 0, ϕ 0 i
hmatch t on [q for f ; . . . ] end, π ∧ ¬π 0, ϕ i →
he 00, π 00, ϕ 00 i

hmatch t on [p for e; q for f ; . . . ] end, π, ϕ i →
hmerge(π 0, e 0, e 00 ), π 0 ∨ π 00, ϕ 0 ∧ ϕ 00 i

SE-Test-Const-Pass
htest c on c for e, π, ϕ i → he, π, ϕ i

SE-Test-Const-Fail
SE-Test-Sym
htest c on α for e, π, ϕ i → he, π ∧ (α = c), ϕ i

SE-Test-Pattern-Variable
htest x on t for e, π, ϕ i → he[t /x ], π, ϕ i

c , c0
htest c on c 0 for e, π, ϕ i → hfail, π, ϕ ∧ ¬π i
SE-Test-Inner-Node
htest p on t for e, π, ϕ i → he 0, π 0, ϕ 0 i
htest p 0 on t 0 for e 0, π 0, ϕ 0 i → he 00, π 00, ϕ 00 i

htest [p, p 0 ] on [t, t 0 ] for e, π, ϕ i → he 00, π 00, ϕ 00 i

SE-Test-Trans
ht, π, ϕ i → ht 0, π 0, ϕ 0 i

SE-Test-Ite
htest p on t for e, π ∧ ψ , ϕ i → he 0, π 0, ϕ 0 i
htest p on t 0 for e, π ∧ ¬ψ , ϕ i → he 00, π 00, ϕ 00 i

htest p on t for e, π, ϕ i →
htest p on t 0 for e, π 0, ϕ 0 i

htest p on ite(ψ , t, t 0 ) for e, π, ϕ i →
hmerge(ψ , e 0, e 00 ), (ψ =⇒ π 0 ) ∧ (¬ψ =⇒ π 00 ), ϕ 0 ∧ ϕ 00 i

SE-Merge

merge (π, ite(ϕ, a, [x, x 0 ]) , ite(ψ , b, [y, y 0 ])) →
ite ((π =⇒ ϕ) ∧ (¬π =⇒ ψ ), ite(π, a, b), [merge(π, x, y), merge(π, x 0, y 0 )])

Fig. 6. The Bonsai Core language and reduction rules. Here, t, e, f range over terms; p, q range over patterns;
x, y range over pattern variables; c ranges over L, the set of possible leaf values; α ranges over S, the set of
symbolic constants; π , ϕ,ψ range over boolean formulas with equality defined on S × L. ht, π , ϕi denotes
term t with path condition π and assertion store ϕ. fresh(A) denotes a fresh symbolic constant ranging over
set A. merge is defined in its most general form: a merge of two ite values. Definitions for merging non-ite
values can be derived by setting ϕ and/or ψ to T/F.
𝑥

internal node (unlabeled)
𝑥

λ
𝑦
𝑥

𝜆𝑦. 𝑥

𝑦

internal node
𝑥

leaf node (labeled with terminals)

leaf node
𝑥

λ

𝑥

𝑦

𝑥𝑦

𝐺(𝑥)

𝐺(𝜆𝑦. 𝑥)

𝑦

𝑥

unused node

𝐺( 𝑥 𝑦 )

Fig. 7. Left: Concrete Bonsai trees for terms x, λy.x, and (x y). Right: and their embeddings in perfect binary
trees.

node-wise under these path conditions. Thus, though we require O(m) operations to merge trees of
size m, the trees never grow: the output of the merge is the same size as each input tree, and the m

Bonsai: Synthesis-Based Reasoning for Type Systems
𝑛1

𝑛2
𝑛3

𝑛4

1:9

internal(𝑛1)

𝑛5
𝑛6 𝑛7

leaf(𝑛2, λ)

internal(𝑛5)
leaf(𝑛7, 𝑥)
leaf(𝑛6, 𝑦)

𝐺(𝜆𝑦. 𝑥)

Fig. 8. The representation of the embedded tree for λy.x.
tree pattern for 𝜆𝒗. 𝒆
𝑛1
𝑛2

𝑛4

𝑛3

𝑛5

λ
𝒗

𝒆

𝒗 ↦ 𝑛4
match(𝑛1 , λ 𝒗 . 𝒆) = 𝒆 ↦ 𝑛5
pc ↦ 𝜙
internal 𝑛1
where 𝜙 ≝ ሥ leaf 𝑛2 , λ
internal(𝑛3 )

𝐺3 ≝ merge(𝜙1 ⇒ 𝐺1 , 𝜙2 ⇒ 𝐺2):
𝐺1

𝜙11

𝐺2
𝜙𝑖1

𝜙12

𝐺3 𝜙13 = (𝜙1 ⇒ 𝜙11 ∧ 𝜙2 ⇒ 𝜙12 )
𝜙𝑖2

…

𝜙𝑖3 = (𝜙1 ⇒ 𝜙𝑖1 ∧ 𝜙2 ⇒ 𝜙𝑖2 )
…

…

Fig. 9. Left: Matching on a Bonsai tree guarantees to return a single match, at the cost of creating a larger
formula. Right: Merging two Bonsai trees. At the constant cost of merging a guard for each node, we avoid
growing the tree.

operations are a constant time cost. In contrast, the symbolic syntax tree grow at each merge, and
thus the time cost grows as more branch-and-merge operations are carried out.
Notice that while the tree itself does not grow, the formulas for the guards do indeed grow at
each merge due to the addition of path conditions. This, however, is not a concern for two reasons.
First, symbolic evaluation engines represent formulas as DAGs. Creating a disjunction of two
formulas does not require us to duplicate each formula in memory, which would be an expensive
operation. Instead, we only need to allocate a fresh “∨” operator node, and create cheap pointers
to existing formulas for the operands. Second, we never have to “look inside” these formulas. We
only construct them and, when finished, pass them on to the SMT solver. As a result, the growing
formulae do not affect the efficiency of the symbolic evaluation.
Example. Figure 10 depicts a small worked example of pattern-matching against and merging
symbolic Bonsai trees. The mini-language has three terms: id(x), which evaluates to its argument,
swap(x, y) which swaps its arguments when evaluated, and a, a constant that evaluates to itself.
The grammar, as well as its embedding in binary trees, is presented in the top half of the figure.
The bottom half depicts the symbolic evaluation of the Bonsai Core term
match (tree 3) on
a for a
[swap, [x, y]] for [swap, [y, x]]
[id, x] for x
end

We first perform each individual match, creating path conditions and results, and then merge the
results under each path condition.
4

IMPLEMENTATION

This section illustrates how to implement Bonsai trees in a specific language, Racket [22], using a
specific symbolic evaluator, Rosette [56]. Of course, guided by the rules in Figure 6, these ideas
can be implemented in other symbolic evaluation platforms as well [48, 49]. After implementing
Bonsai trees, we demonstrate how to use them to check the arithmetic language in Figure 3.
Constructing a symbolic tree. Recall rule SE-Tree from Figure 6. Two fresh symbolic constants
on each node dictate whether it is an internal node or a leaf, and if it is a leaf, which symbol it
represents. We can construct such a node by symbolically evaluating the call to binary-tree!

1:10

Kartik Chandra and Rastislav Bodik
Grammar G:
e ::= a | id e | swap e e

A bonsai embeddings for grammar G:
a

Program P:

id

match t on
a
for a
id 𝑥
for 𝑥
swap 𝑥 𝑦 for swap 𝑦 𝑥
end

swap

𝑖𝑑

a

id 𝑒

a

𝑒1

𝑒2

swap 𝑒1 𝑒2

swap

a

a

𝑖𝑑

a

a

id

a

a

id

a

swap

𝑖𝑑
swap

a

𝑒

a

id

a

a

a

a
a

a

Two tree transformations made by P. Left: on concrete syntax trees. Right: on concrete bonsai trees.

case:
path condition:

a for a

id 𝑥 for 𝑥

𝜙a : 𝑛1 = a

𝜙id : inner 𝑛1 ∧ 𝑛2 = id

swap 𝑥 𝑦 for swap 𝑦 𝑥
𝜙swap : ¬ 𝜙a ∧ 𝜙id

otherwise

a
matched tree:

id

a
result per case

result after merge:

𝑛1
𝑛2
𝑛3

𝑛4

𝑛5
𝑛6 𝑛7

ϕ1′ : ϕa ⇒ a, ϕid ⇒ ϕ5 , ϕswap ⇒ internal
ϕ′2 : ϕid ⇒ ϕ6 , ϕswap ⇒ ϕ5
ϕ′3 : ϕswap ⇒ ϕ6
ϕ′4 : ϕswap ⇒ ϕ7
ϕ′5 : ϕid ⇒ ϕ7 , ϕswap ⇒ ϕ2
ϕ′6 : ϕswap ⇒ ϕ3
ϕ′7 : ϕswap ⇒ ϕ4

internal node
leaf node
unused node
symbolic
(any of the above)

The effect of P on symbolic bonsai trees. 𝜙𝑖 and 𝜙𝑖′ are the conditions of 𝑛𝑖 on entry/exit of P.

Fig. 10. An example of pattern-matching against a symbolic Bonsai tree and merging the results.

Bonsai: Synthesis-Based Reasoning for Type Systems
(define (binary-tree! depth)
(if (> depth 0)
; SE-Tree
(if
(eq? 'leaf (fresh-symbolic! '(leaf inner)))
(fresh-symbolic! all-leaves)
(cons
(binary-tree! (- depth 1))
(binary-tree! (- depth 1))))
; SE-Leaf
(fresh-symbolic! all-leaves)))

1:11

(ite (= s1 leaf)
s2
(cons (ite (= s2 leaf) s4 ...)
(ite (= s3 leaf) s5 ...)))

(define all-leaves '(zero succ zero? if))
; for arithmetic language

Fig. 11. A procedure that generates a fresh symbolic Bonsai tree (left), and its output (right).

shown in Figure 11 (left). The call is recursively unrolled by the symbolic evaluator until the depth
limit reaches zero, at which point we follow SE-Leaf by creating a single symbolic constant to
represent which symbol is represented by the leaf. fresh-symbolic! is a macro that symbolically
selects from a set S, analogous to fresh(S) in Bonsai Core. Internally, it is implemented by creating
symbolic integer constants and maintaining a map from integers to members of S. Inner nodes
are represented by cons pairs so that we can take advantage of existing Racket primitives for
manipulating S-expressions.
The result of symbolically evaluating binary-tree! is a data structure that embeds the symbolic
constants si , pictured in Figure 11 (right). Note that this tree contains no syntactic information:
concrete assignments of values to each si may create syntactically-invalid ASTs.
Pattern-matching. The Bonsai pattern-matching macro, tree-match, is implemented by following
the rules SE-Test-{ Const-Pass, Const-Fail, Sym, Pattern-Variable, Inner-Node, Trans } as
expected. Since the pattern-matcher is written within a symbolically-evaluated language, SE-TestIte follows automatically from the symbolic evaluator’s behavior on operations on ites. Figure 12
illustrates the behavior of the pattern-matcher using the example of syntactic constraints (see
below). Note that as per SE-Match-Nonempty, the pattern-matcher is sensitive to the order in
which patterns are presented. If a tree matches two patterns p1 and p2 , the earlier one (p1 ) is given
priority. The path condition for the p2 match will stipulate that the p1 match fails. This resolves
ambiguities in case the patterns are not mutually exclusive.
Syntactic constraints. To assert that the Bonsai tree embeds only syntactically correct trees, we
can take advantage of pattern-matching. We invoke (assert (is-program? tree)), which traverses
the tree and generates constraints required by the grammar defined in Figure 3. This call expands
into the procedures in Figure 12. More generally, we provide the macro syntax-matches?, which
converts a grammar in BNF to a syntax checker in the style of is-program?.
Merge. Recall from Section 2.1 that symbolic evaluators already perform merges on conditional
branches. Rosette in particular also performs some simplification: when merging two cons pairs, it
first individually merges the heads and tails, and then creates a fresh cons pair of the two merges.
This gives us half of the merge operation “for free”: we must only be careful to arrange for Rosette
to merge pairs separately from leaves, since the simplification does not apply to merging a leaf

1:12

Kartik Chandra and Rastislav Bodik
(define (is-program? p)
(tree-match p
'zero (lambda () #t)
'(succ _) (lambda (x) (is-program? x))
'(if _ _ _) (lambda (c t f)
(and (is-program? c)
(is-program? t)
(is-program? f)))
'(zero? _) (lambda (x) (is-program? x))
'_ (lambda () #f)))

(define (is-program? p)
(cond [(eq? p 'zero) #t]
[(and (pair? p)
(eq? (car p) 'succ)
(null? (cddr p)))
(is-program? (cadr p))]
[(and (pair? p)
(eq? (car p) 'if)
(pair? (cdr p))
(pair? (cddr p))
(pair? (cdddr p))
(null? (cddddr p)))
(and (is-program? (cadr p))
(is-program? (caddr p))
(is-program? (cadddr p)))]
[(and (pair? p)
(eq? (car p) 'zero?)
(null? (cddr p)))
(is-program? (cadr p))]))

Fig. 12. Placing syntactic constraints on the Bonsai tree. The code results from macro expanding the arithmetic
grammar (left). One more level of expansion (right) reveals the internal Bonsai tree structure.

with an inner node. This, however, is always the case as long as the ites being merged satisfy
the invariant described in Section 3. Thus, by carefully regulating the creation of ite values in
binary-tree!, we force Rosette to always perform a Bonsai merge on trees.
4.1

The Bonsai Checker

Equipped with the Bonsai Tree, we now return to our goal of symbolically reasoning about the
language in Figure 3. We begin by searching for counterexamples to soundness. The Bonsai Tree
allows us to efficiently execute the algorithm shown earlier in Figure 2. First, create a symbolic
representation of the set of all ASTs up to some maximum size m. Next, compute symbolic
representations of trees that (a) are syntactically valid; (b) pass the typechecker; (c) fail in the
interpreter. Finally, ask the solver to find a tree in the intersection of these sets. If it exists, this
program is a counterexample.
Recall that the typechecker in Figure 3 has a soundness bug, failing to verify that the two
clauses of ‘if’ expressions have the same type. Bonsai catches this error by executing the algorithm
described above:
(define program (binary-tree! 10))
(assert-pass (syntax-matches? arithmetic-syntax program))
(assert-pass (check program))
(assert-fail (execute program))
(define solution-model (solve))
(echo (evaluate program solution-model))

The first line creates the formula characterizing the set A of all abstract syntax trees of depth 10
or less that adhere to the grammar. The second line creates the formula S, which describes the
subset of programs in A that are syntactically-valid. The third line evaluates the formula on the
typechecker to create the formula T , which describes the set of programs that pass the typechecker.
The fourth line does the same with the interpreter, negating the formula generated to produce I 0.

Bonsai: Synthesis-Based Reasoning for Type Systems

1:13

The fifth line queries the solver for a model that satisfies the formula S ∧ T ∧ I 0, and the sixth line
simply interprets the model to yield a concrete program, which is then echoed to the user. Bonsai
returns the following counterexample in less than 2 seconds.
'(succ (if (zero? (succ zero)) zero (zero? zero)))

Indeed, this program passes the typechecker but causes the interpreter to crash by attempting to
increment a boolean value. If we reintroduce the omitted check in our typechecker, our system
fails to find a counterexample, showing that this check fixes the bug.
4.2

A Variation on the Query

A small variation on the counterexample-finding algorithm above allows us to compute a “diff”
of two typecheckers by querying for programs that are accepted by one but rejected by the other.
Suppose a student submits the unsound arithmetic typechecker above to a teacher. The teacher can
compare it to a correct reference implementation and give the student feedback in the form of a
program accepted by the former but rejected by the latter.
To synthesize such a program, we initialize T , the set of all programs that pass the student’s
implementation, and U , the set of all programs that pass the teacher’s implementation. Then, we
query the SAT solver for any member of the set S ∧ T ∧ U 0.
(define program (binary-tree! 10))
(assert-pass (syntax-matches? arithmetic-syntax program))
(assert-pass (student-check program))
(assert-fail (teacher-check program))
(define solution-model (solve))
(echo (evaluate program solution-model))
; ==> '(if (iszero? zero) zero (iszero? zero))

Note that this program is not a counterexample to soundness because it does not fail at runtime.
However, it behaves differently on the two typecheckers, and thus represents a member of their
“diff.”
5

CASE STUDIES

We now demonstrate how Bonsai can be used to explore three more advanced type systems: an
object-oriented, an ownership-based, and a dependent type system. Besides looking for soundness
issues, we also run queries that help us better understand the type system’s restrictions.
5.1

Featherweight Java

Featherweight Java [26] is a calculus that models essential features of the Java programming
language. Featherweight Java has classes with methods, as well as inheritance via subclasses.
We test Bonsai’s ability to identify the classical bug in function subtyping, which is to insist that
function arguments are covariant, i.e. to assume that s <: t implies (s → u) <: (t → u). The correct
approach is to require contravariance in function arguments, i.e. if s <: t then (s → u) :> (t → u).
This bug is of historical interest because it appeared in early versions of the Eiffel programming
language, and its discovery came as a surprise to the Eiffel community [12].
After we introduced the bug into our Featherweight Java implementation, Bonsai reported the
following counterexample in a few seconds. This counterexample has been manually formatted to
Java syntax:
class A extends Object {
B bar(A arg) {
return arg.bar(this);
} }
class B extends A {

1:14

Kartik Chandra and Rastislav Bodik
B quux(C arg) {
return new A().bar(arg);
} }
class C extends B {
B bar(B arg) {
return arg.quux(this);
} }
new C().quux(new C());

The call stack execution trace:
Error : class A has no method quux
in new 2 A (). quux ( new 1 C ()); // line
... new 1 C (). bar ( new 2 A ()); // line
... new 2 A (). bar ( new 1 C ()); // line
... new 0 C (). quux ( new 1 C ()); // line
...[ init ]

11
3
7
13

In the stack trace, we can see that the failure is caused by new C().bar(new A()). This call occurs
because the method C.bar is unsoundly allowed to be used in place of A.bar because of their
covariant argument types. This explains why the covariant argument rule is problematic: whenever
C <: A, the rule promises that we can safely use a C wherever we use an A. This promise is violated
because A.bar accepts inputs that C.bar does not. Note that this issue does not apply to true Java,
because shadowing an inherited method with a different argument type overloads that method
name, creating a distinct method.
The symbolic evaluation of Featherweight Java is much more demanding than that of the
arithmetic language. To typecheck and evaluate Featherweight Java, we must make lookups into a
class table in order to traverse the subclass hierarchy; when the class table is symbolic, a lookup
could potentially be any of the entries in the table. Representing the class table as a Bonsai Tree
allows us to efficiently merge all possible results of a lookup into small, compact formulas that can
easily be manipulated by the interpreter.
5.2

Ownership Java

Our next language augments Featherweight Java with an object-oriented ownership type system,
Ownership Java [9, 11]. The safety guarantee made by Ownership Java is that well-typed objects
must access only objects that they own. The type system statically enforces this encapsulation
guarantee by keeping track of the binary ownership relation on objects, which is declared in
annotations on each class, method, and field.
A canonical example of Ownership Java is the implementation of a stack. The stack object is
allowed to access its inner linked list but not the objects stored in the linked list; those can only
be accessed by the client of the stack. The stack class is thus defined with two owner parameters.
The first parameter is special because it is the owner of the stack object at runtime. The second
owner parameter denotes the client who owns the data in the list; this parameter is used by the
stack class implementation to annotate its methods and the encapsulated linked list. For example,
the return value from the pop method is annotated with the second owner parameter, allowing the
client to access objects retrieved from the stack.
To prove soundness of Ownership Java, Boyapati et al. [11] introduce an “ownership tree,” a
transitive view of the ownership relation: o 2 is a direct descendant of o 1 if o 1 owns o 2 . The ownership
tree is rooted at the special owner world. Using the ownership tree, the encapsulation theorem is
stated: object x can access object o only if (1) x = o, (2) x is a descendant of o in the ownership tree,
or (3) x is an inner class object of o. This invariant can be checked by tools like Pipal (Section 7).

Bonsai: Synthesis-Based Reasoning for Type Systems

1:15

With the Bonsai Checker, however, we do not need to formulate any such invariant. Instead,
we only need one straightforward dynamic check to detect unsoundness. The check asserts that
the owner stored in the accessed object (object) is owned by the receiver of the accessor method
(this):
(define (evaluate-expression ...)
...
(assert
(owns? this object)
"Error: attempted invalid access!")
...)

This check is easy to implement because it is a direct statement of the desired guarantee.
We believe that a counterexample that violates this assertion provides a more intuitive understanding of the issue than a counterexample that violates the encapsulation theorem because a
trace shows the origins of the unsafe state. We reproduce one such counterexample below, found
by Bonsai in about 90 seconds when we disabled the static owner check of method calls:
class Main<O1, O2> extends Foo {
Main<O1, O1> meth3(Main<O1, O1> arg) {
(arg.meth3(arg)).main(arg);
} }
class Foo<O1, O2> extends Object {
Main<O2, O2> main(Main<O2, O2> arg) {
(new Main<O2, O2>()).meth3(arg);
} }
new Main<world, world>().main(new Main<world, world>());

This program fails at runtime because Foo<O1, O2> should not be allowed to access methods of
a Main<O2, O2> on line 7. It should only be allowed to access an instance of Main that it owns,
which could be a Main<this, O1> or a Main<this, world>.
Why have additional constraints on owners? Next, we illustrate Bonsai’s ability to compare type
systems by formulating queries involving multiple typecheckers and interpreters.
When instantiating a new object with owner parameters o 0...n , the Ownership Java type system
insists that the object’s owner o 0 is a descendant of all other owner parameters o 1...n in the
ownership tree. It is not immediately obvious why this condition is imposed — it is dictated by
features interacting with subtyping [10].
A language designer could thus be posed the question, “What are the consequences of this extra
check? Specifically, does adding the check reject any correct programs that were accepted prior to
adoption of this rule?” We answer this question with Bonsai. First, we create a version of Ownership
Java (OJ) called Reduced Ownership Java (ROJ) where subtyping is prohibited and the additional
constraint on owners is removed. As expected, Bonsai fails to find a soundness counterexample in
the ROJ language.
Now we are ready to query for the program of interest. This program must (1) fail the OJ
typechecker, (2) pass the ROJ typechecker, and (3) succeed at runtime. This program is rejected by
OJ, does not use subtyping, and is correct, per the three conditions in the query. Bonsai produces
the following counterexample in just over a minute.
class Main<O1, O2> {
Main<world, O2> main(Main<O1, O2> arg) {
return new Main<world, O2>();
} }
new Main<world, world>.main(new Main<world, world>)

1:16

Kartik Chandra and Rastislav Bodik

This program fails the Ownership Java typechecker because world is not a descendant of O2 in
the ownership tree. However, this program is otherwise correct: it passes our Reduced Ownership
Java typechecker and does not fail at runtime. While the counterexample itself is not particularly
profound, it provides evidence that suggests that a less restrictive static type rule could be designed.
The comparison between OJ and ROJ is made possible by the novel way in which Bonsai allows
users to compose sets of constraints when querying the solver. Crucially, by comparing two versions
of a typechecker, we can better understand how the difference in type rules affects which programs
are rejected.
Simplifying Counterexamples with Minimization. Ownership Java programs can easily grow
extremely large, due to the presence of unused classes and methods. In order to have an easilyunderstandable counterexample, we present our SMT solver with an additional goal: to minimize
the size of the generated program. Thus, the counterexamples listed above are minimal: no smaller
program satisfies the constraints we imposed.
5.3

Dependent Object Types (DOT)

Dependent Object Types, or DOT [4] is both a formalization of the essence of Scala [40] and the basis
for dotty [38], an experimental Scala compiler. This makes DOT a good candidate for a real-world
type system that underlies a common, modern, and practical programming language.
DOT features path-dependent types. For example, the signature
feed(pet : Animal, food: pet.FoodType) : Boolean

describes a function whose second argument has a type pet.FoodType that depends on the first
argument pet, hence the name path-dependent types. DOT also provides record types such as
{ name : String }, and intersection types such as type Nat = Int ∧ Positive.
In this section, we examine the Scala soundness issue SI-9633 [2, 3]. The issue was discovered by
reasoning about extending DOT with some features of full Scala, namely the addition of the null
object. In this section, we demonstrate how to add null to DOT and use the Bonsai Checker to
find a counterexample to the issue1 .
With the Bonsai Checker library, we need just over 400 lines of code to implement DOT. The
implementation closely follows the specification by Amin et al. [5]. For example, three of the
subtyping rules are below:
Γ ` T <: >

Γ ` ⊥ <: T

Γ ` S <: T

Γ ` S <: U

Γ ` S <: T ∧ U

Their corresponding implementations in Bonsai are almost direct translations:
(define/rec (dot-subtype? sub sup)
(tree-match `(,sub . ,sup)
'(_ . Any)
(lambda (T) #t)
'(Nothing . _)

(lambda (T) #t)

'(_ . (and . (_ . _))) (lambda (S T U)
(and (dot-subtype? sub T)
(dot-subtype? sub U)))
...))

The NanoDOT language. Figure 13 shows the syntax of the version of DOT we use to investigate
the issue SI-9633. There are two deviations: first, for convenience, we add a global variable φ
1 Our Bonsai models

of NanoDOT and NanoScala are available at https://bitbucket.org/bonsai-checker/dot/.

Bonsai: Synthesis-Based Reasoning for Type Systems
htermi ::= htermi . hnamei
selection
| hdefinitioni
object instantiation
| hnamei
variable reference
| λ ( hnamei : htypei ) : htypei { htermi } lambda
| htermi ( htermi )
application
hdefinitioni ::= { val hnamei = htermi }
| { type hnamei = htypei }
| hdefinitioni ∧ hdefinitioni

field
type
aggregate

1:17

htypei ::= > | ⊥
top, bottom
| htermi . hnamei
type projection
| { val hnamei : htypei }
field decl
| { type hnamei >: htypei <: htypei } type decl
| htypei ∧ htypei
intersection
| htypei → htypei
function
hnamei ::= a | b | c | φ

Fig. 13. The NanoDOT language.

of type > to the environment; its value will populate records in counterexamples. This addition
makes counterexamples more readable: since DOT itself does not provide any primitive types,
in pure DOT, Bonsai would have to use type-tags as leaf values in counterexamples. Second, we
omit recursive types, because DOT’s definition of recursive types using call-by-name semantics is
incompatible with our call-by-value implementation.
We now discuss two counterexamples found using Bonsai. The first explains a restriction imposed
by DOT, while the second is a variant on the counterexample in SI-9633.
Disjoint domains in intersection types. DOT restricts intersection types and aggregate definitions
to field-disjoint terms. That is, AndDef-I reads [5]:
Γ ` d 1 : T1
d 2 : T2
dom(d 1 ) ∩ dom(d 2 ) = ϕ
Γ ` d 1 ∧ d 2 : T1 ∧ T2
where di are definitions and dom(d) is the set of fields bound in d.
A reader lacking expertise in type systems might not immediately see the rationale for this
restriction. Such a reader can simply remove AndDef-I from our implementation of NanoDOT and
observe the results. Bonsai constructs the following useful counterexample:
λ ( b : { val a : { val a : > } } ): > {
b.a.a
} ( { val a = φ } ∧ { val a = { val a = φ }} )

When given this program, the interpreter crashes, finding that b.a is undefined. Since b is bound
to an intersection where both sides have a value for the field a, the value b.a could be either φ or
{ val a = φ }. If the left side is chosen, we get a runtime error. If the right side is chosen, we get
φ. Since our implementation gives precedence to the left member of an intersection, our interpreter
throws a runtime error, making this program a counterexample. In summary, this example points
out that if the interpreter is to make a greedy choice among intersected values, these values must
have no conflicting fields, which explains AndDef-I.
Collapsing the subtype hierarchy using bad bounds (SI-9633). A common soundness issue with
dependent types relates to bad bounds, which allows creating uninhabitable types. For instance, the
type { type S >: > <: ⊥ }, which means that > <: S <: ⊥, should clearly be uninhabitable.
Otherwise, we would be able to collapse the subtype hierarchy and prove all types equivalent,
much like how a single contradiction allows proving anything in an inconsistent logical system [5].
DOT does not check the bounds of dependent types but ensures that values have types with
correct bounds. So, one can create the badly-bounded type { type S >: > <: ⊥ } but values are

1:18

Kartik Chandra and Rastislav Bodik

syntactically constrained to have coinciding lower and upper bounds, using the construct { type S
= > }, which expands to { type S >: > <: > }. As a result, while types with bad bounds can
be created in DOT, it is impossible to instantiate values with badly-bounded dependent types. This
restriction makes it easy to check the bounds of a value upon its instantiation.
In Scala, however, it is possible to create a value without going through a constructor, which
makes bounds checking hard. Odersky [39] describes three situations where this is possible: using
lazy for delayed instantiation, using null for uninstantiated values, and using type projection. In
these cases, the compiler cannot check for bad bounds of dependent types. In Scala, it is possible to
instantiate values with badly-bounded dependent types. This is the basis for SI-9633.
Scala soundness bugs, including SI-9633, are traditionally demonstrated with an example that
casts an arbitrary value to the type Nothing. Since Nothing is a subtype of all other types, this
allows us to cast a value to any other value, for example, via the sequence Number → Nothing →
String. In practice, such an operation leads to the runtime ClassCastException in the JVM.
To explore bugs related to bad bounds, we extend NanoDOT to NanoScala with a null value of
type ⊥. We also add a term to allow casting. The term cast t to T is typechecked in the usual
manner, by ensuring that t : S ∧ S <:T . At runtime, the cast performs the same check to detect
counterexample programs. This is sufficient to model the relevant Scala issues in NanoScala.
We are now ready to query Bonsai for a NanoScala equivalent of the SI-9633 counterexample.
This program was found in around 4 minutes:
cast
(λ ( a : { type b >: > <: ⊥}): a . b {
φ
})( cast null to { type b >: > <: ⊥})
to ⊥

Why does this program typecheck? The inner cast typechecks because null is of type ⊥, which
is a subtype of all types — this includes the type { type S >: > <: ⊥ }, regardless of its bad
bounds. The outer cast to ⊥ typechecks because the type a.b is bounded above by ⊥; this is allowed
because badly-bounded types can be created in DOT.
Why does the program fail at runtime? At runtime, the issue occurs when null is cast to
{ type S >: > <: ⊥ }. This type is uninhabited, yet, modeling Scala, NanoScala nevertheless
casts null to it. The execution continues with a value with badly-bounded dependent types. As
a consequence, we can now invoke the lambda expression synthesized by Bonsai. This lambda
should not be called, since its argument is of an uninhabited type. However, when called anyway,
it returns φ : > which is cast to ⊥. This raises an exception.
In summary, NanoScala allows us to cast a non-null value to ⊥, which is at the heart of the
SI-9633 counterexample. This is because the NanoScala null and cast terms violate NanoDOT’s
property that all dependent types are backed with an instantiated value.
There are two important notes regarding our implementation of DOT: First, to prevent Bonsai
from synthesizing counterexamples related to null dereferencing, we must tell Bonsai to disregard
bugs involving the selection operator. Second, our current implementation of NanoDOT does not
maintain type information at runtime. Thus, we only raise an exception on casts of non-null values
to ⊥, which can be detected without any runtime type information. This is sufficient to catch the
runtime errors we are interested in; the Scala example Number → String would fail when Number
is cast to Nothing, which we model as DOT ⊥.
Finally, we can translate the NanoScala counterexample to Scala. We must manually make two
minor changes. First, unlike DOT, Scala does check type annotations that have bad bounds. A

Bonsai: Synthesis-Based Reasoning for Type Systems
trait A { type L <: Nothing }
trait B { type L >: Any }
def toL(b: A with B): b.L = 123
val p: B with A = null
toL(p): Nothing

1:19

trait A { type L <: Nothing }
trait B { type L >: Any }
def toL(b: B)(x: Any): b.L = x
val p: B with A = null
println(toL(p)("hello"): Nothing)

Fig. 14. Comparing Bonsai’s counterexample with SI-9633. Left: A counterexample found by Bonsai, manually
translated to Scala with variables renamed for clarity. Right: The counterexample reported on SI-9633 [3],
copied verbatim.

simple layer of indirection suffices to avoid this check: we create our badly-bounded type { type S
>: > <: ⊥ } as an intersection of two well-bounded types P and Q:
trait P {type B <: Nothing}
trait Q {type B >: Any}

Note that Scala’s intersection types are not commutative due to shadowing, so we must care to use
either P with Q or Q with P, depending on the context.
The second change is purely syntactic. Scala’s lambdas do not allow path-dependent return type
annotations in the same style as methods, so we translate the lambda to a named method.
def bad(a: P with Q): a.B = 123
bad(null: Q with P): Nothing

When run with scala, this example produces:
java.lang.ClassCastException:
java.lang.Integer cannot be cast
to scala.runtime.Nothing

After variable renaming, this counterexample corresponds almost exactly with the one reported on
SI-9633. Figure 14 presents a side-by-side comparison.
Discussion. We demonstrate the use of Bonsai in studying DOT, a language with a complex type
system. We provide two subtle bugs that can be introduced in DOT by modifying the language, and
show that in each case Bonsai produces elegant counterexamples after only a couple of minutes.
The latter of these counterexamples reproduces a soundness counterexample for the Scala compiler,
SI-9633.
6

EMPIRICAL EVALUATION OF PERFORMANCE

In this section, we evaluate the efficiency of Bonsai. We consider the speed of symbolic evaluation
and solving, the sizes of the counterexamples, and the sizes of program spaces that are explored. We
find that Bonsai reliably finds bugs in a few seconds or minutes. When left to run for longer periods
of time, Bonsai explores spaces containing programs much larger than the minimal counterexample,
providing a margin of assurance.
6.1

Comparing Bonsai with Fuzzers

Here, we compare Bonsai to the fuzzers mentioned in Section 7: in particular, the syntactic fuzzer
built into Redex [30], and the type fuzzer based on judgement trees [18].

1:20

Kartik Chandra and Rastislav Bodik

The benchmark. We implemented2 the “stlc+lists” language from the Redex benchmark [45] in
Bonsai and introduced each of the nine bugs to our implementation (these were all one-line changes).
We compared the performance of Bonsai to the performance of the syntactic fuzzer and type fuzzer
from the Redex benchmark in two respects: first, the time taken to find a counterexample, and
second, the average size of counterexamples found. Note that all tests were run on the same
machine.
Results. Our results are plotted in Figure 15 (left), and the times and sizes, correlated by bug, are
listed in Table 1. We make two important observations below.
First, we note Bonsai’s consistency. While fuzzers are slightly faster than Bonsai on some
benchmarks, they are several orders of magnitude slower on others, taking anywhere from a few
minutes to over an hour. Bonsai, on the other hand, takes between 1 and 5 seconds on every
benchmark. Consider, for example, bugs 4 and 5, which were the hardest for fuzzers to find, despite
both being labeled “shallow” errors in the benchmark suite. Bug 5 changes the interpreter to return
the head of a list when tail is applied, while bug 4 assigns the return type of cons to int, rather
than Listof int as expected. Bonsai finds these bugs just as fast as it finds other bugs. However,
these bugs are many orders of magnitude more difficult for fuzzers to reveal. This is because these
bugs require a specific set of interactions in the counterexample program, and thus the probability
of randomly generating such a program is extremely low.
Second, we compare the sizes of counterexamples produced by the two tools. The type fuzzer,
though efficient, generates extremely large and complex programs as counterexamples. This likely
contributes to its effectiveness, since larger programs are likelier to uncover soundness bugs [62].
However, such programs are extremely difficult for users to reason about, with (for example) dozens
of layers of nested lambdas. In contrast, Bonsai consistently produces small counterexamples.
In almost all cases, Bonsai’s counterexamples were identical to the ones suggested by the Redex
benchmark authors — one was smaller.
Inspired by the latter observation, we evaluated Bonsai’s efficiency on constructing minimal
counterexamples by querying the solver for a solution that minimizes the size of the counterexample.
Our results are shown in Table 2. We find that the most of the counterexamples produced by Bonsai
were already minimal, even without the minimization query. However, for the three bugs that
could be further minimized, the minimization query only took 10%-30% longer than the standard
query.
As a final demonstration of Bonsai’s efficiency compared to fuzzers, we consider a historic bug
involving let-polymorphism in the presence of mutable references, in e.g. ML [55, 61]. This “classic
let+references” bug is included in the Redex benchmark as let-poly-2. However, the syntactic fuzzer
has been run on it for several days with no results. The type fuzzer cannot model let-poly due to
the presence of polymorphism, which requires the generator to make parallel choices that must
match up, and CPS-transformed type judgements, which impede its termination heuristics [18].
Bonsai, on the other hand, finds this bug in just over twenty minutes3 , with a counterexample
almost identical to the one presented in literature [55].
6.2

Comparing Bonsai with Pipal

We compare the scalability of Bonsai to the the scalability of Pipal as described by Roberson et al.
[44]. This comparison is only an approximation because Bonsai and Pipal encode different search
spaces (symbolic programs and symbolic intermediate states, respectively). Thus, for example,
2 Our Bonsai model

of stlc+lists, with patchfiles to introduce each bug, is available at https://bitbucket.org/bonsai-checker/
stlc-benchmark/.
3 Our Bonsai model of let-poly-2 is available at https://bitbucket.org/bonsai-checker/let-poly/.

Bonsai: Synthesis-Based Reasoning for Type Systems
Bug
stlc-1
stlc-2
stlc-3
stlc-4
stlc-5
stlc-6
stlc-7
stlc-8
stlc-9
Full suite
let-poly-2

Bonsai (sec)
0.86s
0.99s
0.84s
3s
0.99s
2s
1s
4.6s
1.2s
16s
1200s

Syntax/Bonsai
Time
0.61
56
0.25
1200+
3600+
1000
8
14
0.4
600+
24-hr timeout

1:21

Type/Bonsai

Bonsai

Type/Bonsai

5n
9n
5n
17n
9n
17n
9n
29n
15n

Syntax/Bonsai
Size
1
1
3.6
N/A
N/A
0.76
2
0.88
1.4

1
7.7
0.054
34
40
15
0.07
0.061
0.049
12
Cannot find

47n

N/A

N/A

57
14
51
1.8
14
5.7
19
6.2
13

Table 1. The performance of Bonsai and the syntax and type fuzzers described in the text. Note that fuzzer
statistics are provided as ratios against Bonsai statistics. “+” indicates a lower bound due to a one-hour
timeout. Size is measured in nodes (n) as per the Redex benchmark: “the number of pairs of parentheses
and atoms in the s-expression representation of the term” [45]. Figure 15 (left) represents this data on a
scatter plot. Note that the type fuzzer cannot model let-poly-2 due to polymorphism and CPS-transformed
judgement rules [18].

Bug
stlc-1
stlc-2
stlc-3
stlc-4
stlc-5
stlc-6
stlc-7
stlc-8
stlc-9

Time (sec)
0.92s
1.1s
0.99s
2.7s
1.0s
2.6s
1.2s
4.9s
1.3s

Min. Size
5n
9n
5n
17n
9n
13n*
5n*
21n*
15n

Table 2. The performance of Bonsai on constructing minimal counterexamples. The star (*) indicates that the
minimized counterexample is smaller than the one produced without the minimization query.

Bonsai must model all heap objects, while Pipal must limit the exploration to four heap objects and
n integer literals. Furthermore, the Pipal experiments were performed using different symbolic
execution frameworks and solvers. Nevertheless, Pipal results for comparable trials are listed in
Table 3.
These measurements illustrate that Bonsai and Pipal generally scale to around the same order
of magnitude. Thus, we find that even though Bonsai performs symbolic execution on both the
typechecker and the interpreter, it still has comparable performance to Pipal, which only performs
symbolic execution on the typechecker. That is, compared to Pipal, Bonsai does not sacrifice
efficiency for its versatility and ease-of-use.
6.3

The Bonsai Encoding

Here, we compare the classical “syntax tree” described in Section 3 (with subtree sharing) against
the Bonsai tree. We evaluate the time required to check a type system as a function of the program

1:22

Kartik Chandra and Rastislav Bodik
Benchmark: stlc+lists
250

150
100

Time taken (ms)

200
Timeout (1 hour)

Counterexample Size (n)

Comparison of Classical and Bonsai encodings
Bonsai symbolic execution
Classical symbolic execution
10 7
Bonsai solving
Classical solving
10 6
10 8

Syntax fuzzer
Type fuzzer
Bonsai

10 5
10 4
10 3

50

10 2

0
10

1

100

101
102
Time (log sec)

103

10 1

10 12 10 25 10 50 10 100 10 200 10 400 10 800
# syntactically-valid trees

Fig. 15. Left: Comparing fuzzers and Bonsai on the Redex benchmark. Right: Comparing the classical syntax
tree and Bonsai on verifying the lambda calculus.

space size. We break down the time into symbolic evaluation and solving. We find that the Bonsai
tree scales significantly better than the classical syntax tree, allowing us to explore much larger
search spaces in the same amount of time.
The benchmark. We implemented a simple recursive-descent interpreter for the lambda calculus,
bounded at 4 recursive calls. We then added a ‘typechecker’ that checks for free variables. We
searched for counterexamples using both encodings, with the same typechecker and interpreter.
Thus, the only variable between the trials is the symbolic tree encoding used and its size.
In this setup, there are no possible counterexamples. This is intentional: a satisfiable formula
requires the solver to reach any valid model, whereas an unsatisfiable formula requires the solver
to visit all models and prove that none are satisfiable. Thus, an unsatisfiable formula represents a
more taxing stress test for the solver. In practice, we find that satisfiable queries almost always
take less than half the time that unsatisfiable queries take, and are usually even faster.
Since tree ‘size’ has different meanings for the classical and Bonsai encodings, we normalize by
the number of syntactically valid ASTs represented by a symbolic tree of a given depth.
Results. The graph in Figure 15 (right) shows that the Bonsai encoding allows us to scale to a
much larger number of ASTs than the classical encoding in the same amount of time. For example,
if we impose a time limit of approximately 20 seconds, then the classical encoding explores less
than 1025 ASTs while the Bonsai encoding explores more than 1050 ASTs. Similarly, if we want to
explore 1025 trees, then Bonsai is roughly a thousand times faster than the classical encoding. In our
experience, the classical encoding does not scale to be able to catch most of the counterexamples
discussed in this paper.
Note that the Bonsai encoding consistently spends less time in the solver than the classical
encoding, even though Bonsai pushes the complexity of the formal grammar to the solver. This
suggests that even though Bonsai often creates larger symbolic trees than the classical encoding to
represent the same AST, it has a performance advantage in both symbolic execution and the solver.
In practice, we rarely search ASTs beyond depth 10; smaller trees are always enough to synthesize
counterexamples identified by experts (see Table 3). Nevertheless, we provide data for much larger
trees in this graph to show that the encoding is scalable to much larger spaces if needed.

Bonsai: Synthesis-Based Reasoning for Type Systems
Language
Arithmetic

Description
Typed
arithmetic [41]
Simply-typed λ- From
Recalculus
dex [45], bug
5
Featherweight A minimal core
Java
calculus
for
Java with inheritance [26]
Ownership
Featherweight
Java augmented
Java
with ownership
types [11]

Parameters
depth = 9
no bound
depth = 5
bound = 4

1:23

|S |
104

|ce |
13

tBonsai
1s

t Pipal
0.5s

|S + |
1088

|ce + |
99

t+
11m

104

9

0.97s

—

1021

43

1.7m

# classes = 3
1027
42
3s
2.1s 10119
163 13m
# methods = 3
depth = 6
bound = 7
# classes = 2
1063
72
17s >250s 10342
158 30m
# methods = 4
# owners = 2
depth = 8
bound = 7
NanoDOT
Subset of depen- depth = 10
1019
23
211s
—
1039
49
8m
dent object type obj depth = 6
calculus [5]
no bound
24
175s
—
NanoScala
NanoDOT
Same as Nano- 1020
1064
39 48m
augmented
DOT
with casts and
null
Table 3. An overview of the languages implemented with Bonsai. Here, tBonsai is the time required to catch the
soundness bug described in the text, |ce | is the size of the counterexample measured as in Table 1, and |S | is
the number of syntactically-correct programs explored. t + , |S + |, and |ce + | are analogous, but for long-running
trials. We show relevant comparisons with Pipal where possible.

6.4

Summary of Case Studies

The benchmark. We implemented several different languages with Bonsai, and searched for
counterexamples by planting bugs in the typecheckers. We collected data for the smallest parameters
needed to catch these bugs, as well as for scaled-up trials. The scaled-up trials were run with the
same queries, but parameters modified in order to search larger spaces.
Results. Table 3 lists data collected for several languages implemented with Bonsai. We find
that each of the counterexamples, including those found by experts, can be synthesized by Bonsai
within a few minutes. This suggests that Bonsai is suitable for interactive use while developing a
type system.
Additionally, we find that Bonsai scales to much larger search spaces effectively, searching
through larger, more complex programs. Indeed, the new ‘scaled-up’ counterexamples were often
several times as large as the ‘minimal’ counterexamples. Thus, while bounded model checking is not
a substitute for a formal proof, these results suggest that Bonsai can be used to search through large
spaces of programs efficiently to provide confidence that the type system is most likely sound—or,
alternatively, reveal a large counterexample that may not be found by a human.
Finally, we note that Bonsai performs well on a wide variety of languages, allowing users to easily
implement features such as closures, environments, classes/objects, ownership types, dependent
types, records, and polymorphism in their languages.

1:24
7

Kartik Chandra and Rastislav Bodik

RELATED WORK

Most existing tools for type system designers are focused on checking for soundness bugs. Here,
we discuss the various techniques used to detect such bugs. Empirical evaluations of Bonsai
against these tools are presented in Section 6. Additionally, we discuss additional related work in
theorem-proving and symbolic execution.

7.1

Fuzzing

A type system fuzzer generates random programs and tests them on the typechecker and interpreter
until it finds one that (1) passes the typechecker, and (2) fails in the interpreter. If such a program
is found, it witnesses a soundness bug.
Fuzzing presents serious scalability challenges. Recall Figure 1, which shows a high-level
overview of the fuzzing process. At each step, the parser, typechecker, or interpreter rejects the
vast majority of its inputs, making the probability of a random program witnessing a soundness
error very small. Modern fuzzers address this problem by carefully generating random programs
that are likelier to be counterexamples. For example, syntactic fuzzers such as the one used by PLT
Redex [30] generate random syntactically-valid programs, bypassing the parser. Syntactic fuzzers
have been shown to find a wide variety of bugs in real languages [29]. However, they are still not
scalable enough to catch many simple bugs [18].
A type fuzzer generates random well-typed programs, bypassing both the parser and the typechecker. Type fuzzing can be done in many ways: for example, by using constraint logic programming to express the typechecker declaratively (this has been used to fuzz Rust [15]) or by
generating random type judgment trees and then using that to derive a program (this has been
used to fuzz GHC [18]).
Fuzzing is an effective technique for two reasons. First, a fuzzer can easily check actual implementations of languages. This eliminates the need to formalize the language, and allows users
to catch implementation-dependent bugs that would be missed by a formalization. Second, a
fuzzer produces a concrete counterexample program, which makes it easy to diagnose and fix the
soundness issue. This claim is supported by a recent study, which used NanoMaLy [47] to produce
counterexamples that cause ill-typed ML programs to crash. Students who were given NanoMaLy’s
counterexamples in an exam setting were 10% to 30% more likely to correctly explain and fix the
type error than students who were given only a printout of the compiler error.
However, fuzzers have a critical weakness: by their nature, random fuzzers are non-exhaustive.
If after 24 hours no soundness error has been discovered, we cannot assume that the typechecker
is sound. Indeed, neither syntactic fuzzers nor type fuzzers are able to discover certain simple bugs
in the PLT Redex benchmark [29] after many hours [18], because those bugs are only witnessed by
a small set of programs that are extremely unlikely to be generated randomly.

7.2

Handling non-exhaustiveness with Pipal

One specialized kind of type fuzzer does make some exhaustiveness guarantees. Pipal [43, 44]
requires a typechecker to be encoded as a set of constraints imposed on a finite set of intermediate
program states. At each iteration, Pipal queries a constraint solver for a well-typed state and
performs a single step of evaluation to see whether progress or preservation were violated.
In order to search the space of intermediate states efficiently, Pipal carefully monitors how
the intermediate state was manipulated during the single step of evaluation. If the program is
not a counterexample, Pipal uses this information to add more constraints to the set of programs,
effectively pruning the search space for the next iteration. Eventually, if no counterexample is found,

Bonsai: Synthesis-Based Reasoning for Type Systems

1:25

the solver returns UNSAT, which implies that the search space has been exhaustively checked. That
is, no state within that space witnesses a soundness bug.
While Pipal is scalable, it requires typecheckers to be manually rewritten as a set of declarative
constraints and carefully-formulated invariants on intermediate states. Not only is this tedious for
the user, but it also prevents users from directly checking the implementations of typecheckers. Thus,
Pipal loses one of the primary benefits of fuzzing, which is to check executable implementations
directly.
The Bonsai algorithm, on the other hand, combines the ease-of-use of a fuzzer with the scalability of Pipal. Bonsai uses symbolic execution to automatically convert an executable language
implementation into constraints for a solver, and it directly solves for a counterexample with a
single call to the solver. In this sense, Bonsai may be regarded as a final successor to the type fuzzer,
deriving many of Pipal’s scalability benefits “for free” without any additional effort on the part
of the user. Importantly, Bonsai searches for full executable programs as counterexamples: these
programs are easier to understand than the intermediate states reported by Pipal. Finally, unlike
Pipal’s iterative algorithm, Bonsai makes only one query to the solver. This property allows us to
ask the solver a variety of questions beyond soundness, and is at the heart of Bonsai’s versatility.
7.3

Theorem Proving

If a fuzzer or a bounded model checker fails to find a witness to a soundness bug, then we cannot
claim to have a proof of soundness: there is always the possibility that a program larger than
the bound might expose a bug. In practice, the small-scope hypothesis [6] conjectures that all
soundness bugs will be revealed by small witness programs, and thus for a sufficiently large search
bound the failure to find a counterexample is usually compelling evidence (but not proof) that the
type system is correct.
Unlike fuzzing or bounded model checking, however, a mathematical proof of soundness provides
complete assurance that a type system is sound. Such proofs can be developed manually or
using proof assistants such as [53] and [37]. For instance, Drossopoulou and Eisenbach [17]
prove soundness of a subset of Java manually, while Nipkow and von Oheimb [36] do so using
Isabelle/HOL [37].
Unfortunately, theorem-proving requires a formalized model of the language, such as Featherweight Java [26] for Java and DOT [4] for Scala. Most modern languages are too complex to be
fully formalized, and the models that do emerge often take years of development. Furthermore,
the actual proofs are often long and tedious, requiring significant manual effort. For example, the
mechanized proof of the DOT language [4] using the Coq proof assistant [53] consists of several
thousand lines of code [46], even though the language can be formalized in a couple of pages [5].
We hope that Bonsai may aid in model design in a fashion similar to PLT Redex [29].
7.4

Symbolic execution and synthesis

Bounded verification tools [1, 13, 16, 24, 31, 32, 50, 52, 59] encode the concrete semantics of the
language and translate the program (or just one execution path) into a logical formula. The formula
represents constraints whose solution answers queries about symbolic inputs to the program.
Symbolic execution has become competitive in advanced analysis tasks, such as analysis of highorder contracts [35].
Generation of a counterexample program is related to program synthesis because we can think
of the type system as the specification: the desired program passes the typechecker and fails
in the interpreter. Synthesizers can be roughly divided into three kinds: rewriting [20, 23, 42],
deductive [33, 34, 51], and those based on searching a space of programs with contraint solvers [7,

1:26

Kartik Chandra and Rastislav Bodik

25, 50, 51, 60]. While the first two categories derive a program from a specification, the last category
searches a space of programs, conceptually evaluating each against the specification. This search is
analogous to Bonsai’s search for the counterexample program.
Reducing the path explosion during symbolic evaluation has been previously addressed in
ESC/Java [21] and Rosette [57].
Bonsai trees are a so-called symbolic data structure [8]: despite producing an unusual encoding when symbolically evaluated, they offer programmers the usual AST interface, facilitating
specification of compact (big step) typecheckers and interpreters.
8

CONCLUSION

Bonsai is a type system designer’s assistant, which uses symbolic evaluation to convert typecheckers
and interpreters into constraints. By combining these constraints, Bonsai can query a constraint
solver for programs with specific properties. Such queries can be used to find soundness errors
(including intricate bugs that took experts many years to discover), compare two type systems, find
unnecessary restrictions, and even synthesize simple typechecks automatically.
Bonsai uses a novel data structure to encode sets of abstract syntax trees. This allows it to scale
to extremely large search spaces, while still being fast enough to use interactively while designing a
type system. Together, these results suggest that Bonsai can significantly aid type system designers
in developing novel type systems.
REFERENCES
[1] JavaPathFinder. http://babelfish.arc.nasa.gov/trac/jpf/.
[2] N. Amin and R. Tate. Java and scala’s type systems are unsound: The existential crisis of null pointers. In Proceedings
of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and
Applications, OOPSLA 2016, pages 838–848, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4444-9. doi:
10.1145/2983990.2984004. URL http://doi.acm.org/10.1145/2983990.2984004.
[3] N. Amin and R. Tate. Soundness issue with path-dependent type on ‘null‘ path.
https://issues.scala-lang.org/browse/SI-9633, 2016.
[4] N. Amin, T. Rompf, and M. Odersky. Foundations of path-dependent types. In Proceedings of the 2014 ACM
International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA ’14, pages
233–249, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2585-1. doi: 10.1145/2660193.2660216. URL
http://doi.acm.org/10.1145/2660193.2660216.
[5] N. Amin, S. Grütter, M. Odersky, T. Rompf, and S. Stucki. The Essence of Dependent Object Types, pages 249–272.
Springer International Publishing, Cham, 2016. ISBN 978-3-319-30936-1. doi: 10.1007/978-3-319-30936-1 14. URL
http://dx.doi.org/10.1007/978-3-319-30936-1 14.
[6] A. Andoni, D. Daniliuc, S. Khurshid, and D. Marinov. Evaluating the “small scope hypothesis”. Technical report, MIT
Laboratory for Computer Science, 2003.
[7] D. Angluin and C. H. Smith. Inductive inference: Theory and methods. ACM Comput. Surv., 15(3):237–269, 1983.
[8] R. Bodı́k, K. Chandra, P. M. Phothilimthana, and N. Yazdani. Domain-specific symbolic compilation. In B. S. Lerner,
R. Bodı́k, and S. Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10,
2017, Asilomar, CA, USA, volume 71 of LIPIcs, pages 2:1–2:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2017. ISBN 978-3-95977-032-3. doi: 10.4230/LIPIcs.SNAPL.2017.2. URL https://doi.org/10.4230/LIPIcs.SNAPL.2017.2.
[9] C. Boyapati. SafeJava: A Unified Type System for Safe Programming. PhD thesis, Massachusetts Institute of
Technology, February 2004.
[10] C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In
Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and
Applications, OOPSLA ’02, pages 211–230, New York, NY, USA, 2002. ACM. ISBN 1-58113-471-1. doi:
10.1145/582419.582440. URL http://doi.acm.org/10.1145/582419.582440.
[11] C. Boyapati, B. Liskov, and L. Shrira. Ownership types for object encapsulation. In Proceedings of the 30th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’03, pages 213–223, New York, NY, USA,
2003. ACM. ISBN 1-58113-628-5. doi: 10.1145/604131.604156. URL http://doi.acm.org/10.1145/604131.604156.
[12] W. R. Cook. A proposal for making Eiffel type-safe. Comput. J., 32(4):305–311, July 1989. ISSN 0010-4620. doi:
10.1093/comjnl/32.4.305. URL http://dx.doi.org/10.1093/comjnl/32.4.305.

Bonsai: Synthesis-Based Reasoning for Type Systems

1:27

[13] G. Dennis, F. S.-H. Chang, and D. Jackson. Modular verification of code with SAT. In International Symposium on
Software Testing and Analysis (ISSTA’06), 2006.
[14] K. Dewey, J. Roesch, and B. Hardekopf. Language fuzzing using constraint logic programming. In I. Crnkovic,
M. Chechik, and P. Grünbacher, editors, ACM/IEEE International Conference on Automated Software Engineering, ASE
’14, Vasteras, Sweden - September 15 - 19, 2014, pages 725–730. ACM, 2014. ISBN 978-1-4503-3013-8. doi:
10.1145/2642937.2642963. URL http://doi.acm.org/10.1145/2642937.2642963.
[15] K. Dewey, J. Roesch, and B. Hardekopf. Fuzzing the Rust typechecker using CLP. In Proceedings of the 2015 30th
IEEE/ACM International Conference on Automated Software Engineering (ASE), ASE ’15, pages 482–493, Washington,
DC, USA, 2015. IEEE Computer Society. ISBN 978-1-5090-0025-8. doi: 10.1109/ASE.2015.65. URL
http://dx.doi.org/10.1109/ASE.2015.65.
[16] J. Dolby, M. Vaziri, and F. Tip. Finding bugs efficiently with a sat solver. In 6th International Symposium on the
Foundations of Software Engineering (FSE’07), page 204. ACM, 2007.
[17] S. Drossopoulou and S. Eisenbach. Java is type safe - probably. In In European Conference On Object Oriented
Programming, pages 389–418. Springer-Verlag, 1997.
[18] B. Fetscher, K. Claessen, M. Pa lka, J. Hughes, and R. B. Findler. Making Random Judgments: Automatically Generating
Well-Typed Terms from the Definition of a Type-System, pages 383–405. Springer Berlin Heidelberg, Berlin, Heidelberg,
2015. ISBN 978-3-662-46669-8. doi: 10.1007/978-3-662-46669-8 16. URL
http://dx.doi.org/10.1007/978-3-662-46669-8 16.
[19] B. Fetscher, K. Claessen, M. H. Palka, J. Hughes, and R. B. Findler. Making random judgments: Automatically
generating well-typed terms from the definition of a type-system. In J. Vitek, editor, Programming Languages and
Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on
Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9032 of Lecture Notes in
Computer Science, pages 383–405. Springer, 2015. ISBN 978-3-662-46668-1. doi: 10.1007/978-3-662-46669-8 16. URL
https://doi.org/10.1007/978-3-662-46669-8 16.
[20] B. Fischer and J. Schumann. Autobayes: a system for generating data analysis programs from statistical models. J.
Funct. Program., 13(3):483–508, 2003. ISSN 0956-7968.
[21] C. Flanagan and J. B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In C. Hankin
and D. Schmidt, editors, Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, London, UK, January 17-19, 2001, pages 193–205. ACM, 2001. ISBN 1-58113-336-7. doi:
10.1145/360204.360220. URL http://doi.acm.org/10.1145/360204.360220.
[22] M. Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010-1, PLT Design Inc., 2010.
https://racket-lang.org/tr1/.
[23] M. Frigo and S. G. Johnson. The design and implementation of FFTW3. Proceedings of the IEEE, 93(2):216–231, 2005.
Special issue on “Program Generation, Optimization, and Platform Adaptation”.
[24] J. Galeotti, N. Rosner, C. Pombo, and M. Frias. Analysis of invariants for efficient bounded verification. In 2010
International Symposium on Software Testing and Analysis (ISSTA’10), 2010.
[25] S. Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL, pages 317–330, 2011.
[26] A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Proceedings of
the 14th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA
’99, pages 132–146, New York, NY, USA, 1999. ACM. ISBN 1-58113-238-7. doi: 10.1145/320384.320395. URL
http://doi.acm.org/10.1145/320384.320395.
[27] J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385–394, 1976. ISSN 0001-0782.
[28] C. Klein, J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen, M. Flatt, J. A. McCarthy, J. Rafkind, S. Tobin-Hochstadt,
and R. B. Findler. Run your research: on the effectiveness of lightweight mechanization. In J. Field and M. Hicks,
editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 285–296. ACM, 2012. ISBN 978-1-4503-1083-3. doi:
10.1145/2103656.2103691. URL http://doi.acm.org/10.1145/2103656.2103691.
[29] C. Klein, J. Clements, C. Dimoulas, C. Eastlund, M. Felleisen, M. Flatt, J. A. McCarthy, J. Rafkind, S. Tobin-Hochstadt,
and R. B. Findler. Run your research: On the effectiveness of lightweight mechanization. In Proceedings of the 39th
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pages 285–296, New
York, NY, USA, 2012. ACM. ISBN 978-1-4503-1083-3. doi: 10.1145/2103656.2103691. URL
http://doi.acm.org/10.1145/2103656.2103691.
[30] C. Klein, M. Flatt, and R. B. Findler. The racket virtual machine and randomized testing. Higher Order Symbol.
Comput., 25(2-4):209–253, Dec. 2012. ISSN 1388-3690. doi: 10.1007/s10990-013-9091-1. URL
http://dx.doi.org/10.1007/s10990-013-9091-1.
[31] A. S. Köksal, V. Kuncak, and P. Suter. Constraints as control. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT
symposium on Principles of programming languages, POPL ’12, pages 151–164, New York, NY, USA, 2012. ACM. ISBN

1:28

Kartik Chandra and Rastislav Bodik

978-1-4503-1083-3. doi: 10.1145/2103656.2103675. URL http://doi.acm.org/10.1145/2103656.2103675.
[32] D. Kroening. CBMC. http://www.cprover.org/cbmc/.
[33] N. Mateev, K. Pingali, P. Stodghill, and V. Kotlyar. Next-generation generic programming and its application to sparse
matrix computations. In Proceedings of ICS’00, pages 88–99.
[34] J. McDonald and J. Anton. SPECWARE - producing software correct by construction. Technical Report KES.U.01.3.,
2001.
[35] P. C. Nguyen, S. Tobin-Hochstadt, and D. V. Horn. Higher-order symbolic execution for contract verification and
refutation. CoRR, abs/1507.04817, 2015. URL http://arxiv.org/abs/1507.04817.
[36] T. Nipkow and D. von Oheimb. Java`iдht is type-safe — definitely. In Proc. 25th ACM Symp. Principles of
Programming Languages, pages 161–170. ACM Press, 1998.
[37] T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag,
Berlin, Heidelberg, 2002. ISBN 3-540-43376-7.
[38] M. Odersky. We got liftoff! The Dotty compiler for Scala bootstraps.
http://www.scala-lang.org/blog/2015/10/23/dotty-compiler-bootstraps.html, 2015.
[39] M. Odersky. Scaling DOT to Scala - soundness. http://scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html,
2016.
[40] M. Odersky and al. An overview of the Scala programming language. Technical Report IC/2004/64, EPFL, Lausanne,
Switzerland, 2004.
[41] B. C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. ISBN 0262162091, 9780262162098.
[42] M. Püschel, J. M. F. Moura, J. Johnson, D. Padua, M. Veloso, B. Singer, J. Xiong, F. Franchetti, A. Gacic, Y. Voronenko,
K. Chen, R. W. Johnson, and N. Rizzolo. SPIRAL: Code generation for DSP transforms. Proceedings of the IEEE, special
issue on “Program Generation, Optimization, and Adaptation”, 93(2):232– 275, 2005.
[43] M. Roberson and C. Boyapati. Efficient modular glass box software model checking. In Proceedings of the ACM
International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’10, pages
4–21, New York, NY, USA, 2010. ACM. ISBN 978-1-4503-0203-6. doi: 10.1145/1869459.1869461. URL
http://doi.acm.org/10.1145/1869459.1869461.
[44] M. Roberson, M. Harries, P. T. Darga, and C. Boyapati. Efficient software model checking of soundness of type
systems. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and
Applications, OOPSLA ’08, pages 493–504, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-215-3. doi:
10.1145/1449764.1449803. URL http://doi.acm.org/10.1145/1449764.1449803.
[45] B. F. Robert Bruce Findler, Casey Klein and M. Felleisen. Redex: Practical Semantics Engineering, 2017. URL
http://docs.racket-lang.org/redex/index.html.
[46] T. Rompf and N. Amin. From F to DOT: Type soundness proofs with definitional interpreters. Technical report,
Purdue University and EPFL, 2016.
[47] E. L. Seidel, R. Jhala, and W. Weimer. Dynamic witnesses for static type errors. In 21st ACM SIGPLAN International
Conference on Functional Programming, 2016. URL http://eric.seidel.io/pub/nanomaly-icfp16.pdf.
[48] K. Sen, S. Kalasapur, T. G. Brutch, and S. Gibbs. Jalangi: a selective record-replay and dynamic analysis framework for
javascript. In B. Meyer, L. Baresi, and M. Mezini, editors, Joint Meeting of the European Software Engineering
Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint
Petersburg, Russian Federation, August 18-26, 2013, pages 488–498. ACM, 2013. doi: 10.1145/2491411.2491447. URL
http://doi.acm.org/10.1145/2491411.2491447.
[49] K. Sen, G. C. Necula, L. Gong, and W. Choi. Multise: multi-path symbolic execution using value summaries. In E. D.
Nitto, M. Harman, and P. Heymans, editors, Proceedings of the 2015 10th Joint Meeting on Foundations of Software
Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015, pages 842–853. ACM, 2015. doi:
10.1145/2786805.2786830. URL http://doi.acm.org/10.1145/2786805.2786830.
[50] A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. In
Proceedings of the 12th international conference on Architectural support for programming languages and operating
systems, ASPLOS XII, pages 404–415, New York, NY, USA, 2006. ACM. ISBN 1-59593-451-0. doi:
10.1145/1168857.1168907. URL http://doi.acm.org/10.1145/1168857.1168907.
[51] S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In POPL, 2010.
[52] M. Taghdiri. Automating Modular Program Verification by Refining Specifications. PhD thesis, Massachusetts Institute
of Technology, 2007.
[53] The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. URL http://coq.inria.fr.
Version 8.0.
[54] M. Tofte. Type inference for polymorphic references. Inf. Comput., 89(1):1–34, 1990. doi:
10.1016/0890-5401(90)90018-D. URL https://doi.org/10.1016/0890-5401(90)90018-D.

Bonsai: Synthesis-Based Reasoning for Type Systems

1:29

[55] M. Tofte. Type inference for polymorphic references. Inf. Comput., 89(1):1–34, Sept. 1990. ISSN 0890-5401. doi:
10.1016/0890-5401(90)90018-D. URL http://dx.doi.org/10.1016/0890-5401(90)90018-D.
[56] E. Torlak. The Rosette Guide. University of Washington, 2016. URL
http://emina.github.io/rosette/doc/rosette-guide/index.html.
[57] E. Torlak and R. Bodı́k. A lightweight symbolic virtual machine for solver-aided host languages. In ACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11,
2014, page 54, 2014. doi: 10.1145/2594291.2594340. URL http://doi.acm.org/10.1145/2594291.2594340.
[58] E. Torlak and R. Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the
35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, pages 530–541, New
York, NY, USA, 2014. ACM. ISBN 978-1-4503-2784-8. doi: 10.1145/2594291.2594340. URL
http://doi.acm.org/10.1145/2594291.2594340.
[59] E. Torlak, M. Vaziri, and J. Dolby. MemSAT: Checking axiomatic specifications of memory models. In Programming
Language Design and Implementation (PLDI’10), pages 341–350, 2010.
[60] M. T. Vechev, E. Yahav, and D. F. Bacon. Correctness-preserving derivation of concurrent garbage collection
algorithms. In PLDI, pages 341–353, 2006.
[61] A. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38–94, Nov. 1994. ISSN
0890-5401. doi: 10.1006/inco.1994.1093. URL http://dx.doi.org/10.1006/inco.1994.1093.
[62] X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in c compilers. In Proceedings of the 32Nd
ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 283–294, New York,
NY, USA, 2011. ACM. ISBN 978-1-4503-0663-8. doi: 10.1145/1993498.1993532. URL
http://doi.acm.org/10.1145/1993498.1993532.
[63] A. Zeller. Yesterday, my program worked. today, it does not. why? In O. Nierstrasz and M. Lemoine, editors, Software
Engineering - ESEC/FSE’99, 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT
Symposium on the Foundations of Software Engineering, Toulouse, France, September 1999, Proceedings, volume 1687 of
Lecture Notes in Computer Science, pages 253–267. Springer, 1999. ISBN 3-540-66538-2. doi: 10.1007/3-540-48166-4 16.
URL https://doi.org/10.1007/3-540-48166-4 16.

