用于位向量算术的 SMT 求解器
我正在计划使用现成的 SMT 求解器对 C 代码的符号执行进行一些实验，并想知道使用哪个求解器；例如，查看 SMT 竞赛参赛者，并仅采用开源系统，将范围缩小到 Beaver、Boolector、CVC3、OpenSMT、Sateen、Sonolar、STP、Verit；这仍然是一个很长的清单。
试图进一步缩小范围，我注意到一些系统宣传处理位向量算术的能力，而其他系统仅宣传处理一般整数算术的能力。原则上，前者对于 C 来说是正确的，其中变量是机器字，而不是无界整数。它在实践中有多大区别？如果您尝试使用通用整数系统来完成此类工作，会发生什么？以下场景之一是否适用？
位向量系统效率稍高，但您可以使用其中任何一个，没有问题。
您可以使用通用整数系统并进行一些调整。
一般的整数系统对于signed int 是没问题的（因为溢出的结果是未定义的），但是对于unsigned 会给出错误的答案。
通用整数系统对于机器字算术来说是不正确的，我可以将我的简短列表减少到仅提供位向量算术的系统。
还有什么...？
我试图提出尽可能具体的问题，但如果有人可以提出任何其他标准来缩小列表范围，那就太好了！
I'm planning some experiments in symbolic execution of C code, using an off-the-shelf SMT solver, and wondering which solver to use; looking at e.g. the SMT contest entrants, and taking only the open-source systems, narrows it down to Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; which is still a long list.
Trying to narrow it down a little further, I notice that some of the systems advertise the ability to handle bit vector arithmetic, whereas others only advertise the ability to handle general integer arithmetic. In principle, the former is correct for C, where variables are machine words, not unbounded integers. How much difference does it make in practice? What happens if you try to use a general integer system for this kind of job? Does one of the following scenarios apply?
A bit vector system is slightly more efficient, but you can use either, no problem.
You can use a general integer system with a bit of tweaking.
A general integer system is fine for signed int (because the result of overflow is undefined) but will give the wrong answer for unsigned.
A general integer system just isn't correct for machine word arithmetic, and I can reduce my short list to only those systems that provide bit vector arithmetic.
Something else...?
I've tried to ask as specific a question as possible, but if anyone can suggest any other criteria for narrowing down the list, that would be great!
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
我在使用 STP 进行符号执行方面拥有丰富的经验。 STP 正是为此任务而设计的。此外，已经有许多符号执行工具成功地使用 STP 来实现此目的，因此有理由相信 STP 并不糟糕。我肯定会向其他人推荐 STP 作为此类实验的默认选择。
不过，我没有尝试过其他系统，所以我不知道 STP 与它们相比如何。
就我个人而言，我将 STP 视为此类应用程序的基准和默认选择。因此，如果您只有时间尝试一种求解器，那么尝试 STP 似乎是一个相当合理的选择。
如果我不得不猜测，我的猜测是支持位向量算术很重要，因为任何大型系统代码都会有大量执行按位运算的代码。另外，我怀疑/担心某些系统代码可能依赖于无符号算术的行为来包装模 2n，如果您尝试用整数对其进行建模，您将无法获得 C 的语义是的（因为，正如您所说，整数对于机器字算术来说是不正确的），因此，如果您尝试使用仅整数求解器，您可能会遇到一些困难。然而，我没有确凿的证据来证明这些怀疑。
PS Z3 也可能是一个值得添加到您的考虑列表中的竞争者。 （你真的需要你的解算器是开源的，只要它是免费的？我希望符号执行工具只会将它用作黑盒，而不进行修改。）
I've had good experience using STP for symbolic execution. STP was designed precisely for this task. Also, there have been a number of symbolic execution tools that have successfully used STP for this purpose, so there is reason to believe that STP doesn't suck. I would definitely recommend STP to others as a default choice for this sort of experimentation.
However, I haven't tried the other systems, so I don't know how STP compares to them.
Personally, I see STP as the baseline and the default choice for this kind of application. So, if you only have time to try one solver, trying STP seems like a pretty reasonable choice.
If I had to guess, my guess would be that bit-vector arithmetic is important to support, because any large systems code is going to have a non-trivial amount of code that performs bitwise operations. Also, I'd suspect/worry some systems code may rely upon the behavior of unsigned arithmetic to wrap modulo 2n, and if you try to model it with integers, you will not get the semantics of C right (because, as you say, integers just aren't correct for machine-word arithmetic) and consequently, if you try to use an integer-only solver, you may experience some difficulties. However, I have no hard evidence for either of these suspicions.
P.S. Z3 might also be a contender to add to your list to consider. (Do you really need your solver to be open-source, as long as it is free? I'd expect that a symbolic execution tool would use it only as a blackbox, without modification.)
根据 2011 年 8 月的 SMT-Wikipedia，我们有：
我只是检查这些东西 - 到目前为止，这三个似乎都是合理的，加上旧的 CVC -> CVC3。
According to SMT-Wikipedia at 2011-08, we have:
I'm just checking this stuff - so far, all three seems reasonable, plus older CVC -> CVC3.