Frama-c: вызовы функций и статические переменные
В настоящее время я открываю для себя возможности frama-c, особенно инструменты анализа WP & Value. Моя конечная цель - использовать frama-c в больших кодах, включающих несколько уровней:
- много вызовов функций
- использование сложных структур данных
- статические и / или глобальные переменные
До сих пор я пытался применить восходящий метод, то есть начать указывать функции, которые не включают в себя какие-либо вызовы функций, и анализировать их поведение, изолируя их благодаря опциям ядра -lib-entry и -main. Делая это, я проверяю, что если предварительные условия предполагаются истинными, то весь контракт функции проверяется. Как только я попытался указать верхние уровни, которые вызывают эти функции, все усложняется. Во-первых, мне часто приходится указывать поведение вызываемых функций, что не всегда просто, потому что эти функции могут иметь дело с переменными / функциями вне области текущей функции.
Позвольте привести простой пример:
Скажем, в file1.h мы определяем структуру данных "my_struct", которая содержит номер поля и четность поля.
В file1.c у меня есть две функции:
- Первая функция "check_parity", которая просто проверяет правильность поля четности статической переменной _sVar.
- Вторая функция "correct_parity", которая вызывает первую функцию и корректирует четность, если поле было неправильным.
В file2.c у меня есть функция "outside_caller", которая просто вызывает correct_parity(). Моя цель состоит в том, чтобы иметь возможность указывать outside_caller так же, как я указываю correct_parity. Ниже приведен соответствующий исходный код:
file1.h
/* parity = 0 => even ; 1 => odd */
typedef unsigned char TYP_U08;
typedef unsigned short TYP_U16;
typedef unsigned int TYP_U32;
typedef unsigned long TYP_U64;
typedef struct {
unsigned char parity;
unsigned int number;
} my_stuct;
typedef enum
{
S_ERROR = -1
,S_OK = 0
,S_WARNING = 1
} TYPE_STATUS;
/*@ ghost my_stuct* g_sVar; */
/*@ predicate fc_pre_is_parity_ok{Labl}(my_stuct* i_sVar) =
(
\at(i_sVar->parity, Labl) == ((TYP_U08) (\at(i_sVar->number,Labl) % 2u))
);
@ predicate fc_pre_valid_parity{Labl}(my_stuct* i_sVar) =
(
(\at(i_sVar->parity,Labl) == 0) ||
(\at(i_sVar->parity, Labl) == 1)
);
@ predicate fc_pre_is_parity_readable(my_stuct* i_sVar) =
(
\valid_read(&i_sVar->parity)
);
@ predicate fc_pre_is_parity_writeable(my_stuct* i_sVar) =
(
\valid(&i_sVar->parity)
);
@ predicate fc_pre_is_number_readable(my_stuct* i_sVar) =
(
\valid_read(&i_sVar->number)
);
@ predicate fc_pre_is_number_writeable(my_stuct* i_sVar) =
(
\valid(&i_sVar->number)
);
*/
TYPE_STATUS check_parity(void);
TYPE_STATUS correct_parity(void);
file1.c
static my_stuct* _sVar;
/*@ requires check_req_parity_readable:
fc_pre_is_parity_readable(_sVar);
@ requires check_req_number_readable:
fc_pre_is_number_readable(_sVar);
@ assigns check_assigns:
g_sVar;
@ ensures check_ensures_error:
!fc_pre_valid_parity{Post}(g_sVar) ==> \result == S_ERROR;
@ ensures check_ensures_ok:
(
fc_pre_valid_parity{Post}(g_sVar) &&
fc_pre_is_parity_ok{Post}(g_sVar)
) ==> \result == S_OK;
@ ensures check_ensures_warning:
(
fc_pre_valid_parity{Post}(g_sVar) &&
!fc_pre_is_parity_ok{Post}(g_sVar)
) ==> \result == S_WARNING;
@ ensures check_ensures_ghost_consistency:
\at(g_sVar, Post) == _sVar;
*/
TYPE_STATUS check_parity(void)
{
//@ ghost g_sVar = _sVar;
TYPE_STATUS status = S_OK;
if(!(_sVar->parity == 0 || _sVar->parity == 1)) {
status = S_ERROR;
} else if ( _sVar->parity == (TYP_U08)(_sVar->number % 2u) ){
status = S_OK;
} else {
status = S_WARNING;
}
return status;
}
/*@ requires correct_req_is_parity_writeable:
fc_pre_is_parity_writeable(_sVar);
@ requires correct_req_is_number_readable:
fc_pre_is_number_readable(_sVar);
@ assigns correct_assigns:
_sVar->parity,
g_sVar,
g_sVar->parity;
@ ensures correct_ensures_error :
!fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;
@ ensures correct_ensures_ok :
(
fc_pre_valid_parity{Pre}(g_sVar) &&
fc_pre_is_parity_ok{Pre}(g_sVar)
) ==> \result == S_OK;
@ ensures correct_ensures_warning :
(
fc_pre_valid_parity{Pre}(g_sVar) &&
!fc_pre_is_parity_ok{Pre}(g_sVar)
) ==> \result == S_WARNING;
@ ensures correct_ensures_consistency :
fc_pre_is_parity_ok{Post}(g_sVar);
@ ensures correct_ensures_validity :
fc_pre_valid_parity{Post}(g_sVar);
@ ensures correct_ensures_ghost_consistency :
\at(g_sVar, Post) == _sVar;
*/
TYPE_STATUS correct_parity(void)
{
//@ ghost g_sVar = _sVar;
TYPE_STATUS parity_status = check_parity();
if(parity_status == S_ERROR || parity_status == S_WARNING) {
_sVar->parity = (TYP_U08)(_sVar->number % 2u);
/*@ assert (\at(g_sVar->parity,Here) == 0) ||
(\at(g_sVar->parity, Here) == 1);
*/
//@ assert \at(g_sVar->parity, Here) == (TYP_U08)(\at(g_sVar->number,Here) % 2u);
}
return parity_status;
}
file2.c
/*@ requires out_req_parity_writable:
fc_pre_is_parity_writeable(g_sVar);
@ requires out_req_number_writeable:
fc_pre_is_number_readable(g_sVar);
@ assigns out_assigns:
g_sVar,
g_sVar->parity;
@ ensures out_ensures_error:
!fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;
@ ensures out_ensures_ok :
(
fc_pre_valid_parity{Pre}(g_sVar) &&
fc_pre_is_parity_ok{Pre}(g_sVar)
) ==> \result == S_OK;
@ ensures out_ensures_warning :
(
fc_pre_valid_parity{Pre}(g_sVar) &&
!fc_pre_is_parity_ok{Pre}(g_sVar)
) ==> \result == S_WARNING;
@ ensures out_ensures_consistency:
fc_pre_is_parity_ok{Post}(g_sVar);
@ ensures out_ensures_validity:
fc_pre_valid_parity{Post}(g_sVar);
*/
TYPE_STATUS outside_caller(void)
{
TYPE_STATUS status = correct_parity();
//@ assert fc_pre_is_parity_ok{Here}(g_sVar) ==> status == S_OK;
/*@ assert !fc_pre_is_parity_ok{Here}(g_sVar) &&
fc_pre_valid_parity{Here}(g_sVar) ==> status == S_WARNING; */
//@ assert !fc_pre_valid_parity{Here}(g_sVar) ==> status == S_ERROR;
return status;
}
Здесь основная проблема заключается в том, что для определения outside_caller() мне нужно получить доступ к _sVar, который находится вне области действия в file2.c. Это подразумевает работу с фиктивной переменной (g_sVar), которая объявлена в file1.h и обновлена в функции correct_parity. Чтобы вызывающая сторона (correct_parity) могла использовать контракты вызываемых абонентов, в контрактах вызываемых абонентов должна использоваться призрачная переменная g_sVar.
Вот результаты анализа WP:
(1) check_parity ()
frama-c -wp src / main.c src / test.c -cpp-command 'gcc -C -E -Isrc /' -main 'check_parity' -lib-entry -wp-timeout 1 -wp-fct check_parity -wp -rte -wp-fct check_parity -then -report
[rte] аннотирующая функция check_parity
[wp] 14 голов запланировано
[wp] Доказанные цели: 14/14
Qed: 9 (4 мс)
Alt-Ergo: 5 (8 мс-12 мс-20 мс) (30)
(2) correct_parity ()
frama-c -wp src / main.c src / test.c -cpp-command 'gcc -C -E -Isrc /' -main 'correct_parity' -lib-entry -wp-timeout 1 -wp-fct correct_parity -wp -rte -wp-fct correct_parity -then -report
[rte] аннотирующая функция correct_parity [wp] 18 запланированных целей
[wp] Доказанные цели: 18/18
Qed: 12 (4 мс)
Alt-Ergo: 6 (4 мс-37 мс-120 мс) (108)
(3) outside_caller()
frama-c -wp src / main.c src / test.c -cpp-command 'gcc -C -E -Isrc /' -main 'outside_caller' -lib-entry -wp-timeout 1 -wp-fct outside_caller -wp -rte -wp-fct outside_caller -then -report
[rte] аннотирующая функция outside_caller
[wp] 14 голов запланировано
[wp] [Alt-Ergo] Цель typed_outside_caller_assign_exit: неизвестно (Qed:4 мс) (515 мс)
[wp] [Alt-Ergo] Цель typed_outside_caller_call_correct_parity_pre_correct_req_is_par___: неизвестно (636 мс)
[wp] [Alt-Ergo] Цель typed_outside_caller_assert: Тайм-аут
[wp] [Alt-Ergo] Цель typed_outside_caller_assign_normal_part1: время ожидания
[wp] [Alt-Ergo] Цель typed_outside_caller_call_correct_parity_pre_correct_req_is_num___: неизвестно (205 мс)
[wp] Доказанные цели: 9/14
Qed: 9 (4 мс)
Alt-Ergo: 0 (прервано: 2) (неизвестно: 3)
==> WP: GUI Output
В этой конфигурации вызываемые указываются с помощью призрачной переменной g_sVar, за исключением предложений require и assings по двум причинам:
- Мне нужно проверить доступ к _sVar R/W с помощью \valid & \valid_read, так как это указатель
- Когда я попытался указать предложения присваивания вызываемых с помощью g_sVar, я не смог проверить соответствующее предложение.
Но тем самым я каким-то образом сделал спецификацию вызывающего абонента недействительной, как вы можете увидеть на выходе WP.
Почему кажется, что чем больше у меня вызовов функций, тем сложнее доказать поведение функций? Есть ли правильный способ иметь дело с несколькими вызовами функций и статическими переменными?
Заранее большое спасибо!
PS: Я работаю с версией Magnesium-20151002, на виртуальной машине, работающей с Ubuntu 14.04, 64-битная машина. Я знаю, что начало работы с WhyML и Why3 может мне сильно помочь, но до сих пор я не смог установить Why3 ide ни в Windows, ни в Ubuntu после каждого шага этого урока.
1 ответ
Прежде всего, обратите внимание, что -main а также -lib-entry не очень полезны для WP (вы упомянули, что вы также заинтересованы в EVA/Value Analysis, но ваш вопрос направлен на WP).
Ваша проблема со статическими переменными известна, и самый простой способ ее решить - объявить в заголовке переменную-призрак. Но тогда вы должны выразить свои контракты через призрачную переменную, а не static один. В противном случае абоненты не смогут использовать эти контракты, так как они ничего не знают о _sVar, Как правило, лучше поместить контракт в заголовок: таким образом, вы обязаны использовать только те идентификаторы, которые видны за пределами единицы перевода.
Что касается вызовов функций, главное, что любая функция, вызываемая функцией, которую вы пытаетесь доказать с помощью WP, должна иметь контракт, который по крайней мере содержит assigns пункт (и, возможно, более точные спецификации, в зависимости от того, насколько эффекты вызываемого объекта релевантны для свойства, которое вы хотите доказать для вызывающего). Здесь важно помнить, что, с точки зрения WP, после вызова только то, что прямо указано в договоре вызываемого абонента, через ensures это правда, плюс тот факт, что любое место не в assigns пункт был оставлен без изменений.