تنزيل pytea - تنزيل رمز المصدر pytea

pytea

فئات أخرى

Initial release

تنزيل

Pytea: محلل خطأ في شكل Pytorch

صفحة المشروع الورقي

متطلبات

node.js >= 12.x
python >= 3.8
- z3-solver >= 4.8

كيفية التثبيت والاستخدام

 # install node.js
sudo apt-get install nodejs

# install python z3-solver
pip install z3-solver

# download pytea
wget https://github.com/ropas/pytea/releases/download/v0.1.0/pytea.zip
unzip pytea.zip

# run pytea
python bin/pytea.py path/to/source.py

# run example file
python bin/pytea.py packages/pytea/pytest/basics/scratch.py

كيفية البناء

 # install dependencies
npm run install:all
pip install z3-solver

# build
npm run build

الوثائق

إعدادات
بناء وتصحيح
كيفية إضافة واجهة برمجة تطبيقات جديدة

شرح موجز لنتيجة التحليل

يتكون Pytea من اثنين من المحللين.

التحليل عبر الإنترنت: Node.js (TypeScript / JavaScript)
- ابحث عن عدم تطابق الشكل الرقمي المستند إلى المدى وإساءة استخدام حجة API. إذا وجدت Pytea أي خطأ أثناء تحليل الرمز ، فسيتوقف عند هذا الموضع ويبلغ الأخطاء وينتهك قيود المستخدم.
تحليل غير متصل: Z3 / Python
- يتم تمرير القيود التي تم إنشاؤها إلى Z3py. سيقوم Z3 بحل مجموعات القيد لكل مسار وطباعة القيد الأول الذي تم انتهاكه (إذا كان موجودًا).

تنقسم نتيجة المحلل عبر الإنترنت إلى ثلاث فصول:

مسار النجاح المحتمل : لم يعثر المحلل على عدم تطابق الشكل حتى الآن ، ولكن يمكن انتهاك مجموعة القيود النهائية إذا قام Z3 بتحليله عند التفتيش الدقيق.
المسار المحتمل الذي لا يمكن الوصول إليه : وجد المحلل عدم استخدام الشكل أو واجهة برمجة التطبيقات ، ولكن لا تزال هناك قيود على المسار . باختصار ، قيود المسار هي حالة فرع لم يتم حلها ؛ هذا يعني أن المسار المتوقف قد يكون غير قابل للوصول إذا كانت قيود المسار المتبقية لها تناقض. سيتم تمييز هذه الحالات عن التحليل غير المتصلة بالإنترنت .
المسار الفوري الفوري : وجد المحلل خطأً ، ويوقف تحليله على الفور.

التحذير : إذا كان الرمز يحتوي على Pytorch أو واجهات برمجة تطبيقات غيرها الأخرى التي لم ننفذها ، فسوف يرفع إنذارات خاطئة. ومع ذلك ، فإننا نسجل أيضًا كل مكالمة API غير المنفذة. راجع قسم LOGS من النتيجة والبحث الذي يتم إجراء مكالمة API غير المنفذة.

تنقسم النتيجة النهائية للتحليل دون اتصال إلى عدة حالات.

مسار صالح : SMT Solver لم يجد أي خطأ. كل قيد سوف يتم الوفاء به دائمًا.
مسار غير صالح : SMT Solver وجد حالة يمكن أن تنتهك بعض القيود. لاحظ أن هذا لا يعني أن الكود سيتعطل دائمًا ، لكنه وجد حالة متطرفة تعطل بعض عمليات الإعدام.
المسار غير القابل للذات : حقق SMT Solver قيودًا غير قابلة للحل ، ثم مهلة. يمكن تصنيف بعض الصيغ غير الخطية في هذه الحالة.
مسار لا يمكن الوصول إليه : تحتوي القيود الصلبة والمسار على قيود متناقضة ؛ لن يتحقق هذا المسار من البداية.