可满足性模理论 (Satisfiability Modulo Theories)

RSS 阅读器可能不支持渲染数学公式。 点击这里阅读原文：

SMT 的出现，本质上是为了解决一个核心矛盾：很多实际问题用纯命题逻辑（SAT）表达时，要么根本无法表达，要么表达后规模爆炸；而用一般的一阶逻辑或高阶逻辑表达虽然自然，却无法自动高效求解。

看一段再普通不过的代码：

voidf(int x, int y) {
    int a[100] = {0};
    a[0] = 5;
    if (x + y > 10 && a[0] == 5) {
        // 目标分支
    }
}

假设 x、y 是来自外部的整数。我们想知道：有没有一组输入，能走进这个分支？

沿着这条路径，把进入分支需要满足的条件收集起来：

问题于是变成：这组约束有没有解？

纯 SAT 求解器也能做，但你得先把 x、y 各拆成 32 个布尔变量，把加法展开成加法器电路，把数组展开成 100 个元素，最后交给它几千条子句。它只认识真假，不认识整数，也不认识数组。

SMT 求解器则直接读原式：x + y > 10 交给算术，a[0] = 5 交给数组。算术说取 x = 6, y = 5 就行，数组说 a[0] = 5 本来就成立。两边一对，返回 sat，并给出这组解。

同一个问题，一个要把语义拆成门电路，一个能直接利用语义。SMT 要做的，就是后者。

一、SMT 是什么

1.1 定义

把上面的过程抽象一下。SMT 是「SAT + 背景理论」：在某个理论 规定的语义下，判定一个一阶逻辑公式是否存在满足它的赋值。

这里的关键词是「模理论」（modulo theories）。「模」可以理解为「相对于」：我们不再问公式在全部数学结构里是否成立，而是问它在某个特定理论——比如整数算术、位向量、数组——的解释下是否成立。

形式化一点，SMT 要回答的是：

也就是：是否存在一个赋值 ，把每个变量映射到理论域里的值，使得 在这个理论的所有公理下为真。

回到开头的例子： 是算术原子， 是数组原子，理论 就是整数算术与数组的组合。SMT 要回答的，正是这组原子能不能同时为真。

1.2 公式的样子

SMT 公式由布尔结构和理论原子组成：

其中 是理论原子，形如 、、、。原子内部的项由变量、常量和理论函数符号组成。

下面这个公式同时用到了三种理论：

• 属于线性整数算术：它知道 是加法、 是全序；
• 属于数组理论：它知道 select 和 store 的读写语义；
• 属于未解释函数：它不知道 具体算什么，只知道「同一个输入必须得到同一个输出」。

对 SAT 来说，这三个原子只是三个裸的布尔变量 。对 SMT 来说，它们各自带着一整套内部结构。

这张图就是 SMT 的骨架：布尔层负责「怎么组合」，理论层负责「每个原子是什么意思」。

1.3 背景理论

SMT 里常用的理论有这么几类：

• EUF（QF_UF）：只处理相等和未解释函数，适合描述对象相等、指针别名。
• 线性算术（QF_LRA / QF_LIA）：处理 、 和常数；实数版是 QF_LRA，整数版是 QF_LIA。
• 非线性算术（QF_NRA / QF_NIA）：允许乘法；实数版可判定，整数版不可判定。
• 位向量（QF_BV）：描述机器整数和硬件电路，加法是模 的。
• 数组（QF_AX / QF_AUFBV）：用 select 和 store 描述内存读写。
• 浮点（QF_FP）：描述 IEEE 754 浮点运算。
• 字符串：描述 concat、contains 等操作，工业实现常常不完整。

QF 是 quantifier-free 的缩写，意思是「无量词」。绝大多数 SMT 求解器面对的都是这个片段。

可以把 SAT 看成 SMT 的一个特例：当理论 为空、所有原子都是裸命题时，SMT 就退化成 SAT。

反过来，SMT 也可以看成 SAT 的一次「语义升级」：布尔骨架不变，但每个命题不再是黑盒，而是有内部结构、可以被理论求解器检查和反驳的对象。

这个升级带来的好处，要放到具体的历史困境里才看得清楚。

二、SMT 之前

2.1 位爆破

SAT 只认布尔变量。要用它处理整数，标准做法叫位爆破（bit-blasting）：把整数拆成一个个布尔变量，再把算术运算展开成逻辑门电路，最后用 Tseitin 变换把电路转成 CNF 子句。

看一个具体的小例子。取两个 4 位无符号整数 ，约束是：

SAT 看到的是 8 个布尔变量 和 。为了表达加法，需要 4 个全加器。每个全加器有三个输入 、两个输出 ，满足：

把这两个等式转成 CNF，一个全加器大约 17 条子句。4 位加法器就是 4 个全加器，约 70 条子句。再加上「和等于 1010、进位为 0」的 5 条单元子句，以及一个 4 位比较器的几十条子句，整个约束变成一百多条子句、几十个辅助变量。

而原始约束只有一行：

x + y == 10 && x > y

求解器可能给出 、，但它并不知道这是 6 和 4。它只知道这一组真假值恰好让所有子句为真。

规模还不是最麻烦的，语义丢失才是。假设我们想证明 。在算术里这是一条公理，一秒都不用。但在 SAT 里，左边是一个「先加 再加 」的电路，右边是一个「先加 再加 」的电路，两个电路内部结构不同，SAT 只能把两边都展开，再逐位证明输出相等。它不知道「加法可交换」，只知道一堆门。

打个比方：这就像为了判断一首诗是否押韵，先把它拆成一个个字母，再让机器从字母的排列里重新发现什么是韵脚。信息没有丢，但结构没了。

2.2 不可判定

那干脆用表达力最强的一阶逻辑，让自动定理证明器去证，不行吗？

不行。看一个具体方程：

它看起来很简单。它有整数解，一个已知解是：

这三个数都是 16 位数，直到 2019 年才被找到。如果把 都编码成 64 位整数，搜索空间是 ；按每秒试十亿个赋值来算，也要 年量级。位爆破在这里基本不可行。

更根本的是，这不是「这一个方程特别难」的问题。希尔伯特第十问题问的是「是否存在算法判定整系数多项式方程有没有整数解」，这个问题在 1970 年被马蒂亚谢维奇证明为否。证明的思路很巧妙：任给一台图灵机和一段输入，都能构造出一个整系数多项式方程，使方程有解当且仅当图灵机停机。既然停机问题不可判定，一般的方程判定问题也不可判定。换句话说，想写一个能判定所有这类方程的通用算法，这件事本身就是不可能的。

工程上的后果很直接：自动定理证明器可能跑了一整天，最后告诉你「我不知道」。对于一个需要每秒判定成千上万条路径条件的程序分析工具来说，这是不可接受的。

2.3 难以组合

另一条路是「一个问题配一个专用算法」：线性规划用单纯形法，只懂实数线性约束；并查集只懂「相等」；BDD 只懂布尔函数；自动机只懂正则语言和字符串匹配。

这些算法在各自领域都很好用，但真实的程序约束往往是混合的。看一个只有两个原子的例子：

假设我们分别去问两个求解器：

• 算术求解器只看 ，回答 sat，比如 ；
• EUF 求解器只看 ，也回答 sat：它把 当成两个不同的常量，令 、。

如果把两个答案一拼，说「两边都可满足，所以整体可满足」，就错了。因为 意味着 必须等于 ，与 直接矛盾。整体其实是 unsat。

要得到正确答案，两个求解器必须交换信息：算术把等式 告诉 EUF，EUF 立刻推出 ，冲突。谁来负责交换？交换哪些事实？什么时候交换？在 SMT 之前，这些都是需要人工设计的事情。

数组和算术之间也有同样的坑。i = j ∧ a[i] ≠ a[j] 单独看两边都可满足，合起来却不可满足，因为下标相等就意味着读到的值相等。没有任何一个专用算法能独自看出这一点。

2.4 门槛太高

还有一条路是 Coq、Isabelle、ACL2 这类交互式定理证明器。它们的表达力极强，能处理带量词、带归纳的复杂性质，但代价是需要人写证明脚本。

比如在 Coq 里证明「任何自然数加零都等于它自己」，要写：

Theorem plus_0_r : forall n : nat, n + 0 = n.
Proof.
  induction n as [| n' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

这几行不是装饰：

• induction n 把目标拆成两种情况： 和 ；
• 第一种情况，simpl 把 化简成 ，reflexivity 确认两边相等；
• 第二种情况，simpl 把 化成 ，再用归纳假设 IH 把 换成 ，最后 reflexivity 收尾。

每一步往哪走、用哪条归纳假设，都是人选的。这还只是自然数加零。真实的程序验证要证循环不变式、数组不变式、指针分离，脚本可能几百上千行。

程序分析场景里，工具每秒要生成并判定几千条路径条件。不可能每条都停下来等工程师写一段证明。自动化程度不够，就无法工业部署。

2.5 小结

几条路，各有各的难处：

• 纯 SAT 快，但把高层语义压成门电路之后，规模爆炸、语义丢失；
• 一阶逻辑表达力强，但一般情形不可判定，自动证明器可能永远给不出答案；
• 专用算法在自己的理论里很好用，碰到混合约束就各自为政；
• 交互式定理证明能处理复杂性质，但每条路径都等人写脚本，工业化无从谈起。

SMT 要做的，就是在这几条路的夹缝里找一个中间地带：表达力足够描述程序，判定过程保证自动，还能把多个理论组合起来。

三、SMT 的解法

3.1 收缩片段

SMT 的第一个策略是主动放弃一部分表达力，只保留可判定的片段。

具体做法是：把主战场放在无量词片段，只允许特定理论的组合。这样既避开了 2.2 节里的不可判定性，又保留了描述程序行为所需的大部分能力。

为什么可以放弃量词？因为程序分析产生的验证条件，大多数天然就是无量词的。符号执行收集到的路径条件，是对「这一条路径上各个变量的具体取值」的约束，不需要「对所有 ，」这种全称陈述。

需要量词的地方——循环不变式、数组的整体性质、归纳证明——通常由上层工具负责：抽象解释负责生成不变式，-induction 负责把归纳化归为有限次查询，SMT 只作为底层的判定引擎。这是一个分工，而不是缺陷。

当然，「可判定」不等于「容易」。QF_UF、QF_LIA、QF_BV 都是 NP-complete；QF_LRA 是多项式时间；QF_NRA 可判定，但最坏情况是双指数；QF_NIA 则直接不可判定。

SMT 在选定的片段内保证了「答案一定会来」，但不保证「答案来得快」。工程上的成败，很大程度上取决于启发式和问题编码。

3.2 直接表达

第二个策略是让公式直接说人话。

同样是「 且 」，SMT 不需要把 拆成 64 个布尔变量，也不需要把数组展开成 100 个元素。它把这两个条件原样保留为两个理论原子，交给对应的求解器。

关键在于「按需展开」：

• 算术：直接用单纯形法或分支定界，在整数/实数域上推理，完全不经过布尔编码。
• 数组：用 read-over-write 公理，只在公式里真的出现某个下标时才实例化。
• 位向量：这一条要诚实一点——大多数求解器内部仍然会做位爆破，因为位级编码对硬件电路太有效了。但这件事发生在求解器内部，只针对相关子表达式，而且会配合字级重写（比如 、）和等价类合并。对使用者来说，它仍然是透明的。

数组的 read-over-write 公理长这样：

如果公式里只关心 ，求解器就只实例化 这一条，剩下的 99 个元素根本不会出现。这是「按需」和「全局」的区别，也是 SMT 能在数组上跑赢位爆破的原因。

所以更准确的说法不是「SMT 消灭了底层编码」，而是：SMT 把「怎么编码」的决定权从用户手里交给了求解器。求解器可以根据理论特性选择最合适的内部表示，而不是让用户先做一次不可逆的全局展开。

用同一个约束对比一下。纯 SAT 的版本要生成数百到上千个布尔变量、上千条子句；SMT 的版本只保留两个理论原子。SAT 只能做布尔剪枝，SMT 能利用算术和数组的语义；SAT 的答案是一组布尔赋值，还要反解出 ，SMT 直接给出 。

3.3 组合理论

第三个策略是让不同理论通过共享等式来协作。

最经典的方法是 Nelson–Oppen 组合。它的前提是：两个理论的签名不相交（各自管各自的符号），并且都满足「稳定无限」性质（任何可满足的公式都有无穷模型）。在这个前提下，两个理论只需要交换变量之间的等式，就能组合成一个完整的判定过程。

看一个例子：

• 算术部分看到 ，本身没有矛盾；
• EUF 部分如果不知道 ，就会认为 和 可以不同，也不会报错；
• 一旦算术把等式 传给 EUF，EUF 立刻推出 ，与 冲突。

于是整个公式被判为不可满足。这个结论不是某一个理论单独得出的，而是两个理论「对了一下账」才对出来的。

再看一个反方向的例子：

这里算术部分自己就能算出 ，直接判 unsat，根本不需要 EUF 参与。

现代求解器（Z3、cvc5 等）通常不严格照搬经典 Nelson–Oppen，而是在 DPLL(T) 框架下做「理论传播 + 冲突解释」。但核心思想没变：每个理论只懂自己那一摊，通过交换少量关键事实来达成全局一致。

有一个细节值得注意：如果理论是「非凸」的，光交换等式还不够。比如在整数算术里， 等价于 ，这是一个析取，没法用一组等式表达。上层只能做情况分裂（case split），分别假设每一支再检查。这会让组合复杂度上升，也是混合理论求解有时会突然变慢的原因之一。

3.4 给出解释

第四个策略是不只回答是或否，还给出可操作的结果。

• sat：求解器返回一个模型，给出每个变量的具体取值。对符号执行来说，这就是一条能触发目标路径的测试输入。
• unsat：求解器可以返回一个 unsat core，也就是一组不可满足的子约束，告诉你「是这几条打架了」。
• 插值：从 的不可满足性中提取一个只含共同变量的中间公式（Craig interpolant），用于程序验证中的不变式合成和抽象精化。
• 证明：部分求解器能输出 resolution 证明，供独立检查，避免「求解器说有漏洞，但你不知道为什么」的黑盒困境。

这一点经常被忽略，但它决定了 SMT 能不能真正嵌进工具链。一个只会输出 unsat 的求解器，在调试时几乎没用；一个能告诉你「第 3、7、9 条约束冲突」的求解器，才能帮工程师定位问题。

3.5 增量求解

第五个策略是增量求解（incremental solving）。

符号执行的路径是一棵树：父路径的约束是子路径约束的前缀。如果每换一条路径都从头求解，大量工作会被重复浪费。

SMT-LIB 提供了 push / pop 和 check-sat-assuming，允许在已有约束的基础上临时加入假设、求解、再回退。求解器会保留之前学到的子句和理论状态。一条路径判 unsat 后回退到分叉点，下一条路径可以接着用。

KLEE、angr 这类工具都重度依赖这个特性。没有增量求解，符号执行的性能会差一个数量级。

四、DPLL(T)

4.1 总体架构

现代 SMT 求解器的标准架构叫 DPLL(T)，更准确的名字是 CDCL(T)：外层是带冲突学习的 SAT 求解器，内层挂一个或多个理论求解器。

用一句话概括这个循环：

1. 把公式里的每个理论原子替换成一个命题变量，得到一个纯布尔公式；
2. 让 SAT 求解器找一个布尔模型；
3. 把布尔模型翻译回理论原子的真假，交给理论求解器检查；
4. 如果理论层说「一致」，就得到 sat 和模型；
5. 如果理论层说「冲突」，就把冲突总结成一条新的布尔子句，塞回 SAT 层，让它换个方向再搜；
6. 如果 SAT 层把所有可能性都穷尽了，就得到 unsat。

可以把它想象成一个总承包商和几个专业工种的协作：总承包商（SAT）负责排期和组合，电工、水管工（理论求解器）负责检查自己那部分是否可行。电工说「这个排期下电线会短路」，总承包商就把这条经验记下来，换一个排期重新试。

4.2 布尔抽象

布尔抽象（也叫 propositional abstraction）是两层之间的接口。

以这个公式为例：

引入三个命题变量：

布尔骨架变成：

SAT 求解器在这个骨架上的搜索空间只有 种赋值。它先试 ，把这三个真值交回理论层。

理论层看到的是三个文字（literal）：

线性算术求解器立刻发现：前两个推出 ，与第三个矛盾。这是一次理论冲突。

注意，理论层收到的不是「原子为真」，而是「带正负号的文字」。 对应的是 ，也就是 。理论求解器必须能处理这种否定形式，这也是为什么它通常直接操作形如 的不等式，而不是只处理等式。

4.3 CDCL

SAT 层用的是 CDCL（冲突驱动子句学习）。它的核心循环大致如下：

loop:
    conflict = unit_propagate()      # 单元传播
    if conflict:
        if decision_level == 0: return UNSAT
        lemma = analyze(conflict)    # 冲突分析
        backtrack()                  # 非时序回跳
        add_clause(lemma)            # 学习子句
    else:
        if all_variables_assigned(): return SAT
        decide()                     # 选一个未赋值的变量

三个关键机制：

• 单元传播：一条子句里只剩一个未赋值的文字时，强制它取能让子句为真的值。
• 冲突分析：从冲突出发，反向找出是哪几个决策导致的，生成一条新的子句。这条子句是原公式的逻辑推论，加进去不会改变解集。
• 非时序回跳：不退回上一层，而是直接跳回冲突的真正源头，跳过大量无用的搜索。

CDCL 是过去二十年 SAT 求解器性能提升的主要来源。SMT 做的事情，基本上是把这套成熟的工程能力「复用」到理论层。

4.4 理论求解器

理论层要做的事情叫 T-一致性检查：给定一组带正负号的原子，判断它们在理论 下是否可能同时为真。

不同理论有不同的算法。

EUF

EUF（Equality with Uninterpreted Functions）只关心相等关系和函数的一致性。核心是两件事：

1. 用并查集维护变量的等价类；
2. 用同余闭包（congruence closure）保证：如果 ，那么 。

例子：

并查集把 合并成一个类；同余闭包发现 和 的参数相等，于是把 也合并；但公式又要求它们不等，冲突，判 unsat。

EUF 在程序分析里非常有用，因为指针别名、对象身份、类型相等，本质上都是「未解释函数的相等性」。

线性算术

QF_LRA 用单纯形法（更准确地说，是 SMT 里常用的 general simplex）。它先维护一组满足所有等式的赋值，再通过枢轴变换（pivot）调整变量的取值，直到所有上下界约束也被满足；如果怎么调都满足不了，就报告冲突。

QF_LIA 在此基础上加分支定界：先按实数求解，如果解里某个整数变量取了小数，就分裂成两支，比如 和 ，分别再解。

例子：

实数松弛下， 是一个解，但 不是整数。分支：

• 假设 ： 只能取 或 ； 时 仍不是整数， 时 ，得到整数解，sat；
• 另一支 就无须再看了。

如果两支都不可行，就判 unsat。实际求解器还会加上割平面（cut）和更强的预处理，避免分支树爆炸。

位向量

QF_BV 最常用的方法还是位爆破：把位向量运算展开成门电路，再交给 SAT 层。但因为位向量有固定宽度，这种展开是有限且可预测的。

现代求解器会先做字级重写，把明显恒真的部分消掉，比如：

然后再决定哪些子表达式值得展开。乘法是位向量的难点，因为乘法器电路规模大，求解器通常会配合专门的乘法推理和等价类传播。

位向量的语义是模运算，这一点非常重要：

在 32 位无符号整数里，唯一满足 的值就是 0xFFFFFFFF，所以这个公式是 unsat。如果把它当成数学整数， 又不等于 0xFFFFFFFF，结论就完全不同。选错理论，漏洞检测就会漏报或误报。

数组

数组理论的核心是 select 和 store 两条操作，以及前面提到的 read-over-write 公理。

求解器不会一次性展开所有下标，而是采用惰性公理实例化（lazy axiom instantiation）：先假设数组是一致的，当检查中发现某个 select(store(...)) 需要用到公理时，才生成对应的引理加入公式。这叫「按需生成」，也叫 lemma-on-demand。

例子：

由 和 read-over-write 公理，左边等于 ；于是 ，与 冲突，unsat。整个过程中，数组的长度、其他下标的值，全都不需要知道。

其他理论

字符串理论通常用自动机或序列理论处理，word equation 本身可判定，但加上长度约束、正则约束后很多片段会变得不可判定，工业求解器往往采用不完整但实用的策略。浮点理论通常把 IEEE 754 的位级语义编码成位向量，再交给 QF_BV 后端。

4.5 冲突学习

理论冲突不会只让当前搜索失败一次，它会变成一条理论引理（theory lemma），永久加入布尔公式。

前面 4.2 节的例子：

这三条文字不可同时为真，所以下面这条子句是理论有效的：

把它翻译回命题变量，就是：

SAT 层学到这条子句之后，就再也不会同时选 都为真了。这一步是 DPLL(T) 效率的关键：理论层的「一次性检查」变成了布尔层的「永久知识」。

如果没有冲突学习，SAT 层会在同一个理论冲突上反复撞墙；有了它，搜索空间被真正地剪掉了。

4.6 完整例子

还是用这个公式：

第 1 轮：SAT 层选择 。理论层检查 ，发现 ，冲突。生成引理 并回跳。

第 2 轮：SAT 层在引理约束下重新搜索，可能选择 。理论层检查：

取 ，三条同时成立。理论层返回一致，求解器输出：

这就是一个完整的 DPLL(T) 循环：一次冲突、一次学习、一次成功。

在真实求解器里，理论层还会做理论传播：不等 SAT 层给出完整赋值，就提前推出某些文字必须为真或为假，从而更早剪枝。这让循环通常只需要很少几轮。

理论正确不代表跑得快。工业级求解器还依赖大量工程优化：

• 预处理：化简公式、消除冗余变量、把公式规范化成求解器偏好的形式。
• 理论传播：理论层主动推导文字，而不是被动等待完整赋值。
• 重启策略：按 Luby 序列或指数策略重启，避免陷入坏的搜索区域。
• 子句删除：学习子句太多会拖慢传播，需要定期清理。
• 多引擎组合：同一个问题用不同策略并行求解（portfolio），谁先出结果用谁。
• 专用推理：针对乘法、数组、字符串等难点，加入专门的推理规则。

4.7 复杂度边界

必须强调：可判定不等于可解。

• SAT 是 NP-complete；
• QF_BV、QF_LIA、QF_UF 也都是 NP-complete；
• QF_LRA 虽然是多项式时间，但实际常数很大；
• QF_NRA 可判定，但最坏情况是双指数；
• QF_NIA 直接不可判定。

这意味着，工业问题的最坏情况仍然是指数级的。求解器的成功，很大程度上依赖问题结构、编码方式和启发式。遇到超时，工具通常只能返回「未知」，而不是「安全」。

这也是为什么实际系统里，SMT 很少单独使用，而是和抽象解释、fuzzing、测试生成等方法组合。

五、漏洞检测

5.1 问题转化

软件漏洞检测的核心问题可以写成一句话：

是否存在一个输入，让程序走到某个危险位置，并且违反某条安全性质？

形式化之后，它就是一个存在性查询：

• 是路径条件，描述「走到这里需要满足哪些约束」；
• 是安全性质的否定，描述「怎样才算越界/溢出/空指针解引用」。

如果这个公式 sat，求解器给出的模型就是一条能触发漏洞的输入，漏洞可达；如果 unsat，说明在这条路径上不可能违反性质，可以安全剪枝。

这个转化是整个应用的基石：「找漏洞」变成了「解约束」。

5.2 缓冲区溢出

先看一个最直观的例子：

voidprocess(char *input, int len) {
    char buf[8];
    if (len > 4 && len < 12) {
        memcpy(buf, input, len);   // 可疑点
    }
}

buf 只有 8 字节，而 memcpy 拷贝 len 字节。如果 len 能大于 8，就会发生栈溢出。

符号执行引擎把 input 和 len 当作符号变量，沿路径走到 memcpy 时，收集到的路径条件是：

要判断溢出是否可达，就在路径条件上再加一条「写入长度超过缓冲区大小」：

写成 SMT-LIB：

(set-logic QF_LIA)
(declare-const len Int)
(assert (and (> len 4) (< len 12) (> len 8)))
(check-sat)
(get-model)

求解器返回：

sat
(model
  (define-funlen()Int9)
)

len = 9 是一个合法解：它满足 ，同时 。这条路径可达，memcpy 会往 8 字节的缓冲区里写 9 字节，溢出 1 字节。是否真的覆盖到返回地址取决于栈布局，但「越界写」这个事实本身已经成立。

如果把代码改成：

if (len > 4 && len <= 8) {
    memcpy(buf, input, len);
}

约束就变成：

求解器返回 unsat。这条溢出路径不可达，工具不会报告漏洞。

注意这里用的是 QF_LIA（整数线性算术）。真实的 C 代码里 len 是 32 位 int，更精确的建模应该用 QF_BV：

(set-logic QF_BV)
(declare-const len (_ BitVec 32))
(assert (and (bvsgt len (_ bv4 32))
             (bvslt len (_ bv12 32))
             (bvsgt len (_ bv8 32))))
(check-sat)
(get-model)

注意这里用的是有符号比较（bvsgt / bvslt），因为 C 里的 int 是有符号的。一个可能的模型是 len = #x00000009。对这个例子来说，两种建模的结论一样；但下一个例子就会看到，理论选错，结论可能完全相反。

5.3 整数溢出

voidcopy(char *src, unsignedint off, unsignedint len) {
    char buf[64];
    if (off + len <= 64) {
        memcpy(buf + off, src, len);
    }
}

看起来检查很严：只有 off + len 不超过 64 才拷贝。但 off 和 len 都是 32 位无符号整数，加法是模 的。

攻击者可以取：

计算一下：

，检查通过。但 buf + off 指向的是缓冲区外大约 4GB 的位置，memcpy 会往一个完全无关的地址写 32 字节。这是一个典型的整数溢出导致的任意地址写。

用位向量理论来问：

(set-logic QF_BV)
(declare-const off (_ BitVec 32))
(declare-const len (_ BitVec 32))
(assert (bvule (bvadd off len) (_ bv64 32)))
(assert (bvugt off (_ bv64 32)))
(assert (bvule len (_ bv64 32)))
(check-sat)
(get-model)

求解器返回 sat，模型可能是：

off = #xfffffff0
len = #x00000020

漏洞可达。

如果换一种建模，把 off 和 len 当成数学整数：

这个公式是 unsat，因为 直接和第一条矛盾。工具会得出结论「没有漏洞」，而实际上漏洞就在那里。

同一个程序，两种理论，两个相反的答案。 这就是为什么漏洞检测工具必须精确建模目标语言的整数语义：C 的 unsigned int 是模运算，不是数学整数。

5.4 空指针

静态分析经常报「可能的空指针解引用」。这类告警里有很多是误报，SMT 可以用来过滤。

intread_flag(struct node *p) {
    if (p == NULL) return0;
    return p->flag;     // 静态分析：p 可能为空？
}

工具在 p->flag 处收集路径条件。走到这一行，必然经过了 p == NULL 为假的分支，所以路径条件里包含：

静态分析如果只做局部启发式，可能会说「p 可能是空指针」。这时问 SMT：

这是明显的矛盾，返回 unsat，告警被排除。

反过来，如果代码是：

intread_flag(struct node *p) {
    if (p->flag == 1) {   // 这里没有检查 preturn1;
    }
    return0;
}

路径条件里没有 ，查询：

返回 sat，模型给出 p = NULL。这是一条真实可达的空指针路径，告警保留。

这个用法体现了一个重要原则：SMT 不负责发现漏洞，它负责判断「这条路径到底可不可能」。发现可疑点靠前端分析，排除误报靠 SMT。

5.5 数组越界

intget(int *a, int i) {
    if (i < 100) {
        return a[i];     // i 可能为负
    }
    return-1;
}

只检查了上界，没检查下界。问 SMT：

返回 sat，例如 i = -1。a[-1] 是一次越界读。

如果加上下界检查：

if (i >= 0 && i < 100) {
    return a[i];
}

约束变成：

返回 unsat，越界路径被排除。

这个例子还可以扩展成带数组理论的版本。比如要验证「下标不同时，写入 a[j] 不会影响对 a[i] 的读取」，可以把「影响了」写成公式，再问它是否可满足：

数组理论会展开 read-over-write 公理，算术理论会处理 ，两个理论协作给出 unsat——也就是说，「写入影响了另一个下标」的情况不可能发生。这正是 3.3 节里理论组合的实际用武之地。

5.6 完整流程

把上面的步骤串起来，一个典型的漏洞检测流程是这样的：

整个系统里，SMT 只负责中间那个方框。前面「怎么把程序变成公式」是符号执行引擎的事，后面「怎么确认漏洞」是测试和人工的事。公式建得对不对，直接决定 SMT 的结论有没有意义。

所以，SMT 在漏洞检测里的正确定位是：一个强大但需要被正确使用的判定引擎。它能把「这条路径可不可能」回答得很准，但「该问哪些问题」「怎么把程序翻译成问题」，仍然依赖前端工具和工程师的判断。

六、小结

回到开头那道小学题。SMT 的价值，不是把 算得更快，而是让机器在保留「整数」「数组」「位向量」这些概念的前提下，仍然能自动地回答「有没有解」。

SMT = SAT + 背景理论。 布尔层负责组合，理论层负责语义，两者通过「原子真值」这一层接口通信。 它的核心取舍是用表达力换可判定性。 把主战场放在无量词的可判定片段，换来一个在片段内保证终止、且能处理工业规模混合约束的自动判定过程。