abstract-interpretation

6 posts

abstract-interpretationllmstatic-analysisfalse-positives

LLM可以為你的靜態分析警告排序。只是無法解釋原因。

大語言模型可以幫助分流靜態分析中的誤報，但它們無法像抽象詮釋那樣理解程式語義。以下是如何將兩者結合。

你的靜態分析器剛剛在一個週五下午發出了847條警告。從統計上看，其中大約5%到15%是真正的缺陷。其餘都是誤報：生成程式碼中的無效儲存、對工具來說可疑但對人類來說顯而易見的空值檢查、無關緊要的雜湊函式中的整數溢位。 手動逐一排查令人心力交瘁。於是你想：能不能直接問LLM哪些是真的？…
abstract-interpretationstatic-analysismetainfer

Meta用從不執行程式的靜態分析器在投產程式碼中發現了10萬個缺陷

Meta的Infer利用抽象詮釋和雙向推理，透過推理程式碼結構而非執行來發現空指標解引用、記憶體洩漏和競態條件。以下是它的運作原理以及如何在您自己的程式碼庫中使用它。

Meta已經發布了超過10萬個由靜態分析器在程式碼到達使用者之前捕獲的缺陷修復。這個工具名為Infer，它是開源的，並且不會執行您的程式碼。它讀取程式碼，建構程式碼可能執行的數學模型，並證明某些壞事不可能發生。或者它會找到一條可能發生的路徑。…
abstract-interpretationstatic-analysissafety-criticalaviation

靜態分析無法證明你的飛機不會墜毀，但它能證明更有價值的事

抽象解釋會對每一個可能的程式狀態進行過度近似。如果除零錯誤在抽象層中無法觸及，那麼在真實程式碼中也同樣無法觸及。以下是它的運作原理與局限性。

靜態分析無法證明飛機不會墜毀。但它可以證明你的高度計控制迴路絕不會發生除零、絕不會陣列索引越界，也絕不會讓定點累加器溢位。這兩者之間的區別至關重要：前者是關於物理、空氣動力學，以及鋁合金在壓力下的主張；後者則是關於你可以在飛機離地前就驗證完的程式碼。…
abstract-interpretationstatic-analysisruntime-errorsverification

如何證明你的程式沒有執行時錯誤（以及為什麼你很可能會放棄嘗試）

抽象解釋讓你在執行前就能證明執行時錯誤不可能發生。以下說明它實際上如何運作、為什麼很困難，以及它在你的工具鏈中扮演什麼角色。

你的測試套件通過了。你的型別檢查器是綠燈。你發布了。兩小時後，生產環境在某個沒人想到要測試的邊緣案例上拋出了 。 測試能找到錯誤。型別能防止一部分。但兩者都無法證明你的程式完全沒有執行時錯誤。為此，你需要更強大的東西：一種能夠同時對所有可能的執行路徑進行推理、而不需要實際執行程式的方法。…