clam

クラム：クラブ用のLLVMフロントエンド

CLAMは、CRABライブラリに基づいてLLVMビットコードの誘導性不変性を計算する抽象的な解釈ベースの静的分析器です。このブランチはLLVM 14をサポートしています。

利用可能なドキュメントは、クラムウィキとクラブウィキの両方にあります。

Docker

コマンドを使用して、Docker Hub（Nightly Build）からハマグリを取得できます。

 docker pull seahorn/clam-llvm14:nightly

要件

CLAMはC ++で書かれており、Boost Libraryを非常に使用しています。主な要件は次のとおりです。

• C ++ 14をサポートする最新のC ++コンパイラ
• ブースト> = 1.65
• GMP
• MPFR（ -DCRAB_USE_APRON=ONまたは-DCRAB_USE_ELINA=ON場合のみ）
• フリント（ -DCRAB_USE_PPLITE=ON場合のみ）
• Python> = 3.6

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

テスト

インフラストラクチャのテストは、いくつかのPythonパッケージに依存します。テストを実行するには、 litとOutputCheckをインストールする必要があります。

 pip3 install lit
 pip3 install OutputCheck

編集とインストール

基本的な編集手順は次のとおりです。

 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 

2行目のコマンドは、標準パスからLLVM 14を見つけようとします。標準以外のパスにLLVM 14をインストールした場合は、オプション-DLLVM_DIR=$LLVM-14_INSTALL_DIR/lib/cmake/llvm 2行目に追加します。3行目のコマンドはCRABをダウンロードしてソースからコンパイルします。 CLAMは、4行目のextraターゲットを介してインストールされている2つの外部コンポーネントを使用します。これらのコンポーネントは次のとおりです。

• Sea-DSAは、LLVMメモリ命令の翻訳に使用されるヒープ分析です。詳細はこちらとこちらをご覧ください。

• LLVM-Seahornは、LLVMコンポーネントの特殊なバージョンを提供して、検証に適したものにします。 llvm-seahornはオプションですが、高度に推奨されています。

ボックス/エプロン/エリナ/ppliteドメインには、サードパーティライブラリが必要です。これらのドメインに興味がないユーザーへの負担を回避するために、ライブラリのインストールはオプションです。

• ボックスドメインを使用する場合は、オプション-DCRAB_USE_LDD=ONを追加します。

• エプロンライブラリドメインを使用する場合は、オプション-DCRAB_USE_APRON=ONを追加します。

• Elina Libraryドメインを使用する場合は、オプション-DCRAB_USE_ELINA=ONを追加します。

• ppliteライブラリドメインを使用する場合は、 -DCRAB_USE_APRON=ON -DCRAB_USE_PPLITE=ON optionsを追加します。

重要：エプロンとエリナは現在互換性がないため、 -DCRAB_USE_APRON=ONと-DCRAB_USE_ELINA=ON同時に有効にすることはできません。

たとえば、ボックスとエプロンでクラムをインストールするには：

 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 

たとえば、5行目と6行目は、それぞれボックスとエプロンライブラリをダウンロード、コンパイル、インストールします。これらのライブラリをマシンに既にコンパイルしてインストールしている場合は、5行目と6行でコマンドをスキップし、2行目に次のオプションを追加します。

• エプロンの場合： -DAPRON_ROOT=$APRON_INSTALL_DIR
• Elina： -DELINA_ROOT=$ELINA_INSTALL_DIR
• ボックスの場合： -DCUDD_ROOT=$CUDD_INSTALL_DIR -DLDD_ROOT=$LDD_INSTALL_DIR
• for pplite： -DPPLITE_ROOT=$PPLITE_INSTALL_DIR -DFLINT_ROOT=$FLINT_INSTALL_DIR

インストールの確認

いくつかの回帰テストを実行するには：

 cmake --build . --target test-simple

使用法

CLAMは、ユーザーと対話するために、 clam.py （ $DIR/binにある$DIR binにあるディレクトリ）と呼ばれるPythonスクリプトを提供します。最も単純なコマンドはclam.py test.cです。タイプclam.py --helpすべてのオプションのヘルプとwikiを読んでください。