Learning Guided Enumerative Synthesis for Superoptimization

The field of program synthesis has seen substantial recent progress in new ideas, e.g., program sketching and synthesis modulo pruning, and applications, e.g., in program repair and superoptimization, which is our focus in this paper. The goal of superoptimization is to generate a program which is functionally equivalent to the given program but is optimal with respect to some desired criteria. We develop a learning-based approach to guide the exploration of the space of candidate programs to parts of the space where an optimal solution likely exists. We introduce the techniques of bulk and sequence orderings which enable this directed search. We integrate these machine learning techniques with an enumerative superoptimizer and experimentally evaluate our framework using a suite of subjects. Our findings demonstrate that machine learning techniques can play a useful role in reducing the amount of candidate program space that the enumerative search must to explore in order to find an optimal solution; for the subject programs, the reduction is up to 80% on average.