符号执行基础：什么是符号值、符号状态、路径约束？
好，咱们正式开始聊符号执行的核心概念。
说实话，我第一次接触符号执行的时候，也被一堆术语搞得有点懵。什么符号值、符号状态、路径约束……听着像哲学概念。但你别怕，这些东西说白了，就是把程序里的变量从「具体数值」变成「数学表达式」。就这么简单。
我习惯用一个比喻来理解：具体执行就像你亲自走一条路，符号执行就像你拿着地图看所有可能的路。嗯，咱们一个一个拆开讲。
符号值：从数字到公式
先说说符号值。
普通程序里，变量存的是具体数字。比如 int x = 5;，x 就是 5。但在符号执行里，我们不赋值，而是给 x 一个「符号」——比如叫 α。这个 α 代表「任意可能的整数」。
你想想看，这有什么好处？
好处大了去了。当程序往下跑的时候，x 参与运算，结果就不再是一个数，而是一个表达式。比如：
int x = symbolic(); // x = α
int y = x + 10; // y = α + 10
int z = y * 2; // z = 2 * (α + 10) = 2α + 20
看到了吗？y 和 z 都变成了关于 α 的表达式。这就是符号值——用符号代替具体数值，用表达式记录计算过程。
关键点：符号值不是「一个值」，而是一组可能值的数学表示。它保留了变量之间的依赖关系。
我在项目中遇到过一个问题：用具体值测试时，某个 bug 死活复现不了。后来换成符号执行，发现是因为输入值必须满足 a > 100 && b < 50 这个条件才会触发。具体测试时我随便填的 a=10, b=20，当然碰不上。符号值帮我找到了这个隐藏的「触发条件」。
符号状态：程序的快照
好，符号值说完了。那符号状态是什么？
说白了，符号状态就是程序在某个时刻的「内存快照」——只不过这个快照里存的不是具体数字，而是符号表达式。
举个例子。假设程序执行到某一行，当前有变量 x、y、z。符号状态就是一张表：
| 变量 | 符号值 |
|---|---|
| x | α |
| y | α + 10 |
| z | 2α + 20 |
这就是一个符号状态。它记录了每个变量当前「等于什么表达式」。
但符号状态不止包含变量映射。它还包含一个重要的东西——路径约束。嗯，这就是咱们下一个要聊的概念。
我的习惯：调试符号执行引擎时，我经常把符号状态打印出来看。如果某个变量的表达式长得离谱（比如嵌套了十几层 if-else），那基本可以断定路径爆炸了。这时候就得考虑优化策略。
路径约束：走过的路
路径约束，是符号执行里最核心、也最容易出问题的地方。
你想想看，程序里有分支语句——if、else、switch。每遇到一个分支，程序就可能走两条不同的路。符号执行不像具体执行那样只选一条，它两条路都走。
但问题来了：走不同的路，需要满足不同的条件。比如：
if (x > 0) {
// 路径 A：需要 x > 0
} else {
// 路径 B：需要 x <= 0
}
路径约束，就是记录「要走到当前这个位置，必须满足哪些条件」。
假设 x 是符号值 α。那么：
- 走到路径 A 的约束是：
α > 0 - 走到路径 B 的约束是：
α <= 0
随着程序继续执行，路径约束会不断累积。比如再遇到一个 if (y < 100)，约束就变成：
- 路径 A-1：
α > 0 && (α + 10) < 100 - 路径 A-2：
α > 0 && (α + 10) >= 100
这就是路径约束——一组关于符号值的条件表达式，描述了到达当前程序点所经过的所有分支判断。
我曾经踩过的坑：路径约束里如果出现浮点数比较，千万别直接扔给求解器。浮点运算不满足结合律，求解器算出来的结果可能和实际执行不一致。我因为这个浪费了整整两天。后来学乖了，遇到浮点分支直接走具体执行，不做符号化。
三者如何协同工作？
好，三个概念都讲完了。它们怎么配合？
我画个简单的流程：
- 初始化：把输入变量设为符号值（比如 α、β、γ）
- 模拟执行：逐条执行指令，遇到赋值就更新符号状态中的表达式
- 遇到分支：把分支条件加到路径约束里，然后分叉——每个分支维护自己的符号状态和路径约束
- 遇到目标（比如 assert 失败、崩溃点）：把当前的路径约束交给约束求解器，看有没有解
- 有解：生成测试用例，复现 bug
说白了，符号值负责「表示」，符号状态负责「记录」，路径约束负责「限制」。三者缺一不可。
一句话总结：符号执行 = 符号值 + 符号状态 + 路径约束 + 约束求解器。前三个是数据结构，求解器是引擎。
一个完整的例子
咱们看个实际点的代码。假设有这么一个函数：
void check(int x, int y) {
int z = x + y;
if (z > 100) {
if (x < 50) {
// 目标位置：这里可能有问题
abort(); // 崩溃
}
}
}
用符号执行分析：
| 步骤 | 符号状态 | 路径约束 |
|---|---|---|
| 初始 | x=α, y=β | true |
| z = x + y | x=α, y=β, z=α+β | true |
| 遇到 if(z>100) | 同上 | 分叉： 路径1: α+β > 100 路径2: α+β <= 100 |
| 路径1继续，遇到 if(x<50) | 同上 | 分叉： 路径1-1: α+β>100 && α<50 路径1-2: α+β>100 && α>=50 |
| 路径1-1到达 abort() | 同上 | α+β>100 && α<50 |
最后，把路径约束 α+β>100 && α<50 扔给求解器。求解器会返回一组值，比如 α=30, β=80。这就是一个能触发崩溃的测试用例。
一个小技巧：实际做漏洞挖掘时，我通常不会只满足于「能触发崩溃」。我会在路径约束上加一些额外条件——比如让 α 尽量小、β 尽量大。这样生成的测试用例更「极端」，更容易暴露边界问题。
需要注意的坑
嗯，最后聊几个实际中容易踩的坑。
第一个：路径爆炸。每遇到一个 if，路径数就翻倍。循环里套 if？那路径数是指数级增长。我见过一个只有 50 行的函数，符号执行跑了 3 个小时还没完。解决办法？后面章节会讲——剪枝、合并、启发式搜索。
第二个：约束求解超时。路径约束里如果有非线性运算（乘法、除法、取模），求解器可能算不出来。我习惯的做法是：给求解器设个超时时间，比如 5 秒。超时了就放弃这条路径，或者回退到具体执行。
第三个：外部函数调用。如果程序调用了库函数（比如 strlen、memcpy），符号执行引擎不知道内部实现，就没法生成符号表达式。这时候需要手动建模——给这些函数写「符号化版本」。嗯，这部分内容后面会专门讲。
好了，符号值、符号状态、路径约束这三个基础概念，咱们就聊到这儿。下节课我会讲约束求解器——那个能把路径约束变成测试用例的「黑魔法」工具。