CPAchecker 上手 — SV 1 程式作業

這一頁的每個指令都在 Linux 上實跑過，輸出就是你會看到的那些。目標不是把工具學完，是讓教材裡的名詞變成你螢幕上的檔案。

0 你只需要 Docker

CPAchecker 是 Java 程式，需要 Java 21 以上，還會用到幾個編譯過的 SMT solver。自己配環境要花時間，而官方有維護得很勤的容器映像檔——sosylab/cpachecker，351 MB。

docker --version        # 有輸出就行

沒有 Docker 就先裝（Linux 用套件管理員，macOS/Windows 用 Docker Desktop）。真的裝不了的話跳到第 6 節，那裡有不用 Docker 的路。

1 拉映像檔

docker pull sosylab/cpachecker:latest

實測約 18 秒拉完。latest 目前是 4.2.2。

注意版本落差：教材引用的 tutorial paper 寫的是 CPAchecker 3.0，而你拉到的是 4.2.2。基本用法沒變，但如果某個選項對不上，那是版本差異，不是你做錯。

2 第一次執行：一支安全的程式

開一個工作目錄，因為 CPAchecker 會把結果寫進當前目錄的 output/：

mkdir cpa-test && cd cpa-test

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker /cpachecker/doc/examples/example.c

最後幾行會是：

Verification result: TRUE. No property violation found by chosen configuration.
More details ... in the directory "./output".
Graphical representation included in the file "./output/Report.html".

-v "$PWD":/workdir 把當前目錄掛進容器；-u "$(id -u):$(id -g)" 讓產出的檔案屬於你而不是 root（少了它，output/ 會變成 root 所有，之後刪不掉）。

TRUE 的意思：在這個設定下沒有找到違反。注意那句 by chosen configuration——換一個設定可能有不同結果，這正是 SV 2 和 SV 3 在講的事。

3 讓它找到一個真的 bug

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker /cpachecker/doc/examples/example_bug.c

Verification result: FALSE. Property violation (assertion in line 39:
Condition "There are 5 or more non-prime numbers between 2 and 100"
failed in "example_bug.c", line 39) found by chosen configuration.
Graphical representation included in the file "./output/Counterexample.1.html".

它不只說「有錯」，還指到第 39 行，並且產生一份反例。

用瀏覽器打開 output/Counterexample.1.html——那是一份互動式報告，可以順著錯誤路徑一步一步看變數怎麼變成違反條件的值。

4 這一步最重要：把產出對回教材

跑完之後 ls output/，你會看到一堆檔案。其中幾個就是教材裡那些名詞的實體：

產出的檔案	教材裡哪一段講的
`cfa.dot`	control-flow automaton —— 程式被畫成的那張圖
`ARG.dot`	abstract reachability graph —— 探索過程的紀錄
`ARGRefinements.dot`	CEGAR 每一輪 refinement 做了什麼
`abstractions.txt`	predicate abstraction 在每個位置算出來的東西
`Counterexample.1.c`	那條走得通的錯誤路徑，被抽成一支程式

.dot 是 Graphviz 格式，可以轉成圖：

# 容器裡沒有 graphviz，用你自己機器上的（沒裝就 apt install graphviz / brew install graphviz）
dot -Tpng output/cfa.dot -o cfa.png
dot -Tpng output/ARG.dot -o arg.png

打開 cfa.png 對照教材 0.11 節那張「程式的圖」，打開 arg.png 對照 ARG 那一段。 這一步做完，那些詞就不再是定義了。

5 換分析，看差別

預設設定其實是同時跑好幾個分析、誰先成功就用誰。你在第 2 節的輸出裡應該看得到這些字眼：

parallel-IMC.properties            ← interpolation-based model checking
parallel-valueAnalysis-Cegar       ← CEGAR
parallel-dataFlow                  ← data-flow analysis
LoopBoundCPA                       ← 迴圈次數上限，BMC 靠它實現「有界」
Adjusting maxLoopIterations to 2   ← 那個 k 值正在被調整

教材裡的名詞，有一半直接印在螢幕上。

指定單一設定的寫法：

# predicate abstraction（SV 1 那一篇的做法）
docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker -predicateAnalysis /cpachecker/doc/examples/example.c

# BMC：把迴圈展開固定圈數
docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker -config config/bmc.properties /cpachecker/doc/examples/example.c

config/ 底下有 245 個設定檔。跟教材相關的幾個：

設定檔	對應
`predicateAnalysis.properties`	SV 1 的 predicate abstraction
`predicateAnalysis-ImpactRefiner-ABEl.properties`	IMPACT 式的 refinement
`bmc.properties`	BMC
`bmc-induction.properties`	k-induction
`bmc-interpolationSequence.properties`	interpolant 序列

值得動手比一比：同一支程式，-predicateAnalysis 跟 -config config/bmc.properties 的輸出差在哪？產生的 output/ 檔案一樣嗎？

6 沒有 Docker 的路（macOS 特別看這裡）

CPAchecker 預設用的 SMT solver 是編譯過的二進位檔，而官方不提供 macOS 版——所以在 Mac 上很多分析跑不起來。

解法是改用 SMTInterpol，它是純 Java 寫的，沒有原生依賴：

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker -predicateAnalysis-linear \
  -setprop solver.solver=SMTInterpol /cpachecker/doc/examples/example.c

實測輸出：

Using predicate analysis with SMTInterpol 2.5-1242-g5c50fb6d and JFactory 1.21.
Using refinement ... PredicateAbstractionRefinementStrategy
Verification result: TRUE.

沒有載入任何原生 solver。這個組合也可以直接用在本機安裝的 CPAchecker 上（下載 release、裝 JDK 21、跑 bin/cpachecker），不需要容器。

代價是 SMTInterpol 比 MathSAT 慢、支援的理論也少一些，所以設定名字裡有 linear——只處理線性算術。但對這幾支範例程式綽綽有餘，而且它支援 interpolation，正好是 SV 1 那篇的核心。

7 可以自己玩的東西

映像檔裡有 12 支範例，涵蓋不同性質：

docker run --rm --entrypoint /bin/ls sosylab/cpachecker /cpachecker/doc/examples/

example.c                 example_bug.c            example-const.c
example-safe.c            example-unsafe.c         example-sym.c
example-multithread.c     example-nonterminating.c example-terminating.c
example-safe-memsafety.c  example-unsafe-memsafety.c

幾個值得試的方向：

寫一支自己的程式丟進去。最小的例子只要幾行——一個迴圈、一個 assert，看它能不能證明。
故意寫一支它證不出來的。例如迴圈次數依賴輸入、或是需要非線性算術的性質。看它是回 UNKNOWN、逾時、還是誤報。
同一支程式換三種設定（predicateAnalysis / bmc / bmc-induction），比較結果與時間。這是 SV 3 那篇整篇在做的事，只是它做得嚴謹得多。
打開 Counterexample.1.html 順著路徑走一遍，然後回頭看教材裡 CEGAR 的第 4、5、6 步——你會看到那三步的實體。

遇到問題時

output/ 是 root 的、刪不掉 → 少了 -u "$(id -u):$(id -g)"
想看完整記錄 → output/CPALog.txt
分析跑太久 → 預設有 900 秒 CPU 上限，可以用 -timelimit 60s 縮短
想知道某個設定在做什麼 → 設定檔本身就是純文字，docker run --rm --entrypoint /bin/cat sosylab/cpachecker /cpachecker/config/bmc.properties