صحت کامپایلر

از ویکی‌پدیا، دانشنامهٔ آزاد

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

روش‌های صوری[ویرایش]

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

کاملترین نمونه این رویکرد CompCert است که کامپایلر بهینه سازی شده‌ایست که به طور صوری اعتبارسنجی شده و برای یک زیر مجموعه بزرگ از C99 می‌باشد.[۲][۳][۴]

این روشها شامل وارسی مدل، اعتبارسنجی صوری و تولید کامپایلر معناشناخته می‌باشد.[۵]

آزمایش[ویرایش]

آزمایش بخش قابل توجهی از توسعه کامپایلر می‌باشد، که با این حال در نوشته‌ها و کتاب‌ها پوشش کمی روی آن داده می‌شود. نسخه ۱۹۸۶ کتاب Aho, Sethi & Ullman تنها یک بخش از یک صفحه به آزمایش کامپایلر اختصاص داده شده که آن هم بدون هیچ نمونه نامگذاری شده می‌باشد.[۶]

نسخه ۲۰۰۶ این کتاب بخشی مربوط به آزمایشن دارد، اما اهمیت آن را تأکید می کند: "بهینه سازی کامپایلرها آنقدر سخت است که به جرات می توان گفت که هیچ کامپایلر بهینه سازی شده کاملاً عاری از خطا نیست بنابراین ، مهمترین هدف در نوشتن کامپایلر صحیح بودن آن است."[۷]

نسخه ۱۹۹۵ کتاب Fraser & Hanson بخش مختصری از آزمون رگرسیون دارد. کد آن نیز موجود است.[۸]

نسخه ۲۰۰۳ کتاب Bailey & Davidson تست فراخوانی رویه‌ها را پوشش میدهد.[۹] تعدادی از مقالات تأیید می کنند که بسیاری از کامپایلرهای منتشر شده اشکالات قابل توجهی در صحتشان دارند.[۱۰]

نسخه ۲۰۰۷ کتاب Sheridan احتمالاً جدیدترین مقاله ژورنال در مورد آزمایش کامپایلرهای عمومی می باشد.[۱۱]

کامپایلرهای تجاری منطبق بر اعتبارسنجی از [۱۲]Solid Sands [۱۳] ،Perennial و Plum-Hall[۱۴] در دسترس هستند. برای اکثر اهداف، بزرگترین اطلاعات موجود در مورد آزمایش کامپایلرها از مجموعه های اعتبار سنجی Fortran[۱۵] و Cobol[۱۶] در دسترس هستند.

برخی تکنیک‌های معمول دیگر برای آزمایش کامپایلرها عبارتند از فازینگ[۱۷] (که برنامه‌های تصادفی ایجاد می‌کند تا اشکالات کامپایلر را بیابد) و کاهش مورد آزمایشی (که سعی می کند یک مورد آزمایشی پیدا شده را کوچکتر کند تا فهم مشکل و آن مورد آزمایشی راحت تر باشد).[۱۸]

جستارهای وابسته[ویرایش]

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

  1. ↑ De Millo, R. A.; Lipton, R. J.; Perlis, A. J. (1979). "Social processes and proofs of theorems and programs". Communications of the ACM. 22 (5): 271–280. doi:10.1145/359104.359106
  2. ↑ Leroy, X. (2006). "Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant". ACM SIGPLAN Notices. 41: 42–54. doi:10.1145/1111320.1111042
  3. ↑ Leroy, Xavier (2009-12-01). "A Formally Verified Compiler Back-end". Journal of Automated Reasoning. 43 (4): 363–446. arXiv:0902.2137
  4. ↑ "CompCert - The CompCert C compiler". compcert.inria.fr. Retrieved 2017-07-21.
  5. ↑ Stephan Diehl, Natural Semantics Directed Generation of Compilers and Abstract Machines,Formal Aspects of Computing, Vol. 12 (2), Springer Verlag, 2000. doi:10.1007/PL00003929
  6. ↑ Compilers: Principles, Techniques and Tools, infra 1986, p. 731.
  7. ↑ ibid, 2006, p. 16.
  8. ↑ Christopher Fraser; David Hanson (1995). A Retargetable C compiler: Design and Implementation. Benjamin/Cummings Publishing. ISBN 978-0-8053-1670-4., pp. 531–3.
  9. ↑ Mark W. Bailey; Jack W. Davidson (2003). "Automatic Detection and Diagnosis of Faults in Generated Code for Procedure Calls" (PDF). IEEE Transactions on Software Engineering. 29 (11): 1031–1042. CiteSeerX 10.1.1.15.4829. doi:10.1109/tse.2003.1245304. Archived from the original بایگانی‌شده در ۲۸ آوریل ۲۰۰۳ توسط Wayback Machine (PDF) on 2003-04-28. Retrieved 2009-03-24., p. 1040.
  10. ↑ E.g., Christian Lindig (2005). "Random testing of C calling conventions" (PDF). Proceedings of the Sixth International Workshop on Automated Debugging. ACM. ISBN 1-59593-050-7. Archived from the original بایگانی‌شده در ۱۱ ژوئیه ۲۰۱۱ توسط Wayback Machine (PDF) on 2011-07-11. Retrieved 2009-03-24., and Eric Eide; John Regehr (2008). "Volatiles are miscompiled, and what to do about it" (PDF). Proceedings of the 7th ACM international conference on Embedded software. ACM. ISBN 978-1-60558-468-3. Retrieved 2009-03-24.
  11. ↑ Flash Sheridan (2007). "Practical Testing of a C99 Compiler Using Output Comparison" (PDF). Software: Practice and Experience. 37 (14): 1475–1488. doi:10.1002/spe.812. Retrieved 2009-03-24. Bibliography at "http://pobox.com/~flash/compiler_testing_bibliography.html%22.
  12. ↑ "peren.com/pages/products_set.htm". Retrieved 2009-03-13.
  13. ↑ "www.solidsands.nl". Retrieved 2011-01-15.
  14. ↑ "plumhall.com/suites.html" بایگانی‌شده در ۲۰ دسامبر ۲۰۱۹ توسط Wayback Machine. Retrieved 2009-03-13.
  15. ↑ "Source of Fortran validation suite". Retrieved 2011-09-01.
  16. ↑ "Source of Cobol validation suite". Retrieved 2011-09-01.
  17. ↑ Chen, Yang; Groce, Alex; Zhang, Chaoqiang; Wong, Weng-Keen; Fern, Xiaoli; Eide, Eric; Regehr, John (2013). Taming Compiler Fuzzers. Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '13. New York, NY, USA: ACM. pp. 197–208. CiteSeerX 10.1.1.308.5541. doi:10.1145/2491956.2462173. ISBN 9781450320146.
  18. ↑ Regehr, John; Chen, Yang; Cuoq, Pascal; Eide, Eric; Ellison, Chucky; Yang, Xuejun (2012). Test-case Reduction for C Compiler Bugs. Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI '12. New York, NY, USA: ACM. pp. 335–346. doi:10.1145/2254064.2254104. ISBN 9781450312059.
برگرفته از «https://fa.wikipedia.org/w/index.php?title=صحت_کامپایلر&oldid=36065068»