jdataflow
1.0.0
JDATAFLOF是Java源代碼的基於Z3求解器的數據流分析儀。
目前，JDataflow的檢查器允許檢測邏輯錯誤（始終是正確/false表達式），無指針刪除，數組索引符合界限等等。
例如：
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
}查看測試目錄以獲取更多示例。
通常，JDATAFLOF能夠靜態評估表達式，執行符號執行，處理程序的控制流，等等。它還具有適當的內存模型，因此可以很好地處理參考混疊。
為了構建JDATAFLOF，您需要JDK 8或更新。另外，您必須下載並安裝Z3。
gradlew build注意：視覺C ++ 2015可能需要重新分配。
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildexport 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檢查螞蟻，Maven或Gradle的項目，則應使用掃描utils。
JDATAFLOF使用Spoon庫以後訂單的方式構建和穿越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);
處理功能調用的最明顯方法是將它們內聯。不幸的是，由於性能考慮，我們只能為小型功能（例如Getters或Setter）做到這一點。
另一種方法是構建功能摘要（自動或手動），其中包含有關合同，純度，返回值等的信息。
但是通常，任何未知函數都重置其參數的值。
處理循環的最明顯方法是展開它們。不幸的是，我們只有在靜態且相對較小的迭代次數時才可以做到這一點。
因此，通常，我們必須找到循環不變式並重置其他所有內容，例如對於未知功能。
但是，某些特殊情況可能會有所不同。
JDATAFLOF使用類型索引的內存模型（BurstAll的內存模型）。在此內存模型中，每個數據類型或字段都有其自己的內存數組。它允許檢測類似的東西：
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}以下是一些有用的鏈接，並對不同的內存模型進行了更詳細的說明：
目前，該項目只是概念證明，因此有很多工作要做：
