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 الخاص بك.
الآن يمكنك الذهاب إلى دليل الإنشاء وتشغيل الجرة الناتجة:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]
إذا كنت ترغب في التحقق من مشروع ANT أو Maven أو Gradle مع JDataFlow ، فيجب عليك استخدام Utils Scan.
يستخدم JDataFlow مكتبة Spoon لإنشاء وتجارة AST بطريقة ما بعد الترتيب. أثناء عبور AST ، فإنه يترجم رمز المصدر إلى نموذج يمكن مفهومه بواسطة Z3 Solver. ثم يتم إجراء الشيكات بواسطة حلال.
بادئ ذي بدء ، من أجل استخدامه مع Z3 ، يجب أن يكون الكود موجودًا في نموذج تعيين واحد ثابت. نقوم بذلك للحفاظ على ترتيب البرنامج في صيغة منطقية. هنا مثال بسيط:
الشكل الأصلي:
x = 1;
y = 2;
x = x + y;
نموذج SSA:
x0 = 1;
y0 = 2;
x1 = x0 + y0;
بعد العبارة إذا كان البيان ، نقوم بإنشاء متغير جديد ، وهو نتيجة لوظيفة خاصة إذا كانت else التي توفرها Z3. هذه الوظيفة تنضم بشكل أساسي إلى القيم من الفروع على حالة.
الشكل الأصلي:
if (c) {
x = 1;
} else {
x = 2;
}
نموذج SSA:
if (c) {
x0 = 1;
} else {
x1 = 2;
}
x3 = ITE(c0, x0, x1);
النهج الأكثر وضوحا للتعامل مع مكالمات الوظائف هو ضمورها. لسوء الحظ ، يمكننا القيام بذلك فقط للوظائف الصغيرة (مثل getters أو المستقلين) ، بسبب اعتبارات الأداء.
هناك طريقة أخرى تتمثل في إنشاء ملخصات الوظائف (تلقائيًا أو يدويًا) ، والتي تحتوي على معلومات حول العقود والنقاء وقيم الإرجاع وما إلى ذلك.
ولكن بشكل عام ، تعيد أي وظيفة غير معروفة ضبط قيم وسيطاتها.
النهج الأكثر وضوحا للتعامل مع الحلقات هو إلحاقها. لسوء الحظ ، لا يمكننا القيام بذلك فقط عندما يكون عدد التكرارات معروفًا بشكل ثابت وصغير نسبيًا.
لذلك بشكل عام ، يتعين علينا العثور على ثبات حلقة وإعادة ضبط كل شيء آخر ، مثل الوظائف غير المعروفة.
ومع ذلك ، يمكن التعامل مع بعض الحالات الخاصة بشكل مختلف.
يستخدم JDataFlow نموذج الذاكرة المحتملة من النوع (نموذج ذاكرة Burstall). في نموذج الذاكرة هذا ، يحتوي كل نوع أو حقل على صفيف الذاكرة الخاص به. يسمح باكتشاف شيء كهذا:
void m () {
C a = new C ();
a . x = 10 ;
C b = a ;
b . x = 20 ;
if ( a . x == 20 ) {} // <= always true
}فيما يلي بعض الروابط المفيدة مع شرح أكثر تفصيلاً لنماذج الذاكرة المختلفة:
في الوقت الحالي ، يعد هذا المشروع مجرد دليل على المفهوم ، لذلك هناك الكثير من العمل الذي يجب القيام به:
