Solving CHCs over ADTs and RDFs

Artifact for Solving Constrained Horn Clauses modulo Algebraic Data Types and Recursive Functions

This page describes steps to reproduce empirical results from the paper titled “Solving Constrained Horn Clauses modulo Algebraic Data Types and Recursive Functions” (paper #629).

The paper can be found here. The empirical results are presented as Table 1 and Table 2 in section 8 (page 23) of the paper: Tables

Our algorithm is called Racer. In our paper, we called it ALG to respect the double blind review process. Another discrepancy between the paper and the artifact is that the tool VeriMAP in Table 2, is called adtrem in the artifact.

Our Results

The empirical results are presented as Table 1 and Table 2 in section 8 (page 23) of the paper. Table 1 compares our tool, Racer, with 3 other solvers (Spacer, Hoice, and Eldarica) on the rust-horn benchmark suite. Table 2 compares Racer with 4 other solvers (Spacer, Eldarica, CVC4 and VeriMAP) on the leon benchmark suite.

Steps to replicate experiment results:

Install docker

If you don’t already have docker, you will have to setup docker repository and install docker. The instructions can be found at the docker install page. For your convenience, we have copy pasted all the required commands for Ubuntu here:

sudo apt-get update
sudo apt-get install \
apt-transport-https \
  ca-certificates \
  curl \
  gnupg \
  lsb-release
curl -fsSL https://download.docker.com/linux/ubuntu/gpg | sudo gpg --dearmor -o /usr/share/keyrings/docker-archive-keyring.gpg
echo \
  "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/docker-archive-keyring.gpg] https://download.docker.com/linux/ubuntu \
 $(lsb_release -cs) stable" | sudo tee /etc/apt/sources.list.d/docker.list > /dev/null
sudo apt-get update
sudo apt-get install docker-ce docker-ce-cli containerd.io

If you are on windows or mac, please follow the instruction from the docker install page.

Pull image from docker cloud Run docker pull hgvk/chcmodadtrdf to pull the artifact image

Run short version of experiment to make sure that everything is working. Use the command
docker run --rm -ti hgvk/chcmodadtrdf:latest /bin/sh /popl22-ae/scripts/test.sh. This script will run all solvers on all benchmarks for 1 second each. This experiment will take ~30mins and print two tables on the command line. This is what we get as output for the trial run:

Run full experiment

docker run --rm -ti hgvk/chcmodadtrdf:latest /bin/sh to start the docker container
cd /popl22-ae/scripts && ./table1.sh and cd /popl22-ae/scripts && ./table2.sh to replicate the results. The first script should take around 6 hours and the second should take around 8 hours to finish. The scripts will save the output in directories /popl22-ae/rust-horn-experiment/ and /popl22-ae/leon-experiment/ respectively. The output of solver sol is named sol-op.txt. The summary of the results are stored in /popl22-ae/rust-horn-experiment/table1.txt and /popl22-ae/leon-experiment/table2.txt.

Contents of AE:

The artifact is a container. It contains everything required to replicate our experiment results:

Executables
Source code for Racer in /popl22-ae/racer
Benchmarks in /popl22-ae/benchmarks
The following scripts are in the /popl22-ae/scripts directory inside the container
- table1.sh
- table2.sh
- run-racer.sh
- run-spacer.sh
- run-eldarica.sh
- run-cvc4.sh
- run-adtrem.sh
- test.sh
- run-preprocessing.sh

Running pre-processing on benchmarks

The command /popl22-ae/scripts/run-preprocessing.sh dir will run our preprocessing steps on all .smt2 files in the directory dir and produce files with termabs-w-rf prefix in the same location. As explained in section 8, pre-processing happens in two phases. The first identifies horn clauses that encode RDFs and creates RDFs for each such horn clause. The second phase does term abstraction: for each argument of an uninterpreted predicate to which an RDF can be applied, add an additional argument to the uninterpreted predicate to store the result of applying the RDF on the argument. The second phase then modifies horn clauses as necessary to keep track of the new arguments.

Running Racer on your own benchmarks

To run Racer on benchmarks not included with the artifact, do

Map benchmark directory to a directory inside the docker container Run docker with the option -v /path/to/bench/:/hostBench/ to map the directory /path/to/bench in the host machine to /hostBench in the docker container. The full command is

docker run -rm -ti -v /path/to/bench/:/hostBench/ hgvk/chcmodadtrdf:latest /bin/sh

Optionally, run preprocessing from inside docker using the command /popl22-ae/scripts/run-preprocessing.sh /hostBench. This will create a new benchmark in the same directory

Run Racer using the command /popl22-ae/scripts/run-racer.sh /hostBench/termabs-w-rf-bench.smt2

Artifact for Solving Constrained Horn Clauses modulo Algebraic Data Types and Recursive Functions

Our Results

Steps to replicate experiment results:

Contents of AE:

Running pre-processing on benchmarks

Running Racer

Running Racer on your own benchmarks

Looking at our results

Trending Tags