將IR轉換爲Z3公式？

Question

我在IR中有一些代碼，並且此代碼已經以SSA形式出現。 現在我試圖將此代碼轉換爲SMT公式，然後將其提供給Z3以進行一些驗證。我有一些問題：

1. 是否有任何技術文件詳細說明如何將SSA IR轉換爲SMT公式？我四處搜尋，無濟於事。

2. 對於那些計算指令，轉換爲Z3公式沒有太多問題。但是，我仍然在無條件的和有條件的分支指令中掙扎。有關如何將這些指令轉換爲Z3公式的建議？

非常感謝！

Answer 1

我認爲這是公平的兩大類來劃分基於SMT程序驗證工具：

• 模糊器和錯誤發現者。這些工具從本質上將程序的一個執行路徑編碼爲SMT公式。這些工具使用SMT來檢查特定的執行路徑是否可行。示例或此類工具是：Pex,EXE，Sage。根據您的問題，您似乎已經知道如何將一條路徑編碼爲SMT。

• 擴展靜態跳棋和驗證編譯器。這些工具通常會將程序減少到中間形式。然後，生成幾個驗證條件（VC）併發送到SMT解算器。他們中的大多數（都是？）嘗試進行模塊化驗證，因爲驗證整個程序作爲單個SMT問題太昂貴。 Boogie-PL是一種非常流行的中間格式。如果將IR映射到Boogie-PL，則可以使用Boogie以SMT格式生成VC。文章「Weakest-Precondition of Unstructured Programs」描述了Boogie-PL如何編碼爲公式。請注意，Boogie是開源的，代碼非常易讀。所以，你也可以瀏覽代碼來澄清細節。 Rustan Leino也有一堆幻燈片，說明如何將Boogie VC編碼成公式。其他相關項目有ESC/Java 2,Why3,VeriFast。

編輯（處理循環）：用於處理循環只展現他們的給定次數最簡單的技術。當我們這樣做時，我們的驗證工具變成了一個「bug發現者」，因爲我們基本上放棄了分析所有可能的路徑。在工具（如ESC/Java，Why3，VeriFast）中，使用loop invariants。 Rustan關於循環不變式有一個不錯的video and lectures notes。循環不變量可以由用戶提供，或自動計算。關於「循環不變綜合」的論文很多。

循環不變例子：函數duplet在這個Why3 verification example。

另一種可能性是將您的IR編碼爲muZ。 muZ是Z3中的固定點引擎。 在這種方法中，循環可以直接編碼（請參閱muZ頁面上的文章），並且不需要提供循環不變量。然而，像muZ這樣的引擎作爲最先進的SMT解算器還不成熟。