jdataflow
1.0.0
Jdataflow ist ein Z3 Solver-basierter Datenflussanalysator für den Java-Quellcode.
Im Moment hat Jdataflow über Checkers, die es ermöglichen, logische Fehler (immer wahr/falsche Ausdrücke), Nullzeiger -Dereferenzen, Array -Indizes außerhalb der Grenzen usw. zu erkennen, usw.
Zum Beispiel:
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
}Weitere Beispiele finden Sie unter dem Testverzeichnis.
Im Allgemeinen kann Jdataflow die Ausdrücke statisch bewerten, eine symbolische Ausführung durchführen, den Kontrollfluss eines Programms verarbeiten usw. Es verfügt auch über ein richtiges Speichermodell, sodass es sich mit Referenz -Aliasing gut befasst.
Um Jdataflow zu bauen, benötigen Sie JDK 8 oder neuer. Außerdem müssen Sie Z3 herunterladen und installieren.
gradlew buildHinweis: Möglicherweise ist Visual C ++ 2015 erforderlich.
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildexport DYLD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildBeachten Sie, dass Sie möglicherweise noch Umgebungsvariablen oder Java.lang.Path in Ihrer IDE einrichten müssen.
Jetzt können Sie zum Build -Verzeichnis gehen und das resultierende Glas ausführen:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
Wenn Sie Ihre Ameise-, Maven- oder Gradle -basierten Projekt mit JDataflow überprüfen möchten, sollten Sie Scan -Utils verwenden.
Jdataflow verwendet die Spoon Library, um AST nach der Bestellung aufzubauen und zu durchqueren. Während des Durchlaufens des AST übersetzt er den Quellcode in ein von Z3 Solver verständlicher Form. Dann werden die Schecks vom Löser durchgeführt.
Um mit Z3 verwendet zu werden, sollte der Code im statischen Einzelzuweisungsformular vorhanden sein. Wir tun dies, um die Reihenfolge eines Programms in einer Logikformel aufrechtzuerhalten. Hier ist ein einfaches Beispiel:
Originalform:
x = 1;
y = 2;
x = x + y;
SSA -Form:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
Nach dem Durchlaufen der Anweisung erstellen wir eine neue Variable, die das Ergebnis einer speziellen IF-Then-ELSE-Funktion von Z3 ist. Diese Funktion verbindet im Wesentlichen Werte von Zweigen über eine Bedingung.
Originalform:
if (c) {
x = 1;
} else {
x = 2;
}
SSA -Form:
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
Der offensichtlichste Ansatz, um mit Funktionsaufrufen umzugehen, besteht darin, sie zu inline. Leider können wir dies nur für kleine Funktionen (wie Gettter oder Setter) aufgrund der Leistungsüberlegungen tun.
Ein anderer Ansatz besteht darin, Funktionsfunktionen (automatisch oder manuell) zu erstellen, die Informationen zu Verträgen, Reinheit, Rückgabetwerten usw. enthalten.
Im Allgemeinen setzt jede unbekannte Funktion die Werte ihrer Argumente zurück.
Der offensichtlichste Ansatz, um mit Schleifen umzugehen, besteht darin, sie abzuwickeln. Leider können wir es nur dann tun, wenn die Anzahl der Iterationen statisch und relativ klein bekannt ist.
Im Allgemeinen müssen wir Loop -Invarianten finden und alles andere zurücksetzen, wie für die unbekannten Funktionen.
Einige Sonderfälle könnten jedoch unterschiedlich behandelt werden.
Jdataflow verwendet Typindexed-Speichermodell (Burstall-Speichermodell). In diesem Speichermodell verfügt jedes Datentyp oder das Feld für ein eigenes Speicherarray. Es ermöglicht so etwas:
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}Hier sind einige nützliche Links mit einer detaillierteren Erklärung verschiedener Speichermodelle:
Im Moment ist dieses Projekt nur ein Beweis für das Konzept, daher gibt es viel zu tun:
