我正在计划一些C代码的符号执行实验，使用现成的SMT求解器，并想知道使用哪个求解器;看着例如SMT比赛的参赛者，只采用开源系统，将其缩小为Beaver，Boolector，CVC3，OpenSMT，Sateen，Sonolar，STP，Verit;这仍然是一个很长的名单 .
为了进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统只宣传处理一般整数算术的能力 . 原则上，前者对于C是正确的，其中变量是机器词，而不是无界的整数 . 它在实践中有多大差异？如果您尝试使用通用整数系统进行此类工作会发生什么？是否适用以下方案之一？
-
位向量系统效率稍高，但你也可以使用，没问题 .
-
您可以使用一般整数系统进行一些调整 .
-
一般的整数系统适用于signed int（因为溢出的结果是未定义的）但是会给出unsigned的错误答案 .
-
一般整数系统对机器字算法不正确，我可以将我的短列表减少到只提供位向量算术的系统 .
-
别的......？
我试图尽可能地问一个问题，但是如果有人可以建议缩小列表的任何其他标准，那就太棒了！
2 回答
我在使用STP进行符号执行方面有很好的经验 . STP专为此任务而设计 . 此外，有许多符号执行工具已成功使用STP用于此目的，因此有理由相信STP不会吮吸 . 我肯定会向其他人推荐STP作为此类实验的默认选择 .
但是，我还没有尝试过其他系统，所以我不知道STP与它们的比较 .
就个人而言，我将STP视为此类应用程序的基线和默认选择 . 所以，如果你只有时间尝试一个求解器，尝试STP似乎是一个非常合理的选择 .
如果我不得不猜测，我的猜测是位向量算法对于支持是很重要的，因为任何大型系统代码都将具有执行按位运算的非常少量的代码 . 此外，我怀疑/担心一些系统代码可能依赖于无符号算术的行为来包装modulo 2n，如果你尝试用整数建模它，你就不会得到C语义（因为，正如你所说，整数对于机器字算法来说是不正确的，因此，如果你尝试使用仅整数求解器，你可能会遇到一些困难 . 但是，我没有任何证据证明这些怀疑 .
附： Z3也可能是添加到列表中的竞争者 . （你真的需要你的求解器是开源的，只要它是免费的吗？我希望一个符号执行工具只能将它用作黑盒子而不做修改 . ）
根据2011-08的SMT-Wikipedia，我们有：
我只是检查这些东西 - 到目前为止，所有三个似乎都合理，加上旧的CVC - > CVC3 .