jdataflow
1.0.0
JDataFlow-это анализатор потока данных на основе Z3 для исходного кода Java.
На данный момент у Jdataflow есть шашки, которые позволяют обнаруживать логические ошибки (всегда истинные/ложные выражения), Null Pointer Dereferences, индексы массива из границ и т. Д.
Например:
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
}Проверьте Test Directory для получения дополнительных примеров.
В целом, Jdataflow способен оценить выражения статически, выполнять символическое выполнение, обрабатывать поток управления программой и так далее. Он также оснащен правильной моделью памяти, поэтому она хорошо справляется со ссылкой на псевдонивание.
Чтобы построить jdataflow, вам нужен JDK 8 или новее. Кроме того, вы должны загрузить и установить Z3.
gradlew buildПримечание: может потребоваться Visual C ++ 2015.
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildexport DYLD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildОбратите внимание, что вам все равно потребуется настроить переменные среды или java.lang.path в вашем IDE.
Теперь вы можете перейти в каталог сборки и запустить полученную банку:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
Если вы хотите проверить свой проект, основанный на муравьях, Maven или Gradle с JDataFlow, вы должны использовать Scan UTIL.
Jdataflow использует библиотеку Spoon для построения и прохождения AST в постороннем порядке. Пройдя AST, он переводит исходный код в форму, понятную с помощью Z3 Solver. Затем проверки выполняются решателем.
Прежде всего, для использования с Z3 код должен присутствовать в статической форме единого назначения. Мы делаем это, чтобы поддерживать порядок программы в логической формуле. Вот простой пример:
Оригинальная форма:
x = 1;
y = 2;
x = x + y;
Форма SSA:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
После прохождения оператора, мы создаем новую переменную, которая является результатом специальной функции if-then-else, предоставленной Z3. Эта функция по существу соединяет значения из ветвей над условием.
Оригинальная форма:
if (c) {
x = 1;
} else {
x = 2;
}
Форма SSA:
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
Наиболее очевидный подход для борьбы с функциональными вызовами - это встроить их. К сожалению, мы можем сделать это только для небольших функций (например, Getters или Setters) из -за соображений производительности.
Другой подход заключается в создании резюме функций (автоматически или вручную), которые содержат информацию о контрактах, чистоте, возврате значений и так далее.
Но в целом любая неизвестная функция сбрасывает значения своих аргументов.
Самый очевидный подход для борьбы с петлями - развернуть их. К сожалению, мы можем сделать это только тогда, когда число итераций известно статически и относительно мало.
Итак, в целом мы должны найти инварианты петли и сбросить все остальное, как для неизвестных функций.
Тем не менее, некоторые особые случаи могут рассматриваться по -разному.
JDataflow использует модель памяти, индексированная типовым, (модель памяти Burstall). В этой модели памяти каждый тип данных или поле имеет свой собственный массив памяти. Это позволяет обнаружить что -то подобное:
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}Вот несколько полезных ссылок с более подробным объяснением различных моделей памяти:
На данный момент этот проект является лишь доказательством концепции, поэтому предстоит много работы:
