Frama-C/WP kann die Schleifeninvariante mit \at nicht beweisen

Question

Ich habe Probleme, 2 Schleifeninvarianten zu beweisen:

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

Ich vermute, dass \at für Arrays nicht funktioniert, wie ich es erwarte.

Es gibt eine ähnliche Funktion in ACSL by Example (Seite 68, swap_ranges), die dies verwendet, aber, wie angegeben, konnten sie diese bestimmte Funktion nicht mit dem WP-Plugin beweisen. Ich habe es auf meinem Computer probiert und tatsächlich kann die gleiche Invariante nicht bewiesen werden.

Vollständiger Code

/*
 * memswap()
 *
 * Tauscht die Inhalte zweier nicht überlappender Speicherbereiche.
 * Das könnte wirklich schneller gemacht werden...
 */

#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*)m2)[0..\at(n, Pre)-1], p, q;
        loop variant n;
    @*/
    while (/*n--*/ n) {
        tmp = *p;
        *p = *q;
        *q = tmp;

        p++;
        q++;

        n--; // eingefügter Code
    }
}

EDIT

Ich verwende Frama-C Oxygen-Version und habe automatisches Beweisen mit alt-ergo(0.94) und cvc3(2.4.1) versucht

Ausgabe von 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 : Unbekannt
[wp] [Cvc3] Goal store_memswap_loop_inv_6_preserved : Unbekannt

alt-ergo:

[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_established : Gültig
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_established : Gültig
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_preserved : Zeitüberschreitung
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_preserved : Zeitüberschreitung

Answer 1

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

Sie haben die falschen loop assigns. Die loop assigns Annotationen geben an, welche Speicherorte bei jeder Iteration geändert wurden. Die Anzahl der Speicherorte sollte normalerweise mit dem Fortschreiten der Schleife zunehmen (in Ihrem Fall, wenn n abnimmt). Es ähnelt folgendem:

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

Aber mein eigener Vorschlag oben könnte in die eine oder andere Richtung um einen Wert falsch sein. Ich finde es schwierig, mich genau daran zu erinnern, wie diese "beweglichen" loop assigns Klauseln genau funktionieren.

---

Als Alternative können Sie eine einfachere, "statische" loop assigns Annotation (wie Ihre) schreiben und die Informationen hinzufügen, was sich noch nicht in der Schleifeninvariante geändert hat. Das ist das, was ich normalerweise mache, um meine Unfähigkeit zu umgehen, mich daran zu erinnern, wie komplexe loop assigns Klauseln funktionieren. Das wäre etwas wie (ungetestet):

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