Frama-C WP Tutorial | 函数契约

由霍尔逻辑，霍尔三元组可以定义为

\{P\} C \{Q\}

其中 $P$ 和 $Q$ 是谓词，即在特定程序点上表达内存属性的逻辑公式。 $C$ 是定义程序的一系列指令。

函数契约的目标是说明函数期望的输入属性，以及作为交换，输出将得到保证的属性。函数的期望输入称为前置条件，输出的属性称为后置条件。契约用 ACSL 表达，它和 C 语言长得比较像。

1
/*@
2
  //契约
3
*/
4
void foo(int bar){
5

6
}

注释块开头的 @，向 Frama-C 表明接下来的是注释不是要忽略的注释块。

后置条件

用 ensures 子句引入函数的后置条件。比如函数 abs()：

1
/*@
2
  ensures \result >= 0;
3
*/
4
int abs(int val){
5
  if (val < 0){
6
    return -val;
7
  }
8
  return val;
9
}

\result 是一个特殊的变量，表示函数的返回值。上面的后置条件表明，函数的返回值总是大于等于 0。显然这个条件很宽泛，进一步约束函数的一般行为的话，可以继续补充：

1
/*@
2
  ensures \result >= 0;
3
  ensures (val >= 0 ==> \result == val) &&
4
          (val < 0 ==> \result == -val);
5
*/
6
int abs(int val){
7
  if (val < 0){
8
    return -val;
9
  }
10
  return val;
11
}

这里出现的 ==> 就是 $\Rightarrow$ ，表示逻辑蕴含。同理，<==> 表示逻辑等价。

我们可以通过给属性命名来减少重复。比如上面的例子可以改写为：

1
/*@
2
  ensures positive_value: function_result: \result >= 0;
3
  ensures (val >= 0 ==> \result == val) &&
4
          (val < 0 ==> \result == -val);
5
*/
6
int abs(int val){
7
  if (val < 0){
8
    return -val;
9
  }
10
  return val;
11
}

通过 Frama-C 的 -wp 选项，我们可以检查函数契约是否满足。比如上面的例子可以用下面的命令检查：

1
frama-c -wp abs.c

输出为：

1
❯ frama-c -wp abs.c
2
[kernel] Parsing abs.c (with preprocessing)
3
[wp] Warning: Missing RTE guards
4
[wp] 2 goals scheduled
5
[wp] Proved goals:    4 / 4
6
  Terminating:     1
7
  Unreachable:     1
8
  Qed:             2
9
[wp:pedantic-assigns] abs.c:6: Warning:
10
  No 'assigns' specification for function 'abs'.
11
  Callers assumptions might be imprecise.

如果输出中有 Proved goals: 4 / 4，表示所有的目标都被证明了。Terminating: 1 表示函数是终止的，Unreachable: 1 表示有一个不可达的目标。

但这样并不能排除运行时错误（RTE）。比如上面的 abs() 函数没有处理整数溢出的问题。在 Ivette 中可以用以下设置来处理：

rte

然后就能看到 Frama-C 生成了一些运行时错误（RTE）保护代码。比如上面的 abs() 函数会生成以下代码：

1
/*@ assert rte: signed_overflow: -2147483647 ≤ val; */

但是执行验证时会发现，WP 不能证明这个断言的真伪（橙色），也就是说无法保证整数溢出不会发生。

rte-overflow

对应的，在 cli 中的输出会是：

1
❯ frama-c -wp -wp-rte abs.c
2
[kernel] Parsing abs.c (with preprocessing)
3
[rte:annot] annotating function abs
4
[wp] 3 goals scheduled
5
[wp] [Timeout] typed_abs_assert_rte_signed_overflow (Alt-Ergo)
6
[wp] Proved goals:    4 / 5
7
  Terminating:     1
8
  Unreachable:     1
9
  Qed:             2
10
  Timeout:         1
11
[wp:pedantic-assigns] abs.c:6: Warning:
12
  No 'assigns' specification for function 'abs'.
13
  Callers assumptions might be imprecise.

说明这个断言无法被证明是因为超时了。

前置条件

前置条件用 requires 子句引入。比如函数 abs() 的前置条件可以是：

1
#include <limits.h>
2

3
/*@
4
  requires INT_MIN < val;
5

6
  ensures \result >= 0;
7
  ensures (val >= 0 ==> \result == val) &&
8
          (val < 0 ==> \result == -val);
9
*/
10
int abs(int val){
11
  if (val < 0){
12
    return -val;
13
  }
14
  return val;
15
}

这时候再运行 frama-c -wp -wp-rte abs.c，会发现所有的目标都被证明了。

1
❯ frama-c -wp -wp-rte abs.c
2
[kernel] Parsing abs.c (with preprocessing)
3
[rte:annot] annotating function abs
4
[wp] 3 goals scheduled
5
[wp] Proved goals:    5 / 5
6
  Terminating:     1
7
  Unreachable:     1
8
  Qed:             3
9
[wp:pedantic-assigns] abs.c:10: Warning:
10
  No 'assigns' specification for function 'abs'.
11
  Callers assumptions might be imprecise.

也可以写一个函数契约的测试程序来验证函数契约是否满足。比如：

1
void foo(int a){
2
  int b = abs(42);
3
  int c = abs(-42);
4
  int d = abs(a);
5
  int e = abs(INT_MIN);
6
}

再次验证：

1
❯ frama-c -wp -wp-rte abs.c
2
[kernel] Parsing abs.c (with preprocessing)
3
[rte:annot] annotating function abs
4
[rte:annot] annotating function foo
5
[wp] 9 goals scheduled
6
[wp] [Timeout] typed_foo_call_abs_4_requires (Qed 1ms) (Alt-Ergo)
7
[wp] [Timeout] typed_foo_call_abs_3_requires (Qed 0.56ms) (Alt-Ergo)
8
[wp] Proved goals:    9 / 11
9
  Terminating:     1
10
  Unreachable:     1
11
  Qed:             7 (0.56ms-0.21ms-1ms)
12
  Timeout:         2
13
[wp:pedantic-assigns] abs.c:10: Warning:
14
  No 'assigns' specification for function 'abs'.
15
  Callers assumptions might be imprecise.
16
[wp:pedantic-assigns] abs.c:17: Warning:
17
  No 'assigns' specification for function 'foo'.
18
  Callers assumptions might be imprecise.

Frama-C WP Tutorial | 函数契约

目录

后置条件

前置条件