IR のコードがあり、このコードは既に SSA 形式になっています。今、このコードを SMT フォーミュラに変換し、それを Z3 にフィードして検証しようとしています。いくつか質問があります:
SSA IR を SMT フォーミュラに変換する方法を詳細に説明しているテクニカル ペーパーはありますか? 私は周りを探しましたが、役に立ちませんでした。
これらの計算命令については、Z3 式への変換に大きな問題はありません。ただし、無条件および条件付き分岐命令にはまだ苦労しています。これらの指示を Z3 式に変換する方法について何か提案はありますか?
本当にありがとう！！！
SMT ベースのプログラム検証ツールを 2 つの主要なグループに分けるのは公平だと思います。
ファザーとバグファインダー。これらのツールは、基本的に、プログラムの 1 つの実行パスを SMT 式にエンコードします。これらのツールは、SMT を使用して、特定の実行パスが実行可能かどうかを確認します。例またはそのようなツールは次のとおりです。Pex、EXE、Sage。あなたの質問に基づいて、1 つのパスを SMT にエンコードする方法を既に知っているようです。
拡張静的チェッカーと検証コンパイラ。これらのツールは通常、プログラムを中間形式に縮小します。次に、いくつかの検証条件 (VC) が生成され、SMT ソルバーに送信されます。プログラム全体を 1 つの SMT 問題として検証するにはコストがかかりすぎるため、それらのほとんど (すべて?) はモジュール検証を試みます。Boogie-PL は非常に人気のある中間フォーマットです。IR を Boogie-PL にマッピングすると、Boogieを使用して SMT 形式で VC を生成できます。記事「構造化されていないプログラムの最も弱い前提条件」では、Boogie-PL が式にエンコードされる方法について説明しています。Boogie はオープンソースであり、コードは非常に読みやすいことに注意してください。そのため、コードを参照して詳細を明確にすることもできます。ルスタン・レイノBoogie VC を数式にエンコードする方法を説明するスライドも多数あります。その他の関連プロジェクトは、ESC/Java 2、Why3、VeriFastです。
編集(ループの処理): ループを処理するための最も簡単な手法は、指定された回数ループを展開するだけです。これを行うと、考えられるすべてのパスを分析することを基本的にあきらめるので、検証ツールは「バグ ファインダー」になります。ツール (ESC/Java、Why3、VeriFast など) では、ループ不変条件が使用されます。Rustan は、ループの不変条件に関する優れたビデオとレクチャー ノートを提供しています。ループの不変条件は、ユーザーによって提供されるか、自動的に計算されます。「ループ不変合成」に関する論文は数多くあります。
ループ不変の例:dupletこのWhy3 検証例の関数。
さらに別の可能性は、IR をmuZにエンコードすることです。muZ は、Z3 で使用できる固定小数点エンジンです。このアプローチでは、ループを直接エンコードすることができ (muZ ページの記事を参照)、ループ不変条件を提供する必要はありません。ただし、muZ のようなエンジンは、最先端の SMT ソルバーとしてはまだ成熟していません。