Sippy

This repository contains the code for the paper "Inductive Synthesis of Inductive Heap Predicates", where three different components are presented:

1. Sippy: the tool for synthesizing inductive heap predicates from examples, based on open-source tool Popper, whose benchmark is in the folder ./predicates/experiments, and implemented in the folder ./popper.
2. Grippy-benchmark: the tool and benchmark to generate input graphs for Sippy using Grippy, shown in the folder ./graphgen_experiments.
3. SuSLik-benchmark: the benchmark that uses output of Sippy to synthesize heap-manipulating programs by SuSLik, shown in the folder ./suslik_experiments.
4. ShaPE-benchmark: the benchmark from Sippy to be tested with ShaPE, shown in the folder ./ShaPE_experiments.

Requirements

• pyswip
• SWI-Prolog (8.4.2 or above)
• Clingo (5.5.0 or above)
• SuSLik (to run the SuSLik benchmarks)
• ShaPE (to run the ShaPE benchmarks)

Instructions

Python dependencies

To install the required Python dependencies, you can use the following command:

pip install -r requirements.txt

Sippy

To run Sippy, you can use the following command:

./sippy.sh <path-to-examples>

For example, to run the benchmark for the sll predicate, you can use the following command:

./sippy.sh ./predicates/experiments/sll

The detailed execution logs will be saved in ./example.log.

To compare with Popper, and with or without the use of optimisations, you can use the following commands:

./sippy.sh ./predicates/experiments/sll --unopt
./popper.sh ./predicates/experiments/sll 
./popper.sh ./predicates/experiments/sll --unopt

Grippy-benchmark

As an example to generate input graphs for sorted list by find functions, you can use the following commands:

cd graphgen_experiments/graph_generation/c-programs/srtl
python3 c-graphs-generator.py srtl-find.c

or the following with timeout:

timeout 10m python3 c-graphs-generator.py srtl-find.c 

SuSLik-benchmark

To run the SuSLik benchmarks, you can use the following command:

(Assume suslik is added to the path)

suslik ./suslik_experiments/copy/dll.syn