<!-- [](https://dev.azure.com/seahorn/seahorn/_build) -->

About

[SeaHorn][seahorn-web] is an automated analysis framework for LLVM-based languages. This version compiles against LLVM 14.

Some of the supported features are

• Abstract Interpretation-based static analysis
• Unification-based Context-Sensitive pointer analysis
• SMT-based Bounded Model Checking (i.e., symbolic execution)
• CHC-based Software Model Checking (i.e., invariant inference)
• Executable counterexamples (i.e., no reports, just bugs!)

SeaHorn is developed primarily as a framework for conducting research in automated verification. The frameworks provides many components that can be put together in a variety of ways. However, it is not an "out-of-the-box" static analysis tool.

Many analysis tools and examples are provided with the framework. We are constantly looking for new applications and provide support to new users. For more information on what is happening, check our (infrequently updated) [blog][seahorn-blog].

License

[SeaHorn][seahorn-web] is distributed under a modified BSD license. See license.txt for details.

Introduction

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

The result of sea-pf is unsat if all assertions hold, an sat if any of the assertions are violated.

The option pf tells SeaHorn to translate file.c into LLVM bitcode, 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).

Static Analysis with Abstract Interpretation

Inference of Inductive Invariants using Crab

SeaHorn does not use Crab by default. To enable Crab, 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:

1. Compile with cmake options -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON
2. Run sea with option --crab-dom=DOM where DOM can be:
   • int for intervals
   • term-int for intervals with uninterpreted functions
   • boxes: for disjunctive intervals
   • oct for octagons
   • pk for polyhedra

To use the crab inter-procedural analysis you need to 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-track=mem --crab-singleton-aliases=true to reason about memory contents.

How to use Invariants generated by Crab in Spacer

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 to bg then invariants are only used to help spacer in proving a lemma is inductive.
• If VAL is equal to always then the behavior is similar to bg but in addition invariants are also used to help spacer 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.

Property Specification

Properties are assumed to be assertions. SeaHorn provides a static assertion command sassert, as illustrated in the following example

/* 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);
}

Internally, 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.

Inspect Code

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 described in FMCAD19. This command generates a FUN.mem.dot file for each function FUN in the input program. To visualize the graph of the main function, use web graphivz interface, or the following commands:

$ dot -Tpdf main.mem.dot -o main.mem.pdf

More details on the memory graphs is in the SeaDsa repository: here.

Use sea inspect --help to see all options. Currently, the available options are:

• sea inspect --profiler prints the number of functions, basic blocks, loops, etc.
• sea inspect --mem-callgraph-dot prints to dot 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.

Installation

The easiest way to get started with SeaHorn is via a docker distribution.

$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly

Start with exploring what the sea command can do:

$ sea --help
$ sea pf --help

The nightly tag is automatically refreshed daily and contains the latest development version. We maintain all other tags (that require manual update) infrequently. Check the dates on DockerHub and log an issue on GitHub if