用於位向量算術的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。