books environment interactions
If you do not find what you're looking for, you can use more accurate words.
تفاعلات البيئة (Info)
تتفاعل البرامج مع بيئتها عن طريق إجراء مكالمات النظام أو تلقي الإشارات وما إلى ذلك. قد تنشأ مشاكل الاتساق عندما يصل التنفيذ إلى مكونات لا تخضع لسيطرة أداة التنفيذ الرمزية (على سبيل المثال، النواة أو المكتبات). خذ بعين الاعتبار المثال التالي:
1 int main() 2 { 3 FILE *fp = fopen("doc.txt"); 4 ... 5 if (condition) { 6 fputs("some data", fp); 7 } else { 8 fputs("some other data", fp); 9 } 10 ... 11 data = fgets(..., fp); 12 }
يفتح هذا البرنامج ملفًا، وبناءً على بعض الشروط، يكتب نوعًا مختلفًا من البيانات إلى الملف. ثم يقرأ البيانات المكتوبة لاحقًا. من الناحية النظرية، سوف ينفذ التنفيذ الرمزي مسارين عند السطر 5 وسيكون لكل مسار من هناك نسخة خاصة به من الملف. وبالتالي، فإن العبارة الموجودة في السطر 11 ستعيد البيانات التي تتوافق مع قيمة "الشرط" في السطر 5. من الناحية العملية، يتم تنفيذ عمليات الملف كمكالمات النظام في النواة، وهي خارجة عن سيطرة أداة التنفيذ الرمزية. الطرق الرئيسية لمواجهة هذا التحدي هي:
تنفيذ المكالمات إلى البيئة مباشرة. ميزة هذا النهج هو أنه سهل التطبيق. العيب هو أن الآثار الجانبية لمثل هذه المكالمات سوف تفسد جميع الحالات التي يديرها محرك التنفيذ الرمزي. في المثال أعلاه، ستعرض التعليمات الموجودة في السطر 11 "بعض البيانات الأخرى للبيانات" اعتمادًا على الترتيب التسلسلي للحالات.
نمذجة البيئة. في هذه الحالة، يقوم المحرك باستدعاء النظام باستخدام نموذج يحاكي آثارها ويحافظ على جميع الآثار الجانبية في التخزين لكل حالة. الميزة هي أن المرء سيحصل على نتائج صحيحة عند تنفيذ البرامج التي تتفاعل مع البيئة بشكل رمزي. العيب هو أن المرء يحتاج إلى تنفيذ والحفاظ على العديد من النماذج التي يحتمل أن تكون معقدة من مكالمات النظام. تستخدم أدوات مثل KLEE، وCloud9 وأخرى. هذا النهج من خلال تطبيق نماذج لعمليات نظام الملفات والمقابس وIPC، إلخ.
تقوية حالة النظام بالكامل. تحل أدوات التنفيذ الرمزية القائمة على الأجهزة الافتراضية مشكلة البيئة عن طريق التلاعب بحالة الآلة الافتراضية بأكملها. على سبيل المثال، في S2E، كل حالة هي لقطة آلة افتراضية مستقلة يمكن تنفيذها بشكل منفصل. يخفف هذا النهج من الحاجة إلى كتابة النماذج المعقدة وصيانتها ويسمح بتنفيذ أي برنامج ثنائي بشكل رمزي. ومع ذلك، فإنه يحتوي على تكلفة غير مباشرة لاستخدام ذاكرة أعلى (قد تكون لقطات آلة افتراضية كبيرة).
