SV 2 — Configurable Software Verification
原文：CAV 2007 · doi:10.1007/978-3-540-73368-3_51 · 開啟原文 PDF ↗
上一篇解決了一個具體問題：predicate 從哪裡來。這一篇問的問題大得多：
程式分析和 model checking，是不是同一件事？
兩個社群、兩套詞彙、兩種工具，做的事卻高度重疊。這篇給出的答案是：它們是同一個演算法的兩種設定，而且中間還有一整片沒人探索過的空間。
0 你需要先會的東西
0.1 精確與快速，只能挑一個
自動驗證程式時有個永遠的取捨（論文 §1, p.504）：
- 越精確，誤報越少，但越貴，能處理的程式越小
- 越快，能處理越大的程式，但誤報越多
歷史上這個取捨長成兩個社群：
| program analysis | model checking | |
|---|---|---|
| 偏好 | 效率 | 精確 |
| 路徑處理 | 匯合時合併（path-insensitive） | 保持分開 |
| 資料結構 | 沿 CFG 邊傳播，算到 fixpoint | 展開成 reachability tree |
| 典型規模 | 大程式、簡單性質 | 小程式、複雜性質 |
論文一開始就講了一句很誠實的話：理論上早就知道兩者互為對方的特例，但*這種理論關係對實務幾乎沒有影響*。這篇要做的是把它變成能用的東西。
0.2 兩條路走到同一個地方，然後呢
先看清楚差別在哪。假設程式長這樣：
if (c)
x = 1;
else
x = 2;
// 兩條路在這裡匯合
y = x;
執行到 y = x 這一行時，前面有兩條路走過來，各自帶著不同的資訊（x = 1 或 x = 2）。這時要怎麼辦？
- 合併：把兩條路的資訊併成一個。我們只知道「x 是 1 或 2」，通常會粗略地記成「x 未知」。狀態少了一個，但資訊也少了。
- 分開：兩條路各自繼續往下走。資訊完整，但狀態數變成兩倍。
程式分析選合併，model checking 選分開。這就是全部的差別——至少是最核心的那個差別。
0.3 lattice：把「資訊多寡」排成順序
要談合併，得先有辦法比較「誰的資訊比較多」。這就是 lattice（格）在做的事。
想像我們追蹤變數 x 的值。可能的知識狀態有：
⊤ （完全不知道）
/ | \
... 1 2 3 ...
\ | /
⊥ （這條路根本走不到）
- $\top$（top）：什麼都不知道，涵蓋所有可能
- $\bot$（bottom）：不可能，空的
- 中間是具體的知識
序關係寫成 $\sqsubseteq$。$e_1 \sqsubseteq e_2$ 讀作「$e_1$ 的資訊不少於 $e_2$」，或者說「$e_1$ 描述的狀態集合被 $e_2$ 包含」。
線代橋：$\sqsubseteq$ 就是子空間的 $\subseteq$。$\top$ 是全空間，$\bot$ 是零空間。這個對照可以一直用下去。
join（$\sqcup$）是「同時涵蓋兩邊的最小者」。x=1 和 x=2 的 join 是 $\top$——因為沒有更精確的東西能同時涵蓋兩者。
線代橋：$U \sqcup V$ 就是 $\mathrm{span}(U \cup V)$，同樣是「包含雙方的最小子空間」。
0.4 fixpoint：算到不再變為止
程式分析的執行方式是：沿著 CFG 的邊反覆傳播資訊，直到再傳也不會變為止。那個不再變的狀態叫 fixpoint（不動點）。
寫成式子就是 $F(x) = x$：把運算再套一次，結果跟原本一樣。
注意這裡的線代橋是斷的。 不要類比成特徵向量——$Ax = 3x$ 也是特徵向量，但 $3x \ne x$，它根本不是不動點。要找線代錨點的話，用投影矩陣的冪等性 $P^2 = P$：投影兩次跟投影一次一樣，那才是不動點。
0.5 worklist：你已經會這個演算法
這一節是好消息。CPA 的演算法核心，你在計概就寫過了。
回想 BFS：
把起點放進佇列
while 佇列非空:
取出一個節點
for 每個鄰居:
if 還沒訪問過:
標記訪問過
放進佇列
CPA 的演算法是一模一樣的骨架，只是把「訪問過沒有」這個判斷換成兩個可以替換的零件：
| BFS | CPA |
|---|---|
| 佇列 | waitlist（待處理的 abstract state） |
| 已訪問集合 | reached（已到達的 abstract state） |
| 「這個鄰居訪問過了嗎」 | stop（這個新狀態被已有的涵蓋了嗎） |
| （沒有對應） | merge（要不要跟已有的狀態合併） |
多出來的 merge 就是 0.2 那個問題的答案位置。整篇論文的力量都來自「把這兩個判斷抽出來變成參數」。
0.6 CFA 和 concrete state
兩個記號。CFA（control-flow automaton）是程式的圖：$(L, pc_0, G)$——位置集合、進入點、邊集合。每條邊 $g \in G$ 標著一個操作。
concrete state（具體狀態）是一組完整的變數賦值，包含 program counter。程式執行就是在具體狀態之間跳。所有具體狀態的集合寫成 $C$。
abstract state 則是「一群具體狀態的簡略描述」。從 abstract state 還原回它代表哪些具體狀態的函數，叫 concretization function，寫成 $\llbracket \cdot \rrbracket : E \to 2^C$。
以上是前置。接下來是論文本身。
1 這篇要解決的問題
程式分析和 model checking 的差別，能不能變成一個可以調的參數，而不是兩套不同的工具？
論文的答案是可以，而且只需要抽出兩個運算子。
2 在這之前，卡在哪裡
論文 §1（p.505）講的痛點很具體，而且動機是實務的，不是理論的。
理論上，你當然可以重新定義一個 abstract interpreter，把合併策略和終止條件都寫死在裡面。問題是：
- 現成的 abstract interpreter（論文舉的是 predicate abstraction 與 shape analysis）都是別人寫好的、經過驗證的積木
- 每換一種合併策略就重寫一次 abstract interpreter，成本高到沒人會做
- 結果就是每種組合都是硬接的（hard-wired）：predicated lattices 是一種組合、lazy shape analysis 是另一種，各寫各的
作者想要的是：把 abstract interpreter 當零件重用，只換執行引擎的設定。
這也解釋了為什麼這篇的貢獻是「一個框架」而不是「一個更好的演算法」。
3 關鍵洞察：四個零件
論文 §2.1（p.506）把一個 configurable program analysis 定義成四元組：
$$\mathbb{D} = (D, \rightsquigarrow, \mathsf{merge}, \mathsf{stop})$$3.1 abstract domain $D$
$D = (C, \mathcal{E}, \llbracket \cdot \rrbracket)$：具體狀態集合、一個 semi-lattice $\mathcal{E} = (E, \top, \bot, \sqsubseteq, \sqcup)$、以及 concretization function。
它決定分析看得見什麼。 追蹤變數區間？追蹤 predicate 真假？追蹤 heap 形狀？這裡決定。
3.2 transfer relation $\rightsquigarrow$
$\rightsquigarrow \subseteq E \times G \times E$。給一個 abstract state 和一條 CFA 邊，算出後繼的 abstract state。
它決定「執行一步」是什麼意思。
3.3 merge：匯合時合不合併
$\mathsf{merge} : E \times E \to E$。這是 0.2 那個問題的答案所在。
論文給了兩個標準選擇：
| 運算子 | 定義 | 行為 |
|---|---|---|
| $\mathsf{merge}^{sep}$ | $\mathsf{merge}(e, e') = e'$ | 不合併，兩條路各走各的 |
| $\mathsf{merge}^{join}$ | $\mathsf{merge}(e, e') = e \sqcup e'$ | 併成一個 |
注意 merge 不是對稱的，它不等於 lattice 的 $\sqcup$。它的簽名是「拿第一個參數的資訊去影響第二個」，結果必須滿足 $e' \sqsubseteq \mathsf{merge}(e, e')$——只能變得更抽象，不能更精確。這條限制是 soundness 的一部分。
3.4 stop：什麼時候可以不再往下走
$\mathsf{stop} : E \times 2^E \to \mathbb{B}$。檢查一個新的 abstract state 是否已經被 reached 裡的東西涵蓋。
| 運算子 | 定義 | 行為 |
|---|---|---|
| $\mathsf{stop}^{sep}$ | $\exists e' \in R : e \sqsubseteq e'$ | 找單一個已有狀態涵蓋它 |
| $\mathsf{stop}^{join}$ | $e \sqsubseteq \bigsqcup_{e' \in R} e'$ | 把 $R$ 全部 join 起來再比 |
$\mathsf{stop}^{join}$ 有前提。 論文 p.507 寫的是「or —if $D$ is a powerset domain— can join the elements of $R$」：只有當 abstract domain 是 powerset domain（註腳 2 的定義：$\llbracket e_1 \sqcup e_2 \rrbracket = \llbracket e_1 \rrbracket \cup \llbracket e_2 \rrbracket$，join 之後代表的具體狀態剛好是聯集、不多不少）才能這樣做。不是 powerset domain 的話，join 會把範圍放大，「$e$ 被 join 覆蓋」就不再蘊含「$e$ 被 $R$ 覆蓋」，下面那條 soundness 要求就破了。
soundness 的要求是：$\mathsf{stop}(e, R) = \mathit{true}$ 必須蘊含 $\llbracket e \rrbracket \subseteq \bigcup_{e' \in R} \llbracket e' \rrbracket$——說「可以停」的時候，就真的不能漏掉狀態。
3.5 演算法：BFS 加兩個旋鈕
論文 Algorithm 1（p.508）的骨架：
reached := {e₀}
waitlist := {e₀}
while waitlist ≠ ∅:
從 waitlist 取出 e
for 每個後繼 e'（由 ⇝ 算出）:
for reached 裡的每個 e'':
eₙₑw := merge(e', e'') ← 旋鈕一
if eₙₑw ≠ e'':
用 eₙₑw 取代 e''（兩個集合都換）
if ¬ stop(e', reached): ← 旋鈕二
把 e' 加進 waitlist 和 reached
return reached
跟 0.5 的 BFS 對照著看，多出來的只有 merge 那一段，以及把「訪問過沒有」換成 stop。
Theorem 1（Soundness）：對任何 CPA 和初始狀態，這個演算法算出的 abstract state 集合，其涵蓋範圍是真正可達狀態的過近似。也就是說——它可能多算，但不會漏。
3.6 兩個經典方法都掉出來了
| 你想要 | merge | stop |
|---|---|---|
| data-flow analysis | $\mathsf{merge}^{join}$ | $\mathsf{stop}^{join}$ |
| model checking | $\mathsf{merge}^{sep}$ | $\mathsf{stop}^{sep}$ |
換兩個運算子，同一份程式碼就從一種方法變成另一種。
而中間那一整片是新的。 $\mathsf{merge}^{join}$ 配 $\mathsf{stop}^{sep}$ 呢？在某些位置合併、某些位置不合併呢？Abstract（p.504）的原話是這個工具提供「many intermediate settings that have not been evaluated before」，而且「such customization may lead to dramatic improvements in the precision-efficiency spectrum」。
注意這句的主詞是「可配置」本身，不是「中間設定比較好」。 實驗裡表現最好的是設定 C，而 C 的 merge／stop 其實跟純 model checking 完全相同（見 §6 的導覽表）——它贏在第三個零件 transfer relation，不在 merge／stop 的中間。
論文舉的三個 instance：Location Analysis（只追蹤 program counter）、Predicate Abstraction、Shape Analysis。（這裡的 predicate abstraction 論文 p.507 引的是 Ball et al. 的 cartesian predicate abstraction，不是 SV 1 那篇；但你在 SV 1 建立的直覺完全用得上。）它們都能寫成這個四元組——這正是「把 abstract interpreter 當積木重用」的意思。
4 手算一遍
看一次 merge 造成的差異，比讀十遍定義有用。
5 對後續的影響
先講清楚一件事：這篇的實作不是 CPAchecker。 論文全文沒出現這個名字。當時的實作是把 BLAST 改造出來的——Introduction（p.504）說「we have extended the software model checker BLAST」，Conclusion（p.517）說得更完整：「We have therefore modified BLAST from a tree-based software model checker to a tool that can be configured」。
CPAchecker 是後來的事。 這個框架日後的實作平台才是它——SV 3 的註腳（p.301）明說 Our implementation is based on CPAchecker，你在下一篇讀到的每個運算子都是在它裡面實作的。
更重要的是這個框架後來被撐大了。 SV 3 會告訴你，光有這四個零件還不夠——要把 BMC、k-induction、IMPACT 都裝進來，還需要第五、第六個零件。那一篇用的是 CPA+（順帶一提，CPA+ 也不是 SV 3 提出的，它出自同一批作者的 ASE'08）：
$$(D, \Pi, \rightsquigarrow, \mathsf{merge}, \mathsf{stop}, \mathsf{prec})$$多出來的是 precision 的集合 $\Pi$ 和 precision-adjustment operator $\mathsf{prec}$。而且演算法本身也再擴充了一次（CPA++，加上 abort 和 forced covering）。
這個差別要記住，別把兩篇的 CPA 當成同一個東西——下一篇的 prec 正是它統一四種演算法的機制。
6 讀原文時的導覽
只有 15 頁，但密度高。
下表的章節名與起始頁都逐頁對照過原文。
| 章節 | 頁 | 建議 |
|---|---|---|
| Abstract、§1 Introduction | p.504–506 | 必讀。 特別是 p.505 講 merge/stop 動機那兩段，是全篇最好的解釋 |
| §2.1 Configurable Program Analysis | p.506–508 | 必讀。 四個零件的定義與 soundness 要求 (a)–(d)（p.507） |
| §2.2 Execution Algorithm | p.508–510 | 必讀。 Algorithm 1（p.508）與 Theorem 1（p.509） |
| §2.3 Composite Program Analyses | p.510–512 | 進階但重要。多個分析怎麼組合、資訊怎麼透過 strengthening 運算子互通 |
| §3 Experiments | p.512–517 | 值得看，但要讀仔細。Table 1（p.516）列出六種設定 A–F，註腳 8 有每種的一句話說明。Summary（p.517）說 configuration C is the best choice，但同一段馬上補一句 we cannot conclude that configuration C is the preferred configuration for any combination——別把它當成通則 |
| §4 Conclusion | p.517 | 一頁，可快速掃過 |
取得原文：台大校內網路可直接下載，見頁首 DOI。
下一步：SV 3 會把這個框架再撐大，然後用它證明一件事——BMC、k-induction、predicate abstraction、IMPACT 其實是同一個演算法的四種設定。