学习如何证明 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()。

现在对我来说更清楚了，它可能是导致先决条件失败的附加断言。处理的函数契约如下，其中的 cmets 指示每个断言的状态：

/*@ 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 专家才能知道取决于其优先级的公式的含义。

除此之外，在不涉及函数调用的代码 sn-p 中的前置条件永远不会有任何问题。前置条件不是相对于函数的实现而是相对于使用函数的上下文来证明的属性。您可能犯了一个错误并编写了 \false 的逻辑等价物，并且前提条件仍然适用于您的 sn-p（这只意味着对该函数的所有调用都是无效的，并且必须证明它们本身是不可访问的)。

为了使您的问题有意义，它必须：

• 涉及f_mount_temp 的后置条件的证明（或缺乏证明）并提供此函数的实现，或
• 涉及f_mount_temp的前置条件的证明（或缺乏证明）和调用f_mount_temp的函数的代码，包括该函数的前置条件，以便可以判断是否此调用函数尊重f_mount_temp 的前提条件。在后一种情况下，不需要提供f_mount_temp 的代码或后置条件，除非在调用者中多次调用它。此外，不需要提供从调用者调用的其他函数的代码，但应该提供它们的合约。

你在这里做了什么，提供f的代码并询问为什么f的前置条件没有被证明，不连贯。

2) 基于 .Why 文件中的输出，我应该采取什么方法来找出问题所在？

这不是一个糟糕的地方，我认为如果你再次询问正确的信息，你会得到帮助。

3) 有人可以指点我学习如何调试我的函数合约的资源吗？

我不知道其中很多，但是如果您再次询问，此站点可能会成为解释最常见调试技巧的资源……