jdataflow
1.0.0
JDataFlowは、JavaソースコードのZ3ソルバーベースのデータフローアナライザーです。
現時点では、JDATAFLOWには、論理エラー（常に真/偽式）を検出できるチェッカー、ヌルポインターの避難、境界のない配列インデックスなどがあります。
例えば：
void f ( boolean c ) {
int x = 5 ;
int y = c ? 3 : 2 ;
if ( x < y ) {} // <= always false
}
void g ( int x , int y ) {
if ( 2 * x + 3 * y == 12 ) {
if ( 5 * x - 2 * y == 11 ) {
if ( x == 3 ) {} // <= always true
if ( y == 2 ) {} // <= always true
}
}
}
void h ( Something x ) {
if ( x == null ) {
x . f (); // <= null dereference
}
}
void z () {
int [] arr = new int [] { 1 , 2 , 4 , 8 , 16 , 32 };
int x = arr [ 9 ]; // <= array index out of bounds
}その他の例については、テストディレクトリをご覧ください。
一般に、JDataFlowは、表現を静的に評価し、象徴的な実行を実行し、プログラムの制御フローを処理することができます。また、適切なメモリモデルを備えているため、参照エイリアシングをうまく扱います。
JDATAFLOWを構築するには、JDK 8以降が必要です。また、Z3をダウンロードしてインストールする必要があります。
gradlew buildを実行します注：Visual C ++ 2015の再配布可能な場合があります。
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildを実行しますexport DYLD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildを実行しますIDEに環境変数またはjava.lang.pathを設定する必要がある場合があることに注意してください。
これで、ビルドディレクトリにアクセスして、結果のJARを実行できます。
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
JdataFlowを使用したアリ、メイベン、またはグラードベースのプロジェクトを確認する場合は、スキャンユーティルを使用する必要があります。
JDATAFLOWは、スプーンライブラリを使用して、注文後の方法でASTを構築および通過します。 ASTを通過している間、ソースコードをZ3ソルバーが理解できるフォームに変換します。その後、チェックはソルバーによって実行されます。
まず、Z3で使用するには、コードを静的な単一の割り当てフォームに存在する必要があります。これを行い、プログラムの順序をロジック式で維持します。簡単な例を次に示します。
原形：
x = 1;
y = 2;
x = x + y;
SSAフォーム：
x0 = 1;
y0 = 2;
x1 = x0 + y0;
IFステートメントを通過した後、新しい変数を作成します。これは、Z3によって提供される特別なIF-THEN-ELSE関数の結果です。この関数は、本質的に条件を介して枝の値を結合します。
原形：
if (c) {
x = 1;
} else {
x = 2;
}
SSAフォーム：
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
関数呼び出しに対処するための最も明白なアプローチは、それらをインライン化することです。残念ながら、パフォーマンスの考慮事項のため、小さな機能（ゲッターやセッターなど）のみで行うことができます。
別のアプローチは、契約、純度、返品値などに関する情報を含む関数の要約（自動または手動で）を構築することです。
しかし、一般に、未知の関数はその引数の値をリセットします。
ループを扱う最も明白なアプローチは、それらを展開することです。残念ながら、反復数が静的かつ比較的少ない場合にのみ、それを行うことができます。
したがって、一般に、不明な機能のように、ループの不変剤を見つけて、他のすべてをリセットする必要があります。
ただし、いくつかの特別なケースは異なる方法で扱われる可能性があります。
JDataFlowは、タイプインデックスされたメモリモデル（バーストールのメモリモデル）を使用します。このメモリモデルでは、各データ型またはフィールドには独自のメモリアレイがあります。それはそのようなものを検出することを可能にします：
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}さまざまなメモリモデルのより詳細な説明を含むいくつかの有用なリンクを以下に示します。
現時点では、このプロジェクトは単なる概念の証明であるため、やるべきことがたくさんあります。
