ikos
Public release 3.4
IKOS (kernel الاستدلال للمحللين الثابتين المفتوح) هو محلل ثابت لـ C/C ++ بناءً على نظرية التفسير التجريدي.
بدأت IKOS كمكتبة C ++ مصممة لتسهيل تطوير محللات ثابتة سليمة بناءً على تفسير مجردة. يعد تخصص محلل ثابت لتطبيق أو عائلة من التطبيقات أمرًا بالغ الأهمية لتحقيق الدقة وقابلية التوسع. إن تطوير مثل هذا المحلل أمر شاق ويتطلب خبرة كبيرة في التفسير التجريدي.
يوفر IKOS تنفيذًا عامًا وفعالًا لهياكل بيانات التفسير المجردة الحديثة والخوارزميات ، مثل الرسوم البيانية للتدفق ، وتكرارات FixPoint ، والمجالات التجريدية العددية ، إلخ. IKOs مستقلة عن لغة برمجة معينة.
يوفر IKOS أيضًا محللًا ثابتًا C و C ++ يعتمد على LLVM. وهو ينفذ تحليلات قابلة للتطوير للكشف عن وإثبات عدم وجود أخطاء وقت التشغيل في برامج C و C ++.
تم إصدار IKOS بموجب الإصدار 1.3 اتفاقية المصادر الوطنية لناسا ، راجع الترخيص. pdf
انظر الإصدارات.
انظر استكشاف الأخطاء وإصلاحها
لتثبيت IKOS على Linux أو MacOS ، نوصي باستخدام Homebrew .
أولاً ، قم بتثبيت Homebrew باتباع هذه التعليمات.
ثم ، ببساطة تشغيل:
$ brew install nasa-sw-vnv/core/ikos
بالنسبة لنظام التشغيل Windows ، فكر في استخدام نظام Windows الفرعي لـ Linux.
لنفترض أننا نريد تحليل برنامج C التالي في ملف ، يسمى Loop.C :
1 : #include <stdio.h>
2 : int a [ 10 ];
3 : int main ( int argc , char * argv []) {
4 : size_t i = 0 ;
5 : for (; i < 10 ; i ++ ) {
6 : a [ i ] = i ;
7 : }
8 : a [ i ] = i ;
9 : printf ( "%i" , a [ i ]);
10 : }لتحليل هذا البرنامج مع IKOS ، ببساطة تشغيل:
$ ikos loop.c
سترى الإخراج التالي. تقارير IKOS اثنين من الحدوث في التدفق العازلة في السطر 8 و 9.
[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
يأخذ الأمر ikos ملف مصدر ( .c ، .cpp ) أو ملف LLVM Bitcode ( .bc ) كمدخلات ، يحلله للعثور على أخطاء وقت التشغيل (تسمى أيضًا السلوكيات غير المحددة) ، تنشئ قاعدة بيانات output.db في دليل العمل الحالي وطباعة تقرير.
في التقرير ، يحتوي كل سطر على أحد الوضع التالي:
بشكل افتراضي ، يعرض IKOS تحذيرات وأخطاء مباشرة في محطةك ، مثل برنامج التحويل البرمجي.
إذا كان تقرير التحليل كبيرًا جدًا ، فيجب عليك استخدام:
ikos-report output.db لفحص التقرير في المحطة الخاصة بكikos-view output.db لفحص التقرير في واجهة ويبمزيد من المعلومات:
فيما يلي تعليمات لبناء IKOs من المصدر. هذا فقط للمستخدمين المتقدمين الذين يرغبون في حزم IKOs لنظام التشغيل أو تجربة قاعدة الشفرة. خلاف ذلك ، يرجى اتباع التعليمات أعلاه.
لبناء وتشغيل المحلل ، ستحتاج إلى التبعيات التالية:
يمكن تثبيت معظمهم باستخدام مدير الحزمة الخاص بك.
ملاحظة: إذا قمت بإنشاء LLVM من المصدر ، فأنت بحاجة إلى تمكين معلومات نوع التشغيل (RTTI).
الآن بعد أن حصلت على جميع التبعيات على نظامك ، يمكنك إنشاء وتثبيت IKOS.
عندما تفتح توزيع IKOS ، سترى هيكل الدليل التالي:
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
يستخدم IKOS نظام بناء CMAKE. ستحتاج إلى تحديد دليل التثبيت الذي سيحتوي على جميع الثنائيات والمكتبات والرؤوس بعد التثبيت. إذا لم تحدد هذا الدليل ، فسيقوم Cmake بتثبيت كل شيء ضمن install في الدليل الجذر للتوزيع. في الخطوات التالية ، سنقوم بتثبيت IKOS Under /path/to/ikos-install-directory .
فيما يلي خطوات إنشاء وتثبيت IKOS:
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
ثم ، أضف ikos في طريقك (فكر في إضافة هذا في .bashrc):
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
لبناء وتشغيل الاختبارات ، ببساطة اكتب:
$ make check
انظر المساهمين
Sung Kook Kim ، Arnaud J. Venet ، Aditya V. Thakur. حساب Fixpoint التوازي الحتمي. في مبادئ لغات البرمجة (POPL 2020) ، نيو أورليانز ، لويزيانا (PDF).
Guillaume Brat ، Jorge Navas ، Nija Shi و Arnaud Venet. IKOS: إطار للتحليل الثابت على أساس التفسير التجريدي. في وقائع المؤتمر الدولي حول هندسة البرمجيات والأساليب الرسمية (SEFM 2014) ، Grenoble ، فرنسا (PDF).
أرنود فينيت. المجال المقياس: التحليل القابل للتطوير لمثبال عدم المساواة الخطي. في وقائع التحقق بمساعدة الكمبيوتر (CAV 2012) ، بيركلي ، كاليفورنيا ، الولايات المتحدة الأمريكية 2012.
انظر DOC/CODING_STANDARDS.MD
انظر Doc/Overview.md
