Symbolic Execution：把输入变成未知数，程序能自己找出崩溃条件吗？

测试一个程序时，最常见的做法是准备若干具体输入：空字符串、很长的字符串、正常账号和异常账号。Symbolic Execution 则把输入当成未知变量，让程序沿着不同分支运行，并把每条路径上的条件记录成约束。这样，工具不仅能告诉你“这里可能出错”，还可能给出一组触发错误的输入条件。

具体输入和符号输入

考虑一个简单函数：当 x > 10 时访问数组的第一个位置，否则访问第二个位置。用具体输入运行，只能走其中一条路。用符号变量 x 运行，执行器会分成两条路径，并分别记录 x > 10 与 x <= 10。

如果后续代码又要求 x 必须小于 0，某条路径的条件就可能变成矛盾；如果访问下标要求 x 在数组范围之外，约束求解器便可能构造出一个能触发越界的具体数字。

符号执行最大的困难是路径爆炸。一个程序里有很多 if、循环和递归，路径数量可能呈指数增长。实际工具会采用边界限制、路径合并、状态缓存、随机搜索和优先级策略，把资源集中在更可能发现问题的路径上。

符号值本身也有边界。字符串、系统调用、浮点数和外部服务很难完全用简单数学表达。工具往往需要模型化这些环境，或者在符号分析和具体执行之间切换。

符号执行常用于发现崩溃、越界、整数溢出和某些安全漏洞。对 AI 生成代码，它可以成为测试之外的一层检查：不是只问“这几个样例通过了吗”，而是询问“在什么条件下，这段代码会走到危险路径”。

但它不是万能证明器。工具覆盖的路径受到时间、内存、模型精度和程序结构限制。一个没有被发现的 bug，不代表所有输入都安全；一个被发现的路径，也还需要工程师判断是否能在真实环境中复现。

Symbolic Execution 的直觉很简单：把“输入一个数字”变成“输入满足某些条件的任意数字”，让程序自己暴露路径约束。它把测试从样例驱动，推进到条件驱动。