Superoptimization is a compilation strategy that uses search to
improve code quality, rather than relying on a canned sequence of
transformations, as traditional optimizing compilers do.
%
This search can be seen as a program synthesis problem: from
unoptimized code serving as a specification, the synthesis
procedure attempts to create a more efficient implementation.
%
An important family of synthesis algorithms works by enumerating
candidates and then successively checking if each refines the
specification, using an SMT solver.
%
The contribution of this paper is a pruning technique which reduces
the enumerative search space using fast dataflow-based techniques
to discard synthesis candidates that contain symbolic constants and
uninstantiated instructions.
%
We demonstrate the effectiveness of this technique by improving the
runtime of an enumerative synthesis procedure in the Souper
superoptimizer for the LLVM intermediate representation.
%
The techniques presented in this paper eliminate 65% of the solver
calls made by Souper, making it 2.32x faster (14.54 hours vs 33.76
hours baseline, on a large multicore) at solving all 269,113 synthesis
problems that Souper encounters when optimizing the C and C++ programs
from SPEC CPU 2017.