SV 1 — Abstractions from Proofs

原文：POPL 2004 · doi:10.1145/982962.964021

這一篇要回答一個很具體的問題：程式驗證器要追蹤哪些事實？

追蹤太少，驗證器會誤報；追蹤太多，它會跑不動。POPL'04 給出的答案是：不要用猜的，去讀「這條路走不通」的證明，答案就寫在裡面。

前半（第 0 節）從你已經會的東西鋪到讀得懂論文為止，不會叫你去讀別的資料再回來。後半是論文本體。

0 你需要先會的東西

0.1 一個電腦「應該」看得出來的問題

int x = 1;
int y = x + 1;
if (y < 0) { ERROR; }

ERROR 到得了嗎？到不了，因為 y 一定是 2。

你花了不到一秒。問題是：電腦要怎麼自動得到同樣的結論？它不能「看一眼」，它需要一套機械的程序。這一整篇論文都在回答這件事的其中一環。

0.2 把程式變成一條邏輯公式

第一步是把「執行路徑」翻譯成「數學式子」。規則只有兩條：

上面那條通往 ERROR 的路徑，翻譯後是：

$$x = 1 \;\wedge\; y = x + 1 \;\wedge\; y < 0$$

現在問題變成純數學的了：這三個條件能同時成立嗎？不能——前兩式逼出 $y = 2$，跟第三式牴觸。

「路徑走得通」等價於「公式有解」。這個轉換是整個領域的地基。

0.3 為什麼變數要加下標（SSA）

上面的翻譯有個漏洞。看這段：

x = 1;
x = x + 1;

照 0.2 的規則會翻成 $x = 1 \wedge x = x + 1$。但第二式 $x = x+1$ 在數學上永遠是假的——沒有任何數字等於自己加一。翻譯出錯了。

問題在於：程式裡的 x 是一個會變的盒子，數學裡的 $x$ 是一個固定的值。同一個名字被當成兩種東西。

解法是給每次賦值後的值一個新名字：

$$x_1 = 1 \;\wedge\; x_2 = x_1 + 1$$

現在它有解了（$x_1 = 1$、$x_2 = 2$），而且忠實反映程式行為。這種「每個變數的每個版本各有一個名字」的寫法叫 SSA（static single assignment）。

論文用的記號是 $\langle x, 1 \rangle$，意思是「第 1 個指令執行後 $x$ 的值」。看到尖括號就是這個意思。

這一小節請確認你真的懂了。 後面所有公式都帶下標，不懂下標就會處處卡住。SV 3 的 path formula 也整篇建立在 SSA 上。

0.4 有解、無解，和回答這件事的工具

給一堆等式與不等式，問「有沒有一組數字代進去讓它們同時成立」：

SAT solver 和 SMT solver 就是回答這個問題的程式。你不需要知道它們內部怎麼運作，只要知道它們回答什麼：丟一條公式進去，它回答有解或無解。有解時它還會給你一組解。

對我們來說：

公式意思
satisfiable這條路走得通，可能真的有 bug
unsatisfiable這條路走不通，是誤報

0.5 光知道「無解」還不夠

假設驗證器找到一條通往 ERROR 的路徑，丟給 solver，solver 說「無解」。誤報排除了，很好——然後呢？

問題在於程式有無限多條路徑（有迴圈的話）。一條一條排除永遠排不完。我們需要的是一個理由，一個能一次擋掉一整類路徑的事實。

比如 0.1 的例子，真正的理由是「執行到 if 的時候 $y = 2$」。抓住這個事實，就不必再檢查任何走這條路的變體。

這些「事實」該長什麼樣、從哪裡來，就是這篇論文的主題。

0.6 predicate abstraction：只記是非題

事實要怎麼表示？答案是 predicate（述詞）——一個對程式狀態的是非問句，例如 $y > 0$、$x = \mathit{ctr} - 1$、$\mathit{lock} = 1$。

predicate abstraction 的做法是：不追蹤變數的確切數值，只追蹤一組 predicate 的真假。

假設我們選了三個 predicate $p_1, p_2, p_3$，那麼任何一個程式狀態都被壓縮成三個位元，例如 $(\text{真}, \text{假}, \text{真})$。原本無限多的狀態，變成最多 $2^3 = 8$ 種。有限了，就可以窮舉。

代價是資訊流失：兩個不同狀態可能壓成同一組位元。這正是我們要的——抽象就是刻意丟掉不重要的細節。難的是決定「哪些不重要」。

線代的類比：這就像用一組基底把向量寫成座標。基底選得好，少數幾個座標就夠用；選得差，就得帶一大堆。

0.7 CEGAR：猜錯了就改

沒有人一開始就知道該選哪些 predicate。標準做法是一個迴圈，叫 CEGAR（counterexample-guided abstraction refinement）：

  1. 先用很少的 predicate 做一個粗略的抽象
  2. 在抽象上找通往 ERROR 的路徑
  3. 找不到 → 程式安全，結束
  4. 找到了 → 把這條路徑翻成公式（0.2）丟給 solver
  5. 公式有解 → 真的 bug，回報
  6. 公式無解 → 誤報。加入新的 predicate 讓抽象變細，回到第 2 步

這個迴圈本身不難懂。難的全部集中在第 6 步的三個字：「加入新的 predicate」。

加哪些？加多少？加在哪裡？加太少，同一條誤報路徑會再冒出來，迴圈不會結束；加太多，$2^n$ 的狀態數會爆掉。

POPL'04 就是在回答第 6 步。

0.8 Craig interpolation：只用共同語言說話

現在來看這篇論文用的工具。

把一條走不通的路徑從中間切開，前半段叫 $\varphi^-$，後半段叫 $\varphi^+$。兩者合起來無解（路徑走不通）。

interpolant（插值式）是一個公式 $\psi$，滿足三個條件（論文 §2, p.234）：

  1. $\varphi^- \Rightarrow \psi$ —— 前半段成立時，$\psi$ 一定成立
  2. $\psi \wedge \varphi^+$ 無解 —— $\psi$ 已經足以跟後半段矛盾
  3. $\psi$ 只用同時出現在 $\varphi^-$ 和 $\varphi^+$ 裡的符號

Craig interpolation theorem 保證：只要 $\varphi^- \wedge \varphi^+$ 無解，這樣的 $\psi$ 一定存在。（證明不在本文範圍，你只要知道有這個保證。）

用一個比喻。前半段講的是中文，後半段講的是日文，$\psi$ 只能用兩邊都寫得出來的漢字。條件 1 說「$\psi$ 是前半段的合理摘要」，條件 2 說「這份摘要已經足以拆穿後半段」，條件 3 說「摘要只能用共同詞彙」。

第 3 條就是我們要的東西。 切點兩側的共同符號，正是「執行到切點時，變數當下的值」——不多不少，剛好是那個程式位置需要記住的事實。

0.9 怎麼讀推導規則

論文裡有很多長這樣的東西：

   前提1    前提2
  ----------------
      結論

讀法很簡單：橫線上方全部成立時，橫線下方就成立。 旁邊的名字是規則名稱。

例如「兩個不等式可以相加」寫成：

   0 ≤ a      0 ≤ b
  -------------------
       0 ≤ a + b

就這樣。第 4 節你會實際用到它。

0.10 strongest postcondition：條件怎麼往後推

還有一個記號要認識。$\mathsf{SP}.\varphi.\mathit{op}$ 讀作「在滿足 $\varphi$ 的狀態下執行 $\mathit{op}$ 之後，會滿足什麼」。它是能推出的最強結論。

兩個情況就夠用了：

操作效果
賦值 x := e舊的 $x$ 換個名字，加上「新 $x$ 等於 $e$」
assume(p)直接把 $p$ 加進去

例如 $\mathsf{SP}.(x = \mathit{ctr}).(\mathit{ctr} := \mathit{ctr}+1)$ 得到 $x = \mathit{ctr} - 1$：$\mathit{ctr}$ 變大了一，所以 $x$ 現在比它小一。

這其實就是 0.2 和 0.3 在做的事，只是給了個正式名字。你不需要學完整的 Hoare logic。

0.11 CFA：程式的圖

CFA（control-flow automaton）就是把程式畫成一張有向圖：節點是程式位置，邊上標著要執行的操作。

你在計概畫過的流程圖就是這個東西。論文寫成 $C_f = (L_f, E_f, l_f^0, \mathit{Op}_f, V_f)$，拆開來就是「節點集合、邊集合、起點、操作標記、變數集合」。

0.12 線代這座橋，以及它斷在哪裡

接下來兩篇會大量用到 lattice 和 fixpoint。你的線代剛好可以當梯子——但梯子有兩階是斷的，先講清楚，免得之後摔下來。

論文的概念線代的對應能不能用
抽象狀態的序 $\sqsubseteq$子空間的包含 $\subseteq$可以
join $\sqcup$$\mathrm{span}(U \cup V)$，兩者都是「包含雙方的最小者」可以
predicate abstraction 壓成位元向量用一組基底表示向量可以
fixpoint $F(x) = x$特徵向量 $Ax = \lambda x$不行
abstraction投影到子空間可以，但有邊界

為什麼 fixpoint 不能類比成特徵向量。 特徵向量允許縮放：$Ax = 3x$ 也算特徵向量，但 $3x \ne x$，它根本不是不動點。兩者的核心不同。fixpoint 請直接照字面理解：反覆套用同一個運算，直到結果不再改變。真的需要線代錨點時，用投影矩陣的冪等性 $P^2 = P$，那才是不動點。

abstraction 像投影，但只像一半。 「丟掉部分資訊、做兩次跟做一次一樣、保留你關心的分量」——這層直覺是對的，很好用。但這裡沒有內積、沒有正交、沒有『最近的逼近』。abstract interpretation 要的是一個安全的過近似（寧可多算一些狀態，不能漏），不是距離最小的投影。記住這條邊界，之後看到 widening 和 precision 才不會有錯誤期待。

以上就是全部前置。接下來是論文本身。

1 這篇要解決的問題

CEGAR 的迴圈卡在第 6 步：發現誤報之後，該加哪些 predicate？

前人的做法會產生太多、而且擺錯位置的 predicate。程式一大就跑不動。

這篇的答案：把「這條路走不通」的證明拿來讀，需要的 predicate 就寫在裡面——而且能讀出每個程式位置各自需要哪幾個。

2 在這之前，卡在哪裡

論文 §2（p.233）用一個 locking 的例子說明。程式長這樣：

while (*) {
1:  if (p1) lock();
    if (p1) unlock();
2:  if (p2) lock();
    if (p2) unlock();
    ...
n:  if (pn) lock();
    if (pn) unlock();
}

要驗證的性質是 lock 和 unlock 必須交替出現。這程式是對的：每個 lock 後面緊跟著條件相同的 unlock。

但一個不追蹤 p1 的分析器會誤報：它以為第一個 if 可以進去、第二個 if 可以不進去，於是看到「lock 之後沒有 unlock」。

修法很明顯——追蹤 p1 的值。麻煩的是這裡有 $n$ 個這種 if。

兩個問題

第一，數量爆炸。 要排除所有誤報，$p_1, \dots, p_n$ 全都得追蹤。$n$ 個布林 predicate 就是 $2^n$ 種組合，抽象狀態直接指數成長。

第二，位置放錯。 前人的做法是把找到的 predicate一律加到所有程式位置。但仔細看：$p_1$ 只在標籤 1 和 2 之間有用，過了標籤 2 就再也用不到。把 $p_1$ 帶到程式的每個角落，是純粹的浪費。

論文用 parsimonious（精簡）形容理想的抽象：在每個控制位置，只指定當下變數之間的關係，而且只留證明正確性真正需要的那些（Abstract, p.232）。前人的抽象不精簡，原因有二——predicate 裡混進了變數的「舊值」（symbolic variables），而且是靠啟發式規則撒到各處的。

這個觀察有多值錢

論文的實測（§1, p.233）：一個 138,000 行的 C 程式驅動程式，總共需要 382 個 predicate 才能證明正確——但平均每個程式位置只需要 8 個。

382 對 8。這就是為什麼「哪些 predicate 用在哪裡」值得單獨解一次。

3 關鍵洞察

3.1 證明裡面就有答案

論文 §1（p.233）的原話是：一條抽象路徑之所以走不通，理由已經簡潔地編碼在「它走不通」的證明裡了。

所以不要猜。去解那條路徑的公式，solver 說無解時它其實有一份反駁證明（refutation）。把證明讀一遍，需要的事實就浮出來。

而且成本很低：論文說 interpolant 可以用對證明做一次線性掃描得到，不需要額外的定理證明工作。

3.2 這篇真正的貢獻，不是「用了 interpolation」

這點很容易被誤讀，講清楚：Craig interpolation 是 1957 年就有的定理，不是這篇發明的。

這篇發明的是一套可以機械執行的推導規則。 論文 §3 定義了兩層東西：

第一層，一個證明系統（Fig. 3, p.235）。四條規則 HYP、COMB、CONTRA、RES，用來對線性算術的子句集合產生反駁證明。

第二層，帶插值的推導規則。 把上面每條規則改寫成這個形式：

$$(\varphi^-, \varphi^+) \vdash \Gamma \;[\psi]$$

讀作：「在把公式切成 $\varphi^-$ 和 $\varphi^+$ 的前提下，推出了 $\Gamma$，而目前累積的插值式是 $\psi$。」

方括號就是重點。 推導一路往下走，方括號裡的東西同步累積；推到矛盾（$\vdash \bot$）時，方括號裡剩下的就是 interpolant。

不用猜，不用驗證，照著規則走就會掉出來。第 4 節你會親手做一次。

論文用 Invariant 1 和 Invariant 2 證明這些規則是健全的——也就是說，這樣算出來的東西保證滿足 0.8 的三個條件。

3.3 locality：每個位置一份清單

第二個洞察在論文 §3 的 Locality 段（p.235）。

不要只在一個地方切開路徑。沿著路徑的每一個切點都切一次，每個切點各求一個 interpolant。

在第 $i$ 個切點求出的 interpolant，只會用到那個切點兩側的共同符號——也就是執行到那裡時各變數當下的值。把它翻譯回程式變數，就得到「第 $i$ 個位置需要知道的事實」。

於是我們不是得到一包全域 predicate，而是得到一張表：位置 1 需要這些、位置 2 需要那些。382 對 8 的差距就是這樣來的。

論文特別指出，這件事跟 lazy abstraction 搭配時還有一個好處：predicate 集合不再只增不減，沿著路徑走，用得上的 predicate 會換人——interpolation 因此順便給出了「什麼時候某個 predicate 已經沒用了」的判準。

4 手算一遍

這一節你要自己動手。分三段，跟著做完你就真的懂了。

4.1 論文的例子

用論文 Figure 2（p.234）的路徑。ctr 是計數器，m 是另一個變數：

1:  x := ctr;
2:  ctr := ctr + 1;
3:  y := ctr;
4:  assume(x = m);
5:  assume(y ≠ m + 1);

這條路徑走不通。原因：$x$ 抄下舊的 ctr，然後 ctr 加一，$y$ 抄下新的 ctr，所以必然 $y = x + 1$。既然 $x = m$，就有 $y = m+1$，第 5 行的 $y \ne m+1$ 不可能成立。

照 0.3 的 SSA 規則翻成公式（$\langle v, i \rangle$ 表示第 $i$ 個指令後 $v$ 的值）：

行約束
1$\langle x,1 \rangle = \langle \mathit{ctr},0 \rangle$
2$\langle \mathit{ctr},1 \rangle = \langle \mathit{ctr},0 \rangle + 1$
3$\langle y,2 \rangle = \langle \mathit{ctr},1 \rangle$
4$\langle x,1 \rangle = \langle m,0 \rangle$
5$\langle y,2 \rangle = \langle m,0 \rangle + 1$

這五條的 conjunction 就是這條路徑的 trace formula，它無解。

現在在第 2 行後面切一刀：$\varphi^-_2$ 是前兩條，$\varphi^+_2$ 是後三條。兩邊的共同符號是 $\langle x,1 \rangle$ 和 $\langle \mathit{ctr},1 \rangle$——正好就是「執行完前兩行之後，$x$ 和 ctr 當下的值」。

論文算出的 interpolant 是

$$\psi_2 = (\langle x,1 \rangle = \langle \mathit{ctr},1 \rangle - 1)$$

把 SSA 名字翻回程式變數，得到 $\hat\psi_2 = (x = \mathit{ctr} - 1)$。

這就是位置 2 需要記住的唯一事實。 不是 ctr 的值，不是 x 的值，而是它們的差。對五個切點各做一次，就得到 Figure 2 最右欄那一整排 predicate。

4.2 換你算

上面直接給了答案 $\psi_2$。但論文的重點是不用猜——照著規則走，interpolant 會自己掉出來。

下面這題你自己動手。三段：先建立直覺，再認識工具，最後用論文 Figure 4（p.237）的例子實際推導一次。答錯會告訴你錯在哪，答對才解鎖下一步。進度會存著，關掉瀏覽器再回來不會歸零。

為了讓你專心在機制上，這裡只用線性算術的三條規則，不碰 resolution（那需要先學 CNF，留到第 6 節當延伸閱讀）。

4.3 兩個容易混淆的「為什麼」

這裡有個陷阱，很多人第一次會弄混，請把兩件事分開。

問題一：$y$ 是在哪裡消失的？

在第 3 步。$0 \le y-x$ 和 $0 \le z-y$ 相加，$-y$ 和 $+y$ 抵銷，剩下 $0 \le z-x$。這是國中就會的代數消去，跟 HYP-B、跟 interpolation 理論都沒有關係。

問題二：那為什麼 interpolant 能『保證』只含共同變數？

這是另一回事，而且答案不是「因為 HYP-B 記 $0 \le 0$」。真正的保證來自整套規則共同維持的不變量（論文的 Invariant 1 與 Invariant 2）：每一條規則都被設計成不會把非共同符號漏進方括號，所以不論推導怎麼走、多長，結論都成立。

HYP-B 記 $0 \le 0$ 是這套設計的一環——它確保來自 $\varphi^+$ 的資訊不會被抄進插值式——但它只是其中一環，不是全部理由。

把這兩件事混為一談的後果：你會以為「代數消去 = 只含共同變數」。這在上面這個例子恰好看起來成立，但換到 resolution 那半套規則就完全對不上，整個理解會崩掉。

記住：消去是這個例子的計算過程，不變量才是通則的保證。

5 對後續的影響

直接產物是 BLAST，論文作者群的軟體模型檢查器。加上這套 predicate discovery 之後，它成功處理了超過 130,000 行的 C 程式——用「撒 predicate」的舊方法做不到這個規模。

更長遠的影響是它被吸收進一個更大的框架。 SV 2 提出 configurable program analysis，把 model checking 和 program analysis 統一成同一個演算法的不同設定；這篇的 predicate abstraction 就成為其中一種設定。到了 SV 3，連 BMC、k-induction、IMPACT 都被放進同一個框架比較——而 refinement 步驟裡求的東西，正是這篇的 interpolant 的序列版本。

所以讀完這篇不要停。它是三篇裡的第一塊，後面兩篇會把它放回更大的圖裡。

6 讀原文時的導覽

章節頁建議
Abstract、§1 Introduction232–233必讀。 問題意識與 parsimonious 的定義都在這
§2 Overview233–234必讀。 Figure 1 的 locking 例子、Figure 2 的完整範例鏈
§3 Interpolants from Proofs235–237必讀。 但初次讀可以只看 Fig. 3、Fig. 4 和 Locality 那段，跳過 Invariant 的證明
§4 Languages and Abstractions236–237可略讀。程式語言的形式定義，四個程式類別 PI–PIV
§5 Predicate Inference238–240進階。Extract 演算法與 Theorem 1 的細節
§6 General Programs240–242進階。指標與函式呼叫的處理
§7 Experiments243值得看 Table 1，382 對 8 的數據就在這

延伸閱讀。 第 4 節刻意避開了 resolution 規則（RES、RES-A、RES-B），因為那需要先學 CNF 與布林推理。想補齊的話，從 §3 的 Fig. 5 開始，它示範了用 resolution 推導 interpolant。

取得原文。 台大校內網路可直接下載，見本頁頂端的 DOI 連結。本站只放解讀，不放原文。

下一步：SV 2 會問一個更大的問題——這篇的 predicate abstraction、傳統的 data-flow analysis、還有 model checking，它們能不能是同一個演算法？