Smyth

Smyth is a program synthesizer that will fill in "holes" in a program in a typed, functional language (approximately Elm in our formulation) when given input-output examples, or, more generally, arbitrary assertions about the behavior of the code. These assertions are just "normal code" and can serve as unit tests once the synthesis has completed.

Evaluation of these assertions internally gives rise to input-output examples which, along with the types in the program, guide the synthesis search to fill in the holes. The key technical innovation, live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches (that is, programs with holes).

Live bidirectional evaluation enables Smyth not only to specify and solve interdependent synthesis goals over holes at arbitrary locations in the program, it also removes the need to specify "trace-complete" sets of examples recursive functions (that is, sets of examples that mirror the intended recursive behavior of the function to be synthesized), a major limitation of prior work on evaluator-based synthesis.

The name "Smyth" is a portmanteau of "sketching" and "Myth" (the type-and-example directed program synthesizer upon which the theory of Smyth is based). It was coined by Robert Rand who, incidentally, also coined the name "Myth."

Additional Resources

• A formal exposition of the system (including its evaluation and underlying theory) can be found in our ICFP 2020 publication, Program Sketching with Live Bidirectional Evaluation.

• A non-academic introduction to the Smyth project can be found on the project webpage.

• Code documentation for the system can be found here. The documentation for the core synthesis algorithm as outlined in our ICFP 2020 publication specifically can be found in the smyth/Smyth/ subdirectory. The codebase section below gives a high-level overview of the system.

• Further details about the implementation of Smyth can be found in Justin Lubin's undergraduate thesis, Forging Smyth: The Implementation of Program Sketching with Live Bidirectional Evaluation.

Installation

1. Install opam, the OCaml package manager.

2. Install OCaml 4.08.1 with the flambda optimizer by running opam switch create 4.08.1+flambda. OCaml versions after 4.08.1 should work fine too, but are untested.

3. Run make deps in the root directory of this project to download all the necessary opam dependencies.

4. Run make to build the Smyth executable. The executable is accessible via the smyth symlink in the root directory of this project.

To replicate the experiments we have run to evaluate Smyth, you will also need the following tools installed:

• GNU Octave
• LaTeX
• Python 2.7
• Python 3

To modify the documentation, you will also need the following tools installed:

• BeautifulSoup 4

The benchmark sketches from the experimental evaluation of Smyth are stored in suites/SUITE_NAME/sketches and the input-examples used for those sketches are stored in suites/SUITE_NAME/examples. If you want to see the actual synthesis output on just one of these sketches, you can use the forge helper script that we have provided in the root directory of this project as follows:

./forge <top1|top1r|top3> <suite-name> <sketch-name>

So, for example, you could run

./forge top1 no-sketch list_sorted_insert

to see the top result of running the list_sorted_insert benchmark from the no-sketch suite.

Updates

August 20, 2020: A new release, icfp-2020-v1 includes module-level documentation for the smyth library and fixes a bug that caused Experiments 2b and 3b to fail to run.

Running the Experimental Evaluation

Quick summary: navigate to experiments/, run ./run-all 10, look at /experiments/latex-tables/smyth-experiment-tables.pdf

To run all the data collection and analysis for Smyth as described in our ICFP paper, navigate to the experiments/ directory and run the script run-all, which takes a positive integer N as an argument that indicates how many trials per example-set size to run for each benchmark in Experiment 2b and 3b (the randomized experiments).

We ran these experiments with N = 50 (that is, ./run-all 50), which takes about 2 to 2.5 hours to run on a Mid 2012 MacBook Pro with a 2.5 GHz Intel Core i5 CPU and 16 GB of RAM.

If you would prefer to get the results faster (with the loss of statistical precision), we would recommend running the experiments with N = 10 (that is, ./run-all 10), which takes about 30 minutes to run on the same MacBook.

Once this script is complete, you can take a look at the results with any phenomena of note explained in experiments/latex-tables/smyth-experiment-tables.pdf.

Note: Rarely, due to timing issues with the UNIX Timer API, one of the benchmarks that is not indicated as a failure might crash with a "Timeout" exception during Experiments 2b and 3b. Even more rarely, a stack overflow error might occur. To combat these situations, the Experiment 2b and 3b scripts automatically retry a benchmark on unexpected failure.

The Codebase

The lib/smyth directory contains all the code for the core implementation of the Smyth synthesis algorithm. The lib/stdlib2 directory contains helper functions that are used throughout the codebase. The src/ directory contains the code relevant to the command-line interface to Smyth, as well as some code that is used for its experimental evaluation.

The following table provides a roadmap of where each concept/figure in the paper can be found in the codebase, in order of presentation in the paper.

Concept	File (in lib/smyth/)
Syntax of Core Smyth	lang.ml
Type checking	type.mli/type.ml
Expression evaluation	eval.mli/eval.ml
Resumption	eval.mli/eval.ml
Example satisfaction	example.mli/example.ml
Constraint satisfaction	constraints.mli/constraints.ml
Constraint merging	constraints.mli/constraints.ml
Live bidirectional example checking	uneval.mli/uneval.ml
Example unevaluation	uneval.mli/uneval.ml
Program evaluation	eval.mli/eval.ml
Result consistency	res.mli/res.ml
Assertion satisfaction and simplification	uneval.mli/uneval.ml
Constraint simplification	solve.mli/solve.ml
Constraint solving	solve.mli/solve.ml
Type-and-example-directed hole synthesis	fill.mli/fill.ml
Type-directed guessing (term generation)	term_gen.mli/term_gen.ml
Type-and-example-directed refinement	refine.mli/refine.ml
Type-and-example-directed branching	branch.mli/branch.ml

To see how these concepts all fit together with actual code, you can take a look at the "synthesis pipeline" in lib/smyth/endpoint.ml (specifically, the solve function).