1. 什么是约束求解

一个约束求解器（也叫 SMT Solver，Satisfiability Modulo Theories Solver）是符号执行的“大脑”。它的工作是解决一个公式（或一组公式）是否可满足

例如，对于一个简单的程序：

int main(int x, int y) {
    if (x + y > 10) {
        printf("Branch 1");
    } else {
        printf("Branch 2");
    }
}

符号执行会将 x 和 y 变成符号 X 和 Y。如果要探索 Branch 1，它就会生成约束：X + Y > 10

约束求解器接收这个约束，然后找到满足这个条件的具体值。一个可能的解是 X=5，Y=6。符号执行器就可以用 x=5, y=6 作为输入，来验证 Branch 1 是否可达

2. 约束求解的内部工作原理

约束求解器本身是基于一套复杂的算法来工作的，主要包括：

a. 逻辑分解

求解器首先会分析给定的约束公式，将其分解为更小的、可管理的子问题。例如，一个复杂的逻辑表达式 (A && B) || C 会被分解成两个独立的子问题：A && B 和 C

b. 理论推理

SMT Solver 的“理论”部分是它的核心能力。它能够理解并处理不同领域（如整数、数组、位向量等）的约束。例如：

当一个约束公式涉及到多个理论时，SMT Solver 会使用一种叫 CDCL(T)（Conflict-Driven Clause Learning with Theories）的算法，协调各个理论求解器来解决问题。

c. 变量赋值与回溯

求解器会尝试给变量赋值，并检查这些赋值是否满足约束

这个过程很像解决数独，每一步的赋值都会影响后续的选择，而当发现无解时，就需要退回到上一步重新选择

3. 符号执行与约束求解的结合

符号执行器和约束求解器是紧密配合的

符号执行器：
- 遍历程序代码，将变量抽象为符号
- 遇到分支（if, while）时，为每个分支生成一个路径约束
- 将路径约束传递给约束求解器
约束求解器：
- 接收路径约束
- 尝试找到满足约束的一组具体值
- 如果找到了解，就将解返回给符号执行器
符号执行器：
- 使用求解器返回的具体值作为输入，来探索新的代码路径
- 如果求解器返回“无解”（unsatisfiable），则说明该代码路径不可达

28.19 符号执行是如何做约束求解的

results matching ""