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.
Wed 25 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00
Program Generation and SynthesisOnward! Papers at Regency B
Chair(s): Emina Torlak University of Washington
|Generating Chat Bots from Web API Specifications|
Mandana Vaziri IBM Research, Louis Mandel IBM Research, Avraham Shinnar IBM Research, Jerome Simeon IBM Research, Martin Hirzel IBM Research
|ChimpCheck: Property-based Randomized Test Generation for Interactive Apps|
Edmund Lam University of Colorado Boulder, Peilun Zhang , Bor-Yuh Evan Chang University of Colorado Boulder
Abhinav Jangda University of Massachusetts, Amherst, Greta Yorsh Queen Mary University of London