C程序是否有靜態不變量發現工具？

Question

我正在尋找一種可以靜態發現C程序中不變量的工具。我檢出了Daikon，但它只是動態地發現不變量。

有什麼工具可用於我正在尋找的？謝謝！

Answer 1

如果您的意思是最廣義的「不變」，就像Daikon的鏈接頁面所使用的那樣，那麼許多靜態分析工具的工作可以被描述爲「發現不變量」，也許不是您正在尋找的表情不變量對於。

Frama-C的價值分析爲每個陳述積累了其結果，所有變量的可能值。在分析結束時，它可以在每個語句中呈現關於程序中每個變量的域變化的非關係信息。在this screenshot中，對於該確定性程序的所有執行，不變是在選定指令之前S總是0,1,3或6。

你的問題中的兩個隱藏參數是你感興趣的不變量的形狀，以及你想要找到這些不變量的程序的形狀。例如，在Ira的回答中提到的SLAM被設計用於處理設備驅動程序代碼，並推斷只包含驗證正確使用系統API的必要信息的不變量。另一個工具，Astrée，在推斷正確的不變量以演示飛行控制軟件的運行時安全方面做得非常出色。

兩個自由度使得設計空間非常大。你不會找到任何適用於各種C程序的東西，並推斷出你可能感興趣的所有不變量，但如果你針對特定的應用領域和各種不變式細化你的問題，你將有更好的機會找到相關的答案。

Answer 2

參見The SLAM project: debugging system software via static analysis。它聲稱以靜態方式推斷不變量，正如你所要求的C語言一樣。作者Tom Ball因其在程序分析方面的傑出工作而廣爲人知。