64 lines
2.9 KiB
Markdown
64 lines
2.9 KiB
Markdown
### 符号执行是如何做约束求解的
|
||
|
||
**1. 什么是约束求解**
|
||
|
||
一个约束求解器（也叫 SMT Solver，Satisfiability Modulo Theories Solver）是符号执行的“大脑”。它的工作是解决一个公式（或一组公式）是否可满足
|
||
|
||
例如，对于一个简单的程序：
|
||
|
||
```c
|
||
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 的“理论”部分是它的核心能力。它能够理解并处理不同领域（如整数、数组、位向量等）的约束。例如：
|
||
|
||
- **算术理论（Arithmetic Theory）**：处理 `+`, `-`, `*`, `>` 等数学运算
|
||
- **位向量理论（Bitvector Theory）**：处理二进制位运算，如 `&`, `|`, `^`, `<<` 等。这对于分析底层二进制代码至关重要
|
||
- **数组理论（Array Theory）**：处理数组的读写操作
|
||
|
||
当一个约束公式涉及到多个理论时，SMT Solver 会使用一种叫 **CDCL(T)**（Conflict-Driven Clause Learning with Theories）的算法，协调各个理论求解器来解决问题。
|
||
|
||
**c. 变量赋值与回溯**
|
||
|
||
求解器会尝试给变量赋值，并检查这些赋值是否满足约束
|
||
|
||
- **如果满足**：它会继续给其他未赋值的变量赋值，直到找到一个完整的解
|
||
- **如果不满足**：它会回溯（backtrack），撤销之前的赋值，并尝试新的组合
|
||
|
||
这个过程很像解决数独，每一步的赋值都会影响后续的选择，而当发现无解时，就需要退回到上一步重新选择
|
||
|
||
**3. 符号执行与约束求解的结合**
|
||
|
||
符号执行器和约束求解器是紧密配合的
|
||
|
||
1. **符号执行器**：
|
||
- 遍历程序代码，将变量抽象为符号
|
||
- 遇到分支（`if`, `while`）时，为每个分支生成一个**路径约束**
|
||
- 将路径约束传递给约束求解器
|
||
2. **约束求解器**：
|
||
- 接收路径约束
|
||
- 尝试找到满足约束的一组具体值
|
||
- 如果找到了解，就将解返回给符号执行器
|
||
3. **符号执行器**：
|
||
- 使用求解器返回的具体值作为输入，来探索新的代码路径
|
||
- 如果求解器返回“无解”（unsatisfiable），则说明该代码路径不可达 |