Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them hence the program can be processed by a tool without support for symbolic manipulation.
The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend.
- full text (pdf, revision 1, 26.5.2018)
Installation
A source tarball of the version evaluated in the paper is available. For information on building and installing DIVINE from the tarball, please refer to the manual.
Alternatively, a prebuilt static binary for x84-64 Linux is available here: divine-4.1.5+2018.05.29.
Evaluation and Benchmarks
For evaluation, we have used the tools described in the following sections.
DIVINE + the transformation from the paper
- a developement version included with this paper (see Installation)
- using the following options:
--symbolic -o nofail:malloc -o ignore:arithmetic - certain SV-COMP benchmarks contain bugs unrelated to the their primary property, in those cases,
-o ignore:controlwas also used - the option
--sequentialfor sequential benchmarks - detailed results for the tool are located here: divine.md
SymDIVINE
- in version 0.5: https://github.com/paradise-fi/SymDIVINE
- to run benchmarks, we used helper script
scripts/run_symdivine.pyshipped with the tool - detailed results for the tool are located here: symdivine.md
CBMC
- in version 5.8: http://www.cprover.org/cbmc
- with no additional arguments (only the C source file and where required,
-Doptions for the preprocessor were passed tocbmc) - detailed results for the tool are located here: cbmc.md
For benchmarking, we have used a subset of the SV-COMP test cases, namely 7 categories, sumarized in the comparison section. We have only taken examples with finite state spaces since the simple approach outlined in the paper cannot handle infinite recursion or infinite accumulation loops. In total, we have selected 1160 SV-COMP inputs. The whole set of benchmarks is available from here: benchmarks.zip.
Comparison
The number of benchmarks correctly solved by each of the evaluated tools. The
best result in each category is rendered in boldface.
| category | total | DIVINE* | SymDIVINE | CBMC |
|---|---|---|---|---|
| array | 190 | 96 | 68 | 93 |
| bitvector | 32 | 17 | 9 | 2 |
| loops | 178 | 72 | 67 | 9 |
| product-lines | 575 | 336 | 411 | 234 |
| pthread | 45 | 9 | 0 | 1 |
| recursion | 81 | 47 | 43 | 22 |
| systemc | 59 | 14 | 27 | 0 |
| total | 1160 | 591 | 625 | 361 |
Time Comparison
We have compared benchmarks on which both tools have finished. Both axes in the plots are in seconds.
DIVINE compared to SymDIVINE:
DIVINE compared to CBMC:
State-space Comparison
We have only compared SymDIVINE and DIVINE regarding the size of state spaces, because CBMC does not build an explicit state space.
