تنفيذ رمزي
في علم الحاسوب، يعد التنفيذ الرمزي أو التقييم الرمزي وسيلة لتحليل برنامج لتحديد المدخلات التي تتسبب في تنفيذ كل جزء من البرنامج. يتبع المترجم البرنامج، بافتراض قيم رمزية للمدخلات بدلاً من الحصول على مدخلات فعلية كما يفعل التنفيذ العادي للبرنامج. وبالتالي تصل إلى التعبيرات من حيث تلك الرموز للتعبيرات والمتغيرات في البرنامج، والقيود من حيث تلك الرموز للنتائج المحتملة لكل فرع شرطي.
يطبق مجال المحاكاة الرمزية نفس المفهوم على الأجهزة. يطبق الحساب الرمزي المفهوم على تحليل التعبيرات الرياضية.
مثال
عدلخذ بعين الاعتبار البرنامج أدناه، الذي يقرأ في قيمة ويفشل إذا كان الإدخال 6.
int f() {
...
y = read();
z = y * 2;
if (z == 12) {
fail();
} else {
printf("OK");
}
}
أثناء التنفيذ العادي (التنفيذ «الملموس»)، سيقرأ البرنامج قيمة إدخال ملموسة (على سبيل المثال، 5) ويعينها إلى y. سيتابع التنفيذ بعد ذلك عملية الضرب والفرع الشرطي، والذي سيتم تقييمه إلى خطأ ويطبعOK.
أثناء التنفيذ الرمزي، يقرأ البرنامج قيمة رمزية (على سبيل المثال، λ) ويعينها إلى y. ثم يواصل البرنامج عملية الضرب ويخصص λ * 2 إلى z. عند الوصول إلى جملة if، سيتم تقييم λ * 2 == 12. في هذه المرحلة من البرنامج، يمكن أن تأخذ λ أي قيمة، وبالتالي يمكن أن يستمر التنفيذ الرمزي على طول كلا الفرعين، عن طريق «توجيه» مسارين. يحصل كل مسار على نسخة من حالة البرنامج في تعليمات الفرع بالإضافة إلى قيد المسار.
في هذا المثال، قيد المسار هو λ * 2 == 12 للفرع then وλ * 2 != 12 للفرع else. يمكن تنفيذ كلا المسارين بشكل رمزي بشكل مستقل. عندما تنتهي المسارات (على سبيل المثال، نتيجة لتنفيذ fail() أو الخروج ببساطة)، يحسب التنفيذ الرمزي قيمة محددة لـ λ عن طريق حل قيود المسار المتراكمة على كل مسار. يمكن اعتبار هذه القيم الملموسة بمثابة حالات اختبار ملموسة يمكن، على سبيل المثال، مساعدة المطورين على إعادة إنتاج الأخطاء. في هذا المثال، سيحدد خلال القيد أنه من أجل الوصول إلى عبارة fail()، يجب أن λ تساوي 6.
محددات
عدلانفجار المسار
عدللا يتناسب تنفيذ جميع مسارات البرامج الممكنة بشكل رمزي مع البرامج الكبيرة. يزداد عدد المسارات الممكنة في البرنامج بشكل كبير مع زيادة حجم البرنامج ويمكن أن يكون لانهائي في حالة البرامج ذات التكرارات غير المحدودة.[1] تستخدم حلول مشكلة انفجار المسار بشكل عام إما الاستدلال لإيجاد المسار لزيادة تغطية الشيفرة،[2] أو تقليل وقت التنفيذ عن طريق موازنة المسارات المستقلة،[3] أو عن طريق دمج مسارات مماثلة.[4]
الكفاءة المعتمدة على البرنامج
عدليتم استخدام التنفيذ الرمزي للتفكير في برنامج مسار عن طريق وهو ميزة تفوق التفكير حول إدخال برنامج من خلال الإدخال مثل نماذج الاختبار الأخرى التي تستخدمها (مثل تحليل البرنامج الديناميكي). ومع ذلك، إذا سلك عدد قليل من المدخلات نفس المسار من خلال البرنامج، فلن يكون هناك الكثير من التوفير مقارنة باختبار كل مدخل على حدة.
تعرج الذاكرة
عدليكون التنفيذ الرمزي أكثر صعوبة عندما يمكن الوصول إلى موقع الذاكرة نفسه من خلال أسماء مختلفة (استرداف). لا يمكن دائمًا التعرف على الاسم المستعار بشكل ثابت، لذلك لا يمكن لمحرك التنفيذ الرمزي التعرف على أن التغيير في قيمة أحد المتغيرات يغير أيضًا الآخر.[5]
مصفوفات
عدلنظرًا لأن المصفوفة عبارة عن مجموعة من العديد من القيم المميزة، يجب على المنفذين الرمزية إما التعامل مع المصفوفة بأكملها كقيمة واحدة أو معاملة كل عنصر من عناصر المصفوفة كموقع منفصل. المشكلة في معالجة كل عنصر من عناصر المصفوفة بشكل منفصل هي أنه يمكن تحديد مرجع مثل "[A [i" ديناميكيًا فقط، عندما تكون قيمة i ذات قيمة محددة.[5]
تفاعلات البيئة
عدلتتفاعل البرامج مع بيئتها عن طريق إجراء مكالمات النظام أو تلقي الإشارات وما إلى ذلك. قد تنشأ مشاكل الاتساق عندما يصل التنفيذ إلى مكونات لا تخضع لسيطرة أداة التنفيذ الرمزية (على سبيل المثال، النواة أو المكتبات). خذ بعين الاعتبار المثال التالي:
int main()
{
FILE *fp = fopen("doc.txt");
...
if (condition) {
fputs("some data", fp);
} else {
fputs("some other data", fp);
}
...
data = fgets(..., fp);
}
يفتح هذا البرنامج ملفًا، وبناءً على بعض الشروط، يكتب نوعًا مختلفًا من البيانات إلى الملف. ثم يقرأ البيانات المكتوبة لاحقًا. من الناحية النظرية، سوف ينفذ التنفيذ الرمزي مسارين عند السطر 5 وسيكون لكل مسار من هناك نسخة خاصة به من الملف. وبالتالي، فإن العبارة الموجودة في السطر 11 ستعيد البيانات التي تتوافق مع قيمة «الشرط» في السطر 5. من الناحية العملية، يتم تنفيذ عمليات الملف كمكالمات النظام في النواة، وهي خارجة عن سيطرة أداة التنفيذ الرمزية. الطرق الرئيسية لمواجهة هذا التحدي هي:
تنفيذ المكالمات إلى البيئة مباشرة. ميزة هذا النهج هو أنه سهل التطبيق. العيب هو أن الآثار الجانبية لمثل هذه المكالمات سوف تفسد جميع الحالات التي يديرها محرك التنفيذ الرمزي. في المثال أعلاه، ستعرض التعليمات الموجودة في السطر 11 «بعض البيانات الأخرى للبيانات» اعتمادًا على الترتيب التسلسلي للحالات.
نمذجة البيئة. في هذه الحالة، يقوم المحرك باستدعاء النظام باستخدام نموذج يحاكي آثارها ويحافظ على جميع الآثار الجانبية في التخزين لكل حالة. الميزة هي أن المرء سيحصل على نتائج صحيحة عند تنفيذ البرامج التي تتفاعل مع البيئة بشكل رمزي. العيب هو أن المرء يحتاج إلى تنفيذ والحفاظ على العديد من النماذج التي يحتمل أن تكون معقدة من مكالمات النظام. تستخدم أدوات مثل KLEE،[6] وCloud9 وأخرى.[7] هذا النهج من خلال تطبيق نماذج لعمليات نظام الملفات والمقابس وIPC، إلخ.
تقوية حالة النظام بالكامل. تحل أدوات التنفيذ الرمزية القائمة على الأجهزة الافتراضية مشكلة البيئة عن طريق التلاعب بحالة الآلة الافتراضية بأكملها. على سبيل المثال، في S2E، كل حالة هي لقطة آلة افتراضية مستقلة يمكن تنفيذها بشكل منفصل. يخفف هذا النهج من الحاجة إلى كتابة النماذج المعقدة وصيانتها ويسمح بتنفيذ أي برنامج ثنائي بشكل رمزي. ومع ذلك، فإنه يحتوي على تكلفة غير مباشرة لاستخدام ذاكرة أعلى (قد تكون لقطات آلة افتراضية كبيرة).
إصدارات سابقة من الأدوات
عدلتاريخ
عدلتم تقديم مفهوم التنفيذ الرمزي أكاديميًا مع وصف: نظام Select،[9] ونظام EFFIGY،[10] ونظام DISSECT،[11] ونظام Clarke.[12] انظر فهرس يضم المزيد من الأوراق الفنية المنشورة حول التنفيذ الرمزي.
انظر أيضًا
عدلمراجع
عدل- ^ Anand، Saswat؛ Patrice Godefroid؛ Nikolai Tillmann (2008). "Demand-Driven Compositional Symbolic Execution". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. ج. 4963. ص. 367–381. DOI:10.1007/978-3-540-78800-3_28. ISBN:978-3-540-78799-0.
- ^ Ma، Kin-Keng؛ Khoo Yit Phang؛ Jeffrey S. Foster؛ Michael Hicks (2011). "Directed Symbolic Execution". Proceedings of the 18th International Conference on Statis Analysis. ص. 95–111. ISBN:9783642237010. اطلع عليه بتاريخ 2013-04-03.
- ^ Staats، Matt؛ Corina Pasareanu (2010). "Parallel symbolic execution for structural test generation". Proceedings of the 19th International Symposium on Software Testing and Analysis. ص. 183–194. DOI:10.1145/1831708.1831732. ISBN:9781605588230. S2CID:9898522.
- ^ Kuznetsov، Volodymyr؛ Kinder، Johannes؛ Bucur، Stefan؛ Candea، George (1 يناير 2012). "Efficient State Merging in Symbolic Execution". Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, NY, USA: ACM. ص. 193–204. CiteSeerX:10.1.1.348.823. DOI:10.1145/2254064.2254088. ISBN:978-1-4503-1205-9. S2CID:135107.
- ^ ا ب DeMillo، Rich؛ Offutt، Jeff (1 سبتمبر 1991). "Constraint-Based Automatic Test Data Generation". IEEE Transactions on Software Engineering. ج. 17 ع. 9: 900–910. DOI:10.1109/32.92910.
- ^ Cadar، Cristian؛ Dunbar، Daniel؛ Engler، Dawson (1 يناير 2008). "KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs". Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI'08: 209–224. مؤرشف من الأصل في 2018-12-01.
- ^ Turpie، Jonathan؛ Reisner، Elnatan؛ Foster، Jeffrey؛ Hicks، Michael. "MultiOtter: Multiprocess Symbolic Execution" (PDF). مؤرشف من الأصل (PDF) في 2020-07-20.
- ^ Cadar، Cristian؛ Ganesh، Vijay؛ Pawlowski، Peter M.؛ Dill، David L.؛ Engler، Dawson R. (2008). "EXE: Automatically Generating Inputs of Death". ACM Trans. Inf. Syst. Secur. ج. 12: 10:1–10:38. DOI:10.1145/1455518.1455522. S2CID:10905673.
- ^ Robert S. Boyer and Bernard Elspas and Karl N. Levitt SELECT--a formal system for testing and debugging programs by symbolic execution, Proceedings of the International Conference on Reliable Software, 1975,page 234--245, Los Angeles, California
- ^ James C. King,Symbolic execution and program testing, Communications of the ACM, volume 19, number 7, 1976, 385--394
- ^ William E. Howden, Experiments with a symbolic evaluation system, Proceedings, National Computer Conference, 1976.
- ^ Lori A. Clarke, A program testing system, ACM 76: Proceedings of the Annual Conference, 1976, pages 488-491, Houston, Texas, United States
