Abstract

Program Inversion is the long-standing challenge problem of
automatically synthesizing an inverse I for a given program P.
This problem arises naturally in paired computations such as
compression/decompression, serialization/deserialization,
transactional memory rollback, bidirectional programming, and
even client-server applications. In this paper, we propose
a novel, automated synthesis algorithm for discovering program inverses.

Our approach combines ideas from symbolic execution-based testing and
constraint-based program analysis. We exploit the observation that I has
a control flow structure very related to that of P, and the expressions and
guards are related as well. Using P, we syntactically mine the control
flow structure, expression and guard sets for I, finitizing the
problem but with an exponential search space. To efficiently find a
solution in this space, we propose a technique that iteratively
refines the space of possible inverses. We pick a candidate inverse
and identify a feasible path for the candidate through P and I.
Using ideas from constraint-based analysis we find potential solutions
that satisfy the specification for the set of paths accumulated. We
continue this Path Based Inductive Synthesis (PINS)
procedure until the space contains only valid inverses.

Using a tool that implements PINS, we show we can synthesize inverses
for compressors (e.g., LZ77), packers (e.g., UUEncode), and arithmetic
transformers (e.g., image rotations). Additionally, we extend the idea
to programs composed in parallel and use it to synthesize a TFTP
client from its server. The inverses for these difficult programs
range from 5 to 20 lines of code, and our tool synthesizes them in a
median time of 40 seconds, demonstrating the viability of our
inversion approach.