Authors: Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, Vladimír Štill
Abstract:

The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built on an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.

Documents:

Download

DIVINE can be downloaded from the links below. These links reflect the state of DIVINE at the time of the finalization of this paper.

Usage

Apart from the short guide included in the paper, there is a longer and more elaborate guide in the manual.

Example Programs

Here you can find some commented example programs which demonstrate features of DIVINE. Below, you will find pointers to additional, more complex examples.

Simple Memory Access Error

#include <cstdio>
#include <cassert>

void foo( int *array ) {
    for ( int i = 0; i <= 4; ++i ) {
        printf( "writing at index %d\n", i );
        array[i] = 42;
    }
}

int main() {
    int x[4];
    foo( x );
    assert( x[3] == 42 );
}

[download]

$ divine verify memory.c

This code demonstrates DIVINE’s ability to uncover an invalid access to a stack variable (array x). It also shows that traces produced by DIVINE contain strings that the program wrote to the standard output and the error output.

Constant Memory Write Error

#include <stdio.h>

const int x = 0;
const int y = 42;
int z = 10;

void foo( int *val ) {
    printf( "foo got val %d\n", *val );
    *val = 16;
    printf( "val set to %d\n", *val );
}

int main() {
    foo( &z );
    foo( &y );
    foo( &x );
}

[download]

$ divine verify constants.c

In this code, we can see that DIVINE can detect attempts to write into constant memory.

Simple C++ Threading

#include <cstdio>
#include <cassert>
#include <thread>

int main() {
    int x = 0;
    puts( "starting thread" );
    std::thread t1( [&] {
        puts( "thread started" );
        ++x;
        puts( "thread done" );
    } );
    puts( "incrementing" );
    ++x;
    puts( "waiting for the thread" );
    t1.join();
    puts( "thread joined" );
    assert( x == 2 );
}

[download]

$ divine verify -std=c++11 -o nofail:malloc thread.cpp

This program demonstrates that C++11 threads are supported in DIVINE. There is a data race between the two increment operations on x. Please note that -o nofail:malloc is used to suppress fault injection in memory allocation (std::thread allocates memory for passing arguments to the created thread; it would be also possible to solve this problem in the program by catching an exception of type std::bad_alloc).

Uninitialised Value Detection

#include <stdio.h>
#include <pthread.h>

void *thread( void *state ) {
    puts( "thread is running" );
    int *x = state;
    if ( *x == 0 )
        puts( "x is zero" );
    else if ( *x == 1 )
        puts( "x is one" );
    else
        puts( "x is neither zero nor one" );
    puts( "thread is done" );
    return NULL;
}

int main() {
    puts( "entering main" );
    pthread_t tid;
    int x;
    puts( "going to create thread" );
    pthread_create( &tid, NULL, thread, &x );
    puts( "thread created" );
    x = 1;
    puts( "initialized x, going to wait for the thread" );
    pthread_join( tid, NULL );
    puts( "thread finished, exiting" );
}

[download]

$ divine verify undef.c

In this program, DIVINE detects use of an uninitialised value in a conditional statement. Here, the error is caused by a data race that results in a read of an uninitialised value (x) at line 7.

pthreads Deadlock Detection

#include <stdio.h>
#include <pthread.h>
#include <assert.h>

pthread_mutex_t mtx1 = PTHREAD_MUTEX_INITIALIZER,
                mtx2 = PTHREAD_MUTEX_INITIALIZER;

int x;

void *thr1( void *_ ) {
    puts( "1: locking mutex 2" );
    pthread_mutex_lock( &mtx2 );
    puts( "1: locking mutex 1" );
    pthread_mutex_lock( &mtx1 );
    ++x;
    puts( "1: unlocking mutex 1" );
    pthread_mutex_unlock( &mtx1 );
    puts( "1: unlocking mutex 2" );
    pthread_mutex_unlock( &mtx2 );
    return _;
}

int main() {
    pthread_t t1;

    pthread_create( &t1, NULL, thr1, NULL );

    puts( "0: locking mutex 1" );
    pthread_mutex_lock( &mtx1 );
    puts( "0: locking mutex 2" );
    pthread_mutex_lock( &mtx2 );
    ++x;
    pthread_mutex_unlock( &mtx2 );
    puts( "0: unlocking mutex 2" );
    pthread_mutex_unlock( &mtx1 );
    puts( "0: unlocking mutex 1" );

    pthread_join( t1, 0 );

    assert( x == 2 );
}

[download]

$ divine verify deadlock.c

This is an example of a program which contains a deadlock caused by improper use of pthread mutexes.

Further Examples

Some further examples can be found in DIVINE’s testsuite (in the test directory in DIVINE sources). For example test/cpp/2.fifo-bug.cpp is a unit test of a parallel reader-writer queue which was used in DIVINE 3 and in which DIVINE discovered an error (fixed version is in test/cpp/2.fifo.cpp).

Another nice example is a unit test of the parallel hash table used in DIVINE: hashset.zip. In this case, the program also contains headers and can use preprocessor macros for configuration. Therefore, it is better to use DIVINE’s compiler (divine cc) to compile the program to LLVM IR first. It can be compiled and verified using the following commands (in the directory with the test):

$ divine cc -I. -std=c++14 -o testcase.bc -DITEMS=5 -DCHECK=1 hashset.cpp
$ divine verify -o nofail:malloc testcase.bc

(Memory allocation failure simulation is disabled as the hashset is not supposed to be resilient to memory exhaustion).

  1. Windows Subsystem for Linux (WSL, also known as Bash on Windows) allows you to run Linux binaries on Windows 10, please refer to https://msdn.microsoft.com/en-us/commandline/wsl/install_guide for installation instructions. Once you have WSL installed, it should be sufficient to run bash, download DIVINE binary using wget https://divine.fi.muni.cz/2017/divine4/divine && chmod +x divine and then run ./divine.↩︎