Cyclic Program Synthesis
Shachar Itzhaky

Hila Peleg

Nadia Polikarpova

Technion
Israelshachari@cs.technion.ac.il

University of California, San DiegoUSA
hpeleg@eng.ucsd.edu

University of California, San DiegoUSA
nadia.polikarpova@ucsd.edu

Reuben N. S. RoweIlya Sergey

Royal Holloway, University of London
United Kingdom
reuben.rowe@rhul.ac.uk

Yale-NUS College
National University of Singapore
Singapore
ilya.sergey@yale-nus.edu.sg

Abstract

1 Introduction

We describe the first approach to automatically synthesizing heap-manipulating programs with auxiliary recursive
procedures. Such procedures occur routinely in data structure transformations (e.g., flattening a tree into a list) or
traversals of composite structures (e.g., n-ary trees). Our approach, dubbed cyclic program synthesis, enhances deductive
program synthesis with a novel application of cyclic proofs.
Specifically, we observe that the machinery used to form
cycles in cyclic proofs can be reused to systematically andefficiently abduce recursive auxiliary procedures.
We develop the theory of cyclic program synthesis byextending Synthetic Separation Logic (SSL), a logical framework for deductive synthesis of heap-manipulating programsfrom Separation Logic specifications. We implement our approach as a tool called Cypress, and showcase it by automatically synthesizing a number of programs manipulating
linked data structures using recursive auxiliary procedures
and mutual recursion, many of which were beyond the reachof existing program synthesis tools.

Consider the task of flattening a binary tree into a linked
list, which is typically solved by writing a recursive data
traversal program. The promise of program synthesis is toautomate such tedious data manipulation tasks by generating programs automatically from high-level, declarative
specifications. Several recent synthesizers [1, 19, 27ś29] areindeed capable of generating recursive programs given only
the top-level description of their behavior. For example, SuSLik [29] can generate a provably correct, recursive C-like
program that deallocates a binary tree given as input thefollowing specification in Separation Logic (SL) [26, 34]:
(1){tree(x, s)} treefree(x) emp

CCS Concepts: · Software and its engineering → Automatic programming.

where sll describes a singly-linked list, and the location r
initially stores the root of the input tree, and eventually theoutput list as computed by flatten. Much to the programmer’s frustration, however, SuSLik fails to synthesize an
implementation: it times out, without producing any useful
output. In fact, given only the specification (2) or a similar
one, and no additional hints, this example is out of reach for
all other state-of-the-art synthesizers for recursive programs.

This specification says that initially the heap contains abinary tree rooted at address x with set of elements s, and thatafter executing treefree the heap must be empty. Inspiredby the success with treefree, the programmer might try tosynthesize tree flattening from the specification below:
(2){r 7→ x ∗ tree(x, s)} flatten(r) r 7→ y ∗ sll(y, s)

Keywords: Program Synthesis, Separation Logic, Cyclic Proofs
ACM Reference Format:
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe,and Ilya Sergey. 2021. Cyclic Program Synthesis. In Proceedings ofthe 42nd ACM SIGPLAN International Conference on Programming
Language Design and Implementation (PLDI ’21), June 20ś25, 2021,
Virtual, Canada. ACM, New York, NY, USA, 16 pages. https://doi.
org/10.1145/3453483.3454087

Challenge: recursive auxiliaries. This failure can be
more readily understood when considering the expected
solution. One such solution, depicted below, begins with tworecursive calls which flatten the immediate subtrees of the
input tree, obtaining two linked lists. Now, the synthesizer
is at an impasse: how to combine the two lists to create theoutput list? This step requires an operationthat appends lists,
which is in itself a recursive program (and one which cannot
be implemented by another call to flatten, for example).
This synthesis task illustrates a fundamental limitation ofexisting approaches to synthesis of recursion: tree flattening

Permission to make digital or hard copies of part or all of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. Copyrights for thirdparty components of this work must be honored. For all other uses, contact
the owner/author(s).
PLDI ’21, June 20ś25, 2021, Virtual, Canada© 2021 Copyright held by the owner/author(s).
ACM ISBN 978-1-4503-8391-2/21/06.
https://doi.org/10.1145/3453483.3454087

945

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey

cannot be accomplished without rxa recursive auxiliary function.1 Existing synthesizers can generate
xr
flatten given the specification ofxl
append as a hint from the user [29]: flatten
flattenusing this auxiliary specificationylyr
as a stepping stone, they can then???
generate code for both flattenyand append as two synthesis tasks.
It is, however, often non-trivial forthe programmer to come up with this kind of hints.
Inferring auxiliary specifications automatically has been along-standing open challenge in program synthesis. Since thehypothesis space is very large, simply allowing the synthesizer to conjecture any arbitrary auxiliary definition would
be impractical, as that would make the search space explode.
The state of the art is the work by Eguchi et al. [13], whichattacks this problem in the context of functional programming by assuming a set of predefined recursion templates (e.g.
a fold-right over lists). While syntactic templates help curb
the search space explosion, they also limits the applicabilityof the technique, and in particular, preclude traversals ofarbitrary user-defined data structures.

Our contributions. Realizing the idea of cyclic synthesis
requires a carefully designed deductive system, in which
the repeated goals observed in program derivations can beused to form backlinks. Our first contribution is the designof such a deductive system, which we dub Cyclic SSL (SSL⟲ ).
This system builds on top of Synthetic Separation Logic(SSL), the deductive synthesis framework underlying SuSLik [29]. SSL⟲ features a new set of rules for synthesizing procedure calls, incorporating an expressive trace-based
termination checking mechanism from cyclic proofs [7, 8].
This mechanism enables SSL⟲ to derive a wider range ofrecursive programs, including programs with auxiliaries andnon-structural recursion.
Our second contribution is an implementation of SSL⟲
in a new synthesis tool Cypress, which extends and subsumes SuSLik. The addition of cyclic reasoning requires anefficient mechanism for detecting potential companions forthe current goal during search. Cypress achieves this via acall abduction oracle, which matches up goals that are notsyntactically equal, adjusting them accordingly. Cypress also
features more efficient theory reasoning via a mechanism
we dub unification modulo theories, as well as new best-first
proof search, guided by the size and shape of the goal.
We evaluated Cypress on 46 synthesis benchmarks. Ourevaluation shows that Cypress is able to solve a numberof challenging tasks requiring nested traversals of linked
structures (e.g., sorting or de-duplicating a linked list) or
traversals of mutually-recursive data structures (e.g., n-ary
trees). To the best of our knowledge, these programs arebeyond reach of any existing approaches to automated hintfree synthesis from declarative specifications.

Cyclic program synthesis. We present a new synthesis
technique, dubbed cyclic program synthesis, capable of automatically discovering recursive auxiliaries without the needfor built-in templates or additional hints from the user. In particular, given the specification (2), our technique synthesizes
a provably correct tree-flattening program, automaticallydiscovering a recursive auxiliary that appends two lists.
Our technique draws inspiration fromÐand owes its nametoÐcyclic proofs, a powerful reasoning mechanism from theline of work on automated theorem proving [3, 9, 11, 25, 36,
37, 39]. In cyclic proofs, derivation łtreesž can have backlinks from non-axiomatic leaves (called buds) to identicalinternal nodes (called companions). These backlinks enable
an automation-friendly approach to proofs by induction: instead of conjecturing an induction hypothesis a-priori, themethod exploits a similarity between a current goal anda companion goal elsewhere in the derivation, essentiallyturning the latter into an induction hypothesis on demand.
The key insight of this work is to apply the cyclic proof
approach to automated deductive synthesis of recursive programs: instead of conjecturing auxiliary specifications a priori, one can abduce them from the repeated goal patterns
encountered during the main program derivation. For example, in flatten the synthesizer starts generating the code ofappend inline, and later recognizes that the program can becompleted by extracting the code into a function and addinga recursive call.

Paper outline. The following sections provide a brief
primer on synthesis via SSL, outlining this work’s innovations via a series of examples (Sec. 2); give a description of
SSL⟲ and its meta-theory (Sec. 3); describe the synthesis
algorithm (Sec. 4); and report on our evaluation (Sec. 5).

2 Cyclic Program Synthesis, by Example
This section presents the main ideas of Synthetic Separation
Logic (SSL), followed by an overview of the scenarios enabled
by our new rules and cyclic proofs principles. All code examples shown in this section are synthesized automaticallyusing our novel synthesis tool Cypress.
2.1 Background: SSL and Its Limitations
Specfications. Deductive synthesis based on SSL takes
as input a pair of Hoare-style pre- and postconditions. For
instance, recall the specification (1) for deallocating a tree:{tree(x, s)} treefree(x) emp

Here the precondition tree(x, s) states that treefree may
assume that it starts from a heap containing a binary tree
rooted at address x with payload set s; the postcondition

1 The choice of auxiliary is not unique, e.g. one may propose an auxiliarythat uses a list accumulator.

946

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, CanadaEmp

emp states that treefree must guarantee that the heap isempty upon its termination.2 Note that the tree root x also
appears as a parameter to treefree, and hence is a program
variable, i.e., can be mentioned in the synthesized program;the payload set s, on the other hand, is a logical variable andmust not appear in the program. In the rest of this section,
we distinguish program variables from logical variables byusing monotype font for the former.
In general, in a specification {P} f(...) {Q}, assertions
P, Q have the form ϕ; P, where the spatial part P describes
the shape of the heap, while the pure part ϕ is a plain firstorder formula that states the relations between variables(in (1) the trivial pure part true is omitted from both preand postcondition). For the spatial part, SSL employs thestandard symbolic heap fragment of Separation Logic [26, 34].
Informally, a symbolic heap is a set of atomic formulas called
heaplets joined with separating conjunction (∗). The simplest
kind of heaplet is a points-to assertion x 7→ e, which describes
a single memory location with address x and payload e. For
example, the formula x 7→ 5 ∗ y 7→ 10 describes a heap withtwo memory locations, x and y, which store values 5 and 10,
and are distinct, as per the semantics of the ∗ connective.
To capture linked data structures, such as lists and trees,
SSL specifications make extensive use of inductive heap predicates, which are standard in Separation Logic. For instance,
the tree predicate from (1) is inductively defined as follows:
tree(x, s) ≜ x = 0 ⇒ s = ∅; emp| x , 0 ⇒ {s = {v} ∪ sl ∪ sr ;[x, 3] ∗ x 7→ v ∗ ⟨x, 1⟩ 7→ l ∗ ⟨x, 2⟩ 7→ r ∗tree(l, sl ) ∗ tree(r , sr )}

⊢ϕ ⇒ψ


ϕ; emp { ψ ; emp skip

Free

Frame




ϕ; P { ψ ; Q c
ϕ; P ∗ R { ψ ; Q ∗ R

R = [x, n] ∗∗0≤i ≤n (⟨x, i⟩ 7→ ei )

Read





c

ϕ; P { { Q } c

ϕ; P ∗ R { { Q } free(x); c
y is fresh [y/a] ϕ; ⟨x, ι⟩ 7→ a ∗ P { [y/a]{ Q } cϕ; ⟨x, ι⟩ 7→ a ∗ P { { Q } let y = ∗(x + ι); c

Write



Vars(e ) ⊆ PVϕ; ⟨x, ι⟩ 7→ e ∗ P { ψ ; ⟨x, ι⟩ 7→ e ∗ Q c
ϕ; ⟨x, ι⟩ 7→ e ′ ∗ P { ψ ; ⟨x, ι⟩ 7→ e ∗ Q ∗(x + ι) = e; cFigure 1. Selected SSL rules (simplified).

of the SSL judgment {P} { {Q} | c for some program c. Intuitively, this judgment has the same meaning as the Hoare
triple {P} c {Q} (different syntax is used to emphasise that
operationally the program c is łthe outputž rather than łtheinputž). The derivation is constructed by applying inference
rules, a subset of which is presented in Fig. 1.
Inference rules gradually simplify the initial synthesis
goal {P} { {Q}, until symbolic heaps in both pre- and postconditions are empty, at which point the terminal rule Emp
concludes the derivation and łemitsž a trivial program skip.
The Frame rule reduces the synthesis goal to a smaller one
by removing matching symbolic heaps in its pre- and postcondition. The Free rule eliminates a dynamically-allocatedblock of memory from the precondition by emitting a freestatement. The rules Read and Write synthesize reads andwrites of heap locations, correspondingly. The role of theWrite rule is to łequalisež points-to heaplets that have thesame address but different payloads, so that they can be subsequently łtrimmedž by Frame. The role of the Read rule is
to turn a logical variable a into a program variable y, whichmight enable subsequent application of Free or Write. Notethat reading from the heap always creates a fresh program
variable (hence the let syntax), and variables, unlike heap
locations, are never re-assigned.
To deal with inductive predicates, SSL features rules Openand Close (elided from this overview), which unfold predicate definitions in the pre- and the postcondition, respectively. Finally, the Call rule synthesizes a recursive call ifsome part of the current goal’s precondition matches theprecondition P of the top-level, user-provided specification.

(3)

This definition consists of two guarded clauses: the first one
describes the empty tree (and applies when the root pointer x
is null), and the second one describes a non-empty tree. In thesecond clause, a tree node is represented by a three-element
record starting at address x. The first field of the record storesthe payload v, while the other two store the addresses l andr of the left and right subtrees, correspondingly. Records
are represented using a generalized form of the points-to
assertion with an offset: for example, the heaplet ⟨x, 1⟩ 7→ l
describes a memory location at the address x + 1. The block
assertion [x, 3] is an artifact of C-style memory management:
it represents a memory block of size three at address x thathas been dynamically allocated by malloc (and hence canbe de-allocated by free). The two disjoint heaps tree(l, sl )and tree(r, sr ) store the two subtrees. Finally, the pure partof the second clause indicates that the payload of the whole
tree consist of v and the subtree payloads, sl and sr .

Deriving treefree. Let us illus- 1 void treefree(x) {if (x = 0) {trate how all those rules work in 23} else {tandem to synthesize the imple- 4
let l = *(x + 1);
let r = *(x + 2);
mentation of treefree shown on 56
free(x);the right from the specification (1). 7
treefree(l);We start by unfolding the defini- 89 }} treefree(r);tion of tree in the top-level goal{tree(x, s)} { emp , which generates two sub-goals (onefor each clause of the predicate):

Deductive synthesis. Given a pre-/postcondition pair P,
Q, deductive synthesis proceeds by constructing a derivation
2 This specification also implicitly guarantees that treefree always termi-

nates and executes without memory errors (e.g., null-pointer dereferencing).

947

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey

Call
(
)



x = 0 ∧ s = ∅; emp { emp | c 1()
ϕ f ; P { ψ f ; S f (x i ) ⊢ ϕ ⇒ [σ ]ϕ f()
ϕ ∧ [σ ]ψ f ; [σ ]S ∗ R { { Q } cϕ; [σ ]P ∗ R { { Q } f (σ (x i )); c(4){x , 0; [x, 3] ∗ x 7→ v ∗ ⟨x, 1⟩ 7→ l ∗ ⟨x, 2⟩ 7→ r

(5)ϕ; P { ψ ; Q cϕ; P { ψ ; Q f (x i )Figure 2. Rules for calls and definitions in SSL⟲ (simplified).

∗ tree(l, sl ) ∗ tree(r , sr )} { emp | c 2

2.2

The programs c 1 and c 2 emitted by these subgoals will beconjoined via the statement if (x = 0) { c 1 } else { c 2 }. The
first subgoal (4) is trivially solved by the rule Emp, resulting in a program skip. In the second subgoal (5), the twograyed fragments enable two subsequent applications of therule Read, adding two reads statements, from *(x + 1) and*(x + 2), correspondingly, creating two new program-levelbindings, l and r and transforming the current goal into

Recursive Programs from Cyclic Proofs

The primary difference between SSL and SSL⟲ , is that the latter synthesizes a program by searching for a cyclic derivation,with recursive calls arising from backlinks in the proof.
New rules for function definitions and calls. To caterfor synthesizing recursive calls using cyclic proofs, SSL⟲
introduces a new, more general version of the Call rule,shown in Fig. 2. As before, this rule synthesizes a function callf (σ (x i )) (where σ substitutes actuals for formals) wheneversome part of the current symbolic heap can be unified withf ’s spatial precondition P. The main difference is that the
new rule no longer requires f ’s pre-/postcondition to be the
top-level specification provided by the user. InsteadÐperhaps
surprisinglyÐthis rule simply requires that this pre-/post can
synthesize the call f (x i ). At a first glance, this rule is not very
useful: in order to synthesize a function call, we (seemingly)
need to synthesize a function call! The intention of this rule
is to use its first premise as a bud, i.e., link it back to an
identical companion goal earlier in the derivation.
But where do we find a companion goal whose emitted
program is f (x i )? This is where the second new rule ofSSL⟲ , Proc, comes into play (Fig. 2). The Proc rule should beunderstood as a way to łlabelž a node in a program derivation
with a function definition f (x i ). According to this rule, one
can synthesize a definition for the function f (x i ), if one cansynthesize the body c for this function out of the goal withsame pre- and postconditions. Note that unlike all the rules
we’ve seen so far, Proc does not propagate the code emitted
by its premise (the function body) to the conclusion; instead
it abstracts this code away into an identity call f (x i ), i.e., acall whose actual parameters coincide with the formals. The
most common occurrence of the rule Proc is at the root of
the derivation, with the top-level goal being its conclusion.
However, we will see in Sec. 2.3 how this rule also makes it
possible to synthesize auxiliary recursive functions.

{x , 0; [x, 3] ∗ x 7→ v ∗ ⟨x, 1⟩ 7→ l ∗ ⟨x, 2⟩ 7→ r∗ tree(l, sl ) ∗ tree(r, sr )} { emp

Proc


(6)

The Free rule now applies to the grayed fragment of thegoal’s precondition, emitting free(x), and simplifying thesynthesis goal to:(7){. . . ; tree(l, sl ) ∗ tree(r, sr )} { empTo complete the synthesis, we notice that each of the twoheaplets in the precondition matches the top-level specification (1), and hence can trigger the rule Call, synthesizing aprocedure call with a suitable argument.
Limitations. The Call rule of SSL imposes significant
limitations on the kinds of recursive functions it can derive.
The first limitation is that it only allows using the top-level
synthesis goal provided by the user as the specification forthe callee; this precludes synthesis of recursive auxiliary
functions, as required, for example, to flatten a tree into a
list, as explained in the introduction.
A second, somewhat subtler limitation arises from theway SSL enforces termination of synthesized programs. To
avoid generating trivial non-terminating solutionsÐsuch as
treefree(x) immediately calling treefree(x) againÐSSL restricts synthesized programs to be structurally recursive.3
More precisely, synthesis starts by picking a single inductive
predicate in the precondition that the program will łrecurseonž, and only allows a recursive call once this predicate has
been unfolded at least once. This limitation makes it impossible to synthesize programs with more complex recursion
patterns: even something as simple as a (helper-free) function that deallocates two trees, as such a function would needto traverse both of those trees recursively in a single run.
In the remainder of this section we will demonstrate how
SSL⟲ overcomes both of these limitations by harnessing thecyclic proof methodology to enhance the Call rule.

Cyclic derivation of treefree. We now demonstrate theapplication of these new rules to build a cyclic derivaiton oftreefree, shown in Fig. 3. For the sake of brevity, we omit the
payload set variables and pure constraints related to them(e.g., s = {v} ∪ sl ∪ sr ) from the goals, as they don’t play anyrole in our example. The instances of the tree predicate areannotated with cardinality variables α, α l , and α r , whichplay a role in the termination argument, as we will explain
shortly. The proof’s root goal serves as a conclusion for an
application of Proc, with the łconjecturedž function f being
treefree. Most of the subsequent applications follow thesequence of rewritings via standard SSL rules outlined in

3 Proof assistants like Coq [10] impose similar restrictions on recursion.

948

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, Canada
(2)
(1)
(



(

)


tree α (x) { emp treefree(x)(Call)) 
tree α r (r) { emp treefree(r)tree α (x) { emp treefree(x)(Call)() . . . ; tree α l (l) ∗ tree α r (r) { emp treefree(l); . . .
(Free)() . . . ; [x, 3] ∗ tree α l (l) ∗ tree α r (r) ∗ . . . { emp free(x); . . .
(Read)() . . . ; [x, 3] ∗ tree α l (l) ∗ tree α r (r ) ∗ . . . { emp let r = . . .
)((Read)

x , 0 ∧ α l < α ∧ α r < α ; [x, 3] ∗ x 7→ v ∗ 




 
 ⟨x, 1⟩ 7→ l ∗ tree α l (l ) ∗ ⟨x, 2⟩ 7→ r ∗ tree α r (r )  { emp let l = . . .
(Open)) (
tree α (x) { emp if (x = 0) {. . . } else {. . . }(Proc)() 
tree α (x) { emp treefree(x)(Emp)
x = 0; emp { emp skip

Figure 3. A derivation of treefree(x) with backlinks. Some pure assertions are omitted.
Sec. 2.1, with some evident parts of the goals elided. An
important twist happens at the two inner derivation nodes
corresponding to the premise of applying of the rule Call.
The goal in both nodes matches precisely the conclusion of
the top-level application of Proc. These pairs of matchingnodes create backlinks in the program derivation, connecting
the premises of two Call applications to the top-level goal.

arbitrarily alternating cycles (1) and (2). In each cycle, wewill start by tracing α , and then switch to either α l or α r ,depending on which cycle is being traversed. In either case,when we make the switch, the traced cardinality strictly
decreases (following the cardinality constraints in the predicate definition), while elsewhere along the cycle is stays
unchanged. Hence we have shown that along each infinite
path the cardinality must strictly decrease infinitely often.
As prior work has shown [35], given cardinally constraints,
the appropriate sequence of cardinalities to trace can be inferred automatically using automata-theoretic toolsÐan observation that is crucial for automating synthesis via SSL⟲ .
This mechanism subsumes termination measures based on
maximum and/or lexicographic ordering of multiple arguments, and enable SSL⟲ to synthesize non-structurally recursive programs, for example, one that deallocates two trees
as part of the same traversal (see technical report [16]).

Proving termination. Cyclic reasoning is not valid in
general: cyclic proofs must satisfy a well-formedness condition in order to preclude infinite derivations. Intuitively,
one can view the derivation as a directed graph with edges
pointing from conclusions to premises and from buds to companions. The well-formedness condition requires that along
every infinite path in this graph, some well-founded measuredecreases infinitely often [8]. In SSL⟲ , infinite paths in thederivation correspond to potential infinite traces of the program’s execution. The well-formedness condition ensuresthat no such infinite executions exist since this would entail
an infinitely decreasing chain in a well-founded set.
To trace well-founded measures, SSL⟲ annotates inductive predicates with cardinality variables, which can be seen
as sizes of the heap models of the corresponding predicate.
We automatically instrument all predicate definitions withcardinality information; for example, the instrumentation of
the tree predicate (3) is highlighted via gray boxes below:

2.3

Synthesizing Auxiliary Recursive Functions

We now move on to the core of our contribution and illustrate
how cyclic synthesis handles the motivating example fromthe introduction: the procedure that flattens a tree into alinked list, whose specification (2) we repeat for convenience:{r 7→ x ∗ tree(x, s)} { r 7→ y ∗ sll(y, s)
We omit the definition of the singly-linked list predicate sll,
since it is standard for Separation Logic [34] and analogous
to the tree predicate (3). The specification enforces that the
payload set of the output list be the same as that of the
input tree by using the same logical variable s in the pre- andpostcondition. For the sake of brevity, we omit the set-related
reasoning in the derivations shown below.

tree α (x, s ) ≜ x = 0 ⇒ s = ∅; emp
α l < α ∧ α r < α ∧ s = {v } ∪ sl ∪ s r ; 






 [x, 3] ∗ x 7→ v ∗⟨x, 1⟩ 7→ l ∗ ⟨x, 2⟩ 7→ r 
x ,0⇒







 ∗tree α l (l, s ) ∗ tree α r (r, s )rlNote the highlighted cardinality constraints we add to thesecond (recursive) clause, which state that cardinalities αland α r of the the left and right subtrees are strictly smaller
than α, that of the enclosing tree. Given this instrumentation,
the cardinality constraints end up in the goal’s precondition
upon unfolding the predicate (via Open), as shown in Fig. 3.
To show that the derivation in Fig. 3 is well-formed, wemust pick a sequence of cardinality variables to trace alongeach infinite path and prove that this sequence is strictly
decreasing. All infinite paths in this derivation consist of

Synthesized code. The program synthesized from thisspecification is shown in Fig. 5. We have given more descriptive names (in lieu of automatically-generated ones) to local
variables and the auxiliary function. The main procedure
flatten calls itself recursively twice to produce the lists corresponding to the left and right subtrees of the node x. The
head of the first list, returned from the call in line 9 via r, isthen stored in yl, while the head of the second list is stored inr (through an extra level of indirection) after the call in line

949

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey(Read), (Write)

(3)

.
.
.
β
β
.
l
(yl) ∗ . . . { r 7→ y ∗ sll (y ) append(yl, v, x, r)
r 7→ yr ∗ sll (yr ) ∗ sll(Call)
(
) (
)
′
β
β
β ′ < βl ; r 7→ yr ∗ sll βr (yr) ∗ sll l (n) ∗ ⟨yl, 1⟩ 7→ n ∗ . . . { r 7→ y ∗ sll (y ) append(n, v, x, r); . . .




βr

(

)

(b)

l

·
· (Read), (Open)
·

 (
)
β
βr
l
{
r
→
7
y
∗ sll β (y ) let yr = ∗r; if (yl = 0) {. . . } else {. . . }r 7→ yr ∗ sll (yr) ∗ sll(yl) ∗ . . .
 ((Proc))
βr 7→ yr ∗ sll βr (yr ) ∗ sll βl (yl) ∗ . . . { r 7→ y ∗ sll (y ) append(yl, v, x, r)
(2)
.
.
) (
(
)
.
.
r 7→ x ∗ tree α (x ) { r 7→ y ∗ sll β (y ) flatten(r)(Call)
) (
(
)
β
α
β
r 7→ xr ∗ tree r (xr) ∗ sll l (yl) ∗ . . . { r 7→ y ∗ sll (y ) flatten(r); append(yl, v, x, r)·· (Read), (Write)
· ) (
(
)
α
βl
r 7→ yl ∗ sll (yl ) ∗ tree r (xr) ∗ . . . { r 7→ y ∗ sll β (y ) let yl = . . .
(1)
.
.
(
)
) (
.
β
α
.
r 7→ x ∗ tree (x ) { r 7→ y ∗ sll (y ) flatten(r)(Call)()) (βαα l < α ∧ α r < α ; r 7→ xl ∗ tree l (xl) ∗ tree α r (xr) ∗ . . . { r 7→ y ∗ sll (y ) flatten(r); let yl = . . .
·· (Open), (Read), (Write)
·
(
)
) (
α
r 7→ x ∗ tree (x) { r 7→ y ∗ sll β (y ) if (x = 0) { } else {. . . }(Read)()) (r 7→ x ∗ tree α (x ) { r 7→ y ∗ sll β (y ) let x = ∗r; if (x = 0) { } else {. . . }(Proc)()) (r 7→ x ∗ tree α (x ) { r 7→ y ∗ sll β (y ) flatten(r)

(a)
(c)

Figure 4. A derivation of flatten and its recursive auxiliary append.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

void flatten(r) {let x = *r;
if (x = 0) {} else {let v = *x;
let xl = *(x + 1);
let xr = *(x + 2);*r = xl;
flatten(r);let yl = *r;*r = xr;
flatten(r);append(yl, v, x, r);
}
}

16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

of this derivation is uneventful and quite similar to what wehave already seen for treefree in Fig. 3: the two applicationsof Call induce two backlinks (1) and (2) to the top-levelgoal and correspond to the recursive calls to flatten(r) inlines 9 and 12 of Fig. 5.
After these two calls, however, we find ourselves in thenode (a) of the derivation5 , with the following synthesis goal:

void append(yl, v, x, r){
let yr = *r;
if (yl = 0) {let y = malloc(2);free(x);*y = v;*(y + 1) = yr;*r = y;} else {let n = *(yl + 1);
append(n, v, x, r);
let y = *r;*(yl + 1) = y;*r = yl;} }(s = {v} ∪ sl ∪ sr ; r 7→ yr ∗ sll(yl, sl ) ∗ sll(yr , sr ) ∗[x, 3] ∗ x 7→ v ∗ ⟨x, 1⟩ 7→ _ ∗ ⟨x, 2⟩ 7→ _{ r 7→ y ∗ sll(y, s))(8)Here, we are given two lists, yl and yr , and we need to obtain a single list y that contains all of their elements plus
v. How should the synthesizer proceed to solve this goal?
It proceeds just like it would for any goal that contains inductive predicates in the precondition: by unfolding one of
their instancesÐin this case sll(yl, sl )Ðvia Open. The recursive premise of Open is depicted in the derivation node (b),whose precondition again features two lists: one of them, yr,
is the same as before, and the other one, n, is the tail of yl.

Figure 5. Tree flattening program synthesized by Cypress.
12. As its last statement, flatten calls the recursive auxiliary
function append, passing it the pointers to the two lists, yl
and r, as well as the parent tree node x and its payload v.
The auxiliary procedure append concatenates the two lists,
yl and r, inserting a new element with payload v in the
middle (hence, computing an in-order unfolding of the tree).
To this end, it traverses the first list, yl, recursively. Once itreaches the base case where yl is empty (lines 19ś23), it frees
the tree node x4 , allocates a new list node y with payloadv, and prepends it to the second list, storing the result in r.
Its inductive case (lines 25ś29) calls append recursively on
the tail of yl, after which it adjusts the tail pointer (yl + 1)
appropriately and stores the result again in r.

Abducing the auxiliary. At this point the synthesizer
realizes that the Call rule is applicable again; this time, however, the companion goal is not the top-level specification (2),but rather the goal (8) from node (a). Indeed, a sub-heap of
the current precondition (the one containing everything but
the head of yl) can be unified with the precondition of (8)by substituting n for yl. In order to become an eligible companion, however, a node must emit a procedure call, which
is clearly not the case for (a). To bridge this mismatch, thesynthesizer retroactively inserts an application of Proc justbelow (a) and creates a new node (c) as its conclusion. The

Cyclic derivation of flatten. To understand how theauxiliary append has been discovered, let us take a look at the
SSL⟲ derivation of flatten, shown in Fig. 4. The first half
4 Instead of passing x to append, it would have been more natural to deal-

locate it immediately in flatten. Although SSL⟲ is capable of deriving
either program, our implementation makes the less natural choice, which
we discuss further in Sec. 5.4.

5 For now, imagine that node (c) and the adjacent application of Proc are

not there. We will come back to them shortly.

950

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Variablex, y Alpha-numeric identifiers ∈ PV
Size, offset n, ι Non-negative integers
Expression e ::= 0 | true | x | e = e | e ∧ e | ¬e | d
T -expr. d ::= n | x | d + d | n · d | { } | {d } | · · ·Command c ::= let x = ∗(x + ι) | ∗(x + ι) = e |let x = malloc(n) | free(x ) | error| f (e i ) | c; c | if (e ) {c } else {c }ProgramΠ ::= f (x i ) { c } ; c

Logical variable
T -term
Pure logic termν, ωCardinality variable ακ::= ν | e | · · ·ϕ,ψ , χ ::= κ | ϕ = ϕ | ϕ ∧ ϕ | ¬ϕSymbolic heap

P,Q, R ::= emp | ⟨e, ι⟩ 7→ e | [e, ι] | pα (ϕ i ) | P ∗ Q()
D::= pα (x i ) : e j ⇒ ∃y . χ j ; R jP, Q ::= ϕ; P

Heap predicate
Assertion
EnvironmentΓ:= ∀ x i . ∃ y j .

Context Σ ::= D

Figure 6. SSL⟲ programming language and assertion syntax.
new node has the same synthesis goal as (a) and an identity call to a fresh procedureÐhere append(yl,v,x,r)Ðas theemitted code.
This lazy application of Proc corresponds to abducing
the recursive auxiliary on demand. The parameters of the
new procedure are all the program variables of (a); its preand postcondition are defined by (8), the synthesis goal of(a); finally, its body is the code emitted by (a) (derived by the
SSL⟲ sub-derivation rooted at (a)).

Cypress is able to generate a pair of mutually recursive functions that deallocate a rose tree.

3 Cyclic Program Synthesis, FormallyIn this section, we give a formal presentation of declarative
rules of SSL⟲ and describe the underlying metatheory.
3.1 Programs and Assertions
Programming language. The target language of SSL⟲
is an imperative, C-like fragment with dynamic memory
allocation, deallocation, store and load (Fig. 6, left). Values
include at least booleans and integers, and a special typeloc designates pointer variables. Pointers are isomorphic tounsigned integers, but there is only a single pointer constant,
0 (null). Expressions include at least variables, literal constants, equality check and logical connectives. Additional
theory-specific expressions are allowed depending on the underlying theory used for checking entailment in derivations;
our implementation supports linear integer arithmetic andsets. The language allows pointer arithmetic in the formx + ι, but other arithmetic operations are disabled for pointers. The statement f (ei ) denotes a procedure call with actual
parameters ei . Procedures do not have a return value: thebehavior of return is emulated by passing in an address of theheap location where the result should be stored. There areno variable re-assignments and no while loops. A program isa sequence of procedure definitions, followed by a statement.

Termination. As before, we perform a global well-formedness check on the entire derivation. Note, however, that inthis case infinite paths can either follow some combinationof backlinks (1) and (2) or always follow the backlink (3); inother words, in the absence of mutual recursion, the termination arguments for the two procedures are entirely disjoint.
Termination follows from the highlighted cardinality constraints: αl < α , α r < α , and βl′ < βl .
2.4 More Examples
We conclude this section by outlining two examples thatshowcase unique capabilities of SSL⟲ and Cypress and go
beyond the state of the art in synthesis with auxiliaries [13].
More details and synthesized code for these examples canbe found in our technical report [16].
Flattening a tree in-place. Our first example leverages
the imperative nature of our underlying language, allowing
Cypress to flatten a binary tree into a doubly-linked list inplace: {tree(x, s)} flatten_to_dll(x) {dll(x, z, s)}. Note that
here we require that the root of the input tree and the headof the output list be located at the same address x. We omit
the standard definition of the dll predicate, but note thatin-place flattening is possible because both a tree node anda doubly-linked list node are represented as a three-element
record, so one can be reinterpreted as the other.

Assertion language. The assertion language comprises
pure assertions in the underlying theory, and SL assertions
with inductively defined predicates (Fig. 6, right). Its semantics have been explored throughout Sec. 2. The set of purelogic terms (ϕ,ψ , χ ) is a superset of program expressions e.
The logic is sorted, and pure parts (ϕ in {ϕ; P }) are ensured to
be Boolean expressions via simple type checking. Predicate
instances are annotated with cardinality variables α and β.
Assertions are interpreted in an environment Γ in whichsome of the variables are universally quantified and others
existentially quantified, with a prefix of the form ∀x .∃y. Program variables are always included in the universal prefix.
Logical variables are split between universal (also called ghost
variables) and existential. We denote Vars(Γ) = {x, y} for all
quantified variables, and PV(Γ) = {x }∩PV, GV(Γ) = {x }\PV,EV(Γ) = {y} for program variables, ghost variables and existentials of Γ, respectively. We also use e[Γ] for the set of all

Mutual recursion. Our final example shows the ability of Cypress to synthesize manipulations with mutuallyrecursive data structures. An n-ary tree, a.k.a. rose tree [23],can be implemented by storing the children of a tree node ina linked list. Its definition in Separation Logic uses a pair ofmutually recursive predicates: rtree, representing a tree, andchildren, representing a linked list of trees. Given these pred
icates and a specification {rtree(x, s)} rtree_free(x) emp ,951

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey

R0 Terminal rules
Emp

Inconsistency

⊢ϕ ⇒ψ


Γ; ϕ; emp { ψ ; emp skip⊢ϕ ⇒⊥Γ; ϕ; P { Q error

R1 Pointer operations

3.2 Proof Rules
Fig. 7 lists all synthesis-related SSL⟲ rules in a declarative
manner. The rules operate on transforming entailment judgments Γ; P { Q | c, which informally means that any statethat satisfies the assertion P can be transformed into somestate that satisfies Q by a statement c [29]. Within rules, forclarity, we follow the convention of using lower latin lettersx, y for program variables, e, t for program-level terms (ofthe syntactic class e in Fig. 6), greek letters ν, ω for logical variables, and ϕ, ψ , χ for logical formulas. We will now
describe the rules and their effects on the synthesis.
R0 Terminal rules. The rules Emp and Inconsistency
form the leaves of a derivation by emitting a skip for a trivial
goal or error for a vacuous goal (unsatisfiable precondition).
Here ⊢ ϕ ⇒ ψ denotes entailment between pure formulasin the underlying theory; our implementation uses an SMT
solver to discharge these premises.
R1 Rules for atomic operations. Each of the pointer operations of the target language has a corresponding rulethat describes when to emit it: Read and Write for memory access, Alloc and Free for dynamic memory management. These rules are more restricted versions of the corresponding symbolic execution rules of standard Separation
Logic [5]; the additional restrictions are required to guide
rule applications in the context of synthesis, where the program is not available. For example, the Write rule uses theheaplet ⟨x, ι⟩ 7→ e in the goal’s postcondition to determine
what should be written into the address x.
R2 Rules for inductive predicates. The two rules Openand Close unfold definitions of inductive predicates in the
pre- and the postcondition, respectively. These rules have
dual effects on the program in the sense that Open eliminatesa predicate instance and hence performs a case split on its
clauses, while Close introduces an instance and hence picks
a single clause non-deterministically. As a result, Close does
not emit any code, while Open emits a conditional statementwith one branch per clause, using clause selectors as guards.
R3 Rules for procedures. These rules are the main innovation of SSL⟲ as compared with SSL. The rules Proc andCall were discussed in detail in Sec. 2.2. The rule Proc delineates procedure boundaries by emitting a call to a procedure
whose body is emitted by its single premise.
Procedure calls are generated via the rule Call. It bundles together Separation Logic-style framing, with R as theframe, and substitution of actual into formal parameters via

σ , which is also applied to the postcondition ψ ′; S . Existential variables in the procedure’s environment are remappedto fresh ghost variables in the second premise of the rule.
Formal parameters x i are mapped to program expressionse[Γ] using program variables of Γ, and ghosts ν j are mapped
to logical terms using any variables of Γ.
CallSetup handles the situations when some code has tobe emitted before the call can be made. To see why this rule

Read 

x ∈ PV y ∈ PV \ Vars(Γ)∀y.Γ; ϕ ∧ y = e; ⟨x, ι⟩ 7→ e ∗ P { Q c
Γ; ϕ; ⟨x, ι⟩ 7→ e ∗ P { Q let y = ∗(x + ι); c
Write



Γ; ϕ; ⟨x, ι⟩ 7→ e ∗ P { ψ ; ⟨x, ι⟩ 7→ e ∗ Q c
Vars(e) ⊆ PV′Γ; ϕ; ⟨x, ι⟩ 7→ e ∗ P { ψ ; ⟨x, ι⟩ 7→ e ∗ Q ∗(x + ι) = e; c

Alloc

(


)
Γ; ϕ; [y, n] ∗ y, i 7→ ti 0≤i <n ∗ P {)(x ∈ EV(Γ)ψ ; [x, n] ∗ ⟨x, i⟩ 7→ ei 0≤i <n ∗ Q c

)
(


Γ; ϕ; P { ψ ; [x, n] ∗ ⟨x, i⟩ 7→ ei 0≤i <n ∗ Q let y = malloc(n); cFreeΓ; ϕ; P { Q cx ∈ PV)(Γ; ϕ; [x, n] ∗ ⟨x, i⟩ 7→ ei 0≤i <n ∗ P { Q free(x ); c
R2 Predicate unfolding
Open

(
)
Γ ∪· ∀ω jk ; [ti /νi ] ϕ ∧ e j ∧ χ j ; R j ∗ P { Q c j for all j=1..r()∈Σ
ω jk < Vars(Γ), GV(ti ) = ∅pα (νi ) : e j ⇒ ∃ω jk . χ j ; R j
j=1..r)(Γ; ϕ; pα (ti ) ∗ P { Q

if ([ti /νi ]e 1 ) {c 1 }else if ([ti /νi ]e 2 ) {c 2 } else · · ·

Close

(
)
Γ ∪· ∃ω jk ; P { [ti /νi ] ϕ ∧ e j ∧ χ j ; R j ∗ Q c j for some j=1..r()
pα (νi ) : e j ⇒ ∃ω jk . χ j ; R j∈Σω jk < Vars(Γ)
j=1..r()α
Γ; P { ϕ; p (ti ) ∗ Q c

R3 Procedures
ProcΓ; P { Q | c{x i } = PV(Γ)Γ; P { Q | f (x i )
Call



∀x i , ν j .∃ωk ; ϕ ′; P { ψ ′; S f (x i )
′dom (σ ) = {x i , ν j , ωk }
Γ ∪· ∀σ (ωi ); [σ ]ψ ∧ ϕ; [σ ]S ∗ R { Q c⊢ ϕ ⇒ [σ ]ϕ ′σ (x i ) ∈ e[Γ]; σ (ν j ) ∈ κ[Γ]
Γ; ϕ; [σ ]P ∗ R { Q f (σ (x i )); c
CallSetupΓ ∪· BV(c 1 ); ψ ; S ∗ R { Q f (ei ); c 2
Γ; ϕ; P { ψ ; S c 1
Γ; ϕ; P ∗ R { Q c 1 ; f (ei ); c 2

Figure 7. Synthesis rules of SSL⟲ .

expressions that can be constructed using PV(Γ), and κ[Γ]Ð
all logical terms that can be constructed with Vars(Γ). Whenjoining environments, the quantifier pattern is preserved,
and we use the notation ∀x .∃y ∪· ∀x ′ .∃y ′ = ∀x, x ′ .∃y, y ′.
All variable sets x, x ′, y, y ′ must be disjoint.
A clause e ⇒ ∃y. χ ; R in a definition of a heap predicate
pα (x i ) consists of a selector expression e and an assertionχ ; R . As explained in Sec. 2.2, the pure part χ contains a
cardinality constraint of the form α k < α for each predicate
instance qα k (. . .) inside R. These are not part of the surface
syntax, but are added automatically during pre-processing.

952

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, Canada

is required, consider the recursive call flatten(r) in line 9 ofFig. 5. To enable this call we first need to write the root of theleft subtree xl into the return location r; but to trigger thiswrite, we need to have r 7→ xl in the goal’s postcondition!
CallSetup enables that: it performs sequential decomposition
of the synthesis goal with the call’s precondition ψ ; S as
the intermediate state. As a result, r 7→ xl ends up in the
postcondition of its first subgoal, triggering the synthesisof the write in line 8. Although the declarative presentationin Fig. 7 makes it look like the assertion ψ ; S is chosen
non-deterministically, in Sec. 4 we explain how Cypress
implements this rule efficiently via a call abduction oracle.

Definition 3.2 (Traces). A trace is an infinite sequence α i(i ≥ 0) of cardinality variables. We say that a trace follows apath Gi (i ≥ 0) in a pre-proof P when (α i , α i+1 ) is a trace pairfor (Gi , Gi+1 ) for each i ≥ 0. When (α i , α i+1 ) is progressing,
we say that the trace progresses at i. A trace is called infinitely
progressing if it progresses at infinitely many points.
Definition 3.3 (Proofs). A pre-proof P is said to satisfy the
global trace condition when every infinite path in P is followed by an infinitely progressing trace.
The global trace condition is an ω-regular property, so it
is decidable when a pre-proof is a proof, cf. [9, Prop. 7.4]. We
write ⊢ G when there is a proof deriving G.

Logical rules. The remainder of SSL⟲ rules are logicalrules, which do not emit new code, but instead transform thegoal in a way that would ultimately allow the applicationof other (operational) rules. Our logical rules are mostly
standard for SL-based theorem provers [5], so we relegate
them to the technical report [16] to save space. They include
the Frame rule we have seen in Sec. 2, as well as rules for purereasoning, e.g. eliminating existentials. In Sec. 4 we discuss
how Cypress implements such pure reasoning efficiently.

3.4

Soundness

SSL⟲ inherits the memory model and operational semantics
from traditional SL [5]. In the interest of space we only state
the soundness theorem here. Its proof and the rest of themetatheory are relegated to the technical report [16].
Theorem 3.4 (Soundness). If ⊢ Γ; P { Q | c, then for any
heap/stack pair ⟨h, s⟩ that satisfies P, there exists a heap/stackpair ⟨h ′, s ′⟩ that satisfies Q, such that executing c from state⟨h, s⟩ terminates in state ⟨h ′, s ′⟩.

3.3 Cyclic Program Derivations
An SSL⟲ derivation is a tree consisting of goals Γ; P { Q | c,and constructed using the inference rules in Fig. 7. In contrast to the standard notion of a proof as a finite derivation
tree, SSL⟲ derivations are permitted to be regular, non-wellfounded (i.e., infinitely tall) trees. Regularity ensures thatan SSL⟲ derivation tree always has a finite representation
as a (possibly) cyclic graph. Concretely, we represent SSL⟲
derivations as finite trees, along with a set of backlinks connecting each non-terminal leaf node to a syntactically identical ancestor node. In other words, we allow goals fromthe middle of the proof to be used again as premises higher
up the derivation tree. Formally, each backlink denotes theinfinite unfolding of the path connecting the leafÐcalledbudÐwith its associated internal nodeÐcalled companion.
We call SSL⟲ derivations pre-proofs, since they do notnecessarily derive terminating programs. To ensure termination, we require that pre-proofs satisfy an additional global
property, defined in terms of traces of cardinality variables.

4 Cyclic Program Synthesis, Pragmatically
We implemented cyclic program synthesis in a new synthesizer called Cypress [17]. Cypress takes as input a synthesis
goal {P} f (x i ) {Q} together with the definitions of all inductive predicates it mentions, and performs backtracking proof
search for an SSL⟲ derivation of the judgment P { Q | f (x i ).
Once a proof has been constructed, extracting the synthesized program is straightforward: we simply consider eachapplication of the Proc rule in isolation; each such application gives rise to a procedure, whose signature and body are
the code emitted by the conclusion and the premise of Proc,
respectively. For example, the two applications of Proc in
Fig. 4 give rise to two procedures, flatten and append.
In the rest of this section we outline the mechanisms thatmake our proof search tractable. Since Cypress builds upon
SuSLikÐthe original implementation of SSLÐwe only focus on the new mechanisms, which make Cypress moregeneral and/or more efficient than its predecessor. Cypress
also leverages existing proof search features of SuSLik, suchas early failure rules, phased proof search, and branch abduction (which enables it to synthesize conditionals beyond
those in predicate selectors); we refer the reader to [29] fora detailed account of these features.

Definition 3.1 (Trace pairs). Let G and G ′ be, respectively,
the conclusion and a premise of an inference rule r , and let
α and β be cardinality variables occurring universally in G
and G ′, respectively. We say that (α, β ) is a trace pair for(G, G ′ ) when: either r is Call with substitution σ , G ′ is theleft-hand premise, and α = σ (β ); or ⊢ ϕ ⇒ β ≤ α holds,
where ϕ is the pure precondition of G. If ⊢ ϕ ⇒ β < α also
holds, we say that the trace pair is progressing.

Best-first search. One difference in the overall search algorithm is that Cypress uses memoizing best-first search (inspired by [19]), instead of SuSLik’s naïve depth-first search.
The search is guided by a cost function that assigns a cost toeach heaplet in the goal’s pre- and postcondition, with predicate instances growing more expensive as they get unfolded

A path in a pre-proof P is a sequence Gi (i ≥ 0) of nodes in
P such that each node Gi is the parent of Gi+1 in the infinite
derivation corresponding to P.

953

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey

Unify


Γ; ϕ; P ∗ [σ1 ]R { ψ ∧ ψ ′ ; Q ∗ [σ1 ]R c^
(σ1 (ν ) = σ2 (ν ))dom (σ1 ) = dom (σ2 ) = V
ψ =

Emp


emp { s ∪ {a } = {a } ∪ s; emp
Solve-∃

emp { s ∪ {a } = {a } ∪ w ; emp
Frame{sll(x, s ∪ {a }) } { {s ∪ {a } = {a }∪w ; sll(x, s ∪ {a }) }
Unify

′

ν ∈V



Γ; ϕ; P ∗ [σ1 ]R { ψ ; Q ∗ [σ2 ]RcSolve-∃{sll(x, s ∪ {a }) } { {sll(x, {a } ∪ w ) }Γ; ϕ; P { [σ ] ψ ; Q c⊢ ϕ ⇒ [σ ]ψ
dom (σ ) = {ω }; EV(Γ) = ∅Γ ∪· ∃ω; ϕ; P { ψ ; Q c

Figure 9. An example derivation with rules from Fig. 8.
Termination checking. Whenever the call abduction oracle succeeds, Cypress adds appropriate applications of Calland CallSetup, inserts an application of Proc below thecompanion candidate (using all its program variables as formals and a fresh procedure name), and forms a backlink fromthe first premise of Call to the conclusion of Proc. Everytime a backlink is formed, Cypress checks whether the preproof constructed so far satisfies the trace condition fromSec. 3.3. To this end, it builds a graph of the current pre-proof
with edges labeled with all available trace pairs, according toDef. 3.1. It then invokes Cyclist [35], an off-the-shelf cyclic
theorem prover, which uses an automata-theoretic algorithm
to check whether every infinite path in the graph contains
an infinitely progressing trace.

Figure 8. Two algorithmic rules for pure reasoning.
or go through a call. This cost function prevents the searchfrom getting stuck in a branch that performs infinitely many
unfoldings or calls, and encourages it to focus on smaller(and therefore, hopefully, easier to solve) goals.
4.1 Synthesizing Calls
To understand how Cypress applies the rules Call and
CallSetup in practice, let us revisit the tree flattening program from Fig. 5. After the initial sequence of Read and Openapplications, which generate lines 1ś7, we find ourselveswith a pre-heap r 7→ x ∗ tree(xl) ∗ tree(xr) ∗ . . . (where ellipsis stands for the node at x and its payload, and we omit cardinality and set parameters for brevity). To decide whether acall can be synthesized from this goal, Cypress considers all
candidate companion goals, i.e. all ancestor goals separated
from the current goal by at least one application of Open.
Open is the only rule where cardinality traces can progress,
hence any well-formed cycle in the derivation must include
an application of Open. In our case, the top-level goal withthe pre-heap r 7→ x ∗ tree(x) is such a candidate.

4.2 Pure Reasoning
Until now we have focused on synthesis rules, which directly
emit code; the success of synthesis, however, also cruciallyrelies on logical rules, which transform the goal into a form
where synthesis rules can fire. Logical reasoning in SSL⟲ is
far from straightforward because it needs to support arbitrary SMT-decidable theories in its pure formulas.
To illustrate the challenges of pure reasoning, consider
the following (simplified but representative) synthesis goal:∀x, s, a.∃w.{sll(x, s ∪ {a})} { {sll(x, {a} ∪ w )}(9)Call abduction oracle. Given a candidate companion,
synthesizing a call involves guessing (1) the substitution σof formals into actuals (e.g., [x 7→ xl]); (2) the frame R,
i.e., the part of the precondition untouched by the call (e.g.,tree(xr) ∗ . . .); and (3) the setup statement c required to satisfy the companion’s precondition (here *r = xl). Cypress
finds all these three components at once, using a mechanism
we dub call abduction oracle. This oracle is a separate synthesis problem that attempts to łbridge the gapž between thecurrent goal’s precondition and that of the companion. In
our example, the oracle attempts to derive:{r 7→ x ∗ tree(xl) ∗ tree(xr) ∗ . . .} { r ′ 7→ x ′ ∗ tree(x ′ ) c
Note that all variables in the companion goal are replacedwith fresh existentials. The call abduction oracle only uses
the subset of SSL⟲ rules triggered by the post-condition (e.g.
Write and Alloc), since the rest of rules (e.g. Read, Open,Call) could already fire before the oracle was invoked. It alsouses a modified version of the Emp rule, which allows the preheap to remain non-empty. Upon successful completion, theremaining pre-heap becomes the frame R, the code emitted
during this derivation becomes the setup statement c, and theσ comprises all existential substitutions from this derivation.

The simplestÐand hence most desirableÐsolution to this goalis skip, which informally can be obtained by simply framingaway the sll heaplets; but formally, before Frame can apply, we need to transform the post-heap to be syntactically
identical to the pre-heap, which requires: (a) exploiting commutativity of set union, and (b) instantiating the existential
w with s. Fig. 8 shows two novel logical rules implemented
in Cypress, which perform such transformations efficiently;
Fig. 9 demonstrates how these rules work together to solve
the synthesis goal (9) (we omit the emitted program skip
and highlight new parts in each sub-goal for readability).
Unification modulo theories. The traditional approach
to exploiting equational theoriesÐsuch as commutativityof union in our exampleÐis to eagerly normalize the goal
after every proof step, by computing all implied equalities
between its subterms [4]. For example, if a specification
mentions both s ∪ {a} and {a} ∪ s, normalization would
replace one with the other. The normalization approach has
two downsides: first, it is rather inefficient if you assume
only blackbox access to the SMT solver; second, it does nothelp with the goal like (9), because here s ∪ {a} = {a} ∪954

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, Canada

w is not a logical necessity, but rather a possibility, whichhappens to lead to the shortest solution. To circumvent theselimitations, Cypress implements a new, lazy approach toequational reasoning via the rule Unify in Fig. 8, which we
dub unification modulo theories. Unify looks for a pair ofheaplets [σ1 ]R and [σ2 ]R in the pre- and postcondition that
only differ in pure subterms, and speculatively unifies them,adding equalities between mismatched subterms, σ1 (ν ) =σ2 (ν ), as proofs obligation to the pure postcondition. In Fig. 9,
Unify is used to unify the pre- and post-heap of the goal
(9), producing the proof obligation s ∪{a} = {a}∪w. Even in
the absence of existentials, this approach is more efficientthan eager normalization, because the SMT solver only needs
to check equalities between terms that appear in matchingpositions inside a heaplet.

benchmarks from SuSLik, and the 11 recursive benchmarks from ImpSynt (these two sets overlap); the excluded
five ImpSynt benchmarks are iterative versions of theirrecursive benchmarks, and similarly require sketches.
3. We supplement this set with 14 new benchmarks, half ofwhich, to the best of our knowledge, cannot be solved byany existing synthesis tools. These benchmarks involvethe interplay between auxiliary functions and heap manipulation (e.g., an in-place tree flattening) or operate on
cyclic or mutually recursive structures (e.g., rose trees).
Out of the 46 benchmarks, 19 exercise complex recursion,i.e., they either require a non-trivial termination measure
or a recursive auxiliary procedure (not given as a libraryfunction). We refer to this benchmark set as complex and use
it as a primary focus of our empirical evaluation. All complex
benchmarks are by construction out of reach for SuSLik. The
remaining 27 benchmarks only exercise simple (structural)
recursion. We refer to this benchmark set as simple; although
not the focus of our evaluation, we use these benchmarks todemonstrate the versatility of Cypress.

Pure synthesis. The other major challenge is to find appropriate instantiations for existential variables. To this end,
Cypress includes the rule Solve-∃ in Fig. 8, which picks asubstitution σ from existentials to universals that validates
the pure specification. To find such a substitution, Cypress
needs to solve the constraint ∃σ .∀x .ϕ ⇒ [σ ]ψ , which is itself
a synthesis problem in the pure subset of our logic. Althoughsuch pure synthesis is generally a challenging task, it has
been the subject of much prior work [2, 21, 32]. Cypress outsources pure synthesis queries to the CVC4 synthesizer [33].

Experiment setup. For our main experiment, we ran Cypress on the complex benchmark set, and measured synthesistime and size of the generated code. For our second experiment, we ran Cypress on the simple benchmark suite andcompared the synthesis times with SuSLik. The purpose ofthis experiment is to confirm that searching a larger program
space does not lead to significant degradation in performance.
All experiments were conducted on a commodity laptop (2.7
GHz Intel Core i7 Lenovo Thinkpad with 16GB RAM), andCypress was run as a single-threaded process. Timeout for
all experiments was set to one hour.

5 Evaluation
We evaluated Cypress empirically along three axes: (1) generality: its ability to synthesize programs with complex recursion; (2) efficiency: the time it takes to synthesize programs;and (3) utility: the size of the input specification comparedto the size of the generated programs, and the quality ofgenerated programs.
5.1

5.2

Results

Experiment results on the complex benchmarks are shownin Tab. 1, and on the simple benchmarks in Tab. 2. All specifications and generated code can be found in the technicalreport [16].

Benchmarks and Setup

For our empirical evaluation we have assembled a suite of 46
synthesis benchmarks for pointer-manipulating programs.
Each benchmark is defined by a top-level synthesis goal
expressed as separation-logic specification (and optionally,
specifications of library functions the code is allowed to
invoke). We collected these benchmarks from three sources:
1. State of the art in synthesis with recursive auxiliaries [13].
We include eight out of their nine benchmarks. The remaining one, merge_sort, has a specification identicalto another one (sort), but a different program template,which forces their tool to synthesize merge sort instead of
insertion sort; Cypress does not use program templates,
so the difference between these two benchmarks does notmake sense in our setting. The tool [13] synthesizes functional programs from refinement types, so we manuallytranslated these benchmarks into Separation Logic.
2. State of the art in synthesis of heap-manipulating programs: SuSLik [29] and ImpSynt [31]. We include all 22

5.2.1 Generality. The results in Tab. 1 confirm that Cypress is able to synthesize a variety of functions with complex recursion. Benchmarks 10ś13 were discussed in Sec. 2.
Out of all benchmarks in Tab. 1, only 10 and 17 can be solved
without auxiliaries, but they require a complex termination
metric; interestingly, for 17Ðsorted list mergeÐCypress generates an auxiliary anyway (see discussion in Sec. 5.3) All
the other benchmarks require one or even two auxiliaries;
for example, benchmark 14 flattens a rose tree into a list,
and needs one auxiliary for flattening the list of children andanother one for appending two lists (a flattened tree and aflattened list of children).
Finally, four of the synthesized programs feature mutual
recursion. Two of them operate on rose trees, where mutual
recursion is expected, while the other twoÐflattening a tree955

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey

Table 1. Benchmarks with complex recursion; all of these areout of reach for SuSLik. We report the number of Procedures
generated, total number Stmt of statement in those procedures, the ratio Code/Spec of code to specification (in AST
nodes), and the synthesis Time (in seconds).
Group

SinglyLinkedList

List of
Lists
Binary
Tree
Rose
Tree
Sorted
list
BST

Id
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

1 From [13]DescriptionProc
deallocate two2
append three2
non-destructive append
2
union
2
intersection1
3
difference1
2
deduplicate1
2
deallocate
2
flatten1
2
deallocate two
1
flatten2
flatten to dll in place2†
deallocate
2†
flatten3†
1
reverse2
sort1
2
merge22from list1
2
to sorted list1
2†
2 From [31]

Stmt
9
14
21
24
33
22
23
11
19
16
24
15
9
25
11
12
23
27
35

Code/Spec
6.2x
2.3x
3.0x
5.9x
7.3x
5.5x
7.8x
10.7x
4.8x
11.8x
7.4x
9.6x
12.0x
8.0x
3.3x
3.6x
2.2x
5.0x
6.4x

Table 2. Comparison with SuSLik on benchmarks with simple recursion. We report the number of statements Stmt andsynthesis Time in seconds for both Cypress and SuSLik.
Each benchmark generates a single procedure.

Time
0.3
1.2
5.2
9.6
95.6
8.1
6.2
0.3
0.8
0.3
1.5
2.7
0.3
12.6
1.1
1.9
33.6
11.5
10.2

† Mutually-recursive

into doubly-linked list (12) and flattening a binary searchtree (BST) into a sorted list (19)Ðcame as a surprise.
Comparison with other tools. Cypress was able to synthesize all eight selected benchmarks from [13]. Unlike theirtool, Cypress does not use function templates as hints, andalso targets pointer-manipulating programs instead of functional programs, which is arguably a harder problem. To
the best of our knowledge, Cypress generates code withsimilar recursive structure to their tool: for example, list
reversal, deduplication, and sorting all have the structureof two nested right-folds (and hence quadratic complexity);
one exception is list intersection, discussed below, where
Cypress generates an overly complex solution.
Cypress can also handle all 22 original SuSLik benchmarks (which are all part of the simple set). Finally, Cypress
was also able to solve all 11 recursive benchmarks from ImpSynt [31] (one of which is in the complex set and the rest
are in the simple set). Unlike ImpSynt, we do not require
the user to provide program sketches, and additionally, our
synthesis times on a commodity laptop are at least an orderof magnitude faster than the run times reported in [31] on aserver with 10 cores and 96GB of RAM.
On the other hand, SuSLik cannot handle any of the benchmarks in the complex setÐbecause of complex recursionÐand
also fails on five benchmarks in the simple set. All five failures are due to restrictions on predicate unfolding, which
SuSLik had to impose due to its ad-hoc termination checking
mechanism, which in Cypress has been replaced with themore powerful cardinality-based mechanism from Sec. 3.3.

Group

Id
20
Integers 21
22
23
24
Singly 25
Linked 26
27
List
28
29
30
31
Sorted 32
list
33
34
35
36
Tree
37
38
39
40
BST
41
42
43
Doubly 44
Linked 45
List
46

Description
swap two3
min of two3,4
length2,3
max2,3
min2,3
singleton3,4
dispose3
initialize3
copy3,5append3,5delete3,5prepend2,3
insert2,3
insertion sort2,3
size3
dispose3
copy3
flatten w/append3
flatten w/acc3
insert2,3
rotate left2,3
rotate right2,3delete root2
copy
append5
delete5
single to double

2 From [31]3 From SuSLik [29]

Stmt
4
3
6
7
7
4
4
4
11
6
12
4
25
7
9
6
16
19
12
19
5
5
29
22
10
19
21

Code/Spec
1.0x
1.1x
1.2x
1.9x
1.9x
0.9x
5.5x
1.6x
2.7x
1.1x
2.6x
0.5x
2.6x
1.0x
2.5x
8.0x
3.8x
5.4x
2.1x
1.9x
0.2x
0.2x
1.7x
4.3x
1.6x
3.7x
5.5x

4 From [22]Time
Cypress SuSLik
0.2
< 0.1
1.5
0.4
1.1
1.1
0.7
0.7
0.6
0.7
0.3
< 0.1
0.2
< 0.1
0.6
0.1
0.8
0.3
0.5
0.4
1.6
0.4
0.3
0.2
4.4
5.2
1.2
1.4
0.7
0.3
0.2
< 0.1
2.8
0.7
0.4
0.7
0.7
0.7
9.8
36.9
6.2
23.9
4.8
9.1
1304.3
7.3
2.3
4.7
1.3
-

5 From [30]Although in principle ImpSynt is capable of solving complex
benchmarks that require recursive auxiliaries using nested
loops instead, none of the results reported in [31] containnested loops, and in any case, ImpSynt relies on program
sketches. To our knowledge, no existing synthesizer (for either functional or heap-manipulating programs) is able togenerate mutually-recursive programs.
5.2.2 Efficiency. Our experiments show that Cypress isefficient in synthesizing a variety of programs: all 19 complex
benchmarks were synthesized within two minutes, and all
but two of them take less than fifteen seconds. Our comparison of Cypress with SuSLik on the simple benchmarks
demonstrates that despite searching a larger space of programs, Cypress remains efficient. It is slightly slower on easy
benchmarks: of the 18 benchmarks that take less than fiveseconds for SuSLik, the average time is 0.5 seconds for SuSLik compared to 0.8 seconds for Cypress; the remaining four
hard benchmarks is where Cypress’s new search strategy
pays off: the average time for those four benchmarks is 18.8
seconds for SuSLik and only 6.3 seconds for Cypress.
5.2.3 Utility. To quantify synthesis utility, we measured
the ratio between the size of synthesized code and the input
specification (taken as AST sizes). For all benchmarks from956

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, Canada

the complex set, the generated code is larger than the specification by at least 2.2x (sorted list merge) and at most 12x(deallocate rose tree). This confirms our intuition that for
simple, boilerplate data structure manipulations, like deallocation and copying, synthesis offers a good trade-off, since
their specifications are very simple, while the code can bequite tricky. We only include pre- and postconditions inthe specification size and omit predicate definitions, sincethose are reused between benchmarks. Anecdotally, the new
benchmarks created for this paper were quick and easy towrite: most predicate definitions were either reused from
SuSLik or were standard SL predicates. In both cases, thepre- and postconditions were very straightforward. Notethat the code-to-spec ratios for the simple benchmarks arelower (between 0.2x and 8.0x), which serves as evidence
that deductive synthesis for heap-manipulating programs
delivers larger pay-off for complex traversals.
5.3

predicate ul). The simplest specification for intersection is:

Notable Benchmarks

Merge. One benchmark where Cypress surprised us ismerging two sorted lists (benchmark 17). We initially thoughtthat this problem required an extension to the tool, because
the traditional recursive implementationÐwithout auxiliariesÐ
has to unfold both input lists in order to compare their heads,
but then fold one of the lists back again to pass it to the recursive call; this łfolding backž is something that Cypress
does not explicitly support. To our surprise, Cypress was
instead able to solve this problem by inventing an auxiliarythat merges two lists one of which is non-empty. This implementation is even slightly more efficient, since it eliminates
a redundant emptiness check for one of the lists.
Sort. An important difference between the functional setting of [13] and our setting is that SL specifications givethe the user more fine-grained control over the relationshipbetween input and output data structures in memory. For
sorting (benchmark 16), we took the liberty of requiring thesort to be in-place, by using the following specification:{sll(x, n, l, h)} { {srtl(x, n, l, h)}Here sll is a list rooted at x with length n and lower and upperbounds on the elements l and h, and srtl is a sorted list withthe same parameters (notably, rooted at the same addressx). Such in-place sorting is not expressible using refinement
types from [13]. Given this specificationÐwhich contains
no insight as to which algorithm to use to sort the listÐ
Cypress synthesizes a rather peculiar version of in-place
insertion sort: while traditionally insertion sort on linked
lists performs insertion by switching next pointers, Cypress
chose instead to do it by swapping elements in out-of-order
list cells (similarly to a typical insertion sort on an array).

{r 7→ x ∗ ul(x, s 1 ) ∗ ul(y, s 2 )} { {r 7→ z ∗ ul(z, s 1 ∩ s 2 )}With this specification, however, Cypress fails to find a solution due to a limitation on the class of auxiliaries it cangenerate. Unlike the original functional setting, there is no
simple, fold-like solution for this specification, because it
is destructive: once it computes the intersection z ′ of y andthe tail of x , the list y is lost, and we cannot decide whether
the head of x should be added to z ′. A more sophisticatedsolution would require an auxiliary that tests membership,
which is beyond the capabilities of cyclic synthesis.
To circumvent this issue, we added ∗ul(y, s 2 ) to the postcondition to preserve the input list y. Even with this change,
however, Cypress fails to generate the simple solution witha single auxiliary (one that searches for the head of x in y,and if found, prepends it to z ′), because doing so requires
weakening of the auxiliary’s pure precondition, which cyclic
synthesis currently does not support. Surprisingly, Cypress
finds another solution, which uses a second auxiliary to append the head of x to z ′ instead of prepending it. This solution
is so unusual that we worried we found a soundness issue,
until we checked it with an external program verifier: thesolution is indeed correct (albeit inefficient), and both of theinferred auxiliary specifications are inductive.
5.4

Limitations

When does Cypress fail? The main limitation of SSL⟲
is that it can only derive a certain class of auxiliary functions.
Intuitively, it can only extract auxiliary specifications fromthe goals in the main derivation, and cannot invent them łoutof thin airž, so, for example, the auxiliary cannot take extra
parameters or return a new data structure, which the main
specification does not mention. For this reason, Cypress cannot synthesize linear-time implementations of list reversal
or tree flattening, which would require conjecturing an extra
accumulator parameter. As explained in Sec. 5.3, SSL⟲ also
lacks support for generalizing the pure part of the auxiliary
specification, which prevents it from deriving simpler version of set intersection. It is difficult to precisely characterize
the class of synthesis problems that cyclic synthesis can andcannot solve, because, as illustrated above, it often finds
alternative solutions that circumvent the limitations. Suchcharacterization is an interesting direction for future work;
another important and challenging direction is extending
SSL⟲ with additional rules to support a wider class of programs, while continuing to strike a careful balance between
expressiveness and tractability of proof search.
Quality of solutions. A Cypress solution might havesuboptimal performance even if a more efficient programis derivable via SSL⟲ . The core issue is that SSL⟲ has nomeans of analyzing program efficiency, and hence no reason
to prefer a more efficient solution. A promising approach for
producing efficient heap-manipulating would be to adopt a

Intersection. Perhaps the most curious case is benchmark
5, which computes the intersection of two sets represented as
linked lists with unique elements (denoted by the inductive957

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey

flavor of Separation Logic with time credits [15], combining
it with techniques for resource-aware synthesis for purefunctional programs [20].
We also noticed that the division of code between theprocedures in Cypress solutions is sometimes unnatural: forexample, the tree flattening program in Fig. 5 deallocatestree nodes inside the auxiliary append function instead of themain function; in terms of abstraction boundaries, it would
be better if append were only concerned with appending lists
and had no knowledge of tree nodes. The division of code
depends on the order in which Cypress tries applying synthesis rules (in this case, the relative order of Call and Free);currently the order is optimized for efficiency of proof searchrather than for optimal abstraction boundaries. We leave theinvestigation of improving program quality to future work.
Loop support. SSL⟲ currently has no support for loops,
which are often a more natural and efficient alternative torecursion in imperative programs. There are several existing
techniques for deductive verification of loops using cyclic
proofs [7, 43]; hence we believe the general cyclic synthesis
technique could be extended to also handle them. To keep
proof search tractable, however, we might not want to support both recursion and loops in our target language; a betteridea might be to synthesize tail-recursive programs and thentranslate them into loops using standard techniques. The
challenge, however, is that most tail-recursive programs require invented accumulator parameters (equivalently: mostloops require temporary variables). Hence adding support
for loops goes hand-in-hand with the extending the logic tosupport a wider class of auxiliaries.

termination measure by instantiating one of the pre-definedrecursion/looping schemas [19, 31].
Synthesis of auxiliary functions. Eguchi et al. [13] implement a technique for automatically synthesizing implementations of pure functional programs with recursive helper
functions from refinement types [45]. Their approach infers specifications for recursive helper functions by trying
a number of predefined templates for the łmainž function,
which exercise different flavours of recursion (structuralfolds or divide-and-conquer) on the input data structures.
Our work is complementary in that it considers imperative
heap-manipulating programs, and also takes a fundamentallydifferent proof-driven (rather than template-driven) approach
to identify recursion patterns. By doing so, our techniqueremoves the need to conjecture recursion principles upfront,
yet it is capable of discovering many of those automatically,
including non-trivial ones, such as traversals of a rose tree.
Several other techniques cannot synthesize recursive auxiliaries directly, but can synthesize nested folds [14] or nested
loops [31, 38, 40]. Out of these techniques, λ2 [14] is restricted
to a set of predefined templates, and also provides no correctness guarantees beyond a finite set of input-output examples.
Sketching-based approaches [31, 38, 40] are very flexible, but
require the programmer to provide an extensive program
sketch in order to make synthesis with nested loops tractable.
Cyclic proofs. The techniques and metatheory of cyclic
proofs originates in the logic and proof theory community.
Most related to our current work is the application of cyclic
proof to reasoning about program correctness [7, 35, 43], as
well as to proving pure entailments of Separation Logic withinductively defined predicates [6, 41, 42]. In particular, ouruse of cardinalities with Separation Logic coincides with theapproach used by Rowe and Brotherston [35].

6 Related Work
Deductive program synthesis. Our work on SSL⟲ extends a line of research on synthesizing programs from logical specifications [22, 31, 38, 40, 44], and, in particular, on deductive synthesis [12, 19, 24, 28], which implements a searchin the space of proofs of program correctness (rather thanin the space of programs). Our work is the first to combine
deductive synthesis with cyclic proof to generate provably
correct and terminating programs with complex recursion
patterns. Our technical contributions build primarily on thework by Polikarpova and Sergey [29], extending their logic
SSL and the tool SuSLik with ideas from cyclic proofs. The
best-first search algorithm of Cypress is inspired by theLeon system for deductive program verification, synthesis,
and repair [18, 19], but tailored to Separation Logic.
Our work advances the state of the art for deductive synthesis tools with regard to establishing termination of synthesized programs. Specifically, it enables automated derivationof a termination argument along with the program being
synthesized without being subject to restrictions of previous approaches: (1) requiring the user to provide an explicit
termination measure [28]; (2) restricting the recursion tosyntactic structural one [27, 29]; and (3) determining the

7 Conclusion
We have demonstrated that cyclic proofs, already known as
an automation-friendly method for reasoning about program
termination, can also be an effective tool for automaticallysynthesizing programs with recursive auxiliary functions. By
investigating this synergy between verification and synthesis, we have once again witnessed that the ideas developedby the logic community for scalable reasoning about heapmanipulating procedures can be instrumental in practicalsynthesis of correct-by-construction programs.

Acknowledgments
The authors would like to thank the anonymous reviewers
and our shepherd, Kwangkeun Yi, for their valuable feedback
on earlier drafts of this paper. This work was supported by
the National Science Foundation under Grant No. 1911149,
by Singapore MoE Tier 1 Grant No. IG18-SG102, by the Israeli
Science Foundation (ISF) Grants No. 243/19 and 2740/19, andby the United States-Israel Binational Science Foundation(BSF) Grant No. 2018675.

958

Cyclic Program Synthesis

PLDI ’21, June 20ś25, 2021, Virtual, Canada

References[19] Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013.
Synthesis modulo recursive functions. In OOPSLA. ACM, 407ś426.
https://doi.org/10.1145/2544173.2509555[20] Tristan Knoth, Di Wang, Nadia Polikarpova, and Jan Hoffmann. 2019.
Resource-guided program synthesis. In PLDI. ACM, 253ś268. https://doi.org/10.1145/3314221.3314602[21] Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. 2010.
Complete Functional Synthesis. In PLDI. 316ś329. https://doi.org/10.
1145/1809028.1806632[22] K. Rustan M. Leino and Aleksandar Milicevic. 2012. Program Extrapolation with Jennisys. In OOPSLA. ACM, 411ś430. https://doi.org/10.
1145/2398857.2384646[23] Grant Malcolm. 1990. Data Structures and Program Transformation.
Sci. Comput. Program. 14, 2-3 (1990), 255ś279. https://doi.org/10.1016/
0167-6423(90)90023-7[24] Zohar Manna and Richard J. Waldinger. 1980. A Deductive Approachto Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (1980),90ś121. https://doi.org/10.1145/357084.357090[25] Damian Niwiński and Igor Walukiewicz. 1996. Games for the µhttps:
Calculus. Theor. Comput. Sci. 163, 1&2 (1996), 99ś116.
//doi.org/10.1016/0304-3975(95)00136-0[26] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local
Reasoning about Programs that Alter Data Structures. In CSL (LNCS,
Vol. 2142). Springer, 1ś19. https://doi.org/10.1007/3-540-44802-0_1[27] Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-exampledirected program synthesis. In PLDI. ACM, 619ś630. https://doi.org/
10.1145/2737924.2738007[28] Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In PLDI. ACM,
522ś538. https://doi.org/10.1145/2980983.2908093[29] Nadia Polikarpova and Ilya Sergey. 2019. Structuring the Synthesis
of Heap-Manipulating Programs. Proc. ACM Program. Lang. 3, POPL
(2019), 72:1ś72:30. https://doi.org/10.1145/3290385[30] Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy
Madhusudan. 2013. Natural proofs for structure, data, and separation.
In PLDI. ACM, 231ś242. https://doi.org/10.1145/2499370.2462169[31] Xiaokang Qiu and Armando Solar-Lezama. 2017. Natural synthesis ofprovably-correct data-structure manipulations. PACMPL 1, OOPSLA(2017), 65:1ś65:28. https://doi.org/10.1145/3133889[32] Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, andClark W. Barrett. 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In CAV (Part II) (LNCS, Vol. 9207). Springer,
198ś216. https://doi.org/10.1007/978-3-319-21668-3_12[33] Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett,and Morgan Deters. 2019. Refutation-based synthesis in SMT. Formal
Methods Syst. Des. 55, 2 (2019), 73ś102. https://doi.org/10.1007/s10703017-0270-2[34] John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable
Data Structures. In LICS. IEEE Computer Society, 55ś74. https://doi.
org/10.1109/LICS.2002.1029817[35] Reuben N. S. Rowe and James Brotherston. 2017. Automatic cyclic
termination proofs for recursive procedures in separation logic. In
CPP. ACM, 53ś65. https://doi.org/10.1145/3018610.3018623[36] Luigi Santocanale. 2002. A Calculus of Circular Proofs and Its Categorical Semantics. In FoSSaCS (LNCS, Vol. 2303). Springer, 357ś371.
https://doi.org/10.1007/3-540-45931-6_25[37] Alex Simpson. 2017. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In FoSSaCS (LNCS, Vol. 10203). Springer, 283ś300. https://doi.org/10.1007/978-3-662-54458-7_17[38] Armando Solar-Lezama. 2013. Program sketching. STTT 15, 5-6 (2013),
475ś495. https://doi.org/10.1007/s10009-012-0249-7[39] Christoph Sprenger and Mads Dam. 2003. On the Structure of Inductive
Reasoning: Circular and Tree-Shaped Proofs in the µ-Calculus. In
FoSSaCS (LNCS, Vol. 2620). Springer, 425ś440. https://doi.org/10.1007/
3-540-36576-1_27[1] Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In CAV (Part II) (LNCS, Vol. 9780). Springer,934ś950. https://doi.org/10.1007/978-3-642-39799-8_67[2] Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin,
Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando
Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntaxguided synthesis. In FMCAD. IEEE, 1ś8. https://doi.org/10.1145/
3434311[3] David Baelde, Amina Doumane, and Alexis Saurin. 2016. Infinitary
Proof Theory: the Multiplicative Additive Case. In CSL (LIPIcs, Vol. 62).
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 42:1ś42:17. https://doi.org/10.4230/LIPIcs.CSL.2016.42[4] Josh Berdine and Nikolaj Bjùrner. 2014. Computing All Implied
Equalities via SMT-Based Partition Refinement. In IJCAR. 168ś183.
https://doi.org/10.1007/978-3-319-08587-6_12[5] Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Symbolic Execution with Separation Logic. In APLAS (LNCS, Vol. 3780).
Springer, 52ś68. https://doi.org/10.1007/11575467_5[6] James Brotherston. 2007. Formalised Inductive Reasoning in the Logicof Bunched Implications. In SAS (LNCS, Vol. 4634). Springer, 87ś103.
https://doi.org/10.1007/978-3-540-74061-2_6[7] James Brotherston, Richard Bornat, and Cristiano Calcagno. 2008.
Cyclic proofs of program termination in separation logic. In POPL.
ACM, 101ś112. https://doi.org/10.1145/1328897.1328453[8] James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen. 2012. A Generic Cyclic Theorem Prover. In APLAS (LNCS,
Vol. 7705). Springer, 350ś367. https://doi.org/10.1007/978-3-642-351822_25[9] James Brotherston and Alex Simpson. 2011. Sequent Calculi for Induction and Infinite Descent. J. Log. Comput. 21, 6 (2011), 1177ś1216.
https://doi.org/10.1093/logcom/exq052[10] Coq Development Team. 2020. The Coq Proof Assistant Reference
Manual - Version 8.11. Available at http://coq.inria.fr/.
[11] Anupam Das and Damien Pous. 2018. Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices). In CSL (LIPIcs, Vol. 119).
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 19:1ś19:18. https://doi.org/10.4230/LIPIcs.CSL.2018.19[12] Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam
Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types ina Proof Assistant. In POPL. ACM, 689ś700. https://doi.org/10.1145/
2775051.2677006[13] Shingo Eguchi, Naoki Kobayashi, and Takeshi Tsukada. 2018. Automated Synthesis of Functional Programs with Auxiliary Functions. In
APLAS (LNCS, Vol. 11275). Springer, 223ś241. https://doi.org/10.1007/
978-3-030-02768-1_13[14] John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing
data structure transformations from input-output examples. In PLDI.
ACM, 229ś239. https://doi.org/10.1145/2737924.2737977[15] Armaël Guéneau, Arthur Charguéraud, and François Pottier. 2018.
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via
Deductive Program Verification. In ESOP (LNCS, Vol. 10801). Springer,533ś560. https://doi.org/10.1007/978-3-319-89884-1_19[16] Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, andIlya Sergey. 2021. Cyclic Program Synthesis. Technical Report. University of California, San Diego. https://cseweb.ucsd.edu/~npolikarpova/
publications/cypress-extended.pdf[17] Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, andIlya Sergey. 2021. Cypress (PLDI 2021 Artifact): Code and Benchmarks.
https://doi.org/10.5281/zenodo.4679743[18] Etienne Kneuss, Manos Koukoutos, and Viktor Kuncak. 2015. Deductive Program Repair. In CAV (LNCS, Vol. 9207). Springer, 217ś233.
https://doi.org/10.1007/978-3-319-21668-3_13959

PLDI ’21, June 20ś25, 2021, Virtual, Canada

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey[40] Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. 2010. From
program verification to program synthesis. In POPL. ACM, 313ś326.
https://doi.org/10.1145/1706299.1706337[41] Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan
Chin. 2016. Automated Mutual Explicit Induction Proof in Separation
Logic. In FM (LNCS, Vol. 9995), John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer, 659ś676.
[42] Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan
Chin. 2018. Automated lemma synthesis in symbolic-heap separation
logic. Proc. ACM Program. Lang. 2, POPL (2018), 9:1ś9:29. https://doi.org/10.1145/3158097[43] Gadi Tellez and James Brotherston. 2020. Automatically Verifying
Temporal Properties of Pointer Programs with Cyclic Proof. J. Autom.
Reasoning 64, 3 (2020), 555ś578. https://doi.org/10.1007/978-3-31963046-5_30[44] Emina Torlak and Rastislav Bodík. 2014. A lightweight symbolic
virtual machine for solver-aided host languages. In PLDI. ACM, 530ś
541. https://doi.org/10.1145/2666356.2594340[45] Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon
L. Peyton Jones. 2014. Refinement types for Haskell. In ICFP. ACM,
269ś282. https://doi.org/10.1145/2628136.2628161

960