=======

Diffy is the prototype tool that implements the verification technique reported in the paper "Diffy: Inductive Reasoning of Array Program using Difference Invariants". Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. In Proc of CAV 2021.

The artifact associated with the paper can be obtained from the Online Archives.

==================

Diffy accepts as input a C program in the format similar to SV-COMP. It verifies if the given post-condition of the program holds or not. Note that arrays in the program need to be stack allocated and not malloc'd.

	diffy [options] `filename`

Example:

	diffy cav21-bench/safe/nested-as1.c

Help:

	diffy --help

DIFFY_VERIFICATION_SUCCESSFUL - when the given post-condition is verified.

DIFFY_VERIFICATION_FAILED - when the given post-condition is violated.

DIFFY_VERIFICATION_UNKNOWN - when the result cannot be determined.

==============================

The recommended way to install this artifact is by compiling the Docker image based on Ubuntu 18.04. Instructions to install Docker can be found here. Subsequently, run the steps (1 through 6) listed below. Use a bash terminal to execute all commands on a linux system.

Step 4 builds the docker image and fetches packages and tools (approximately 1GB) over the internet. It may take more than an hour to build the entire docker image, depending on the network speed and machine configuration. Note that the "." at the end of the command in step 4 is important and needs to be typed in.

The built image includes all the tools and the required dependencies to reproduce the experiments reported in the paper and works without an active internet connection. The built image will occupy about 4GB of disk space. Step 5 runs the docker image in a container and opens a terminal into the container.

1. Download the artifact file diffy-artifact.tar.gz
2. tar -xvf diffy-artifact.tar.gz
3. cd diffy-artifact/
4. sudo docker build -t diffy .
5. sudo docker run --mount type=bind,source="$(pwd)/storage",target=/root --name diffy-artifact -it diffy:latest
6. diffy cav21-bench/safe/nested-as1.c

If the output of step 6 is DIFFY_VERIFICATION_SUCCESSFUL then diffy is functional and we are ready to run all the experiments.

At this point one may choose to exit the container (using the exit command) or continue running all the experiments as described in the next section.

Note: If docker is used on Windows OS then the word pwd needs to be surrounded with braces instead of parentheses as --mount type=bind,source="${pwd}/storage",target=/root for the command to function correctly.

Instead of steps 1 and 2, the repository can be cloned from GitHub.

===========================================

If the container was exited, execute the first two commands below to restart and run the same container. Otherwise, skip the first two instructions below.

1. sudo docker start diffy-artifact
2. sudo docker attach diffy-artifact
3. run-cav21-expts.sh safe 60
4. run-cav21-expts.sh unsafe 60

Steps 3 and 4 above execute the tools diffy [1], vajra [2], veriabs [3] and viap [4] on the benchmarks in cav21-bench/safe and cav21-bench/unsafe directories. vajra, veriabs and viap are the tools against which diffy is compared in the paper. Programs that satisfy the given post-condition are categorized as "Safe" as in Table 1 of the paper, and 157 such benchmarks are included in the cav21-bench/safe directory. Programs that violate the given post-condition are categorized as "Unsafe" as in Table 1 of the paper, and 146 such benchmarks are included in the cav21-bench/unsafe directory. A timeout of 60 seconds is set for each tool to verify a benchmark. We run diffy, vajra, veriabs and viap sequentially on all benchmarks in a directory. Collecting the verification results and generating the csv files and plots takes a small amount of additional time. Running step 3 to completion takes approximately 4 hours, and running step 4 to completion takes approximately 3 hours on a machine with Intel i7-6500U CPU, 16GB RAM, running at 2.5 GHz, and Ubuntu 18.04.5 LTS operating system. The execution time may vary based on machine configuration of the host, docker performance overhead, and CPU utilization by other applications running on the host machine.

Step 3 above creates the sub-directory cav21-bench/safe/plots that stores the plots as well as the summary of experimental results in the following files:

• safe_table_data_60.csv - Summary of experimental results on safe benchmarks in Table 1 (first four lines) of the paper
• safe_bench_60.pdf - Plot in figure 3(a) of the paper
• safe_bench_60.csv - Data for generating the plot in figure 3(a) of the paper
• safe_C1_60.pdf - Plot in figure 4(a) of the paper
• safe_C1_60.csv - Data for generating the plot in figure 4(a) of the paper
• safe_C2C3_60.pdf - Plot in figure 5(a) of the paper
• safe_C2C3_60.csv - Data for generating the plot in figure 5(a) of the paper

Step 4 creates the sub-directory cav21-bench/unsafe/plots that stores the plots as well as the summary of experimental results in the following files:

• unsafe_table_data_60.csv - Summary of experimental results on unsafe benchmarks in Table 1 (last four lines) of the paper
• unsafe_bench_60.pdf - Plot in figure 3(b) of the paper
• unsafe_bench_60.csv - Data for generating the plot in figure 3(b) of the paper
• unsafe_C1_60.pdf - Plot in figure 4(b) of the paper
• unsafe_C1_60.csv - Data for generating the plot in figure 4(b) of the paper
• unsafe_C2C3_60.pdf - Plot in figure 5(b) of the paper
• unsafe_C2C3_60.csv - Data for generating the plot in figure 5(b) of the paper

The directories cav21-bench/safe/plots and cav21-bench/unsafe/plots are copied to the host machine at diffy-artifact/storage/safe_plots_60 and diffy-artifact/storage/unsafe_plots_60 respectively. The pdf and csv readers on the host machine can now be used to view the plots and summary of experimental results from the csv files.

To generate the plots in figure 6(a) and figure 6(b) of the paper, execute the steps shown below with a timeout of 100 seconds. Due to the timeout value of 100 seconds, these steps take more time to execute than they required when the timeout was of 60 seconds.

1. run-cav21-expts.sh safe 100
2. run-cav21-expts.sh unsafe 100

=======================================

Since the submission of our paper to CAV, we have been able to run our tool, diffy, on additional benchmarks. These further demonstrate the advantages of diffy over the tools vajra, veriabs and viap. While data from these additional experiments do not appear in the paper (because these experiments were not completed before the submission of the paper), we are including these as part of the artifact evaluation, in case the artifact reviewers want to check out the performance of diffy on these additional benchmarks. These are included in additional-bench directory.

Tools diffy, vajra, veriabs, and viap can be tried on all the benchmarks in additional-bench/safe and additional-bench/unsafe directories with a timeout of 60 seconds using the following commands:

	run-all-tools.sh additional-bench/safe 60
	run-all-tools.sh additional-bench/unsafe 60

To execute only diffy on the benchmarks in additional-bench/safe directory with a timeout of 60 seconds, run the following commands:

        cd additional-bench/safe
        run-all-benchmarks.sh diffy 60
        cd -

diffy can be directly executed on individual benchmarks as follows:

	diffy additional-bench/safe/nested-ssn2.c

===================================

• Experiments submitted as part of this artifact generate all plots & the table with summary of results as described in the experiments section of the paper. Run times may slightly differ depending on machine configuration, docker performance overhead, and CPU utilization by other applications running on the host machine.

• diffy successfully verifies additional challenging benchmarks beyond those reported in the paper (given in the additional-bench directory).

===========

Following commands can be used to remove the docker container and the compiled image. Be careful as this will permanently delete the docker image for this artifact as well as the generated plots and data in the shared folder diffy-artifact/storage.

	sudo docker container rm diffy-artifact
	sudo docker image rm diffy
	sudo docker image prune
	rm -rf storage/*

=================================

Docker version 20.10.2 was used to test the image creation and its execution in a container.

In the folder that contains the Dockerfile, run the following command:

	sudo docker build -t diffy .

This command fetches the required packages/tools and downloads approximately 1GB of data from the internet. Depending on the network speed and machine configuration, the command may take more than an hour to run till completion. After the image is built, it will include all required tools and required dependencies. The built container will occupy about 4GB of disk space. Please ensure that there is enough disk-space for its storage and execution.

	sudo docker run --mount type=bind,source="$(pwd)/storage",target=/root --name diffy-artifact -it diffy:latest

--mount type=bind,source="$(pwd)/storage",target=/root specifies a persistent volume (i.e. the folder storage in the diffy-artifact directory) so that the generated plots (pdf,png files) can be saved in the diffy-artifact/storage folder and can be viewed using the pdf and csv readers from the host machine. Any data that needs to be transferred to the host machine or needs to be persistent across containers must be copied/created in this folder.

Note: If docker is used on Windows OS then the word pwd needs to be surrounded with braces instead of parentheses as --mount type=bind,source="${pwd}/storage",target=/root for the command to function correctly.

Running this command again will start a fresh container which does not retain any data from the previous runs. To create a fresh container using this command, ensure to use a different name in --name parameter, else an error will be encountered. To retain the data/computation and generated files from a container run, it needs to be re-started using the commands described in the next section.

To restart the container that you were working with, such that the files and data generated from that run are retained, use the following commands:

	sudo docker start diffy-artifact

	sudo docker attach diffy-artifact

View the docker containers running on the system:

	sudo docker ps -a

Remove the docker container named diffy-artifact running on the system:

	sudo docker container rm diffy-artifact

Remove any dangling docker images from the system to free-up space:

	sudo docker image prune

View docker images installed on the system:

	sudo docker images

Remove the installed docker image named diffy from the system:

	sudo docker image rm diffy

Create a docker image with all packages pre-installed:

	sudo docker save diffy:latest | gzip > diffy_latest.tar.gz

===========================

The diffy/bin directory contains a pre-compiled diffy executable file as well as the libraries that it depends on. It requires LLVM version 6.0, BOOST version 1.68 and Z3 version 4.8.7 to be installed on the system where it will be used. The following libraries are bundled with the binary:

• libboost_filesystem.so.1.68.0
• libboost_program_options.so.1.68.0
• libboost_system.so.1.68.0

• libz3.so.4.8.7.0

The source code and compilation instructions of the above library files can be found at the links below:

Boost version 1.68 can be found here

Z3 version 4.8.7 can be found here

Please follow the below instructions to use the pre-compiled binaries on a linux system:

	cd diffy/bin

	ln -s libz3.so.4.8.7.0 libz3.so.4.8

	export LD_LIBRARY_PATH=.:$LD_LIBRARY_PATH

	export PATH=.:$PATH

Note: Install LLVM 6.0 using the apt install command below if it is not already installed on the system.

============================

	sudo apt install git g  -7 cmake libboost-program-options-dev libboost-filesystem-dev libboost-system-dev flex bison

	sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 100 --slave /usr/bin/g   g   /usr/bin/g  -7 --slave /usr/bin/gcov gcov /usr/bin/gcov-7

Some package names may not be exact and will depend on the OS in use.

Run the following command to install LLVM 6.0 on the system:

	sudo apt install clang-6.0 clang-format-6.0 clang-tidy-6.0 libclang-6.0-dev

Run the following commands to patch the installation of LLVM 6.0 on the system:

	sudo ln -s /usr/share/llvm-6.0/cmake/ /usr/lib/llvm-6.0/lib/cmake/clang
	sudo ln -s /usr/lib/llvm-6.0/bin/clang /usr/lib/llvm-6.0/bin/clang-6.0

The second command in the patch may or may not be required depending on the OS in use. The patch for LLVM 6.0 is as suggested in this webpage.

To compile, navigate to the diffy directory containing the Makefile and execute the following command:

	make

This will result in the executable binary file diffy generated in the folder.

Note: Compilation requires an active internet connection for the first run as it fetches Z3 sources. This step may take an hour or more depending on the machine configuration as it compiles diffy along with the Z3 source code.

Navigate to the diffy directory containing the Makefile and execute the following command:

	make debug

This will result in the executable binary file diffy generated in the folder. The executable file takes nearly 2GB of disk-space.

Note: Requires an active internet connection for the first time as it fetches LLVM 6.0 sources before compiling them in debug mode. For the first run, this step may take more than 24 hours depending on the machine configuration as it compiles diffy, z3 and llvm in debug mode.

================================

	|- diffy/
	|	* Top level folder with source code, benchmarks, binaries and logs.
	|- diffy/bin/
	|	* Contains pre-compiled binaries of various tools, libraries and scripts.
	|	* run-cav21-expts.sh - script to reproduce CAV21 experiments and generate plots.
	|	* run-all-tools.sh - script for running all tools on all benchmarks in a directory.
	|	* run-all-benchmarks.sh - script for running a tool on all benchmarks in a directory.
	|	* extract-cav21-expt-csv.py - script to extract execution time and other data in csv format from the logs.
	|- diffy/Makefile
	|	* Make file for compiling the tool.
	|- diffy/src
	|	* Directory that contains the entire source code of the tool.
	|	* CMakeLists.txt - specification file for the cmake compilation utility.
	|	* main.cpp - file with the main function where the execution begins.
	|- diffy/src/aggregation
	|	* Compiler passes for code transformation based on LLVM IR.
	|	* array_ssa.cpp - generate a new ssa name for arrays in each loop of the program.
	|	* simplify_nl.cpp - simplify the input program for subsequent analysis.
	|	* create_pnm1.cpp - generation of $P_{N-1}$ from the input program.
	|	* create_qnm1.cpp - generation of $Q_{N-1}$ from the input program.
	|	* extract_peels.cpp - generation of $peel(P_N)$ from the input program.
	|	* diff_preds.cpp - incorporate the computed difference invariants in the analysis.
	|- diffy/src/bmc
	|	* Translation of LLVM IR to SMT formulas and inductive verification APIs.
	|	* array_model.cpp - modeling the arrays in llvm ir for creating the bmc formula.
	|	* glb_model.cpp - modeling global variables in llvm ir for creating the bmc formula.
	|	* witness.cpp - generation of the witness when the property can be violated.
	|	* bmc_ds.cpp - data structure classes for storing information while translating to bmc. 
	|	* bmc_pass.cpp - base class for translating the input to a bmc formula.
	|	* bmc_fun_pass.cpp - sub-class of bmc_pass, runs initialization for each function.
	|	* bmc_loop_pass.cpp - sub-class of bmc_pass, runs initialization for each loop a function.
	|	* bmc.cpp - class that defines APIs to execute the bmc pass and access varied information. 
	|	* bmc_llvm_aggr.cpp - implements the inductive verification using smt solving, it checks
	|	* the base-case, inductive case and computes Dijkstra's weakest pre-condition.
	|- diffy/src/irtoz3expr
	|	* Create smt expressions corresponding to LLVM IR expressions and store them for later use.
	|	* irtoz3expr.cpp - defines APIs for converting ir to smt before bmc translation is invoked.
	|- diffy/src/utils
	|	* Utilities for manipulating the LLVM IR, Z3 expressions and parsing parameter options.
	|	* llvmUtils.cpp - APIs and classes for analyzing and manipulating the llvm ir of the input program.
	|	* z3Utils.cpp - APIs for manipulating the z3 expressions created while analyzing the input program.
	|	* options.cpp - parse the parameters passed to the tool and store them appropriately.
	|- diffy/cav21-bench/
	|	* Safe & unsafe benchmarks used during the experimentation for CAV 2021.
	|- diffy/additional-bench/
	|	* Additional benchmark programs for experimentation beyond those in the paper.
	|- diffy/logs-cav21-expts/
	|	* Log files generated during the experiments for CAV 2021.
	|	* File and directory names are indicative of the content.
	|- storage/
	|	* Shared directory to copy content between host machine and docker container.
	|- DIFFY_LICENSE
	|	* License file for the tool.
	|- Dockerfile
	|	* Docker script for building the container.
	|- README.md
	|	* Readme file describing the contents of the artifact and the evaluation procedure.

==================

The source code, benchmarks and compiled executable files are permanently available in the following archives:

figshare

GitHub

==========

This work is licensed under the MIT License - see the LICENSE file for details.

===========

[1] Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat. "Diffy: Inductive Reasoning of Array Programs using Difference Invariants." International Conference on Computer-Aided Verification (CAV). 2021.

[2] Supratik Chakraborty, Ashutosh Gupta, and Divyesh Unadkat. "Verifying Array Manipulating Programs with Full-Program Induction." International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2020.

[3] Mohammad Afzal, et al. "Veriabs: Verification by abstraction and test generation (competition contribution)." International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 2020.

[4] Pritom Rajkhowa, and Fangzhen Lin. "VIAP 1.1." International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS). 2019.

===========

Write to us for any issues, queries, suggestions and feedback. We are continuously working to make our algorithms and implementation better, faster and more robust.

===================

We thank all the reviewers for taking time to evaluate our artifact. We appreciate your effort and feedback.