Bottom-Up Synthesis of Memory Mutations
with Separation Logic

Bottom-up enumeration with an OE-reduction uses a component set $𝒞$ comprising functions, operators, variables, and literals, to search for a program specified by a vector of input-output examples, $\overrightarrow{ℰ}$, where each example is of the form $\iota \to \omega$. For each program we compute its equivalence class’s label. In classical OE, we use its evaluation result, $⟦p⟧(\iota )$, for each $\iota$ in $\overrightarrow{ℰ}$. In our example, the expression arr has the observed behavior $[10,100,90,-1,2]$ on the provided input, so its equivalence class is $⟨[10,100,90,-1,2]⟩$.

To enumerate the space of programs, we use a bank to store representatives of equivalence classes, as seen in Figure 1(a). For each function or operator $f\in 𝒞$ with arity $k$, we collect all $k$-tuples of programs already in the bank and use them as arguments to apply $f$. This is usually done with some notion of iterations, e.g., as in Figure 1(a), by increasing number of AST nodes. When enumerating programs of AST size 5, then, the enumerator considers the component array dereference ([]), which has an arity of $2$. Among pairs of programs collected from the bank with a total size of 4 will be the program arr, representative of the equivalence class $⟨[10,100,90,-1,2]⟩$, and the program n - 1, representative of $⟨4⟩$. Applying array dereference yields arr[n - 1] with the observed behavior $⟨2⟩$. Crucially, we do not have to evaluate the full program arr[n - 1] to get this value: we can use observed values $[10,100,90,-1,2]$ and $4$ and only compute the final step.

When the enumeration finds a program from an equivalence class with no representative in the bank – i.e., no program in the bank has the same label – it is added to the bank to be used when constructing larger programs. This is the case with arr[n - 1], which is added to the bank at size 5. Alternatively, if a representative of the equivalence class already exists in the bank, we discard the new program. If a program’s observed values are equal to the provided outputs, the program is a solution. Since we only use discovered equivalence classes (i.e., programs) to construct larger programs, the effect of OE’s pruning compounds.

We quickly run into issues when $𝒞$ contains functions or operators that can cause side-effects. The next step in solving our example is to enumerate arr.sort()[0] + arr[n - 1]. But, as we are about to see, using the classical approach this program will not be evaluated correctly, and it may even be pruned away.

We already saw how the subprogram $p_1=$ arr[n - 1] was enumerated and labeled $⟨2⟩$, and $p_2=$ arr.sort()[0] will be enumerated similarly: at size 4, it will be composed from arr.sort() (size 2) and 0 (size 1), and added to the bank as a representative of $⟨-1⟩$.

The first source of trouble is that OE is a dynamic programming algorithm: when constructing the larger $p_2$ + $p_1$, the enumerator uses the memoized observed values to compute: $⟨-1+2⟩=⟨1⟩$. However, since $p_2$ modifies arr, $p_2$ + $p_1$ actually evaluates to 99 on the input $\iota$. Worse, this erroneous value means the synthesizer will consider $p_2$ + $p_1$, our solution, equivalent to $p_1$ + $p_2$ so it may be discarded. While a seemingly simple solution is to just evaluate the program in full each time, ensuring labels are correct, this is not only expensive, depending on the operation, but more importantly, insufficient. If the synthesizer sees the constant value $2$, e.g., by enumerating 1 + 1, this would cause the larger – and seemingly equivalent – arr[n - 1] to be discarded. OE hinges on the enumeration only discarding a program when it already has a suitable replacement, but arr[n - 1] evaluated after arr.sort() would still have no equivalent program in the bank.

Our problem was not distinguishing between the same program when evaluated using different values of arr. We also saw in Section 1 the need for distinction between programs that return the same value, but their effect on variables is different, e.g., n and n++ when evaluated using the same value of n.

We replace programs with triples in Concrete Heap Separation Logic (CHSL): the precondition records the variables before its evaluation, and the postcondition comprises an assertion recording the variables after evaluation and the result of the evaluation, like so:

From here on, we name the original array value $ar{r}_{\text{orig}}$ and its sorted value $ar{r}_{\text{sort}}$, and use them in our examples and figures for brevity. In this representation, we can tell apart these two triples:

where the first is arr evaluated on the original array, returning the original array value, and the second is evaluated on a state where the array has been sorted, returning the sorted value. We use the second triple to construct larger programs evaluated after sort().

Notice that since all values are concrete, CHSL does not need domain- or library-specific inference rules to connect the pre- and postcondition of the triple, but can rely entirely on evaluation.

These pre- and postconditions do not encode fully-concrete states, they leave n unconstrained. This makes our representation of the space more compact: the triple $\{\text{arr}\mapsto ar{r}_{\text{orig}}\}\text{arr}\text{.}\text{sort}\text{()}\{\text{arr}\mapsto ar{r}_{\text{sort}};ar{r}_{\text{sort}}\}$ takes advantage of the fact that only constraining arr is sufficient to reason about the behavior of this program. We only need to constrain the footprint of the program.

CHSL includes the notion of the separating conjunction $\ast$ to indicate separate parts of the heap (or, in our case, variable store) that can be reasoned about locally. Thanks to aliasing restrictions of the synthesizer’s target language detailed in Section 3.1, any two variables can be separated with $\ast$. E.g., the assertion $\text{arr}\mapsto ar{r}_{\text{orig}}\ast \text{n}\mapsto 5$ describes the concrete initial state. Once we replace the programs in our bank with CHSL triples, we can now further borrow from Separation Logic when considering evaluation sequences.

Let us consider the last subprogram of our target program: arr[n - 1]. It is going to be added with arr.sort()[0], which means that for that composition to be allowed, it must match the state after arr is sorted. Specifically, we consider the first argument of the array dereference, which will be needed to enumerate it:

Importantly, this triple will never be enumerated if the enumerator only considers triples starting at a precondition describing the initial state, but without it we will never find the target program.

We have to ensure, therefore, that we also enumerate programs that have other preconditions. $t{r}_3$ is a necessary building block for such programs.

To this end, whenever a new assertion is discovered by the enumerator, e.g., when a mutating component is evaluated, creating a never-before-seen assertion in the postcondition, as enumerating $\{\text{arr}\mapsto ar{r}_{\text{orig}}\}\text{arr}\text{.}\text{sort}\text{()}\{\text{arr}\mapsto ar{r}_{\text{sort}};ar{r}_{\text{sort}}\}$ does, we get ready to enumerate programs that begin in this new assertion: we create $t{r}_3$, which any program starting at $\text{arr}\mapsto ar{r}_{\text{sort}}$ will need to incorporate, and add it to the bank, which also adds $\text{arr}\mapsto ar{r}_{\text{sort}}$ to the bank as a precondition. The next time the enumerator selects arguments to an operator, $t{r}_3$ will be available. This lets the enumerator create programs that begin at $\text{arr}\mapsto ar{r}_{\text{sort}}$.

Now that we have $t{r}_3$, the first argument to the array dereference, let us consider the second:

We enumerate this program at the initial value of n, i.e., without the need for its precondition to be discovered. However, when the enumerator tries to compose it with $t{r}_3$ into a sequence of arguments to [], it runs into a problem: the two triples do not make a valid sequence. The assertion in the postcondition of the first argument, $\text{arr}\mapsto ar{r}_{\text{sort}}$, is different than the precondition of the following argument, $\text{n}\mapsto 5$.

However, we clearly see that these two assertions deal with separate parts of the heap, and do not interfere with each other. This is where we draw on Separation Logic’s powerful tool: the Frame rule. Since these are separate parts of the heap, we can use the separating conjunction to create a unified heap in the pre- and postcondition of both triples. The more constrained triples are now composable, so the enumerator can apply array dereference and Eval, yielding:

The full derivation is shown in Figure 3. Then similarly, the same extension – now adding $\text{n}\mapsto 5$ to $t{r}_2$ and nothing to the second argument – is applied to allow the enumerator to compose the target program. This is an important strength of our technique: the same triple for n - 1 can compose with any value for arr – we will only enumerate it once!

We notice that in this case, this will discover a new assertion not as a postcondition as we did when sort() mutated arr but as a precondition. Once the program is added to the bank, the enumerator will continue to enumerate more programs with this new assertion as their precondition.

The equivalence class labels above define an equivalence relation for OE. However, in this setting, we can do even better: there are cases where we want to discard programs even though one is not equivalent to the other. Let us consider two triples:

where emp is the unconstrained heap.

Both triples have the same evaluation result (0), and the same effect (no effect), but different assertions at the pre- and postconditions. But they are not completely different: if we select a frame axiom $R=\text{n}\mapsto 5$, we can bridge their difference: $\{\text{emp}\ast R\}\text{0}\{\text{emp}\ast R;0\}$ is equivalent to $t{r}_4$. Under this condition, we say that $t{r}_5$ is more general than $t{r}_4$: it describes a program that behaves the same over more concrete states. If we let the more general equivalence class subsume less general ones, we further compact our representation of the space while remainting correct. While we cannot tractably apply this additional reduction to the entire space, we can at least discard less general programs once more general ones exist in the bank.

This tactic cannot stand on its own: naively employing it means $t{r}_6=\{\text{emp}\}\text{5}\{\text{emp};5\}$ subsumes $t{r}_7=\{\text{n}\mapsto 5\}\text{n}\{\text{n}\mapsto 5;5\}$ in the same way. However, in Figure 2 similar subsumptions do not happen: $\{\text{emp}\}\text{-}\text{1}\{\text{emp};-1\}$ does not subsume $\{\text{arr}\mapsto ar{r}_{\text{sort}}\}\text{arr}\text{[}\text{0}\text{]}\{\text{arr}\mapsto ar{r}_{\text{sort}};-1\}$ and $\{\text{arr}\mapsto ar{r}_{\text{orig}}\ast \text{n}\mapsto 5\}\text{arr}\text{[}\text{n}\text{-}\text{(}\text{1}\text{+}\text{1}\text{)]}\{\text{arr}\mapsto ar{r}_{\text{orig}}\ast \text{n}\mapsto 5;-1\}$, which are still in the bank. Why?

We notice that if these subsumptions are allowed, the programs will no longer be interchangeable, and some will break entirely. Consider the application of ++: while $\{\text{n}\mapsto 5\}\text{n}\text{++}\{\text{n}\mapsto 6;5\}$ uses $t{r}_7$ as its argument, 5++ using $t{r}_6$ does not compile. Likewise, replacing arr within arr.sort() with the array literal with arr’s value would produce a different mutation of the heap, indicting they should be separate programs. The difference, which must be encoded into our representation, is what is reachable from state variables, and if so, from where.

Our evaluation result therefore comprises two components: the value returned by evaluation, and the location of that value. $t{r}_3$, then, returns $ar{r}_{\text{sort}}\mathrm{@}\text{arr}$, and $t{r}_7$ returns $5\mathrm{@}n$. This ensures the interchangeability within ++ or sort: the new program will not only compile, it will affect the same variable.

What, then, should be the location of a temporary variable, i.e., a variable that is not reachable from the stack? We must consider the location’s purpose: to separate programs enough to preserve interchangeability when the heap is mutated. Two temporary values, on the other hand, are (inherently) interchangeable, so we do not want to over-separate them which would inflate the number of equivalence classes in the bank. We therefore give all temporary values the same location: $\perp$. This way, $t{r}_4$ and $t{r}_5$ both return $0\mathrm{@}\perp$, preserving the subsumption, and $t{r}_6$ returns $5\mathrm{@}\perp$ which separates it from $t{r}_7$.

Figure 2 omits this for simplicity, but does still separate $\{\text{emp}\}\text{-}\text{1}\{\text{emp};-1\}$ with result $-1\mathrm{@}\perp$ from $\{\text{arr}\mapsto ar{r}_{\text{sort}}\}\text{arr}\text{[}\text{0}\text{]}\{\text{arr}\mapsto ar{r}_{\text{sort}};-1\}$ with result $-1\mathrm{@}arr[0]$ and from $\{\text{arr}\mapsto ar{r}_{\text{orig}}\ast \text{n}\mapsto 5\}\text{arr}\text{[}\text{n}\text{-(}\text{1}\text{+}\text{1}\text{)]}\{\text{arr}\mapsto ar{r}_{\text{orig}}\ast \text{n}\mapsto 5;-1\}$ with result $-1\mathrm{@}arr[3]$.

We are almost finished: like classical OE, we continue iteratively enumerating programs into the bank until a solution is found. Our final step is to reconsider the definition of a solution to a synthesis specification.

When enumerating a program in a non-mutating space with an OE-reduction using the examples’ inputs, a solution is a program that is labeled by (i.e., that evaluates to) the provided outputs. In SObEq this is insufficient: the enumerator can find a triple returning the correct value in some precondition. To be correct when evaluated on the concrete example inputs, we require that a solution’s precondition describe the concrete initial state $\iota$. In our example, $\text{arr}\mapsto ar{r}_{\text{orig}}\ast \text{n}\mapsto 5$ trivially describes $\iota$ – it is equal to it – but so does $\text{n}\mapsto 5$.

Thus, to be a solution, a triple must: 1) return the values of the example outputs, and 2) have a precondition that describes $\iota$.

SObEq is, to our knowledge, the first proof-directed synthesis algorithm that works bottom-up. It is also the first bottom-up enumerative synthesizer for general mutating components with a correctness guarantee: if a solution exists in the space spanned by $𝒞$, SObEq will find an equivalent solution.

In CHSL, we use a heap notation to reason about the concrete values assigned to variables from the input. We can reason locally about each individual variable because SObEq’s target language does not allow assignments, and so as long as nothing is aliased at the input – we can enforce this when generating the synthesis task – each variable is separate from all others and can be separated from them with a separating conjunction, $\ast$.

CHSL reasons about concrete values assigned to variables. As such, a CHSL assertion comprises heaplets of the form $x\mapsto v$ where $v$ is a concrete value.

This also means we can trivially transform a state (partial function) $\sigma$ into an assertion describing an identical heap s.t. $x_1\mapsto \sigma (x_1)\ast \mathrm{\cdots }\ast x_n\mapsto \sigma (x_n)$ for all $x_i\in dom(\sigma )$. We use the function interchangeably with its assertion equivalent, i.e., $\sigma$ as a shorthand for the assertion above.

For a vector of states $\overrightarrow{\sigma }$, corresponding to the vector of examples $\overrightarrow{ℰ}$, CHSL likewise uses a vector of assertions. We therefore also define a vector separating conjunction s.t. $\overrightarrow{P}\ast \overrightarrow{R}={⟨P_i\ast R_i⟩}_i$.

In the presence of mutations, we must also consider that some values are reachable from our heap. As shown in Section 2, this is important for components that modify their arguments (e.g. arr.sort()), especially components that return a self-reference and are therefore composable, as in arr.sort().reverse(), where both sort and reverse mutate arr.

To support this, a result $r\in ℛ$ comprises two components: a value and that value’s location, $l\in ℳ$ that can be a variable, a variable at a concrete index, or $\perp$. We use $\perp$ to indicate a value not reachable from any variable, i.e., a temporary value. We decompose the result as $r=v\mathrm{@}l$. As with variable values, the values in results are concrete.

A triple in CHSL comprises a precondition $\overrightarrow{P}\in {𝒜}^k$ (where $|\overrightarrow{ℰ}|=k$), the program $p$, and a postcondition. Our postconditions have two components: i) an assertion $\overrightarrow{Q}\in {𝒜}^k$, and ii) the evaluation results of $p$ on $\overrightarrow{P}$. Vectors of assertions and results form a conjunction: $\{\overrightarrow{P}\}p\{\overrightarrow{Q};\overrightarrow{r}\}$ means all triples $\{P^1\}p\{Q^1;r^1\},\{P^2\}p\{Q^2;r^2\},\mathrm{\dots },\{P^k\}p\{Q^k;r^k\}$ hold.

We call the subset of each assertion $Q$ whose values are different from $P$ the effect of the program on $P$. For example, in the triple $\{\text{x}\mapsto 1\ast \text{y}\mapsto 2\}\text{x}\text{++}\text{+}\text{y}\{\text{x}\mapsto 2\ast \text{y}\mapsto 2;3\}$ the effect is $\text{x}\mapsto 2$.

We consider $\{\overrightarrow{P}\}p\{\overrightarrow{Q};\overrightarrow{r}\}$ to be a valid triple if it accurately tracks the evaluation of $p$ on $\overrightarrow{P}$. In other words, assuming a (deterministic) small-step operational semantics for programs the behavior of which is defined by the interpreter of the language: $\to :(\mathbb{P},𝒜)\to (ℛ,𝒜)$, we say $\{\overrightarrow{P}\}p\{\overrightarrow{Q};\overrightarrow{r}\}$ is valid if $\forall 1\le i\le k.(p,P^i)\to (r^i,Q^i)$.

Because SObEq will be enumerating triples, it is crucial that it can construct valid triples.

When constructing a new triple, the Eval rule denotes the use of the interpreter to ensure the resulting triple is valid. Because an evaluation of an AST node will first evaluate its children in sequence, then use the results to evaluate the node’s operation, Eval requires a sequence of triples. As in the classical Hoare Logic Sequence rule, Eval requires matching midconditions. However, since we often want to form a sequence from triples where $Q_i\ne P_{i+1}$, we use the Frame rule to find a larger composed heap where the midconditions do match.

Generally, all triples in the space contain only their footprint in their pre- and postcondition. As the example in Figure 3 shows, in this compact representation midconditions may not match. We recall that the frame rule allows us to reason about a larger heap by equally extending the pre- and postcondition with an additional assertion called the frame axiom.

Fortunately, in CHSL, frame axioms are very easy to find. To prepare a pair of arguments for Eval, then, one of two things is true: either for every $i$, $Q_1^i\cup P_2^i$ is still a partial function (i.e., if the same variable appears in both, it maps to the same value) and $R_1^i,R_2^i$ are found by their difference, or the two triples cannot form a valid sequence.

When the SObEq enumeration will apply a function or operator $f$ to $k$ child triples, this will combine the two rules. Since not all valid sequences of possible arguments to $f$ have matching midconditions, we apply the Frame rule to the entire sequence: given a set of $k=\text{arity}(f)$ triples $t{r}_i=\{{\overrightarrow{P}}_i\}{p}_i\{{\overrightarrow{Q}}_i;{\overrightarrow{r}}_i\}$, Eval is applicable if there exist $k$ frame axioms ${\overrightarrow{R}}_1,\mathrm{\dots },{\overrightarrow{R}}_k$ where ${\overrightarrow{Q}}_1\ast {\overrightarrow{R}}_1={\overrightarrow{P}}_2\ast {\overrightarrow{R}}_2,{\overrightarrow{Q}}_2\ast {\overrightarrow{R}}_2={\overrightarrow{P}}_3\ast {\overrightarrow{R}}_3,\mathrm{\dots },{\overrightarrow{Q}}_{k-1}\ast {\overrightarrow{R}}_{k-1}={\overrightarrow{P}}_k\ast {\overrightarrow{R}}_k$. Some of these ${\overrightarrow{R}}_i$ may be $\overrightarrow{\text{emp}}$. Now that the midconditions of the triples match, Eval can be applied, yielding a triple that evaluates from the new shared precondition $\overrightarrow{P_1}\ast \overrightarrow{R_1}$, and computing the result and precondition for $f(p_1,\mathrm{\dots },p_k)$.

We denote the vector of input states $\overrightarrow{I}={⟨{\iota }_i\mid {\iota }_i\to {\omega }_i⟩}_i$. The direct translation of $\overrightarrow{ℰ}$ to CHSL, then, is $\{\overrightarrow{P}\}\mathrm{\_}\{\mathrm{\_};{⟨{\omega }_i\mathrm{@}\mathrm{\_}⟩}_i\}$, where $\exists \overrightarrow{R}.\overrightarrow{P}\ast \overrightarrow{R}=\overrightarrow{I}$. In other words, the precondition needs to describe the initial states (it is a footprint, so it may not describe all input variables), any postcondition will satisfy our specification, and the correct values can be at any location.

Users may want to constrain specific mutations as well as the value. We let the user pair with each example any constraints on the effect, e.g., the value of n must be $9$, or arr must end in its initial value $[10,100,90,-1,2]$. To do this, we let the user provide an effect constraint $q:𝒱\to 𝒦$, constraining the target value for any variable, where if $x\notin dom(q)$, $x$ is unconstrained.

A PBE user does not need to know about CHSL. Much like the original $\overrightarrow{ℰ}$, they provide a vector $\overrightarrow{\mathrm{\Phi }}$ where each $\phi \in \overrightarrow{\mathrm{\Phi }}$ is a pair of example and effect constraint: $\phi =(\iota \to \omega ,q)$. If they are unconcerned with effects, this is identical to providing $\overrightarrow{ℰ}$.

We then turn $\overrightarrow{\mathrm{\Phi }}$ into a synthesis goal in CHSL:

The SObEq task is to find a triple $\{\overrightarrow{\sigma }\}p\{{\overrightarrow{\sigma }}^{\prime };\overrightarrow{r}\}$ that matches ${𝒢}_{\overrightarrow{\mathrm{\Phi }}}$.

In a problem domain with no side-effects, observational equivalence unifies programs with the same evaluation results on the example inputs. This is expressed in the equivalence relation ${\equiv }_{\overrightarrow{ℰ}}$ that deems two programs $p_1,p_2$ (observationally) equivalent if $\forall \iota \to \omega \in \overrightarrow{ℰ}.⟦p_1⟧(\iota )=⟦p_2⟧(\iota )$. The OE-reduced space ${⦇𝒞⦈}^{OE}$ is then defined using ${\equiv }_{\overrightarrow{ℰ}}$. This idea was first suggested by Udupa et al. [59] and Albarghouthi et al. [2] and is in wide use today.

A classical bottom-up enumeration (CBE), keeps a bank of programs, and the vector of observed results is used to label the program’s equivalence class. Only one program with each vector is added to the bank, meaning any observationally equivalent programs are discarded.

In the presence of mutations, the space of possible programs no longer comprises only programs evaluated in the initial states $\overrightarrow{I}$. As we saw in Section 2, composition in this space requires subprograms that are evaluated in a modified state.

The full program space when $ℱ$ includes mutations is constructed inductively, building larger valid triples from smaller ones via applications of Eval, and the Frame rule when necessary. We denote the possible values for each $x\in 𝒱$ as ${𝒦}_x$. We define the full space of programs $⦇𝒞⦈$:

Finally, given $⦇𝒞⦈$, we can define the OE-reduced space that SObEq will enumerate.

Finally, we consider the generality ordering of triples and (implicitly) of their equivalence classes, which will let us find more general programs.

In Section 2, we considered the two triples $t{r}_4=\{\text{n}\mapsto 5\}\text{n}\text{-}\text{n}\{\text{n}\mapsto 5;0\mathrm{@}\perp \}$ and $t{r}_5=\{\text{emp}\}\text{0}\{\text{emp};0\mathrm{@}\perp \}$. While $t{r}_4$ and $t{r}_5$ are not observationally equivalent under Definition 3, as $\text{emp}\ne \text{n}\mapsto 5$, $t{r}_5$ is more general than $t{r}_4$: it produces the same result ($0\mathrm{@}\perp$) and the same effect ($\mathrm{\varnothing }$) from more concrete states. If $t{r}_5$ can absorb $t{r}_4$, we can arrive at a more compact representation of the space. To this end, we formally define this generality: the partial order of programs that differ by only a more general pre- and postcondition.

While ${⊑}_{\overrightarrow{\mathrm{\Phi }}}$ is clearly not an equivalence relation (the existence of a frame axiom is not symmetrical) so it cannot be used to partition the space into classes, we notice that replacing a triple with one that is larger according to ${⊑}_{\overrightarrow{\mathrm{\Phi }}}$ does preserve the two properties of an OE-relation, interchangeability and consistency, in one direction. Originally [45], interchangeability states that swapping two equivalent programs within a larger program will yield an equivalent larger program, and consistency states that two equivalent programs either both satisfy a given specification $\phi$ or neither does. Under $⊑$, however, a slightly weaker – but still useful – version holds.

Interchangeability under ${⊑}_{\overrightarrow{\mathrm{\Phi }}}$ means that given $f\in ℱ,\text{arity}(f)=k$, $k$ triples $t{r}_j=\{{\overrightarrow{P}}_j\}{p}_j\{{\overrightarrow{Q}}_j;{\overrightarrow{r}}_j\}$, $1\le j\le k$, and $k$ assertions ${\overrightarrow{R}}_j$ s.t. Eval can be applied on $f$ and $\{{\overrightarrow{P}}_j\ast \overrightarrow{R_j}\}{p}_j\{{\overrightarrow{Q}}_j\ast \overrightarrow{R_j};{\overrightarrow{r}}_j\}$ to infer $\{\overrightarrow{P}\}f(p_1,\mathrm{\dots },p_k)\{\overrightarrow{Q};\overrightarrow{r}\}$, and a triple $t{r}_i^{\prime }=\{{\overrightarrow{P}}_i^{\prime }\}{p}_i^{\prime }\{{\overrightarrow{Q}}_i^{\prime };{\overrightarrow{r^{\prime }}}_i\}$ s.t. $t{r}_i{⊑}_{\overrightarrow{\mathrm{\Phi }}}t{r}_i^{\prime }$ for some $1\le i\le k$, then:

1. 1.

   There exists ${\overrightarrow{R^{\prime }}}_i$ s.t. Eval can still be applied on $f$ when replacing $\{{\overrightarrow{P}}_i\ast \overrightarrow{R_i}\}{p}_i\{{\overrightarrow{Q}}_i\ast \overrightarrow{R_i};{\overrightarrow{r}}_i\}$ with $\{{\overrightarrow{P^{\prime }}}_i\ast \overrightarrow{R_i^{\prime }}\}{p}_i^{\prime }\{{\overrightarrow{Q^{\prime }}}_i\ast \overrightarrow{R_i^{\prime }};{\overrightarrow{r^{\prime }}}_i\}$ to infer $\{\overrightarrow{P^{\prime }}\}f(p_1,\mathrm{\dots },p_i^{\prime },\mathrm{\dots },p_k)\{\overrightarrow{Q^{\prime }};\overrightarrow{r^{\prime }}\}$, and

2. 2.

   $\{\overrightarrow{P}\}f(p_1,\mathrm{\dots },p_k)\{\overrightarrow{Q};\overrightarrow{r}\}{⊑}_{\overrightarrow{\mathrm{\Phi }}}\{\overrightarrow{P^{\prime }}\}f(p_1,\mathrm{\dots },p_i^{\prime },\mathrm{\dots },p_k)\{\overrightarrow{Q^{\prime }};\overrightarrow{r^{\prime }}\}$

Consistency under ${⊑}_{\overrightarrow{\mathrm{\Phi }}}$ means that for goal $𝒢$, if $\{{\overrightarrow{P}}_1\}{p}_1\{{\overrightarrow{Q}}_1;{\overrightarrow{r}}_1\}{⊑}_{\overrightarrow{\mathrm{\Phi }}}\{{\overrightarrow{P}}_2\}{p}_2\{{\overrightarrow{Q}}_2;{\overrightarrow{r}}_2\}$, then if there exists $\overrightarrow{R_1}$ s.t. $\{{\overrightarrow{P}}_1\ast \overrightarrow{R_1}\}{p}_1\{{\overrightarrow{Q}}_1\ast \overrightarrow{R_1};{\overrightarrow{r}}_1\}$ matches $𝒢$, then there exists $\overrightarrow{R_2}$ s.t. $\{{\overrightarrow{P}}_2\ast {\overrightarrow{R}}_2\}{p}_2\{{\overrightarrow{Q}}_2\ast {\overrightarrow{R}}_2;{\overrightarrow{r}}_2\}$ matches $𝒢$. It’s important to notice that the $\iff$ of the equivalence version of consistency is now $\Rightarrow$: if $\{{\overrightarrow{P}}_1\}{p}_1\{{\overrightarrow{Q}}_1;{\overrightarrow{r}}_1\}$ is a solution, so is $\{{\overrightarrow{P}}_2\}{p}_2\{{\overrightarrow{Q}}_2;{\overrightarrow{r}}_2\}$, but since $\{{\overrightarrow{P}}_2\}{p}_2\{{\overrightarrow{Q}}_2;{\overrightarrow{r}}_2\}$ is more general ${\overrightarrow{P}}_2$ might describe $\overrightarrow{I}$ even if ${\overrightarrow{P}}_1$ did not.

The proof of Lemma 5 is found in the extended version of the paper.

With the program space $⦇𝒞⦈$ and the SObEq equivalence relation and generality ordering, we are ready to search for a program, i.e., to construct the OE-reduced space via enumeration.

Many synthesizers [16, 45, 36, 5] use a base OE enumeration of expressions to synthesize additional language constructs, e.g., conditionals, higher-order functions, and assignments. These techniques are parameterizable in their base enumerator, and so could leverage SObEq to expand their target language.

We show that Algorithm 1 is correct: that if a solution $p$ exists in the unreduced space, SObEq’s enumeration will find a solution observationally equivalent to $p$ or more general than $p$.

In the extended version of the paper we prove Theorem 6 in two steps: first we define the (unreduced) space reachable via enumeration and show that any solution will still be in that space, then we apply the reduction of ${\equiv }_{\overrightarrow{\mathrm{\Phi }}}$ to the space, defining the SObEq-reduced program space ${⦇𝒞⦈}^S$, and prove that any solution will have an observationally equivalent or more general under ${⊑}_{\overrightarrow{\mathrm{\Phi }}}$ solution in ${⦇𝒞⦈}^S$.

We considered several synthesizers as baselines for SObEq, ruling out synthesizers built for a single example [22], synthesizers that mutate by assigning synthesized pure expressions [16, 17, 59], and tools hinging on Java’s rich type system [15, 61]. FrAngel [52] is the current state of the art in synthesis of general programs with heap mutations: it is specified with input-output examples, it has the same ability as SObEq to declare a variable as immutable, and its stochastic search carries no additional requirements for specification other than the ability to evaluate – just as SObEq does. This makes it the most suitable baseline.

FrAngel targets Java collection implementations, which have many more methods than their JavaScript counterparts. This means FrAngel and SObEq can yield solutions that are entirely incomparable. To ensure an apples-to-apples comparison, we created new Java classes that mimic JavaScript types in Java, recreating the same $𝒞$ used by SObEq’s implementation. We then defined our benchmark set over these types.

In addition, in order to force FrAngel to create a straight-line sequence of expression statements as SObEq does, we also removed from its enumeration loops, conditionals, and assignments. Notice that removing choices from its random sampling only improves FrAngel’s odds of finding a solution; before this additional change, FrAngel’s run times were considerably worse.

FrAngel also has the option to set inputs as immutable, which let us encode immut variables, and an option to set a target value for an input, which we used for encoding effect constraints in the benchmark. This means FrAngel can run on every benchmark in SObEq’s suite.

We consider two timeouts for our runs. First, we set our timeout at 60 minutes, extending the original 30 minute timeout used to evaluate FrAngel. However, since we aim SObEq to be used in interactive systems, and by other OE-based systems as the base enumerator, we also consider results at an interactive timeout or a timeout needed for the synthesizer to run in a user-facing tool and not create a disruptive interruption [43]. Building on recent interactive synthesizers, we choose 7 seconds as our interactive timeout.

While the size of solutions is not, in itself, a good proxy for quality, it is telling in combination with overfitting and spurious operations. SObEq postprocessed solutions had an average of 6.2 AST nodes at an interactive timeout and 6.9 at a 1-hour timeout (max 14, 25, resp.) where Must benchmarks were generally smaller – 5.7 nodes at the interactive timeout and 6.1 in an hour – compared to May benchmarks – 6.4 and 7.1 nodes.

The left and center of Figure 5 show the AST size for each SObEq solution compared to each of FrAngel’s solutions for the same benchmark. Overall, FrAngel’s solutions are much larger than SObEq’s. There are two benchmarks where SObEq’s solution is considerably larger than FrAngel’s: Is All Positive? (originally from FrAngel), both SObEq’s and FrAngel’s solutions were overfitted. In Get first name from name with comma (originally from Probe [7]), FrAngel returned two overfitted solutions similar to SObEq’s, both appearing closer to the diagonal line, and three times found a solution closer to the gold standard solution, which is shorter, though never the gold standard solution itself. (The two identical solutions and three identical solutions overlap in Figure 5.) An interesting trend in SObEq’s solutions was that the enumeration order favored extracting postfix increment to a sequence. E.g., instead of buffer[idx++]++, idx SObEq returns the larger but functionally identical buffer[idx]++, idx++, idx.

We define overfitted solutions as solutions that do not generalize beyond the provided examples. This was determined by manual inspection of both SObEq and FrAngel solutions, and with reference to task descriptions and gold standard solutions, if they exist.

Two SObEq solutions were overfitted, and one additional benchmark was close to a gold standard solution for the task, but since all its inputs were of length 4, it replaced str.length in the gold standard solution with 4. Altogether, 3 of SObEq’s 54 solutions were overfitted (6%). Of 279 FrAngel solutions (up to five per benchmark, which sometimes differ) 47 were overfitted (17%). As the right of Figure 5 shows, both tools were more prone to overfitting in May benchmarks.

We bring several examples of FrAngel’s overfitted solutions here.

For example in the Max and Min benchmark, a simplified version of the example in Section 1, all four solutions (one run timed out) are overfitted and different. Two of them are:

where the result number (max plus min) is generated by indexOf, and

where it is generated by the length of a string.

We also consider FrAngel’s results on the three benchmarks that SObEq overfitted on: For the Is All Positive? benchmark mentioned above for its large solutions, both SObEq and FrAngel overfit to the examples in two different ways. FrAngel overfit all give solutions, returning true only for arrays where the smallest element is 1, and SObEq looked for a ’-’ in an overfitted location in the printed array. For get from name with comma, four of five FrAngel solutions were not overfit. The fifth is: