Existing superoptimization and synthesis approaches consider candidate instruction sequences of increasing length and use constraint solvers to check whether a candidate correctly implements the source code. This works well for optimizing short straight-line code. With the increase in length of the target sequence, the search space dramatically increases, posing a challenge for existing approaches.

We describe a new approach to code generation and optimization. Our approach uses an SMT solver in a novel way to generate efficient code for modern architectures and guarantee that the generated code correctly implements the source code. The distinguishing characteristic of our approach is that the size of the constraints does not depend on the length of the candidate sequence of instructions.

We implemented a preliminary prototype of the approach and applied it to optimize small but tricky examples used as standard benchmarks for other superoptimization and synthesis tools. Our implementation handles arbitrary loop-free code (not only basic blocks) as input and output. The quality of generated code compares favorably with production compilers and other superoptimization tools.