jdataflow
1.0.0
JDataFlow adalah penganalisa aliran data berbasis pemecah Z3 untuk kode sumber Java.
Saat ini JDataFlow memiliki pemeriksa yang memungkinkan untuk mendeteksi kesalahan logis (selalu ekspresi benar/false), null pointer dereferences, indeks array di luar batas, dll.
Misalnya:
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
}Lihat direktori tes untuk lebih banyak contoh.
Secara umum, JDataFlow mampu mengevaluasi ekspresi secara statis, melakukan eksekusi simbolik, menangani aliran kontrol suatu program, dan sebagainya. Ini juga memiliki model memori yang tepat, sehingga baik berurusan dengan aliasing referensi.
Untuk membangun jdataflow, Anda memerlukan JDK 8 atau lebih baru. Juga, Anda harus mengunduh dan menginstal Z3.
gradlew buildCatatan: Visual C ++ 2015 dapat didistribusikan kembali mungkin diperlukan.
export LD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildexport DYLD_LIBRARY_PATH=/path/to/z3/bin./gradlew buildPerhatikan bahwa Anda mungkin masih perlu mengatur variabel lingkungan atau java.lang.path di IDE Anda.
Sekarang Anda dapat pergi ke Direktori Bangun dan menjalankan toples yang dihasilkan:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
Jika Anda ingin memeriksa proyek semut, maven, atau lulusan Anda dengan JDADAFLOW, Anda harus menggunakan util pemindaian.
JDataFlow menggunakan Perpustakaan Spoon untuk membangun dan melintasi AST dengan cara pasca-pemesanan. Saat melintasi AST, itu menerjemahkan kode sumber ke dalam bentuk yang dapat dimengerti oleh Z3 Solver. Kemudian cek dilakukan oleh solver.
Pertama -tama, untuk digunakan dengan Z3, kode harus ada dalam formulir penugasan tunggal statis. Kami melakukan ini untuk mempertahankan urutan program dalam formula logika. Berikut adalah contoh sederhana:
Bentuk Asli:
x = 1;
y = 2;
x = x + y;
Formulir SSA:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
Setelah melintasi Pernyataan IF, kami membuat variabel baru, yang merupakan hasil dari fungsi IF-Then-Else khusus yang disediakan oleh Z3. Fungsi ini pada dasarnya bergabung dengan nilai dari cabang di atas suatu kondisi.
Bentuk Asli:
if (c) {
x = 1;
} else {
x = 2;
}
Formulir SSA:
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
Pendekatan yang paling jelas untuk menangani panggilan fungsi adalah dengan menyambung mereka. Sayangnya, kita dapat melakukannya hanya untuk fungsi kecil (seperti getters atau setter), karena pertimbangan kinerja.
Pendekatan lain adalah membangun ringkasan fungsi (secara otomatis atau manual), yang berisi informasi tentang kontrak, kemurnian, nilai pengembalian dan sebagainya.
Tetapi secara umum, fungsi apa pun yang tidak diketahui mengatur ulang nilai -nilai argumennya.
Pendekatan yang paling jelas untuk berurusan dengan loop adalah membuka gulungan mereka. Sayangnya, kita dapat melakukannya hanya ketika jumlah iterasi diketahui secara statis dan relatif kecil.
Jadi secara umum, kita harus menemukan invarian loop dan mengatur ulang yang lainnya, seperti untuk fungsi yang tidak diketahui.
Namun, beberapa kasus khusus dapat diobati secara berbeda.
JDataFlow menggunakan model memori yang diindeks tipe (model memori Burstall). Dalam model memori ini, setiap tipe atau bidang data memiliki array memori sendiri. Itu memungkinkan untuk mendeteksi sesuatu seperti itu:
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}Berikut adalah beberapa tautan yang berguna dengan penjelasan yang lebih rinci tentang model memori yang berbeda:
Saat ini proyek ini hanyalah bukti konsep, jadi ada banyak pekerjaan yang harus dilakukan:
