lart

LART：LLVMの抽象化と改良ツール

LART = LLVM抽象化と改良ツール。このツールの目標は、さまざまなプログラムの抽象化を実装するLLVMからLLVMへの変換を提供することです。命令セットに関しては、結果のプログラムは、実行および分析できる通常の具体的なLLVMプログラムです。 （フラグメント）プログラムを介した抽象化に関する追加情報は、特別なLLVM固有関数とLLVMメタデータノードを使用して挿入されます。 LARTは、ディスク上のビットコードファイルを処理するスタンドアロンツールと、複雑なLLVMベースのツールに統合できるフレームワークの両方を提供します。 LARTの背後にある主な動機は、LLVMベースのモデルチェッカーやその他の分析ツールに「プリプロセッサ」を提供し、分析の健全性を損なうことなく問題のサイズを縮小することで仕事を簡素化することです。 LARTによって実装された抽象化は、通常、抽象化の「部分」がラフすぎるという特定の指示に基づいて洗練できます（抽象化が粗すぎると、後続の分析に見えるが、元のプログラムには存在しないスプリアスエラーが発生します）。

LLVMビットコードの抽象化

演習全体の目的は、LLVMビットコードから情報を抽象化し、その後の分析をより効率的にします（ある程度の正確さを犠牲にして）。この目的のために、主にLLVMプログラムで非決定的な選択をエンコードできる必要があります。これは、特別な目的の関数（LLVM内在性と同様）を通じて単純に行うことができます。この関数は@lart.choiceという名前で、引数として一対の境界を取り、非決定論的にそれらの境界の間に該当する値を返します。

LLVMセマンティクスへのこの拡張は、ダウンストリームツールによって認識される必要があります。これは、標準のLLVMビットコードからの唯一の重要な偏差でもあります。多くの分析ツールは、内部または外部インターフェイスを使用して、同様のメカニズムを既に実装しています。 @lart.choiceをサポートせずにLARTを使用するためにツールを適応させることは、通常非常に簡単です。

LART、すなわち@lart.meta.*ファミリーによって提供される他の特別な段階的関数がありますが、これらの指示に関する限り、ほとんどのツールは、既存の@llvm.dbg.*通話のように、その存在を安全に無視することができます。プログラムの変換は、LARTが抽象化を改良するために呼び出された場合にそれらの呼び出しを保持することが期待されます（LARTが提供する各抽象化には、抽象化によって挿入された@lart.metaコールを見つける必要があることがよくあります）。

ほとんどの従来の抽象化エンジンは通訳として機能しますが、抽象化をプログラムに「コンパイル」することもできます。指示を象徴的に解釈する代わりに、象徴的な指示をまとめることができます。述語の抽象化の場合、結果のビットコードは、具体的な変数の代わりに直接的な評価評価を操作し、使用します。上で説明したように、重要な違いは、一部の述語には不確定な評価がある可能性があるため、ビットコードが非決定的な選択を行う必要があることです（真実と偽）。一部の変数は完全に抽象化される可能性があり、そのような変数のすべてのテストは、はいとノーの両方の回答の両方をもたらします。

建てる

./devcontainer/Dockerfileからセットアップを使用または繰り返します。

次に使用してください：

 ./scripts/build.sh

コンパイラを実行します

 ./build/bin/lartcc <domain> <compiler arguments> in.c

Opt

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

テスト

 lit -v build/test

注： build/lartcc/lartccは、Exacutabple Permisionsが必要です。