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);

我猜测\对于阵列不起作用,正如我所料.

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氧气释放并尝试使用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注解告诉什么内存位置已在每次迭代中被修改.位置数通常应随着循环的进展而增加(在您的情况下,作为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;
…
@*/