Crab: A C++ Library for Building Program Static Analyses

Crab is a C++ library for building program static analyses based on
Abstract Interpretation. Crab provides
a rich set of abstract domains, Kleene-based fixpoint solvers, as well
as different analyses such as dataflow, inter-procedural and
backward. The design of Crab is quite modular so that it is easy to
plugin new abstract domains and solvers or build new analyses.

Crab abstract domains can reason about memory contents, C-like arrays
and numerical properties. Crab uses efficient implementations of
popular numerical domains such as Zones and
Octagons and novel
domains to reason, for instance, about symbolic
terms (aka
uninterpreted functions). Crab also implements popular non-relational
domains such as interval or congruences using efficient environment
maps,
and allows the combination of arbitrary domains via standard reduced
product constructions. Crab also provides non-convex domains such as
specialized disjunctive intervals called
Boxes
based on linear decision diagrams and a more general value
partitioning strategy that lifts an arbitrary domain to an
over-approximation of its disjunction completion. In addition to these
domains, all developed by Crab authors, the Crab library integrates
popular abstract domain libraries such as
Apron,
Elina, and PPLite.

Crab provides the state-of-the-art interleaved fixpoint
solver
that uses Bourdoncle’s Weak Topological
Ordering to
select the set of widening points. To mitigate precision losses during
widening, Crab implements some popular techniques such as widening
with thresholds and lookahead
widening.

Crab provides two different implementations of inter-procedural
analyses: a top-down with memoization inter-procedural analysis with
support for recursive calls, and a hybrid of bottom-up + top down
analysis. Last but not least, Crab also implements a more experimental
backward analysis that can be used to compute necessary preconditions
and/or reduce the number of false alarms.

Crab does not analyze directly a mainstream programming language but
instead it analyzes its own CFG-based intermediate representation
called
CrabIR.
CrabIR is three-address code and it is strongly typed. In CrabIR,
control flow is defined via non-deterministic goto instructions. Apart
from standard boolean and arithmetic operations, CrabIR provides
special assume and assert statements. The former can be used to refine
the control flow and the latter provides a simple mechanishm to check
for user-defined properties. In spite of its simple design, CrabIR is
rich enough to represent languages such as
LLVM.

Crab is actively under development. If you find a bug please open an
Github issue. Pull requests with new features are very welcome. The
available documentation can be found in our
wiki. If you use this library please cite this paper.

Windows	Ubuntu	OS X	Coverage
TBD		TBD

Docker

A (nightly) pre-built version of Crab that runs all tests can be
obtained using Docker:

docker pull seahorn/crab:bionic
docker run -v `pwd`:/host -it seahorn/crab:bionic

Requirements

Crab is written in C++ and relies on the Boost library. The main
requirements are:

• C++11 compiler
• Boost >= 1.65
• GMP
• MPFR (if -DCRAB_USE_APRON=ON or -DCRAB_USE_ELINA=ON)
• FLINT (only if -DCRAB_USE_PPLITE=ON)

In linux, you can install requirements typing the commands:

sudo apt-get install libboost-all-dev libboost-program-options-dev
sudo apt-get install libgmp-dev
sudo apt-get install libmpfr-dev    
sudo apt-get install libflint-dev

Compilation and Installation

To install Crab, type:

 1. mkdir build && cd build
 2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
 3. cmake --build . --target install 

The tests directory contains many examples of how to build programs
written in CrabIR and compute invariants using different analyses and
abstract domains. To compile these tests add option -DCRAB_ENABLE_TESTS=ON to line 2.

and then, for instance, to run test1:

build/test-bin/test1

Include third-party abstract domain libraries

The Boxes/Apron/Elina/PPLite domains require third-party libraries. To avoid
the burden to users who are not interested in those domains, the
installation of the libraries is optional.

• If you want to use the Boxes domain then add -DCRAB_USE_LDD=ON option.

• If you want to use the Apron library domains then add
  -DCRAB_USE_APRON=ON option.

• If you want to use the Elina library domains then add
  -DCRAB_USE_ELINA=ON option.

• If you want to use the PPLite library domains then add
  -DCRAB_USE_PPLITE=ON option.

Important: Apron and Elina are currently not compatible so you
cannot enable -DCRAB_USE_APRON=ON and -DCRAB_USE_ELINA=ON at the same time.

For instance, to install Crab with Boxes and Apron, type:

 1. mkdir build && cd build
 2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
 3. cmake --build . --target ldd && cmake ..
 4. cmake --build . --target apron && cmake ..    
 5. cmake --build . --target install     

Lines 3 and 4 will download, compile and install the Boxes and Apron domains, respectively. Replace apron at line 4 with elina or pplite if you want to use Elina or PPLite instead. If you have already compiled and installed these libraries in your machine then skip commands at line 3 and 4 and add the following options at line 2.

• For Apron: -DAPRON_ROOT=$APRON_INSTALL_DIR
• For Elina: -DELINA_ROOT=$ELINA_INSTALL_DIR
• For Boxes: -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
• For PPLite: -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

Using Crab library in other C++ projects

To include Crab in your C++ application you need to:

• Include the C++ header files located at the
  $INSTALL_DIR/crab/include, and

• Link your application with the Crab libraries installed in
  $INSTALL_DIR/crab/lib.

If you compile with Boxes/Apron/Elina/PPLite you need also to include
$INSTALL_DIR/EXT/include and link with $INSTALL_DIR/EXT/lib
where EXT=apron|elina|ldd|pplite.

CMake

If your project uses cmake then you just need to add in your project’s CMakeLists.txt:

add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})

And then link your executable with ${CRAB_LIBS}

Make

If your project uses make, read this
sample Makefile.