sea dsa
1.0.0
SeaDsa 、DSAにインスパイアされたLLVMビットコードのコンテキスト、フィールド、およびアレイに敏感な統一ベースのポイントツー分析です。 SeaDsa 、コンテキスト感度の取り扱い、部分的な流れの感度の追加、およびタイプ認識の改善により、 Dsaよりも数桁スケーラブルで正確であり、 SeaDsaの以前の実装です。
SeaDsa任意のLLVMビットコードを分析できますが、C/C ++プログラムのプログラム検証で使用するために調整されています。スタンドアロンツールとして、またはSeahorn Vidification Frameworkとその分析と一緒に使用できます。
このブランチはLLVM 14をサポートしています。
SeaDsaはC ++で書かれており、Boost Libraryを使用しています。主な要件は次のとおりです。
テストを実行するには、次のパッケージをインストールします。
sudo pip install lit OutputChecksudo easy_install networkxsudo apt-get install libgraphviz-devsudo easy_install pygraphvizGraph 、 Cell 、およびNodeはinclude/Graph.hhおよびsrc/Graph.ccで定義されています。include/Local.hhおよびsrc/DsaLocal.ccに含まれています。include/BottomUp.hhおよびsrc/DsaBottomUp.ccに含まれています。include/TopDown.hhおよびsrc/DsaTopDown.ccにあります。include/Cloner.hhおよびsrc/Clonner.ccに含まれています。include/FieldType.hh 、 include/TypeUtils.hh 、 src/FieldType.cc 、およびsrc/TypeUtils.ccです。include/AllocWrapInfo.hhおよびsrc/AllocWrapInfo.ccに含まれています。 実行中のプログラム検証ベンチマークの指示と、実際のプロジェクトと私たちの結果を構築するためのレシピとともに、Tea-DSA-Extrasで見つけることができます。
SeaDsaには、 includeとsrc 2つのディレクトリが含まれています。 SeaDsa LLVMビットコードを分析しているため、LLVMヘッダーファイルとライブラリは、 SeaDsaを構築するときにアクセスできる必要があります。
プロジェクトがcmakeを使用している場合は、プロジェクトのCMakeLists.txtを追加するだけです。
include_directories(seadsa/include)
add_subdirectory(seadsa)
すでにマシンにllvm-14をインストールしている場合：
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake ..
cmake --build . --target install
さもないと：
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install
テストを実行するには：
cmake --build . --target test-sea-dsa
tests/c/simple.cと呼ばれるCプログラムを検討してください：
#include <stdlib.h>
typedef struct S {
int * * x ;
int * * y ;
} S ;
int g ;
int main ( int argc , char * * argv ){
S s1 , s2 ;
int * p1 = ( int * ) malloc ( sizeof ( int ));
int * q1 = ( int * ) malloc ( sizeof ( int ));
s1 . x = & p1 ;
s1 . y = & q1 ;
* ( s1 . x ) = & g ;
return 0 ;
} ビットコードを生成します：
clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
オプション-O0は、Clangの最適化を無効にするために使用されます。一般に、Clangの最適化を可能にすることをお勧めします。ただし、 simple.cのような些細な例では、Clangはあまりにも多く単純化するため、有用なものは何も観察されません。 Options -c -emit-llvm -S人間が読み取る形式でビットコードを生成します。
ビットコードでsea-dsaを実行し、メモリグラフをドット形式に印刷します。
seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot simple.ll
Options -sea-dsa=butd-cs -sea-dsa-type-aware FMCAD'19論文に実装されている分析を有効にします（参考文献を参照）。このコマンドは、ビットコードプログラムの各関数のFUNにFUN.mem.dotファイルを生成します。私たちの場合、唯一の関数はmainであるため、 main.mem.dotという名前の1つのファイルがあります。ファイルは現在のディレクトリで生成されます。 .dotファイルを別のディレクトリDIRに保存する場合は、オプション-sea-dsa-dot-outdir=DIR追加します
main.mem.dotをpdfファイルに変換して視覚化します。
dot -Tpdf main.mem.dot -o main.mem.pdf
open main.mem.pdf // replace with you favorite pdf viewer
メモリモデルでは、ポインター値は、メモリオブジェクトとオフセットのペアであるセルで表されます。メモリオブジェクトは、メモリグラフのノードとして表されます。エッジはセル間にあります。
各ノードフィールドはセルを表します（つまり、ノードのオフセット）。たとえば、それぞれ%6および%15で指されたノードフィールド<0,i32**>および<8,i32**>は、同じメモリオブジェクトからの2つの異なるセルです。フィールド<8,i32**>対応するメモリオブジェクトのオフセット8のセルを表し、そのタイプはi32**です。黒いエッジは、セル間のポイントと関係を表します。それらは、宛先ノードのオフセットを表す数字でラベル付けされています。青いエッジは、関数の正式なパラメーターをセルで接続します。紫色のエッジは、LLVMポインター変数をセルと接続します。ノードには、 S （スタック割り当てメモリ）、 H （ヒープ割り当てメモリ）、 M （修正されたメモリ）、 R （読み取りメモリ）、 E （外部割り当てメモリ）などのマーカーを持つことができます。ノードが赤の場合、分析はそのノードに対してフィールド感度を失ったことを意味します。ラベル{void}は、ノードが割り当てられているが、プログラムでは使用されていないことを示すために使用されます。
sea-dsa間接呼び出しを解決することもできます。間接コールは、Calleeが静的に知られていないという呼び出しです。 sea-dsa間接コールのすべての可能なCalleesを識別し、LLVMコールグラフを出力として生成します。
この例をtests/c/complete_callgraph_5.cで考えてみてください：
struct class_t ;
typedef int ( * FN_PTR )( struct class_t * , int );
typedef struct class_t {
FN_PTR m_foo ;
FN_PTR m_bar ;
} class_t ;
int foo ( class_t * self , int x )
{
if ( x > 10 ) {
return self -> m_bar ( self , x + 1 );
} else
return x ;
}
int bar ( class_t * self , int y ) {
if ( y < 100 ) {
return y + self -> m_foo ( self , 10 );
} else
return y - 5 ;
}
int main ( void ) {
class_t obj ;
obj . m_foo = & foo ;
obj . m_bar = & bar ;
int res ;
res = obj . m_foo ( & obj , 42 );
return 0 ;
}コマンドを入力します：
clang -c -emit-llvm -S tests/c/complete_callgraph_5.c -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll
現在のディレクトリでcallgraph.dotという.dotファイルを生成します。繰り返しますが、 .dotファイルは.pdfファイルに変換され、コマンドで開くことができます。
dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf
sea-dsaコールグラフ解像度プロセスに関するいくつかの統計を印刷することもできます（ clangを呼び出して-gを使用してファイル、行、列情報を印刷する必要があることに注意してください）：
sea-dsa --sea-dsa-callgraph-stats ex.ll
=== Sea-Dsa CallGraph Statistics ===
** Total number of indirect calls 0
** Total number of resolved indirect calls 3
%16 = call i32 %12(%struct.class_t* %13, i32 %15) at tests/c/complete_callgraph_5.c:14:12
RESOLVED
Callees:
i32 bar(%struct.class_t*,i32)
%15 = call i32 %13(%struct.class_t* %14, i32 10) at tests/c/complete_callgraph_5.c:23:16
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
%11 = call i32 %10(%struct.class_t* %2, i32 42) at tests/c/complete_callgraph_5.c:36:9
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
外部呼び出しのポインターセマンティクスはseadsa/seadsa.hで定義されているこれらの関数のいずれかを呼び出すラッパーを書くことによって定義できます。
extern void seadsa_alias(const void *p, ...);extern void seadsa_collapse(const void *p);extern void seadsa_mk_seq(const void *p, unsigned sz); seadsa_aliasすべての議論のセルを統合し、 seadsa_collapse sea-dsa p sea-dsa （つまり、フィールド感受性の喪失） sz指示しseadsa_mk_seq p
たとえば、次のように定義されている外部foo検討してください。
extern void* foo(const void*p1, void *p2, void *p3);
返されたポインターをp2 p1統合する必要があると仮定します。さらに、 p3に対応する細胞を崩壊させたいと思います。次に、 fooの上記のプロトタイプを次の定義に置き換えることができます。
#include "seadsa/seadsa.h"
void* foo(const void*p1, void *p2, void*p3) {
void* r = seadsa_new();
seadsa_alias(r,p2);
seadsa_collapse(p3);
return r;
}
A. GurfinkelとJa Navasによる「C/C ++プログラムの検証のためのコンテキストに敏感なメモリモデル」。 SAS'17で。 （論文）| （スライド）
J. Kuderski、Ja Navas、およびA. Gurfinkelによる「オーバーシェアングなしの統一ベースのポインター分析」。 FMCAD'19で。 （紙）
