符号执行和 SAT 求解器有什么区别？

Question

我的理解是，符号执行仅处理特定路径和不良模式，而 SAT 求解器或一般的可满足性模理论则提供对程序更可靠的分析。

有人可以验证上面的陈述并（简要地）解释这两种形式验证方法之间的差异吗？

Answer 1

长话短说： 它们的基本输入和输出有所不同。SAT 和 SMT 求解器不知道程序是什么；它们是回答有关数学公式是或否问题的工具。另一方面，符号执行是一种分析程序的方法。符号执行通常依赖于 SAT 和 SMT 求解器，但反之则不然。

---

SAT 和 SMT 求解器 与程序没有直接关系。相反，SAT 或 SMT 求解器将数学描述的“公式”作为输入，并粗略地回答该公式的真假。（通常允许第三种选择， 未知, ，适用于求解器无法找出答案的情况。）

例如，SAT 求解器的可能输入是 (a and not b) or (not a and c). 。也就是说，它是一个数学公式，其中 a, b, ， 和 c 这里是布尔（0 或 1）常量。SAT 求解器应该通过选择以下值来决定公式是否可能为真： a, b, ， 和 c. 。SMT 求解器类似，但是 a, b, ， 和 c 将被使用整数、字符串、函数等的更复杂的公式取代，例如 x + 3 = y^2.

---

符号执行 是运行程序的一种奇特方式，但不是程序的预期运行方式。相反，该程序使用所谓的“符号”值运行，这些值有点像占位符。举例说明这意味着什么，假设我有一个类似的函数 f(x) = if x > 0 then 1 else 0. 。现在，通常情况下，我会通过输入以下内容来运行程序： 3, ，并得到 f(3) = 1, ， 自从 3 大于 0. 。通过符号执行，我通过输入占位符变量来运行程序， input, ，我评估该程序以获得两种情况：任何一个 input > 0 and answer = 1 或者 input <= 0 and answer = 0. 。这可能看起来没什么用，但它最终成为分析程序的强大方法。

---

两者之间的联系 问题是符号执行在执行过程中通常依赖于 SMT 求解器，以确定某个路径是否实际上可行，或者是否应该被丢弃。例如，SMT 求解器可用于确定是否 input <= 0 and answer = 0 是可能的（答案是肯定的，例如如果 input = 0）。这样，SMT 就成为了使符号执行变得可行的“驱动力”。