你的測試套件通過了。你的型別檢查器是綠燈。你發布了。兩小時後，生產環境在某個沒人想到要測試的邊緣案例上拋出了 IndexError。
測試能找到錯誤。型別能防止一部分。但兩者都無法證明你的程式完全沒有執行時錯誤。為此，你需要更強大的東西：一種能夠同時對所有可能的執行路徑進行推理、而不需要實際執行程式的方法。
抽象解釋就是讓這成為可能的技術。它驅動了 Astrée、Facebook 的 Infer 等靜態分析器內部的核心，也解釋了 Rust 借用檢查器中的健全性保證。它同時也說明了為什麼大多數靜態分析「零誤報」的行銷宣稱都是謊言。
執行時錯誤是一個可達性問題
執行時錯誤只不過是某個操作到達了不良狀態。除以零、空指標解引用、緩衝區溢位、索引超出範圍。每一個都是因為執行到達了某個程式點，而該處的操作是不安全的。
要證明不存在任何執行時錯誤，你就必須證明在每一種可能的執行中，每一個不安全的操作都是不可達的。每一種輸入。每一個分支。每一次迴圈迭代。
窮舉測試對任何超出玩具等級的程式都是不可能的。符號執行的擴充性很差，因為路徑爆炸會拖垮你。抽象解釋採取了不同的路線：它放棄了知道精確數值，改為追蹤能夠保證涵蓋所有真實執行的近似屬性。
抽象解釋實際上在做什麼
抽象解釋由 Patrick 和 Radhia Cousot 於 1976 年提出。核心思想極為優雅而簡單：執行你的程式，但不用真實的數字、字串和指標來計算，而是使用能夠過度近似真實數值的抽象表示來計算。
可以把它想像成用一個「影子」執行來取代你的具體執行，這個影子執行會追蹤你關心的屬性。與其知道 x = 42，你可能只知道 x > 0。與其知道 arr 的長度是 10，你可能只知道 arr 是非空的。
關鍵的約束是健全性。每一個具體狀態都必須被某個抽象狀態所表示。如果抽象執行說某個操作是安全的，那麼它所代表的每一個具體執行都是安全的。代價則是精確度：如果抽象狀態太過模糊，你就會得到誤報（對安全操作發出虛假的警告）。
一個具體範例：區間分析
這裡是一個最簡化的抽象直譯器，能夠證明除以零是不可能的。它使用區間來追蹤每個變數的可能範圍。
# A tiny abstract interpreter for interval analysis
from dataclasses import dataclass
from typing import Dict
@dataclass(frozen=True)
class Interval:
lo: float
hi: float
def __contains__(self, val: float) -> bool:
return self.lo <= val <= self.hi
TOP = Interval(float("-inf"), float("inf"))
def eval_expr(env: Dict[str, Interval], expr) -> Interval:
if isinstance(expr, int):
return Interval(float(expr), float(expr))
if isinstance(expr, str):
return env.get(expr, TOP)
if expr[0] == "+":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
return Interval(l.lo + r.lo, l.hi + r.hi)
if expr[0] == "-":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
return Interval(l.lo - r.hi, l.hi - r.lo)
if expr[0] == "*":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
products = [l.lo * r.lo, l.lo * r.hi, l.hi * r.lo, l.hi * r.hi]
return Interval(min(products), max(products))
if expr[0] == "/":
l = eval_expr(env, expr[1])
r = eval_expr(env, expr[2])
if r.lo <= 0 <= r.hi:
raise ValueError("Possible division by zero")
return TOP
raise ValueError(f"Unknown expr: {expr}")
def merge_envs(env1: Dict[str, Interval], env2: Dict[str, Interval]) -> Dict[str, Interval]:
keys = set(env1) | set(env2)
result = {}
for k in keys:
a = env1.get(k, TOP)
b = env2.get(k, TOP)
result[k] = Interval(min(a.lo, b.lo), max(a.hi, b.hi))
return result
def analyze(program, env: Dict[str, Interval]) -> Dict[str, Interval]:
env = dict(env)
for stmt in program:
if stmt[0] == "assign":
_, var, expr = stmt
env[var] = eval_expr(env, expr)
elif stmt[0] == "if":
_, cond, true_branch, false_branch = stmt
t_env = analyze(true_branch, dict(env))
f_env = analyze(false_branch, dict(env))
env = merge_envs(t_env, f_env)
elif stmt[0] == "while":
_, cond, body = stmt
old = dict(env)
for _ in range(10):
new = analyze(body, dict(old))
changed = False
for k in set(old) | set(new):
prev = old.get(k, TOP)
curr = new.get(k, TOP)
widened = Interval(min(prev.lo, curr.lo), max(prev.hi, curr.hi))
if widened.lo != prev.lo or widened.hi != prev.hi:
changed = True
old[k] = widened
if not changed:
break
env = old
return env
# Example program: y = 10 / (x + 1) where x >= 0
program = [
("assign", "t", ("+", "x", 1)),
("assign", "y", ("/", 10, "t")),
]
# This should pass: x >= 0 means t >= 1, so no division by zero
safe_env = analyze(program, {"x": Interval(0, 100)})
print("Safe env:", safe_env)
# This should fail: x could be -1
try:
bad_env = analyze(program, {"x": Interval(-5, 5)})
except ValueError as e:
print("Caught:", e)執行它。第一個案例證明了安全性，因為 t 的區間是 [1.0, 101.0]，排除了零。第二個案例正確地標記了風險，因為當 x 為 -1 時，t 可能為零。
if 處理器透過取區間的聯集來合併兩個分支。while 處理器會反覆迭代，直到區間不再增長（也就是達到不動點）。這就是抽象解釋的核心：你用精確數值換取保證的過度近似，並透過證明不良狀態落在近似範圍之外來證明安全性。
在哪裡會崩潰：精確度的障壁
上面的範例只是玩具等級。真實程式有別名、遞迴、堆積分配，以及具有資料相依邊界的迴圈。每一項都會以可預期的方式摧毀精確度。
考慮一個將 i 從 0 遞增到 100 的迴圈。一個朴素的區間分析可能會將 i 擴展到 [0, +inf)，而且永遠無法恢復上界。你需要關係型域（例如多面體或八角形）來追蹤 i <= 100。這些域的複雜度在變數數量上是三次方或指數級的。對於一個有 1,000 個變數的程式，你根本不可能執行多面體分析。
這就是為什麼商業工具會做出不同的選擇。Astrée 使用一個精心選擇的抽象域格，針對嵌入式 C 手動調校。Infer 使用分離邏輯和雙向推導來擴展到數百萬行的行動裝置程式碼，但它在某些語言特性上放棄了健全性。Rust 的借用檢查器本質上是一個抽象直譯器，只不過它只有一個極度精確的域：所有權。
你無法迴避的權衡
健全性、精確度，以及擴充性。選兩個。
一個健全且高精確度的分析器無法擴展到small modules之外。一個可擴展且健全的分析器會用誤報淹沒你。一個可擴展且精確的分析器會漏掉真實的錯誤。
你選擇的抽象域就是調整的旋鈕。區間分析快速但模糊。多面體分析精確但緩慢。謂詞抽象居中，並驅動了大多數軟體模型檢查器。
如何實際運用這些
你大概不會自己寫一個抽象直譯器。你會使用已經存在的工具。
對於 C 和嵌入式系統，Astrée 和 Frama-C 是成熟的選擇。Frama-C 的 EVA 外掛能夠對真實世界的 C 程式碼執行區間和記憶體分析。
對於 Rust，型別系統已經編碼了一個所有權抽象域。Miri 是一個直譯器，而不是抽象直譯器，但它能捕捉到型別系統遺漏的未定義行為。
對於通用程式碼，Meta 的 Infer 是最接近可擴展抽象直譯器的工具，適用於 Java、C++ 和 Objective-C。它能在生產環境的codebases中找到真實的空指標解引用和記憶體洩漏錯誤。
如果你想自己實驗，可以從一個簡單的符號分析或區間分析開始，用你自己解析的語言。龍書涵蓋了資料流分析。Nielson 和 Nielson 的《Principles of Program Analysis》是專門針對抽象解釋的標準參考書。
證明否定
抽象解釋不會讓你的程式完全沒有錯誤。它給你的是一個數學框架，用於證明特定類別的執行時錯誤是不可能發生的。這個證明的品質取決於你的抽象域、你的擴展策略，以及你容忍誤報的意願。
大多數團隊從良好的測試和健全的型別系統中獲得更多價值。但當你撰寫的程式碼一旦出現執行時錯誤就會導致衛星從天上掉下來時，抽象解釋就是你晚上能夠安心入睡的方法。