Windows | Ubuntu | OS X | Chat with us | Coverage |
---|---|---|---|---|
TBD | TBD |
SeaHorn is an automated analysis framework for LLVM-based languages. This version supports LLVM 5.0.
This master
branch is obsolete and not maintained anymore. We plan to replace it soon.
Meanwhile, the development/active branch is dev10
which supports LLVM 10.
SeaHorn is distributed under a modified BSD license. See license.txt for details.
cd seahorn ; mkdir build ; cd build
(The build directory can also be outside the source directory.)cmake -DCMAKE_INSTALL_PREFIX=run ../
(Add-GNinja
to use the Ninja generator instead of the default one. Build types (Release, Debug) can be set with-DCMAKE_BUILD_TYPE=<TYPE>
.)cmake --build .
to build dependencies (Z3 and LLVM)cmake --build . --target extra && cmake ..
to download extra packagescmake --build . --target crab && cmake ..
to configure crab (ifextra
target was run)cmake --build . --target install
to build seahorn and install everything inrun
directory
Note that the install target is required!
The install target installs SeaHorn all of it dependencies under build/run
.
The main executable is build/run/bin/sea
.
Usually, compilation time with clang and lld linker are faster than other options on Linux. The magic cmake configuration line is something like the following:
cmake -DCMAKE_INSTALL_PREFIX=run -DCMAKE_BUILD_TYPE="Release" -DCMAKE_CXX_COMPILER="clang++-8" -DCMAKE_C_COMPILER="clang-8" -DSEA_ENABLE_LLD="ON" -GNinja -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../
This command should be run instead of the cmake command 2. in the installation instructions above.
SeaHorn provides several components that are automatically cloned and installed via the extra
target. These components can be used by other projects outside of
SeaHorn.
-
llvm-dsa:
git clone https://github.com/seahorn/llvm-dsa.git
llvm-dsa
is the legacy DSA implementation from PoolAlloc. DSA is a heap analysis used by SeaHorn to disambiguate the heap. -
sea-dsa:
git clone https://github.com/seahorn/sea-dsa.git
sea-dsa
is a new DSA-based heap analysis. Unlikellvm-dsa
,sea-dsa
is context-sensitive and therefore, a finer-grained partition of the heap can be generated in presence of function calls. -
clam:
git clone https://github.com/seahorn/crab-llvm.git
clam
provides inductive invariants using abstract interpretation techniques to the rest of SeaHorn's backends. -
llvm-seahorn:
git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn
provides tailored-to-verification versions ofInstCombine
andIndVarSimplify
LLVM passes as well as a LLVM pass to convert undefined values into nondeterministic calls, among other things.
SeaHorn doesn't come with its own version of Clang and expects to find it
either in the build directory (run/bin
) or in PATH. Make sure that the
version of Clang matches the version of LLVM that comes with SeaHorn
(currently 5.0). The easiest way to provide the right version of Clang is
to download it from llvm.org,
unpact it somewhere and create a symbolic link to clang
and clang++
in run/bin
.
cd seahorn/build/run/bin
ln -s place_where_you_unpacked_clang/bin/clang clang
ln -s place_where_you_unpacked_clang/bin/clang++ clang++
Running tests require several python packages:
pip install lit OutputCheck
easy_install networkx
apt-get install libgraphviz-dev
easy_install pygraphviz
Tests can be run using:
$ export SEAHORN=<install_dir>/bin/sea
$ cmake --build . --target test-all
We can use gcov
and lcov
to generate test coverage information for SeaHorn. To build with coverage enabled,
we need to run build under a different directory and set CMAKE_BUILD_TYPE
to Coverage
during cmake configuration.
Example steps for opsem
tests coverage:
-
mkdir coverage; cd coverage
create and enter coverage build directory -
cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../
configure cmake withCoverage
build type, follow Installation or Compiling with Clang on Linux to set other flags -
follow step 3 through 6 in Installation section to finish build
-
cmake --build . --target test-opsem
Run OpSem tests, now .gcda and .gcno files should be created under correspondingCMakeFiles
directory -
lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info
collect coverage data from desired module, ifclang
is used as the compiler instead ofgcc
, create a bash scriptllvm-gcov.sh
:
#!/bin/bash
exec llvm-cov gcov "$@"
$ chmod +x llvm-gcov.sh
then append --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh
to the lcov -c ...
command.
6. extract data from desired directories and generate html report:
lcov --extract coverage.info "*/lib/seahorn/*" -o lib.info
lcov --extract coverage.info "*/include/seahorn/*" -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report
then open coverage_report/index.html
in browser to view the coverage report
Compilation database for the seahorn project and all its subprojects (e.g., llvm, z3, SeaDsa)
can be generated by adding -DCMAKE_EXPORT_COMPILE_COMMANDS=1
to the first
cmake command presented in Installation. This will produce an additional file
in the selected build directory -- compile_commands.json
.
An easy way to get code indexing to work with with compilation database support
is to copy the .json
file into the main project directory and follow
instructions specific to your editor:
- Clion -- https://www.jetbrains.com/help/clion/compilation-database.html
- Vim (YouCompleteMe) -- https://github.com/Valloric/YouCompleteMe#option-1-use-a-compilation-database
- Emacs (rtags) -- https://vxlabs.com/2016/04/11/step-by-step-guide-to-c-navigation-and-completion-with-emacs-and-the-clang-based-rtags/
For a detailed guide for a remote workflow with CLion check Clion-configuration.
SeaHorn provides a python script called sea
to interact with
users. Given a C program annotated with assertions, users just need to
type: sea pf file.c
This will output unsat
if all assertions hold or otherwise sat
if
any of the assertions is violated.
The option pf
tells SeaHorn to translate file.c
into LLVM
bitecode, generate a set of verification conditions (VCs), and
finally, solve them. The main back-end solver
is spacer.
The command pf
provides, among others, the following options:
-
--show-invars
: display computed invariants if answer wasunsat
. -
--cex=FILE
: stores a counter-example inFILE
if answer wassat
. -
-g
: compiles with debug information for more trackable counterexamples. -
--step=large
: large-step encoding. Each transition relation corresponds to a loop-free fragments. -
--step=small
: small-step encoding. Each transition relation corresponds to a basic block. -
--track=reg
: model (integer) registers only. -
--track=ptr
: model registers and pointers (but not memory content) -
--track=mem
: model both scalars, pointers, and memory contents -
--inline
: inlines the program before verification -
--crab
: inject invariants inspacer
generated by the Crab abstract-interpretation-based tool. Read here for details about all Crab options (prefix--crab
). You can see which invariants are inferred by Crab by typing option--log=crab
. -
--bmc
: use BMC engine.
sea pf
is a pipeline that runs multiple commands. Individual parts
of the pipeline can be run separately as well:
-
sea fe file.c -o file.bc
: SeaHorn frontend translates a C program into optimized LLVM bitcode including mixed-semantics transformation. -
sea horn file.bc -o file.smt2
: SeaHorn generates the verification conditions fromfile.bc
and outputs them into SMT-LIB v2 format. Users can choose between different encoding styles with several levels of precision by adding:-
--step={small,large,fsmall,flarge}
wheresmall
is small step encoding,large
is block-large encoding,fsmall
is small step encoding producing flat Horn clauses (i.e., it generates a transition system with only one predicate), andflarge
: block-large encoding producing flat Horn clauses. -
--track={reg,ptr,mem}
wherereg
only models integer scalars,ptr
modelsreg
and pointer addresses, andmem
modelsptr
and memory contents.
-
-
sea smt file.c -o file.smt2
: Generates CHC in SMT-LIB2 format. Is an alias forsea fe
followed bysea horn
. The commandsea pf
is an alias forsea smt --prove
. -
sea clp file.c -o file.clp
: Generates CHC in CLP format. -
sea lfe file.c -o file.ll
: runs the legacy front-end
To see all the commands, type sea --help
. To see options for each
individual command CMD (e.g, horn
), type sea CMD --help
(e.g.,
sea horn --help
).
By default, SeaHorn does not use Crab, our abstract interpreter. To enable
it, add the option --crab
to the sea
command.
The abstract interpreter is by default intra-procedural and it uses the Zones domain as the numerical abstract domain. These default options should be enough for normal users. For developers, if you want to use other abstract domains you need to:
- Compile with
cmake
options-DCLAM_ALL_DOMAINS=ON -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON
- Run
sea
with option--crab-dom=DOM
whereDOM
can be:int
for intervalsterm-int
for intervals with uninterpreted functionsboxes
: for disjunctive intervalsoct
for octagonspk
for polyhedra
To use the crab inter-procedural analysis you need to:
- Compile with cmake option
-DCLAM_ENABLE_INTER=ON
- Run
sea
with option--crab-inter
By default, the abstract interpreter only reasons about scalar
variables (i.e., LLVM registers). Run sea
with the options
--crab-singleton-aliases=true --crab-track=arr
to reason about
memory contents.
Crab is mostly path-insensitive while Spacer, our Horn clause solver,
is path-sensitive. Although path-insensitive analyses are more
efficient, path-sensitivity is typically required to prove the
property of interest. This motivates our decision of running first
Crab (if option --crab
) and then pass the generated invariants to
Spacer. There are currently two ways for Spacer to use the invariants
generated by Crab. The sea
option --horn-use-invs=VAL
tells
spacer
how to use those invariants:
- If
VAL
is equal tobg
then invariants are only used to helpspacer
in proving a lemma is inductive. - If
VAL
is equal toalways
then the behavior is similar tobg
but in addition invariants are also used to helpspacer
to block a counterexample.
The default value is bg
. Of course, if Crab can prove the program is
safe then Spacer does not incur in any extra cost.
This is an example of a C program annotated with a safety property:
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd();
int main(void) {
int k = 1;
int i = 1;
int j = 0;
int n = nd();
while (i < n) {
j = 0;
while (j < i) {
k += (i - j);
j++;
}
i++;
}
sassert(k >= n);
}
SeaHorn follows SV-COMP convention of
encoding error locations by a call to the designated error function
__VERIFIER_error()
. SeaHorn returns unsat
when
__VERIFIER_error()
is unreachable, and the program is considered
safe. SeaHorn returns sat
when __VERIFIER_error()
is reachable and
the program is unsafe. sassert()
method is defined in
seahorn/seahorn.h
.
Apart from proving properties or producing counterexamples, it is
sometimes useful to inspect the code under analysis to get an idea of
its complexity. For this, SeaHorn provides a command sea inspect
. For instance, given a C program ex.c
type:
sea inspect ex.c --sea-dsa=cs+t --mem-dot
The option --sea-dsa=cs+t
enables the new context-, type-sensitive
sea-dsa analysis implemented in our
FMCAD'19
paper. This
command will generate a FUN.mem.dot
file for each function FUN
in
the bitcode program. To visualize the graph of the main function
type:
dot -Tpdf main.mem.dot -o main.mem.pdf
open main.mem.pdf // replace with you favorite pdf viewer
Read this link for more details about memory graphs.
Type sea inspect --help
for all options. Currently, these options are available:
-
sea inspect --profiler
prints the number of functions, basic blocks, loops, etc. -
sea inspect --mem-callgraph-dot
prints todot
format the call graph constructed by SeaDsa. -
sea inspect --mem-callgraph-stats
prints to standard output some statstics about the call graph construction done by SeaDsa. -
sea inspect --mem-smc-stats
prints the number of memory accesses that can be proven safe by SeaDsa.
The following packages are recommended to build SeaHorn on Ubuntu 18.04. Not
everything is necessary for all configurations, but it is simpler to have these
installed. This assumes that clang
is used as a compiler as per-instructions
above.
sudo apt install cmake git build-essential ninja-build llvm-8 clang-8 clang-tools-8 lld-8 libboost-dev subversion g++-7-multilib gcc-multilib lib32stdc++7 libgmp-dev libgmpxx4ldbl libgraphviz-dev libncurses5-dev ncurses-doc