If you have the soid Docker image, to get started with it you'll need to install both the Docker Engine and the Docker Compose plugin. You can then just load the image, download docker-compose.yml (no need to clone the whole repository), and run the appropriate docker compose run ... command below.
To run the GUI, do:
$ docker compose run soid-guiAfter initialization, the GUI is available from the host at localhost:3000. If the GUI complains about not having access to a display, you might need to install xvfb on the host machine, and do
$ Xvfb :0 -screen 0 1024x768x24 -ac +extension GLX +render -noreset &> xvfb.log &
$ export DISPLAY=:0
$ docker compose run soid-guiinstead. You can also spin up the hardcoded broadside crash scenario from the paper with
$ docker compose run soid-gui-crashas well.
To work directly with soid, or to modify the GUI, you first need to spin the image up, and then get a shell.
$ docker compose run soidOnce in the container there is a minimal development environment, so to edit files you may need to do, e.g.:
$ apt-get update && apt-get emacs-noxto get Emacs, or equivalently for Vim or otherwise. If you want to launch the GUI from inside the image, just run
$ ./usr/src/soid/examples/gui/duckietown-soid/launchfor the normal scenario or
$ ./usr/src/soid/examples/gui/duckietown-soid/launch -cfor the crash.
First you'll need to clone the repository with submodules:
$ git clone --recurse-submodules -j8 git@github.com:sjudson/soid.gitThen, run on debian/ubuntu:
$ sudo apt-get install -y build-essential \
wget \
curl \
libcap-dev \
git \
cmake \
libncurses5-dev \
python2-minimal \
unzip \
libtcmalloc-minimal4 \
libgoogle-perftools-dev \
libsqlite3-dev \
doxygen \
python3 \
python3-pip \
python3-dev \
virtualenv \
gcc-multilib \
g++-multilib \
z3 \
clang-11 \
llvm-11 \
llvm-11-dev \
llvm-11-tools \
m4 \
bison \
flex \
bc \
libboost-dev \
unzip \
libtool \
freeglut3-dev \
libglib2.0-0 \
libsm6 \
libxrender1 \
libxext6 \
libgl1-mesa-glx \
ffmpeg \
npm \
xvfb \
mesa-utilsAfter this completes, all that is left is to run the dependency install script from within the deps folder of the soid repo:
$ ./install-deps
This will a) setup a Python virtualenv with the necessary dependencies installed, b) build klee-uclibc and klee for non-floating point analysis, and c) build llvm3.4, another version of klee-uclibc, and klee-float for floating point analysis. It can take some time to run, but has very verbose output throughout the install process.
Additionally, it takes two options. First, llvm3.4 can have issues finding a gcc install on the host machine, so it may be necessary to specify an exact path. For example, you may need to do something like
$ ./install-deps -g /usr/lib/gcc/x86_64-linux-gnu/10
or alternatively --gcc-path to get everything to build successfully. Also, you can run
$ ./install-deps -c
or alternatively --with-cvc5 to also get a build of cvc5, for some synthesis functionality as yet not yet fully implemented into soid.
To run soid, first enable the virtual environment created by the install, by
$ source ./deps/venv/bin/activate
Then invoke the soid tool using the cli interface, specifying the source program makefile -m and the directory containing the python module with the queries -qs, e.g.,:
$ ./scripts/soidcli -m ./examples/other/car/defensive/Makefile -qs ./examples/other/car/queries
will execute the car example.
Soid current takes four options:
-m,--make: the location of the source program makefile, defaults to./Makefile.-p,--path: an alias for-mfor symbolic execution engines that do not use makefiles.-qs,--queries: the location of the queries formulated as a python package, defaults to./.-se,--symbexec: symbolic execution engine, only 'klee' (the default) is supported.