可達性和符號執行

Question

現在我對符號執行（SE）和可達性分析（RA）感到困惑。據我所知，SE使用符號來執行一些代碼以分支條件到達每個分支。 RA可以用來查找每個分支的可達性，對嗎？當使用RA時，我們可以提取每個分支的分支條件。如果是這樣，他們之間有什麼區別？他們可以迅速嗎？他們都是靜態分析嗎？

感謝，夏娃

Answer 1

符號執行也不是一成不變的，它象徵性地執行程序。 對於性能的擔憂，像klee這樣的符號執行工具不會在遇到分支時解決分支條件。它使用便宜的分析來查看它是否可能可達。 它將嘗試在到達程序的退出時生成測試用例。 如果從起始點（主函數）到 出口收集到的約束條件滿足，則會給出測試用例，否則出口無法到達。 SE使用可達性分析來生成測試用例來覆蓋代碼。

Answer 2

符號執行沒有執行程序就完成了。因此它是靜態分析。

一個好的符號分析將計算每個程序點的路徑條件。一個更好的人將能夠推理路徑公式，證明它是可行的（程序點是可達的）或不（程序點是死的）。

相比於編譯的代碼執行速度，符號執行往往是相當緩慢。

Answer 3

可達性分析主要用於查看模型是否可以達到某個狀態。然而，符號執行是一種靜態分析技術（有時也是動態的，像什麼KLEE一樣）找到一個程序/源代碼，所有的路徑。