Backends.txt

                               Symbolic backends


We support different symbolic backends; currently, we have our own backend,
which is a custom thin wrapper around Z3, and the QSYM backend. Users choose
with a build option which backend to use. This file documents the internals of
this mechanism.

At compile time, we always insert the same calls, no matter which backend is
used. Also, we always link against "libSymRuntime.so", so the choice of backend
is deferred until run time. From the target program's point of view, the only
requirement on a backend is that it be a shared library with the expected name
that implements the interface defined in runtime/RuntimeCommon.h (with type
"SymExpr" defined to be something of pointer width).

Depending on the build option QSYM_BACKEND we build either our own backend or
parts of QSYM (which are pulled in via a git submodule) and a small translation
layer. The code used by both backends is in the directory "runtime", while the
specific parts are in "runtime/simple" and "runtime/qsym".

The QSYM backend expects to be passed the program counter at each jump
instruction, which is used to uniquely identify the jump site and implement a
per-site back-off mechanism. However, there is no reason for the supplied value
to be the program counter as long as it is a unique identifier. Since it is
somewhat challenging to obtain the current program counter in our
compilation-based setting, we follow an alternative approach: in the compiler
pass, we identify each jump site by the address of the LLVM object that
represents the instruction; experiments suggest that it is a good enough
identifier. This value is embedded into the target program as a constant and
passed to the backend at run time.

Before compiling the QSYM code, we are expected to execute two Python scripts
that the QSYM authors use for code generation; two custom CMake targets take
care of running the scripts and tracking changes to the relevant source files.