آشنایی با Frama-C، ابزاری برای تست کد C

Frama-C یک پلتفرم اختصاصی و قابل گسترش برای آنالیز سورس کد زبان C است.Frama-C یک سری تکنیک های آنالیز ایستا را در یک فریمورک گرد هم آورده. این رویکرد Frama-C باعث شده که آنالیزگرها از نتایج از پیش محاسبه شده یکدیگر استفاده کنند و به لطف این رویکرد ابزارهای پیچیده ای همچون آنالیز وابستگی و Slicer در Frama-C ارائه میشوند.این ابزار برای سیستم عامل های Mac و لینوکس ارائه شده و از طریق ابزار Cygwin و یا WIndows Subsystem for Linux در ویندوز نیز قابل استفاده است. توضیحات اینجانب بر اساس اجرای Frama-C بر روی Ubuntu 19.10 Eoan Ermine است اما قابل اجرا بر روی نسخه های قبل تر نیز میباشد.پلاگینی برای افزودن پشتیبانی از ++CFrama-Clang یک پلاگین است که Frama-C را قادر میکند تا برنامه های C++ را به عنوان ورودی بگیرد.این پلاگین همانطور که از نامش پیداست، مبتنی بر clang compiler است.آپدیت کردن پکیج های سیستم عامل:دستورات زیر به ترتیب وارد میشوند.sudo apt-get update sudo apt-get upgradeدستور اول برای گرفتن اطلاعات پکیج ها از منابع مشخص شده در فایل /etc/apt/sources.list و دستور دوم برای نصب آپدیت پکیج های از پیش نصب شده روی سیستم است.نصب opam و Frama-Cبرای نصب frama-c روش opam انتخاب شده. Opam یک Package Manager برای OCamle است. برای نصب opam از دستور زیر استفاده میشود:sudo apt-get install opamFrama-c یک سری dependency های غیر OCamle ای از جمله Gtk و GMP دارد. در بسیاری از سیستم ها opam میتواند این وابستگی های خارجی را با پلاگین depext فراهم کند. برای استفاده از depext اینگونه عمل میکنیم:opam install depext opam depext frama-cاگر سیستم توسط depext پشتیبانی نشود باید Gtk, GtkSourceView, GnomeCanvas و GMP جداگانه نصب شوند.بعد از نصب وابستگی ها، خود frama-c با دستور زیر نصب میشود:opam install frama-c اجرای رابط کاربری گرافیکی Frama-Cبا وارد کردن دستور frama-c-gui در ترمینال میتوان رابط کاربری گرافیکی یا gui این برنامه را اجرا کرد.در زمان اجرای frama-c-gui ممکن است با خطای زیر مواجه شوید:Gtk-Message: Failed to load module "canberra-gtk-moduleخطای بالا به احتمال فراوان با دستور زیر رفع میشود:sudo apt-get install libcanberra-gtk*ممکن است حین اجرای دستور بالا با خطایی بدین شکل مواجه شوید:E: Could not get lock /var/lib/dpkg/lock - frontend – open (11: Resource temporarily unavailable)در این صورت با دستور زیر process ها را بسته و دوباره کد نصب libcanberra-gtk را وارد میکنید:sudo killall apt apt-getاگر دوباره ارور قبلی را دریافت کردید ری استارت کردن را امتحان کنید.در صورتی که باز هم این مشکل را داشتید طبق این آموزش پیش بروید (و اگر سوالی داشتید در قسمت نظرات بپرسید).شروع کار با Frama-C و استفاده از Call Graphبرای افزودن پروژه (سورس برنامه) از تب Project گزینه New Project را فشرده و فایل سورس کد را انتخاب میکنیم.این سورس کدی است که در این آزمون استفاده شده (محاسبه بزرگترین مقسوم علیه مشترک و کوچکترین مضرب مشترک):#include <stdio.h> long gcd(long, long); int unused; int test; int main() { long x, y, hcf, lcm; printf(&quotEnter two integers:\n&quot); scanf(&quot%ld%ld&quot, &x, &y); hcf = gcd(x, y); lcm = (x*y)/hcf; printf(&quotGreatest common divisor of %ld and %ld = %ld\n&quot, x, y, hcf); printf(&quotLeast common multiple of %ld and %ld = %ld\n&quot, x, y, lcm); return 0; } long gcd(long x, long y) { if (x == 0) { return y; } while (y != 0) { if (x > y) { x = x - y; } else { y = y - x; } } return x; }یکی از ساده ترین کاربردهای Frama-C استخراج Call Graph برنامه است که میتوانیم از طریق آن فراخوانی های توابع را مشاهده کنیم. برای مشاهده Call graph کل برنامه، گزینه Show entire callgraph از تب Analyses و برای مشاهده callgraph تابع انتخاب شده، گزینه show callgraph from current function را انتخاب میکنیم.Call graphلیست آنالیزهای Frama-Cلیست کامل آنالیزهای Frama-C که از طریق گزینه Analyses در تب Analyses در دسترس هستند در تصویر زیر قابل مشاهده است:Frama-C Analysesآنالیز Usersاین آنالیز توابع فراخوانی شده، printf ها و scanf های یک تابع را نشان میدهد. نتیجه را در تب کنسول پایینِ برنامه میتوانید مشاهده کنید.Frama-C Users آنالیز inoutورودی ها و خروجی های تابع را آنالیز کرده و از EVA نیز استفاده میکند. EVA هم یک سری Assertion به سورس کد برنامه می افزاید (دایره های نارنجی در عکس پایین). با EVA در ادامه پست آشنا میشوید.inout and EVA analyses آنالیز PDGگراف وابستگی برنامه یا Program Dependence Graph، گرافی است که وابستگی های کنترلی و داده ای statement ها به یکدیگر را نشان میدهد. برای استخراج PDG سورس کد در قالب فایل dotو تبدیل آن به pdf بدین صورت عمل میکنیم:1: در مسیری که سورس کد وجود دارد کلیک راست کرده و open in terminal را میزنیم.2: دستورهای زیر را وارد میکنیم. به جای file.c نام فایل خود را تایپ میکنیم.در دستور دوم به جای pdg در pdg.pdf، نام دلخواه خود را تعیین میکنیم.frama-c -pdg -pdg-dot graph -pdg-print file.c > pdg.dot dot -Tpdf graph.main.dot > pdg.pdfPDGآنالیز Postdominatorsاین آنالیز با scanf و printf مشکل دارد. برای استفاده از این آنالیز یک راه حل، ورودی را دستی وارد کردن ( استفاده نکردن از scanf ) و استفاده از return به جای printf است، یک راه دیگر کامنت کردن دستورات scanf و printf است.به جای file.c نام فایل سورس کد را وارد میکنیم. برای نمایش postdominators هر تابع در قالب pdf از دستورات دوم و سوم استفاده شده. دستور دوم postdominators تابع gcd برنامه نمونه را فراهم میکند و دستور سوم postdominators تابع main را.frama-c file.c -dot-postdom main dot -Tpdf main.gcd.dot > gcdPostdominators.pff dot -Tpdf main.main.dot > mainPostdominators.pdfآنالیز WPپلاگین WP یک پیاده سازی فوق العاده از Weakest Precondition calculus برای برنامه های annotated به زبان C است. یکی از مزیت های WP این هست که مثل Jessie کد C را به Why کامپایل نمیکند و به همین خاطر مشکلی نیست که نتایج WP با تکنیک های دیگری همچون Eva plug-in ترکیب شود.به طور پیشفرض، WP Plug-in هیچ proof obligation ای مبنی بر وجود نداشتن runtime errors (خطاهای زمان اجرا) تولید نمیکند. وجود نداشتن خطاهای زمان اجرا میتواند توسط تکنیک های دیگری (برای مثال Eva plug-in) یا با تولید تمام annotation های ضروری توسط RTE Plug-in ثابت شود.پلاگین WP در Frama-c از پلتفرم Why3 برای اجرای external prover ها استفاده میکند. دلیل استفاده از external prover ها اثبات یا verify کردن ACSL annotations است. پلتفرم Why3 و Alt-Ergo prover به صورت اتوماتیک توسط opam موقع نصب frama-c نصب میشوند.به جز Alt-Ergo این prover ها نیز در سایت Frama-C به عنوان Prover های پیشنهادی و بهینه معرفی شده اند: CVC4 و Z3Z3 ارائه شده توسط Microsoft Research و تحت لیسانس MIT است. Z3 برای بسیاری زبان های برنامه نویسی از جمله Python, Java, C++, .NET و ...Binding دارد. Why3 بعد از نصب باید Config )پیکربندی) بشود تا برای Frama-C/WP در دسترس قرار گیرد. این پیکربندی با دستور زیر انجام میشود:Why3 config -detectWP هم از طریق GUI و هم batch mode (Terminal) قابل دسترسی است. از دستور frama-c -wp gcdlcm.c برای اجرای wp در batch mode استفاده کردیم و نتیجه زیر حاصل شد. (gcdlcm.c نام برنامه مورد نظر است)WP Pluginاگر با خطای زیر مواجه شدید اول با اجرای دستور opam install alt-ergo altgr-ergo از نصب alt-ergo اطمینان حاصل کنید، و بعد با دستور Why3 config -detect که قبل تر نیز اشاره کردیم پیکربندی را انجام دهید:User Error: No prover in /home/yourusername/.why3.conf corresponds to "alt-ergo"در این سایت میتوانید alt-ergo را امتحان کنید. برش بندی یا Slicingعبارت است از عمل برش بندی برنامه بر اساس یک معیار برش بندی (Slicing Criterion). وقتی برش بندی انجام شود تمام کدهایی که بر روی معیار برش بندی تاثیر مستقیم یا غیرمستقیم دارند در یک برش قرار میگیرند. به جای file.c نام برنامه خود و به جای variable متغیری که میخواهید به عنوان معیار برش تعیین شود را تایپ کنید.frama-c -slice-wr variable file.c > slice.txtاین پلاگین از نتایج پلاگین Value analysis و محاسبات وابستگی های تابع استفاده میکند.آنالیز Metricsاین آنالیز برای ما موارد زیر را محاسبه میکند:• McCabe's cyclomatic complexity• Halstead complexity • Value analysis coverage estimateکد اول آنالیز metrics را انجام داده و در ترمینال نتیجه را نشان میدهد، کد دوم آنالیز را اجرا میکند اما نتیجه را در یک فایل txt ذخیره میکند:frama-c file.c -metrics frama-c file.c -metrics > metrics.txtبرای استفاده از گزینه -metrics-value-cover این پلاگین به نتایج Value analysis نیاز دارد.آنالیز EVAEVA مخفف Evolved Value Analysis است.پلاگین EVA به صورت خودکار variation domain های متغیرهای برنامه را محاسبه میکند و assertion های لازم را اضافه میکند.این پلاگین هم در GUI و هم در batch mode قابل استفاده است.دستور اجرای EVA در ترمینال:frama-c -eva file1.c EVA Plug-inدستور اجرای همزمان EVA روی دو فایل:frama-c -eva file1.c file2.cنتایج EVA توسط بسیاری از پلاگین ها استفاده میشود.محدودیت ها: فراخوانی های بازگشتی در حال حاظر پشتیبانی نمیشوند و فقط کد Sequential میتواند آنالیز شود.آنالیز Rte:annotation پلاگینی است برای ساخت خطاهای زمان اجرای معمول، overflow های عملیات های unsigned integer و function contracts inlining در محل های فراخوانی (call sites)این پلاگین نیز همانند بسیاری از پلاگین ها هم از طریق GUI و هم batch mode قابل استفاده است.نتیجه استفاده در gui با فعال بودن تمام گزینه ها:RTE Plug-inاستفاده معمولی از Rte:frama-c -rte file.cبرای تولید همه ی annotation های همه توابع، از جمله function contracts inlining از دستور زیر استفاده میشود:frama-c -rte -rte-unsigned-ov file.cبرای اینکه annotation های یک یا چند تابع مشخص از برنامه را تولید کنیم از کد زیر استفاده میکنیم:frama-c -rte -rte-select function1,function 2 file.cیکی از محدودیت های RTE این است که هیچ contract ای در محل های فراخوانی توابعی که از طریق pointer صدا زده شده اند تولید نمیشود.آنالیز Sparecodeاین پلاگین کار حذف کدهای غیرضروری در برنامه را انجام میدهد. Statement ها و توابعی که برای محاسبه نتیجه برنامه لازم نیستند توسط کد زیر حذف میشوند:Frama-c -sparecode-analysis file.cکد زیر هم متغیرهای سراسری و type های تعریف شده اما استفاده نشده را حذف میکند و کد جدید (بدون آن موارد استفاده نشده را) در یک فایل txt ذخیره میکند:Frama-c -sparecode-rm-unused-globals file.c > sparecode.txtکد برنامه را تغییر دادیم و دو دستور غیرضروری و بدون کاربرد را اضافه کردیم. یک متغیر سراسری تعریف کردیم به نام test و در تابع gcd مقدار y را در متغیر test قرار دادیم. برای اجرای این آنالیز از طریق gui گزینه Analyses را از تب Analyses انتخاب کرده و سپس از لیست گزینه sparecode را انتخاب میکنیم.