Authors: Petr Ročkai, Jiří Barnat

Abstract:

In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples.

Documents:

full text (pdf, revision 1, 2021-01-01)

Source Code

The source code which has been used for the evaluation in the paper is available here: divine-4.4.2+divsim.tar.gz. This tarball also includes the 3rd-party Qt-based graphical user interface. Unfortunately, the code does not work correctly with current version of the Qt toolkit (fix pending).

The testcases used in Section 8 (Evaluation) of the paper are under the test directory, each category (described in the paper) corresponding to a single subdirectory in the tarball. Testcases tagged todo (in the comments near the top of each file) and those in directories cc, dioscc, draw, lart, leak, liveness, misc, pdclib, sim and verify have been excluded, mainly due to their limited relevance to the simulator.

Build Instructions

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 the _build.release/tools subdirectory by default. For more details, please refer to the manual.

Running the Simulator

The binary can be executed directly from the build directory and does not need to be installed. The simulator is available as divine sim. See divine help sim for detailed help on command line options. The most common invocations are:

to explore a stand-alone C or C++ program: divine sim program.c,
to load a counterexample: divine sim --load-report program.report (the report can be obtained by running divine check program.c).

Suitable test programs can be found, for instance, in the directory test/demo.

Bundled GUI

TODO: Add instructions to build and run the bundled version of the GUI once the code is fixed to work with Qt 5.15+.

GUI (Upstream Version)

The original version, as published by Vojtěch Frnoch, the author of the user interface, is available as well: divsim-gui.tar.gz. The following instructions were provided by the author.

Requirements:

A POSIX-compatible operating system.
The program make.
GNU C++ 7.3.1 or compatible.
CMake 3.2 or compatible.
GraphViz 2.4 or compatible.
The library libedit.
Qt 5.10 or compatible.
KF5SyntaxHighlighting version 5.44 or compatible.

Instructions:

Extract the tarball and enter the newly created directory divine.
Open a terminal there.
Run make.
Enter the directory divine/gui.
Run cmake CMakeLists.txt.
Run make.
Change into ../../_build.release.gui.
Run the program as ./gui.

Example Transcript

Below is a 1:1 reproduction of an example session (using one of the test programs bundled with the source code). The command prompt of divine sim is marked with >. The configuration file ~/.divine/sim.init in this case contains setup --sticky source which causes the source code of the currently executing function to be shown after each command.

Hitting enter at the prompt without typing a command repeats the last command (i.e. step in the example below).

$ divine check test/demo/undef.c
compiling test/demo/undef.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 483.871
state count: 15
mips: 2.3

error found: yes
error trace: |
  [0] entering main
  [0] going to create thread
  [1] thread is running
  FAULT:  conditional jump depends on an undefined value
  [1] FATAL: control error in userspace

active stack:
  - symbol: void __dios::FaultBase::handler<__dios::Context>(_VM_Fault, _VM_Frame*, void (*)())
    location: /dios/sys/fault.hpp:119
  - symbol: thread
    location: test/demo/undef.c:7
  - symbol: __pthread_start
    location: /dios/libc/pthread/pthread-init.cpp:79
  - symbol: __pthread_entry
    location: /dios/libc/pthread/pthread-core.cpp:50
a report was written to undef.report

$ divine sim --load-report undef.report
compiling test/demo/undef.c

           ^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
          ———      |     |   |   |     |   |   |\    |  |         |    |
         —(o)—     |     |   |   |     |   |   |  \  |  |————     '————|
        ———————    |     |   |    \   /    |   |    \|  |              |
       —————————   —————'   —'—     '     —'—  '     '  '—————         '

Welcome to 'divine sim', an interactive debugger. Type 'help' to get started.
T: [0] entering main
T: [0] going to create thread
▶ state    #5 [new] -- active threads: 0:0 [0:1] --
T: [1] thread is running
T: FAULT:  conditional jump depends on an undefined value
      4 void *thread( void *state ) {
      5     puts( "thread is running" );
      6     int *x = state;
>>    7     if ( *x == 0 ) /* ERROR */
      8         puts( "x is zero" );
      9     else if ( *x == 1 )
     10         puts( "x is one" );
     11     else
     12         puts( "x is neither zero nor one" );
     13     puts( "thread is done" );
     14     return NULL;
     15 }
# executing void __dios::FaultBase::handler<{Context}>(_VM_Fault, _VM_Frame*, void (*)())
#        at /dios/sys/fault.hpp:119
# NOTE: $frame in thread
> start
▶ state    #1 [cex] -- active threads: [0:0] --
     17 int main() {
>>   18     puts( "entering main" );
     19     pthread_t tid;
     20     int x;
     21     puts( "going to create thread" );
     22     pthread_create( &tid, NULL, thread, &x );
     23     puts( "thread created" );
     24     x = 1;
     25     puts( "initialized x, going to wait for the thread" );
     26     pthread_join( tid, NULL );
     27     puts( "thread finished, exiting" );
     28 }
# executing main at test/demo/undef.c:17
> step
  %01 = alloca [i32 1 d]                                                        # [alloca* 87582d7 0 ddp]
  %02 = alloca [i32 1 d]                                                        # [alloca* 96d518e 0 ddp]
     17 int main() {
>>   18     puts( "entering main" );
     19     pthread_t tid;
     20     int x;
     21     puts( "going to create thread" );
     22     pthread_create( &tid, NULL, thread, &x );
     23     puts( "thread created" );
     24     x = 1;
     25     puts( "initialized x, going to wait for the thread" );
     26     pthread_join( tid, NULL );
     27     puts( "thread finished, exiting" );
     28 }
# executing main at test/demo/undef.c:18
>
  %03 = call @puts [global* 6 0 ddp]                                            # [i32 0 u]
T: [0] entering main
     17 int main() {
     18     puts( "entering main" );
     19     pthread_t tid;
     20     int x;
>>   21     puts( "going to create thread" );
     22     pthread_create( &tid, NULL, thread, &x );
     23     puts( "thread created" );
     24     x = 1;
     25     puts( "initialized x, going to wait for the thread" );
     26     pthread_join( tid, NULL );
     27     puts( "thread finished, exiting" );
     28 }
# executing main at test/demo/undef.c:21
>
  %06 = call @puts [global* 7 0 ddp]                                            # [i32 0 u]
T: [0] going to create thread
     17 int main() {
     18     puts( "entering main" );
     19     pthread_t tid;
     20     int x;
     21     puts( "going to create thread" );
>>   22     pthread_create( &tid, NULL, thread, &x );
     23     puts( "thread created" );
     24     x = 1;
     25     puts( "initialized x, going to wait for the thread" );
     26     pthread_join( tid, NULL );
     27     puts( "thread finished, exiting" );
     28 }
# executing main at test/demo/undef.c:22
>
  %08 = call @pthread_create %01 [global* 0 0 ddn] thread %07                   # [i32 0 u]
▶ state    #2 [cex] -- active threads: 0:0 [0:1] --
▶ state    #3 [cex] -- active threads: 0:0 [0:1] --
      4 void *thread( void *state ) {
>>    5     puts( "thread is running" );
      6     int *x = state;
      7     if ( *x == 0 ) /* ERROR */
      8         puts( "x is zero" );
      9     else if ( *x == 1 )
     10         puts( "x is one" );
     11     else
     12         puts( "x is neither zero nor one" );
     13     puts( "thread is done" );
     14     return NULL;
     15 }
# executing thread at test/demo/undef.c:5
> step
  %07 = call @puts [global* 1 0 ddp]                                            # [i32 0 u]
▶ state    #4 [cex] -- active threads: [0:0] 0:1 --
     17 int main() {
     18     puts( "entering main" );
     19     pthread_t tid;
     20     int x;
     21     puts( "going to create thread" );
     22     pthread_create( &tid, NULL, thread, &x );
>>   23     puts( "thread created" );
     24     x = 1;
     25     puts( "initialized x, going to wait for the thread" );
     26     pthread_join( tid, NULL );
     27     puts( "thread finished, exiting" );
     28 }
# executing main at test/demo/undef.c:23
> step
  %09 = call @puts [global* 8 0 ddp]                                            # [i32 0 u]
▶ state    #5 [cex] -- active threads: 0:0 [0:1] --
T: [1] thread is running
      4 void *thread( void *state ) {
      5     puts( "thread is running" );
      6     int *x = state;
>>    7     if ( *x == 0 ) /* ERROR */
      8         puts( "x is zero" );
      9     else if ( *x == 1 )
     10         puts( "x is one" );
     11     else
     12         puts( "x is neither zero nor one" );
     13     puts( "thread is done" );
     14     return NULL;
     15 }
# executing thread at test/demo/undef.c:7