verification - 用于位向量算术的 SMT 求解器

Question

我正在计划使用现成的 SMT 求解器对 C 代码的符号执行进行一些实验，并且想知道使用哪个求解器；看着例如SMT 竞赛参赛者只选择开源系统，将范围缩小到 Beaver、Boolector、CVC3、OpenSMT、Sateen、Sonolar、STP、Verit；这仍然是一个很长的 list 。

试图进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统仅宣传处理一般整数算术的能力。原则上，前者对于 C 来说是正确的，其中变量是机器字，而不是无界整数。它在实践中有多大区别？如果您尝试使用通用整数系统来完成此类工作，会发生什么？以下场景之一是否适用？

1. 位向量系统的效率稍高，但您可以使用其中任何一个，没有问题。

2. 您可以使用通用整数系统并进行一些调整。

3. 一般的整数系统对于signed int 是没问题的(因为溢出的结果是未定义的)，但对于unsigned 则会给出错误的答案。

4. 一般的整数系统对于机器字算术来说是不正确的，我可以将我的简短列表减少到仅提供位向量算术的系统。

5. 还有别的事吗...？

我试图提出尽可能具体的问题，但如果有人可以提出任何其他标准来缩小列表范围，那就太好了!

Answer 1

我在使用 STP 进行符号执行方面拥有丰富的经验。 STP 正是为此任务而设计的。此外，已经有许多符号执行工具成功地使用 STP 来实现此目的，因此有理由相信 STP 并不糟糕。我肯定会向其他人推荐 STP 作为此类实验的默认选择。

但是，我没有尝试过其他系统，所以我不知道 STP 与它们相比如何。

就我个人而言，我将 STP 视为此类应用程序的基准和默认选择。因此，如果您只有时间尝试一种求解器，那么尝试 STP 似乎是一个相当合理的选择。

如果我不得不猜测，我的猜测是支持位向量算术很重要，因为任何大型系统代码都会有大量执行按位运算的代码。另外，我怀疑/担心某些系统代码可能依赖于无符号算术的行为来包装模 2ⁿ，如果您尝试用整数对其进行建模，您将无法获得 C 的语义是的(因为，正如您所说，整数对于机器字算术来说是不正确的)，因此，如果您尝试使用仅整数求解器，您可能会遇到一些困难。然而，我没有确凿的证据来证明这些怀疑。

附注Z3 也可能是一个值得添加到您的考虑列表中的竞争者。 (你真的需要你的解算器是开源的吗？只要它是免费的？我希望符号执行工具只会将它用作黑盒，而不进行修改。)