DIVINE: Extended Compilation-based Symbolic Verification (competition contribution)

Authors: Zuzana Baranová, Lukáš Korenčik, Henrich Lauko, Adam Matoušek, Vladimír Štill, Petr Ročkai
Abstract:

DIVINE is an explicit-state model checker based on the LLVM framework with a focus on real-world C and C++ programs. Verification in DIVINE covers a wide variety of aspects of these languages like concurrency, memory safety, verification of programs with exceptions as well as programs that interact with an operating system, including file system and POSIX syscalls. Furthermore, these programs usually interact with their environment and obtain nondeterministic values. In DIVINE, we tackle data nondeterminism via symbolic computation that is instrumented into the original program on the level of LLVM bitcode. Using this approach, we limit modifications of DIVINE’s internal interpreter which can remain purely explicit.

Up till now, DIVINE was able to instrument an abstraction of scalar integers. This year we have enriched DIVINE’s abilities by instrumentation of floating-point values abstraction. Moreover, we present instrumentation for array abstractions, which allows DIVINE to allocate symbolically large arrays and compete on a broader set of benchmarks.

This page corresponds to the submission of DIVINE to SV-COMP 2020.

Installation

DIVINE should work on any reasonably recent Linux distribution. It might also be possible to make it work on macOS, *BSD or even on Windows using Windows Subsystem for Linux, but this is not tested routinely.

Binary Distribution

The binary distribution is intended for SV-COMP and therefore should work on Ubuntu 18.04. However, as a binary distribution, it might not work on other Linux distributions or even on Ubuntu due to updates.

To use it, it is sufficient to extract the archive. Then run ./divine help in the main archive directory. If this succeeds (gives you a list of commands), you should be good to go with the binary distribution, if not, you should build DIVINE from the sources as your system is not compatible with the SV-COMP archive.

Building from Source

To build from the source, you will need some prerequisites, namely a C++11 compiler such as reasonably recent GCC (>= 4.9) or Clang (>= 3.2), make, CMake (>= 3.2), libedit, perl, and about 12GB of disk space and 4GB or RAM. For the symbolic verification to work as in SV-COMP, you will also need the Z3 solver, including its libraries.

You should extract the archive and then run make divine in its main directory. This should build DIVINE into _build.release/tools subdirectory by default. For more details, please refer to the manual.

Usage

If you use the binary distribution, both the SV-COMP wrapper (divine-svc) and the main DIVINE binary divine, are located in the divine-svc directory of the archive. If you have built DIVINE from the source, the wrapper resides in tools/divine-svc, while the built binary resides in _build.release/tools/divine.

In order to analyze an SV-COMP benchmark, you will also need a checkout of the SV-Benchmarks repository. Then you can analyze a benchmark as follows:

PATH_TO_DIVINE_WRAP/divine-svc PATH_TO_DIVINE_BIN PROPERTY.prop BENCHMARK.i

Where PATH_TO_DIVINE_WRAP is the path where divine-svc resides, PATH_TO_DIVINE_BIN is the path where the binary resides. The last line of the result should be the result given in SV-COMP.

Description of the Wrapper

The divine-svc wrapper handles translation from the SV-COMP property specification to DIVINE’s options and configuration based on some main features of the program.