آشنایی با 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 است اما قابل اجرا بر روی نسخه های قبل تر نیز میباشد.

• پلاگینی برای افزودن پشتیبانی از ++C

Frama-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 opam

Frama-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 را انتخاب میکنیم.

• لیست آنالیزهای Frama-C

لیست کامل آنالیزهای Frama-C که از طریق گزینه Analyses در تب Analyses در دسترس هستند در تصویر زیر قابل مشاهده است:

• آنالیز Users

این آنالیز توابع فراخوانی شده، printf ها و scanf های یک تابع را نشان میدهد. نتیجه را در تب کنسول پایینِ برنامه میتوانید مشاهده کنید.

• آنالیز inout

ورودی ها و خروجی های تابع را آنالیز کرده و از EVA نیز استفاده میکند. EVA هم یک سری Assertion به سورس کد برنامه می افزاید (دایره های نارنجی در عکس پایین). با EVA در ادامه پست آشنا میشوید.

• آنالیز 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.pdf

• آنالیز 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 و Z3

Z3 ارائه شده توسط Microsoft Research و تحت لیسانس MIT است. Z3 برای بسیاری زبان های برنامه نویسی از جمله Python, Java, C++, .NET و ...Binding دارد.

Why3 بعد از نصب باید Config )پیکربندی) بشود تا برای Frama-C/WP در دسترس قرار گیرد. این پیکربندی با دستور زیر انجام میشود:

Why3 config -detect

WP هم از طریق GUI و هم batch mode (Terminal) قابل دسترسی است.

از دستور frama-c -wp gcdlcm.c برای اجرای wp در batch mode استفاده کردیم و نتیجه زیر حاصل شد. (gcdlcm.c نام برنامه مورد نظر است)

اگر با خطای زیر مواجه شدید اول با اجرای دستور 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 نیاز دارد.

• آنالیز EVA

EVA مخفف Evolved Value Analysis است.

پلاگین EVA به صورت خودکار variation domain های متغیرهای برنامه را محاسبه میکند و assertion های لازم را اضافه میکند.

این پلاگین هم در GUI و هم در batch mode قابل استفاده است.

دستور اجرای EVA در ترمینال:

frama-c -eva file1.c 

دستور اجرای همزمان 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:

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 را انتخاب میکنیم.