jdataflow
1.0.0
JDataFlow es un analizador de flujo de datos basado en el solucionador Z3 para el código fuente de Java.
En este momento, JDataFlow tiene verificadores que permiten detectar errores lógicos (siempre expresiones verdaderas/falsas), deserencias de puntero nulo, índices de matriz fuera de los límites, etc.
Por ejemplo:
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
}Consulte el directorio de prueba para obtener más ejemplos.
En general, JDataFlow es capaz de evaluar las expresiones estáticamente, realizar una ejecución simbólica, manejar el flujo de control de un programa, etc. También presenta un modelo de memoria adecuado, por lo que trata muy bien con alias de referencia.
Para construir JDataFlow, necesitas JDK 8 o más nuevo. Además, debe descargar e instalar Z3.
gradlew buildNota: Se puede requerir Visual C ++ 2015 Redistributable.
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildexport DYLD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildTenga en cuenta que aún puede necesitar configurar variables de entorno o java.lang.path en su IDE.
Ahora puede ir al directorio de compilación y ejecutar el frasco resultante:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
Si desea verificar su hormiga, maven o proyecto de gradle con JDataFlow, debe usar Utils Scan.
JDataFlow utiliza la biblioteca Spoon para construir y atravesar AST de una manera posterior al orden. Mientras atraviesa el AST, traduce el código fuente en un formulario comprensible por Z3 Solver. Luego, el solucionador realiza los controles.
En primer lugar, para usarse con Z3, el código debe estar presente en el formulario de asignación única estática. Hacemos esto para mantener el orden de un programa en una fórmula lógica. Aquí hay un ejemplo simple:
Forma original:
x = 1;
y = 2;
x = x + y;
Forma SSA:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
Después de atravesar la declaración IF, creamos una nueva variable, que es el resultado de una función especial IF-Then-Else proporcionada por Z3. Esta función esencialmente une valores de ramas sobre una condición.
Forma original:
if (c) {
x = 1;
} else {
x = 2;
}
Forma SSA:
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
El enfoque más obvio para tratar las llamadas de funciones es en línea. Desafortunadamente, solo podemos hacerlo para funciones pequeñas (como Getters o Setters), debido a las consideraciones de rendimiento.
Otro enfoque es construir resúmenes de funciones (automáticamente o manualmente), que contienen información sobre contratos, pureza, valores de devolución, etc.
Pero en general, cualquier función desconocida restablece los valores de sus argumentos.
El enfoque más obvio para tratar con los bucles es desenrollarlos. Desafortunadamente, podemos hacerlo solo cuando el número de iteraciones se conoce estáticamente y relativamente pequeño.
Entonces, en general, tenemos que encontrar invariantes de bucle y restablecer todo lo demás, como para las funciones desconocidas.
Sin embargo, algunos casos especiales podrían tratarse de manera diferente.
JDataFlow usa el modelo de memoria índice de tipo (modelo de memoria de Burstall). En este modelo de memoria, cada tipo de datos o campo tiene su propia matriz de memoria. Permite detectar algo así:
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}Aquí hay algunos enlaces útiles con una explicación más detallada de diferentes modelos de memoria:
Por el momento, este proyecto es solo una prueba de concepto, por lo que hay mucho trabajo por hacer:
