تفسیر انتزاعی

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

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

• در داخل کامپایلرها، برای تجزیه و تحلیل برنامه‌ها که تصمیم بگیرید آیا بعضی بهینه‌سازی‌ها یا تحولات مناسب هستند یا خیر.
• برای اشکال زدایی یا حتی تأیید مجوز برنامه‌ها در برابر اشکالات.

تفسیر انتزاعی توسط دو شریک علوم کامپیوتر فرانسوی، پاتریک کوسوت و رادیا کوسوت در اواخر دهه ۱۹۷۰ رسمیت یافت.^[۱][۲]

بینش

این بخش تفسیر انتزاعی را به وسیله رویدادهای دنیای واقعی بدون مثال‌های محاسباتی نمایش می‌دهد.

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

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

اگر ما فقط به برخی از اطلاعات خاص نیاز داشته باشیم، مثلاً در پرسش "آیا شخصی با سن n در اتاق وجود داشته‌است؟"، نگه داشتن لیستی از همه اسامی و تاریخ تولدها ضروری نیست. ما می‌توانیم بدون از دست دادن دقت، به نگه داشتن لیستی از سن شرکت کنندگان اکتفا کنیم. اگر این کار هم زیاد است، کافی است فقط سن جوانترین و پیرترین فرد را نگه داریم. اگر سؤال در مورد سنی است که به‌طور متوسط کمتر از m یا بالاتر از M است، بنابراین با اطمینان می‌توانیم پاسخ دهیم که هیچ شرکت کننده ای حضور نداشته‌است. در غیر این صورت، ما فقط می‌توانیم بگوییم که نمی‌دانیم.

در مورد محاسبات دقیق که در زمان و حافظه محدود قابل محاسبه نیست (به قضیه رایس و مشکل متوقف کردن مراجعه کنید) از انتزاع استفاده می‌شود تا پاسخ‌های تعمیم یافته مثل شاید را برای سوالاتی که جواب قطعی بله یا قطعاً خیر را نمی‌دانیم به عنوان "بله یا خیر "بسازیم. وقتی که الگوریتم تفسیر انتزاعی نمی‌تواند جواب دقیق را با قطعیت محاسبه کند این روش مشکلات را ساده‌تر می‌کند و برای آنها راه حل‌های خودکار می‌سازد. یک شرط اساسی برای ساختن جواب مبهم این است که بتواند مشکلات را کنترل کند و در عین حال دقت کافی را برای پاسخ به سؤالات مهم حفظ کند (مانند "ممکن است برنامه خراب باشد؟")

تفسیر انتزاعی از برنامه‌های رایانه ای

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

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

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

در عمل انتزاعات باید متناسب با هر دو هدف یک برنامه کامپیوتری یعنی تحزیه و تحلیل و مجموعه ای هدفمند بون باشد. اولین تجزیه خودکار مقیاس بزرگ برنامه‌های کامپیوتری به وسیله تفسیر انتزاعی را می‌توان یک اتفاق تصادفی دانست که منجر به تخریب اولین پرواز موشک Ariane 5 در سال ۱۹۹۶ شد.^[۳]

رسمیت

مثال: انتزاع مجموعه‌های عدد صحیح (قرمز) برای امضای مجموعه‌ها (سبز)

L یک مجموعه مرتب است و، یک مجموعه دقیق نامیده شود همجنین L ′ یک مجموعه مرتب دیگر باشد، به نام یک مجموعه انتزاعی. این دو مجموعه L و L' با تعریف توابع کل که عناصر توابع را از یکی به دیگری ترسیم می‌کند، به یکدیگر مرتبط می‌شوند.

تابع α یک تابع انتزاع است اگر عنصر x را از مجموعهٔ دقیق L به عنصر (x)α را در مجموعه L ′ تصویر کند. عنصر α (x) در L ′ x در L است.

تابع γ d یک تابع دقیق گفته می‌شوداگر عنصر x ′ در مجموعه انتزاعی L ′ به یک عنصر γ (x ′) در مجموعه دقیق L ترسیم شود .. یعنی عنصر γ (x ′) L یک ترسیم دقیق x ′ در L ′ می‌باشد.

مجموعه‌های L ₁، L ₂، L ′ ₁ و L ′ ₂ را در نظر بگیرید. معناشناسی دقیق f یک تابع یکنواخت از L ₁ تا L _{2 است}. تابع f ′ L ′ تا ′ ₂ انتزاع معتبر از f نامیده می‌شود اگر برای هر x ′ L ′ (f ∘ γ)(x′) ≤ (γ ∘ f′)(x′)

معناشناسی برنامه را به‌طور کلی می‌توان به وسیله نقاط ثابت در حضور حلقه‌ها یا روش‌های بازگشتی توصیف کرد. فرض کنید که L یک شبکه کامل است و f یک تابع یکنواخت از L به L می‌باشد. پس هر x' بطوریکه f(x′) ≤ x′ باشد یک انتزاع از نقطه ثابت از f،است، قضیه Knaster-تارسکی.

اکنون می‌خواهیم x' را بدست آوریم. اگر L ′ از ارتفاع محدود، یا حداقل تأیید شرایط زنجیره صعودی (تمام دنباله صعودی در نهایت ثابت هستند)، در این صورت مقداری به عنوان حد ثابت از دنباله صعودی دست آمده به نام x' بصرت زیر وجود دارد: x ′ ₀ = ⊥ (کمترین عنصرL ′)_n) و x′_n+1=f′(x′_n).

در موارد دیگر یافتن این x ′ از طریق اپراتور گسترده‌ای ممکن است^[۴] ∇: برای همه x و y , x y باید بزرگتر مساوی x و y باشد و برای هر رشته y ′ _n، دنباله ای است که توسط x ′ ₀ = و x ′ _{n +1} = x ′ _n ∇ y ′ _n که ثابت در نظر گرفته می‌شود. سپس می‌توانیم y′) را برابر f′(x′_n) در نظر بگیریم.

در برخی موارد، می‌توان انتزاعات را با استفاده از اتصالات Galois (α، γ) تعریف کرد که α در آن از L به L ′ و γ از L ′ به L است. این کار را با فرض وجود بهترین انتزاع انجام می‌دهد که لزوماً نمی‌توان تضمین کرد که بهترینی وجود داشته باشد. مثلاً اگر مجموعه ای از زوج‌های (x , y) از اعداد حقیقی را با محصور کردن چند ضلعی محدب انتزاعی کنیم، هیچ انتزاع بهینه ای نسبت به نسبت به x ² + y ² =۱ موجد نیست.

نمونه‌هایی از دامنه‌های انتزاعی

به هر متغیر x موجود در یک برنامه، فاصله زمانی [L _x ، H _x] را اختصاص می‌دهیم. فرض کنیمبرای هر ٓ در برنامه v(x) را به x برای این فواصل [L _x ، H _x] اختصاص داشته باشیم، از فواصل [L _x ، H _x] و [L _y ، H _y] برای متغیرهای x و y، می‌توان به راحتی فواصل x+y ([L_x+L_y, H_x+H_y] و برای x−y ([L_x−H_y, H_x−L_y]) را اختصاص می‌دهیم. این‌ها انتزاعات دقیق هستند چون مجموعه نتایج احتمالی مثلاً x + y دقیقاً بازه ([L _x + L _y ، H _x + H _y]) است. به همین ترتیب می‌توان روابط پیچیده تری را برای ضرب، تقسیم و غیره بدست آورد و به اصطلاح حسابی بازه ای انجام داد.^[۵]

اکنون اجازه دهید برنامه بسیار ساده زیر را در نظر بگیریم:

y = x;
z = x - y;

ترکیبی از حسابی فاصله (green) و تعدیل تعدیل ۲ در اعداد صحیح (cyan) به عنوان دامنه انتزاعی برای تجزیه و تحلیل یک قطعه ساده از کد C (red: مجموعه‌های بتونی از مقادیر ممکن در زمان اجرا). با استفاده از اطلاعات هماهنگی (0 = حتی، 1 = عجیب و غریب)، یک تقسیم صفر می‌تواند حذف شود. (از آنجا که فقط یک متغیر درگیر است، مسئله رابطه در مقابل دامنه‌های غیر مرتبط در اینجا مسئله ای نیست)

یک چند ضلعی به عنوان مثال محدب ۳ بعدی که مقادیر احتمالی ۳ متغیر را در برخی از برنامه‌ها توصیف می‌کند. هر یک از متغیرها ممکن است صفر باشد، اما هر سه به‌طور همزمان نمی‌توانند صفر باشند. ویژگی دوم را نمی‌توان در حوزه حسابی با فاصله توصیف کرد.

با انواع حسابی معقول، نتیجهٔ z باید صفر باشد. اما اگر محاسبه ای را از x در بازه [۰ ، ۱] شروع کنیم، یکی از zها در بازه [-۱ ، +۱] می‌شود. این مثال نشان می‌دهد با این که هر عملیات به صورت جداگانه انتزاعی بود، ترکیب آنها انتزاعی نیست.

مشکل کاملاً مشهود است: ما رابطه بین x و y را در نظر نگرفتیم. در اصل، این دامنه از فاصله‌ها رابطه بین متغیرها را در نظر نمی‌گیرد پس یک دامنه غیر رابطه ای می‌باشد. دامنه‌های غیر رابطه ای برای اجرای سریع و ساده هستند اما نادرست.

چند نمونه از دامنه‌های انتزاعی عددی رابطه ای عبارتند از:

• روابط کنگره ای در اعداد صحیح^[۶][۷]
• چند ضلعی محدب^[۸] (عکس چپ) - با برخی هزینه‌های محاسباتی بالا
• ماتریس‌های با اختلاف جزئی^[۹]
• «هشت ضلعی‌ها»^[۱۰][۱۱]
• برابری‌های خطی^[۱۲]

و ترکیبات آن (مانند محصول کاسته شده،^[۲] به عنوان تصویر درست).

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

ابزارها

ابزارهای صوتی

ابزارهای صوتی تضمین می‌کنند که که آلارم آنها دقیق و درست است و هرگز اشتباهاً منفی ارایه نمی‌دهند اما با عدم اطمینان ممکن است آلارم‌های اشتباهاً مثبت تولید کنند که سیگنال خطای احتمالی را نمایش می دهدا (زیرا تجزیه و تحلیل ایستا به اندازه کافی دقیق نیست تا خطای احتمالی را از بین ببرد).

• آنالایزر پیشرفته مطلق^[۱۳]
• آستر
• CodeContracts چک کننده استاتیک^[۱۴]
• CodePeer
• CPAchecker
• فرار
• نوسان
• تجزیه و تحلیل ارزش Frama-C
• IKOS^[۱۵]
• آنالایزر جولیا استاتیک برای کدهای جاوا، اندروید و جاوا^[۱۶]
• پنجیلی^[۱۷]
• Polyspace
• درنده^[۱۸]
• وراسکو^[۱۹]

ابزارهای غیر صوتی

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

• کدونار^[۲۰]
• از پوشش جلوگیری می‌کند
• بینش Klocwork ^{[نیازمند شفاف‌سازی]}
• تست C / C ++ Parasoft ^{[نیازمند شفاف‌سازی]}
• پاراتفت جتست ^{[نیازمند شفاف‌سازی]}
• مارمولک قرمز Goanna ^{[نیازمند شفاف‌سازی]}

جستارهای وابسته

• تعبیر استاندارد
• بررسی مدل
• شبیه‌سازی نمادین
• اجرای نمادین
• لیست ابزارهای تجزیه و تحلیل کد استاتیک — شامل هر دو ابزار مبتنی بر تفسیر انتزاعی (صدا) و آگهی تعاملی (نامفهوم) است
• تجزیه و تحلیل برنامه استاتیک — مروری بر روش‌های تحلیل، تفسیر انتزاعی شامل، اما محدود به آنها نیست

منابع

1. Cousot, Patrick; Cousot, Radhia (1977). "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints" (PDF). Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977. ACM Press. pp. 238–252. doi:10.1145/512950.512973.
2. Cousot, Patrick; Cousot, Radhia (1979). "Systematic Design of Program Analysis Frameworks" (PDF). Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979. ACM Press. pp. 269–282. doi:10.1145/567752.567778.
3. Faure, Christèle. "PolySpace Technologies History". Retrieved 3 October 2010.
4. Cousot, P.; Cousot, R. (August 1992). "Comparing the Galois Connection and Widening / Narrowing Approaches to Abstract Interpretation" (PDF). In Bruynooghe, Maurice (ed.). Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP). Lecture Notes in Computer Science. Vol. 631. Springer. pp. 269–296. ISBN 978-0-387-55844-8.
5. Cousot, Patrick; Cousot, Radhia (1976). "Static determination of dynamic properties of programs" (PDF). Proceedings of the Second International Symposium on Programming. Dunod, Paris, France. pp. 106–130.
6. Granger, Philippe (1989). "Static Analysis of Arithmetical Congruences". International Journal of Computer Mathematics. 30 (3–4): 165–190. doi:10.1080/00207168908803778.
7. Philippe Granger (1991). "Static Analysis of Linear Congruence Equalities Among Variables of a Program". In Abramsky, S.; Maibaum, T.S.E. (eds.). Proc. Int. J. Conf. on Theory and Practice of Software Development (TAPSOFT). Lecture Notes in Computer Science. Vol. 493. Springer. pp. 169–192.
8. Cousot, Patrick; Halbwachs, Nicolas (January 1978). "Automatic Discovery of Linear Restraints Among Variables of a Program" (PDF). Conf. Rec. 5th ACM Symp. on Principles of Programming Languages (POPL). pp. 84–97.
9. Miné, Antoine (2001). "A New Numerical Abstract Domain Based on Difference-Bound Matrices". In Danvy, Olivier; Filinski, Andrzej (eds.). Programs as Data Objects, Second Symposium, (PADO). Lecture Notes in Computer Science. Vol. 2053. Springer. pp. 155–172. arXiv:cs/0703073.
10. Antoine Miné (2006). "The Octagon Abstract Domain". Higher Order Symbol. Comput. 19: 31–100. arXiv:cs/0703084. doi:10.1007/s10990-006-8609-1.
11. Clarisó, Robert; Cortadella, Jordi (2007). "The Octahedron Abstract Domain". Science of Computer Programming. 64: 115–139. doi:10.1016/j.scico.2006.03.009.
12. Michael Karr (1976). "Affine Relationships Among Variables of a Program". Acta Informatica. 6 (2): 133–151. doi:10.1007/BF00268497.
13. AbsInt Advanced Analyzer
14. CodeContracts static checker (cccheck)
15. IKOS
16. «Julia Static Analyzer for Java, Android and Java bytecode». بایگانی‌شده از اصلی در ۲۰ دسامبر ۲۰۱۹. دریافت‌شده در ۲۰ دسامبر ۲۰۱۹.
17. "Penjili". Archived from the original on 2014-05-18. Retrieved 2014-05-18.
18. predator
19. Verasco
20. «Codesonar». بایگانی‌شده از اصلی در ۷ دسامبر ۲۰۱۵. دریافت‌شده در ۲۰ دسامبر ۲۰۱۹.

پیوند به بیرون

• یک صفحه وب در مورد تفسیر چکیده توسط پاتریک کاسوت
• مقاله روبرتو بانگارا که نشان می‌دهد چگونه می‌توان آنالیزور استاتیک مبتنی بر تفسیر انتزاعی را برای یک زبان برنامه‌نویسی C مانند
• Symposia Analysis Static , دادرسی که در سریال Springer LNCS ظاهر می‌شود
• کنفرانس تأیید، بررسی مدل و تفسیر چکیده (VMCAI)، وابسته در کنفرانس POPL , رویه‌هایی که در مجموعه Springer LNCS ظاهر می‌شوند

یادداشت‌های سخنرانی

• تفسیر چکیده پاتریک کاسوت. MIT
• یادداشتهای سخنرانی دیوید اشمیت در مورد تفسیر انتزاعی بایگانی‌شده در ۳ آوریل ۲۰۱۶ توسط Wayback Machine
• یادداشت‌های سخنرانی مولر و شوارتزاک در مورد تحلیل برنامه استاتیک
• یادداشت‌های سخنرانی آگوستینو کورتسی در مورد تجزیه و تحلیل برنامه و تأیید صحت
• اسلایدها توسط Grégoire Sutre در هر مرحله از تفسیر انتزاعی با مثالهای بسیاری - همچنین معرفی اتصالات Galois