Abstract

In this paper, we investigate the problem of semi-automated inversion of imperative programs, which has the potential to make it much easier and less error prone to write programs that naturally pair as inverses, such as insert/delete operations, compressors/decompressors, and so on. Viewing inversion as a subproblem of program synthesis, we propose a novel synthesis technique called Path-based Inductive Synthesis (PINS) and apply it to inversion. PINS starts from a program P and a template T for its inverse. PINS then iteratively refines the space of template instantiations by exploring paths in the composition of P and T with symbolic execution. PINS uses an SMT solver to intelligently guide the refinement process, based on the paths explored so far. The key idea motivating this approach is the small path-bound hypothesis: that the behavior of a program can be summarized with a small, carefully chosen set of its program paths.

We evaluated PINS by using it to invert 14 programs such as compressors (e.g., Lempel-Ziv-Welch), encoders (e.g., UUEncode), and arithmetic operations (e.g., vector rotation). Most of these examples are difficult or impossible to invert using prior techniques, but PINS was able to invert all of them. We also found that a semi-automated technique we developed to mine a template from the program to be inverted worked well. In our experiments, PINS takes between one second to thirty minutes to synthesize inverses. We believe this proof-of-concept implementation demonstrates the viability of the PINS approach to program synthesis.