آنالیز تخصیص قطعی

آنالیز تخصیص قطعی (به انگلیسی: Definite assignment analysis) در علوم کامپیوتر، آنالیز جریان داده‌ای است که توسط کامپایلرها استفاده می‌شود تا به‌طور محافظه کارانه مطمئن شویم که یک متغیر یا آدرس، همیشه قبل از استفاده، تخصیص داده شده باشد.

هدف

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

دو راه متداول برای حل این مشکل وجود دارد. یکی این است که اطمینان حاصل شود که همه‌ی مکان‌ها قبل از خواندن، نوشته شده‌اند. قضیه رایس ثابت می‌کند که این مشکل به طور کلی برای همه‌ی برنامه‌ها قابل حل نیست. با این حال، می‌توان یک تحلیل محافظه کارانه (غیر دقیق) به وجود آورد که فقط برنامه‌هایی را بپذیرد که این محدودیت را برآورده کنند، در حالی که برخی از برنامه‌های صحیح را رد کرد، و تحلیل تخصیص قطعی چنین تحلیلی است. مشخصات زبان برنامه نویسی جاوا و سی شارپ مستلزم آن است که کامپایلر یک خطای زمان کامپایل را در صورت شکست آنالیز، گزارش کند. هر دو زبان به شکل خاصی از تحلیل نیاز دارند که با جزئیات دقیق بیان شده باشد. در جاوا، این تجزیه و تحلیل توسط استارک و همکارانش رسمیت یافت و برخی از برنامه‌های صحیح رد می‌شوند و باید برای معرفی تخصیص غیر ضروری و مشخص تغییر داده شوند. در سی شارپ، این تجزیه و تحلیل توسط Fruja رسمیت یافت، و دقیق و درست است، به این معنا که همه متغیرهای تخصیص داده شده در طول تمام مسیرهای جریان کنترل، به طور قطعی، اختصاص داده شده در نظر گرفته می شوند. زبان سایکلون نیز به برنامه‌ها نیاز دارد که تجزیه و تحلیل تخصیص مشخصی را انجام دهند، اما فقط روی متغیرهایی با انواع پوینتر، تا انتقال برنامه‌های سی آسان شود.

راه دوم برای حل این مشکل این است که همه‌ی مکان‌ها را به یک مقدار ثابت و قابل پیش بینی در نقطه‌ای که در آن تعریف شده اند به طور خودکار مقداردهی کنیم ، اما این وظایف جدیدی را معرفی می کند که ممکن است عملکرد را مختل کند. در این حالت ، تجزیه و تحلیل تکلیف قطعی ، بهینه سازی کامپایلر را امکان پذیر می کند که در آن تکالیف اضافی — تکالیفی که پس از آن تکالیف دیگر دنبال می شوند و هیچ خوانشی احتمالی در آن‌ها وجود ندارد — قابل حذف است. در این مورد ، هیچ برنامه ای رد نمی شود ، اما برنامه‌هایی که تجزیه و تحلیل آن‌ها در تعیین تکلیف مشخص نمی تواند شامل مقداردهی اولیه اضافی باشد. زیرساخت زبان مشترک متکی بر این رویکرد است.

واژه شناسی

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

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

آنالیز

موارد زیر بر اساس رسمی‌سازی Fruja در تجزیه و تحلیل تخصیص قطعی درون رویه‌ای (تک روشی) سی شارپ است، که مسئول اطمینان از تخصیص همه متغیرهای محلی قبل از استفاده از آن‌ها است. آن را به طور همزمان تجزیه و تحلیل تخصیص مشخص و انتشار ثابت مقادیر بولین انجام می‌دهد. ما پنج تابع استاتیک را تعریف می کنیم:

نام	دامنه	توضیح
قبل	تمام عبارات	متغیرهایی که قبل از ارزیابی عبارت، اختصاص داده شده‌اند.
بعد	تمام عبارات	متغیرهایی که قطعاً پس از ارزیابی عبارت، با فرض اینکه به طور معمول کامل شود، اختصاص داده می شوند.
vars	تمام عبارات	همه متغیرهای موجود در محدوده‌ی عبارت داده شده.
درست	تمام عبارات بولین	متغیرهایی که پس از ارزیابی عبارت داده شده، با فرض درست بودن عبارت، قطعاً اختصاص داده می‌شوند.
نادرست	تمام عبارات بولین	متغيرهایی که قطعاً پس از ارزيابي عبارت، با فرض نادرست بودن عبارت، تخصيص داده مي شوند.

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

• هر عبارت e که بر مجموعه متغیرهایی که به طور قطعی اختصاص داده شده‌اند، تأثیر نمی‌گذارد: after(e) = before(e)
• فرض کنید e عبارت تخصیص loc = v باشد. آنگاه before(v) = before(e) و after(e) = after(v) U {loc}.
• فرض کنید e عبارت «درست» باشد. آنگاه true(e) = before(e) و false(e) = vars(e). به عبارت دیگر، اگر e مقدار «نادرست» را بگیرد، همه‌ی متغیرها (به صورت خالی) به طور قطعی اختصاص داده می شوند، زیرا e مقدار «نادرست» را نگرفته است.
• از آنجایی که آرگومان‌های متد از چپ به راست ارزیابی می شوند، before(arg_i + 1) = after(arg_i). پس از تکمیل یک متد، پارامترهای خروجی قطعاً اختصاص داده شده‌اند.
• فرض کنید s عبارت شرطی if (e) s₁ else s₂ باشد. آنگاه before(e) = before(s), before(s₁) = true(e), before(s₂) = false(e), و after(s) = after(s₁) intersect after(s₂).
• فرض کنید s عبارت حلقه‌ی while (e) s₁ باشد. آنگاه before(e) = before(s), before(s₁) = true(e), and after(s) = false(e).
• و غیره ...

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

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

 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} و مجموعه‌ی تهی است. با این حال، می‌توان نشان داد که به دلیل شکل یکنواخت معادلات جریان داده، یک نقطه ثابت ماکسیمال منحصر به فرد (نقطه ثابت با بزرگترین اندازه) وجود دارد که بیشترین اطلاعات ممکن را در مورد متغیرهای قطعی اختصاص داده شده ارائه می‌دهد. چنین ماکسیمال (یا ماکسیمم) نقطه ثابت ممکن است با تکنیک‌های استاندارد محاسبه شود. به تحلیل جریان داده رجوع کنید. یک مسئله دیگر این است که یک پرش جریان کنترلی ممکن است برخی جریان‌های کنترلی را غیرممکن کند. به عنوان مثال، در این قطعه کد، متغیر i قطعا قبل از استفاده، اختصاص داده شده است:

 int i;
 if (j < 0) return; else i = j;
 print(i);

معادله جریان داده برای if می گوید که after(2) = after(return) پس از (i = j) متقاطع می‌شوند. برای اینکه این کار به درستی انجام شود، تعریف می‌کنیم after(e) = vars(e) برای همه‌ی پرش‌های کنترل جریان. این به همان دلیل تایید شده است که معادله false(true) = vars(e) است؛ زیرا امکان ندارد کنترل بلافاصله پس از پرش جریان کنترل، به نقطه‌ای برسد.