SuFu

Artifact for PLDI'24: Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis.

The updates of this project can be found on GitHub.

Install

You can either build SuFu from the source, use it in a docker container, or directly try it online.

Build from source (Tested on Ubuntu 20.04)

Install dependencies. This project requires gcc $\geq 9$, CMake $\geq 3.13$, opam (tested on version 2.1.3 and switch ocaml.4.10.0), and python3. The other dependencies can be installed as follows.
```
$ apt-get install libjsoncpp-dev libgoogle-glog-dev libgflags-dev pkg-config
$ pip3 install tqdm argparse
$ opam install ocamlfind yojson
```

Clone SuFu

$ git clone https://github.com/jiry17/SuFu

Build the whole project under the root directory of the project.
```
$ cd SuFu; ./install
```
(optional) SuFu will perform better when Gurobi, a commercial constraint solver, is available. You can get an academic license of gurobi via the following steps.
1. Register or login at the webside of Gurobi.
2. Visit the Free Academic License page and follow the instructions on it.
3. Get a command like grbgetkey x...x at the bottom of the webpage.
4. Execute this command under directory SuFu/thirdparty/gurobi912/linux64/bin/.
5. Test your license by running gurobi.sh under the same directory as Step 4.

Download docker image

We also released a docker image of SuFu. You can download and run it using the following commands.

$ docker pull takanashirikka/sufu
$ docker run -i -t takanashirikka/sufu

In this image, SuFu is built under directory /root/SuFu. Its file structure is the same as this repository (see the last section of this document) and the executable of SuFu is available as /root/SuFu/build/executor/run.

Note: Gurobi is unavailable in this docker image because the adademic license of Gurobi cannot be used on virtual machines. Therefore, we still recommend building this project from source.

Run tests

Note: In the remainder of this document, all commands are assumed to be executed in the root directory of SuFu, which is /root/SuFu in our docker image and is the directory created by git clone if SuFu is built from the source.

Test whether the project is successfully built:
```
$ build/executor/run --benchmark=benchmark/autolifter/single-pass/sum.f --output=res.f --use_gurobi=false
```
The last line of the command-line output shoud be Success, and there should be an optimized program in file res.f.
Test whether SuFu works normally with gurobi. Note that the docker version must fail on this task because it does not have a gurobi license.
```
$ build/executor/run --benchmark=benchmark/autolifter/single-pass/sum.f --output=res.f --use_gurobi=true
```
Similar to the previous test, the last line of the command-line output should be Success, and there should be an optimized program in file res.f.

Run SuFu on a Single Task

You can run SuFu using the binary file build/executor/run.

$ build/executor/run --benchmark=BENCHMARK --output=OUTPUT --use_gurobi={true, false}

--benchmark: the file of the reference program.
--output: the output file of the optimized program.
--gurobi: whether to use Gurobi as the underlying constraint solver.

For example, the following command runs SuFu (without Gurobi) to optimize a reference program in file benchmark/autolifter/single-pass/mts.f and stores the optimized program to file res.f.

build/executor/run --benchmark=benchmark/autolifter/single-pass/mts.f --output=res.f --use_gurobi=false

Reproduce Results in Our Paper

We provide a script exp/python/main.py to reproduce the results in our paper. Its usage is as follows.

$ cd exp/python
$ python3 main.py [-exp {rq1,rq2,rq3,total}]
                  [-c {Restart,Continue,R,C}] [-g {false,true}] [-t TIMEOUT]
# For example, reproduce all statistics in our paper using the cached results
$ python3 main.py -exp total -c C

-exp: the name of the experiment. rq1, rq2, and rq3 correspond to Tables 5, 7, and 8 in our paper, respectively, and total denotes all of them.
-c: whether to clear the cached results: R represents yes while C represents no. All cached results can be found in exp/result_cache.
-g: whether to use Gurobi as the underlying solver of SuFu.
-t: the time out of each execution (in seconds), where the default value is 600

For the case of building from source, you need to install the baseline solvers (in directory thirdparty) before re-running the comparison with baseline solvers. In our docker image, we have installed all baseline solvers such that you can directly re-run the comparisons with Synduce and Grisette.

Note: The baseline solver AutoLifter requires Gurobi as an underlying solver. Therefore, the comparison with AutoLifter requires a Gurobi license and cannot be reproduced in docker.

Install AutoLifter

Install the bounded verifier cbmc as follows.
```
$ apt-get install cbmc
```

Clone AutoLifter and build it from source.

$ cd thirdparty
$ git clone https://github.com/jiry17/AutoLifter.git
$ cd AutoLifter; ./install

Test whether AutoLifter is successfully built.
```
$ cd thirdparty/AutoLifter/run
$ ./run -p dac -t sum --solver Relish
```
The last few lines of the command-line output should be Success followed by some synthesis results and some statistics.

Install Synduce

Install Synduce (in directory thirdparty) following the instructions in its repository.
Test whether Synduce is successfully built for our usage.
```
$ cd thirdparty/Synduce
$ ./Synduce benchmarks/combine/mts.ml
```
The last few lines of the command-line outputs should be Solution found in … followed by the synthesis results.

Install Grisette

Install dependencies. haskell-stack is required to build Grisette.

Install Grisette and build the execution environment.

$ cd thirdparty/Grisette/src/run_test
$ stack ghci

Test whether Grisette is successfully built for our usage.
```
$ cd thirdparty/Grisette
$ cp benchmark/autolifter/single-pass/sum.hs src/run_test/Main.hs
$ cd src; echo "main" | stack ghci
```
The output in ghci should be "success!" followed with a line showing the time cost.

The Structure of This Repository

Evaluation results

All evaluation results are available in directory exp, organized as follows.

The performance of each solver is summarized in exp/result_cache/*.json, where the synthesis status (fail or success) and the time cost are recorded.
exp/label records the fully annotated program generated by our sketch extraction approach, exp/oup/sufu records the command-line output of each execution, and exp/res/sufu records the optimized programs generated by SuFu.

Besides, all benchmarks in our dataset are vailable in directory benchmark.

Source code

Our source code is stored in src, where src/surface implements our surface language in Ocaml, and the other sub-directories of src implement SuFu in C++, organized as follows.

Directory	Description
`basic`	Those basic data structures required to describe a synthesis task, such as values (`values`), semantics (`semantics`), and programs (`program`).
`executor`	The entrance of invoking SuFu (`executor/run_incre_label.cpp`).
`incre`	The core of SuFu, where `analysis` extracts examples, `autolabel` implements our sketch extraction approach, `solve` implements the core synthesis algorithm, and `grammar` constructs the program spaces used in synthesis.
`include`	The head files of this C++ project.
`solver`	The implementation of PolyGen, which is used to synthesize sketch holes from separate input-output examples.