تحليل التخصيص المحدد
في علوم الحاسوب ، يُعد تحليل التعيين المحدد تحليلًا لتدفق البيانات تستخدمه المترجمات لضمان تعيين متغير أو موقع دائمًا قبل استخدامه.
تحفيز
في برامج C و C++ ، يُعد السلوك غير الحتمي الناتج عن قراءة المتغيرات غير المهيأة مصدرًا للأخطاء التي يصعب تشخيصها بشكل خاص ؛ ويمكن أن يختلف هذا السلوك بين المنصات والإصدارات وحتى من تشغيل لآخر.
هناك طريقتان شائعتان لحل هذه المشكلة. الأولى هي ضمان كتابة جميع المواقع قبل قراءتها. تنص نظرية رايس على أنه لا يمكن حل هذه المشكلة بشكل عام لجميع البرامج؛ ومع ذلك، من الممكن إنشاء تحليل متحفظ (غير دقيق) يقبل فقط البرامج التي تستوفي هذا الشرط، مع رفض بعض البرامج الصحيحة، ويُعد تحليل التخصيص النهائي أحد هذه التحليلات. تتطلب مواصفات لغتي البرمجة جافا [ 1 ] وسي شارب [ 2 ] أن يُبلغ المُصرّف عن خطأ وقت الترجمة إذا فشل التحليل. تتطلب كلتا اللغتين شكلاً محدداً من التحليل مُفصّلاً بدقة متناهية. في جافا، قام ستارك وآخرون [ 3 ] بصياغة هذا التحليل ، ويتم رفض بعض البرامج الصحيحة ويجب تعديلها لإدخال تخصيصات غير ضرورية صريحة. في سي شارب، قام فروجا بصياغة هذا التحليل، وهو دقيق وسليم، بمعنى أن جميع المتغيرات المُخصصة على طول جميع مسارات تدفق التحكم ستُعتبر مُخصصة نهائياً. [ 4 ] تتطلب لغة Cyclone أيضًا من البرامج اجتياز تحليل التخصيص المحدد، ولكن فقط على المتغيرات ذات أنواع المؤشرات، لتسهيل نقل برامج C. [ 5 ]
الطريقة الثانية لحل المشكلة هي تهيئة جميع المواقع تلقائيًا بقيمة ثابتة يمكن التنبؤ بها عند تعريفها، ولكن هذا يُدخل عمليات إسناد جديدة قد تُعيق الأداء. في هذه الحالة، يُتيح تحليل الإسناد المحدد للمُصرّف تحسينًا يُمكن من خلاله حذف عمليات الإسناد الزائدة - أي عمليات الإسناد التي تليها عمليات إسناد أخرى فقط دون أي قراءات وسيطة مُحتملة . في هذه الحالة، لا يتم رفض أي برامج، ولكن البرامج التي يفشل التحليل في التعرف على الإسناد المحدد فيها قد تحتوي على تهيئة زائدة. تعتمد بنية اللغة المشتركة (CLAN) على هذا النهج. [ 6 ]
مصطلحات
يمكن القول إن المتغير أو الموقع يكون في إحدى ثلاث حالات في أي نقطة معينة من البرنامج:
- تم تعيينها بشكل قاطع : من المعروف على وجه اليقين أن المتغير قد تم تعيينه.
- غير مُخصصة قطعاً : من المعروف على وجه اليقين أن المتغير غير مُخصص.
- غير معروف : قد يكون المتغير معيناً أو غير معين؛ التحليل ليس دقيقاً بما يكفي لتحديد أي منهما.
التحليل
يستند ما يلي إلى صياغة فروجا الرسمية لتحليل التعيين المحدد داخل الإجراءات (الطريقة الواحدة) في لغة C#، وهو المسؤول عن ضمان تعيين جميع المتغيرات المحلية قبل استخدامها. [ 4 ] يقوم هذا التحليل في آنٍ واحد بتحليل التعيين المحدد ونشر القيم المنطقية الثابتة . نُعرّف خمس دوال ثابتة:
| اسم | اِختِصاص | وصف |
|---|---|---|
| قبل | جميع البيانات والتعبيرات | يتم تحديد المتغيرات بشكل قاطع قبل تقييم العبارة أو التعبير المعطى. |
| بعد | جميع البيانات والتعبيرات | يتم تعيين المتغيرات بشكل مؤكد بعد تقييم العبارة أو التعبير المعطى، بافتراض اكتماله بشكل طبيعي. |
| المتغيرات | جميع البيانات والتعبيرات | جميع المتغيرات المتاحة في نطاق العبارة أو التعبير المحدد. |
| حقيقي | جميع التعبيرات المنطقية | يتم تعيين المتغيرات بشكل نهائي بعد تقييم التعبير المعطى، بافتراض أن التعبير يُقيّم إلى صحيح . |
| خطأ شنيع | جميع التعبيرات المنطقية | يتم تعيين المتغيرات بشكل نهائي بعد تقييم التعبير المعطى، بافتراض أن التعبير يُقيّم إلى خطأ . |
نُقدّم معادلات تدفق البيانات التي تُحدّد قيم هذه الدوال في مختلف التعبيرات والعبارات، بدلالة قيم الدوال في تعبيراتها الفرعية. لنفترض مؤقتًا عدم وجود عبارات goto أو break أو continue أو return أو معالجة الاستثناءات . فيما يلي بعض الأمثلة على هذه المعادلات:
- أي تعبير أو عبارة e لا تؤثر على مجموعة المتغيرات المعينة بشكل مؤكد: بعد ( e ) = قبل ( e )
- ليكن e تعبير التعيين loc = v . إذن قبل ( v ) = قبل ( e )، وبعد ( e ) = بعد ( v ) U {loc}.
- لنفترض أن e هي العبارة الصحيحة . عندئذٍ، true ( e ) = before ( e ) و false ( e ) = vars ( e ). بعبارة أخرى، إذا كانت قيمة e تساوي false ، فسيتم تعيين جميع المتغيرات ( بشكل قاطع ) بشكل نهائي، لأن قيمة e لا تساوي false.
- بما أن وسائط الدالة تُقيّم من اليسار إلى اليمين، فإن before( arg i + 1 ) = after( arg i ). بعد اكتمال الدالة، يتم تعيين معلمات الإخراج بشكل نهائي.
- لنفترض أن s هي العبارة الشرطية إذا ( e ) s1 وإلا s2 . عندئذٍ قبل ( e ) = قبل ( s )، قبل ( s1 ) = صحيح ( e )، قبل ( s2 ) = خطأ ( e )، وبعد ( s ) = بعد ( s1 ) يتقاطع بعد ( s2 ) .
- لنفترض أن s هي عبارة حلقة while while ( e ) s 1 . إذن before( e ) = before( s ), before( s 1 ) = true( e ), and after( s ) = false( e ).
- وهكذا دواليك.
في بداية العملية، لا يتم تحديد أي متغيرات محلية بشكل قاطع. يقوم المُدقِّق بالتكرار على شجرة بناء الجملة المجردة ، ويستخدم معادلات تدفق البيانات لنقل المعلومات بين المجموعات حتى الوصول إلى نقطة ثابتة . بعد ذلك، يفحص المُدقِّق المجموعة السابقة لكل تعبير يستخدم متغيرًا محليًا للتأكد من احتوائه على هذا المتغير.
تتعقد الخوارزمية بإضافة قفزات التحكم في التدفق مثل goto و break و continue و return ومعالجة الاستثناءات. أي عبارة يمكن أن تكون هدفًا لإحدى هذه القفزات يجب أن تتقاطع مع مجموعة المتغيرات المُعينة مسبقًا عند مصدر القفزة. عند إضافة هذه القفزات، قد يحتوي تدفق البيانات الناتج على نقاط ثابتة متعددة، كما في هذا المثال:
int i = 1 ;L :انتقل إلى L ؛بما أن الوسم L يمكن الوصول إليه من موقعين، فإن معادلة تدفق التحكم لأمر goto تنص على أن قبل (2) = بعد (1) يتقاطع قبل (3). ولكن قبل (3) = قبل (2)، لذا فإن قبل (2) = بعد (1) يتقاطع قبل (2). يوجد لهذا نقطتان ثابتتان قبل (2)، وهما {i} والمجموعة الفارغة. مع ذلك، يمكن إثبات أنه نظرًا للشكل الرتيب لمعادلات تدفق البيانات، توجد نقطة ثابتة عظمى فريدة (نقطة ثابتة ذات أكبر حجم) توفر أكبر قدر ممكن من المعلومات حول المتغيرات المُخصصة بشكل نهائي. يمكن حساب هذه النقطة الثابتة العظمى (أو القصوى) باستخدام التقنيات القياسية؛ انظر تحليل تدفق البيانات .
ثمة مشكلة إضافية تتمثل في أن قفزة التحكم في التدفق قد تجعل بعض تدفقات التحكم غير قابلة للتنفيذ؛ على سبيل المثال، في جزء التعليمات البرمجية هذا، يتم تعيين المتغير i بالتأكيد قبل استخدامه:
int i ;إذا كان ( j < 0 ) فارجع ؛ وإلا i = j ؛اطبع ( i );تنص معادلة تدفق البيانات لـ if على أن after (2) = after( return ) يتقاطع مع after( i = j ). ولجعل هذا صحيحًا، نُعرّف after ( e ) = vars ( e ) لجميع قفزات تدفق التحكم؛ وهذا صحيح بشكل بديهي بنفس معنى صحة المعادلة false ( true ) = vars ( e )، لأنه من غير الممكن أن يصل التحكم إلى نقطة مباشرة بعد قفزة تدفق التحكم.
مراجع
- ↑ ج. جوسلينج؛ ب. جوي؛ ج. ستيل؛ ج. براخا. "مواصفات لغة جافا، الطبعة الثالثة" . الفصل 16 (الصفحات 527-552) . تاريخ الاطلاع: 2 ديسمبر 2008 .
- ↑ "معيار ECMA-334، مواصفات لغة C#" . ECMA International . القسم 12.3 (الصفحات 122-133) . تم الاطلاع عليه بتاريخ 2 ديسمبر 2008 .
- ^ ستارك، روبرت ف. إي بورجر؛ يواكيم شميد (2001). Java وجهاز Java الظاهري: التعريف والتحقق والتحقق من الصحة . سيكوكس، نيوجيرسي، الولايات المتحدة الأمريكية: Springer-Verlag New York, Inc.، ص. القسم 8.3. رقم ISBN 3-540-42088-6.
- 1 2 فروجا، نيكو ج. (أكتوبر 2004). "صحة تحليل التعيين المحدد في لغة سي شارب" . مجلة تكنولوجيا الكائنات . 3 (9): 29-52 . CiteSeerX 10.1.1.165.6696 . doi : 10.5381/jot.2004.3.9.a2 . تاريخ الاسترجاع: 2008-12-02 .
في الواقع، نثبت أكثر من مجرد الصحة: نُبين أن حل التحليل هو حل مثالي (وليس مجرد تقريب آمن).
- ↑ "سايكلون: مهمة محددة" . دليل مستخدم سايكلون . تم الاطلاع عليه بتاريخ 16 ديسمبر 2008 .
- ↑ "المعيار ECMA-335، البنية التحتية للغة المشتركة (CLI)" . ECMA International . ص. القسم 1.8.1.1 (القسم الثالث، ص. 19) . تم الاطلاع عليه في 2 ديسمبر 2008 .
- تحليل تدفق البيانات
