這個單元的材料投影片補充教材程式作業

換一個運算子 — SV 2 程式作業

SV 2 那篇的主張很大膽：程式分析與 model checking 的差別，可以縮成兩個可替換的運算子。這份作業就是去把那個運算子真的換掉，看數字怎麼變。

每個指令與每個數字都實跑過。

0 先說原本該用的工具，以及它卡在哪

這一週的 hands-on 原本是 CPV（circuit-based program verifier）。它的想法很漂亮——把 C 程式翻成 Btor2 電路，丟給硬體 model checker 去驗，再把反例翻回軟體世界。那正好把這個暑訓的三個主題串起來。

但它沒辦法開箱即用。 CPV 依賴 Kratos2 做 C→K2 的翻譯，而 repo 裡只附了 Kratos2 的 Python 前端（kratos2/tools/c2kratos/*.py）——真正的 kratos 二進位檔不在裡面，要另外去 FBK 的網站取得。直接跑會停在第一步：

cpv.task_translator.TranslationFailedError: C-to-K2 translation failed!

環境本身是滿足的（Ubuntu 24.04、Python 3.12、clang 18、cgroup2 都在），submodule 也拉得下來。缺的只有那個二進位檔。 拿到之後這份作業可以再補一節。

所以這裡改用 CPAchecker——而且它其實更貼近 SV 2 的主題，因為那篇論文的實作本來就是 BLAST 的擴充，而 CPAchecker 是它的後繼。

1 環境

跟 SV 1 的程式作業一樣，只需要 Docker：

docker pull sosylab/cpachecker:latest
mkdir -p cpa-merge && cd cpa-merge

參數語法要注意。 CPAchecker 4.x 之後改用雙破折號，而且新舊語法不能混用。舊的 -config / -setprop 現在寫成 --config / --option；混著寫會直接被拒絕： 

> Mix of old and new command-line arguments detected, which is not supported.
>
另外 --config 的路徑是相對於工作目錄，而設定檔在容器裡，所以要寫絕對路徑 /cpachecker/config/...。

2 準備一支會遇到匯合點的程式

merge 運算子只在兩條路徑匯合的時候才起作用，所以測試程式要有分支。

cat > merge-demo.c <<'EOF'
extern int __VERIFIER_nondet_int(void);
extern void reach_error(void);

int main() {
  int a = __VERIFIER_nondet_int();
  int b = __VERIFIER_nondet_int();
  int c = __VERIFIER_nondet_int();
  int d = __VERIFIER_nondet_int();
  int w, x, y, z;

  if (a) w = 1; else w = 2;   /* 每個 if 之後都是一個匯合點 */
  if (b) x = 1; else x = 2;
  if (c) y = 1; else y = 2;
  if (d) z = 1; else z = 2;

  if (w + x + y + z == 99) { reach_error(); }   /* 永遠不成立：最大是 8 */
  return 0;
}
EOF

四個 if，所以有四個匯合點。性質是成立的（四個變數最大加起來是 8，不可能是 99）。

3 核心實驗：只換 merge

# merge^sep —— 兩條路各走各的（model checking 那一端）
docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" sosylab/cpachecker \
  --config /cpachecker/config/valueAnalysis-NoCegar.properties \
  --option cpa.value.merge=SEP merge-demo.c

# merge^join —— 匯合時併成一個（data-flow analysis 那一端）
docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" sosylab/cpachecker \
  --config /cpachecker/config/valueAnalysis-NoCegar.properties \
  --option cpa.value.merge=JOIN merge-demo.c

跑完看 output/Statistics.txt。實測結果：

merge=SEPmerge=JOIN
結果TRUETRUE
Size of reached set11027
Number of computed successors12482
Max size of waitlist52

抽象狀態數差了四倍，而指令只差一個字。

這就是教材 §3.6 那張表的實驗版本：

你想要mergestop
data-flow analysis$\mathsf{merge}^{join}$$\mathsf{stop}^{join}$
model checking$\mathsf{merge}^{sep}$$\mathsf{stop}^{sep}$

同一份程式碼、同一個工具，換掉一個運算子，行為就從一端移到另一端。

4 我在這裡踩了一個坑，值得你也踩一次

我第一次做這個實驗時，用的是兩個現成的設定檔：

--config /cpachecker/config/valueAnalysis-NoCegar.properties        # 沒有 merge 設定
--config /cpachecker/config/valueAnalysis-NoCegar-join.properties   # 有 cpa.value.merge = join

數字漂亮地出來了：110 對 27。我差點就寫成「merge 造成四倍差距」。

但把那兩個檔案打開看：

# valueAnalysis-NoCegar-join.properties
analysis.traversal.order = bfs
analysis.traversal.useReversePostorder = true
cpa.value.merge = join

它們差的不只是 merge，還差了走訪順序。 那個 110 對 27 有可能一部分來自 BFS 而不是 join，我沒有辦法從那組數據分辨。

正確的做法是第 3 節那樣：固定同一個設定檔，只用 --option 改一個參數。重跑之後數字仍然是 110 對 27，所以結論成立——但那是驗證過的結論，不是碰巧看起來對的結論。

這正是 SV 2 和 SV 3 兩篇論文整篇在講的事。 SV 3 §0.1 說得更直接：跨論文的效能比較不可靠，因為你分不清差距來自演算法還是來自實作細節。我在一個只有四個 if 的玩具程式上，一樣掉進同一個坑。

5 另一半的取捨：精度呢

教材說 join 換來的效率是有代價的——資訊會流失。所以我又寫了一支程式，它的性質需要記得兩個變數來自同一條路徑才能證明：

cat > merge-precision.c <<'EOF'
extern int __VERIFIER_nondet_int(void);
extern void reach_error(void);

int main() {
  int c = __VERIFIER_nondet_int();
  int x, y;
  if (c) { x = 1; y = 1; } else { x = 2; y = 2; }
  /* x 與 y 永遠相等，所以 (x==1 && y==2) 不可能 */
  if (x == 1 && y == 2) { reach_error(); }
  return 0;
}
EOF

預期是：SEP 保住兩條路的關聯，證得出來；JOIN 把 x、y 都併成未知，應該產生誤報。

實測結果不是這樣：

merge=SEPmerge=JOIN
結果TRUETRUE
Size of reached set1313

兩邊都證出來了，狀態數也一樣。 精度損失沒有被觸發。

這不是教材錯了，也不是實驗失敗——它是一個真實的觀察：理論上存在的取捨，在玩具程式上不一定顯現。CAV'07 的實驗跑的是真實的 Windows 驅動程式（最大 138,000 行），差別要在那個尺度才穩定看得出來。

這是留給你的第一道題：設計一支能讓 JOIN 真的產生誤報的 C 程式，或者說明為什麼在 CPAchecker 的 value analysis 裡不容易做到。（提示：先搞清楚它的 join 到底把兩個狀態併成什麼——output/ 裡有線索。）

6 其他可以轉的旋鈕

# 換 stop 運算子
--option cpa.value.stop=SEP        # 或 JOIN

# 換走訪順序（第 4 節那個變因，這次單獨看它值多少）
--option analysis.traversal.order=bfs
--option analysis.traversal.useReversePostorder=true

# 換整個分析（predicate 而不是 value）
--config /cpachecker/config/predicateAnalysis.properties
--option cpa.predicate.merge=SEP   # 或 JOIN

想知道某個設定檔到底設了什麼，直接印出來看——它們都是純文字：

docker run --rm --entrypoint /bin/cat sosylab/cpachecker \
  /cpachecker/config/valueAnalysis-NoCegar-join.properties

7 作業建議

  1. 把第 3 節的表自己跑出來，然後把 merge-demo.c 的 if 從 4 個加到 6 個、8 個，看兩條曲線怎麼分開。
  2. 單獨量走訪順序的影響（第 4 節那個變因），回答：110 對 27 裡面，有多少真的是 merge 的功勞？
  3. 試第 5 節那道題：讓 JOIN 產生誤報。
  4. 換成 predicate analysis 再做一次，比較 cpa.predicate.merge 的效果跟 value analysis 是否一致。
  5. 進階：教材 §3.6 說「中間那一整片是新的」——merge=JOIN 配 stop=SEP 是什麼行為？跑跑看，然後回頭讀 §3.6 最後那段對設定 C 的討論。

遇到問題時