Frama-C/WP 不能用 \at 证明循环不变

Question

我无法证明 2 个循环不变量：

    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);

我猜 \at 不像我预期的那样适用于数组。

ACSL by Example（第 68 页，swap_ranges）中有一个类似的函数，它使用了这个，但是，如前所述，他们无法用 WP 插件证明这个特定的函数。我在我的机器上试过了，确实不能证明同样的不变量。

完整代码

/*
 * memswap()
 *
 * Swaps the contents of two nonoverlapping memory areas.
 * This really could be done faster...
 */

#include "string.h"

/*@
    requires n >= 1;
    requires \valid(((char*)m1)+(0..n-1));
    requires \valid(((char*)m2)+(0..n-1));
    requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
    assigns ((char*)m1)[0..n-1];
    assigns ((char*)m2)[0..n-1];
    ensures \forall integer i; 0 <= i < n ==> ((char*)m1)[i] == \old(((char*)m2)[i]);
    ensures \forall integer i; 0 <= i < n ==> ((char*)m2)[i] == \old(((char*)m1)[i]);
@*/
void memswap(void *m1, void *m2, size_t n)
{
    char *p = m1;
    char *q = m2;
    char tmp;

    /*@
        loop invariant 0 <= n <= \at(n, Pre);
        loop invariant p == m1+(\at(n, Pre) - n);
        loop invariant q == m2+(\at(n, Pre) - n);
        loop invariant (char*)m1 <= p <= (char*)m1+\at(n, Pre);
        loop invariant (char*)m2 <= q <= (char*)m2+\at(n, Pre);
        loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
        loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
        loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
        loop variant n;
    @*/
    while (/*n--*/ n) {
        tmp = *p;
        *p = *q;
        *q = tmp;

        p++;
        q++;

        n--; // inserted code
    }
}

编辑

我正在使用 Frama-C Oxygen 版本并尝试使用 alt-ergo(0.94) 和 cvc3(2.4.1) 进行自动证明

frama-c 的输出：

cvc3:

[wp] [Cvc3] Goal store_memswap_loop_inv_7_established : Valid
[wp] [Cvc3] Goal store_memswap_loop_inv_6_established : Valid
[wp] [Cvc3] Goal store_memswap_loop_inv_7_preserved : Unknown
[wp] [Cvc3] Goal store_memswap_loop_inv_6_preserved : Unknown

alt-ergo：

[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_established : Valid
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_established : Valid
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_preserved : Timeout
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_preserved : Timeout

Answer 1

/*@
…
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
    loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
…
@*/

你打错了loop assigns。 loop assigns 注释告诉what memory locations have been modified at each iteration。位置的数量通常应随着循环的进行而增加（在您的情况下，随着n 的减少）。是这样的：

loop assigns n, tmp, ((char*)m1)[0..(\at(n, Pre) - n - 1)], ((char*)um2)[0..(\at(n, Pre) - n - 1)], p, q;

但我自己上面的建议可能会在一个方向或另一个方向上偏离。我发现很难准确地记住这些“移动”循环分配子句是如何工作的。

---

或者，您可以编写一个更简单的“静态”loop assigns 注释（如您的），并在循环不变量中添加有关尚未更改的内容的信息。这是我通常会做的，以规避我无法记住loop assigns 子句的复杂性。就像（未经测试）：

/*@
…
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
    loop invariant \forall integer i; (\at(n, Pre) - n) <= i < \at(n, Pre) ==> ((char*)m1)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; (\at(n, Pre) - n) <= i < \at(n, Pre) ==> ((char*)m2)[i] == \at(((char*)m2)[i], Pre);
    loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
…
@*/