// HACKER NEWS — CYBERSECURITY
Synthesizing Loop-Free Programs with Rust and Z3 (2020)
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.
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.
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?!
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:
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.