| Windows | Ubuntu | OS X | Chat with us | Stories |
|---|---|---|---|---|
| TBD |  |
TBD |  |
 |
SeaHorn is an automated analysis framework for LLVM-based languages. LLVM version is 3.8.
SeaHorn is distributed under a modified BSD license. See license.txt for details.
cd seahorn ; mkdir build ; cd buildcmake -DCMAKE_INSTALL_PREFIX=run ../cmake --build .to build dependencies (Z3 and LLVM)cmake --build . --target extra && cmake ..to download extra packagescmake --build . --target crab && cmake ..to configure crab-llvm (ifextratarget was run)cmake --build . --target installto build seahorn and install everything inrundirectory
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.
SeaHorn provides several components that are installed via the extra
target. These components can be used by other projects outside of
SeaHorn.
-
llvm-seahorn:
git clone https://github.com/seahorn/llvm-seahorn.gitllvm-dsais 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.gitsea-dsais a new DSA-based heap analysis. Unlikellvm-dsa,sea-dsais context-sensitive and therefore, a finer-grained partition of the heap can be generated in presence of function calls. -
crab-llvm:
git clone https://github.com/seahorn/crab-llvm.gitcrab-llvmprovides inductive invariants using abstract interpretation techniques to the rest of SeaHorn's backends. -
llvm-seahorn:
git clone https://github.com/seahorn/llvm-seahorn.gitllvm-seahornprovides tailored-to-verification versions ofInstCombineandIndVarSimplifyLLVM 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 3.8). 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++
Tests require lit and OutputCheck. These can be installed using
pip install lit OutputCheckTest can be run using
$ cmake --build . --target test-simple
$ cmake --build . --target test-solve
$ cmake --build . --target test-abc
$ cmake --build . --target test-dsaNote: test-dsa requires additional python packages
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 inFILEif 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 inspacergenerated 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.bcand 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}wheresmallis small step encoding,largeis block-large encoding,fsmallis 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}whereregonly models integer scalars,ptrmodelsregand pointer addresses, andmemmodelsptrand memory contents.
-
-
sea smt file.c -o file.smt2: Generates CHC in SMT-LIB2 format. Is an alias forsea fefollowed bysea horn. The commandsea pfis 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).
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.