Synthesis tools have seen significant success in recent times. However,
past approaches often require a complete and accurate embedding of the source
language in the logic of the underlying solver, an approach difficult for
industrial-grade languages. Other approaches couple the semantics of the source
language with purpose-built synthesizers, necessarily tying the synthesis engine
to a particular language model.
In this paper, we propose Absynthe, an alternative approach based on
user-defined abstract semantics that aims to be both lightweight and language
agnostic, yet effective in guiding the search for programs.
A synthesis goal in Absynthe is specified as an abstract
specification in a lightweight user-defined abstract domain and concrete test
cases.
The synthesis engine is parameterized by the abstract semantics and independent
of the source language.
Absynthe validates candidate programs against test cases using the
actual concrete language implementation to ensure correctness.
We formalize the synthesis rules for Absynthe
and describe how the key ideas are scaled-up in our implementation in Ruby. We
evaluated Absynthe on SyGuS strings benchmark and found it competitive with
other enumerative search solvers. Moreover, Absynthe's ability to combine
abstract domains allows the user to move along a cost spectrum, i.e., expressive
domains prune more programs but require more time. Finally, to verify
Absynthe can act as a general purpose synthesis tool, we use Absynthe to
synthesize Pandas data frame manipulating programs in Python using simple
abstractions like types and column labels of a data frame. Absynthe reaches
parity with AutoPandas, a deep learning based tool for the same benchmark
suite. In summary, our results demonstrate Absynthe is a
promising step forward towards a general-purpose approach to synthesis that may
broaden the applicability of synthesis to more full-featured languages.