lart

لارت: أداة التجريد والصقل LLVM

Lart = LLVM أداة التجريد والصقل. الهدف من هذه الأداة هو توفير تحويلات LLVM-to-LLVM التي تنفذ تجريدات البرامج المختلفة. فيما يتعلق بمجموعة التعليمات ، تكون البرامج الناتجة طبيعية ، برامج LLVM ملموسة يمكن تنفيذها وتحليلها. يتم إدراج معلومات إضافية حول التجريد (S) ساريًا على برنامج (شظية) باستخدام وظائف LLVM الداخلية الخاصة وعقد بيانات التعريف LLVM. يوفر LART كلاً من الأداة المستقلة التي تعالج ملفات Bitcode على القرص ، بالإضافة إلى إطار يمكن دمجه في أدوات معقدة قائمة على LLVM. يتمثل الدافع الأساسي وراء LART في توفير "المعالج المسبق" لمدخلات النموذج المستندة إلى LLVM وأدوات التحليل الأخرى ، مما يؤدي إلى تبسيط وظيفتها عن طريق تقليل حجم المشكلة دون المساس بصلة التحليلات. يمكن عادةً تحسين التجريدات التي تنفذها LART بناءً على تعليمات محددة حول أي جزء من التجريد أمر قاسي للغاية (التجريد الذي يكون خشنًا للغاية سيخلق أخطاء زائفة مرئية للتحليلات اللاحقة ولكنها غير موجودة في البرنامج الأصلي).

التجريدات ل LLVM bitcode

الغرض من التمرين بأكمله هو تجريد المعلومات من LLVM Bitcode ، مما يجعل التحليلات اللاحقة أكثر كفاءة (على حساب بعض الدقة). تحقيقًا لهذه الغاية ، نحتاج بشكل أساسي إلى أن نكون قادرين على تشفير الاختيار غير الحتمي في برامج LLVM ، والتي يمكن القيام بها ببساطة من خلال وظيفة متعددة الأغراض (على غرار الوادعيات LLVM). تُسمى الوظيفة @lart.choice ، وتأخذ زوجًا من الحدود كوسائط ولا تُرجع من الناحية المحددة القيمة التي تقع بين تلك الحدود.

يجب التعرف على هذا الامتداد لدلالات LLVM بواسطة أداة المصب. هذا هو أيضًا الانحراف الحاسم الوحيد عن Bitcode LLVM القياسي. ستنفذ العديد من أدوات التحليل بالفعل آلية مماثلة ، إما داخليًا أو حتى مع واجهة خارجية. عادة ما يكون تكييف الأدوات دون دعم لـ @lart.choice للعمل مع Lart واضحًا جدًا.

هناك وظائف أخرى خاصة بالأغراض التي توفرها LART ، وهي عائلة @lart.meta.* فيما يتعلق بهذه التعليمات ، ستكون معظم الأدوات قادرة على تجاهل وجودها بأمان ، تمامًا كما هو الحال مع المكالمات الموجودة @llvm.dbg.* . من المتوقع أن تحتفظ تحولات البرنامج بتلك المكالمات في حالة استدعاء LART لتحسين التجريد (كل تجريد توفره LART يأتي مع إجراء تحسين مقابل ، والذي سيحتاج غالبًا إلى العثور على مكالمات @lart.meta التي يتم إدراجها بواسطة التجريد).

في حين أن معظم محركات التجريد التقليدية تعمل كمترجمين فوريين ، يمكن أيضًا "تجميع" التجريدات في برامج. بدلاً من (إعادة) تعليمات التفسير رمزيًا ، يمكن تجميع التعليمات الرمزية. في حالة التجريد الأصلي ، سيقوم Bitcode الناتج بمعالجة التقييمات الأصلية واستخدامها بشكل مباشر بدلاً من متغيرات الخرسانة. كما هو موضح أعلاه ، فإن الاختلاف المهم هو أن الرمز البري يحتاج إلى اتخاذ خيارات غير حية ، لأن بعض المسندات قد يكون لها تقييمات غير محددة (صحيحة وكاذبة على حد سواء). يمكن أن يتم استخلاص بعض المتغيرات تمامًا ، وستؤدي جميع الاختبارات على مثل هذه المتغيرات إلى إحداث نعم ولا توجد إجابات.

يبني

استخدم أو كرر الإعداد من ./devcontainer/Dockerfile في الوقت الحالي.

ثم استخدم:

 ./scripts/build.sh

تشغيل المترجم

 ./build/bin/lartcc <domain> <compiler arguments> in.c

OPT

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

امتحان

 lit -v build/test

ملاحظة: يجب أن يكون لدى build/lartcc/lartcc رسومات exacutabple.