Comment puis-je déboguer ACSL dans frama-c?

Question

Je suis en train d'apprendre ACSL mais je suis en train de trébucher en essayant d'écrire une spécification complète. Mon code

#include 
#include 

#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;
}

Je le lance avec

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

et je vois le journal suivant

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

Il semble donc que mes deux comportements et le "assigns \nothing" n'ont pas pu être prouvés. Comment dois-je procéder à partir d'ici?

EDIT : J'ai donc compris le problème immédiat. Je dois annoter ma boucle :

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

Ma question plus large reste entière : quelle est la meilleure façon de déboguer les problèmes? J'ai résolu celui-ci en changeant et en supprimant simplement du code et en voyant ce qui est prouvé ou non prouvé.

Answer 1

Je crains qu'il ne puisse y avoir une réponse définitive à cette question (pour être honnête, j'ai envisagé de voter pour la fermer comme "trop large"). Voici cependant quelques lignes directrices qui vous aideront probablement dans vos tentatives de preuve :

Identifier les clauses individuelles

Les spécifications ACSL sont rapidement composées de nombreuses clauses (requires, ensures, invariant de boucle, assert, ...). Il est important de pouvoir les distinguer facilement. Pour cela, vous avez deux ingrédients principaux :

1. Utilisez l'interface graphique. Cela rend beaucoup plus facile de voir quelles annotations sont prouvées (point vert), prouvées mais sous l'hypothèse que d'autres clauses non prouvées sont vraies (vert/jaune), ou non prouvées (jaune).
2. Donnez un nom à vos clauses : toute prédicat ACSL peut être attaché à un nom, avec la syntaxe nom : préd. Lorsqu'une clause est équipée d'un nom, WP l'utilisera pour se référer à la clause.

Suspects habituels

Il est très facile de passer à côté d'une partie très importante d'une spécification. Voici une liste de contrôle rapide :

1. Toutes les boucles doivent être équipées d'un invariant de boucle et d'un assigne de boucle
2. Toutes les fonctions appelées par celle analysée doivent avoir un contrat (avec au moins une clause assigne)
3. Si un emplacement mémoire mentionné dans un assigne de boucle n'est pas l'objet d'un invariant de boucle correspondant, vous ne savez rien sur la valeur stockée à cet emplacement en dehors de la boucle. Cela peut poser problème.

Débogage des clauses individuelles

Une fois que vous êtes sûr de n'avoir rien manqué d'évident, il est temps d'enquêter sur des clauses spécifiques.

1. Il est généralement beaucoup plus facile de vérifier qu'un invariant de boucle est établi (c'est-à-dire vrai lors de l'atteinte de la boucle pour la première fois) plutôt que préservé (rester vrai à travers une étape de boucle). Si vous ne parvenez pas à établir un invariant de boucle, il est soit incorrect, soit vous avez oublié des requires pour contraindre l'entrée de la fonction (un cas typique pour les algorithmes sur les tableaux est invariant de boucle 0<=i<=n; qui ne peut pas être prouvé si vous ne requires n>=0;)
2. De même, les assignes et assignes de boucle devraient être plus faciles à vérifier que les propriétés fonctionnelles réelles. Tant qu'ils ne sont pas tous prouvés, vous devriez vous concentrer sur eux (une erreur courante est d'oublier de mettre l'index d'une boucle dans son assigne de boucle, ou de mentionner qu'elle assigne a[i] et non a[0..i]). N'oubliez pas que les assignes doivent inclure toutes les affectations possibles, y compris celles effectuées dans les fonctions appelées.
3. N'hésitez pas à utiliser assert pour vérifier si WP peut prouver qu'une propriété est vraie à un moment donné. Cela vous aidera à comprendre où se situent les problèmes. [ éditer selon le commentaire de @DavidMENTRÉ ci-dessous ] Notez que dans ce cas, vous devez tenir compte du fait que l'obligation de preuve initiale pourrait réussir sous l'hypothèse que le assert est vrai tandis que le assert lui-même n'est pas validé. Dans l'interface graphique, cela se reflète par un point vert/jaune, et bien sûr un point jaune devant le assert. Dans ce cas, la preuve n'est pas terminée, et vous devez comprendre pourquoi le assert n'est pas prouvé, en utilisant éventuellement la même stratégie que précédemment, jusqu'à ce que vous compreniez exactement où se situe le problème.