如何在 frama-c 中调试 ACSL?

How do I debug ACSL in frama-c?

我正在尝试学习 ACSL,但在尝试编写完整规范时遇到困难。我的代码

#include <stdint.h>
#include <stddef.h>

#define NUM_ELEMS (8)

/*@ requires expected != test;
  @ requires \let n = NUM_ELEMS;
  @          \valid_read(expected + (0.. n-1)) && \valid_read(test + (0.. n-1));
  @ assigns \nothing;
  @ behavior matches:
  @   assumes \let n = NUM_ELEMS;
  @           \forall integer i; 0 <= i < n ==> expected[i] == test[i];
  @   ensures \result == 1;
  @ behavior not_matches:
  @   assumes \let n = NUM_ELEMS;
  @           \exists integer i; 0 <= i < n && expected[i] != test[i];
  @   ensures \result == 0;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
int array_equals(const uint32_t expected[static NUM_ELEMS], const uint32_t test[static NUM_ELEMS]) {
  for (size_t i = 0; i < NUM_ELEMS; i++) {
    if (expected[i] != test[i]) {
      return 0;
    }
  }
  return 1;
}

我运行它与

frama-c -wp -wp-rte test.c

我看到了以下日志

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
[rte] annotating function array_equals
test.c:22:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_equals_assign_part1 : Unknown (Qed:2ms) (67ms)
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access_2 : Unknown (Qed:2ms) (128ms)
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access : Unknown (Qed:2ms) (125ms)
[wp] [Alt-Ergo] Goal typed_array_equals_matches_post : Unknown (Qed:10ms) (175ms)
[wp] [Alt-Ergo] Goal typed_array_equals_not_matches_post : Unknown (Qed:7ms) (109ms)
[wp] Proved goals:    4 / 9
     Qed:             4  (0.56ms-4ms)
     Alt-Ergo:        0  (unknown: 5)

所以我的两个行为和"assigns \nothing"似乎无法证明。那么我该如何从这里开始呢?

编辑:所以我想出了眼前的问题。我没有注释我的循环:

  /*@ loop invariant \let n = NUM_ELEMS; 0 <= i <= n;
    @ loop invariant \forall integer k; 0 <= k < i ==> expected[k] == test[k];
    @ loop assigns i;
    @ loop variant \let n = NUM_ELEMS; n-i;
    @*/

我更大的问题仍然存在:调试问题的好方法是什么?我通过更改和删除代码并查看 proved/not 证明了什么来解决了这个问题。

这个问题恐怕没有确定的答案(老实说,我考虑过投票关闭它作为"too broad")。然而,这里有一些指南可能会帮助您进行证明尝试:

识别单个子句

ACSL 规范很快由许多条款组成(requiresensuresloop invariantassert、...)。能够轻松区分它们很重要。为此,您有两个主要成分:

  1. 使用 GUI。它使查看哪些注释已被证明(绿色项目符号)、已证明但假设其他未证明的子句为真(green/yellow)或未证明(黄色)变得容易得多。
  2. 为您的子句命名:任何 ACSL 谓词都可以附加一个名称,语法为 name: pred。当子句带有名称时,WP 将使用它来引用子句。

通常的嫌疑人

很容易错过规范中一些非常重要的部分。这是一个快速检查列表:

  1. 所有循环必须配备loop invariantloop assigns
  2. 被分析对象调用的所有函数必须有契约(至少有一个assigns子句)
  3. 如果 loop assigns 中提到的内存位置不是主题 相应的 loop invariant,你对循环外那个位置存储的值一无所知。这可能是个问题。

调试个别子句

一旦您确信自己没有遗漏任何明显的东西,就是时候了 开始调查具体条款。

  1. 通常,验证一个loop invariant成立要容易得多 (即第一次获得循环时为真)而不是保留(在整个循环步骤中保持为真)。如果你不能建立一个 loop invariant,那要么是错误的,要么你忘记了一些 requires 来约束函数的输入(数组算法的典型情况是 loop invariant 0<=i<=n; 可以如果你不这样做,就无法证明 requires n>=0;)
  2. 同样,assignsloop assigns 应该比真实的功能特性更容易验证。只要它们还没有全部证明,你就应该专注于它们(一个常见的错误是忘记将循环的索引放入 它的 loop assigns,或者说它分配的是 a[i] 而不是 a[0..i])。 不要忘记 assigns 必须包括所有可能的赋值,包括 在被调用者中完成的。
  3. 不要犹豫,使用assert检查WP是否可以证明属性在给定点成立。这将帮助您了解问题出现的位置。 [根据下面@DavidMENTRÉ 的评论进行编辑] 请注意,在这种情况下,您应该注意初始证明义务可能成功的事实假设assert 持有 assert 本身未被验证。在 GUI 中,这由 green/yellow 项目符号反映,当然还有 assert 前面的黄色项目符号。那样的话,证明还没有结束,你要理解断言为什么没有被证明,可能使用和上面一样的策略,直到你准确地理解问题出在哪里。