使用VST验证全局双精度数组时的size_compatible证明问题

核心问题 #

你的处理方式确实不对——你错误地拆分了全局数组的内存断言描述，导致VST无法利用全局数组编译期的对齐保证，进而无法自动推导后续元素的field_compatible和size_compatible。

全局数组在编译时会被分配到满足类型对齐要求的连续内存区域，但你用data_at描述数组头部、再用sepcon拼接mapsto的方式，相当于手动割裂了数组的连续布局，VST无法识别后续元素属于数组的一部分，自然无法自动验证其对齐和大小兼容性。

正确的内存断言写法 #

全局数组应该用单个data_at断言描述整个数组的完整布局，而不是拆分元素：

错误写法（导致验证失败） #

(* 错误：拆分数组的断言描述 *)
data_at Tarray(tdouble) 1 dbls
* sepcon
mapsto (dbls + offset_val 8) tdouble 1.1

正确写法 #

(* 正确：用data_at覆盖整个数组 *)
data_at Tarray(tdouble) 2 dbls

这种写法下，VST会自动处理数组内所有元素的对齐和大小约束——因为全局数组的内存布局在编译时已经保证每个元素都符合tdouble的要求，data_at会将整个数组作为一个连续的、满足类型规范的对象来处理，验证dbls[1]时自然能通过size_compatible检查。

特殊场景下的拆分写法（如果必须拆分） #

如果因为业务逻辑需要拆分数组元素的断言，必须显式添加对齐约束，确保后续元素的起始地址满足tdouble的对齐要求：

data_at Tarray(tdouble) 1 dbls
* sepcon
align (dbls + offset_val 8) tdouble
* sepcon
mapsto (dbls + offset_val 8) tdouble 1.1

align ptr ty断言会直接证明ptr符合类型ty的对齐要求，补上这个断言后就能通过size_compatible的验证。

针对你的示例代码的验证思路 #

对应你给出的C代码：

double dbls[] = {0.0, 1.1};
int main() {
  double sum;
  sum = dbls[0] + dbls[1];
  return 0;
}

在VST的spec中，main函数的前置条件需要完整描述全局数组dbls：

Definition main_spec :=
  DECLARE _main
    WITH gv : globals
    PRE [ ]
      PROP ()
      LOCAL ()
      SEP (data_at Tarray(tdouble) 2 (gv _dbls);
           (* 这里添加其他全局变量的断言 *))
    POST [ tint ]
      PROP ()
      LOCAL (temp ret_temp 0)
      SEP (data_at Tarray(tdouble) 2 (gv _dbls);
           (* 这里添加其他全局变量的断言 *)).

这样在验证dbls[1]的访问操作时，VST会自动从data_at断言中推导该位置的对齐和大小兼容性，无需手动处理。

内容的提问来源于stack exchange，提问作者TJ Machado