验证条件生成

上一节结束时，契约、循环不变式与内联断言都已写进程序。本节回答一个悬而未决的问题：符号执行引擎如何处理这些断言？ 答案是：将“程序满足规约”这个命题，机械地归结为有限条形如 p |-- qp |-- q 的分离逻辑蕴含——验证条件（Verification Conditions，VC）。 只要每条 VC 都得到证明，函数即满足契约。 本节先回顾经典方案（最弱前置条件演算）及其在 C* 上不够直观的三点，然后介绍 C* 实际采用的前向符号执行，最后用三个例子逐一说明 VC。 如何证明这些 VC，是后续章节的主题。

回想基于分离逻辑的规约中的霍尔三元组 。 契约与不变式写好之后，剩下的问题是机械的：如何从一个带标注的程序，算出需要证明的逻辑命题？ 一个经典方法是 Dijkstra 提出的最弱前置条件（Weakest Precondition，WP）演算： 是“执行语句 后 成立”所需的最弱前置条件，沿程序结构递归定义：

循环则借助标注的不变式 ：取 ，同时额外产出两条义务——保持 与出口 。 于是检查整个函数归结为一条蕴含：

这就是经典的验证条件生成器（VCGen），不少演绎验证工具正是按这个思路工作的。

看一个具体例子。下面的程序计算 （），目标后置条件是 ：

给循环标注不变式 ，机械展开 wp——先由循环规则得到 及两条义务，再经两次赋值规则把 中的 、 依次替换为 、——整个函数最终归并为一条公式：

逐一检查：入口与保持都成立，但是出口无法证明—— 只说明循环停了，没说 ；若 为负， 无法推出 。 执行中 显然不会为负（、每轮减一），但这条信息未被记录在不变式中，WP 演算便无从利用。 把不变式加强为 ，三段就都成立了——这正是上一节“边界事实要一并纳入不变式”准则的一个实际体现。

WP 演算简洁漂亮，但直接搬到 C* 这样的工具上，有三点与使用体验不太契合。

其一，方向与程序相反。 先算 再算 ：计算从 ensureensure 出发逐句往回代换，而人写程序、读程序、调试程序都是自上而下。 上面 的例子里，“出口无法证明”是在整条公式算完之后才显示出来的，所以如果出了错，一般而言难以回答“程序的哪一行出了问题”。

其二，一个函数一条大 VC。 WP 把整个函数体归并为一条公式：五行的 简单程序的 VC 已然不小；真实的 C 函数带指针、结构体与分支，每一步的内存效应都要编码进公式，公式规模可能迅速膨胀。 一条巨型 VC 若无法证明（或自动求解超时），用户几乎无从下手。

其三，分离逻辑需要魔术棒。 在分离逻辑上重做 WP，读写堆的语句需要新的连接词。以基于分离逻辑的规约中的写入语句 为例，其最弱前置条件是：

其含义是：当前堆能分离出 处那个单元（故写入安全），且将 处那个单元改为 后重新拼接回去时 成立。 这里的 正是上上节记号表里的魔术棒（Magic Wand）： 表示“再拼接上一块满足 的堆，就得到满足 的堆”。 魔术棒让 WP 在分离逻辑中依然可以按程序结构计算，但包含魔术棒的蕴含的自动求解目前仍是难题。

三个不直观之处指向同一个方向：与其让后置条件往回算，不如让断言沿执行方向往前流——每行都有一个“当前状态”，义务在产生它的那一行就地弹出。 这正是 VSCode 中逐行查看符号状态所呈现的效果。

C* 当前默认启用的符号执行引擎由 QCP（Qualified C Programming） 提供。 QCP 与 WP 方向相反：从 requirerequire 出发，沿程序方向逐句计算最强后置条件（Strongest Postcondition），并在过程中生成多条细小的 VC。 QCP 的前向风格源自 VST-Floyd：那里的证明每一步向前推进一条“当前断言”，任意时刻的证明目标都是“当前断言 + 剩余程序”，如同自上而下填写一份证明大纲。 QCP 把这套方法从交互式证明融入自动化工具，用代码标注引导执行；选择前向的一个直接动机是实时反馈——每写一行代码就能立即符号执行、看到这一行之后的状态，甚至对尚未写完的函数也能增量验证。

在引擎眼中，符号状态（Symbolic State）就是一条分离逻辑断言——正是在 VSCode 中逐行查看到的那条：existsexists 绑定的逻辑变量、factfact 纯事实、data_atdata_at 与表示谓词组成的空间部分。 执行从 requirerequire（参数以 __pre__pre 等入场）出发，对每种语句按固定规则推进：

• 声明与赋值：更新该变量 data_atdata_at 的内容——表达式中各变量的当前值从状态中获取；
• 读内存（*p*p、v->tailv->tail）：在空间部分寻找恰好那个单元的 data_atdata_at 并读出值；找不到就报错停机——引擎不会自行按定义展开表示谓词（下文例子二、三将看到）；
• 写内存：同样先找到那个单元，然后替换其内容；
• 分支：状态一分为二，分别并入条件与其否定，各自推进；
• 循环：以不变式为割点——执行到循环头，弹出一条 VC（“当前状态 |--|-- 不变式”）；随后只带着不变式（合取循环条件）进入循环体；循环体末尾回到循环头，再弹出一条 VC（保持）；循环之后，以“不变式 **** 条件之否定”继续推进；
• 内联断言：弹出一条 VC（当前状态 |--|-- 断言），随后以断言为新状态——上一节已经讲过；
• 函数调用：把被调用函数 requirerequire 声明的资源从当前状态中逐项匹配移除、换成 ensureensure 给出的资源，状态的其余部分保持不变——这正是框架规则在引擎中的化身；匹配后剩余的纯事实弹出为 VC；
• 函数出口：弹出一条 VC——（移除局部资源的）当前状态 |--|-- ensureensure（__return__return 代入返回值）。

所有 VC 都是同一形状 p |-- qp |-- q：左边是引擎一路算出的符号状态，右边是你写的断言（不变式、内联断言、被调函数的 requirerequire 或本函数的 ensureensure），并且每条都带着产生它的源代码行号。 除此之外引擎还会产出第二类 VC——安全 VC：在算术溢出、除零、移位越界等 C 未定义行为的风险点，弹出相应的纯事实义务（例子一将见到）。

对照 WP 的三个不直观之处，前向符号执行恰好逐一消解：

• 前向：状态沿执行方向推进，每一行都有一个可查看的符号状态——VSCode 面板“写一行、看一行”的实时反馈正建立在此之上；
• 小而多：VC 在标注处就地弹出、各带行号，哪条无法证明就回哪一行去看；
• 无需魔术棒：读写内存靠状态中已有的 data_atdata_at，调用靠逐项匹配，全程不需要魔术棒。

还有一点值得说明：并非每条蕴含都会成为你看到的 VC。 QCP 引擎内置了蕴含求解器（基于规则的匹配策略加上轻量算术求解）：堆部分逐项对齐、平凡的纯事实当场消解，能自动解决的不会呈现出来。 所以最终看到的 VC 是自动化剩下的作业——往往空间部分已经对齐，留下的是真正需要人证明的纯事实，或需要按定义展开谓词的那一步。

理论讲完，看真实案例。上一节的 Gauss 求和：

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

对这个文件运行验证，得到三条 VC（输出为适配页宽做了换行处理；行号按上面的代码清单计）：

逐条阅读，有以下观察：

• 首先注意未出现的 VC：循环入口的“建立”不在列表里。进入循环前状态是 ss、ii 两个单元的内容为 0i0i 的精确形态，与不变式逐项匹配后只剩 一类平凡算术，被引擎当场消解——能自动解决的不会呈现出来。
• VC 1 是安全 VC：s + is + i 的结果必须落在 intint 范围内。前件里 ii 的内容已是 iv + 1iiv + 1i（上一行 i = i + 1i = i + 1 已经执行，它自己的溢出检查借助 iv < n__pre <= 1000iv < n__pre <= 1000 被自动消解），要证 sv + iv + 1isv + iv + 1i 不溢出，得从 2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i) 结合边界事实推导出 svsv 的上界——非线性推理超出引擎内置算术求解器的能力，于是保留为 VC。这也解释了上一节的准则：fact(n__pre <= 1000i)fact(n__pre <= 1000i) 若不记录在不变式里，这条 VC 缺少证明的依据。
• VC 2 是保持：前件是执行完循环体的状态（ss、ii 的内容都已更新），后件是整条不变式（existsexists 重新出现）。证明它，就是给 iviv、svsv 挑选新的实例并验算各条 factfact。
• VC 3 是出口：|--|-- 左边是“不变式 **** 循环条件之否定”，data_atdata_at 全部消失只剩 empemp——返回时局部变量的存储单元由引擎回收，纯事实留下；右边是 ensureensure（__return__return 已代入 svsv）。剩下的正是“由 、、 推出 ”这一步初等数学。

这个例子展示了 VC 的常态：空间部分已被引擎对齐消解，留给人的多是纯算术事实。

数组与链表的例子在上一节尚缺少一部分讨论：不变式里的资源折叠在包装谓词里，直接执行会报错。现在来看实际的报错信息。 把上一节 clearclear 循环体内的内联断言移除再验证，引擎在 *p = 0*p = 0 处停机：

注意这是错误，不是 VC：写入 *p*p 需要状态中已有的那个单元 undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar，而它折叠在 undef_suffixundef_suffix 之中；引擎不会替你决定何时按定义展开谓词，于是执行无法继续。 报错随附的符号状态正是排障的线索——一眼可见缺失的资源在哪个谓词的定义之中。

补回上一节那条“展开一步”的内联断言，整个函数就能完整执行，生成四条 VC：

与例子一不同，这次连“建立”也保留为 VC——把 undef_bytes arr__pre n__preundef_bytes arr__pre n__pre 改写成“零单元前缀 **** 整段后缀”（zero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__prezero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__pre）需要按定义展开这三个谓词，超出自动策略的范围。 四条里最值得细看的是断言那条（VC 2）——上一节说“assertassert 并没有消灭证明义务，只是把它从‘受阻执行’变成‘留待证明’”，正是指这条 VC：

两边几乎逐项相同，全部差异集中在最后一行半：左边的 undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre 要拆分为第一个单元与剩余后缀。这一步依赖 undef_suffixundef_suffix 与 undef_array_atundef_array_at 的定义，正是将来要写的证明。 出口那条（VC 4）则比较短：

由边界事实得 iv == n__preiv == n__pre，长度为零的后缀化为空堆，前缀恰好是整段——上一节“出口”的那句叙述，在这里被压缩为一条蕴含。

链表的情况基本相同。去掉内联断言直接验证 reversereverse，引擎在读 v->tailv->tail 时停机：

tailtail 字段那个单元折叠在 sll vv l2sll vv l2 里。补回上一节的断言后执行通过，同样得到四条 VC（建立、断言、保持、出口）。断言那条把 sllsll 按非空分支展开：

证明它要用到两条事实：vvvv 非空时 sll vv l2sll vv l2 只可能来自定义的 CONSCONS 分支，于是 l2l2 必为某个 x :: xsx :: xs，头结点的两个单元 data_atdata_at 与余下的 sll q xssll q xs 随之呈现出来；列表侧则要把 l == l1 ++ l2l == l1 ++ l2 改写为 l == l1 ++ x :: xsl == l1 ++ x :: xs。

保持那条 VC 的前件如实记录了三指针舞步之后的局面——ww 的内容已是 vvvv、vv 的内容已是 qq、头结点的 FtailFtail 那个单元已改写为 wvwv——要把它们重新折叠为不变式的两段 sllsll。出口那条同样简短：

上一节“出口”的三行叙述压缩为一条蕴含：由 vv == 0ivv == 0i 与 sll vv l2sll vv l2 走定义的空列表分支得 l2 == []l2 == []，于是 l1 == ll1 == l，左边的 sll wv (REVERSE l1)sll wv (REVERSE l1) 正是要证的结论。

本节展示的输出都可以在 VSCode 中获取，入口与查看符号状态相同（右键 Show Symbolic StateShow Symbolic State）：

• 光标在函数体内的行上：面板显示该行的符号状态——即前向符号执行推进到此处的最强后置；
• 光标在文件级的行上（比如文件末尾）：面板显示截至该处累计的验证条件列表，每条标着编号与行号（VC n line lVC n line l），展开后按 |--|-- 分为两侧。

VC 列表非空，意味着验证尚未完成——它们正是接下来要用证明填补的缺口：在 [[cst::proof]][[cst::proof]] 中写证明代码构造定理、改写符号状态，直到引擎能把每条 VC 都消解。这是后续章节的主题。

• 验证条件（VC） 是形如 p |-- qp |-- q 的分离逻辑蕴含：左边是引擎算出的符号状态，右边是你写的断言；程序满足规约 所有 VC 得到证明。
• 经典的 WP 演算从 ensureensure 往回代换、整个函数归并为一条大公式，且在分离逻辑上需要魔术棒——三个不直观之处。
• C* 默认的符号执行引擎由 QCP 提供，思想源自 VST-Floyd：从 requirerequire 出发沿程序方向计算最强后置条件；VC 在循环头（建立/保持）、内联断言、函数调用与函数出口就地弹出，另有溢出、除零等安全 VC，各带行号。
• 读写内存所需的资源必须在状态中直接可见：缺少资源是错误而非 VC；何时按定义展开谓词由你用断言（或证明）决定。
• 引擎能自动消解的蕴含不会呈现出来：看到的 VC 是自动化剩下的作业，常见形态是“空间已对齐，剩纯事实”与“差一步定义展开”。