符号执行 | Codeboy's Blog

形式陈述

一个状态代表哪些具体运行

固定控制流图及其语言语义。本页主算法使用无循环、确定性顺序整数程序，操作纯粹且总定义，全部读取有定义，唯一末尾返回；没有堆、异常、并发或机器整数溢出。用 $X,Y$ 表示初始输入符号，而 x,y 仍是可被赋值的程序变量。

符号状态为 $(\ell,\sigma,\Phi)$ ： $\ell$ 是下一控制位置， $\sigma$ 把当前变量映为输入符号表达式， $\Phi$ 是输入必须满足的路径条件。其含义是：每个满足 $\Phi$ 的输入 $a$ 都能沿记录前缀到达 $\ell$ ，且该处变量 $v$ 的实际值为 $\llbracket\sigma(v)\rrbracket_a$ 。初态有 $\sigma(x)=X,\sigma(y)=Y$ ， $\Phi$ 等于允许输入的前置条件。

对赋值 v:=e，先用旧 $\sigma$ 替换 $e$ 中的变量，再更新

\sigma':=\sigma[v\mapsto e[\sigma]].

不能先覆盖 v 再求右侧；例如 x:=x+1 必须读旧 x。对判断 b，令 $B=b[\sigma]$ ，产生真、假两个候选状态，路径条件分别为 $\Phi\land B$ 和 $\Phi\land\neg B$ 。

路径是否存在输入是公式可满足性问题。通过SMT或该模型的其他精确判定器检查条件。UNSAT 分支可删；SAT 分支保留并可取得输入模型；unknown 分支仍未解决，不能按 UNSAT 删除。主算法在所有可行分支上继续，直到返回或待报告的错误节点。[1, §§1、5]

算法维护的覆盖责任

队列初始只有入口状态。每次取一项，赋值生成一个后继，分支生成两个经可靠可满足性检查的后继，返回状态记入结果。单步不变量由表达式替换和真/假互斥穷尽直接保持；对执行长度归纳，任何实际运行都被某个已处理前缀或待处理状态覆盖。

要证明规格 $Q$ ，在每个终端状态检查 $\Phi\land\neg Q[\sigma]$ 。其中一个 SAT 模型给出候选失败输入；按原程序重放后才报告具体轨迹。只有队列已完整处理、所有终端反例条件均 UNSAT、且不存在 unknown 或被截断的路径，才能据此推出所建模输入范围内的全称正确性。

直觉

给值保留来历

实际执行会把 a:=x+1 算成某个数。符号执行暂不选择输入，记下 $a=X+1$ 。到 if y==a 时，它问的就是 $Y=X+1$ ，不是两个没有关联的新变量是否相等。

因此一条符号路径代表一组输入。求解器的任务是判断这一组是否为空并给一个成员，而非替程序做一次随机猜测。路径公式还必须记录此前的分支条件；遗漏前缀会把无法到达该判断的输入也混入。

例子与边界

三条路径，三个返回表达式

使用前页切片，初始 $\Phi=\top$ 。先得到 $a=X+1,r=0$ 。判断4为假时直接返回；为真时再遇到判断5。全部终端状态为

分支记录	路径条件	返回值
4F	$X\le0$	0
4T、5T	$X>0\land Y=X+1$	1
4T、5F	$X>0\land Y\ne X+1$	2

三条件两两不交并覆盖全部整数输入。若规格为返回值不等于1，唯一失败公式为 $X>0\land Y=X+1$ ，输入 $(1,2)$ 是其中一个模型。重放原程序：a=2，两个判断都真，执行6后 r=1，9返回1。

下载脚本的判定器枚举明确的有限域 $D=[-2,2]^2$ 。三条路径分别覆盖15、1、9组输入，共25组；这个域内失败输入只有 $(1,2)$ 。域外如 $(2,3)$ 也失败，说明“唯一反例”只有附上 $D$ 才正确。脚本没有调用 SMT，更没有把25次检查说成无界整数求解。

可行性与错误不能分开求

若在 if x>0 内增加 if x<=0，内层真条件为 $X>0\land X\le0$ ，UNSAT。只单独问 $X\le0$ 会得到0，却不能走到内层判断。报错模型必须满足从入口到错误的同一个合取公式。

赋值版本也不能混淆。执行 x:=x+1; if x==0 后，分支条件是 $X+1=0$ ，所以初始输入应为 $X=-1$ ；把条件误写成 $X=0$ 会生成重放失败的测试。

路径和算术都有边界

有 $b$ 个相互独立二路判断时，可行终端路径最多可达 $2^b$ 。合并状态可以共享公式，却不能在汇合处直接合取互斥路径的条件；应保留分支和值的对应，例如带 guard 的析取或 ite。

带循环时，逐次展开可能无穷。只展开 $k$ 轮所得的是带界结果，未处理回边仍是未完成责任；全局安全可转向候选不变式筛选等证明方法。堆别名、异常、外部调用与位向量回绕也必须加入语义后再分析，本页整数替换规则不自动覆盖它们。

推论与应用

如何给搜索成本记账

设实际探索了 $p$ 条长度至多 $\ell$ 的路径，若逐路径复制，语句处理次数有 $O(p(\ell+1))$ 上界。每步还要支付表达式替换、路径公式构造和求解成本；表达式展开可能膨胀，求解器更不能按一次常数工作计费。持久映射和表达式 DAG 可共享旧表达式，改变实际存储，却不消除可行路径的最坏指数数目。

在下载的有限判定器中，一次含 $j$ 个分支条件的查询至多扫描 $|D|$ 组输入，逐项计算这些表达式；成本由这些表达式的实际求值工作乘 $|D|$ 控制。它提供一个可审查的精确小域后端，目的不是模拟工业求解器的性能。

混合执行保留一份真实运行，并沿这次运行同步记录同样的符号表达式。它每轮有意翻转一个路径前缀，再用新输入重跑，提供另一种遍历路径的调度方式。

迁移练习：将6改成 r:=a-y，重新检查返回值不等于1。5T 路径上 $a-y=X+1-Y=0$ ，其余路径仍返回0或2，所以断言在本页数学模型下成立；关键是利用路径条件化简返回式，而非只看6出现了减法。

参考资料

[1] James C. King，Symbolic Execution and Program Testing，Communications of the ACM 19(7)，1976，385–394页；§1给符号赋值与路径分叉，§5说明符号执行和具体代入的对应。本文独立给出当前队列接口、三路径算例及有限域复算范围。

形式陈述 ​

一个状态代表哪些具体运行 ​

算法维护的覆盖责任 ​

给值保留来历 ​

三条路径，三个返回表达式 ​

可行性与错误不能分开求 ​

路径和算术都有边界 ​

如何给搜索成本记账 ​

反向链接