Syndicate

Getting Started

Artifact Description

The artifact contains the following folders and files:

1. benchmarks: Contains the benchmarks on which we evaluate Syndicate.
2. deps: Contains external dependencies of Syndicate.
3. src: Contains the code for Syndicate and other files used to run the benchmarks and plot the graphs.
4. prerun_logs: Contains logs of Syndicate run on the benchmarks. The user can generate these logs again, for which the instructions are below.

Installation Instructions

1. Build the docker image.

   docker build --no-cache -t syndicate .
   

   The image takes around 13 minutes to build completely.

2. Run the image in interactive mode.

   docker run -v "$PWD/plots:/home/plots" -v "$PWD/logs:/home/logs" -it syndicate
   

   The -v "$PWD/plots:/home/plots" and -v "$PWD/logs:/home/logs" part is used to mount an external plots and logs directory to the internal directory and this can be changed accordingly.

Testing the installation

Make sure that /home/libs/lib/ appears in LD_LIBRARY_PATH or set it using:

export LD_LIBRARY_PATH=/home/libs/lib/:$LD_LIBRARY_PATH

To check if the installation works, run the following command from /home/src:

python3 run.py --file ../benchmarks/custom/example1/Example1.java

It runs Syndicate on a simple terminating example present at Example1. If the installation is correct, one should see an output as follows:

{'loops_rf_inv': {0: ['[[2, -1, 7], [1, -1, 1], [-3, 1, -6]]', '[[0, 0, 0]]']}, 'runtime': 3.898636817932129, 'proved': True}

The loops_rf_inv field of the output gives the ranking function and the invariant used to prove the loop terminating. Note: Syndicate relies on dynamically generated program traces and non-deterministic SMT solver calls (Z3), so the exact ranking functions and invariants may differ across runs; however, all outputs are guaranteed to be sound proofs of termination.

Similarly, when run on a non-terminating example (Example2), Syndicate returns an output with 'proved' set as False, indicating that Syndicate could not prove the termination of the program.

python3 run.py --file ../benchmarks/custom/example2/Example2.java
{'loops_rf': {}, 'runtime': 14.37025761604309, 'proved': False}

Step-By-Step Instructions

Once the installation is complete, the user can use the following command to generate all the tables and plots presented in the paper. The script uses pre-generated logs from the prerun_logs directory. The user can also regenerate the logs, the commands for which can be found below.

Generate tables and plots:

From the home directory, running this command generates all the tables and plots:

python3 src/plot.py --logs prerun_logs

The tables will be displayed on the terminal, and the plots are generated in the plots directory in the root folder. The plots_path argument can be used to specify the path for plots (relative to the project root).

python3 src/plot.py --logs prerun_logs --plots_path my_plots

Regenerating logs

From the home directory, you can regenerate all logs by running the src/run_experiments.sh script using the following command.

bash src/run_experiments.sh --logs logs

This will generate logs for all benchmarks and all configurations present in the prerun_logs directory, using a 120-second timeout per benchmark, and store the results in the logs directory. Running the complete set of experiments takes approximately 48 hours to finish.

To run on a subset of all benchmarks, you can specify the start_ind and end_ind. For instance, to run all experiments on the first 10 programs:

bash src/run_experiments.sh --start_ind 0 --end_ind 9

Users can also specify custom timeout (in seconds) using the timeout flag.

bash src/run_experiments.sh --start_ind 0 --end_ind 10 --timeout 10 --logs logs_10

Note: If the logs are generated with a timeout t, then please use the same timeout to plot the tables and figures.

python3 src/plot.py --logs logs --timeout t

To run specific algorithms presented in the paper:

The src/run_experiments.sh file illustrates how the src/run.py file can be used with different arguments to run Syndicate with various configurations.

Refer to the following for command line arguments:

Argument	Type	Default	Description
--file	str	'all'	Specifies the java file name to test. If not provided, it defaults to processing all files.
--function	str	'all'	Specifies the function within the file that should be analyzed. The default is "loop".
--template	int	3	Specifies which template to use during processing. Allowed templates - 1,2,3,4,5.
--traces	int	100	Number of traces for initialization.
--pref	int	10	Sets the Pref parameter.
--piter	int	10	Sets the Piter parameter.
--unbounded	flag	False	To run syndicate_unbounded.
--full	flag	False	To run syndicate_full.
--bsynergy1	flag	False	To run bsynergy1.
--bsynergy2	flag	False	To run bsynergy2.
--bcombined	flag	False	To run bcombined.

1. Syndicate_best with template t

python3 run.py --file all --template t --best

2. Syndicate_seq

python3 run.py --file all --template 3 --traces 100 --pref 10 --piter 10

3. Syndicate_static with template t

python3 run.py --file all --template t --traces 0 --pref 10 --piter 10 

4. Syndicate_unbounded with template t

python3 run.py --file all --template t --traces 100 --pref 10 --piter 10 --unbounded

5. Syndicate_full with template t

python3 run.py --file all --template t --traces 100 --full

6. Bsynergy1 with template t

python3 run.py --file all --template t --traces 0 --pref 10 --piter 10 --bsynergy1

7. Bsynergy2 with template t

python3 run.py --file all --template t --traces 0 --pref 10 --piter 10 --bsynergy2

8. Bcombined

python3 run.py --file all --template 1 --traces 0 --pref 10 --piter 10 --bcombined

Running Syndicate on a new Java file

To run Syndicate on a new file, specify the path to the Java source file (--file) and the name of the function to be analyzed (--function). This implementation only supports integer Java programs. The only library that can be imported is java.util.Random. To create a new Java file that can be analyzed by Syndicate, there should be a main function of the form:

public static void main(String[] args) {
	if (args.length >= n) {
		int v1 = Integer.parseInt(args[0]);
		int v2 = Integer.parseInt(args[1]);
        ...
		func(v1, v2, ...);
		}
	}

where func is the function to be analyzed. The only function call allowed within func is a call to new Random().nextInt().

To run this new file, use the following command.

python3 run.py --file ../benchmarks/custom/example1/Example1.java