jdataflow
1.0.0
O JDATAFLOF é um analisador de fluxo de dados baseado em solucionário Z3 para código-fonte Java.
No momento, o JDATAFLOF tem damas que permitem detectar erros lógicos (sempre verdadeiros/falsos expressões), desreferências do ponteiro nulo, índices de matriz fora dos limites, etc.
Por exemplo:
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
}Confira o diretório de teste para obter mais exemplos.
Em geral, o JDATAFLOF é capaz de avaliar expressões estaticamente, executar a execução simbólica, manipular o fluxo de controle de um programa e assim por diante. Ele também possui um modelo de memória adequado, por isso lida bem com o aliasing de referência.
Para construir o JDATAFLOF, você precisa de JDK 8 ou mais recente. Além disso, você deve baixar e instalar o Z3.
gradlew buildNOTA: Pode ser necessária redistribuição visual c ++ 2015.
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildexport DYLD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildObserve que você ainda pode precisar configurar variáveis de ambiente ou java.lang.path em seu IDE.
Agora você pode ir ao diretório de construção e executar o frasco resultante:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
Se você deseja verificar seu projeto baseado em formiga, maven ou gradle com o jdataflow, você deve usar os utilitários de digitalização.
O JDataFlow usa a Biblioteca Spoon para construir e atravessar AST de maneira pós-ordem. Ao atravessar o AST, ele traduz o código -fonte em um formulário compreensível pelo Z3 Solver. Em seguida, os cheques são realizados pelo solucionador.
Antes de tudo, para ser usado com Z3, o código deve estar presente no formulário de atribuição única estática. Fazemos isso para manter a ordem de um programa em uma fórmula lógica. Aqui está um exemplo simples:
Formulário original:
x = 1;
y = 2;
x = x + y;
Formulário SSA:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
Após o TraverSing IF, criamos uma nova variável, que é o resultado de uma função especial IF-Then-Else fornecida por Z3. Essa função une essencialmente valores de ramificações em uma condição.
Formulário original:
if (c) {
x = 1;
} else {
x = 2;
}
Formulário SSA:
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
A abordagem mais óbvia para lidar com as chamadas de função é incluí -las. Infelizmente, podemos fazê -lo apenas para pequenas funções (como getters ou setters), devido às considerações de desempenho.
Outra abordagem é criar resumos de função (automaticamente ou manualmente), que contêm informações sobre contratos, pureza, valores de retorno e assim por diante.
Mas, em geral, qualquer função desconhecida redefine os valores de seus argumentos.
A abordagem mais óbvia para lidar com loops é desenrolá -los. Infelizmente, só podemos fazê -lo quando o número de iterações for conhecido estaticamente e relativamente pequeno.
Então, em geral, temos que encontrar invariantes de loop e redefinir todo o resto, como para as funções desconhecidas.
No entanto, alguns casos especiais podem ser tratados de maneira diferente.
O JDATAFLOF usa o modelo de memória indexado do tipo (modelo de memória do Burstall). Neste modelo de memória, cada tipo de dados ou campo possui sua própria matriz de memória. Permite detectar algo assim:
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}Aqui estão alguns links úteis com uma explicação mais detalhada de diferentes modelos de memória:
No momento, este projeto é apenas uma prova de conceito, então há muito trabalho a fazer:
