jdataflow
1.0.0
JDataflow เป็นเครื่องวิเคราะห์การไหลของข้อมูล Z3 Solver สำหรับซอร์สโค้ด Java
ในขณะที่ JDataflow มีหมากรุกซึ่งอนุญาตให้ตรวจจับข้อผิดพลาดเชิงตรรกะ (การแสดงออกจริง/เท็จเสมอ), ตัวชี้ตัวชี้โมฆะ, ดัชนีอาร์เรย์นอกขอบเขต ฯลฯ
ตัวอย่างเช่น:
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
}ตรวจสอบไดเรกทอรีทดสอบสำหรับตัวอย่างเพิ่มเติม
โดยทั่วไปแล้ว 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 ของคุณ
ตอนนี้คุณสามารถไปที่ Build Directory และเรียกใช้ Jar ผลลัพธ์:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
หากคุณต้องการตรวจสอบโครงการ ANT, Maven หรือ Gradle ด้วย JDataflow คุณควรใช้ Utils สแกน
JDataflow ใช้ห้องสมุดช้อนเพื่อสร้างและสำรวจ AST ในลักษณะหลังการสั่งซื้อ ในขณะที่ข้าม AST มันแปลซอร์สโค้ดเป็นรูปแบบที่เข้าใจได้โดย Z3 Solver จากนั้นการตรวจสอบจะดำเนินการโดยตัวแก้
ก่อนอื่นเพื่อที่จะใช้กับ Z3 ควรใช้รหัสในแบบฟอร์มการกำหนดเดียวแบบคงที่ เราทำสิ่งนี้เพื่อรักษาลำดับของโปรแกรมในสูตรตรรกะ นี่คือตัวอย่างง่ายๆ:
แบบฟอร์มดั้งเดิม:
x = 1;
y = 2;
x = x + y;
รูปแบบ SSA:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
หลังจากเดินทางหากคำสั่งเราสร้างตัวแปรใหม่ซึ่งเป็นผลมาจากฟังก์ชั่นพิเศษ if-then-Else ที่ Z3 จัดทำโดย 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
}นี่คือลิงค์ที่มีประโยชน์พร้อมคำอธิบายโดยละเอียดเพิ่มเติมเกี่ยวกับโมเดลหน่วยความจำที่แตกต่างกัน:
ในขณะนี้โครงการนี้เป็นเพียงการพิสูจน์แนวคิดดังนั้นจึงมีงานต้องทำมากมาย:
