Научиться доказывать цели предварительных условий Frama-C

Question

У меня есть следующий пример кода:

typedef struct {
    BYTE    fs_type;        /* FAT sub-type (0:Not mounted) */
    BYTE    drv;            /* Physical drive number */
} FATFS_temp;

FATFS_temp *FatFs_temp[1];  /* Pointer to the file system objects (logical drives) */

/*@ 
@   requires (vol <= 0) && (fs != \null) ==> \valid((fs)) ; // problematic one

@   behavior mount:
@       //assumes \valid(fs) && vol <= 0;
@       assumes fs != \null && vol <= 0;
@       ensures (vol <= 0) ==> (FatFs_temp[vol] == \old(fs));
@       ensures fs->fs_type == 0;

@   behavior unmount:
@       assumes fs == \null && vol <= 0;        
@       ensures (vol <= 0) ==> (FatFs_temp[vol] == \null);

@   behavior error:
@       assumes vol > 0;
@       ensures \result == 88;  

@   complete behaviors mount, unmount, error;
@   disjoint behaviors mount, unmount, error;
*/

int f_mount_temp (
    BYTE vol,       /* Logical drive number to be mounted/unmounted */
    FATFS_temp *fs      /* Pointer to new file system object (NULL for unmount)*/
)
{
    FATFS_temp *rfs;

    if (vol >= 1)           /* Check if the drive number is valid */
        return 88;
    rfs = FatFs_temp[vol];              /* Get current fs object */

    if (rfs) {
        rfs->fs_type = 0;           /* Clear old fs object */
    }

    if (fs) {
        fs->fs_type = 0;            /* Clear new fs object */
    }
    FatFs_temp[vol] = fs;               /* Register new fs object */

    return 22;
}

Но Frama-C / Why3 не может доказать одно из "требований", как указано в коде. В файле.Why говорится следующее:

goal WP "expl:Pre-condition (file src/ff_temp.c, line 12) in 'f_mount_temp'":
  forall vol_0 : int.
  forall malloc_0 : map int int.
  forall fatFs_temp_0 : map int addr.
  forall fs_0 : addr.
  (fs_0 <> null) ->
  (vol_0 <= 0) ->
  ((linked malloc_0)) ->
  ((is_uint8 vol_0)) ->
  (forall k_0 : int. (0 <= k_0) -> (k_0 <= 0) -> (null = fatFs_temp_0[k_0])) ->
  ((valid_rw malloc_0 fs_0 2))

end

ради обучения, мои вопросы:

1) что не так с этим предварительным условием?

2) исходя из выводов в файле.Why, каким должен быть мой подход, чтобы выяснить, что не так?

3) может ли кто-нибудь указать мне ресурсы, чтобы научиться отлаживать мои функциональные контракты?

---

РЕДАКТИРОВАТЬ:

я запустил Frama-c со следующими флагами: "-wp -wp-rte -wp-fct f_mount_temp" я не вызывал этот f_mount_temp из других источников. я запустил Frama-c, чтобы проверить эту функцию f_mount_temp() напрямую.

теперь мне понятнее, скорее всего, дополнительные утверждения, которые привели к провалу предварительного условия. контракты на обработанные функции следующие, с комментариями, указывающими статус каждого утверждения:

/*@ requires vol ≤ 0 ∧ fs ≢ \null ⇒ \valid(fs); // unknown

    behavior mount: // unknown
      assumes fs ≢ \null ∧ vol ≤ 0;
      ensures \old(vol) ≤ 0 ⇒ FatFs_temp[\old(vol)] ≡ \old(fs);
      ensures \old(fs)->fs_type ≡ 0;

    behavior unmount: //unknown
      assumes fs ≡ \null ∧ vol ≤ 0;
      ensures \old(vol) ≤ 0 ⇒ FatFs_temp[\old(vol)] ≡ \null;

    behavior error: //unknown
      assumes vol > 0;
      ensures \result ≡ 88;

    complete behaviors mount, unmount, error; // green
    disjoint behaviors mount, unmount, error; // green
 */

встроенные утверждения, добавленные флагами -wp-rfe:

int f_mount_temp(BYTE vol, FATFS_temp *fs) {
  int __retres;
  FATFS_temp *rfs;
  if ((int)vol >= 1) {
    __retres = 88;
    goto return_label;
  }
  /*@ assert rte: index_bound: vol < 1; */ // ok
  rfs = FatFs_temp[vol];
  if (rfs) {
    /*@ assert rte: mem_access: \valid(&rfs->fs_type); */ //unknown
    rfs->fs_type = (unsigned char)0;
  }
  if (fs) {
    /*@ assert rte: mem_access: \valid(&fs->fs_type); */ // unknown
    fs->fs_type = (unsigned char)0;
  }
  /*@ assert rte: index_bound: vol < 1; */ // unknown
  FatFs_temp[vol] = fs;
  __retres = 22;
  return_label: return __retres;
}

Answer 1

1) что не так с этим предварительным условием?

Ты используешь && а также ==> как будто их относительные приоритеты были хорошо известны. Это неправильно с человеческой точки зрения, потому что, как ==> не появляется на многих языках, кроме ACSL, только специалисты ACSL могут знать, что означает формула, зависящая от ее приоритета.

Кроме того, никогда не может быть ничего плохого с предварительным условием в фрагменте кода, который не включает в себя вызов функции. Предварительное условие - это не свойство, которое доказывается в отношении реализации функции, но в отношении контекста, в котором используется функция. Вы могли ошибиться и написать логический эквивалент \false и предварительное условие все еще будет в порядке для вашего фрагмента (это будет означать, что все вызовы функции недопустимы и должны быть сами по себе признаны недостижимыми).

Чтобы ваш вопрос имел смысл, он должен:

• включать доказательство (или отсутствие доказательств) пост-условия f_mount_temp и обеспечить реализацию этой функции, или
• включать доказательство (или отсутствие доказательств) предварительного условия f_mount_temp и код функции, в которой f_mount_temp вызывается, включая предварительные условия этой функции, так что можно определить, соблюдает ли эта вызывающая функция f_mount_tempпредварительное условие. В этом последнем случае нет необходимости предоставлять f_mount_tempкод или постусловие, если оно не вызывается несколько раз в вызывающей программе. Кроме того, код других функций, вызываемых из вызывающей стороны, необязательно указывать, но их контракты должны быть.

Что вы сделали здесь, предоставив fкод и спрашиваю почему fПредусловие не доказано, не является связным.

2) исходя из выводов в файле.Why, каким должен быть мой подход, чтобы выяснить, что не так?

Это не плохое место, чтобы спросить, и я думаю, что вы могли бы получить помощь, если вы спросите снова с правильными частями информации.

3) может ли кто-нибудь указать мне ресурсы, чтобы научиться отлаживать мои функциональные контракты?

Я не знаю многих из них, но этот сайт может стать ресурсом, объясняющим наиболее распространенные приемы отладки, если вы спросите снова…