Windows	Ubuntu	OS X	Chat with us	Stories
TBD		TBD

SeaHorn is an automated analysis framework for LLVM-based languages. This version supports LLVM 5.0.

SeaHorn is distributed under a modified BSD license. See license.txt for details.

• cd seahorn ; mkdir build ; cd build
• 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 packages
• cmake --build . --target crab && cmake .. to configure crab-llvm (if extra target was run)
• cmake --build . --target install to build seahorn and install everything in run 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++-6.0" -DCMAKE_C_COMPILER="clang-6.0" -DSEA_ENABLE_LLD="ON" -GNinja -DCMAKE_EXPORT_COMPILE_COMMANDS=1 ../

SeaHorn provides several components that are 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. Unlike llvm-dsa, sea-dsa is 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.git

  crab-llvm 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 of InstCombine and IndVarSimplify 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

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 was unsat.

• --cex=FILE : stores a counter-example in FILE if answer was sat.

• -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 in spacer 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:

1. sea fe file.c -o file.bc: SeaHorn frontend translates a C program into optimized LLVM bitcode including mixed-semantics transformation.

2. sea horn file.bc -o file.smt2: SeaHorn generates the verification conditions from file.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} where small 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), and flarge: block-large encoding producing flat Horn clauses.

   • --track={reg,ptr,mem} where reg only models integer scalars, ptr models reg and pointer addresses, and mem models ptr and memory contents.

3. sea smt file.c -o file.smt2: Generates CHC in SMT-LIB2 format. Is an alias for sea fe followed by sea horn. The command sea pf is an alias for sea smt --prove.

4. sea clp file.c -o file.clp: Generates CHC in CLP format.

5. 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.

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-6.0 clang-6.0 lld-6.0 libboost-dev subversion g++-7-multilib gcc-multilib lib32stdc++7 libgmp-dev libgmpxx4ldbl libgraphviz-dev libncurses5-dev ncurses-doc

• Arie Gurfinkel
• Jorge Navas
• Temesghen Kahsai

• Jakub Kuderski
• Nham Le