Symbiotic is an open-source tool for finding bugs in sequential computer programs. It is based on three well-know techniques: instrumentation, static program slicing and symbolic execution. Symbiotic is highly modular and most of its components are self-standing programs of LLVM passes that have their own repositories at https://github.com/staticafi.
The archive used in SV-COMOP 2018 can be downloaded from https://gitlab.com/sosy-lab/sv-comp/archives/raw/svcomp18/2018/symbiotic.zip
Other tarballs with Symbiotic distribution (not updated reguralry) can be downloaded from https://github.com/staticafi/symbiotic/releases After unpacking, Symbiotic is ready to go.
You can use also the docker image:
docker pull mchalupa/symbiotic docker run -ti mchalupa/symbiotic
Building Symbiotic from Sources
First of all you must clone the repository:
$ git clone https://github.com/staticafi/symbiotic
The build script of Symbiotic uses
cmake, so make sure
you have them installed (the script will complain otherwise).
STP theorem prover further needs
flex and minisat needs
These components are needed when building KLEE. However, if you do not want to
build Symbiotic with KLEE (and therefore with STP and minisat), then you can comment
these components out in the build script (there is no switch for not building these
If you have all the dependencies, you are ready to run the
$ cd symbiotic $ ./build.sh -j2
And that should be it! However, if something goes wrong or you need to adust the build process, you can pass different options to the build script. Possible options include:
build-type=TYPE(TYPE one of
3.9.1, other versions are rather experimental)
with-llvm-dir=This set of options orders the script to use already built external LLVM (the build script will build LLVM otherwise if it has not been built already in this folder)
with-zlibBuild also zlib
no-llvmDo not try building LLVM
binStart building Symbiotic from this point
As you can see from the example, you can pass also arguments for make, e.g.
-j2, to the build script.
If you need to specify paths to header files or libraries, you can do it
CPPFLAGS, LDFLAGS environment variables either by exporting
them beforehand, or by passing them as make options (e.g.
If everything goes well, Symbiotic components are built and also installed
install/ directory that can be packed or copied wherever you need.
This directory is under
git control, so you can see the differences between
versions or make an archive using
git archive command.
There is a known problem that can arise while building KLEE:
llvm-config: error: missing: /home/mchalupa/src/symbiotic/llvm-3.9.1/build/lib/libgtest.a llvm-config: error: missing: /home/mchalupa/src/symbiotic/llvm-3.9.1/build/lib/libgtest_main.a CMake Error at cmake/find_llvm.cmake:62 (message): Failed running /home/mchalupa/src/symbiotic/llvm-3.9.1/build/bin/llvm-config;--system-libs Call Stack (most recent call first): cmake/find_llvm.cmake:163 (_run_llvm_config) lib/Basic/CMakeLists.txt:19 (klee_get_llvm_libs)
This is due to b5cd41e2 commit in LLVM. Until we have this fixed, the fastest workaround is to just create empty files
build/lib/libgtest_main.a in the LLVM's folder.
When building on mac, you may need to build LLVM with shared libraries
(modify the build script) or use
with-llvm-* switch with your LLVM build.
You can run Symbiotic directly from the root directory:
scripts/symbiotic <OPTIONS> file.c
Alternatively, you can run Symbiotic also from the install directory:
$ install/bin/symbiotic <OPTIONS> file.c
In the case that something went wrong, try running Symbiotic with
is one of:
When the source code does not contain everything to compile (i.e. it includes
some headers), you can use
CPPFLAGS environment variables to
pass additional options to the compiler (clang). Either export them before
running Symbiotic, or on one line:
CPPFLAGS='-I /lib/gcc/include' scripts/symbiotic file.c
You can also use
--cppflags switch that works exactly the same as environment variables.
If the program is split into more files, you can give Symbiotic all the files.
At least one of them must contain the 'main' function.
scripts/symbiotic main.c additional_definitions.c lib.c
--help switch to see all available options.
Components of Symbiotic can be found at https://github.com/staticafi with the
only exception of
dg library that is currently at https://github.com/mchalupa/dg.
All sowtware used in Symbiotic are open-source projects and are licensed under various
open-source licenses (mostly MIT license, Apache-2.0,
and University of Illinois Open Source license)
For more information send an e-mail to email@example.com.