تحلیل تخصیص قطعی

در علم کامپیوتر، تحلیل تخصیص قطعی، یک تحلیل جریان داده است که توسط کامپایلرها استفاده می شود تا به طور محافظه کارانه اطمینان حاصل شود که یک متغیر یا مکان همیشه قبل از آن که استفاده شود، اختصاص داده شده باشد.

انگیزه[ویرایش]

در برنامه های C و C++، یک منبع خطاهایی که تشخیص آنها دشوار است، رفتار غیرقطعی است که از خواندن متغیرهایی که مقدار دهی اولیه نشده اند، حاصل می شود. این رفتار می تواند بین پلت فرم ها، ساخت ها و حتی از اجرایی تا اجرای دیگر متفاوت باشد.

برای حل این مسئله دو روش معمول وجود دارد. یک روش این است که اطمینان حاصل شود که همه مکان ها قبل از خوانده شدن نوشته شده اند. قضیه رایس ثابت می کند که این مسئله به طور کلی برای کلیه برنامه ها قابل حل نیست. با این وجود، می توان تحلیل محافظه کارانه ای (نادقیق) ساخت که فقط برنامه هایی را که این محدودیت را برآورده می کنند بپذیرد، در حالی که برخی از برنامه های صحیح را رد می کند. تحلیل تخصیص قطعی چنین تحلیلی است. خصوصیات زبان برنامه نویسی جاوا^[۱] و C#^[۲] مستلزم آن است که در صورت عدم موفقیت تحلیل، کامپایلر یک خطای زمان کامپایل گزارش کند. هر دو زبان به یک شکل خاص از تحلیل نیاز دارند که با جزئیات دقیق بیان شده است. در جاوا ، این تحلیل که توسط Stärk و همکاران^[۳] رسمیت یافت، برخی از برنامه های صحیح رد شده و باید برای معرفی تخصیص های غیر ضروری صریح تغییر یابند. در C#، این تحلیل که توسط Fruja رسمیت یافت، دقیق و همچنین صحیح است، به این معنا که تمام متغیرهای اختصاص داده شده درطول جریان کنترل قطعاً اختصاص داده شده در نظر گرفته می شوند.^[۴] زبان Cyclone نیز برای سهولت در انتقال برنامه های C، برنامه ها را مستلزم می کند که برای متغیرهایی که از نوع اشاره گر هستند یک تحلیل تخصیص قطعی انتقال(pass) دهند.^[۵]

روش دوم حل مسئله این است که به صورت خودکار تمام مکانها را به مقداری ثابت و قابل پیش بینی در نقطه ای که آنها تعریف شده اند، مقدار دهی اولیه شوند. اما این کار تخصیص های جدیدی معرفی می کند که ممکن است موجب تأخیر در عملکرد شوند. در این حالت، تحلیل تخصیص قطعی یک بهینه سازی کامپایلر فراهم می کند که در آن تتخصیص های زائد - تخصیص هایی که به دنبال آن ها تخصیص هایی دیگر می آیند، بدون آن که بین آن ها امکان خوانده شدن وجود داشته باشد - می توانند حذف شوند. در این حالت، هیچ برنامه ای رد نمی شود، اما برنامه هایی که برای آن ها تحلیل موفق نمی شود که تخصیص قطعی را تشخیص دهد، ممکن است حاوی تخصیص های زائد باشند. زیرساخت زبان مشترک به این رویکرد متکی است.^[۶]

اصطلاحات[ویرایش]

می توان گفت یک متغیر یا مکان در هر نقطه از برنامه در یکی از سه حالت قرار دارد:

اختصاص داده شده قطعی: این متغیر با اطمینان اختصاص داده شده است.
اختصاص داده نشده قطعی: این متغیر با اطمینان اختصاص داده نشده است.
ناشناس: ممکن است متغیر اختصاص داده شود یا نشده باشد. تحلیل به اندازه کافی دقیق نیست تا مشخص کند کدام یک است.

تحلیل[ویرایش]

آنچه در زیر آمده است بر مبنای رسمی سازی Fruja برای تحلیل تخصیص قطعی (تک روش) C# است، که وظیفه دارد تضمین کند که همه متغیرهای محلی قبل از آن که استفاده شوند،

اختصاص داده شده باشند. این روش همزمان تحلیل تخصیص قطعی و انتشار مداوم مقادیر بولی را همزمان انجام می دهد.^[۴] پنج تابع استاتیک را تعریف می کنیم:

نام	دامنه	تعریف
before	تمام عبارات و گزاره ها	متغیرها قطعا قبل از ارزیابی عبارت یا بیان داده شده اختصاص داده می شوند.
after	تمام عبارات و گزاره ها	متغیرها قطعا پس از ارزشیابی عبارت داده شده،اختصاص داده شده اند، با فرض این که عبارت به صورت معمول کامل می شود.
vars	تمام عبارات و گزاره ها	کلیه متغیرهای موجود در محدوده عبارت یا گزاره داده شده.
true	تمام عبارات بولی	متغیرها قطعا پس از ارزشیابی عبارت داده شده،اختصاص داده شده اند، با فرض این که عبارت به "درست" ارزشیابی می شود.
false	تمام عبارات بولی	متغیرها قطعا پس از ارزشیابی عبارت داده شده،اختصاص داده شده اند، با فرض این که عبارت به "نادرست" ارزشیابی می شود.

ما معادلات جریان داده ای را ارائه می دهیم که مقادیر این توابع را برای عبارات و گزاره های برحسب مقادیر تابع برای زیرعبارات نحوی آنها، تعریف می کند. فرض کنید هیچ یک از گزاره های goto ،break، continue ،return و مدیریت استثنا وجود ندارند. در زیر چند نمونه از این معادلات آورده شده است:

هر عبارت یا گزاره e که بر مجموعه متغیرهایی که قطعاً اختصاص داده شده اند تأثیر نمی گذارد: $before(e)=after(e)$
فرض کنید e گزاره ی تخصیص $loc=v$ باشد. آنگاه $before(v)=before(e)$ و $after(e)=after(v)\bigcup \{loc\}$
فرض کنید e عبارت true باشد. آنگاه $true(e)=before(e)$ و $false(e)=vars(e)$ . به عبارت دیگر، اگر ارزش عبارت e نادرست باشد، تمام متغیرها اختصاص داده شده اند، زیرا e هم ارزش با نادرست نیست.
از آنجا که آرگومانهای تابع از چپ به راست ارزیابی می شوند، $before(arg_{i+1})=after(arg_{i})$ . بعد از پایان یافتن یک تابع، متغیر های خروجی قطعأ تخصیص داده شده اند.
فرض کنید s گزاره ی while به صورت $s_{1}$ (while(e باشد. آنگاه $before(e)=before(s)$ و $before(s_{1})=true(e)$ و $after(s)=false(e)$
و غیره ...

در ابتدای متد، هیچ متغیر محلی قطعی اختصاص داده شده نیست. تأییدکننده بارها درخت نحو انتزاعی را پیمایش می کند و از معادلات جریان داده برای انتقال اطلاعات بین مجموعه ها استفاده می کند تا به یک نقطه ثابت برسد. سپس، تأییدکننده مجموعه before را برای هر عبارتی که از یک متغیر محلی استفاده می کند، بررسی می کند تا اطمینان حاصل کند که آن متغیر را شامل می شود.

این الگوریتم با معرفی پرش های کنترل جریان مانند goto ،break، continue ،return و مدیریت استثنا پیچیده می شود. هر گزاره ای که می تواند هدف یکی از این پرش ها باشد باید مجموعه before برای آن با مجموعه ی متغیرهای اختصاص داده شده قطعی در منبع پرش اشتراک داشتع باشد. هنگامی که اینها معرفی شدند ، جریان داده حاصل ممکن است دارای چندین نقطه ثابت باشد، مانند این مثال:

int i=1;
L;
goto L;

از آنجا که به برچسب L از دو مکان می توان رسید ، معادله کنترل جریان برای goto بیان می کند که $before(2)=after(1)$ با $before(3)$ اشتراک دارد. اما $before(3)=before(2)$ ،پس
$before(2)=after(1)$ با $before(2)$ . این برای $before(2)$ دو نقطه ثابت دارد، $\{i\}$ و مجموعه ی تهی. با این وجود می توان نشان داد که به دلیل شکل یکنواخت معادلات جریان داده، یک نقطه ثابت ماکسیمال یکتا (نقطه ثابت از بزرگترین اندازه) وجود دارد که بیشترین اطلاعات ممکن را در مورد متغیرهای اختصاص داده شده قطعی ارائه می دهد. چنین نقطه ماکسیمالی (یا ماکزیمم) ممکن است توسط تکنیک های استاندارد محاسبه شود. به Data-flow analysis مراجعه کنید.

منابع[ویرایش]

↑ J. Gosling; B. Joy; G. Steele; G. Bracha. "The Java Language Specification, 3rd Edition". pp. Chapter 16 (pp.527&ndash, 552). Retrieved December 2, 2008.صفحه پودمان:Citation/CS1/en/styles.css محتوایی ندارد.
↑ "Standard ECMA-334, C# Language Specification". ECMA International. pp. Section 12.3 (pp.122&ndash, 133). Retrieved December 2, 2008.صفحه پودمان:Citation/CS1/en/styles.css محتوایی ندارد.
↑ Stärk, Robert F.; E. Borger; Joachim Schmid (2001). Java and the Java Virtual Machine: Definition, Verification, Validation. Secaucus, NJ, USA: Springer-Verlag New York, Inc. pp. Section 8.3. ISBN 3-540-42088-6.صفحه پودمان:Citation/CS1/en/styles.css محتوایی ندارد.
↑ ^۴٫۰ ^۴٫۱ خطای لوآ در پودمان:Citation/CS1/en/Identifiers در خط 47: attempt to index field 'wikibase' (a nil value).
↑ "Cyclone: Definite Assignment". Cyclone User's Manual. Retrieved December 16, 2008.صفحه پودمان:Citation/CS1/en/styles.css محتوایی ندارد.
↑ "Standard ECMA-335, Common Language Infrastructure (CLI)". ECMA International. pp. Section 1.8.1.1 (Partition III, pg. 19). Retrieved December 2, 2008.صفحه پودمان:Citation/CS1/en/styles.css محتوایی ندارد.

This article "تحلیل تخصیص قطعی" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:تحلیل تخصیص قطعی. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.