0



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

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

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

让我举一个简单的例子：

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

在file1.c我有两个功能：

  • 第一个函数“check_parity”只测试静态变量_sVar 的奇偶校验字段是否正确。
  • 第二个函数“correct_parity”调用第一个函数，并在字段不正确时更正奇偶校验。

在file2.c中，我有一个函数“outside_caller”，它只调用了正确的奇偶校验（）。我的目标是能够以与指定正确奇偶校验相同的方式指定 outside_caller。下面是对应的源码：

文件1.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);

文件1.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;
}

文件2.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）能够使用被调用者的合约，必须在被调用者的合约中使用ghost变量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 (4ms)
Alt-Ergo：5 (8ms-12ms-20ms) (30)

(2)正确奇偶校验()

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 正确奇偶校验 -then -report
[rte] 注释函数正确奇偶校验 [wp] 18 个预定目标
[wp] 已证明目标：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] 注释函数 outside_caller
[wp] 14 个预定目标
[wp] [Alt-Ergo] 目标 typed_outside_caller_assign_exit : 未知 (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]证明目标：9 / 14
Qed：9（4ms）
Alt-Ergo：0（中断：2）（未知：3）

==> WP：图形用户界面输出

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

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

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

为什么看起来我调用的函数越多，证明函数的行为就越复杂？是否有适当的方法来处理多个函数调用和静态变量？

非常感谢您！

PS：我在运行 Ubuntu 14.04、64 位机器的 VM 上使用 Magnesium-20151002 版本。我知道开始使用 WhyML 和 Why3 对我有很大帮助，但到目前为止，我无法按照本教程的每个步骤在 Windows 和 Ubuntu 上安装 Why3 ide。

4

1 回答 1

1

首先，请注意这对 WP-main并-lib-entry没有那么有用（您提到您也对 EVA/价值分析感兴趣，但您的问题是针对 WP 的）。

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

关于函数调用，要点是，您尝试使用 WP 证明的函数调用的任何函数都必须附带至少包含一个assigns条款的合同（可能还有更精确的规范，具体取决于被调用者与您要在调用者身上证明的属性相关）。这里要记住的重要一点是，从 WP 的角度来看，在调用之后，只有被调用方的合同中明确规定的内容ensures是真实的，而且该assigns条款中没有的任何位置都保持不变。

于 2018-05-17T09:47:48.640 回答