Synthesizing Loop-Free Programs with Rust and Z3

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: 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. 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: Loop-free: We are only synthesizing programs without loops. 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: General Synthesis Component-Based Synthesis Shape of Synthesized Programs Using any number of any of the target language's expressions Using only the components in the library Size of Synthesized Programs Varies Exactly the size of the library, since each component in the library is used exactly once 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