如何在frama-c中调试ACSL？

Question

我正在努力学习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)

因此，我的两种行为和“指派\零”似乎都无法证明。那我该怎么从这里开始呢？

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

  /*@ 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;
    @*/

我更大的问题仍然存在:什么是调试问题的好方法？我解决了这个问题，只需更改和删除代码，并查看已证明/未证明的内容。

Answer 1

恐怕这个问题没有一个明确的答案(老实说，我已经考虑投票结束它，因为它“太宽泛了”)。然而，以下是一些指导原则，它们可能有助于您的验证尝试：

识别个别从句

ACSL规范由许多子句组成(requires、ensures、loop invariant、assert、.)。重要的是能够很容易地区分它们。为此，你有两个主要成分：

1. 使用GUI。这使得更容易看出哪些注释被证明(绿色子弹)，证明，但假设，其他未被证明的子句是真实的(绿色/黄色)，或未证明(黄色)。
2. 命名您的子句:任何ACSL谓词都可以附加一个名称，语法为name: pred。当一个条款有一个名称时，WP将使用它来指该条款。

惯犯

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

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

调试个别子句

一旦你确信你没有遗漏任何明显的东西，现在是时候开始调查具体的条款了。

1. 通常，验证loop invariant是否已建立(即第一次获得循环时为真)要容易得多，而不是保留(在循环步骤中保持为真)。如果您不能建立一个loop invariant，那么它要么是错误的，要么是您忘记了一些requires来约束函数的输入(数组上算法的一个典型例子是loop invariant 0<=i<=n;，如果不使用requires n>=0;就无法证明这一点)
2. 类似地，assigns和loop assigns应该比实际的函数属性更容易验证。只要没有全部证明，您就应该集中精力于它们(常见的错误是忘记将循环的索引放在其loop assigns中，或者提到它分配的是a[i]而不是a[0..i])。别忘了，assigns必须包括所有可能的作业，包括在被叫中完成的作业。
3. 不要犹豫使用assert来检查WP是否能证明某一属性在给定的点上是有效的。这将帮助你理解问题的根源。根据@DavidMENTR在备注下面的评论，编辑:在这种情况下，你应该注意到这样一个事实:在assert本身未被验证的前提下，最初的证明义务可能会成功。在GUI中，这反映在一颗绿色/黄色的子弹上，当然还有一颗在assert前面的黄色子弹。在这种情况下，证据还没有结束，你必须理解为什么断言没有被证明，可能使用与上面相同的策略，直到你完全理解问题所在。