Authors: Henrich Lauko, Lukáš Korenčik, Petr Ročkai
Abstract:

Most C and C++ programs use dynamically allocated memory (often known as a heap) to store and organize their data. In practice, it can be useful to compare addresses of different heap objects, for instance, to store them in a binary search tree or a sorted array. However, comparisons of pointers to distinct objects are inherently ambiguous: the address order of two objects can be reversed in different executions of the same program, due to the nature of the allocation algorithm and other external factors.

This poses a significant challenge to program verification since a sound verifier must consider all possible behaviors of a program, including an arbitrary reordering of the heap. A naive verification of all possibilities, of course, leads to a combinatorial explosion of the state space: for this reason, we propose an under-approximating abstract domain which can be soundly refined to consider all relevant heap orderings.

We have implemented the proposed abstract domain and evaluated it against several existing software verification tools on a collection of pointer-manipulating programs. In many cases, existing tools only consider a single fixed heap order, which is a source of unsoundness. We demonstrate that using our abstract domain, this unsoundness can be repaired at only a very modest performance cost. Additionally, we show that, even though many verifiers ignore it, ambiguous behavior is present in a considerable fraction of programs from software verification competition.

Documents:

This page corresponds to the submission of ACM TOSEM 2021 paper.

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.

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 RAM.

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.

Abstract Domain

The abstraction implementation is located at divine/dios/lava/pointer_arithmetic.hpp and the hierarchy configuration at divine/dios/lamp/pointers.cpp

Refinement

To run the program refinement, you can use the following command. The destination of refined bitcode needs to be specified as a parameter of --output-bc option:

$ divine refine --refinement pointers -o nofail:malloc --output.bc refined.bc program.c

To verfify the refined program, you can run arbitrary analysis that DIVINE provides. You just have to provide specify abstraction configuration. The configuration of PA domain used in the evalution is provided as --lamp pointers option, e.g.:

$ divine check --lamp pointers refined.bc

Benchmarks

Tool Limitations (benchmarks.tar.gz)

Used versions of tools in the evaluation with invocation parameters:

2LS

Invocation: --pointer-check --heap-values-refine --k-induction --object-bits 11 test.c

CPAchecker

Invocation: -default -preprocess test.c

KLEE

Invocation: --exit-on-error test.bc

CBMC

Invocation: --stop-on-fail --pointer-check --stack-trace test.c

ESBMC

Invocation: --force-malloc-success test.c

Nidhugg

Invocation: -- -sc test.c

Predator

Invocation: --propertyfile reachability.prp --trace trace.predator -- test.c

Symbiotic

Invocation: --exit-on-error test.c

SV-COMP (benchmarks)