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

Question

我正在计划一些C代码的符号执行实验,使用现成的SMT求解器,并想知道使用哪个求解器; 看看例如SMT比赛参赛者,并且仅采用开源系统,将其缩小到Beaver,Boolector,CVC3,OpenSMT,Sateen,Sonolar,STP,Verit; 这仍然是一个很长的名单.

为了进一步缩小范围,我注意到一些系统宣传处理位向量算术的能力,而其他系统只宣传处理一般整数算术的能力.原则上,前者对于C是正确的,其中变量是机器词,而不是无界的整数.它在实践中有多大差异？如果您尝试使用通用整数系统进行此类工作会发生什么？是否适用以下方案之一？

1. 有点矢量系统效率稍高,但你可以使用其中任何一个,没问题.

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

3. 一般的整数系统适用于signed int(因为溢出的结果是未定义的)但是会给出unsigned的错误答案.

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

5. 别的......？

我试图尽可能地问一个问题,但是如果有人可以建议缩小列表的任何其他标准,那就太棒了!

Answer 1

我在使用STP进行符号执行方面有很好的经验.STP专为此任务而设计.此外,有许多符号执行工具已成功使用STP用于此目的,因此有理由相信STP不会吮吸.我肯定会向其他人推荐STP作为此类实验的默认选择.

但是,我还没有尝试过其他系统,所以我不知道STP与它们的比较.

就个人而言,我将STP视为此类应用程序的基线和默认选择.所以,如果你只有时间尝试一个求解器,尝试STP似乎是一个非常合理的选择.

如果我不得不猜测,我的猜测是位向量算法对于支持是很重要的,因为任何大型系统代码都将具有执行按位运算的非常少量的代码.另外,我怀疑/担心一些系统代码可能依赖于无符号算术的行为来包装modulo 2 ⁿ,如果你尝试用整数建模它,你就不会得到C语义(因为,​​正如你所说的那样) ,整数只是机器字算法不正确)因此,如果你尝试使用仅整数求解器,你可能会遇到一些困难.但是,我没有任何证据证明这些怀疑.

PS Z3也可能是添加到列表中的竞争者.(你真的需要你的求解器是开源的,只要它是免费的吗？我希望一个符号执行工具只能将它用作黑盒子而不做修改.)