Skip to content

Latest commit

 

History

History
119 lines (84 loc) · 4.73 KB

README.md

File metadata and controls

119 lines (84 loc) · 4.73 KB
Raw

Clam: LLVM front-end for Crab

Clam is an Abstract Interpretation-based static analyzer that computes inductive invariants for LLVM bitcode based on the Crab library. This branch supports LLVM 14.

The available documentation can be found in both Clam wiki and Crab wiki.

Docker

You can get Clam from Docker Hub (nightly built) using the command:

 docker pull seahorn/clam-llvm14:nightly

Requirements

Clam is written in C++ and uses heavily the Boost library. The main requirements are:

  • Modern C++ compiler supporting c++14
  • Boost >= 1.65
  • GMP
  • MPFR (only if -DCRAB_USE_APRON=ON or -DCRAB_USE_ELINA=ON)
  • FLINT (only if -DCRAB_USE_PPLITE=ON)
  • Python >= 3.6

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

Tests

Testing infrastructure depends on several Python packages. To run tests you need to install lit and OutputCheck:

 pip3 install lit
 pip3 install OutputCheck

Compilation and installation

The basic compilation steps are:

1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR ../
3. cmake --build . --target crab && cmake ..   
4. cmake --build . --target extra && cmake ..                  
5. cmake --build . --target install

The command at line 2 will try to find LLVM 14 from standard paths. If you installed LLVM 14 in a non-standard path, then add option -DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm to line 2. The command at line 3 will download Crab and compile it from sources. Clam uses two external components that are installed via the extra target at line 4. These components are:

  • sea-dsa is the heap analysis used to translate LLVM memory instructions. Details can be found here and here.

  • llvm-seahorn provides specialized versions of LLVM components to make them more amenable for verification. llvm-seahorn is optional but hightly recommended.

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_APRON=ON -DCRAB_USE_PPLITE=ON options.

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 Clam with Boxes and Apron:

1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$DIR -DCRAB_USE_LDD=ON -DCRAB_USE_APRON=ON ../
3. cmake --build . --target crab && cmake ..
4. cmake --build . --target extra && cmake ..                
5. cmake --build . --target ldd && cmake ..
6. cmake --build . --target apron && cmake ..             
7. cmake --build . --target install

For instance, lines 5 and 6 will download, compile and install the Boxes and Apron libraries, respectively. If you have already compiled and installed these libraries in your machine then skip commands at line 5 and 6 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

Checking installation

To run some regression tests:

 cmake --build . --target test-simple

Usage

Clam provides a Python script called clam.py (located at $DIR/bin where $DIR is the directory where Clam was installed) to interact with users. The simplest command is clam.py test.c. Type clam.py --help for all options and read our wiki.