crab
1.0.0
CRABは、抽象的な解釈に基づいてプログラムの静的分析を構築するためのC ++ライブラリです。 CRABは、抽象的なドメインの豊富なセット、KleeneベースのFixPointソルバー、およびデータフロー、我調、および後方などのさまざまな分析を提供します。カニの設計は非常にモジュール式であるため、新しい抽象的なドメインとソルバーを簡単にプラグインするか、新しい分析を構築できます。
カニの抽象的なドメインは、メモリの内容、C様アレイ、数値特性について推論することができます。 CRABは、ゾーンやオクタゴンなどの一般的な数値ドメインの効率的な実装を使用して、たとえば、象徴的な用語（別名、解釈されていない関数）について推論します。また、CRABは、効率的な環境マップを使用して、間隔や一致などの一般的な非関連ドメインを実装し、標準の削減製品構造を介して任意のドメインの組み合わせを可能にします。また、CRABは、線形決定図に基づいてボックスと呼ばれる専門的な分離区間隔や、任意のドメインをその分離完了の過度に承認するまで持ち上げるより一般的な価値分割戦略などの非凸ドメインを提供します。これらのドメインに加えて、すべてCRABの著者によって開発されたすべてのドメインであるCRABライブラリは、Apron、Elina、Ppliteなどの一般的な抽象ドメインライブラリを統合しています。
CRABは、Bourdoncleの弱いトポロジー順序を使用して拡大点のセットを選択する最先端のインターリーブフィックスポイントソルバーを提供します。拡大中に精密損失を緩和するために、カニは、しきい値で拡大したり、拡大したりするなど、いくつかの一般的な技術を実装します。
CRABは、2つの異なるプロセス型分析の実装を提供します。再帰コールをサポートしたメモ化中のプロセドラル分析を備えたトップダウンと、ボトムアップ +トップダウン分析のハイブリッドです。最後になりましたが、CRABは、必要な前提条件を計算したり、誤報の数を減らすために使用できる、より実験的な後方分析を実装しています。
CRABは主流のプログラミング言語を直接分析しませんが、代わりにCRABIRと呼ばれる独自のCFGベースの中間表現を分析します。 Crabirは3つのアドレスコードであり、強く入力されています。 Crabirでは、制御フローは非決定的なGOTOの指示を介して定義されます。標準のブールと算術操作は別として、Crabirは特別な想定と主張の声明を提供します。前者は制御フローを改良するために使用でき、後者はユーザー定義のプロパティをチェックするための単純な機械を提供します。そのシンプルなデザインにもかかわらず、CrabirはLLVMなどの言語を表すのに十分なほど豊富です。
カニは積極的に開発中です。バグが見つかった場合は、githubの問題を開いてください。新機能を備えたプルリクエストは大歓迎です。利用可能なドキュメントは、Wikiにあります。このライブラリを使用する場合は、この論文を引用してください。
| Windows | ubuntu | OS X | カバレッジ |
|---|---|---|---|
| TBD |  | TBD |
すべてのテストを実行するCrabの（毎晩）事前に構築されたバージョンは、Dockerを使用して取得できます。
docker pull seahorn/crab:bionic
docker run -v ` pwd ` :/host -it seahorn/crab:bionicCrabはC ++で書かれており、Boost Libraryに依存しています。主な要件は次のとおりです。
-DCRAB_USE_APRON=ONまたは-DCRAB_USE_ELINA=ON ）-DCRAB_USE_PPLITE=ON場合のみ）Linuxでは、コマンドを入力する要件をインストールできます。
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
クラブをインストールするには、入力します。
1. mkdir build && cd build
2. cmake -DCMAKE_INSTALL_PREFIX=$INSTALL_DIR ../
3. cmake --build . --target install
tests Directoryには、Crabirで書かれたプログラムを構築し、異なる分析と抽象的なドメインを使用して不変材を計算する方法の多くの例が含まれています。これらのテストをコンパイルするには、Option -DCRAB_ENABLE_TESTS=ON ON ADDを追加します。
そして、たとえば、 test1を実行するために：
build/test-bin/test1
ボックス/エプロン/エリナ/ppliteドメインには、サードパーティライブラリが必要です。これらのドメインに興味がないユーザーへの負担を回避するために、ライブラリのインストールはオプションです。
ボックスドメインを使用する場合は、オプション-DCRAB_USE_LDD=ONを追加します。
エプロンライブラリドメインを使用する場合は、オプション-DCRAB_USE_APRON=ONを追加します。
Elina Libraryドメインを使用する場合は、オプション-DCRAB_USE_ELINA=ONを追加します。
ppliteライブラリドメインを使用する場合は、 -DCRAB_USE_PPLITE=ON optionを追加します。
重要：エプロンとエリナは現在互換性がないため、 -DCRAB_USE_APRON=ONと-DCRAB_USE_ELINA=ON同時に有効にすることはできません。
たとえば、箱とエプロンでクラブをインストールするには、次を入力します。
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
3行目と4行目は、それぞれボックスとエプロンドメインをダウンロード、コンパイル、インストールします。代わりにElinaまたはPpliteを使用する場合は、4行目のapron elinaまたはppliteに置き換えます。これらのライブラリをマシンに既にコンパイルしてインストールしている場合は、3行目と4行でコマンドをスキップし、2行目に次のオプションを追加します。
-DAPRON_ROOT=$APRON_INSTALL_DIR-DELINA_ROOT=$ELINA_INSTALL_DIR-DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR-DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIRC ++アプリケーションにCRABを含めるには、次のことが必要です。
$INSTALL_DIR/crab/includeにあるC ++ヘッダーファイルを含めると
アプリケーションは$INSTALL_DIR/crab/libにインストールされているクラブライブラリにリンクします。
ボックス/エプロン/elina/ppliteでコンパイルする場合はEXT=apron|elina|ldd|pplite $ install_dir $INSTALL_DIR/EXT/lib $INSTALL_DIR/EXT/includeを含める必要があります。
プロジェクトがcmakeを使用している場合は、プロジェクトのCMakeLists.txtを追加するだけです。
add_subdirectory(crab)
include_directories(${CRAB_INCLUDE_DIRS})
そして、実行可能ファイルを${CRAB_LIBS}でリンクします
プロジェクトがmakeを使用している場合は、このサンプルMakeFileをお読みください。
