Planet Mozilla

Today, on behalf of the Rust Fuzzing Authority, I’d like to announce new releases of the arbitrary, libfuzzer-sys, and cargo fuzz crates. Collectively, these releases better support writing fuzz targets that take well-formed instances of custom input types. This enables us to combine powerful, coverage-guided fuzzers with smart test case generation.

Install or upgrade cargo fuzz with:

cargo install --force cargo-fuzz

To upgrade your fuzz targets, bump your libfuzzer-sys dependency to 0.2.0 on crates.io. That should be all that’s needed for most cases. However, if you were already using Arbitrary inputs for your fuzz target, some changes will be required. See the upgrading fuzz targets section below for more details.

Fuzzing with Well-Formed, Custom Inputs

Imagine we are testing an ELF object file parser. In this scenario, it makes sense to fuzz the parser by feeding it raw byte buffers as input. Parsers for binary formats take raw byte buffers as input; there’s no impedance mismatch here. Additionally, coverage-guided fuzzers like libFuzzer naturally generate byte buffers as inputs for fuzz targets, so getting fuzzing up and running is easy.

Now instead imagine we are testing a color conversion library: converting between RGB colors to HSL colors and back. Our color conversion functions don’t take raw byte buffers as inputs, they take Rgb or Hsl structures. And these structures are defined locally by our library; libFuzzer doesn’t have any knowledge of them and can’t generate instances of them on its own.

We could write a color string parser, parse colors from the fuzzer-provided, raw input bytes, and then pass the parsed results into our color conversion functions. But now the fuzzer is going to spend a bunch of time exploring and testing our color string parser, before it can get “deeper” into the fuzz target, where our color conversions are. Small changes to the input can result in invalid color strings, that bounce off the parser. Ultimately, our testing is less efficient than we want, because our real goal is to exercise the conversions but we’re doing all this other stuff. On top of that, there’s this hump we have to get over to start fuzzing, since we have to write a bunch of parsing code if we didn’t already have it.

This is where the Arbitrary trait comes in. Arbitrary lets us create structured inputs from raw byte buffers with as thin a veneer as possible. As best it can, it preserves the property that small changes to the input bytes lead to small changes in the corresponding Arbitrary instance constructed from those input bytes. This helps coverage-guided fuzzers like libFuzzer efficiently explore the input space. The new 0.3.0 release of arbitrary contains an overhaul of the trait’s design to further these goals.

Implementing Arbitrary for custom types is easy: 99% of the time, all we need to do is automatically derive it. So let’s do that for Rgb in our color conversion library:

use arbitrary::Arbitrary;

#[derive(Arbitrary, Debug, PartialEq, Eq)]
pub struct Rgb {
    r: u8,
    g: u8,
    b: u8,
}

The libfuzzer-sys crate lets us define fuzz targets where the input type is anything that implements Arbitrary:

// The fuzz target takes a well-formed `Rgb` as input!
libfuzzer_sys::fuzz_target!(|rgb: Rgb| {
    let hsl = rgb.to_hsl();
    let rgb2 = hsl.to_rgb();

    // RGB -> HSL -> RGB is the identity function. This
    // property should hold true for all RGB colors!
    assert_eq!(rgb, rgb2);
});

Now we have a fuzz target that works with our custom input type directly, is the thinnest abstraction possible over the raw, fuzzer-provided input bytes, and we didn’t need to write any custom parsing logic ourselves!

This isn’t limited to simple structures like Rgb. The arbitrary crate provides Arbitrary implementations for everything in std that you’d expect it to: bool, u32, f64, String, Vec, HashMap, PathBuf, etc… Additionally, the custom derive works with all kinds of structs and enums, as long as each sub-field implements Arbitrary.

For more details check out the new Structure-Aware Fuzzing section of The Rust Fuzzing Book and the arbitrary crate. The book has another neat example, where we’re testing a custom allocator implementation and the fuzz target takes a sequence of malloc, realloc, and free commands.

Bonus: Improved UX in cargo fuzz

When cargo fuzz finds a failing input, it will display the Debug formatting of the failing input (particularly nice with custom Arbitrary inputs) and suggest common next tasks, like reproducing the failure or running test case minimization.

For example, if we write a fuzz target that panics when r < g < b for a given Rgb instance, libFuzzer will very quickly find an input that triggers the failure, and then cargo fuzz will give us this friendly output:

Failing input:

    fuzz/artifacts/my_fuzz_target/crash-7bb2b62488fd8fc49937ebeed3016987d6e4a554

Output of `std::fmt::Debug`:

    Rgb {
        r: 30,
        g: 40,
        b: 110,
    }

Reproduce with:

    cargo fuzz run my_fuzz_target fuzz/artifacts/my_fuzz_target/crash-7bb2b62488fd8fc49937ebeed3016987d6e4a554

Minimize test case with:

    cargo fuzz tmin my_fuzz_target fuzz/artifacts/my_fuzz_target/crash-7bb2b62488fd8fc49937ebeed3016987d6e4a554

Upgrading Fuzz Targets

First, make sure you’ve upgraded cargo fuzz:

cargo install --force cargo-fuzz

Next, upgrade your libfuzzer-sys from a git dependency to the 0.2.0 version on crates.io in your Cargo.toml:

 [dependencies]
-libfuzzer-sys = { git = "https://github.com/rust-fuzz/libfuzzer-sys.git" }
+libfuzzer-sys = "0.2.0"

If your existing fuzz targets were not using custom Arbitrary inputs, and were taking &[u8] slices of raw bytes, then you’re done!

If you’re implementing Arbitrary for your own custom input types, you’ll need to bump your dependency on Arbitrary to version 0.3. We recommend that, unless you have any specialized logic in your Arbitrary implementation, that you use the custom derive.

Enable the custom derive by requiring the "derive" feature:

[dependencies]
arbitrary = { version = "0.3", features = ["derive"] }

And then derive Arbitrary automatically:

use arbitrary::Arbitrary;

#[derive(Arbitrary, Debug)]
struct MyStruct {
    // ...
}

Finally, if you do you specialized logic in your Arbitrary implementation, and can’t use the custom derive, your implementations will change something like this:

 use arbitrary::{Arbitrary, Unstructured};

 impl Arbitrary for MyType {
-    fn arbitrary<U>(u: &mut U) -> Result<Self, U::Error>
-    where
-        U: Unstructured + ?Sized,
-    {
+    fn arbitrary(
+        u: &mut Unstructured
+    ) -> arbitrary::Result<Self> {
         // ...
     }
 }

The trait has been simplified a little bit, and Unstructured is a concrete type now, rather than a trait you need to parameterize over. Check out the CHANGELOG for more details.

CHANGELOGs

• arbitrary @ 0.3.0
• libfuzzer-sys @ 0.2.0
• cargo fuzz @ 0.7.0

Thank You! 💖

Thanks to everyone who contributed to these releases!

• Alex Rebert
• koushiro
• Manish Goregaokar
• Nick Fitzgerald
• Simonas Kazlauskas

And a special shout out to Manish for fielding so many pull request reviews!

FAQ

What is fuzzing?

Fuzzing is a software testing technique used to find security, stability, and correctness issues by feeding pseudo-random data as input to the software.

Learn more about fuzzing Rust code in The Rust Fuzzing Book!

How is all this different from quickcheck and proptest?

If you’re familiar with quickcheck or proptest and their own versions of the Arbitrary trait, you might be wondering what the difference is between what’s presented here and those tools.

The primary goal of what’s been presented here is to have a super-thin, efficient layer on top of coverage-guided, mutation-based fuzzers like libFuzzer. That means the paradigm is a little different from quickcheck and proptest. For example, arbitrary::Arbitrary doesn’t take a random number generator like quickcheck::Arbitrary does. Instead it takes an Unstructured, which is a helpful wrapper around a raw byte buffer provided by the fuzzer. It’s similar to libFuzzer’s FuzzedDataProvider. The goal is to preserve, as much as possible, the actual input given to us by the fuzzer, and make sure that small changes in the raw input lead to small changes in the value constructed via arbitrary::Arbitrary. Similarly, we don’t want different, customizable test case generation strategies like proptest supports, because we leverage the fuzzer’s insight into code coverage to efficiently explore the input space. We don’t want to get in the way of that, and step on the fuzzer’s toes.

This isn’t to say that quickcheck and proptest are without value! On the contrary, if you are not using a coverage-guided fuzzer like libFuzzer or AFL — perhaps because you’re working on an unsupported platform — and are instead using a purely-random, generation-based fuzzing setup, then both quickcheck and proptest are fantastic options to consider.

Automatically finding a program that implements a given specification is called program synthesis. The main difficulty is that the search space is huge: the number of programs of size \(n\) grows exponentially. Naïvely enumerating every program of size \(n\), checking whether each one satisfies the specification, and then moving on to programs of size \(n+1\) and so on doesn’t scale. However, the field has advanced by using smarter search techniques to prune the search space, leveraging performance improvements in SMT solvers, and at times limiting the scope of the problem.

In this post, I’ll explain one approach to modern program synthesis: counterexample-guided iterative synthesis of component-based, loop-free programs, as described in Synthesis of Loop-Free Programs by Gulwani et al. We’ll dissect exactly what each of those terms mean, and we’ll also walk through an implementation written in Rust that uses the Z3 solver.

My hopes for this post are two-fold:

1. I hope that people who are unfamiliar with program synthesis — just like I was not too long ago — get a little less unfamiliar and learn something new about the topic. I’ve tried to provide many examples, and break down the dense logic formulas from the paper into smaller, approachable pieces.

2. I hope that folks who are already familiar with this kind of program synthesis can help me diagnose some performance issues in the implementation, where I haven’t been able to reproduce the synthesis results reported in the literature. For some of the more difficult benchmark problems, the synthesizer fails to even find a solution before my patience runs out.

Table of Contents

• Motivation
• An Overview of Our Task
• Formalizing the Problem
• A Brief Introduction to SMT Solvers
• Counterexample-Guided Iterative Synthesis
  • CEGIS with Components
    • Verifying a Component-Based Program
    • Finite Synthesis of a Component-Based Program
• Implementation
  • Program Representation
  • Building Programs
  • Defining Components
  • Specifications
  • The Synthesizer
  • Location Mappings
  • Verification
  • Finite Synthesis
  • The CEGIS Loop
• Results
• Conclusion
• References

Motivation

Why write a program that writes other programs for me? Am I just too lazy to write them myself? Of course I am. However, there are many valid reasons why a person who is not as lazy as I am might want to synthesize programs.

Some programs are quite tricky to write correctly by hand, and a program synthesizer might succeed where you or I might fail. Quick! How do you isolate the rightmost zero bit in a word using only three bit manipulation instructions?!

              ,--- The rightmost zero bit.
              |
              V
Input:  011010011

Output: 000000100
              ^
              |
              '--- Only that bit is set.

Did you get it yet?

…

Okay, here’s the answer:

isolate_rightmost_zero_bit(x): // x = 011010011
    a ← not x                  // a = 100101100
    b ← add 1, x               // b = 011010100
    c ← and a, b               // c = 000000100
    return c

Our program synthesizer will find a solution in under a second, and that minimal-length solution in a minute or so. It would take me quite a while longer than that to do the same by hand. We’ll return to this problem throughout the rest of this post, and use it as a running example.

Another reason to use a program synthesizer might be that we need to write many more programs than we have time to write by hand. Take for example a compiler’s peephole optimizer: it considers a sliding window of instruction sequences, and for each sequence, it checks if it knows of an equivalent-but-faster-or-smaller instruction sequence. When it does know of a better instruction sequence, it replaces the original instructions with the better ones.

Peephole optimizers are typically constructed from pattern-matching rules that identify suboptimal instruction sequences paired with the improved instruction sequence to replace matches with:

new PeepholeOptimizer(
    pattern0 → replacement0
    pattern1 → replacement1
    pattern2 → replacement2
    // ...
    patternn → replacementn
)

Each replacementi is a little, optimized mini-program. If we were writing a new peephole optimizer from scratch and by hand, we would have to write \(n\) optimized mini-programs ourselves. And \(n\) can be big: LLVM’s InstCombine peephole optimizer has over 1,000 pattern-and-replacement pairs. Even half that many is way more than I want to write myself.

Instead of writing those optimized mini-programs by hand, we can use each original instruction sequence as a specification, feed it into a program synthesizer, and see if the synthesizer can find the optimal instruction sequence that does the same thing. Finally, we can use all these original instruction sequences and their synthesized, optimal instruction sequences as pattern-and-replacement pairs to automatically construct a peephole optimizer! This idea was first proposed by Bansal et al in Automatic Generation of Peephole Superoptimizers.

Edit: John Regehr pointed out to me that this idea has been floating around since much earlier than 2006, when the Bansal et al paper was published. He pointed me to The Design and Application of a Retargetable Peephole Optimizer by Davidson et al from 1980 as an example, but noted that even this wasn’t the first time it came up.

An Overview of Our Task

Program synthesis is the act of taking a specification, and automatically finding a program that satisfies it. In order to make the problem a little more tractable, we’re limiting its scope in two ways:

1. Loop-free: We are only synthesizing programs without loops.

2. Component-based: We are only synthesizing programs that can be expressed as the composition of a given library of components.

The loop-free limitation is not very limiting for many use cases. For example, peephole optimizers often don’t consider instruction sequences that span across loop boundaries.

Component-based synthesis means that rather than synthesizing programs using any combination of any number of the target language’s expressions, the synthesizer is given a library of components and synthesizes programs that use each of those components exactly once. The synthesizer rearranges the components, rewiring their inputs and outputs, until it finds a configuration that satisfies the specification.

That is, given a library of \(N\) components, it constructs a program of the form

synthesized_program(inputs...):
    temp0 ← component0(params0...)
    temp1 ← component1(params1...)
    // ...
    tempN-1 ← componentN-1(paramsN-1...)
    return tempN-1

where each parameter in paramsi is either a tempj variable defined earlier in the program or one of the original inputs.

For example, given the two components

• f(a)
• g(a, b)

and an input parameter x, the synthesizer can construct any of the following candidate programs (implicitly returning the variable defined last):

a ← g(x, x)
b ← f(x)

or

a ← g(x, x)
b ← f(a)

or

a ← f(x)
b ← g(x, x)

or

a ← f(x)
b ← g(a, x)

or

a ← f(x)
b ← g(x, a)

or

a ← f(x)
b ← g(a, a)

That’s it. That’s all of the programs it can possibly construct given just those two components.

The synthesizer cannot construct the following program, because it doesn’t use every component:

a ← f(x)

And the synthesizer cannot construct this program, because it uses the f component more than once:

a ← f(x)
b ← f(a)
c ← g(b, b)

And, finally, it cannot construct this last program, because this last program uses some function h that is not a component in our given library:

a ← f(x)
b ← h(a, x)

The following table describes some of the properties of component-based synthesis by comparing it to the fully general version of program synthesis:

In our synthesizer, the components will be functions over fixed bit-width integers (also known as “bitvectors” in the SMT solver parlance) and they will correspond to a single instruction in our virtual instruction set: add, and, xor, etc. But in principle they could also be higher-level functions or anything else that we can encode in SMT queries. More on SMT queries later.

While component-based synthesis makes the synthesis problem easier, it does foist a decision on us each time we invoke the synthesizer: we must choose the library of available components. Each component is used exactly once in the synthesized program, but if we want to synthesize a program that performs multiple additions, we can include multiple instances of the add component in the library. Too few components, and the synthesizer might not be able to find a solution. Too many components will slow down the synthesizer, and let it generate non-optimal programs that potentially contain dead code.

To summarize, in component-based synthesis of loop-free programs, our synthesizer’s inputs are

• a specification, and

• a library of components.

Its output is a program that satisfies the specification, expressed in terms of the given components, or an error if can’t find such a program.

Formalizing the Problem

In order to synthesize a program, we need a specification describing the desired program’s behavior. The specification is a logical expression that describes the output when the program is given these inputs.

We define the specification with:

• \(\vec{I}\) as the program inputs,

• \(O\) as the program output, and

• \(\phi_\mathrm{spec}(\vec{I}, O)\) as the expression relating the inputs to the output. This expression should be true when \(O\) is the desired output of running the program on inputs \(\vec{I}\).

The library of components we’re given is a multi-set of specifications describing each component’s behavior. Each component specification comes with how many inputs it takes (e.g. an add(a, b) component takes two inputs, and a not(a) component takes one input) as well as a logical formula relating the component’s inputs to its output. The component inputs, output, and expression all have similar notation to the program specification, but with a subscript:

• \(\vec{I}_i\) is the \(i^\mathrm{th}\) component’s input variables,

• \(O_i\) is the \(i^\mathrm{th}\) component’s output variable, and

• \(\phi_i(\vec{I}_i, O_i)\) is the logical expression relating the \(i^\mathrm{th}\) component’s inputs with its output.

We define \(N\) as the number of components in the library.

For our isolating-the-rightmost-zero-bit example, what is the minimal components library we could give to the synthesizer, while still preserving its ability to find our desired solution? It would be a library consisting of exactly the components that correspond to each of the three instructions in the solution program: a not, an add1, and an and component.

Program synthesis can be expressed as an exists-forall problem: we want to find whether there exists some program \(P\) that satisfies the specification for all inputs given to it and outputs it returns.

\( \begin{align} & \exists P: \\ & \quad \forall \vec{I},O: \\ & \quad \quad P(\vec{I}) = O \implies \phi_\mathrm{spec}(\vec{I}, O) \end{align} \)

Let’s break that down and translate it into English:

This exists-forall formalization is important to understand because our eventual implementation will query the SMT solver (Z3 in our case) with pretty much this formula. It won’t be exactly the same:

• \(P\) is an abstraction that’s hiding some details about components,
• there are a few algebraic transformations we will perform, and
• we won’t pose the whole problem to the solver in a single query all at once.

Nonetheless, the implementation follows from this formalization, and we won’t get far if we don’t have a handle on this.

A Brief Introduction to SMT Solvers

We can’t continue any further without briefly discussing SMT solvers and their capabilities. SMT solvers like Z3 take a logical formula, potentially containing unbound variables, and return whether it is:

• Satisfiable: there is an assignment to the unbound variables that makes the assertions true, and also here is a model describing those assignments.

• Unsatisfiable: the formula’s assertions are false; there is no assignment of values to the unbound variables that can make them true.

SMT solvers take their assertions in a Lisp-like input language called SMT-LIB2. Here is an example of a satisfiable SMT query:

;; `x` is some integer, but we don't know which one.
(declare-const Int x)

;; We do know that `x + 2 = 5`, however.
(assert (= 5 (+ x 2)))

;; Check whether the assertions are satisfiable. In
;; this case, they should be!
(check-sat)

;; Get the model, which has assignments to each of
;; the free variables. The model should report that
;; `x` is `3`!
(get-model)

Open and run this snippet in an online Z3 editor!

Note that even though there isn’t any \(\exists\) existential quantifier in there, the solver is implicitly finding a solution for \(x\) in \(\exists x: x + 2 = 5\), i.e. there exists some \(x\) such that \(x + 2\) equals 5. While some SMT solvers have some support for working with higher-order formulas with explicit \(\exists\) existential and \(\forall\) universal quantifiers nested inside, these modes tend to be much slower and also incomplete. We can only rely on first-order, implicitly \(\exists\) existential queries: that is, formulas with potentially unbound variables and without any nested \(\exists\) existential and \(\forall\) universal quantification.

We can add a second assertion to our example that makes it unsatisfiable:

(declare-const x Int)

(assert (= 5 (+ x 2)))

;; NEW: also, x + 1 should be 10.
(assert (= 10 (+ x 1)))

;; This time, the result should be unsatisfiable,
;; because there are conflicting requirements for `x`.
(check-sat)
(get-model)

Open and run this snippet in an online Z3 editor!

The assertions 10 = x + 1 and 5 = x + 2 put conflicting requirements on x, and therefore there is no value for x that can make both assertions true, and therefore the whole query is unsatisfiable.

Counterexample-Guided Iterative Synthesis

Counterexample-guided iterative synthesis (CEGIS) enables us to solve second-order, exists-forall queries — like our program synthesis problem — with off-the-shelf SMT solvers. CEGIS does this by decomposing these difficult queries into multiple first-order, \(\exists\) existentially quantified queries. These are the kind of queries that off-the-shelf SMT solvers excel at solving. First, we’ll look at CEGIS in general, and after that we’ll examine what is required specifically for component-based CEGIS.

CEGIS begins by choosing an initial, finite set of inputs. There has to be at least one, but it doesn’t really matter where it came from; we can use a random number generator. Then we start looping. The first step of the loop is finite synthesis, which generates a program that is correct at least for the inputs in our finite set. It may or may not be correct for all inputs, but we don’t know that yet. Next, we take that candidate program and verify it: we want determine whether it is correct for all inputs (in which case we’re done), or if there is some input for which the candidate program is incorrect (called a counterexample). If there is a counterexample, we add it to our set, and continue to the next iteration of the loop. The next program that finite synthesis produces will be correct for all the old inputs, and also this new counterexample. The counterexamples force finite synthesis to come up with more and more general programs that are correct for more and more inputs, until finally it comes up with a fully general program that works for all inputs.

Without further ado, here is the general CEGIS algorithm:

\(\begin{align} & \texttt{CEGIS}(\phi_\mathrm{spec}(\vec{I}, O)): \\ & \qquad S = \langle \text{initial finite inputs} \rangle \\ & \qquad \\ & \qquad \textbf{loop}: \\ & \qquad \qquad \texttt{// Finite synthesis.} \\ & \qquad \qquad \textbf{solve for $P$ in } \exists P,O_0,\ldots,O_{\lvert S \rvert - 1}: \\ & \qquad \qquad \qquad \left( P(S_0) = O_0 \land \phi_\mathrm{spec}(S_0, O_0) \right) \\ & \qquad \qquad \qquad \land \ldots \\ & \qquad \qquad \qquad \land \left( P(S_{\lvert S \rvert - 1}) = O_{\lvert S \rvert - 1} \land \phi_\mathrm{spec}(S_{\lvert S \rvert - 1}, O_{\lvert S \rvert - 1}) \right) \\ & \qquad \qquad \textbf{if } \texttt{unsat}: \\ & \qquad \qquad \qquad \textbf{error} \text{ “no solution”} \\ & \qquad \qquad \\ & \qquad \qquad \texttt{// Verification.} \\ & \qquad \qquad \textbf{solve for $\vec{I}$ in } \exists \vec{I},O: \,\, P(\vec{I}) = O \land \lnot \phi_\mathrm{spec}(\vec{I}, O) \\ & \qquad \qquad \textbf{if } \texttt{unsat}: \\ & \qquad \qquad \qquad \textbf{return $P$} \\ & \qquad \qquad \textbf{else}: \\ & \qquad \qquad \qquad \textbf{append $\vec{I}$ to $S$} \\ & \qquad \qquad \qquad \textbf{continue} \end{align}\)

CEGIS decomposes the exists-forall synthesis problem into two parts:

1. Finite synthesis: The first query, the finite synthesis query, finds a program that is correct for at least the finite example inputs in \(S\). Here’s its breakdown:

   \( \exists P,O_0,\ldots,O_{\lvert S \rvert - 1}: \)	There exists some program \(P\) and outputs \(O_0,\ldots,O_{\lvert S \rvert - 1}\) such that
   \( ( \,\, P(S_0) = O_0 \)	\(O_0\) is the output of running the program on inputs \(S_0\)
   \( \land \)	and
   \( \phi_\mathrm{spec}(S_0, O_0) \,\, ) \)	the specification is satisfied for the inputs \(S_0\) and output \(O_0\),
   \( \land \ldots \)	and…
   \( \land \left( P(S_{\lvert S \rvert - 1}) = O_{\lvert S \rvert - 1} \land \phi_\mathrm{spec}(S_{\lvert S \rvert - 1}, O_{\lvert S \rvert - 1}) \right) \)	and \(O_{\lvert S \rvert - 1}\) is the output of running the program on inputs \(S_{\lvert S \rvert - 1}\), and the specification is satisfied for these inputs and output.

   Note that this is a first-order, existential query; it is not using nested \(\forall\) universal quantification over all possible inputs! Instead, it is instantiating a new copy of \(P(S_i) = O_i \land \phi_\mathrm{spec}(S_i, O_i)\) for each example in our finite set \(S\).

   For example, if \(S = \langle 3, 4, 7 \rangle\), then the finite synthesis query would be

   \(\begin{align} & \exists P,O_0,O_1,O_2: \\ & \qquad \left( P(3) = O_0 \land \phi_\mathrm{spec}(3, O_0) \right) \\ & \qquad \land \,\, \left( P(4) = O_1 \land \phi_\mathrm{spec}(4, O_1) \right) \\ & \qquad \land \,\, \left( P(7) = O_2 \land \phi_\mathrm{spec}(7, O_2) \right) \\ \end{align}\)

   This inline expansion works because the finite set of inputs \(S\) is much smaller in practice (typically in the tens, if even that many) than the size of the set of all possible inputs (e.g. there are \(2^{32}\) bitvectors 32 bits wide).

   If the query was unsatisfiable, then there is no program that can implement the specification for every one of the inputs in \(S\). Since \(S\) is a subset of all possible inputs, that means that there is no program that can implement the specification for all inputs. And since that is what we are searching for, it means that the search has failed, so we return an error.

   If the query was satisfiable, the resulting program \(P\) satisfies the specification for all the inputs in \(S\), but we don’t know whether it satisfies the specification for all possible inputs or not yet. For example, if \(S = \langle 0, 4 \rangle \), then we know that the program \(P\) is correct when given the inputs \(0\) and \(4\), but it may or may not be correct when given the input \(1\). We don’t know yet.

2. Verification: Verification takes the program \(P\) produced by finite synthesis and checks whether it satisfies the specification for all inputs. That’s naturally expressed as a \(\forall\) universally quantified query over all inputs, but we can instead ask if there exists any input to the program for which the specification is not satisfied thanks to De Morgan’s law.

   Here’s the breakdown of the verification query:

   \( \exists \vec{I}, O: \)	Does there exist some inputs \(\vec{I}\) and output \(O\) such that
   \( P(\vec{I}) = O\)	\(O\) is the result of running the program on \(\vec{I}\)
   \( \land \)	and
   \( \lnot \phi_\mathrm{spec}(\vec{I}, O) \)	the specification is not satisfied.

   If the verification query is unsatisfiable, then there are no inputs to \(P\) for which the specification is not satisfied, which means that \(P\) satisfies the specification for all inputs. If so, this is what we are searching for, and we’ve found it, so return it!

   However, if the verification query is satisfiable, then we’ve discovered a counterexample: a new input \(\vec{I}\) for which the program does not satisfy the specification. That is, the program \(P\) is buggy when given \(\vec{I}\), so \(P\) isn’t the program we are searching for.

   Next, we add the new \(\vec{I}\) to our finite set of inputs \(S\), so that in the next iteration of the loop, we will synthesize a program that produces a correct result when given \(\vec{I}\) in addition to all the other inputs in \(S\).

As the loop iterates, we add more and more inputs to \(S\), forcing the finite synthesis query to produce more and more general programs. Eventually it produces a fully general program that satisfies the specification for all inputs. In the worst case, we are adding every possible input into \(S\): finite synthesis comes up with a program that fails verification when given 1, and then when given 2, and then 3, and so on. In practice, each counterexample \(\vec{I}\) that verification finds tends to be representative of many other inputs that are also currently unhandled-by-\(P\). By adding \(\vec{I}\) to \(S\), the next iteration of finite synthesis will produce a program that handles not just \(\vec{I}\) but also all the other inputs that \(\vec{I}\) was representative of.

For example, finite synthesis might have produced a program that handles all of \(S = \langle 0,1,5,13 \rangle\) but which is buggy when given a positive, even number. Verification finds the counterexample \(I = 2\), which gets appended to \(S\), and now \(S = \langle 0,1,5,13,2 \rangle\). Then, the next iteration of the loop synthesizes a program that doesn’t just also work for 2, but works for all positive even numbers. This is what makes CEGIS effective in practice.

Finally, notice that both finite synthesis and verification are first-order, \(\exists\) existentially quantified queries that off-the-shelf SMT solvers like Z3 can solve.

CEGIS with Components

Now that we know how CEGIS works in the abstract, let’s dive into how we can use it to synthesize component-based programs.

For every loop-free program that is a composition of components, we can flip the program’s representation into a location mapping:

• Instead of listing the program line-by-line, defining what component is on each line, we can list components, defining what line the component ends up on.

• Instead of referencing the arguments to each component by variable name, we can reference either the line on which the argument is defined (if it comes from the result of an earlier component) or as the \(n^\mathrm{th}\) program input.

For example, consider our program to isolate the rightmost zero bit in a word:

isolate_rightmost_zero_bit(x):
    a ← not x
    b ← add 1, x
    c ← and a, b
    return c

We can exactly represent this program with the following location mapping:

{
    inputs: ["x"],

    components: {
        // Line 1: `b ← add 1, x`
        add1: {
            // The line in the program where this
            // component is placed.
            line: 1,

            // Each entry `a` represents where the
            // argument comes from.
            //
            // If `0 <= a < inputs.len()`, then the
            // argument is `inputs[a]`.
            //
            // Otherwise, when `inputs.len() <= a`,
            // then the argument comes from the value
            // defined by the component on line
            /// `a - inputs.len()`.
            arguments: [
                // `x`
                0,
            ],
        },

        // Line 2: `c ← and a, b`
        and: {
            line: 2,
            arguments: [
                // `a`
                1,
                // `b`
                2,
            ],
        },

        // Line 0: `a ← not x`
        not: {
            line: 0,
            arguments: [
                // `x`
                0,
            ],
        },
    },
}

With component-based CEGIS, we’ll be synthesizing this kind of location mapping. This lets us represent a whole component-based program with a handful of numbers for lines and argument indices. And numbers are something that we can represent directly in an SMT query.

Verifying a Component-Based Program

Let’s start with verying a component-based program before we look at their finite synthesis. Verification takes a location mapping, connects the components’ input and output variables together as described by the location mapping, and asks the SMT solver to find a counterexample.

For convenience, so we don’t have to keep repeating \(\vec{I}_0,\ldots,\vec{I}_{N-1}\) all the time, we define \(\textbf{P}\) as the set of all the parameter variables for each component in the library:

\( \textbf{P} = \, \vec{I}_0 \, \cup \, \ldots \, \cup \, \vec{I}_{N-1} \)

And similarly we define \(\textbf{R}\) as the set of all temporary result variables for each component in the library:

\( \textbf{R} = \{O_0, \, \ldots, \, O_{N-1}\} \)

With our running example of isolating the rightmost zero bit, our minimal library consists of

\( \begin{align} \phi_0(I_0, O_0) &= [O_0 = \texttt{bvadd}(1, I_0)] \\ \phi_1(I_1, I_2, O_1) &= [O_1 = \texttt{bvand}(I_1, I_2)] \\ \phi_2(I_3, O_2) &= [O_2 = \texttt{bvnot}(I_3)] \end{align} \)

and therefore its

\( \begin{align} N &= 3 \\ \textbf{P} &= \{ I_0, I_1, I_2, I_3, I_4 \} \\ \textbf{R} &= \{ O_0, O_1, O_2 \} \end{align} \)

We want to constrain the whole library to behave according to its individual component specifications. The output of each and component should indeed be the bitwise and of its inputs, and the output of each not component should indeed be the bitwise not of its input, etc… We define \(\phi_\mathrm{lib}\) as the combination of every component specification \(\phi_i\):

\( \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) = \phi_i(\vec{I}_0, O_0) \land \ldots \land \phi_i(\vec{I}_{N-1}, O_{N-1}) \)

So for our minimal example library, the \(\phi_\mathrm{lib}\) we get is:

\( \begin{align} \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) &= [ O_0 = \texttt{bvadd}(1, I_0) ] \\ &\land [ O_1 = \texttt{bvand}(I_1, I_2) ] \\ &\land [ O_2 = \texttt{bvnot}(I_3) ] \end{align} \)

That is, the library’s constraints are satisfied when all of

• \(O_0\) is the wrapping addition of \(I_0\) and 1,
• \(O_1\) is the bitwise and of \(I_1\) and \(I_2\), and
• \(O_2\) is the bitwise not of \(I_3\),

Because finite synthesis runs before verification, we already have access to the candidate program’s location mapping when we’re constructing our verification query. This location mapping tells us which actual arguments align with which formal parameters of a component. That means we know what the connections are from each component’s input variables to the program inputs and the temporary result variables for other components. We know the dataflow between components.

Let’s make this concrete with our isolating-the-rightmost-zero-bit example. Having produced this candidate program:

a ← not x
b ← add 1, x
c ← and a, b

With this library:

\( \begin{align} \phi_0(I_0, O_0) &= [O_0 = \texttt{bvadd}(1, I_0)] \\ \phi_1(I_1, I_2, O_1) &= [O_1 = \texttt{bvand}(I_1, I_2)] \\ \phi_2(I_3, O_2) &= [O_2 = \texttt{bvnot}(I_3)] \end{align} \)

We know that \(\texttt{a} = O_2\), since it is the result of the not component \(\phi_2(I_3, O_2)\). And since a is the first argument to and a, b, which uses component \(\phi_1(I_1, I_2, O_1)\), we know that \(\texttt{a} = I_1\). Therefore, we know that \(O_2 = I_1\).

We have these equalities from each component input variable \(I_i\) in \(\textbf{P}\) to either some other component’s output variable \(O_j\) in \(\textbf{R}\) or to one of the program inputs \(\vec{I}\). These equalities are given to us directly by the location mapping for the candidate program that we’re verifying.

Additionally, because our candidate program is implicitly returning the last temporary variable c, which is the result of the and component \(\phi_1(I_1, I_2, O_1)\), and because the \(O\) in \(\phi_\mathrm{spec}(\vec{I}, O)\) represents the result of the whole program, we know that \(O = O_1\).

If we put all these equalities together for our example program we get:

\( \left( I_0 = x \right) \land \left( I_1 = O_2 \right) \land \left( I_2 = O_1 \right) \land \left( I_3 = x \right) \land \left( O = O_1 \right)\)

This represents all the connections between our library’s various components and to the candidate program’s inputs and output. If you imagine connecting the components together like a circuit, this represents all the wires between each component.

We define these component-connecting equalities as \(\phi_\mathrm{conn}\), and its general definition is:

\( \begin{align} \phi_\mathrm{conn}(\vec{I}, O, \textbf{P}, \textbf{R}) &= \left( O = O_\mathrm{last} \right) \\ & \land \left( \vec{I}_0 \, = \, \vec{V}_0 \right) \\ & \land \, \ldots \\ & \land \left( \vec{I}_{N-1} \, = \, \vec{V}_{N-1} \right) \end{align} \)

Where

• \(\vec{V}_i\) are the actual arguments that the candidate program passes into the \(i^\mathrm{th}\) component \(\phi_i\). Each \(\vec{V}_i\) is made up of entries from either the program’s inputs \(\vec{I}\) or from temporary results from \(\textbf{R}\) that are defined by earlier components in the program. This is equivalent to the arguments field defined for each component in our example location mapping’s components map.

• \(O_\mathrm{last}\) is the output variable for the component on the last line of the program, according to our candidate program’s location mapping.

Once again, let’s break that down:

Note that both \(O_\mathrm{last}\) and each \(\vec{V}_i\) are properties of the candidate program’s location mapping, and are known at “compile time” of the verification query. They are not variables that we are \(\exists\) existentially or \(\forall\) universally quantifying over in the query itself. We expand them inline when constructing the verification query.

Ok, so with all of that out of the way, we can finally define the verification constraint that we use in component-based CEGIS:

\( \begin{align} & \exists \vec{I}, O, \textbf{P} , \textbf{R} : \\ & \qquad \phi_\mathrm{conn}(\vec{I}, O, \textbf{P}, \textbf{R}) \land \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) \land \lnot \phi_\mathrm{spec}(\vec{I}, O) \end{align} \)

The verification constraint asks: given that we’ve connected the components together as described by the candidate program’s location mapping, are there any inputs for which the specification is not satisfied?

Let’s break that down once more:

Finding a solution to this query gives us a new counterexample \(\vec{I}\) that we can add to our set of examples \(S\) for future iterations of the CEGIS loop. Failure to find any solution to this query means that the candidate location mapping corresponds to a program that is correct for all inputs, in which case we’re done.

Finite Synthesis of a Component-Based Program

Finite synthesis composes the library components into a program that will correctly handle all the given example inputs. It does this by querying the SMT solver for a location mapping that contains assignments of components to lines in the program, and assignments of variables to each component’s actual arguments.

Recall our example location mapping:

{
    inputs: ["x"],

    components: {
        // Line 1: `b ← add 1, x`
        add1: {
            line: 1,
            arguments: [0], // `[x]`
        },

        // Line 2: `c ← and a, b`
        and: {
            line: 2,
            arguments: [1, 2], // `[a, b]`
        },

        // Line 0: `a ← not x`
        not: {
            line: 0,
            arguments: [0], // `[x]`
        },
    },
}

To encode a location mapping in the finite synthesis query, every component parameter in \(\textbf{P}\) and every component result in \(\textbf{R}\) gets an associated location variable. The finite synthesis query is searching for an assignment to these location variables.

We call the set of all location variables \(L\), and we refer to a particular location variable as \(l_x\) where \(x\) is either a component result in \(\textbf{R}\) or component parameter in \(\textbf{P}\):

\( L = \{ \, l_x \, \vert \, x \in \textbf{P} \cup \textbf{R} \, \} \)

The location variable for a result \(l_{O_i}\) is equivalent to the line field for a component in our JSON-y syntax for example location mappings. It determines the line in the program that the component is assigned to, and therefore where its temporary result is defined.

The location variable for a parameter \(l_p\) is equivalent to an entry in a component’s arguments list in our JSON-y syntax. These location variables determine where the associated parameter gets its value from: either the \(i^\mathrm{th}\) program input or the temporary result defined on the \(j^\mathrm{th}\) line of the program.

To use one index space for both line numbers and program inputs, we follow the same convention that we did with entries in the arguments list in the JSON syntax:

• When \(l_x\) is less than the number of program inputs, then it refers to the \({l_x}^\mathrm{th}\) program input.

• Otherwise, when \(l_x\) is greater than or equal to the number of program inputs, then subtract the number of inputs from \(l_x\) to get the line number it’s referring to.

All loop-free, component-based programs can be described with a location mapping. However, the reverse is not true: not all location mappings describe a valid program.

Consider this location mapping:

{
    inputs: ["x"],

    components: {
        // Line 0: `a ← add 1, x`
        add1: {
            line: 0,
            arguments: [0], // `[x]`
        },

        // Line 0: `a ← sub x, 1`
        sub1: {
            line: 0,
            arguments: [0], // `[x]`
        }
    }
}

This line mapping is inconsistent because it wants to put both its components on line zero of the program, but each line in the program can only use a single component.

To forbid the solver from providing bogus answers of this sort, we add the consistency constraint \(\psi_\mathrm{cons}\) to the finite synthesis query. It requires that no pair of distinct component result location variables can be assigned the same line.

\( \psi_\mathrm{cons}(L) = \bigwedge\limits_{x,y \in \textbf{R}, x \not\equiv y} \left( l_x \neq l_y \right) \)

Once more, let’s break that down:

But there are even more ways that a location mapping might describe an invalid program! Consider this location mapping:

{
    inputs: ["x"],

    components: {
        // Line 0: `a ← and x, b`
        and: {
            line: 0,
            arguments: [0, 2], // `[x, b]`
        },

        // Line 1: `b ← sub a, 1`
        sub1: {
            line: 1,
            arguments: [1], // `[a]`
        }
    }
}

That location mapping describes this program:

f(x):
    a ← and x, b
    b ← sub a, 1

The b temporary result is used before it is defined, and in order to compute b, we need to compute a, but computing a requires computing b, which requires computing a, etc… We have a cycle on our hands.

To forbid mappings that correspond to bogus programs with dataflow cycles, we use the acyclicity constraint \(\psi_\mathrm{acyc}\). This constraint enforces that a particular component’s parameters are defined before this component’s line.

\( \psi_\mathrm{acyc}(L) = \bigwedge\limits_{i=0}^{N-1} \left( \bigwedge\limits_{p \in \vec{I}_i} \left( l_p < l_{O_i} \right) \right) \)

Let’s break that down:

The only other way that location mappings can be invalid is if a location is out of bounds of the program inputs and line numbers, so we’re ready to define the well-formed-program constraint \(\psi_\mathrm{wfp}\). This constraint enforces that any location mapping we synthesize will correspond to a well-formed program.

A well-formed program is

• consistent,

• acyclic,

• its component parameter locations point to either a program input or a line number, and

• its component temporary result locations point to a line number.

Let’s define \(M\) as the number of program inputs plus the number of components in the library:

\( M = \lvert \vec{I} \rvert + N \)

A component parameter location \(l_{p \in \textbf{P}}\) can point to either

• a program input in the range from zero to the number of program inputs: \(0 \leq l_{p} \lt \lvert \vec{I} \rvert\), or

• a line number, which corresponds to the \(N\) locations following the program inputs: \(\lvert \vec{I} \rvert \leq l_p \lt M \).

Since those two ranges are contiguous, it means that component parameter locations ultimately fall within the range \(0 \leq l_p \lt M\).

A component temporary result location \(l_{r \in \textbf{R}}\) must point to a line number, which means that they fall within the range \(\lvert \vec{I} \rvert \leq l_r \lt M\).

Put all that together and we get the well-formed-program constraint \(\psi_\mathrm{wfp}\):

\( \begin{align} \psi_\mathrm{wfp}(L) &= \bigwedge\limits_{p \in \textbf{P}} \left( 0 \leq l_p \lt M \right) \\ & \land \, \bigwedge\limits_{r \in \textbf{R}} \left( \lvert \vec{I} \rvert \leq l_r \lt M \right) \\ & \land \, \psi_\mathrm{cons}(L) \\ & \land \, \psi_\mathrm{acyc}(L) \end{align} \)

And here is its breakdown:

Now that we can constrain finite synthesis to only produce location mappings that correspond to well-formed programs, all we need to do is encode the connections between components and the behavior of the library. This should sound familiar: we need the finite synthesis equivalent of \(\phi_\mathrm{conn}\) and \(\phi_\mathrm{lib}\) from verification. And it turns out that \(\phi_\mathrm{lib}\) doesn’t need to be tweaked at all, because the behavior of the library remains the same whether we are in verification or finite synthesis. But while \(\phi_\mathrm{conn}\) was checking a set of already-known connections between components, in finite synthesis we are searching for those connections, so we need a different query.

These connections define the dataflow between components. They are the wires in the circuit built from our components. A connection from some component result into another component’s input means that we need to constrain the result and input variables to be equal in the finite synthesis query. For example, if component \(\phi_i\) get’s placed on line 3, and parameter \(p\) is assigned the location 3, then \(p\) must take on the same value as the output \(O_i\) of that component.

This leads us to our definition of \(\psi_\mathrm{conn}\): for every pair of location variables \(l_x\) and \(l_y\), if they refer to the same location, then \(x\) and \(y\) must have the same value.

\( \psi_\mathrm{conn}(L, \vec{I}, O, \textbf{P}, \textbf{R}) = \bigwedge\limits_{x,y \in \vec{I} \cup \textbf{P} \cup \textbf{R} \cup { O } } \left( \left( l_x = l_y \right) \implies \left( x = y \right) \right) \)

Here is its piece-by-piece breakdown:

We’re finally ready to define our finite synthesis query for a location mapping. This query asks the solver to find some location mapping that corresponds to a well-formed program that satisfies our specification for each example input in \(S\). In other words, it must enforce that

• the location mapping corresponds to a well-formed program, and

• when the components are connected as described by the location mapping, and when the components behave as described by our library,

• then the specification is satisfied for each of our example inputs in \(S\).

Here it is, finally, our finite synthesis query:

\( \begin{align} & \exists L, O_0, \ldots, O_{\vert S \rvert - 1}, \textbf{P}_0, \ldots, \textbf{P}_{\vert S \rvert - 1}, \textbf{R}_0, \ldots, \textbf{R}_{\vert S \rvert - 1}: \\ & \qquad \psi_\mathrm{wfp}(L) \,\, \land \\ & \qquad \qquad \bigwedge\limits_{i=0}^{\lvert S \rvert - 1} \left( \phi_\mathrm{lib}(\textbf{P}_i, \textbf{R}_i) \land \psi_\mathrm{conn}(L, S_i, O_i, \textbf{P}_i, \textbf{R}_i) \land \phi_\mathrm{spec}(S_i, O_i) \right) \\ \end{align} \)

That’s quite a mouthful, so, one last time, let’s pull it apart and break it down:

When the solver finds a satisfiable assignment for this query, we get a new candidate location mapping that corresponds to a program that is correct for each of the example inputs in \(S\). When the solver finds the query unsatisifiable, that means there is no locaiton mapping that corresponds to a program that is correct for each of the example inputs, which means that our search has failed.

Implementation

I implemented a loop-free, component-based program synthesizer in Rust that uses Z3 to solve the finite synthesis and verification queries. The implementation’s repository is over here.

Our target language has all the operations you would expect for working with fixed-width integers. It has arithmetic operations like add and mul. It has bitwise operations like and and xor. It has comparison operations like eq, that evaluate to one if the comparison is true and zero otherwise. Finally, it has a select operation that takes three operands: a condition, a consequent, and an alternative. When the condition is non-zero, it evaluates to the consequent, and otherwise it evaluates to the alternative.

Values are neither signed nor unsigned. For operations like division that behave differently on signed and unsigned integers, we have a different instruction for each behavior: div_s for signed division and div_u for unsigned division.

Program Representation

A program is a sequence of instructions:

pub struct Program {
    instructions: Vec<Instruction>,
}

An instruction has an operation and binds its result to an identifier:

pub struct Instruction {
    result: Id,
    operator: Operator,
}

An identifier is an opaque wrapper around a number:

pub struct Id(u32);

We won’t support any nice names for identifiers, since essentially everything is a temporary. When we stringify programs, we’ll turn the identifiers into a, b, c, etc…

Additionally, we will uphold the invariant that Id(i) always refers to the value defined by the i^th instruction in the program.

Finally, the Operator enumeration has a variant for each operation in the language, along with the identifiers of its operands:

pub enum Operator {
    Var,                // New input variable.

    Const(u64),         // A constant value.

    Eqz(Id),            // Equals zero?
    Clz(Id),            // Count leading zeros.
    Ctz(Id),            // Count trailing zeros.
    Popcnt(Id),         // Population count.

    Eq(Id, Id),         // Equal?
    Ne(Id, Id),         // Not equal?
    LtS(Id, Id),        // Signed less than?
    LtU(Id, Id),        // Unsigned less than?
    GtS(Id, Id),        // Signed greater than?
    GtU(Id, Id),        // Unsigned greater than?
    LeS(Id, Id),        // Signed less than or equal?
    LeU(Id, Id),        // Unsigned less than or equal?
    GeS(Id, Id),        // Signed greater than or equal?
    GeU(Id, Id),        // Unsigned greater than or equal?

    Add(Id, Id),        // Addition.
    Sub(Id, Id),        // Subtraction.
    Mul(Id, Id),        // Multiplication.
    DivS(Id, Id),       // Signed division.
    DivU(Id, Id),       // Unsigned division.
    RemS(Id, Id),       // Signed remainder.
    RemU(Id, Id),       // Unsigned remainder.

    And(Id, Id),        // And.
    Or(Id, Id),         // Or.
    Xor(Id, Id),        // Exclusive or.
    Shl(Id, Id),        // Shift left.
    ShrS(Id, Id),       // Signed shift right.
    ShrU(Id, Id),       // Unsigned shift right.
    Rotl(Id, Id),       // Rotate left.
    Rotr(Id, Id),       // Rotate right.

    Select(Id, Id, Id), // If then else.
}

Building Programs

To make constructing programs by hand easier, we have a builder for programs. It wraps an inner Program and exposes a method for each operation, to append an instruction using that operation to the program thats being built.

pub struct ProgramBuilder {
    program: Program,
}

impl ProgramBuilder {
    /// Start building a new program!
    pub fn new() -> ProgramBuilder {
        ProgramBuilder {
            program: Program {
                instructions: vec![],
            },
        }
    }

    /// Finish building this program!
    pub fn finish(self) -> Program {
        self.program
    }

    fn next_id(&self) -> Id {
        Id(self.program.instructions.len() as u32)
    }

    // ...

    /// Append an `add a, b` instruction!
    pub fn add(&mut self, a: Id, b: Id) -> Id {
        let result = self.next_id();
        self.program.instructions.push(Instruction {
            result,
            operator: Operator::Add(a, b),
        });
        result
    }

    // ...
}

Here is our isolate-the-righmost-zero-bit example program constructed via the ProgramBuilder:

// isolate_rightmost_zero_bit(x):
//     a ← not x
//     b ← add 1, x
//     c ← and a, b
//     return c

let builder = ProgramBuilder::new();

let x = builder.var();
let a = builder.not(x);
let one = builder.const_(1);
let b = builder.add(one, x);
let c = builder.and(a, b);

let isolate_rightmost_zero_bit = builder.finish();

Having the builder is nice since we intend to write unoptimized programs ourselves, that we then use as specifications for synthesizing optimized programs.

Defining Components

Every operator has an associated component, so that we can synthesize programs that use that operator. Because a library can have a heterogeneous set of components, we’ll define an object-safe Component trait, so we can box them up as trait objects with dynamically dispatched methods, and store them all in the same collection.

A Component has two roles:

1. It must provide the constraints between its inputs and its output for the solver. This is its \(\phi_i(\vec{I}_i, O_i)\) that will be part of the whole library’s \(\phi_\mathrm{lib}(\textbf{P}, \textbf{R})\).

2. After we’ve synthesized some location mapping for a program that uses this component, in order to construct the corresponding Program, the component needs to know how to create the Operator it represents.

The make_expression trait method will handle the first role, and the make_operator trait method will handle the second. make_expression takes Z3 BitVec variables as its operands (the \(\vec{I}_i\) input variables) and returns a new Z3 BitVec expression that represents the result of running the operation on the operands (the \(O_i\) output variable). make_operator takes the Ids of its operands (as described by a synthesized location mapping) and returns its associated Operator with those Ids as its operands.

Note that, because different components have different arities, these methods don’t take their operands as multiple, individual parameters like a: BitVec, b: BitVec or a: Id, b: Id. Instead, components report their arity with the operand_arity trait method and callers pass in a slice of that many operands.

Finally, we also support synthesizing constant values for the const operator. These immediates are handled separately from operands, and so we also have the immediate_arity trait method, and make_expression and make_operator also takes slices of immediates.

pub trait Component {
    /// How many operands does this component take?
    fn operand_arity(&self) -> usize;

    /// How many immediates does this component need
    /// synthesized?
    fn immediate_arity(&self) -> usize;

    /// Construct this component's constraint as a Z3
    /// expression.
    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        immediates: &[BitVec<'a>],
        operands: &[BitVec<'a>],
        bit_width: u32,
    ) -> BitVec<'a>;

    /// Construct an `Operator` from the given
    /// immediates and operands.
    fn make_operator(
        &self,
        immediates: &[u64],
        operands: &[Id]
    ) -> Operator;
}

Let’s take a look at the implementation of a simple, representative component: the add component.

• It has two operands and zero immediates.

• The make_operator implementation is mechanical, pulling out its individual operands from the given slice, just to push them into the Operator::Add.

• The make_expression implementation is similarly concise, but is not quite mechanical. This is where we encode the add operator’s semantics into a Z3 expression. SMT-LIB2 defines a bvadd operatoin for wrapping addition on bitvectors, and the z3 crate we’re using exposes it to us as a method on BitVec. Wrapping addition is exactly what we want for our add instruction, and so all we have to do to encode our add operation’s semantics is bvadd our two operands.

• Because we are always working with components as trait objects, we also define a helper function for boxing up the Add component and turning it into a trait object with dynamically dispatched methods.

struct Add;

impl Component for Add {
    fn operand_arity(&self) -> usize {
        2
    }

    fn immediate_arity(&self) -> usize {
        0
    }

    fn make_operator(
        &self,
        immediates: &[u64],
        operands: &[Id],
    ) -> Operator {
        Operator::Add(operands[0], operands[1])
    }

    fn make_expression<'a>(
        &self,
        _context: &'a z3::Context,
        immediates: &[BitVec<'a>],
        operands: &[BitVec<'a>],
        _bit_width: u32,
    ) -> BitVec<'a> {
        operands[0].bvadd(&operands[1])
    }
}

pub fn add() -> Box<dyn Component> {
    Box::new(Add) as _
}

Most components look pretty much like that: there is some direct encoding into a single SMT expression for the operation.

Other components, like eqz, don’t have a direct encoding as a single SMT expression, and we need to compose multiple.

impl Component for Eqz {
    // ...

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        _immediates: &[BitVec<'a>],
        operands: &[BitVec<'a>],
        bit_width: u32,
    ) -> BitVec<'a> {
        let zero = BitVec::from_i64(
            context,
            0,
            bit_width,
        );
        let one = BitVec::from_i64(
            context,
            1,
            bit_width,
        );
        // `ite` is "if-then-else". If the operand
        // is zero, evaluate to one, otherwise
        // evaluate to zero.
        zero._eq(&operands[0]).ite(&one, &zero)
    }
}

The const component is the only component that uses immediates. It doesn’t have operands. Either its constant value is unbound, in which case we’re synthesizing the value, or we provide a value for it upon constructing the component:

struct Const(Option<u64>);

impl Component for Const {
    fn operand_arity(&self) -> usize {
        0
    }

    fn immediate_arity(&self) -> usize {
        if self.0.is_some() {
            0
        } else {
            1
        }
    }

    fn make_operator(
        &self,
        immediates: &[u64],
        _operands: &[Id]
    ) -> Operator {
        if let Some(val) = self.0 {
            Operator::Const(val)
        } else {
            Operator::Const(immediates[0])
        }
    }

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        immediates: &[BitVec<'a>],
        _operands: &[BitVec<'a>],
        bit_width: u32,
    ) -> BitVec<'a> {
        if let Some(val) = self.0 {
            BitVec::from_i64(
                context,
                val as i64,
                bit_width,
            )
        } else {
            immediates[0].clone()
        }
    }
}

pub fn const_(val: Option<u64>) -> Box<dyn Component> {
    Box::new(Const(val)) as _
}

Finally, a library is just a vector of components:

pub struct Library {
    pub components: Vec<Box<dyn Component>>,
}

Specifications

A specification looks quite similar to a component, but we only need to create its SMT constraints. We don’t need to construct Operators from it, so it doesn’t have an equivalent of the Component::make_operator method.

pub trait Specification {
    fn arity(&self) -> usize;

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        inputs: &[BitVec<'a>],
        output: &BitVec<'a>,
        bit_width: u32,
    ) -> Bool<'a>;
}

We want to use existing, unoptimized programs as specifications for new, optimized programs, and so we implement Specification for Program.

The arity of a program specification is how many input variables the program defines with the var operator:

impl Specification for Program {
    fn arity(&self) -> usize {
        self.instructions
            .iter()
            .take_while(|inst| {
                inst.operator == Operator::Var
            })
            .count()
    }

    // ...
}

To create a Z3 expression for a whole program, we build up subexpressions instruction by instruction in a table. This table serves as our lexical environment. By inspecting an operation’s operand Ids, we pluck the corresponding subexpressions out of this table to pass as operands into the instruction’s Component::make_expression implementation. The final entry in the table is the expression for the whole program, since the program implicitly returns its last value.

impl Specification for Program {
    // ...

    fn make_expression<'a>(
        &self,
        context: &'a z3::Context,
        inputs: &[BitVec<'a>],
        output: &BitVec<'a>,
        bit_width: u32,
    ) -> Bool<'a> {
        // `exprs[i]` is the Z3 subexpression for the
        // value defined on the `i`th instruction of
        // this program.
        let mut exprs: Vec<_> = inputs
            .iter()
            .cloned()
            .collect();

        let mut operands = vec![];

        for instr in self
            .instructions
            .iter()
            .skip(inputs.len())
        {
            // All `const`s in the program already have
            // a bound value, so no instruction will
            // require new immediates.
            let immediates = [];

            // Gather the subexpressions for each
            // operand that this operator is using.
            operands.clear();
            instr
                .operator
                .operands(|Id(i)| {
                    let v = exprs[i as usize].clone();
                    operands.push(v);
                });

            // Create the Z3 expression for this
            // instruction and push it onto `exprs`.
            exprs.push(
                instr
                    .operator
                    .make_expression(
                        context,
                        &immediates,
                        &operands,
                        bit_width,
                    )
            );
        }

        // The last instruction defines our return
        // value, and it should be equal to the
        // `output` variable.
        exprs.last().unwrap()._eq(output)
    }
}

The Synthesizer

The Synthesizer structure solves one synthesis problem for us. It takes a library and spec upon construction, and then we can configure how it will run with a few builder-style methods, and then finally we call its synthesize method to actually kick off the CEGIS loop.

/// A program synthesizer for creating a component-
/// based, loop-free program.
pub struct Synthesizer<'a> {
    // ...
}

impl<'a> Synthesizer<'a> {
    /// Create a new synthesizer with the given
    /// library and specification.
    ///
    /// After creation, we have the opportunity
    /// to configure the synthesis process with
    /// the various builder-style methods.
    pub fn new(
        context: &'a z3::Context,
        library: &'a Library,
        spec: &'a dyn Specification,
    ) -> Result<Self> {
        // ...
    }

    /// Configure whether we should require synthesis
    /// to find the minimal-length program that
    /// satisfies the specification.
    ///
    /// This produces the optimally smallest possible
    /// program, but it tends to take more time.
    pub fn should_synthesize_minimal_programs(
        &mut self,
        should: bool,
    ) -> &mut Self {
        // ...
    }

    /// Configure the timeout.
    ///
    /// No timeout means that we will keep going forever
    /// if necessary. Providing a number of milliseconds
    /// means we will have a soft maximum runtime of of
    /// that many milliseconds before giving up.
    pub fn set_timeout(
        &mut self,
        milliseconds: Option<u32>,
    ) -> &mut Self {
        // ...
    }

    /// Run this configured synthesizer to find a
    /// program that satisfies the specification!
    pub fn synthesize(
        &mut self,
    ) -> Result<Program> {
        // ...
    }
}

This allows us to create, configure, and run a synthesis problem like this:

let program = Synthesizer::new(&context, &library, &spec)
    .should_synthesize_minimal_programs(true)
    .set_timeout(Some(60 * 60 * 1000))
    .synthesize()?;

Location Mappings

A location mapping uses a bunch of line indices to represent a component-based program. Lines are something we can represent directly in SMT expressions, and so location mappings are how we will encode programs for synthesis.

We have the choice of either encoding a line as a mathematical integer, or as a bitvector. I originally used mathematical integers, and perhaps unsurprisingly, it is way slower than using a bitvector. By using a bitvector representation, we can use the minimal number of bits required for our library of components. For example, if there is one program input and seven components in the library, the largest zero-based line number we will ever need is seven, which means we only need bitvectors that are three bits wide to represent every line. The narrower the bitvector, the faster Z3 can work with it. I haven’t seen line representation mentioned in any of the papers I’ve read, but I’m sure it is tribal knowledge that “everyone knows.”

// The index of a line that a component is located
// at, or gets a parameter from.
type Line<'a> = BitVec<'a>;

Location mappings are used differently at different phases of CEGIS. Before we synthesize a program, they are a collection of unbound variables in an SMT query that we’re constructing. After synthesis, those variables get bound to concrete values and we only want to work with the values from then on; we don’t need the variables anymore. Therefore, we split the location mapping into two distinct representations:

1. Before and during finite synthesis we have LocationVars, which is a collection of line variables.

2. After finite synthesis, we pull the values assigned to those variables out into an Assignments structure that is a collection of index values.

A LocationVars has line variables for the program inputs \(\vec{I}\), for all the components’ parameters \(\textbf{P}\), for all the components’ temporary results \(\textbf{R}\), and for the whole program’s output \(O\). It also keeps track of how wide our line location bitvectors are.

struct LocationVars<'a> {
    // Variables for lines assigned to program inputs.
    // These are always assigned `0..inputs.len()`.
    inputs: Vec<Line<'a>>,

    // `params[i]` is the variable for the line that
    // defines the `i`th component parameter.
    params: Vec<Line<'a>>,

    // `results[i]` is the variable for the line on
    // which the `i`th component is placed in the
    // synthesized program, and therefore where the
    // `i`th component's temporary result is defined.
    results: Vec<Line<'a>>,

    // The variable for the line on which the program's
    // output is defined.
    output: Line<'a>,

    // The minimum bit width necessary to represent
    // any line location.
    line_bit_width: u32,
}

Unlike the original paper, we do not always take the program output from the last line in the synthesized location mapping. Instead, we allow setting the output line earlier in the program, essentially inserting early returns. This lets us (optionally) synthesize programs with optimal code size: we can find the earliest output line for which we can still synthesize a correct program. This little trick is taken from Souper.

The Assignments are all those same things, but instead of the variable for the line, we have the value of the line that we pulled out of the model the SMT solver gave us. It also has any synthesized immediate values.

struct Assignments {
    // Synthesized immediate values.
    immediates: Vec<u64>,

    // `params[i]` is the line in the program where the
    // `i`th parameter is defined.
    params: Vec<u32>,

    // `results[i]` is the line in the program where the
    // `i`th component is located, and therefore the
    // `i`th temporary result is defined.
    results: Vec<u32>,

    // The line where the program's final output is
    // defined.
    output: u32,
}

Verification

Verification takes an Assignment produced by finite synthesis, and attempts find a counterexample. If it finds one, then we need to continue the CEGIS loop. If it can’t find a counterexample, then we’ve found a solution and we’re done.

In the original paper, they represent the candidate program in the verification query with \(\phi_\mathrm{lib}\) and \(\phi_\mathrm{conn}\), essentially asking the solver to interpret the connections between components. This is what I originally did as well, but then I had a realization:

• We already need to have the ability to turn an Assignments into a Program for when we find a solution.

• We can already turn a Program into an SMT expression, since we use unoptimized programs as specifications for finding optimized ones.

That means we can convert our Assignments into a Program and then into an SMT expression. Why not verify that this SMT expression implies the specification directly? This means that

• we don’t need to construct \(\phi_\mathrm{lib}\) and \(\phi_\mathrm{conn}\) during verification,

• the solver doesn’t need to unify all the connections between components’ inputs and outputs in \(\phi_\mathrm{conn}\) to solve the verification query, and

• this should generally create smaller queries, which should generally be faster to solve than larger queries.

This did end up saving a little bit of code in the implementation, but does not seem to have yielded a speed up for overall synthesis time. Probably because nearly all time is spent in finite synthesis, and not verification.

Anyways, here is the verification implementation:

impl<'a> Synthesizer<'a> {
    fn verification(
        &mut self,
        assignments: &Assignments,
        bit_width: u32,
    ) -> Result<Verification> {
        // Create fresh input and output variables.
        let inputs: Vec<_> = (0..self.spec.arity())
            .map(|_| {
                fresh_input(self.context, bit_width)
            })
            .collect();
        let output = fresh_output(
            self.context,
            bit_width,
        );

        // Convert the assignments into a program, and
        // then convert that into an SMT expression.
        let mut prog = assignments
            .to_program(self.spec.arity(), self.library)
            .make_expression(
                self.context,
                &inputs,
                &output,
                bit_width,
            );

        let spec = self
            .spec
            .make_expression(
                self.context,
                &inputs,
                &output,
                bit_width,
            );

        // Are there any inputs to our program for
        // which the specification is not upheld?
        let not_spec = spec.not();
        let query = prog.and(&[&not_spec]);
        let solver = self.solver();
        solver.assert(&query);

        match solver.check() {
            // We don't know whether there is a
            // counterexample or not. This typically
            // means that we hit a timeout limit that
            // was previously configured.
            z3::SatResult::Unknown => {
                Err(Error::SynthesisUnknown)
            }

            // There are no more inputs that don't
            // satisfy the spec! We're done!
            z3::SatResult::Unsat => {
                Ok(Verification::WorksForAllInputs)
            }

            // There still exist inputs for which the
            // synthesized program does not satisfy the
            // spec. Return the counterexample.
            z3::SatResult::Sat => {
                let model = solver.get_model();
                self.add_invalid_assignment(assignments);
                let inputs = eval_bitvecs(
                    &model,
                    &inputs,
                );
                Ok(Verification::Counterexample(inputs))
            }
        }
    }
}

In the case where verification finds a counterexample, we make a call to the add_invalid_assignment method. This is another trick taken from Souper: we remember assignments that work for some inputs, but not all of them, and explicitly forbid them in future finite synthesis queries. This saves the SMT solver from reconsidering these seemingly promising assignments, only to find once again that they don’t work for one of the example inputs.

Finite Synthesis

Recall that finite synthesis searches for a location mapping that satisfies the specification for each of our example inputs, but might or might not satisfy the specification when given other inputs.

The first constraint on the location mapping is that it corresponds to a well-formed program. This constraint actually remains the same for every iteration of CEGIS, so we generate the constraint once when creating a new Synthesizer instance, and then reuse the already constructed constraint for each finite synthesis query. Similarly, we also store the location variables in the Synthesizer and reuse them across all iterations of the CEGIS loop.

pub struct Synthesizer<'a> {
    // ...
    locations: LocationVars<'a>,
    well_formed_program: Bool<'a>,
    // ...
}

Recall the definition of the \(\psi_\mathrm{wfp}\) well-formed program constraint:

\( \begin{align} \psi_\mathrm{wfp}(L) &= \bigwedge\limits_{p \in \textbf{P}} \left( 0 \leq l_p \lt M \right) \\ & \land \, \bigwedge\limits_{r \in \textbf{R}} \left( \lvert \vec{I} \rvert \leq l_r \lt M \right) \\ & \land \, \psi_\mathrm{cons}(L) \\ & \land \, \psi_\mathrm{acyc}(L) \end{align} \)

It says that each parameter location \(l_p\) falls within the range \(0 \leq l_p < M \), each temporary result location \(l_r\) falls within the range \(\lvert \vec{I} \rvert \leq l_r < M\), that the locations are consistent, and that there are no dataflow cycles.

Constructing the equivalent SMT expression in Z3 follows pretty much directly from that, except it is a bit noisier, since we’re passing contexts around and need to convert Rust usizes and u32s into Z3 bitvectors of the appropriate width:

impl<'a> LocationVars<'a> {
    fn well_formed_program(
        &self,
        context: &'a z3::Context,
        library: &Library,
        invalid_connections: &mut HashSet<(u32, u32)>,
    ) -> Bool<'a> {
        // We'll build up all of our well-formed program
        // constraints in this list, and then `and` them
        // all together at the end.
        let mut wfp = vec![];

        // A well-formed program is consistent.
        wfp.push(self.consistent(
            context,
            invalid_connections,
        ));

        // A well-formed program is acyclic.
        wfp.push(self.acyclic(context, library));

        let i_len = self.line_from_u32(
            context,
            self.inputs.len() as u32,
        );
        let m = self.line_from_u32(
            context,
            (self.results.len() +
                self.inputs.len()) as u32,
        );
        let zero = self.line_from_u32(context, 0);

        // The inputs are always assigned to the first
        // locations.
        for (i, l) in self.inputs.iter().enumerate() {
            let i = self.line_from_u32(
                context,
                i as u32,
            );
            wfp.push(l._eq(&i));
        }

        // All component parameter locations are in
        // the range `0 <= l < M`.
        for l in &self.params {
            // 0 <= l
            wfp.push(line_le(&zero, l));
            // l < M
            wfp.push(line_lt(l, &m));
        }

        // All component result locations are in the
        // range `|i| <= l < M`.
        for l in &self.results {
            // |i| <= l
            wfp.push(line_le(&i_len, l));
            // l < m
            wfp.push(line_lt(l, &m));
        }

        // `and` all of our constraints together.
        and(context, &wfp)
    }
}

Remember that the \(\psi_\mathrm{cons}\) consistency constraint ensures that we don’t assign two components to the same line:

\( \psi_\mathrm{cons}(L) = \bigwedge\limits_{x,y \in \textbf{R}, x \not\equiv y} \left( l_x \neq l_y \right) \)

Our consistent method creates the corresponding SMT expression for Z3, and additionally records pairs of location indices into the invalid_connections map. This map keeps a record of location variables that well-formed programs cannot have dataflow between. Therefore, we don’t need to add connection clauses for these pairs of location variables in our eventual implementation of the \(\psi_\mathrm{conn}\) connectivity constraint. Leaving those pairs out of the connectivity constraint keeps the SMT expressoin that much smaller, which should help Z3 solve it that much faster. Once again, this trick was taken from Souper.

impl LocationVars<'a> {
    fn consistent(
        &self,
        context: &'a z3::Context,
        invalid_connections: &mut HashSet<(u32, u32)>,
    ) -> Bool<'a> {
        // Build up all the consistency constraints
        // in this list.
        let mut cons = vec![];

        for (i, (index_x, loc_x)) in self
            .results_range()
            .zip(&self.results)
            .enumerate()
        {
            for (index_y, loc_y) in self
                .results_range()
                .zip(&self.results)
                .skip(i + 1)
            {
                // Can't have dataflow from a result to
                // another result directly, they need to
                // be connected through parameters, so
                // add this pair to the invalid
                // connections map.
                invalid_connections.insert(
                    (index_x, index_y)
                );

                // Components cannot be assigned to the
                // same line, so these location variables
                // cannot have the same value:
                // `loc_x != loc_y`.
                cons.push(loc_x._eq(loc_y).not());
            }
        }

        // `and` all the constraints together.
        and(context, &cons)
    }
}

The \(\psi_\mathrm{acyc}\) acyclicity constraint enforces that our synthesized location mappings don’t have dataflow cycles:

\( \psi_\mathrm{acyc}(L) = \bigwedge\limits_{i=0}^{N-1} \left( \bigwedge\limits_{p \in \vec{I}_i} \left( l_p < l_{O_i} \right) \right) \)

Our implementation of the acyclicity constraint doesn’t do anything fancy, and is just a direct translation of the constraints into an SMT expression:

impl LocationVars<'a> {
    fn acyclic(
        &self,
        context: &'a z3::Context,
        library: &Library,
    ) -> Bool<'a> {
        // Build up the constraints in this list.
        let mut acycs = vec![];

        let mut params = self.params.iter();

        for (result_loc, comp) in self
            .results
            .iter()
            .zip(&library.components)
        {
            for _ in 0..c.operand_arity() {
                let param_loc = params.next().unwrap();

                // The component's param's location
                // must be less than the component's
                // result's location, meaning the
                // param is already defined before it
                // is used: `param_loc < result_loc`.
                acycs.push(
                    line_lt(param_loc, result_loc)
                );
            }
        }

        // `and` all the constraints together.
        and(context, &acycs)
    }
}

Our next steps are implementing the \(\psi_\mathrm{conn}\) connectivity constraint and the \(\phi_\mathrm{lib}\) library specification. These do change with each iteration of the CEGIS loop, because we instantiate them for each example input we’re working with. That means we can’t cache-and-reuse them, like we do with the well-formed program constraint.

The \(\psi_\mathrm{conn}\) connectivity constraint encodes the dataflow connections between components in the library. If two location variables refer to the same location, then the entities whose location is assigned by those variables must have the same value.

\( \psi_\mathrm{conn}(L, \vec{I}, O, \textbf{P}, \textbf{R}) = \bigwedge\limits_{x,y \in \vec{I} \cup \textbf{P} \cup \textbf{R} \cup { O } } \left( \left( l_x = l_y \right) \implies \left( x = y \right) \right) \)

The connectivity method constructs a Z3 expression that implements this constraint. Previously, we had recorded pairs of location variables that cannot be connected directly. Now, we filter out any such connections from this constraint, keeping the SMT expression smaller, as explained earlier.

impl<'a> Synthesizer<'a> {
    fn connectivity(
        &self,
        inputs: &[BitVec<'a>],
        output: &BitVec<'a>,
        params: &[BitVec<'a>],
        results: &[BitVec<'a>],
    ) -> Bool<'a> {
        // A table mapping a location variable's index
        // to the location variable and its associated
        // entity: `index -> (l[x], x)`.
        let locs_to_vars: Vec<_> = self
            .locations
            .inputs
            .iter()
            .zip(inputs)
            .chain(
                self.locations
                    .params
                    .iter()
                    .zip(params)
            )
            .chain(
                self.locations
                    .results
                    .iter()
                    .zip(results)
            )
            .chain(iter::once(
                (&self.locations.output, output)
            ))
            .collect();

        // Build up the constraints in this list.
        let mut conn = vec![];

        for (index_x, (l_x, x)) in locs_to_vars
            .iter()
            .enumerate()
        {
            for (index_y, (l_y, y)) in locs_to_vars
                .iter()
                .enumerate()
                .skip(i + 1)
            {
                // If these locations can't ever be
                // connected directly, don't bother
                // constraining them.
                if self.is_invalid_connection(
                    index_x as u32,
                    index_y as u32,
                ) {
                    continue;
                }

                // If these two location variables
                // refer to the same location, then
                // their entities are connected to
                // each other, and must have the
                // same value.
                conn.push(
                    l_x._eq(l_y).implies(&x._eq(y))
                );
            }
        }

        // `and` all the constraints together.
        and(self.context, &conn)
    }
}

Our final prerequisite before we can implement the whole finite synthesis query is the \(\phi_\mathrm{lib}\) library specification, which describes the behavior of the library as a whole:

\( \phi_\mathrm{lib}(\textbf{P}, \textbf{R}) = \phi_i(\vec{I}_0, O_0) \land \ldots \land \phi_i(\vec{I}_{N-1}, O_{N-1}) \)

Implementing the \(\phi_\mathrm{lib}\) library specification involves getting the immediates, operands, and result variables for each component, asking the component to make its SMT expression relating those variables to each other, and finally anding all those expressions together:

impl<'a> Synthesizer<'a> {
    fn library(
        &self,
        immediates: &[BitVec<'a>],
        params: &[BitVec<'a>],
        results: &[BitVec<'a>],
        bit_width: u32,
    ) -> Bool<'a> {
        // Build up each component's spec expression
        // in here.
        let mut lib = vec![];

        let mut immediates = immediates;
        let mut params = params;

        for (result, comp) in results
            .iter()
            .zip(&self.library.components)
        {
            // Chop the immediates for this component off
            // the front of the list.
            let (these_imms, rest) = immediates.split_at(
                comp.immediate_arity()
            );
            immediates = rest;

            // Chop the params for this component off the
            // front of the list.
            let (these_params, rest) = params.split_at(
                comp.operand_arity()
            );
            params = rest;

            // Create the spec for this component, and
            // make sure its result is constrained by it.
            lib.push(
                result._eq(&comp.make_expression(
                    self.context,
                    these_imms,
                    these_params,
                    bit_width,
                ))
            );
        }

        // `and` all of the component specs together.
        and(self.context, &lib)
    }
}

Ok, we finally have all the functions we need to implement finite synthesis! The finite synthesis query assigns values to our location variables such that the resulting mapping corresponds to a well-formed program, and that program satisfies our specification for each of our example inputs.

\( \begin{align} & \exists L, O_0, \ldots, O_{\vert S \rvert - 1}, \textbf{P}_0, \ldots, \textbf{P}_{\vert S \rvert - 1}, \textbf{R}_0, \ldots, \textbf{R}_{\vert S \rvert - 1}: \\ & \qquad \psi_\mathrm{wfp}(L) \,\, \land \\ & \qquad \qquad \bigwedge\limits_{i=0}^{\lvert S \rvert - 1} \left( \phi_\mathrm{lib}(\textbf{P}_i, \textbf{R}_i) \land \psi_\mathrm{conn}(L, S_i, O_i, \textbf{P}_i, \textbf{R}_i) \land \phi_\mathrm{spec}(S_i, O_i) \right) \\ \end{align} \)

Our implementation of the finite synthesis query mostly follows the same structure as that formula:

• We already have the well-formed program constraint cached and ready for reuse, so we don’t need to recreate it here.

• We loop over each of our example inputs:

  • Create fresh program output variables, fresh component parameter variables, and fresh component result variables for each example.

  • Constrain each component’s parameters and output to behave as dictated by our library.

  • Connect cross-component variables together as described by the location mapping, with the connectivity constraint.

  • Require that the program specification is satisfied for this example input.

• Additionally, we assign the program’s output’s location to the line we were given. This lets callers optionally force the synthesis of optimally small programs.

• Finally, we run the query and parse the resulting location mapping’s assignments out of the solver’s model.

impl<'a> Synthesizer<'a> {
    fn finite_synthesis(
        &mut self,
        example_inputs: &HashSet<Vec<u64>>,
        output_line: u32,
        bit_width: u32,
    ) -> Result<Assignments> {
        let immediates = self.fresh_immediates(
            bit_width
        );

        // We'll build up the constraints that the
        // location assignments work for each input
        // in this list.
        let mut works_for_inputs = vec![];

        for inputs in example_inputs {
            // Convert the inputs into bitvectors.
            let inputs: Vec<_> = inputs
                .iter()
                .map(|i| BitVec::from_i64(
                    self.context,
                    *i as i64,
                    bit_width,
                ))
                .collect();

            // Create fresh params, results, and
            // output variables. These are the
            // existentially-quantified `P[i]`,
            // `R[i]`, and `O[i]` from the formula.
            let params = self.fresh_param_vars(
                bit_width
            );
            let results = self.fresh_result_vars(
                bit_width
            );
            let output = fresh_output(
                self.context,
                bit_width,
            );

            // The components behave as described by
            // the library.
            let lib = self.library(
                &immediates,
                &params,
                &results,
                bit_width,
            );
            works_for_inputs.push(lib);

            // The components are connected together as
            // described by the location variables.
            let conn = self.connectivity(
                &inputs,
                &output,
                &params,
                &results,
            );
            works_for_inputs.push(conn);

            // And given that, our specification for
            // desired program behavior is satisified.
            let spec = self
                .spec
                .make_expression(
                    self.context,
                    &inputs,
                    &output,
                    bit_width,
                );
            works_for_inputs.push(spec);
        }

        let works_for_inputs: Vec<&_> = works_for_inputs
            .iter()
            .collect();

        // Enforce that the output is on the required
        // line.
        let output_line = self.locations.line_from_u32(
            self.context,
            output_line,
        );
        let output_on_line = self
            .locations
            .output
            ._eq(&output_line);

        // Put all the pieces together!
        let query = self
            .well_formed_program
            .and(&works_for_inputs)
            .and(&[
                &output_on_line,
                // Do not synthesize any of the
                // assignments we've already
                // discovered to be invalid.
                &self.not_invalid_assignments,
            ]);

        let solver = self.solver();
        solver.assert(&query);

        match solver.check() {
            // It is unknown whether an assignment
            // that fits the constraints exists or
            // not. Usually this is because a timeout
            // was configured and we ran out of time.
            z3::SatResult::Unknown => {
                Err(Error::SynthesisUnknown)
            }

            // There are no assignments for the
            // location variables that satisfies our
            // synthesis constraints. We can't create
            // a program that satisfies the spec with
            // this component library.
            z3::SatResult::Unsat => {
                Err(Error::SynthesisUnsatisfiable)
            }

            // Ok, we have an assignment for the
            // location variables that fits our
            // synthesis constraints! Pull them out
            // of the model and return them.
            z3::SatResult::Sat => {
                let model = solver.get_model();

                let immediates = eval_bitvecs(
                    &model,
                    &immediates,
                );

                let params = eval_lines(
                    &model,
                    &self.locations.params
                );

                let results = eval_lines(
                    &model,
                    &self.locations.results,
                );

                let output = eval_line(
                    &model,
                    &output_line,
                );

                Ok(Assignments {
                    immediates,
                    params,
                    results,
                    output,
                })
            }
        }
    }
}