آموزش ابزار Frama-c برای آزمون نرم افزار

ابزار Frama-C مخفف (Framework for Modular Analysis of C programs) یا (چارچوب برای تجزیه و تحلیل مدولار برنامه های C) که جهت تحلیل کدهای برنامه به زبان c مورد استفاده می باشد.

ابزار Frama-C مجموعه ای از آنالایزرهای برنامه قابل تعامل برای برنامه های C است.به عنوان آنالایزر استاتیک، برنامه ها را بدون اجرای آنها بازرسی می کند.

این ابزار برای سیستم عامل های Mac و لینوکس ارائه شده و از طریق ماشین های مجازی همچون VM،Cygwin و یا WIndows Subsystem for Linux در ویندوز نیز قابل استفاده می باشد.

من از سیستم عامل Ubuntu 18.04 LTS که بر روی VMware نصب کردم استفاده می کنم و آموزش بر اساس این سیستم عامل تهیه کردم

طریقه نصب Frama-c

جهت نصب Frama-c در ubuntu ابتدا terminal را باز میکینم و با استفاده از دستور زیر نصب انجام می شود

sudo apt-get update -y
sudo apt-get install -y frama-c

و تمام، frama-c بر روی سیستم عامل شما نصب شد. اکنون می توانیم به دو صورت از این ابزار استفاده نمایید یکی با استفاده از خط دستور terminal و دیگری محیط گرافیکی ابزار است.

جهت مشاهده ی محیط گرافیکی درون terminal دستور زیر را وارد می نماییم

frama-c-gui

که محیط آن به شکل زیر می باشد

در صورتی که در زمان اجرای frama-c-gui با خطای زیر مواجه شدید

Gtk-Message: Failed to load module "canberra-gtk-module" خطای

با استفاده از این دستور مشکل برطرف می شود

sudo apt-get install libcanberra-gtk*

شروع کار

ما در این بخش به بررسی call graph, inout, users, metrics, pdg, post dominators, slicing, WP بر روی سورس کد زبان C که در ادامه آن را قرار می دهم میپردازیم، هرچند برای تست نرم افزار آیتم های متنوعی وجود دارد اما ما فقط مواردی که گفتیم می پردازیم

سورس برنامه

سورس کدی که ما انتخاب کردیم، مرتب سازی انتخابی (Selection Sort ) می باشد که شامل دو تابع یکی جهت مرتب سازی و دیگر چاپ نتیجه در خروجی است.

#include <stdio.h>
void selection_sort(int a[],int n);
void show_sort_output(int a[],int n);
void main()
{
    int a[30], n;
    int i;
    printf(&quot\nEnter size of an array: &quot);
    scanf(&quot%d&quot, &n);
    printf(&quot\nEnter elements of an array:\n&quot);
    for(i=0; i<n; i++)
        scanf(&quot%d&quot, &a[i]);
    selection_sort(a,n);
    printf(&quot\n\nAfter sorting:\n&quot);
    show_sort_output(a,n);
}
void selection_sort(int a[],int n)
{
    int i, j, min, temp;
    for (i=0; i<n; i++)
    {
        min = i;
        for (j=i+1; j<n; j++)
        {
            if (a[j] < a[min]
                min = j;
        }
        temp = a[i];
        a[i] = a[min];
        a[min] = temp;
    }
}
void show_sort_output(int a[],int n)
{
    int i;
    for(i=0; i<n; i++)
        printf(&quot\n%d&quot, a[i]);
}

برای ورود کد مورد نظر به ابزار در منو Projects گزینه New Project را انتخاب و فایل برنامه مورد نظر را انتخاب می کنیم

نمودار Call graph:

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

با استفاده از محیط گرافیکی:

جهت مشاهده call graph سورس کد خودمان از منوی Analyses گزینه show callgraph را انتخاب می کنیم

نتیجه به شکل زیر می باشد

با استفاده از terminal:

همچنین می توان با استفاده از دستور زیر درون terminal نتیجه را به صورت متنی ذخیره کرد

frama-c-gui -cg call_graph.txt main.c

که call_graph.txt فایل خروجی می باشد و main.c سورس کد برنامه

تست ورودی و خروجی inout:

جهت به دست آوردن ورودی ها و خروجی از هر یک از توابع برنامه مورد استفاده قرار می گیرد

با استفاده از محیط گرافیکی:

برای تهیه inout برنامه ابتدا به منو Analyses رفته سپس بر روی Analyses کلیک کرده و از منوی سمت چپ inout را کلیک کرده و مقادیر out, input, inout را انتخاب کرده و نتیجه در کنسول به نمایش در خواهد آمد.

به عنوان مثال بخشی از نتیجه تولید شده در console برای تابع selection_sort به شکل زیر می باشد، که در آن ورودی ها و خروجی های این تابع را بررسی کرده است

[inout] Out (internal) for function selection_sort:
          a[0..29]; i; j; min; temp
[inout] Inputs for function selection_sort:
          a[0..29]
[inout] InOut (internal) for function selection_sort:
        Operational inputs:
          a[0..29]; a; n
        Operational inputs on termination:
          a[0..29]; a; n
        Sure outputs:
          i

با استفاده از terminal:

می توانیم با استفاده از دستور زیر درون terminal نتیجه را به صورت متنی ذخیره کنیم

frama-c -inout main.c > inout.txt

با اجرای دستور بالا همان نتایج تولید شده درون consol در بخش گرافیک ابزار درون فایل inout.txt ذخیره می شوند

آزمون کاربران users:

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

با استفاده از محیط گرافیکی:

برای استفاده از این آزمون در منو Analyses گزینه Analyses را انتخاب کرده و در پنجره باز شده گزینه users را انتخاب میکنیم سپس مقدار user- را انتخاب کرده و بر روی execute کلیک می کنیم تا در کنسول نتیجه تولید شود.

نتیجه ی این آزمون بر روی سورس کد ما به شکل زیر می باشد

show_sort_output: printf_va_4
main: selection_sort show_sort_output printf_va_1 scanf_va_1 printf_va_2
scanf_va_2 printf_va_3 printf_va_4

از این خروجی متوجه می شویم که هر یک از توابع ما چه توابعی صدا زدن، چه دستورات ورودی و خرجی داشتن(printf و scanf)، برای مثال تابع main توابع selection_sortو show_sort_output را صدا زده است و همچنین دارای دو printf و یک scanf هست.

با استفاده از terminal:

می توانیم با استفاده از دستور زیر درون terminal نتیجه را به صورت متنی ذخیره کنیم

frama-c -users main.c > user.txt

آنالیز metric:

در Metrics اطلاعاتی نظیر تعداد توابع، entry point، حلقه های تکرار، شرط ها و ... را به دست بیاورید.

جهت بدست آوردن metric از دستور زیر استفاده می کنیم

frama-c main.c -metrics

که main.c نام سورس کد ما هستش، جهت ذخیره خروجی درون فایل txt از دستور زیر استفاده می کنیم

frama-c main.c -metrics > metric.txt

خروجی به شکل زیر می باشد:

         Defined functions (3)
          =====================           
         main (0 call); selection_sort (1 call); show_sort_output (1 call); 

          Undefined functions (6)
          =======================
           printf_va_1 (1 call); printf_va_2 (1 call); printf_va_3 (1 call);
           printf_va_4 (1 call); scanf_va_1 (1 call); scanf_va_2 (1 call); 
          
          'Extern' global variables (0)
          =============================

          Potential entry points (1)
          ==========================
           main; 
          
          Global metrics
          ============== 
          Sloc = 39
          Decision point = 5
          Global variables = 0
          If = 5
          Loop = 4
          Goto = 0
          Assignment = 13
          Exit point = 3
          Function = 9
          Function call = 8
          Pointer dereferencing = 7
          Cyclomatic complexity = 8

همانطور که مشاهده می نمایید ما سه تابع داریم، نقطه ی ورود ما تابع main است، 5 شرط، 4 حلقه، 3 نقطه ی خرج و .... داریم

آنالیز PDG:

گراف PDG گراف وابستگی برنامه یا Program Dependence Graph، یک گراف تولید شده از وابستگی های داده ای و وابستگی اجرایی دستورات نسبت به هم تهیه می شوند.

برای استخراج PDG ابتدا سورس کد را به قالب فایل dot تبدیل کرده و سپس آن به pdf تبدیل می کنیم، برای اینکار به شکل زیر عمل میکنیم:

با استفاده از دستور زیر فایل .dot را تولید کرده

frama-c -pdg -pdg-dot graph -pdg-print main.c > pdg.dot

سپس با دستور زیر آن را به pdf تبدیل می کنیم

dot -Tpdg graph.main.dot > pdg.pdf

آنالیز Postdominators:

در Post Dominator دستوراتی که بر روی دستورات دیگر تاثیر میگذارد را مشخص می کنیم و به شکل یک گراف به نمایش داده می شود. این آنالیز با scanf و printf مشکل دارد و باعث ایجاد خطا می شود برای استفاده از این آنالیز، من ورودی را دستی وارد کردم و حذف scanf ها، همچنین کامنت کردن دستورات printf که سورس کد به شکل زیر تغییر کرد:

#include <stdio.h>
void selection_sort(int a[],int n);
void show_sort_output(int a[],int n);
void main()
{
int a[30], n;
int i;
//printf(&quot\nEnter size of an array: &quot);
//scanf(&quot%d&quot, &n);
n=5;
//printf(&quot\nEnter elements of an array:\n&quot);
for(i=0; i<n; i++)
a[i]=i;
selection_sort(a,n);
//printf(&quot\n\nAfter sorting:\n&quot);
show_sort_output(a,n);
}
void selection_sort(int a[],int n)
{
int i, j, min, temp;
for (i=0; i<n; i++)
{
min = i;
for (j=i+1; j<n; j++)
{
if (a[j] < a[min])
min = j;
}
temp = a[i];
a[i] = a[min];
a[min] = temp;
}
}
void show_sort_output(int a[],int n)
{
int i;
//for(i=0; i<n; i++)
//printf(&quot\n%d&quot, a[i]);
}

با استفاده از دستور زیر گراف تولید می نماییم

frama-c main.c -dot-postdom main

و با استفاده از دستور زیر آن را به pdf تبدیل می کنیم

dot -Tpdf main.main.dot > postdom.pdf

خروجی:

برش بندی یا Slicing

یک برش از برنامه حاوی دستوراتی از آن است که ویژگیهای مشخصی از برنامه را به نمایش میگذارد.. برشبندی برای اولین بار برای یافتن عامل بروز خرابی برنامهها ارائه شد؛ اما بعد از آن، کاربردهای مختلفی پیدا کرد. برای مثال، برای یافتن دو برنامه که از نظر معنایی به یکدیگر شباهت دارند میتوان از برشبندی استفاده نمود. به همینترتیب، برای یافتن میزان چسبندگی یک برنامه از برشبندی استفاده میکنند.

در Slicing بر اساس تعیین یک متغیر میتوان دستوراتی که بر روی آن متغیر تاثیر مستقیم و یا غیر مستقیم دارند را شناسایی کنیم.

برش بندی را می توان به دو صورت wr و rd انجام دهیم که در ادامه تفاوت این دو را مشاهده می نمایید

با استفاده از دستور زیر بر روی متغیر a ، slicing انجام میدهیم و عبارت wr به این معنی میباشد که در متغیر مورد نظر نوشته شده است.

frama-c -slice-wr a main.c -slice-print > slice_a_wr.txt

یا با دستور زیر بر روی متغیر a و عبارت rd به این معنی می باشد که از متغیر مورد نظر خوانده شده است(استفاده شده است)

frama-c -slice-rd a main.c -slice-print > slice_a_rd.txt

همانطور که در تصویر مشخص است در فایل سمت چب بر اساس rd متغیر a تولید شده است تابع show_sort_output نیز آورده شده است ولی در برش wr وجود ندارد.

آنالیز WP:

خواص را به صورت قیاسی تأیید می کند، بر پارامتر کردن با توجه به مدل حافظه تمرکز دارد. WP طوری طراحی شده است که برنامه C را مستقیماً به زبان Why وارد می کند ، با سایر افزونه های Frama-C مانند افزونه تجزیه و تحلیل ارزش همکاری می کند. WP می تواند به صورت اختیاری از پلت فرم Why3 برای استناد به بسیاری از پیش بینی های خودکار و تعاملی دیگر استفاده کند.

برای تهیه WP باید از طریق ترمینال دستور زیر را اعمال نماییم.

frama-c -wp -wp-rte main.c > wp.txt

خروجی تولید شده:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing main.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function main
[rte] annotating function selection_sort
[rte] annotating function show_sort_output
main.c:12:[wp] warning: Allocation, initialization and danglingness not yet implemented
              (\initialized(param0))
main.c:11:[wp] warning: Missing assigns clause (assigns 'everything' instead)
main.c:9:[wp] warning: Allocation, initialization and danglingness not yet implemented
              (\initialized(param0))
main.c:23:[wp] warning: Missing assigns clause (assigns 'everything' instead)
main.c:20:[wp] warning: Missing assigns clause (assigns 'everything' instead)
main.c:36:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 20 goals scheduled
[wp] [Qed] Goal typed_main_call_scanf_va_1_pre : Valid
[wp] [Alt-Ergo] Goal typed_main_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_main_call_scanf_va_1_pre_2 : Timeout (Qed:4ms) (10s)
[wp] [Alt-Ergo] Goal typed_main_call_printf_va_1_pre : Timeout (Qed:2ms) (10s)
[wp] [Alt-Ergo] Goal typed_main_call_printf_va_2_pre : Timeout (Qed:18ms) (10s) (Stronger)
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access : Unknown (Qed:5ms) (204ms)
[wp] [Alt-Ergo] Goal typed_main_call_scanf_va_2_pre : Timeout (Qed:9ms) (10s) (Stronger)
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_signed_overflow_2 : Valid
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_2 : Unknown (Qed:5ms) (153ms)
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_4 : Unknown (Qed:5ms) (205ms)
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_3 : Unknown (Qed:5ms) (204ms)
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_6 : Valid
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_mem_access_5 : Unknown (Qed:5ms) (255ms)
[wp] [Alt-Ergo] Goal typed_selection_sort_assert_rte_signed_overflow_3 : Unknown (Qed:7ms) (182ms)
[wp] [Alt-Ergo] Goal typed_show_sort_output_assert_rte_mem_access : Unknown (Qed:7ms) (154ms)
[wp] [Alt-Ergo] Goal typed_show_sort_output_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_main_call_printf_va_3_pre : Timeout (Qed:8ms) (10s) (Stronger)
[wp] [Alt-Ergo] Goal typed_main_call_scanf_va_2_pre_2 : Timeout (Qed:8ms) (10s) (Stronger)
[wp] [Alt-Ergo] Goal typed_show_sort_output_call_printf_va_4_pre : Timeout (Qed:6ms) (10s)
[wp] Proved goals:    6 / 20
     Qed:             1  (0.47ms-5ms-10ms)
     Alt-Ergo:        5  (8ms-19ms) (47) (interrupted: 7) (unknown: 7)

آموزش ابزار Frama-c برای آزمون نرم افزار

شروع کار

سورس برنامه

نمودار Call graph:

تست ورودی و خروجی inout:

آزمون کاربران users:

آنالیز metric:

آنالیز PDG:

آنالیز Postdominators:

برش بندی یا Slicing

آنالیز WP:

ساخت یک notification system عالی در svelte js

سوالات مصاحبه جاوا اسکریپت

بهتره که با Data Binding آشنا بشی !