在VST中使用异构数组验证程序

问题描述

我正在验证一个使用数组存储异类数据的ac程序-特别是，该程序使用数组来实现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;时遇到了麻烦，大概是因为该规范指出该内存包含一个整数数组而不是指针。

解决方法

问题可能如下，并且可以几乎如下解决。

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

但是，Verifiable C确实支持针对这种更严格的强制执行的（已证明基础的）解决方法：

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

即：int_or_ptr类型为void*，但属性为“将其对齐为void*”。因此，它在语义上与void*相同，但是冗余属性提示VST类型系统对C类型强制执行的限制较少。

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

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

遗憾的是，参考手册（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所做的唯一操作是完全合法的“与NULL比较”和“强制转换为整数”或“强制转换为struct foo *”。