Inferring SQL Queries Using Program Synthesis
Alvin Cheung

Armando Solar-Lezama

Samuel Madden

arXiv:1208.2013v1 [] 9 Aug 2012

MIT CSAIL
{akcheung,asolar,madden}@csail.mit.edu

Abstract
Developing high-performance applications that interact with databases
is a difficult task, as developers need to understand both the details
of the language in which their applications are written in, and also
the intricacies of the relational model. One popular solution to this
problem is the use of object-relational mapping (ORM) libraries
that provide transparent access to the database using the same language that the application is written in. Unfortunately, using such
frameworks can easily lead to applications with poor performance
because developers often end up implementing relational operations in application code, and doing so usually does not take advantage of the optimized implementations of relational operations,
efficient query plans, or push down of predicates that database systems provide.
In this paper we present Q BS, an algorithm that automatically
identifies fragments of application logic that can be pushed into
SQL queries. The Q BS algorithm works by automatically synthesizing invariants and postconditions for the original code fragment.
The postconditions and invariants are expressed using a theory of
ordered relations that allows us to reason precisely about the contents and order of the records produced even by complex code fragments that compute joins and aggregates. The theory is close in expressiveness to SQL, so the synthesized postconditions can be readily translated to SQL queries. Using 40 code fragments extracted
from over 120k lines of open-source code written using the Java
Hibernate ORM, we demonstrate that our approach can convert a
variety of imperative constructs into relational specifications.

1. Introduction
Almost all modern, interactive web applications store their persistent state in a relational database. Developing such database-backed
applications is complicated because databases are frequently accessed using SQL, while most application programs are written in
a high-level, often imperative, language such as Java or Python.
These languages usually provide APIs to connect to databases and
allow developers to retrieve and store persistent data by embedding SQL queries within their application code. Unfortunately, this
approach has a number of issues. First, because the developer expresses her queries in SQL, she is forced to learn a different programming language (and often a different programming paradigm)
in order to work with the database. Second, developers must flatten
objects into relational tables, and marshall and unmarshall objects
into SQL queries and out of query results. Third, this approach
breaks the abstraction barrier between the database and application programs, since changes to the object hierarchy might involve
changes to the embedded SQL queries or schemas.
A popular approach to address this so-called “impedance mismatch” between imperative and declarative interfaces is to use systems that allow developers to access database and non-database objects with the same general purpose language that the application
is written in. This notion is sometimes referred to as transparent

1

persistence and implemented in object-oriented databases [23], and
object-relational mappings (ORM) libraries such as Hibernate [3]
and JPA [2]. To use such libraries, the developer first designs objects that are intended to be persistently stored in a database using
special annotations or external mapping files. The library provides
a tool that takes in the user’s design and creates the appropriate
tables in the database, and abstracts the SQL queries that retrieve
and update persistent objects in the database as API calls that the
application can invoke.
Thus, the developer neither needs to learn a separate programming model nor understand how the database processes the queries
that are issued by the application. Such libraries have become extremely popular; for example, as of July, 2012, on the job board
dice.com 15% of the 17,000 Java developer jobs are for programmers with Hibernate experience.
Although popular, such frameworks often lead to inefficient
use of the database. This is because developers often end up implementing many relational operations—e.g., filters, joins, and
aggregates—in application code using loops over a set of records
retrieved earlier from the database. This is due to programmers’
lack of knowledge about relational operations, and/or because the
interfaces for accessing complex relational operations are difficult
to use in these languages. Running such operations in the application is very inefficient, because it does not allow databases to
effectively optimize queries by using specialized operators or indices, and can result in shipping a large amount of unnecessary
data to the application. For example, database systems often have
a number of join implementations and can select the best one depending on the size and ordering of the input tables. In contrast,
programmers using ORMs often implement application-level joins
with nested loops, which can be several orders of magnitude slower
than a database’s optimized join implementations as our measurements show. In fact, anecdotal evidence suggests that when application performance becomes critical, developers using ORM layers
often by-pass the ORM and access the database directly by issuing queries encoded with strings via its native SQL or SQL-like
interface—often provided as a “backdoor” by the ORM libraries.
In this paper, we develop a new compiler analysis algorithm,
Q BS (Query By Synthesis), that allows developers using transparent persistence frameworks to continue writing applications as
usual, implementing logic that could be pushed into the database in
the application. Then, the Q BS algorithm analyzes the code and automatically converts portions of it into SQL expressions that run in
the database. Our algorithm retains the best of both worlds: developers do not need to understand the intricacies of SQL but can still
develop efficient applications. This problem statement is not new:
Cook et al. [32, 33] first identified this as the query extraction problem in a seminal 2007 POPL paper. Our paper significantly expands
on this prior work by extending the subset of source programs that
can be analyzed, and the expressiveness of the SQL queries that
are generated. Specifically, to the best of our knowledge, our work
is the first that is able to identify joins and aggregates in general

2012/8/10

purpose application logic and convert them to SQL queries. Our
analysis ensures that the generated queries are precise in that both
the contents and the order of records in the generated queries are
the same as that produced by the original code.
Our basic approach is to infer an SQL expression that is semantically equivalent to a given block of imperative code, and to replace the imperative code fragment with the inferred SQL expression. The key idea is to recognize that this problem is equivalent
to coming up with a postcondition for the imperative code block
that can be translated into SQL. Our approach follows the classical results from axiomatic semantics [13] to compute verification
conditions for the imperative code fragment symbolically in terms
of the unknown postconditions and loop invariants. The resulting
formula is fed to a constraint-based synthesis engine to solve for
the unknown postconditions and invariants. Our synthesis approach
generates postconditions and invariants using a carefully designed
predicate language that can be readily compiled to SQL. If a postcondition can be found that makes the verification condition valid,
then the corresponding imperative code fragment is converted into
its relational specification in SQL.
In summary, this paper makes the following contributions:
1. We designed a predicate language that is based on a new theory of ordered relations that we developed. The language is designed to bridge the gap between the imperative and relational
worlds. Ordered relations are similar to standard relations, except that each record in the ordered relation is indexed. The theory is expressive enough to model various relational operations,
and at the same time allows us to infer relational specifications
for a variety of imperative program constructs. Using the theory, we are able to prove that the transformations are sound and
fully precise.
2. Based on the theory, we develop the Q BS algorithm based
on automatic program verification. The algorithm takes in a
code fragment written in an imperative language that uses an
ORM library to retrieve records from database, automatically
generates a relational specification from it, and converts it into
an SQL query. Our technique solves the postcondition and loop
invariant inference problem by analyzing the input program
and inferring a grammar that describes the likely structure of
the unknown predicates. This structural hypothesis is fed to a
constraint-based synthesizer [28] that finds predicates that are
likely to be correct based on bounded analysis. Our technique
then uses Z3 [5] to prove that the verification condition is valid
with respect to our theory of ordered relations.
3. We implemented a prototype of our algorithm and evaluated
it on Java programs that use the Hibernate ORM library for
data persistence operations. We demonstrate the feasibility of
our algorithm by inferring relational specifications from 40
different real-world code examples. The experiments show that
our algorithm is able to infer significantly more classes of
relational specifications compared to what was possible with
prior work.
More generally, our system demonstrates the use of constraintbased synthesis technology to provide a general solution to what
had been previously considered a difficult compiler analysis problem, and the theory that we developed also provides a new way to
reason about relational operations in an imperative context.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

List<User> getRoleUser () {
List<User> listUsers = new ArrayList<User>();
List<User> users = this.userDao.getUsers();
List<Role> roles = this.roleDao.getRoles();
for (int i = 0; i < users.size(); i++) {
for (int j = 0; j < roles.size(); j++) {
if (users.get(i).roleId().equals(roles.get(j).roleId())) {
User userok = users.get(i);
listUsers.add(userok);
}
}
}
return listUsers;
}

Figure 1. Sample code that implements join operation in application code, abridged from actual source for clarity
Postcondition
listUsers = π(sort(σ(⊲⊳ (users, roles, True), fσ ), lsort ), fπ )
where
fσ := get(users, i ).roleId = get(roles, j).roleId
fπ projects all the fields from the User class
lsort = [users, roles]

1
2
3
4
5
6
7

Translated code
List<User> getRoleUser () {
List<User> listUsers = db.executeQuery(
"SELECT u
FROM users u, roles r
WHERE u.roleId == r.roleId
ORDER BY u.roleId, r.roleId");
return listUsers; }

Figure 2. Postcondition as inferred from Fig. 1 and code after
query transformation

In this example, the method getRoleUser is used to return the
list of users whose role is currently stored in the database. It first
populates the list users on line 3 using a call to the Hibernate
library to retrieve all User objects that are currently stored in the
database, and similarly for the roles list. The code then iterates
through two loops to compare each user against each role, and adds
those users that pass the criteria to listUsers on line 9. Finally, this
list is returned as the result of the function.
While the example implements the desired functionality and is
easy to read, it performs poorly. First, when the method is executed,
the ORM library needs to fetch all the records from the corresponding tables that store User and Role objects using a SQL query, marshall each record into a Java object, and return the results to the
user application as lists. However, since only a subset of users (and
none of roles) are actually returned, resources are wasted in fetching and marshalling the extra database records that are not needed.
This problem is exacerbated when the sizes of the Users and Roles
relations are large when compared to the size of the returned results. Meanwhile, notice that getRoleUser essentially implements
a relational join and projection operation in application code, but
without utilizing indices or efficient join algorithms the database
system may have access to.
The goal of the Q BS algorithm is to compile the application to
the code shown in the bottom of Fig. 2, where the nested loop is
converted to a SQL query that implements the same functionality
that is assigned to the variable listUsers as in the original code.
The algorithm works by first identifying the program variable that
the results from the inferred query should be assigned to (in the
case of the running example it is listUsers) — we refer this as

2. Overview
In this section we describe the overall operations of the Q BS algorithm, starting with an example of it running on an excerpt from
an open source project management application [4] written using
the Hibernate framework. Figure 1 shows the code fragment for the
example.

2

2012/8/10

the “postcondition variable.” In the current implementation we
mark either the return value of the input code fragment as the
postcondition variable, or ask the user to indicate the result variable
that our algorithm should be applied to using a special annotation
(inferring the postcondition variable automatically is a topic for
future work). The body of the function prior to the location where
the postcondition variable is marked is then considered for SQL
transformation. We currently assume that all database records that
are used in the code fragment to be analyzed are fetched by the
code fragment. For example, we assume that they are not passed in
as function parameters.
Once we have identified the block of code we are going to infer
an equivalent SQL query for, we need to infer an expression for
the postcondition variable that is implied by the code fragment
and is translatable to SQL. In the case of the running example, the
translated result is shown in line 3 in Fig. 2. We describe these steps
in more detail in the rest of this section.

database. Similarly, we only need to discover loop invariants that
are strong enough to prove the postcondition of interest. This insight greatly reduces the space of solutions that we need to consider and also shortens the time needed to find a solution, as our
experiments show in Sec. 8.
Validation and SQL conversion. Once the synthesizer finds a solution to the postconditions and invariants in the verification conditions, the candidates are sent to a theorem prover for verification,
since the synthesizer used in our algorithm is only able to perform
bounded verification. If the prover returns a positive answer, the input program is translated to SQL, as shown in the bottom of Fig. 2.
The predicate language defines rules to translate any expressions
in the language into valid SQL. The details of validation is discussed in Sec. 7 while the rules for SQL conversion are introduced
in Sec. 3.4.
We now turn to a discussion of the theory of ordered relations,
which form the basis of our approach. Once we have presented this
theory, we describe the above steps in more detail, and evaluate our
approach.

Conversion to kernel language representation. Given the input
code fragment, the first step in the Q BS algorithm is to convert the
code fragment into a simplified kernel language. The description of
the kernel language and the process of translation from Java source
into this language are discussed in Sec. 4.

3. Theory of Finite Ordered Relations
The theory used to reason about the postconditions and invariants
in the imperative code is central to our ability to infer relational
specifications from imperative programs. The theory must allow
precise analysis of the imperative code to enable reasoning about
both the set of records produced and the ordering of records. This
is important since many source languages (such as Java) expose
an ordered list interface to manipulate records retrieved from the
database, and subsequent operations in the client code might rely
on the order in which the records are returned.
There are other ways to model relational operations in imperative code (see Sec. 9 for details). However, they are either limited in
expressiveness for reasoning about order-preserving relational operations, or cannot be easily translated to SQL. In this section, we
describe a new theory of finite ordered relations that the Q BS algorithm uses along with the translation of the operators in the theory
into SQL queries.

Generation of verification conditions. As the next step, we compute the verification conditions of the program expressed in the kernel language, without assuming any preconditions when the code
fragment is entered. The verification conditions are written using
the predicate language derived from the theory of ordered relations to be discussed in Sec. 3, and the procedure used to compute verification conditions is a fairly standard one [13, 16]. The
interesting point here is that at this point we do not know what the
postcondition and loop invariants (if any) are. Thus, during this initial verification process we symbolically represent the verification
conditions in terms of unknown invariants and postcondition. The
process of computing verification conditions is discussed in more
detail in Sec. 5.
Synthesis of invariants and postcondition. The definitions of the
postcondition and invariants need to be filled in and validated before translation can proceed. We do this using a synthesis-based
approach that is similar to [29], where we use a synthesizer to
come up with a postcondition that is implied by the computed
verification conditions. During synthesis, the synthesizer performs
bounded verification on the postcondition candidates and only returns those that can be successfully verified. To prevent the synthesizer from generating trivial postconditions (such as True), we
limit the synthesizer to only generate postconditions that can be
translated to SQL, as defined by our theory of ordered relations. If
there are loops in the input code fragment, we ask the synthesizer
to generate loop invariants as well. We provide a template, written in the predicate language, that describes the space of possible
postcondition and invariants to the synthesizer. For instance, from
the example shown in Fig. 1, our algorithm infers the postcondition
shown at the top of Fig. 2, where sort, π, σ, and ⊲⊳ refers to sorting,
relational projection, selection, and join, respectively. The process
of automatic template generation from the input code fragment and
synthesis of the postcondition from the template are discussed in
Sec. 6.
Determining loop invariants is undecidable for arbitrary programs in general [7]. In our case, however, we do not need to determine the strongest invariants or postconditions: we are only interested in finding postconditions that allow us transform the input
program into an SQL expression. In the case of the running example, we are only interested in finding a postcondition of the form
listUsers = Query(q), where q is a SQL query to be issued to the

3.1 Basics
The theory of finite ordered relations is based on the theory of lists
with standard list operations. The theory operates on three types
of values: scalars, records, and ordered relations of finite length.
Records are collections of named fields, and an ordered relation
is a finite list of records. Each record in the relation is labeled
with an integer index that can be used to fetch the record. The
theory defines a number of operators that can be used to manipulate
ordered relations. Figure 3 presents the abstract syntax of the theory
and shows how to combine operators to form expressions. The
theory assumes that all the operators are applied to values of the
right type.
The operators introduced in the language mirror the operators of
standard relational algebra. The operators fall into two categories:
those that return an ordered relation, and those that return a single
record. The first group includes projection of fields from records
(π), selection of records (σ), joining of ordered relations (⊲⊳), sort,
unique, and top. Those that return a single record include get, size,
contains, max, min, and sum. The expression Query represents the
original query; it retrieves records from the database and returns
them as an ordered relation.
3.2 Axioms
The semantics of the operators in the theory are defined recursively
by the axioms in Fig. 4. The operator size(r ) returns the number of
records in relation r , and get(r , i) returns the record that is stored

3

2012/8/10

projection (π)
π([ ], f ) = [ ]

size
size([ ]) = 0

π(h : t, f ) = f (h) : π(t, p)

size(r ) = 1 + size(tail(r ))
selection (σ)
get

i =0
i >0
get(r , i )

→
→
=

σ([ ], f ) = [ ]

getHelper(h : t, i ) = h
getHelper(h : t, i ) = getHelper(t, i − 1)
getHelper(r , size(r ) − i − 1)

f (h) = True
f (h) = False

→
→

σ(h : t, f ) = h : σ(t, f )
σ(h : t, f ) = σ(t, f )
sum

append
append([ ], r ) = r
append(r , e) = r : e

sum([ ]) = 0

max
max([ ]) = −∞

top
top([ ], i ) = [ ]

sum(h : t) = h + sum(t)

append(h : t, r ) = h : append(t, r )
append([ ], e) = [e]

h > max(t)
h ≤ max(t)

top(r , i ) = top(tail(r ), i − 1) : get(r , i − 1)

→
→

join (⊲⊳)
⊲⊳ (r , [ ], f ) = [ ]
⊲⊳ ([ ], r , f ) = [ ]

max(h : t) = h
max(h : t) = max(t)
min

⊲⊳ (h : t, r , f ) = ⊲⊳l (h, r ) : ⊲⊳ (t, r , f )
⊲⊳ (r , h : t, f ) = ⊲⊳r (r , h) : ⊲⊳ (r , t, f )

f (h, e) = True
f (h, e) = False

→
→

⊲⊳l (h : t, e, f ) = (h, e) : ⊲⊳l (t, e, f )
⊲⊳l (h : t, e, f ) = ⊲⊳l (t, e, f )

f (e, h) = True
f (e, h) = False

→
→

⊲⊳r (e, h : t, f ) = (e, h) : ⊲⊳r (e, t, f )
⊲⊳r (e, h : t, f ) = ⊲⊳r (e, t, f )

min([ ]) = ∞
h < min(t)
h ≥ min(t)

→
→

min(h : t) = h
min(h : t) = min(t)

contains
contains(e, [ ]) = False
e=h
e 6= h

→
→

contains(e, h : t) = True
contains(e, h : t) = contains(e, t)

Figure 4. Axioms in the theory of ordered relations
c ∈ constant
e ∈ expression

fπ (e)
fσ (es )
f⊲⊳ (e1 , e2 )
op ∈ binary op

::=
::=
|
|
|
|
|
::=
::=
::=
::=

predicate either compares the value of a record field and a constant,
the values of two record fields, or checks if the record is contained
in another relation using contains.
The ⊲⊳ operator implements the relational join operation between two ordered relations. The operator iterates over each record
h1 from the first relation and pairs that with each record h2 from the
second relation. The two records are passed to the boolean function
f⊲⊳ , and the pair is added to the resulting relation if f⊲⊳ returns True.
f⊲⊳ is similar to fσ , except that it is a conjunction of boolean predicates of the form e1 .fi op e2 .fj , i.e., each predicate compares values
of one of the fields from the first relation to another field from the
other relation. The axioms that define the aggregate operators max,
min, and sum assume that the input relation contains only one numeric field, namely the field to aggregate upon.
The definitions of unique and sort are standard; in the case of
sort, the second argument is a list of fields to sort by. Our system
does not actually reason about these two operations in terms of
their definitions; instead it treats them as uninterpreted functions
with certain algebraic properties outlined in the following section.
Because of this, there are some formulas involving sort and unique
that we cannot prove, but we have not found this to be significant
in practice (see Sec. 8 for details).

True | False | number literal | string literal
c | program var | {fi = ei } | e1 op e2 | ¬ e
[ ] | Query(...) | size(e) | get(er , es )
top(er , es ) | π(e, fπ ) | σ(e, fσ )
⊲⊳ (e1 , e2 , f⊲⊳ ) | append(e1 , e2 )
sort(e, [e.fi ]) | unique(e)
sum(e) | max(e) | min(e)
{e.fi }
∧ e.fi op c | e.fi op e.fj | contains(es , e)
∧ e1 .fi op e2 .fj
∧| ∨ | > | < | ≥ | ≤ | =

Figure 3. Abstract syntax for the predicate language based on the
theory of ordered relations
at index i of relation r . append(r1 , r2 ) inserts relation r2 at the end
of r1 and returns a new ordered relation. top(r , i) returns a relation
containing the first i − 1 records in the relation r .
The axioms for π, σ and ⊲⊳ are modeled after relational projection, selection, and join respectively, but they also define an order
for the records in the output relation relative to those in the input
relations. The π operator performs projection of fields from an ordered relation. The operator passes each record in the relation to
the function fπ , which selects a number of fields and creates a new
record using those fields. Just like the equivalent operation in relational algebra, the same field can be replicated multiple times; fπ
simply renames the new fields as needed. The σ operator uses a
function fσ to filter records from the input relation. fσ is a boolean
function defined as a conjunction of boolean predicates, where each

3.3 Operator Equivalence
The axioms that define the basic operations imply a number of
properties that will be useful when translating expressions in the
predicate language into SQL.
Theorem 1 (Operator Equivalence). The following equivalences
hold, both in terms of the contents of the relations and also the
ordering of the records in the relations:

4

2012/8/10

σ(π(r , fπ ), fσ ) = π(σ(r , fσ ), fπ )
σ(σ(r , fσ1 ), fσ2 ) = σ(r , f ′ ), where f ′ = fσ2 ∧ fσ1
top(σ(r , f ), e) = σ(top(r , e), f )
π(π(r , fπ1 ), fπ2 ) = π(r , f ′ ), where f ′ is the concatenation of
all the fields in fπ1 and fπ2 .
• top(π(r , f ), e) = π(top(r , e), f )
• top(top(r , e1 ), e2 ) = top(r , max(e1 , e2 ))
• ⊲⊳ (r1 , r2 , f⊲⊳ ) = σ(⊲⊳ (r1 , r2 , True), f⊲⊳ ), i.e., joins can be
converted into cross products with selections.
• ⊲⊳ (sort(r1 , l1 ), sort(r2 , l2 ), f ) = sort(⊲⊳ (r1 , r2 , f ), l1 : l2 )
• ⊲⊳ (π(r1 , fπ1 ), π(r2 , fπ2 ), f ) = π(⊲⊳ (r1 , r2 , f ), f ′ ), where f ′
is the concatenation of all the fields in fπ1 and fπ2 .

Let si = π(sort(σ(b, fσi ), lsorti ), fπi ). Trans is defined on expressions
whose subexpressions (if any) are in translatable form, so we have to
consider cases where the sub-expressions are either s or top(s). Each case
is defined below.
Query(...)

Except for the equivalences involving sort, the other ones can
be proven easily from the axiomatic definitions.

where f ′ is the composition of fπ and fπ2 .

•
•
•
•

Trans(Query(...))) = π(sort(σ(Query(...), True), [ ]), f )
where f projects all the fields from the input relation.
π(t, fπ2 )
Trans(π(s, fπ2 ))

=

π(sort(σ(b, fσ ), lsort ), f ′ )

Trans(π(top(s, e), fπ2 ))

=

top(π(sort(σ(b, fσ ), lsort ), f ′ ), e)

σ(t, fσ2 )

3.4 Translating to SQL
Trans(σ(s, fσ2 ))
Trans(σ(top(s, e), fσ ))

The expressions defined in the predicate grammar can be converted
into semantically equivalent SQL queries. In this section we prove
that any expression that does not use append or unique can be
compiled into an equivalent SQL query. We prove this in two
steps; first, we define translatable expressions and show that any
expression that does not use append or unique can be converted
into a translatable expression using the equivalences in Thm. 1.
Then we show how to produce SQL from translatable expressions.

⊲⊳ (t1 , t2 , f⊲⊳ )
Trans(⊲⊳ (s1 , s2 , f⊲⊳ ))
′
= π(sort(σ(⊲⊳ (b1 , b2 , True), fσ′ ), lsort
), fπ′ )
′
= lsort1 : lsort2 ,
where fσ′ = fσ1 ∧ fσ2 ∧ f⊲⊳ , lsort
and fπ′ is the concatenation of the fields from fπ1 and fπ2 .

Definition 1 (Translatable Expressions). The following grammar
defines the set of expressions that can be directly translated into
SQL:

Trans(⊲⊳ (top(s1 , e), top(s2 , e)))
= π(sort(σ(⊲⊳ (top(s1 , e), top(s2 , e)), True), [ ]), id)

b ∈ baseExp
s ∈ sortedExp

::=
::=

Query(...) | top(s, e) | ⊲⊳ (b1 , b2 , True) | agg(t)
π(sort(σ(b, fσ ), [e.fi ]), fπ )

t ∈ translatableExp

::=

s | top(s, e)

Trans(top(s, e))

=

top(s, e)

Trans(top(top(s, e1 ), e2 ))

=

top(s, e ′ )

where

Theorem 2 (Completeness of Translation Rules). All expressions in the predicate grammar in Fig. 3, except for those that
contain any append or unique operators, can be converted into
translatable expressions.

e′

is the maximum value of e1 and e2 .
agg(t)

Trans(agg(s))
Trans(agg(top(s, e)))

=
=

π(sort(σ(agg(s), True), [ ]), id)
π(sort(σ(agg(s), True), [ ]), id)

where id is the identity mapping from input to output record.

Proof. We prove the theorem by defining an algorithm to perform
the conversion. The algorithm is defined in terms of a function
Trans defined in Fig. 5. The function takes in an expression whose
sub-expressions are all translatable expressions and produces an
equivalent translatable expression. By applying this function to the
AST of an arbitrary expression that does not use append or unique
in a bottom up manner, one can convert the expression into an
equivalent translatable one.
The equivalences in Thm. 1 can be used to prove that Trans is
semantics preserving. For example, for Trans(σ(s, fσ2 )):
=
=
=
=

where id is the identity mapping from input to output record.
top(t, e)

where the term agg in the grammar denotes any of the aggregation
operators (min, max, sum, size), and the other operators are the
same as those presented in Fig. 3.

σ(s, fσ2 )

π(sort(σ(b, fσ ∧ fσ2 ), lsort ), fπ )
top(π(sort(σ(b, fσ ∧ fσ2 ), lsort ), fπ ), e)

=
=

sort(t)
Trans(sort(s, lsort ))

=

Trans(sort(top(s, e))

=

where

′
π(sort(σ(b, fσ ), lsort
), fπ )
′
top(π(sort(σ(b, f ), lsort
), fπ ), e)
′
lsort

= ls : lsort .

Figure 5. Definition of Trans
Translatable expressions to SQL. Following the syntax-directed
rules in Fig. 6, it is possible to convert any translatable expression
into an equivalent SQL expression. Most of the rules in Fig. 6 are
direct translations from the operators in the theory into their SQL
equivalents.
One important aspect of the translation is the way that ordering
of records is preserved. Ordering is problematic because although
the operators in the theory define the order of the output in terms
of the order of their inputs, SQL queries are not guaranteed to
preserve the order of records from nested sub-queries; e.g., the
ordering imposed by an ORDER BY clause in a nested query is not
guaranteed to be respected by an outer query that does not impose
any ordering on the records.
To solve this problem, the translation rules introduce a function
getOrder, which scans a translatable expression t and returns a list

σ(π(sort(σ(b, fσ ), lsort ), fπ ), fσ2 )
π(σ(sort(σ(b, fσ ), lsort ), fσ2 ), fπ )
π(sort(σ(b, fσ ∧ fσ2 ), lsort ), fπ )
Trans(σ(s, fσ2 ))

Note that in the definition of Trans, a sort with an empty list of
fields is simply the identity function and has no effect on the order
of the list. This is relevant because in the cases where the argument
to Trans is already a baseExp, Trans simply wraps this argument
with dummy selects, sorts and projections to get a translatable
expression.

5

2012/8/10

[[Query(string )]]

=

( string )

[[top(s, e)]]
[[⊲⊳ (t1 , t2 , True)]]

=
=

SELECT ∗ FROM [[s]] LIMIT [[e]]
SELECT ∗ FROM [[t1 ]], [[t2 ]]

[[agg(t)]]
[[π(sort(σ(t, fσ ), e), fπ )]]

=
=

SELECT agg(field) FROM [[t]]
SELECT [[fπ ]] FROM [[t]] WHERE [[fσ ]]

c ∈ command

ORDER BY [[e]], getOrder(t)

op ∈ binary op

[[unique(t)]]

=

SELECT DISTINCT ∗ FROM [[t]]
ORDER BY getOrder(t)

[[fσ (e)]]
[[fσ (e, t)]]

=
=

[[e]].f1 op [[e]] AND ... [[e]].fN op [[e]]
[[e]] IN [[t]]

[[fπ (e)]]

=

[[e]].f1 , ... , [[e]].fN

c ∈ constant
e ∈ expression

=

[]

getOrder(top(e, i ))
getOrder(π(e, f ))

=
=

getOrder(e)
getOrder(e)

getOrder(σ(e, f ))
getOrder(⊲⊳ (e1 , e2 , f ))

=
=

getOrder(e)
getOrder(e1 ) : getOrder(e2 )

getOrder(sort(e, [e.fi ]))

=

[e.fi ] : getOrder(e)

getOrder(unique(e))
getOrder(agg(e))

=
=

getOrder(e)
[]

True | False | number literal | string literal
c | var | e.f | {fi = ei } | e1 op e2 | ¬ e
[ ] | Query(...) | size(e) | get(er , es )
append(e1 , e2 ) | unique(e)
skip | var := e | if(e) then c1 else c2
while(e) do c | c1 ; c2 | assert e
∧| ∨ | > | < | ≥ | ≤ | =

Figure 8. Abstract syntax of the kernel language
and immutable lists. Lists are used to represent the collection of
records and are modeled after the Iterable interface in Java. They
are also used to model the results that are returned from database
retrieval operations. Lists store either scalar values or records constructed with scalars, and nested lists are assumed to be appropriately flattened. The language currently does not model the threevalued logic of null values in SQL, and does not model updates
to the database. We assume that there is a standard type system in
place to ensure that the input program is well-typed. Figure 8 shows
the syntax of the language.
The semantics of the constructs in the kernel language are
mostly standard, with a few new ones introduced for record retrievals. [ ] constructs creates an empty list. Query(...) retrieves
records from the database and the results are returned as a list. The
records of a list can be randomly accessed using get, and records
can be appended to a list using append. Finally, unique takes in a
list and creates a new list with all duplicate records removed.

Figure 6. Syntax-driven rules for SQL translation from translatable expressions
getOrder(Query(...))

::=
::=
|
|
::=
|
::=

4.2 Conversion from Java Programs

Figure 7. Definition of getOrder
of fields that are used to order the subexpressions in t. The list
is then used to impose an ordering on the outer SQL query with
an ORDER BY clause. The function is defined for each of the
operators in the theory in Fig. 7. One detail of the algorithm not
shown in the figure is that some projections in the inner queries
need to be modified so they do not eliminate fields that will be
needed by the outer ORDER BY clause.

Unfortunately, real-world programs are not written in the kernel
language. Most of the primitive Java operations can be converted
easily after standard transformations such as expression flattening
and function inlining. We currently do not handle polymorphic
types and exceptions. In the following, we describe two types of
transformations from Java programs into the kernel language: the
first group of transformations expand the expressiveness of the
language, and another group for preserving Java semantics.

Append and Unique. The append operation is not included in
translatable expressions because there is no simple means to combine two relations in SQL that preserves the ordering of records in
the resulting relation. We can still translate unique, however, using
the SELECT DISTINCT construct at the outermost level, as Fig. 6
shows. Using unique in nested expressions, however, can change
the semantics of the results in ways that are difficult to reason about
(e.g., unique(top(r , e)) is not equivalent to top(unique(r ), e)).
Thus, the only expressions with unique that we translate to SQL
are those that use it at the outermost level. In our experiments, we
found that omitting those two operators did not significantly limit
the expressiveness of the theory.

Java list operations. The Java collections classes contain many
methods on lists that are not modeled by the kernel language. To
handle that issue, we implement a number of such operations using
the kernel language (e.g., contains, clear, iterators, etc). Doing so
allows us to process more real-world programs as our experiments
show.
Java data structures. The kernel language assumes that the user
program uses lists as the data structure to manipulate persistent
data, but Java includes other data structures as well. While the language does not directly support other data structures, we can, however, implement them using lists. For instance, we model hashtable
as a list of (key, value) pairs, with value being a flattened list
of records that are mapped to the same key. Inserting into the
hashtable is simply appending the appropriate list of values, and
retrieval is implemented by iterating through the list until the given
key is found. Modeling hashtables allow our prototype to recognize a broader set of relational operations in imperative code (such
as hash join), and other data structures can be similarly modeled as
well.

4. Language for Persistent Data Manipulation
Having presented the theory of ordered relations, we now describe
how we use it to automatically convert imperative code to SQL
expressions. We begin by describing the modeling of the input
program using a kernel language. The kernel language allows us
to define simple rules to compute verification conditions as will be
shown in subsequent sections.

Boolean variables. The kernel language includes boolean values
but not boolean variables. As such, boolean variables in the input source are converted into integers, and boolean operations are
converted into integer operations. This allows us to process more
classes of code fragments, as our experiments show.

4.1 A Kernel Language
We use a simple imperative language to model Java programs that
retrieve values from a database and compute on them. The language operates on three types of values: scalars, immutable records,

6

2012/8/10

VC(skip, P)
VC(lv := e, P)
VC(if(e) then c1 else c2 , P)
VC(while(e) do c, P)

=
=
=
=

VC(c1 ; c2 , P)
VC(assert e, P)

=
=

Verification conditions for the outer loop

P
P[e/lv ]
(e ∧ VC(c1 , P)) ∨ (¬e ∧ VC(c2 , P))
I ∧ ∀x1 , ... , xN I → (e → VC(c, I )
∧¬e → P
VC(c1 , VC(c2 , P))
P ∧e

initialization

outerLoopInvariant(0, users, roles, [ ])

termination

i ≥ size(users) ∧ outerLoopInvariant(i , users, roles, listUsers) →
postcondition(listUsers, users, roles)

perservation

(same as inner loop initialization)
Verification conditions for the inner loop

Figure 9. Rules for computing verification conditions for the kernel language
Statements with side effects. The input source code might contain
Java statements with side effects while iterating through records
retrieved from the database. Our kernel language does not model
side effects. In order to process such loops, we remove statements
with side effects from the loop and attempt to convert the remainder
of the loop into SQL. If our algorithm is able to convert the loop
with a SQL query, we create a new loop with the statements with
side effects as the body, and have the loop iterate over the results
from the converted SQL query instead.
Preserving Java semantics on lists. The kernel language assumes
that the list operations do not raise errors or exceptions, which is
not the case for Java programs. For instance, Java get throws an
exception when the index is out of bounds. To model such behavior,
we prepend all get(r , e) with assert e < size(r ). The added
assertion is incorporated into the verification condition. As a result,
if the validity of the prepended assertion cannot be established then
Q BS will not be able to convert the input program into SQL.

initialization

i < size(users) ∧ outerLoopInvariant(i , users, roles, listUsers) →
innerLoopInvariant(i , 0, users, roles, listUsers)

termination

j ≥ size(roles) ∧ innerLoopInvariant(i , j, users, roles, listUsers) →
outerLoopInvariant(i + 1, users, roles, listUsers)

preservation

j < size(roles) ∧ innerLoopInvariant(i , j, users, roles, listUsers) →
(get(users, i ).id = get(roles, j).id ∧
innerLoopInvariant(i , j + 1, users, roles,
append(listUsers, get(users, i )))) ∨
(get(users, i ).id 6= get(roles, j).id ∧
innerLoopInvariant(i , j + 1, users, roles, listUsers))

Figure 10. Verification conditions for the running example

the loop is entered, and computation of verification conditions
proceeds as described.
As an example, Fig. 10 shows the verification conditions that
are generated for the running example. In this case, the verification
conditions are split into two parts, with invariants defined for both
loops. The first two assertions describe the behavior of the outer
loop on line 5, with the first one asserting that the outer loop invariant must be true on entry of the loop (after applying the rule
for the assignments prior to loop entry), and the second one asserting that the postcondition for the loop is true when the loop
terminates. The third assertion asserts that the inner loop invariant is true when it is first entered, given that the outer loop condition and loop invariant are true. The preservation assertion is the
inductive argument that the inner loop invariant is preserved after executing one iteration of the loop body. The list listUsers is
either appended with a record from get(users, i), or is remain unchanged, depending on whether the condition for the if statement,
get(users, i).id = get(roles, j).id, is true or not. Finally, the termination assertion states that the outer loop invariant is valid when
the inner loop terminates.

5. Generating Verification Conditions
Given an input program in the kernel language, the next step in the
our algorithm is to come up with an expression for the postcondition variable of the form pcVar = e, where e is a translatable
expression as defined in Sec. 3.4. In order to infer the postcondition, we first compute verification conditions over each line of
code in the input program. These conditions amount to assertions
that must hold true over the input program, and are expressed using
the predicate language as presented in Fig. 3.
To compute verification conditions, we employ standard results
from axiomatic semantics [19] in systematic verification of program behavior. The rules that are used to compute verification
conditions for the commands in the kernel language are shown in
Fig. 9.
The statement VC(c, P) = P ′ means that given postcondition
P, the verification condition for command c is P ′ . Computation of
verification condition is relatively straight-forward. For instance,
to compute the verification condition for the assignment command
lv := e given postcondition P, we simply replace occurrences of
lv in P with e. As in traditional Hoare logic style verification, computing the verification condition of the while statements involves a
loop invariant I and states that: 1. the invariant has to be true prior to
entry into the loop; 2. if the loop condition e is true, and that invariant is true for all the program variables x1 , ... , xN that are modified
in the loop body c, then the verification condition of the loop body
given the invariant as the postcondition is true (i.e., the loop is preserved) and; 3. when the loop terminates, the postcondition that we
would like to establish, P, is true.
Unlike traditional computation of verification conditions, both
the postcondition and the loop invariants are unknown when the
conditions are generated. This does not pose problems for our
algorithm as we simply treat invariants (and the postcondition) as
functions of the program variables that are currently in scope when

6. Synthesis of Invariants and Postconditions
The verification conditions computed from the previous section
lack definitions for loop invariants and postconditions. We synthesize these predicates using the S KETCH constraint-based synthesis system [28]. S KETCH uses a counterexample guided synthesis
algorithm (CEGIS) to efficiently search very large spaces of candidate expressions for one that is correct according to a bounded
model checking procedure. In order to make the search tractable,
S KETCH takes as input a definition of the space of expressions to
search. In this section, we show how the Q BS algorithm analyzes
the input program to infer a space of candidate expressions for the
synthesizer to search. Q BS actually generates these spaces incrementally, so if the synthesizer fails to find a solution in a smaller
space, a bigger space is attempted.

7

2012/8/10




listUsers | σ(users, f ) |



i | size(users) | size(roles) | size(listUsers) |


⊲⊳ (top(users, e1 ), top(listUsers, e2 ), f ) |
sum(π(users, f )) | sum(π(roles, f )) | max(π(users, f )) |
i op
∧ listUsers op


 ⊲⊳ (σ(top(users, e1 ), f1 ), σ(top(listUsers, e2 ), f2 ), f3 ) | 


...
...



Figure 11. Space of possible invariants for the outer loop of the running example.
the algorithm repeats the template generation process, but increases
the complexity of the template that is generated by considering expressions consisting of more relational operators, and more complicated boolean functions. Our evaluation using real-world examples
shows that most code examples require only a few (< 5) iterations
before finding a candidate solution. Additionally, the incremental
solving process can be done in a parallel fashion (although we did
not implement this), further decreasing runtime if needed.

6.1 Inferring the Space of Possible Invariants
Recall that each invariant is parameterized by the current program
variables that are in scope. Our algorithm assumes that each loop
invariant is a conjunction of predicates, with each predicate having
the form lvi = e, where lv is a program variable that is modified
within the loop, and e is an expression from the predicate grammar
in Fig. 3.
The space of expressions e is restricted to expressions of the
same static type as lv involving the variables that are in scope.
The system limits the size of expressions that the synthesizer can
consider, and incrementally increases this limit if the synthesizer
fails to find any candidate solutions (to be explained in Sec. 6.3).
Fig. 11 shows the set of candidate predicates for the outer loop
in the running example. The figure shows the potential expressions
for the program variable i and listUsers. The definitions for the
various functions used in the relational operators are generated in a
similar way.
One advantage of using the theory of ordered relations is that
invariants can be relatively concise. This has a big impact for
synthesis, because the space of expressions grows exponentially
every time the size of expressions to search over increases.

Breaking symmetries. Symmetries have been shown to be one of
sources of inefficiency in constraint solvers [12, 31]. Unfortunately,
the template generation algorithm presented above can generate
highly symmetrical expressions. For instance, it can generate the
following potential candidates for the postcondition:
σ(σ(users, f1 ), f2 )
σ(σ(users, f2 ), f1 )
Notice that the two expressions are semantically equivalent to
the expression σ(users, f1 ∧ f2 ). However, the synthesizer does not
have that knowledge, and would consider the two expressions individually, leading to inefficiency. Fortunately, the equivalence theorem developed in Sec. 3.3 allows us to prune away a large subset of
symmetrical expressions. The template generation algorithm uses
the theorem as much as possible during expression generation to
reduce the number of expressions that are actually created for both
invariants and postconditions.
One further optimization is applied when generating templates
for postconditions. Since our goal is to translate the postcondition
into SQL, we only need to generate translatable expressions as
defined in Sec. 3.4 as potential candidates. Our experiments have
shown that applying these symmetric breaking optimizations can
reduce the amount of solving time by half.
The current template generation algorithm is simple in that for
a given variable lv , it only uses scope and static types as means
to restrict the number of other variables that can be potentially
related to lv for invariant and postcondition purposes. More static
analysis can be performed on the source code to further restrict the
number of potential variables, for instance using dataflow analysis
to detect variable relationships. However, given that our current
prototype can already infer a variety of imperative constructs in
SQL queries within a reasonable amount of time, we decided to
leave such extensions for future work.

6.2 Creating Templates for Postconditions
The process of creating templates for postconditions is similar to
that of creating templates for invariants. The difference is that we
only need to generate a template for the postcondition variable,
since we are not seeking to generate the strongest postconditions.
The mechanism used to generate possible expressions for the postcondition variable is similar to that for invariants, except that:
• the postcondition must be in the form pcVar = e and not any
other binary operators between pcVar and e, as those do not lead
to meaningful SQL translations.
• similarly, we do not generate the identity form, as that is
trivially true and is not a meaningful expression.
With that in mind, the algorithm would generate the following
template for the postcondition of the running example:

users | σ(users, f ) | top(users, e) |


⊲⊳ (top(users, e1 ), top(roles, e2 ), f ) |
listUsers =

 ⊲⊳ (σ(top(users, e1 ), f1 ), σ(top(roles, e2 ), f2 ), f ) | 

...




Again, the functions and expressions used in the relational operations generated as above.

7. Formal Validation and Source Transformation

6.3 Optimizations

After the synthesizer comes up with candidate invariants and postconditions, they need to be validated using a theorem prover,
since the synthesizer used in our prototype is only able to perform
bounded reasoning as discussed earlier. We have implemented the
theory of ordered relations in the Z3 [5] prover for this purpose.
Since the theory of lists is not decidable as it uses universal quantifiers, the theory of ordered relations is not decidable as well.
However, for practical purposes we have not found that to be limiting in our experiments. In fact, given the appropriate invariants and
postconditions, the prover is able to validate them within seconds
by making use of the axioms that are provided.
If the prover can establish the validity of the invariants and postcondition candidates, the postcondition is then converted into SQL
according to the rules discussed in Sec. 3.4. For instance, for the

The basic algorithm presented above for generating invariant and
postcondition templates is sufficient but not efficient for synthesis.
In this section we describe two optimizations that improve the
synthesis efficiency.
Incremental solving. As an optimization, the generation of templates for invariants and postconditions is done in an iterative manner: our algorithm initially creates simple templates using the production rules from the predicate grammar, such as considering expressions with only one relational operator, and functions that contains only one boolean clause. If the synthesizer is able to generate a candidate that is sufficiently strong to confirm the validity of the verification conditions, then our job is done. Otherwise,

8

2012/8/10

Type

Expression inferred

outer loop
invariant

i ≤ size(users) ∧
listUsers = π(sort(σ(⊲⊳ (top(users, i ), roles, True), fσ ), lsort , fπ )

inner loop
invariant

i < size(users) ∧ j ≤ size(roles) ∧
listUsers = append(
π(sort(σ(⊲⊳ (top(users, i ), roles, True), fσ ), lsort ), fπ )
π(sort(σ(⊲⊳ (get(users, i ), top(roles, j), True), fσ ), lsort ), fπ ))

postcondition

Application
Wilos
itracker
Total

# benchmarks
33
16
49

# trans. by prior work
9
5
14

# trans. by Q BS
28
12
40

Figure 14. Experiment on real-world benchmarks
to convert Java code into real-world applications, and second to
explore the limitations of the current implementation.
We implemented a prototype of the Q BS algorithm. The source
code analysis and computation of verification conditions are implemented using the Polyglot compiler framework [25]. We use Sketch
[28] as the synthesizer for invariants and postconditions, and Z3 [5]
for validating the invariants and postconditions.

listUsers = π(sort(σ(⊲⊳ (users, roles, True), fσ ), lsort ), fπ )

where
fσ := get(users, i ).roleId = get(roles, j).roleId
fπ projects all the fields from the User class
lsort = [users, roles]

8.1 Real-World Benchmarks

Figure 12. Inferred expressions for the running example

In the first set of experiments, we evaluated our implementation of
the Q BS algorithm using real-world examples from two large-scale
open-source applications written in Java. Both applications use the
Hibernate ORM library for data persistence operations. Wilos [4]
is a project management application with 62k LOC, and itracker
[1] is a software issue management system with 61k LOC. We randomly selected a number of classes that are stored persistently and
manually identified code fragments that fetch multiple instances of
such classes from the database and manipulate them in loop constructs (such as the running example in Fig. 1), or pass them to
methods from Java’s collection classes (such as Collections.sort).
We removed fragments that we believed would not benefit from
query inference (such as those that iterate through all fetched objects from the base query and mutate each one). This process resulted in a total of 49 code fragments. We pass each fragment to
our Q BS prototype. Figure 14 reports the number of fragments that
Q BS was able to transform into SQL equivalent expressions. For
comparison purposes, we also report the number of benchmarks
that we believe can be transformed by prior work [32, 33], based
on the published description of these algorithms, where relational
projections and selections are inferred by computing access paths in
loop constructs. The numbers were inferred by manual inspecting
each benchmark and checking if it performs a selection or projection in imperative code. The details of the benchmarks are given in
the appendix.

List objs1 = fetchRecordsFromDB();
List results1 = new ArrayList();
for (Object o : objs1) {
if (f(o))
results1.add(o);
}
List results2 = new ArrayList();
for (Object o : objs1) {
if (g(o))
results2.add(o);
}

Figure 13. Code fragment with alias in results
running example our algorithm found the invariants and postcondition as shown in Fig. 12, and the input code is transformed into the
results in Fig. 2.
If the prover is unable to establish validity of the candidates
(detected via a timeout), we ask the synthesizer to generate other
candidate invariants and postconditions after increasing the space
of possible solutions as described in Sec. 6.3. One reason that
the prover may not be able to establish validity is because the
maximum size of the relations set for the synthesizer was not large
enough. For instance, if the code returns the first 100 elements
from the relation but the synthesizer only considers relations up
to size 10, then it will incorrectly generate candidates that claim
that the code was performing a full selection of the entire relation.
In such cases our algorithm will repeat the synthesis process after
increasing the maximum relation size.

8.2 Discussion
First of all, the experiment shows that the Q BS algorithm is able
to infer relational specifications from a large number of real-world
benchmarks and convert them into SQL equivalents. For the benchmarks that are reported as translatable by Q BS, our prototype was
able to synthesize postconditions and invariants, and also validate
them using the prover. Furthermore, our prototype was able to process most of benchmarks under 5 minutes, with the ones that involve join operations consuming the most amount of time (up to 40
mins maximum). In the following, we broadly describe the common types of relational operations that our Q BS prototype inferred
from the benchmarks, along with some limitations of the current
implementation.

7.1 Object Aliases
Implementations of ORM libraries typically create new objects
from the records that are fetched, and our current implementation
will only transform the input source into SQL if all the objects
involved in the code fragment are freshly fetched from the database,
as in the running example. In some cases this may not be true, as in
the code fragment in Fig. 13.
Here, the final contents of results1 and results2 can be aliases to
those in objs1. In that case, rewriting results1 and results2 into two
SQL queries with freshly created objects will not preserve the alias
relationships in the original code. Our current implementation will
not transform the code fragment in that case, and we leave sharing
record results among multiple queries as future work.

Projections and Selections. A number of benchmarks perform
relational projections and selections in imperative code. Typical
projections include selecting specific fields from the list of records
that are fetched from the database, and selections include filtering
a subset of objects using field values from each object (e.g., user
ID equals to some numerical constant), and a few use criteria that
involve program variables that are passed into the method.
One special case is worth mentioning. In some cases only a
single field is projected out and loaded into a set data structure,

8. Experiments
In this section we report our experiment results. The goal of the
experiments is twofold: first, to quantify the ability of our algorithm

9

2012/8/10

such as a set of integer values. One way to translate such cases (for
instance, using the scheme from prior work) is to generate SQL
that fetches the field from all the records (including duplicates)
into a list, and subsequently eliminate the duplicates and return
the set to the user code. Our prototype, however, improves upon
that scheme by detecting the type of the postcondition variable
and inferring a postcondition involving the unique operator, which
is then translated to a SELECT DISTINCT query that avoids
fetching duplicate records from the database.

Limitations. Finally, there are a few examples from the two applications where our prototype fails to translate the code fragment into
SQL, even though we believe that there is an equivalent SQL query.
For instance, some benchmarks include code fragment where the
input list is sorted by calling Collections.sort, followed by retrieving the last record from the sorted list, which is equivalent to max
or min depending on the sort order. Including extra axioms in the
theory would allow us to reason about such cases. Another set of
benchmarks include advanced use of types, such as storing polymorphic records in the database, and performing different operations based on the type of records retrieved. Incorporating type information in the theory of ordered relations is an interesting area
for future work.

Joins. Another set of benchmarks involve join operations. We
summarize the join operations in the application code into two
categories. The first involves obtaining two lists of objects from two
base queries and looping through each pair of objects in a nested
for or while loop. The pairs are filtered and (typically) one of the
objects from each pair is retained. The running example in Fig. 1
represents such a case. For these cases, our prototype translates the
program fragment into a relational join of the two base queries with
the appropriate join predicate, projection list, and sort operations
that preserve the ordering of records in the results.
Another type of join also involves obtaining two lists of objects
from two base queries. Instead of a nested loop join, however, the
code iterates through each object e from the first list, and searches
if e (or one of e’s fields) is contained in the second list. If the result
is true, then e (or some of its fields) is appended to the resulting list
and is returned at the end. For these cases our prototype converts
the search operation into a contains expression in the predicate
language, after which the expression is translated into a correlated
subquery in the form of SELECT * FROM r1, r2 WHERE r1 IN r2,
with r1 and r2 being the base queries.
As mentioned, our prototype is able to handle both join idioms
mentioned above. However, the loop invariants and postconditions
involved in such cases tend to be more complex as compared to
selections and projections, as illustrated by the running example in
Fig. 12. As a result, they require more iterations of the synthesis
and formal validation before a valid solution can be found, with up
to 40 mins in the longest case and the majority of the time spent
in synthesis and bounded verification. Unfortunately, we are not
aware of any prior techniques that can be used to infer join queries
from imperative code, and we believe that more optimizations can
be devised to speed up the synthesis process for such cases.

8.3 Advanced Idioms
In the second part of experiments, we used synthetic code fragments to demonstrate the ability of our prototype to translate more
complex expressions into SQL. Although we did not find such examples in either of our two real-world applications, we believe that
these can occur in real applications.
Hash Joins. Beyond the join operations that we encountered in the
application benchmarks, we wrote two synthetic test cases for joins
that join relations r and s using the predicate r.a = s.b, where a and
b are integer fields. In the first case, the join is done via hashing,
where we first iterate through records in r and build a hashtable,
whose keys are the values of the a field, and where each key maps
to a list of records from r that has that corresponding value of a. We
then loop through each record in s to find the relevant records from
r to join with, using the b field as the look up key. As mentioned
in Sec. 4.2, the Q BS algorithm models hashtables using lists, and
with that our prototype is able recognize this process as a join
operation and convert the fragment accordingly, similar to the join
benchmarks mentioned above.
Sort-Merge Joins. Our second synthetic test case joins two lists
by first sorting r and s on fields a and b respectively, and then iterating through both lists simultaneously. We advance the scan of r
as long as the current record from r is less than (in terms of fields
a and b) the current record from s, and similarly advance the scan
of s as long as the current s record is less than the current r record.
Records that represent the join results are created when the current
record from r equals to that from s on the respective fields. Unfortunately, our current prototype fails to translate the code fragment
into SQL, as the invariants for the loop cannot be expressed using
the current the predicate language, since that involves expressing
the relationship between the current record from r and s with all the
records that have been previously processed.

Aggregations. Aggregations are used in benchmarks in a different
number of ways. The most straightforward ones are those that simply return the length of the list that is returned from an ORM query,
which are translated into COUNT queries. More sophisticated uses
of aggregates include iterating through all records in a list to find
the maximum or minimum values, or searching if a record exists in
a list. Aggregates such as maximum and minimum are interesting
as they introduce loop-carried dependencies [6], where the running
value of the aggregate is updated conditionally based on the value
of the current record as compared to previous ones. By using the
top operator from the theory of ordered relations, our prototype is
able to generate a loop invariant of the form v = agg(top(r, i)) and
subsequently translate the postcondition into the appropriate SQL
query.
As a special case, a number of benchmarks check for the existence of a particular record in a relation by iterating over all records
and setting a result boolean variable to be true if it exists. As mentioned in Sec. 4.2, boolean variables and operations on booleans are
converted into integer equivalents. Generating invariants that are
similar as in the case of the other aggregates, our prototype translates such code fragments into SELECT COUNT(*) > 0 FROM ...
WHERE e, where e is the expression to check for existence in the
relation. We rely on the database query optimizer to further rewrite
this query into the more efficient form using EXISTS.

Iterating over Sorted Relations. We next tested our prototype
with two usages of sorted lists. We created a relation with one
unsigned integer field id as primary key, and sorted the list using
the sort method from Java. We subsequently scanned through the
sorted list as follows:
List records = Query("SELECT id FROM t");
List results = new ArrayList();
Collections.sort(records); // sort by id
for (int i = 0; i < 10; ++i)
results.add(records.get(i));

Our prototype correctly processes this code fragment by translating it into SELECT id FROM t ORDER BY id LIMIT 10. However,
if the loop is instead written as follows:

10

2012/8/10

the synthesis template is inspired by the PINS algorithm [30], although in our work we do not require user intervention. Meanwhile,
there has been substantial earlier work on automatically detecting
loop invariants, such as using predicate refinement [15] or dynamic
approaches like the Daikon system [14] and invGen [18]. There
has also been work on using synthesis to discover invariants [29].
Our work differs from previous approaches in that we only need
to discover invariants and postconditions that are strong enough to
validate the transformation, and our predicate grammar and translatable expressions greatly prune the space of invariants to those
needed for common relational operations, rather than those needed
for general-purpose programs.

List records = Query("SELECT id FROM t");
List results = new ArrayList();
Collections.sort(records); // sort by id
int i = 0;
while (records.get(i).id < 10) {
results.add(records.get(i));
++i;
}

The two loops are equivalent since the id field is a primary key
of the relation, and thus there can at most be 10 records retrieved.
However, our prototype is not able to reason about the second
code fragment, as that requires an understanding of the schema of
the relation, and that iterating over id in this case is equivalent to
iterating over i in the first code fragment. Both of which require
additional axioms to be added to the theory before such cases can
be converted.

Integrated query languages. Integrating programming languages
and database query languages into a single language has been an
active research area, with projects such as LINQ [24], Kleisli [34],
Links [11], JReq [20], the functional language proposed in [10],
Ferry [17], and DBPL [27]. These solutions provide a means to embed database queries in imperative programs without using ORMlike libraries, or requiring users to embed SQL in their code. Unfortunately, many of them do not support all relational operations,
and the syntax of many of such languages are still quite similar to
SQL, meaning that developers still need to learn new programming
concepts.

9. Related Work
The idea of inferring relational specifications from imperative code
constructs was first studied in [32, 33]. The work uses abstract interpretation and attribute grammar to extract SQL queries from Java
programs. The idea is to compute the set of data access paths that
a piece of imperative code traverses, and replace the imperative
code that performs the explicit path traversal with SQL queries. The
analysis can be applied to recursive function calls, but does not handle code fragments with loop-carried dependencies, or fragments
that implement join or aggregation. It is unclear how this method
(modeling relational operations as access paths) can be extended to
handle such cases.
In contrast, our implementation is able to infer both relational
join and aggregation from imperative code. We currently do not
handle recursive function calls, although we have not encountered
the use of recursive functions in the two real-world applications
used in our experiments.

Improving performance of database programs by code transformation. There is also work in terms of improving application
performance by transforming loops and reordering statements to
expose opportunities for query batching [9, 26], and pushing computations into the database to improve application performance [8].
Our work is orthogonal to this line of research. After converting
portions of the source code into SQL queries, such code transformation tools can still be applied to gain additional performance improvement.

10. Conclusions

Modeling relational operations. Our ability to infer relational
specifications from imperative code relies on using the theory of
ordered relations to connect the imperative and relational worlds.
Previous work modeled such operations differently. In addition to
modeling relational operations using data access paths, other work
has modeled relational databases using bags [10], sets [22], and
nested relational calculus [34]. In that respect, one key insight of
our work is that ordered relations are the right abstraction for our
purpose, as they are similar to the interfaces provided by the ORM
libraries in the imperative code, and allow us to design a sound and
precise transformation into SQL. Other model choices, such as the
theory of sets, would be closer to the relational model, but would
make reasoning about operations such as top difficult, as elements
in a set are not ordered.
To our knowledge, our work is the first one to address the issue
of precision, i.e., the ordering of records, in relational transformations. Precision would not be an issue if the source program only
operated on orderless data structures such as sets or did not perform
any relational operations that create new records, such as joins. Unfortunately, most imperative languages (such as Java) provide interfaces based on ordered data structures, making this problematic.
The benchmarks in our experiments also show that implementing
joins in imperative code is a relatively common operation.

In this paper, we presented the Q BS algorithm for inferring relational specifications from imperative code that retrieves data using ORM libraries. Our algorithm works by automatically inferring
loop invariants and postconditions associated with the source program, and converting the validated postcondition into SQL queries.
Our approach is both sound and precise in preserving the ordering
of records. In developing the algorithm, we designed a new theory of ordered relations that allows efficient encoding of relational
operations into a predicate language. We implemented a prototype
of the algorithm, and demonstrated the applicability and limits using a variety of benchmarks from both real-world applications and
manually-constructed examples.

References

[1] itracker
Issue
Management
System.
http://itracker.sourceforge.net/index.html.
[2] Java Persistence API. http://jcp.org/aboutJava/communityprocess/final/js
[3] JBoss Hibernate. http://www.hibernate.org.
[4] Wilos Orchestration Software. http://www.ohloh.net/p/6390.
[5] z3 Theorem Prover. http://research.microsoft.com/en-us/um/redmond/proj
[6] J. R. Allen and K. Kennedy. Automatic loop interchange. In Proc.
SIGPLAN Symp. on compiler construction, pages 233–246, 1984.
[7] A. Blass and Y. Gurevich. Inadequacy of computable loop invariants.
ACM Trans. Comput. Log., 2(1):1–11, 2001.
[8] A. Cheung, O. Arden, S. Madden, and A. C. Myers. Automatic
partitioning of database applications. PVLDB, 5, 2011.
[9] W. Cook and B. Wiedermann. Remote batch invocation for SQL
databases. In Proc. Database Programming Languages (DBPL), 2011.
[10] E. Cooper. The script-writer’s dream: How to write great sql in
your own language, and be sure it will succeed. In Proc. Database

Automatic mining of program invariants. Our verification-based
approach to finding a translatable postcondition is similar to that
used in earlier work [20, 21], although previous work acknowledges that finding invariants is difficult and instead uses a symbolic execution based approach in reasoning about program behavior in loops. The idea of scanning the source program to generate

11

2012/8/10

A. Benchmark Details

Programming Languages (DBPL), pages 36–51, 2009.
[11] E. Cooper, S. Lindley, P. Wadler, and J. Yallop. Links: Web programming without tiers. In Proc. Int.l Symp. on Formal Methods for Components and Objects, pages 266–296, 2006.
[12] D. Déharbe, P. Fontaine, S. Merz, and B. W. Paleo. Exploiting symmetry in smt problems. In Proc. Int.l Conf. on Automated Deduction,
pages 222–236, 2011.
[13] E. W. Dijkstra. Guarded commands, nondeterminacy and formal
derivation of programs. Commun. ACM, 18(8):453–457, 1975.
[14] M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically
discovering likely program invariants to support program evolution. In
Proc. Int.l Conf. on Software Engineering, pages 213–224, 1999.
[15] C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proc. ACM Symp. on Principles of Programming Languages
(POPL), pages 191–202, 2002.
[16] D. Gries. The Science of Programming. Springer, 1987.
[17] T. Grust, M. Mayr, J. Rittinger, and T. Schreiber. FERRY: databasesupported program execution. In Proc. ACM SIGMOD Int’l Conference on Management of Data, pages 1063–1066, 2009.
[18] A. Gupta and A. Rybalchenko. Invgen: An efficient invariant generator. In Proc. Int.l Conf. on Computer Aided Verification (CAV), pages
634–640, 2009.
[19] C. A. R. Hoare. An axiomatic basis for computer programming.
Commun. ACM, 12(10):576–580, 1969.
[20] M.-Y. Iu, E. Cecchet, and W. Zwaenepoel. Jreq: Database queries in
imperative languages. In Proc. Int’l Conference on Compiler Construction (CC), pages 84–103, 2010.
[21] M.-Y. Iu and W. Zwaenepoel. HadoopToSQL: a mapreduce query
optimizer. In EuroSys, pages 251–264, 2010.
[22] D. Jackson. Alloy: a lightweight object modelling notation. ACM
Trans. Softw. Eng. Methodol., 11(2):256–290, 2002.
[23] W. Kim. Introduction to Object-Oriented Databases. The MIT Press,
2008.
[24] E. Meijer, B. Beckman, and G. Bierman. LINQ: Reconciling objects,
relations and XML in the .NET framework. In Proc. ACM SIGMOD
Int’l Conference on Management of Data, pages 706–706, 2006.
[25] N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: An extensible
compiler framework for Java. In Proc. Int’l Conference on Compiler
Construction (CC), pages 138–152, 2003.
[26] K. Ramachandra, R. Guravannavar, and S. Sudarshan. Program analysis and transformation for holistic optimization of database applications. In Proc. ACM SIGPLAN Int.l Workshop on State of the Art in
Java Program analysis (SOAP), pages 39–44, 2012.
[27] J. W. Schmidt and F. Matthes. The DBPL project: Advances in
modular database programming. Inf. Syst., 19(2):121–140, 1994.
[28] A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodík, V. A. Saraswat,
and S. A. Seshia. Sketching stencils. In Proc. SIGPLAN Conf. on
Programming Language Design and Implementation (PLDI), pages
167–178, 2007.
[29] S. Srivastava and S. Gulwani. Program verification using templates
over predicate abstraction. In Proc. SIGPLAN Conf. on Programming
Language Design and Implementation (PLDI), pages 223–234, 2009.
[30] S. Srivastava, S. Gulwani, S. Chaudhuri, and J. S. Foster. Path-based
inductive synthesis for program inversion. In Proc. SIGPLAN Conf.
on Programming Language Design and Implementation (PLDI), pages
492–503, 2011.
[31] E. Torlak and D. Jackson. Kodkod: a relational model finder. In Proc.
Int.l Conf. on Tools and Algorithms for the Construction and Analysis
of Systems (TACAS), pages 632–647, 2007.
[32] B. Wiedermann and W. R. Cook. Extracting queries by static analysis
of transparent persistence. In Proc. ACM Symp. on Principles of
Programming Languages (POPL), pages 199–210, 2007.
[33] B. Wiedermann, A. Ibrahim, and W. R. Cook. Interprocedural query
extraction for transparent persistence. In Proc. ACM Conf. on ObjectOriented Programming Systems, Languages, and Applications (OOPSLA), pages 19–36, 2008.
[34] L. Wong. Kleisli, a functional query system. J. Funct. Program.,
10(1):19–56, 2000.

In this section we describe the benchmarks from real-world examples that
used in Sec. 8.1. We group the benchmarks according to the type of relational operation each benchmark performs below.
itracker benchmarks
Java Class Name
EditProjectFormActionUtil
IssueServiceImpl
IssueServiceImpl
IssueServiceImpl
IssueServiceImpl
IssueServiceImpl
IssueServiceImpl
IssueServiceImpl
ListProjectsAction
MoveIssueFormAction
NotificationServiceImpl
NotificationServiceImpl
NotificationServiceImpl
NotificationServiceImpl
UserServiceImpl
UserServiceImpl

Line
219
1436
1456
1567
1583
1592
1601
1422
70
144
561
842
941
244
155
412

Operation
F
D
L*
C*
M
M
M
D
N*
K*
O
A
H
O
M
A

wilos benchmarks
Java Class Name
ActivityService
ActivityService
AffectedtoDao
ConcreteActivityDao
ConcreteActivityService
ConcreteRoleAffectationService
ConcreteRoleDescriptorService
ConcreteWorkBreakdownElementService
ConcreteWorkProductDescriptorService
GuidanceService
GuidanceService
IterationService
LoginService
LoginService
ParticipantBean
ParticipantBean
ParticipantService
ParticipantService
ParticipantService
PhaseService
ProcessBean
ProcessManagerBean
ProjectService
ProjectService
ProjectService
ProjectService
ProjectService
ProjectService
RoleDao
RoleService
WilosUserBean
WorkProductsExpTableBean
WorkProductExpTableBean

Line
401
328
13
139
136
55
181
55
245
140
154
102
103
83
1079
681
146
119
266
98
248
243
266
297
338
394
410
248
15
15
717
990
974

Operation
A
A
B
C*
D
E
F
G*
F
A
A
A
H
H
B
H
E
E
F
A
H
B
K*
A
G*
A
A
H
I*
E
B
B
J

where:
A: selection of records
B: return literal based on result size
C: retrieve the max / min record by first sorting and then returning the last element*
D: projection / selection of records and return results as a set
E: nested-loop join followed by projection
F: join using contains
G: type-based record selection*
H: check for record existence in list
I: record selection and only return the one of the records if multiple ones fulfill the
selection criteria*
J: record selection followed by count
K: sort records using a custom comparator*
L: projection of records and return results as an array*
M: return result set size
N: record selection and in-place removal of records*
O: retrieve the max / min record
* indicates those that are not currently handled by the Q BS algorithm

12

2012/8/10

