6

既成のSMTソルバーを使用して、Cコードのシンボリック実行でいくつかの実験を計画しており、どのソルバーを使用するかを考えています。たとえば、SMTコンテストの参加者を見て、オープンソースシステムのみを取り上げ、ビーバー、ブーレクター、CVC3、OpenSMT、サテン、ソノラー、STP、ベリットに絞り込みます。これはまだ長いリストです。

もう少し絞り込んでみると、一部のシステムはビットベクトル演算を処理する機能をアドバタイズしているのに対し、他のシステムは一般的な整数演算を処理する機能のみをアドバタイズしていることに気付きました。原則として、前者はCに対して正しいです。ここで、変数はマシンワードであり、無制限の整数ではありません。実際にはどのくらいの違いがありますか？この種の仕事に一般的な整数システムを使おうとするとどうなりますか？次のシナリオのいずれかが当てはまりますか？

  1. ビットベクトルシステムの方が少し効率的ですが、どちらでも問題ありません。

  2. 少し調整を加えた一般的な整数システムを使用できます。

  3. 一般的な整数システムはsignedintには問題ありませんが（オーバーフローの結果が未定義であるため）、unsignedには間違った答えが返されます。

  4. 一般的な整数システムは、マシンワード演算には正しくありません。短いリストを、ビットベクトル演算を提供するシステムのみに減らすことができます。

  5. 他に…？

私はできるだけ具体的な質問をしようとしましたが、誰かがリストを絞り込むための他の基準を提案できるなら、それは素晴らしいことです！

4

2 に答える 2

7

シンボリック実行に STP を使用した経験は豊富です。STP はまさにこのタスクのために設計されました。また、この目的で STP を使用して成功したシンボリック実行ツールが多数あるため、STP は悪くないと信じる理由があります。この種の実験のデフォルトの選択肢として、STP を他の人に絶対にお勧めします。

ただし、他のシステムを試したことがないので、STP がそれらとどのように比較されるかはわかりません。

個人的には、STP はこの種のアプリケーションのベースラインであり、デフォルトの選択肢であると考えています。そのため、ソルバーを 1 つしか試す時間がない場合は、STP を試すのが妥当な選択のように思えます。

推測する必要がある場合は、ビットベクトル演算をサポートすることが重要であると推測します。大規模なシステム コードには、ビット単位の演算を実行する重要な量のコードが含まれるからです。また、一部のシステムコードは、モジュロ 2 nをラップするために符号なし算術演算の動作に依存している可能性があるのではないかと疑ったり心配したりします。整数でモデル化しようとすると、C のセマンティクスが正しく得られません (なぜなら、あなたが言うように、整数は機械語演算には正しくありません)、したがって、整数のみのソルバーを使用しようとすると、いくつかの問題が発生する可能性があります。しかし、私はこれらの疑惑のいずれについても確固たる証拠を持っていません。

PS Z3 も、検討リストに追加する候補になる可能性があります。(ソルバーが無料である限り、本当にオープンソースである必要がありますか?シンボリック実行ツールは、変更なしでブラックボックスとしてのみ使用することを期待しています。)

于 2011-06-30T06:35:25.253 に答える
2

2011 年 8 月の SMT-Wikipediaによると、次のようになっています。

これらの測定に基づくと、最も活気があり、よく組織されたプロジェクトは、OpenSMT、STP、および CVC4 であると思われます。

私はちょうどこれをチェックしています - これまでのところ、3つすべてが合理的で、さらに古いCVC -> CVC3.

于 2011-09-01T18:44:47.197 に答える