用于位向量算术的SMT解算器

Question

我正在计划一些使用现成SMT解算器进行符号执行C代码的实验，并且想知道使用哪种求解器;看着如SMT比赛的参赛者只考虑开源系统，将其缩小到海狸，Boolector，CVC3，OpenSMT，Sateen，Sonolar，STP，Verit;这仍然是一个长长的名单。

试图一点点进一步缩小范围，我注意到，一些系统做广告来处理位向量的运算能力，而其他人只能做广告来处理一般的整数运算的能力。原则上，前者对于C是正确的，其中变量是机器字，而不是无限整数。它在实践中有多大的差异？如果你尝试为这种工作使用一个整数系统会发生什么？以下情况之一是否适用？

1. 位矢量系统会更有效，但你可以使用，没有问题。

2. 可以使用一般整数系统一些调整。

3. 一般整数系统是罚款符号int（因为溢出的结果是不确定的），但将提供无符号错误的答案。

4. 一般整数系统只是不适合机器字算术正确的，我可以在我的短名单减少到只有那些提供位向量的运算系统。

5. 别的东西......？

我试图问一个具体的问题尽可能，但如果任何人都可以建议任何其他标准缩小名单，那将是伟大的！

Answer 1

我已经有了使用STP进行符号执行的良好经验。 STP的设计正是为了这项任务。此外，还有一些符号执行工具已经成功地将STP用于此目的，所以有理由相信STP不会吸引。我肯定会向其他人推荐STP作为这种实验的默认选择。

不过，我还没有尝试过其他的系统，所以我不知道STP如何比较他们。

就个人而言，我认为STP作为基准，并为这种应用程序的默认选择。所以，如果你只有时间去尝试一个解算器，试试STP看起来是一个非常合理的选择。

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

P.S. Z3也可能成为您添加到列表中考虑的竞争者。 （你真的需要你的解算器是开源的，只要它是免费的？我希望一个象征性的执行工具将它仅用作黑盒，而不需要修改。）

Answer 2

据SMT-Wikipedia在2011-08，我们有：

根据这些措施，似乎最有活力，精心组织项目OpenSMT，STP和CVC4。

我只是检查这个东西 - 到目前为止，所有三个似乎是合理的，再加上较旧的CVC - > CVC3。