Frama-c：函数调用和静态变量

Question

我目前正在探索 frama-c 的功能，尤其是 WP & Value 的分析工具。我的最终目标是能够在涉及多个层的较大代码上使用 frama-c：

很多函数调用
复杂数据结构的使用
静态and/or全局变量

到目前为止，我一直在尝试应用自下而上的方法，即开始指定不包含任何函数调用的函数，并通过使用 -lib-entry 和 -main 内核选项将它们隔离来分析它们的行为。通过这样做，我确保如果前提条件被假定为真，那么整个函数契约就被验证了。一旦我尝试指定调用这些函数的上层，事情就变得复杂了。首先，我经常必须指定被调用函数的行为，这并不总是那么容易，因为这些函数可能处理 variables/functions 超出当前函数的范围。

让我举个简单的例子：

假设在 file1.h 中我们定义了一个数据结构“my_struct”，其中包含一个字段编号和一个字段奇偶校验。

在file1.c中我有两个函数：

第一个函数“check_parity”仅测试静态变量 _sVar 的奇偶校验字段是否正确。
调用第一个函数的第二个函数“correct_parity”，如果字段不正确则更正奇偶校验。

在 file2.c 中，我有一个只调用 correct_parity() 的函数“outside_caller”。我的 objective 能够像指定 correct_parity 一样指定 outside_caller。下面是对应的源码：

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()，我需要访问超出 file2.c 范围的 _sVar。这意味着要处理在 file1.h 中声明并在 correct_parity 函数中更新的幽灵变量 (g_sVar)。为了使调用者（correct_parity）能够使用被调用者的合约，必须使用幽灵变量g_sVar 插入ide被调用者的合约.

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] annotating function check_parity
[wp] 14 goals scheduled
[wp] Proved goals: 14 / 14
Qed: 9 (4ms)
Alt-Ergo: 5 (8ms-12ms-20ms) (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] annotating function correct_parity [wp] 18 goals scheduled
[wp] Proved goals: 18 / 18
Qed: 12 (4ms)
Alt-Ergo: 6 (4ms-37ms-120ms) (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] annotating function outside_caller
[wp] 14 goals scheduled
[wp] [Alt-Ergo] Goal typed_outside_caller_assign_exit : Unknown (Qed:4ms) (515ms)
[wp] [Alt-Ergo] Goal typed_outside_caller_call_correct_parity_pre_correct_req_is_par___ : Unknown (636ms)
[wp] [Alt-Ergo] Goal typed_outside_caller_assert : Timeout
[wp] [Alt-Ergo] Goal typed_outside_caller_assign_normal_part1 : Timeout
[wp] [Alt-Ergo] Goal typed_outside_caller_call_correct_parity_pre_correct_req_is_num___ : Unknown (205ms)
[wp] Proved goals: 9 / 14
Qed: 9 (4ms)
Alt-Ergo: 0 (interrupted: 2) (unknown: 3)

==> WP : GUI Output

在此配置中，被调用者使用 g_sVar ghost 变量指定，requires 和 assings 子句除外，原因有两个：

我需要用 \valid 和 \valid_read 检查 _sVar R/W 访问，因为它是一个指针
当我试图用 g_sVar 指定被调用者的 assigns 子句时，我无法验证相应的子句。

但是通过这样做，我以某种方式使调用者的规范无效，正如您在 WP 的输出中看到的那样。

为什么我调用的函数越多，证明函数的行为就越复杂？有没有正确的方法来处理多个函数调用和静态变量？

非常感谢您！

PS: 我在 VM 运行 Ubuntu 14.04、64 位机器上使用 Magnesium-20151002 版本.我知道开始使用 WhyML 和 Why3 对我有很大帮助，但到目前为止，我无法在 windows 和 Ubuntu 上安装 Why3 ide Ubuntu this教程。

Answer 1

首先，请注意 -main 和 -lib-entry 对 WP 没有太大用处（您提到您也对 EVA/Value 分析感兴趣，但您的问题是针对 WP)。

你的静态变量问题是众所周知的，最简单的处理方法确实是在 header 中声明一个 ghost 变量。但是你必须根据 ghost 变量而不是 static 来表达你的合同。否则，调用者将无法使用这些合约，因为他们对 _sVar 一无所知。根据经验，最好将合同放在 header 中：这样，您就只能使用在翻译单元之外可见的标识符。

关于函数调用，要点是你试图用 WP 证明的函数调用的任何函数必须附带一个至少包含 assigns 子句（可能更多）的合同精确的规范，取决于被调用者的影响与你想在调用者身上证明的属性的相关程度）。这里要记住的重要一点是，从 WP 的角度来看，在调用之后，只有被调用者的合约中通过 ensures 明确声明的内容是真实的，加上任何不在 [=14= 中的位置这一事实] 子句保持不变。

Frama-c：函数调用和静态变量

Frama-c: Function calls and static variables

frama-c

acsl