在 VST 中验证具有异构数组的程序

Question

我正在验证一个使用数组存储异构数据的c程序——具体来说，该程序使用数组来实现cons cells，其中数组的第一个元素是一个整数值，第二个元素是一个指针到下一个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; 大概是因为规范指出内存包含一个整数数组而不是指针。

Answer 1

问题大概如下，可以几乎解决如下

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

但是，可验证 C 确实支持（proved-foundationally-sound）解决此更严格执行的方法：

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，这是 VST-Floyd 提供的类型 Ctypes.type 的定义，当引用这些数组元素的 C-language 类型时，或局部变量这些元素被加载到。

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

在 VST 中验证具有异构数组的程序

Verifying programs with heterogeneous arrays in VST

coq

verifiable-c