CPAchecker 上手 — SV 1 程式作業

這一頁的每個指令都在 Linux 上實跑過，而且每個指令後面都貼著它真正的輸出。 你可以逐行對照——對不上就是哪裡不一樣，不用猜。

目標不是把工具學完，是讓教材裡的名詞變成你螢幕上的檔案。

0 你只需要 Docker

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

docker --version

Docker version 29.1.4, build 0e6fee6

版本號不用一樣，有輸出就行。沒有 Docker 就先裝（Linux 用套件管理員，macOS/Windows 用 Docker Desktop）。真的裝不了的話跳到第 7 節，那裡有不用 Docker 的路。

1 拉映像檔

docker pull sosylab/cpachecker:latest

latest: Pulling from sosylab/cpachecker
Digest: sha256:7dfa00e322323134f4e83e6ae1ff364439f826e851e7e9b6357ae396303ca4c3
Status: Image is up to date for sosylab/cpachecker:latest
docker.io/sosylab/cpachecker:latest

第一次拉會多出一大段層層下載的進度，跑完才變成上面這樣。下載量約 351 MB，但解開後佔的空間是 1.16 GB：

docker images sosylab/cpachecker --format '{{.Repository}}:{{.Tag}}   {{.Size}}'

sosylab/cpachecker:latest   1.16GB

確認版本：

docker run --rm sosylab/cpachecker --version

CPAchecker 4.2.2 (OpenJDK 64-Bit Server VM 21.0.11)

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

2 先講輸出怎麼看，不然你會被淹沒

這一節看似囉嗦，但省下來的時間最多。

直接跑 CPAchecker，螢幕上會捲過幾十行這種東西：

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)
CPAchecker 4.2.2 / default (OpenJDK 64-Bit Server VM 21.0.11) started (CPAchecker.run, INFO)
Parsing CFA from file(s) "/cpachecker/doc/examples/example.c" (CPAchecker.parse, INFO)
...（還有三十幾行）

那些全部在 stderr。 真正的結果在 stdout，而且永遠只有五行：

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

Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

前兩行永遠一樣（heap 與 stack 的預設值），第三行才是答案，後兩行告訴你產出在哪。

這也解釋了兩件會讓人停下來的事：

• 有時會多一行 Warning: Could not write refinement graph to file (Stream closed)，實測十次出現五次。預設是好幾個分析在賽跑，誰先贏就取消其他人，被取消的那個來不及把圖寫完。它在 stderr，加了 2>/dev/null 就不會看到，而且不影響結果。
• 那行 warning 出現的位置每次不同。stderr 與 stdout 是兩條獨立的流，交錯順序不保證。

本頁接下來每個 CPAchecker 指令都加 2>/dev/null，這樣你看到的就跟這裡貼的一模一樣。想看完整過程時把它拿掉，或去讀 output/CPALog.txt。

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

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

mkdir -p cpa-test && cd cpa-test

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

Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found 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 在講的事。

看看產出了什麼：

ls -1 output/

abstractions.txt      ARG.dot               ARGRefinements.dot    ARGSimplified.dot
cfa                   cfa.dot               coverage.info         CPALog.txt
functionCalls.dot     functionCallsUsed.dot invariantPrecs.txt    invariants.txt
predmap.txt           Report.html           Statistics.txt        UsedConfiguration.properties
VariableClassification.log                  VariableTypeMapping.txt
witness-2.0.yml

（實際是每行一個，這裡排成多欄省版面。檔案數會因為贏的是哪個平行分析而略有出入。）

4 讓它找到一個真的 bug

mkdir -p ../bug-test && cd ../bug-test

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

Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
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.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Counterexample.1.html".

三個地方跟上一節不同：結果是 FALSE、指出了第 39 行、最後一行指向 Counterexample.1.html 而不是 Report.html。

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

這一跑的產出多了一整組反例檔案：

ls -1 output/ | grep Counterexample

Counterexample.1.c
Counterexample.1.core.txt
Counterexample.1.dot
Counterexample.1.graphml.gz
Counterexample.1.html
Counterexample.1.spc
Counterexample.1.txt
Counterexample.1.witness-2.0.yml
Counterexample.1.witness.dot.gz

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

用第 4 節那一跑的 output/——第 3 節那支是安全的，不會有反例檔。

predmap.txt 值得特別看一眼，它是這篇論文結論的實體：

head -6 output/predmap.txt

(declare-fun |main::nonprimesCount| () (_ BitVec 32))

main:
(assert (let ((.def_170 (bvslt |main::nonprimesCount| (_ bv5 32)))).def_170))

main N5:

整份檔案 16 行。看得懂的部分是：CPAchecker 決定要追蹤的 predicate 是 nonprimesCount < 5（bvslt 是 32 位元有號小於），而且它列出了哪些位置要追蹤這個 predicate（main:、main N5: …）。

那個「哪個 predicate、在哪個位置」的表，就是論文的 $\Pi$。 論文花了十三頁在講怎麼把它算出來，而它在你的硬碟上是一個 16 行的文字檔。

.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
ls -lh cfa.png arg.png

-rw-rw-r-- 1 you you 2.3M Aug 19 02:45 arg.png
-rw-rw-r-- 1 you you 326K Aug 19 02:45 cfa.png

dot 成功時不印任何東西，所以要用 ls 確認檔案真的生出來了。ARG 的圖比 CFA 大得多（2.3M 對 326K），那個大小差本身就說明了「探索過程」比「程式結構」複雜多少。

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

6 換分析，看差別

config/ 最上層有 227 個設定檔（連子目錄一起算是 841 個）。跟教材相關的幾個：

6.1 predicate abstraction

mkdir -p ../pred-test && cd ../pred-test

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker --config /cpachecker/config/predicateAnalysis.properties \
  /cpachecker/doc/examples/example.c 2>/dev/null

Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

參數語法：CPAchecker 4.x 用雙破折號，而且新舊不能混用（混了會直接被拒絕）。 另外 --config 的路徑是相對於工作目錄，而設定檔在容器裡，所以要寫絕對路徑 /cpachecker/config/...。

6.2 BMC，以及一句很值得注意的話

mkdir -p ../bmc-test && cd ../bmc-test

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker --config /cpachecker/config/bmc.properties \
  /cpachecker/doc/examples/example.c 2>/dev/null

Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Verification result: UNKNOWN, incomplete analysis.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

同一支程式，predicate abstraction 說 TRUE，BMC 說 UNKNOWN。

理由在 stderr 那一行：

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker --config /cpachecker/config/bmc.properties \
  /cpachecker/doc/examples/example.c 2>&1 1>/dev/null | grep "Analysis incomplete"

Analysis incomplete: no errors found, but not everything could be checked. (CPAchecker.analyzeResult, WARNING)

BMC 只展開固定圈數，所以它能說的只有「在這個界限內沒找到錯」——不能說「永遠沒錯」。這正是教材裡 BMC 的先天限制，而工具老實地把它印在結論裡。SV 3 的走查題會讓你自己寫出那條展開公式，親眼看到圈數一改判定就翻面。

6.3 比較兩者的產出——這裡有教材看不到的東西

diff <(ls -1 ../pred-test/output/) <(ls -1 output/)

3d2
< ARGRefinements.dot
12,14d10
< invariantPrecs.txt
< invariants.txt
< predmap.txt

BMC 少了四個檔案，其中三個是關鍵：ARGRefinements.dot（沒有 refinement）、predmap.txt（沒有每位置的 predicate 表）、invariants.txt。因為 BMC 根本不做 CEGAR。

但更值得看的是兩邊都有的那個 abstractions.txt：

cat output/abstractions.txt

0 () @1:
(assert true)

head -4 ../pred-test/output/abstractions.txt

(declare-fun |main::a| () (_ BitVec 32))
(declare-fun |main::i| () (_ BitVec 32))

0 (4) @1:

同一個檔名，一個 26 bytes 只有 (assert true)、一個是一整串真正算出來的 predicate。 那就是「有沒有在做 abstraction」攤在檔案裡給你看。

值得動手比一比：把 bmc-induction.properties 也跑一次。實測它在這支程式上回 TRUE——k-induction 補上了 BMC 缺的那一半。

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

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

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

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker --config /cpachecker/config/predicateAnalysis-linear.properties \
  --option solver.solver=SMTInterpol /cpachecker/doc/examples/example.c 2>/dev/null

Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

確認它真的用了 SMTInterpol（這兩行在 stderr）：

docker run --rm -v "$PWD":/workdir -u "$(id -u):$(id -g)" \
  sosylab/cpachecker --config /cpachecker/config/predicateAnalysis-linear.properties \
  --option solver.solver=SMTInterpol /cpachecker/doc/examples/example.c 2>&1 1>/dev/null \
  | grep -E "SMTInterpol|refinement for predicate"

Using predicate analysis with SMTInterpol 2.5-1242-g5c50fb6d and JFactory 1.21. (...)
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (...)

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

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

這一節是唯一我沒能在 macOS 上實跑的。 上面的輸出是 Linux 上跑出來的，而 macOS 特有的行為（Docker Desktop、brew install graphviz、本機安裝）只有間接證據：映像檔的 lib/native 底下只有 x86_64-linux，而官方 README 明文寫 macOS 不提供 SMT solver 二進位檔，並建議完全相同的 SMTInterpol 組合。在 Mac 上跑不出這個結果的話，請告訴我。

8 可以自己玩的東西

映像檔裡有 11 支 C 範例：

docker run --rm --entrypoint /bin/sh sosylab/cpachecker \
  -c 'ls -1 /cpachecker/doc/examples/*.c'

/cpachecker/doc/examples/example_bug.c
/cpachecker/doc/examples/example.c
/cpachecker/doc/examples/example-const.c
/cpachecker/doc/examples/example-multithread.c
/cpachecker/doc/examples/example-nonterminating.c
/cpachecker/doc/examples/example-safe.c
/cpachecker/doc/examples/example-safe-memsafety.c
/cpachecker/doc/examples/example-sym.c
/cpachecker/doc/examples/example-terminating.c
/cpachecker/doc/examples/example-unsafe.c
/cpachecker/doc/examples/example-unsafe-memsafety.c

（直接 ls 那個目錄還會列出 .xml、.sh、predmap.txt 等四個非範例檔，所以這裡只挑 .c。）

幾個值得試的方向：

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

遇到問題時