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
}以下是一些有用的链接，并对不同的内存模型进行了更详细的说明：
目前，该项目只是概念证明，因此有很多工作要做：
