0

我正在验证使用数组存储异构数据的 ac 程序 - 特别是，该程序使用数组来实现 cons 单元，其中数组的第一个元素是整数值，第二个元素是指向下一个 cons 单元的指针.

例如，此列表的自由操作将是：

void listfree(void * x) {
  if((x == 0)) {
    return;
  } else {
    void * n = *((void **)x + 1);
    listfree(n);
    free(x);
    return;
  }
}

注意：此处未显示，但其他代码部分将读取数组的值并将其视为整数。

虽然我知道表达这一点的自然方式是某种结构，但程序本身是使用数组编写的，我无法更改这一点。

我应该如何在 VST 中指定内存的结构？

我定义了一个lseg谓词如下：

Fixpoint lseg (x: val) (s: (list val)) (self_card: lseg_card) : mpred := match self_card with
    | lseg_card_0  =>  !!(x = nullval) && !!(s = []) && emp
    | lseg_card_1 _alpha_513 => 
      EX v : Z,
      EX s1 : (list val),
      EX nxt : val,
 !!(~ (x = nullval)) && 
   !!(s = ([(Vint (Int.repr v))] ++ s1)) && 
   (data_at Tsh (tarray tint 2) [(Vint (Int.repr v)); nxt] x) * 
   (lseg nxt s1 _alpha_513)
end.

但是，我在尝试评估时遇到了麻烦，void *n = *(void **)x;大概是因为规范声明内存包含整数数组而不是指针。

4

1 回答 1

1

问题大概如下，大致可以如下解决。

C 语义允许将整数（正确大小）转换为指针，反之亦然，只要您实际上不对整数值执行任何指针操作，反之亦然。您的 C 程序很可能遵守这些规则。但是可验证 C 的类型系统试图强制整数类型的局部变量（和数组元素等）永远不会包含指针值，反之亦然（除了特殊的整数值 0，它是 NULL）。

然而，可验证的 C 确实支持对这种更严格的强制执行（经过验证的基础健全）解决方法：

typedef void  * int_or_ptr
 #ifdef COMPCERT
   __attribute((aligned(_Alignof(void*))))
 #endif
  ;

即：int_or_ptr类型为void*，但具有属性“将其对齐为void*”。所以它在语义上与 相同void*，但冗余属性暗示 VST 类型系统对 C 类型强制的限制较少。

所以，当我说“几乎可以解决”时，我在问：你能修改 C 程序以使用“void* 对齐为 void*”的数组吗？

如果是这样，那么您可以继续。您的 VST 验证应该使用int_or_ptr_type，这是Ctypes.typeVST-Floyd 提供的类型定义，当引用这些数组元素或这些元素加载到的局部变量的 C 语言类型时。

不幸的是， int_or_ptr_type 没有记录在参考手册 (VC.pdf) 中，这是一个应该是正确的遗漏。您可以查看 progs/int_or_ptr.c 和 progs/verif_int_or_ptr.v，但它们所做的远比您想要或需要的要多：它们公理化了区分奇数和对齐指针的运算符，这在 C11 中未定义（但与 C11 一致，否则ocaml 垃圾收集器永远无法工作）。即那些公理化的外部函数与CompCert、gcc、clang一致；但是您不需要它们中的任何一个，因为您在 int_or_pointer 上执行的唯一操作是完全合法的“与 NULL 比较”和“转换为整数”或“转换为struct foo *”。

于 2020-09-04T14:37:07.460 回答