Data-Driven Loop Bound Learning for Termination Analysis

Rongchen Xu, Jianhui Chen, and Fei He

Abstract

Termination is a fundamental liveness property for program verification. A loop bound is an upper bound of the number of loop iterations for a given program. The existence of a loop bound evidences the termination of the program. We employ a reinforced black-box learning approach for termination proving, consisting of a loop bound learner and a validation checker. We present efficient data-driven algorithms for inferring various kinds of loop bounds, including simple loop bounds, conjunctive loop bounds, and lexicographic loop bounds. We also devise an efficient validation checker by integrating a quick bound checking algorithm and a two-way data sharing mechanism. We implemented a prototype tool called ddlTerm. Experiments on publicly accessible benchmarks show that ddlTerm outperforms state-of-the-art termination analysis tools by solving 13-48% more benchmarks and saving 40-77% solving time.

Artifact

The docker image contains all scripts, source code and benchmarks in our evaluation.

Install

Docker

Follow the installation documents

Use the file ddlTerm.dockerfile in docker to build the image

 docker build --no-cache -f docker/ddlterm.dockerfile -t ddltermartifact:latest docker

Except 2, you can download the built docker image directly. Then:
```
 docker load -i ddltermartifact.tar
```

Linux

We tested the following procedure on Ubuntu 18.04.

Install the Mono environment

Install python3, gcc/g++, make and the necessary pip packages

 apt install -y gcc g++ make python3 python3-pip
 pip install pandas scipy sklearn antlr4-python3-runtime xlsxwriter

Build Boogie in ice/popl16_artifact/Boogie/Source
```
 msbuild Boogie.sln
```
Build C5.0 in ice/popl16_artifact/C50
```
 make clean; make all
```
- Then, copy all generated c5.0.* into ice/popl16_artifact/Boogie/Binaries
Download z3 4.8.9 from Github

Unzip the zip file, copy the inside bin/z3 into ice/popl16_artifact/Boogie/Binaries and rename it to z3.exe

Run Experiments

Docker

Start the docker image (replace /path/to/a/directory/to/save/the/result)

 docker run -it -v /path/to/a/directory/to/save/the/result:/log --tmpfs /tmpfs --cpus=1 ddltermartifact:latest

Run the experiments (e.g. the main experiment in our paper)

 cd ddlTerm
 python3 experiment/scripts/RunTasks.py experiment/scripts/configurations/ExpMain/LeNLeMixed_Standard.xml

Linux

Please update the configuration XML file in experiment/scripts/configurations before the experiments.

 <!-- A path to tmp directory -->
 <Tmp>/tmpfs</Tmp>
 <!-- A path to output result directory -->
 <Log_Dir>/log</Log_Dir>

Run the experiments (e.g. the main experiment in our paper)

 cd ddlTerm
 python3 experiment/scripts/RunTasks.py experiment/scripts/configurations/ExpMain/LeNLeMixed_Standard.xml

For a precise result, we suggest:

using tmpfs to reduce the time of IO. (By default, tmpfs has been used in docker running)
updating the timeout setting in configuration XML files according to performance of your machine.
setting the cpu limit to one core using cgroup. (By default, cpu limit has been used in docker running)

Baselines in Our Paper

If you want to make a comparative experiment, please follow the install instruments for our baseline tools.

Notes:

Remember to set the cpu limit to one core using cgroup or by the parameter --cpus if using docker.
The benchmarks locate in experiment/benchmarks.
- C-style can be used for AProVE, Ultimate Automizer and MuVal.
- Horn-style can be used for FreqTerm.
We provide some useful scripts in experiment/baseline.scripts to run the experiments for AProVE, Ultimate Automizer and FreqTerm. You can modify the path in the scripts to run these tools. We hope these scripts are useful for you.

Licenses

The safety validator from ICE-DT (locates in ice/popl16_artifact) follows Microsoft Public License (MS-PL). The benchmarks from FreqTerm follows Seahorn License. The other part of our repository follows Apache License 2.0.