假設有兩個程序，它們都能通過你所寫的所有測試。其中一個程序是正確的。另一個程式存在除以零的錯誤，該錯誤僅在特定輸入組合同時出現時才會觸發，而你的測試永遠不會出現這種組合。傳統的測試方法無法告訴你哪個程式是正確的，哪個程式是正確的。但抽象解釋可以。
抽象解釋是一種數學框架，它賦予靜態分析工具在不執行程式的情況下推斷其所有可能行為的能力。 Facebook 的 Infer 工具能夠大規模地尋找空指標錯誤，Astrée 分析器能夠形式化地驗證空中巴士飛行控制軟體，以及所有聲稱具有健全性的靜態分析器（即保證程式透過分析後確實不存在所檢查的錯誤類型），都依賴於這種技術。理解其運作方式可以解釋為什麼有些工具能夠發現其他工具遺漏的錯誤，以及為什麼這些保證需要權衡取捨。
什麼是抽象詮釋？
抽象解釋是 Patrick Cousot 和 Radhia Cousot 於 1977 年提出的程序近似理論。其核心思想是：與其計算所有可能的程序狀態的精確集合（這通常是不可判定的），不如使用易於分析的簡化數學域來計算安全的過近似。
這裡的「抽象」並非指模糊或概念化，而是指一種具體的數學運算：將一組具體的數值抽象化成更簡單的表示形式，保留你關心的屬性，同時捨棄不必要的細節。例如，一個具體的整數值 42 在符號分析抽像中，它變成了「正」。這種抽象會失去資訊（你不再知道確切的值），但會增加可處理性（任何整數的符號都是三種可能性之一：正、負或零）。
這種方法對程式分析的實用之處在於它所帶來的保證：如果分析在抽象領域中未發現錯誤，那麼在任何具體執行中也不存在錯誤。如果分析發現潛在錯誤，該錯誤在實踐中可能發生也可能不會發生，但任何真正的錯誤都無法被隱藏。這就是可靠性。
摘要解讀 vs. AST 分析 vs. 動態分析
這些術語經常被混淆，「AST 代碼分析」出現在本文的搜尋資料中，但它們描述的是不同的事物。
抽象語法樹（AST）是一種表示原始碼語法結構的資料結構。每個編譯器和程式碼檢查工具都會建置一個AST。它是解析、重構工具和基於模式的靜態分析的基礎。基於AST的分析會尋找模式：符合特定規則的程式碼（例如參數過多的函數、透過字串拼接建構的SQL字串）會被標記出來。它不會對值或運行時行為進行推理。
抽象解釋無需運行程式即可推斷運行時行為。它以抽象語法樹（AST）為輸入，但其功能遠不止於此：它還能對值在程式中的流動方式、變數的取值範圍、指標在特定呼叫點是否可能為空以及循環是否終止等進行建模。 AST 分析是模式匹配，而抽象解釋則是行為推理。
大多數程式碼檢查工具（ESLint、Checkstyle、Pylint）主要基於抽象語法樹（AST）。大多數形式化驗證工具（Infer、Astrée、Polyspace）使用抽象解釋。動態分析（運行程式並觀察實際行為）只能發現由特定輸入觸發的錯誤。而抽象解釋則無需執行程式即可發現所有可能輸入下的錯誤。
靜態分析背後的數學原理
搜尋字詞「靜態分析工具背後的數學原理是什麼？」直接出現在搜尋結果中。以下是簡明扼要的答案。
抽象解釋基於三種數學結構：
格。格是一個偏序集，其中任兩個元素都存在一個最小上界（並）和一個最大下界（交）。在靜態分析中，格表示抽象域，即所有可能抽象值的集合，並依其所攜帶的資訊量排序。對於符號分析，格的結構如下：
⊤ (unknown -- could be anything)
/ \
pos neg
\ /
0
|
⊥ (unreachable -- no possible value)沿格向上移動意味著精度降低（知道的資訊減少）。向下移動意味著精度提高（知道的資訊增加）。頂部元素 ⊤ 表示「我們一無所知」。底部元素 ⊥ 表示「此狀態不可達」。
伽羅瓦連接。伽羅瓦連接是具體域（實際程式值）和抽象域（簡化表示）之間的形式關係。它由兩個函數組成：抽象函數 α，它將具體值映射到其抽象表示；以及具體化函數 γ，它將抽象值映射回它們所代表的特定值集合。
關鍵特性：抽象域必須是安全性的過度近似。 γ(α(S)) ⊇ S 對於每個具體集合 S，抽象可能包含比實際存在的值更多的值，這會導致誤報，但它絕不能排除實際存在的值。排除真實存在的值意味著會遺漏真正的錯誤。
定點迭代。對於包含循環的程序，分析必須迭代進行，直到達到穩定狀態。例如，對於以下循環：
c
int x = 0;
while (condition) {
x = x + 1;
}在第一次迭代中， x is {0}經過一個循環體之後， x 可能是 {0, 1}兩個之後， {0, 1, 2}這個集合一直在增長，它永遠不會自行穩定下來。解決方法是： 加寬：一種透過跳到更廣泛的近似值（通常是）來強制收斂的算子 [0, +∞) （用於區間分析）。然後，該分析使用 變窄 為了恢復一些精度。
這種定點計算使得抽象解釋在所有執行路徑（包括循環）上都是完備的，也使得它在計算上比簡單的模式匹配更昂貴。
抽象領域：選擇近似對象
抽象領域決定了分析能夠發現什麼以及不能發現什麼。不同的領域回答關於程序行為的不同問題。
| 抽象領域 | 它追蹤什麼 | 示例使用 | 它缺少什麼 |
|---|---|---|---|
| 符號分析 | 無論數值是正數、負數或零 | 除以零檢測 | 精確值，溢出條件 |
| 區間分析 | 數值的上下限 | 緩衝區溢出，數組存取安全性 | 變數之間的關係 |
| 八角形域 | 變數對之間的線性關係 | 更精確的溢出檢測 | 非線性關係 |
| 指針分析 | 指針是否可能為空或彼此互為別名 | 空引用解引用，釋放後使用 | 物件生命週期、堆形狀 |
| 污點分析 | 價值觀是否來自不可信來源 | SQL注入、XSS檢測 | 透過控制的隱性流動 |
| 多面體域 | 任意線性算術約束 | 循環邊界驗證 | 性能成本呈指數級成長 |
不同域之間的權衡始終是在精確度和效能之間。區間域速度快，能夠捕捉大多數數值錯誤。多面體域精度更高，但複雜度隨變數數量呈指數級增長。實際的靜態分析工具會根據目標應用選擇合適的域來平衡精度和性能：安全關鍵型嵌入式系統可以接受速度較慢但精度更高的分析；而整合到 CI/CD 中的程式碼檢查工具則需要在幾秒鐘內完成。
三種真實工具如何運用抽象解釋
與其孤立地描述理論，不如用具體的工具來闡明其應用。
Facebook Infer使用一種名為雙向溯因推理的抽象解釋方法，分析 Java、C、C++ 和 Objective-C 程式碼中的空指標解參考、資源洩漏和競態條件。雙向溯因推理能夠自動發現函數的前提條件和後置條件，因此無需手動指定即可進行過程間分析。 Infer 已在 Facebook、Spotify、Mozilla 和數十家其他大型組織的持續整合 (CI) 環境中運行，因為它能夠擴展到數百萬行程式碼庫，同時對所檢查的錯誤類型保持穩健。
Astrée使用抽象解釋和數值抽象域來驗證 C 程式中是否存在執行時間錯誤。空中巴士公司曾使用 Astrée 對 A380 的主飛行控制軟體進行形式化驗證，證明整個控制系統不存在運行時錯誤，這是任何測試程序都無法提供的保證。 Astrée 對其檢查的錯誤類型沒有漏檢，但可能會產生需要手動審核的誤報。
Polyspace（MathWorks 公司）對安全關鍵型應用程式中的嵌入式 C 和 C++ 程式碼應用抽象解釋。它將每個操作分類為“綠色”（可證明無錯誤）、“紅色”（肯定有錯誤）或“橙色”（潛在錯誤，需要審查）。綠色分類是一種形式化證明：在該操作處，任何執行都不會導致運行時錯誤。
可靠性-精確性-性能三角
抽象解釋工具需要在相互競爭的屬性三角關係中周旋。沒有任何工具能夠同時最大化這三個屬性的效用。
可靠性意味著不會出現漏報：被分析類別中的所有真實錯誤都能被偵測到。可靠的工具能夠提供保障；不可靠的工具則可能漏掉錯誤。
精確度意味著假陽性率低：發現的問題與實際存在的問題相符，而非理論上不可能出現的問題。高精確度需要更精細的抽象領域和程式間分析。
性能指的是分析能在有效時間內完成。更精確的分析成本更高。證明百萬行程式碼庫中不存在所有執行時間錯誤需要數小時；而程式碼檢查工具只需幾秒鐘即可完成掃描。
不同的應用場景需要在這個三角形中佔據不同的位置：
- IDE linting 和 CI/CD性能第一，精度第二，音質可選。
- 安全掃描：精度優先（減少開發人員的警報疲勞），健全性對於高嚴重性類至關重要
- 安全關鍵認證首要考慮的是系統完整性（不能遺漏真正的漏洞），其次是效能，允許有誤報，但需人工審核。
嵌入式和安全關鍵開發中的抽象解釋
「靜態分析在嵌入式開發中的優勢」這一查詢指出了抽象解釋最重要的應用領域之一。嵌入式系統、汽車控制單元、醫療設備韌體、航太飛行控制軟體等都存在一些限制，使得抽象解釋特別重要：
沒有適用於所有狀態的測試框架。汽車ECU即時響應數千種感知器組合。為每種組合建立測試是不可能的。抽象解釋可以同時涵蓋所有狀態。
認證要求。 DO -178C（航空航太）、ISO 26262（汽車）和IEC 62443（工業控制）均要求證明軟體在所有條件下都能正確運作。使用抽象解釋的形式化驗證可以滿足此要求，而測試覆蓋率報告則無法做到這一點。
資源限制。嵌入式軟體通常沒有記憶體分配器、異常處理機制，也沒有作業系統回退機制。運行時錯誤、空指標解引用、陣列越界等都會導致系統嚴重故障。錯過這些漏洞的代價並非只是一份崩潰報告和緊急修復，而是一起安全事故。
Astrée 和 Polyspace 分析器正是為此而設計的。它們的設計以較高的誤報率和較慢的分析速度為代價，換取了不漏報的保證。
誤報與日益擴大的問題
抽象解釋工具最常見的批評是誤報，即對實際執行中不可能出現的潛在錯誤發出警告。理解誤報的本質是其固有特性而非品質缺陷，有助於更好地管理誤報問題。
假陽性結果主要來自兩方面：
抽象領域的過度近似。 如果區間域追蹤 x ∈ [0, 100]它無法區分以下情況： x 實際上總是小於 50。除以 x 即使程序邏輯保證了這一點，也可能被標記為可能除以零。 x > 0更精確的網域（追蹤確切值，或約束連結） x 將結果轉換為另一個變數）可以消除假陽性，但計算成本更高。
擴大。 使循環分析變得可行的收斂算子必然會失去資訊。在擴展之後 x [0, 5] 至 [0, +∞)分析器不再知道 x 保持在邊界內。如果代碼檢查 assert(x < 1000) 循環結束後，即使在實踐中，這個斷言也無法再被證明。 x 始終遠低於 1000。
管理誤報的實用策略：配置分析以對關鍵模組使用更精確的域（接受較慢的分析），使用有針對性的註釋抑制已確認的誤報，並將工具的橙色/未知結果視為優先審查隊列，而不是已確認的錯誤。
SMART TS XL 在企業級規模上應用靜態分析
SMART TS XL 它運作於抽象解釋理論與企業現實相遇的領域：程式碼庫跨越多種語言、數十年的發展歷程以及組織邊界，使得按程序進行形式化驗證變得不切實際。
與其將單一的抽象領域應用於所有程序， SMART TS XL“ 靜態程式碼分析 結合適用於環境中每種語言（COBOL、JCL、Java、Python、RPG、PL/I、SQL 和現代技術堆疊）的結構分析技術，同時在整個產品組合中產生品質指標、依賴關係資料和安全性發現。
應用程式依賴關係映射功能將圖論分析應用於跨語言呼叫圖，識別程式、資料集和作業流程如何跨越語言邊界進行連接，這是單語言工具無法執行的全系統分析。這是系統層面的結構推理：不是證明單一程式的屬性，而是證明它們如何連接的特性。
影響分析功能對依賴關係圖進行可達性分析：給定一個節點的建議變更，計算從該變更可達的所有節點的集合。這是靜態分析問題“哪些部分會受到影響？”，其答案是基於程式碼結構，而非運行時觀測或人工估計。
對於進行 遺產現代化 程式， SMART TS XL's 結構分析彌合了形式抽象解釋工具（特定於語言，需要領域專業知識進行配置）與理解大型、無文檔的多語言遺留系統實際運作方式的實際需求之間的差距，這是任何不想在執行過程中發現最昂貴意外的現代化專案的先決條件。
常見問題
抽象解釋和模型檢測有什麼不同？兩者都是程序驗證的形式化方法。抽象解釋過度近似所有可能的狀態（可靠但可能不夠精確）。模型偵測窮舉所有狀態空間（完備但僅適用於有限有界系統）。抽象解釋適用於大型程式。模型檢測適用於較小模型上的複雜屬性。它們是互補的，而非競爭的。
抽象解釋是否僅適用於安全關鍵型軟體？並非如此，儘管它在這些軟體中確實能發揮最顯著的價值。 Infer 已應用於大型科技公司的標準 CI/CD 管線中，能夠偵測日常 Java 和 C 程式碼中的空指標解引用和資源外洩。其嚴謹程度取決於個人選擇：一端是提供形式化保證的完全可靠性，另一端是輕量級的啟發式分析，而大多數實用工具則介於兩者之間。
抽象解釋能否分析 COBOL 程式碼？抽象解釋作為一種理論，與語言無關。將其應用於 COBOL 需要實現 COBOL 操作的抽象傳遞函數、PIC 欄位運算、REDEFINES 子句、88 級條件名稱等等。通用抽象解釋工具（例如 Infer 和 Astrée）不支援 COBOL。能夠原生瞭解 COBOL 的企業級結構分析平台會應用相關的靜態分析技術來尋找 COBOL 程式碼庫中的品質問題、死程式碼和架構問題。
