sys

SYS: أداة ثابتة/رمزية للعثور على الأخطاء الجيدة في رمز جيد (متصفح)

إذا كنت مهتمًا ، تحقق من إعادة التنفيذ الجديدة (جدًا جدًا) هنا!

ثَبَّتَ

تثبيت التبعيات

إذا كنت ترغب في تثبيت SYS محليًا:

• LLVM-9 ، LLVM-9-TOOLS
• تم تكوين Boolector مع --shared . راجع وظائف build() و package() في هذا الملف كمثال على كيفية تثبيت Boolector بعد استنساخه. على Arch Linux ، يمكنك فقط تثبيت boolector-git من Aur.
• مكدس أداة Haskell

بدلاً من ذلك ، يمكنك استخدام Dockerfile من Ralf-Philipp Weinmann.

بناء مشروع

بمجرد تثبيت جميع التبعيات ، يجب أن تكون قادرًا على إنشاء الأداة فقط:

 stack build

امتحان

بمجرد قيامك ببناء الأداة ، يمكنك إنشاء وتشغيل اختباراتنا مع:

 stack test

سيؤدي ذلك إلى تشغيل نسخة كاملة أو أقل من جناح الاختبار الخاص بنا ، إلى جانب اختبارات الانحدار لكل خطأ ندرجه في الورقة. يستغرق الجناح ما يزيد قليلاً عن دقيقتين على الكمبيوتر المحمول مع 64 جيجابايت من ذاكرة الوصول العشوائي و 8 خيوط. يجب أن تمر جميع الاختبارات باستثناء واحد --- خطأ الذي نواجه فيه مشكلة في تعقب ---. إذا فشل أي شيء آخر ، فحاول إعادة تشغيل الاختبارات ؛ ربما يكون المحلل قد توقيت (لم يحدث هذا على أجهزتنا ، ولكن نظرًا لأننا لا نستطيع أن نقدم لك تسجيل دخول لإسماعه ، فمن المحتمل أن يحدث على جهازك).

إذا كنت ترغب فقط في إعادة إنتاج نتائج الورق ولا شيء غير ذلك ، فتشرك:

 stack test --ta '-p End-to-end'

يجري

بمجرد إنشاء الأداة ، يمكنك الآن استخدامها للعثور على الأخطاء!

 stack exec sys

تأخذ الأداة عدة خيارات:

  -d DIR    --libdir=DIR   directory (or file) to analyze
  -e EXTN   --extn=EXTN    file extension
  -c CHECK  --check=CHECK  checker to run

• يتم استخدام خيار -d لتحديد الدليل (يحتوي على ملفات LLVM) أو ملف LLVM واحد.
• يتم استخدام خيار -e لتحديد امتداد الملفات للتحقق. يكون هذا مفيدًا عند بناء مشروعك بمستويات تحسينات مختلفة (على سبيل المثال ، .ll-O0 لبناء التصحيح مع -O0 و .ll-O0_p للإنتاج).
  • ll يطابق كل ملفات *.ll
  • O0 يطابق جميع ملفات *.ll-O0 و *.ll-O0_p
  • O1 يطابق جميع ملفات *.ll-O1 و *.ll-O1_p
  • O2 يطابق جميع ملفات *.ll-O2 و *.ll-O2_p
  • O3 يطابق جميع ملفات *.ll-O3 و *.ll-O3_p
  • يطابق Og جميع ملفات *.ll-Og و *.ll-Og_p
  • Os يطابق جميع ملفات *.ll-Os و *.ll-Os_p
  • Oz يطابق جميع ملفات *.ll-Oz و *.ll-Os_z
  • prod يطابق جميع ملفات *_p
  • any تطابق جميع الملفات
• يتم استخدام خيار -c لتحديد المدقق الذي يجب تشغيله ، أحد:
  • uninit : مدقق ذاكرة غير مهتم
  • heapoob : malloc oob checker
  • concroob : فهرس سلبي OOB CHECKER
  • userinput : مدقق إدخال المستخدم

مثال

للعثور على خطأ الوصول إلى الذاكرة غير الملموسة التي وجدت أدائنا في مكتبة Prio Firefox:

 $ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p

الأداة أعلام اثنين من الأخطاء. دعونا نلقي نظرة على الأول:

 Stack uninit bug
Name "serial_read_mp_array_73"
in 
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]

إذا قمت بفحص وظيفة Serial_Read_MP_Array () ، فإن مسار كتلة BUGGY هو %4 (الكتلة الأولى) إلى %71 ، حيث نستخدم [ %73 ].

يساعد

لم نختبر (ومن المحتمل ألا يختبرنا) SYS على أي شيء سوى قوس Linux. يسعدنا دمج التصحيحات التي تضيف دعمًا لأنظمة أنظمة أخرى وإنشاء أنظمة أخرى!

هيكل الدليل

 ├── app            -- Executable used to run the checkers
├── src
│   ├── Checkers   -- Static and symbolic checkers
│   ├── Control    -- Logging helpers
│   ├── LLVMAST    -- LLVM AST interface
│   ├── InternalIR -- Internal IR used to represent paths for both static and symex
│   ├── Static     -- Static checker DSL
│   └── Symex      -- Symbolic DSL and execution engine
├── community      -- Community files
└── test           -- Tests