可以使用LLVM字節碼作爲Z3輸入嗎？

我有一個LLVM字節碼的描述，我需要通過Z3輸入。如果可以完成，它是如何完成的？如果沒有，是否有任何工具可以做到這一點？可以使用LLVM字節碼作爲Z3輸入嗎？

2014-02-11 user2084755

LLVM IR描述程序性程序。 Z3證明了定理。這兩件事顯然不是同構的，所以你必須提供一些關於你想要做什麼的更多細節。你是否試圖證明某個程序（在LLVM IR中給出）？你是否試圖在LLVM IR中編碼一個定理/證明？ – delnan

我有一個LLVM字節碼中需要在Z3中證明的程序的一部分。 – user2084755

您可能正在使用我並不熟悉的Z3術語，但我會走出一條腿並聲稱沒有意義：程序不是一個定理。你想證明有關該計劃的某些財產/聲明嗎？如果是這樣，哪一個？ – delnan

這個問題並不完全合適或清晰，但也許可以查看SMACK工具（https://github.com/smackers/smack/wiki），它使用LLVM的clang編譯C程序（使用聲明）並使用Boogie的中間表示（https://boogie.codeplex.com/），以便查詢Z3關於程序中的斷言。

如果這並不直接滿足您的需求，則可以使用源代碼，以便您瞭解它如何將斷言和LLVM位代碼文件轉換爲Boogie的中間表示形式。

來源

2014-02-12 04:55:57 Taylor

兩個工具可從C代碼翻譯爲形式Z3可以處理：

1）SMACK（https://github.com/smackers/smack）

這轉化註釋C代碼布吉語言，使用LLVM位碼作爲中間表示。然後可以使用Boogie工具（http://boogie.codeplex.com）生成可通過Z3檢查的驗證條件。但是，手動註釋代碼可能是一項艱鉅的任務。特別是，您必須爲所有循環和C函數的前/後條件編寫足夠的歸納不變式，以證明您的程序符合其規範。

2）UFO（https://bitbucket.org/arieg/ufo/wiki/Home）

此工具可以選自C平移通過LLVM位碼的方式來SMT-LIB喇叭的邏輯，一次。結果可以通過Z3的一個定點引擎進行檢查。在這種方法中，您不必手動註釋循環和過程（因爲Z3自己發現了這些註釋），但該工具的容量遠遠不夠。

來源

2014-02-12 18:18:52 user1214978

PAGAI對LLVM位碼執行靜態分析。它會自動計算循環不變量並檢查某些失敗條件（如UFO）的可達性;你可以使用斷言和假設。它在內部做的一件事是將LLVM位代碼中的無循環程序轉換爲表示其語義的SMT公式。

來源

2014-03-01 11:14:37

可以使用LLVM字節碼作爲Z3輸入嗎？

回答

相關問題