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

MoXIchecker 上手 — SV 3 程式作業

這一頁每個指令與每個數字都實跑過。這份作業的核心只有一件事：拿同一個模型，換不同的演算法跑，看它們在什麼情況下有結論、什麼情況下沒有——那正是 SV 3 那篇論文整篇在做的事，只是它做得嚴謹得多。

0 這個工具在整條鏈的哪裡

MoXIchecker 檢查的不是 C 程式，而是 MoXI（Model eXchange Interlingua）——一種中介的模型描述語言。輸入是 JSON 格式的 MoXI 模型，輸出是「query 可達 / 不可達」。

MoXI 模型 (JSON) ─→ 公式抽取 ─→ init / trans / inv / query (PySMT 公式) ─→ 檢查引擎 ─→ 判定

它是 Python 寫的，架構刻意做得容易塞進新演算法——所以它剛好是拿來比較演算法的好平台。

1 安裝

需要 Python 3.10 以上。用容器最乾淨，不會弄髒系統的 Python：

git clone https://gitlab.com/sosy-lab/software/moxichecker.git
cd moxichecker
mkdir -p .container-home

docker run --rm -it -v "$PWD":/work -w /work -u "$(id -u):$(id -g)" \
  -e HOME=/work/.container-home \
  -e PATH=/work/.container-home/.local/bin:/usr/local/bin:/usr/bin:/bin \
  python:3.12 bash

進到容器裡之後：

pip install --user setuptools pysmt==0.9.7.dev333
pysmt-install --z3 --confirm-agreement
pysmt-install --check      # 應該看到 z3 True

把 HOME 指到掛載進來的 .container-home，套件就裝在專案目錄裡——下次進容器不用重裝。

不想用容器的話，python3 -m venv 也行，指令一樣。官方另外推薦 MathSAT（--msat），它比 z3 適合某些理論，但 z3 對這些範例已經夠用。

2 第一次執行

./bin/moxichecker examples/QF_ABV/count2.moxi.json

[INFO] Checking reachability of query 'rch_1' of system 'main'
[INFO] Used theory: QF_ABV
[INFO] Query reached at step 7
[INFO] Model-checking result: REACHABLE

三個資訊：檢查的是哪個 query、用了哪個理論、第幾步到達。

REACHABLE 表示那個 query 條件真的會發生。如果 query 描述的是「壞事」，REACHABLE 就等於找到 bug。

3 核心實驗：同一個模型，換演算法

這是這份作業真正要你做的事。

MoXIchecker 內建三種演算法：

./bin/moxichecker -m bmc   <file>    # bounded model checking
./bin/moxichecker -m kind  <file>    # k-induction（預設）
./bin/moxichecker -m pdr   <file>    # property-directed reachability

範例目錄裡有成對的模型，同一個系統、性質相反：

examples/QF_LIA/IntCounter_reach.moxi.json      ← 性質會被違反
examples/QF_LIA/IntCounter_unreach.moxi.json    ← 性質永遠成立

先自己預測：哪一種演算法在哪一種模型上會有結論？想好再往下。

實測結果（每個限時 45 秒）：

模型bmckindpdr
IntCounter_reach（第 5 步可達）415ms 找到430ms 找到逾時
IntCounter_unreach（永遠不可達）逾時，沒有結論420ms 證明 UNREACHABLE逾時

這張表就是 SV 3 §0.3 那句話的實驗版本：

BMC 只能說「$k$ 步之內沒事」，不能說「永遠沒事」。要證明程式完全正確，BMC 不夠。

IntCounter_unreach 這一格為什麼逾時？因為 BMC 一直展開下去——展 10 步沒事、100 步沒事、1000 步沒事，但它永遠不知道什麼時候可以停。而 k-induction 只要 420 毫秒，因為它證的是「走一步之後還是安全」，不需要展開。

反過來看第一列：找 bug 的時候 BMC 是最快的，而且它給你具體第幾步——那是可以拿去重現的反例。

這正是為什麼要有「統一框架」：這兩個演算法不是誰比較好，是各自擅長不同的問題，而只有把它們放進同一個工具、用同一個 solver，這張表才有意義。

4 換 solver：把變因再固定一次

./bin/moxichecker -s {btor,cvc5,msat,yices,z3} <file>

預設是 z3。要用其他的得先裝：

pysmt-install --msat --confirm-agreement    # MathSAT
pysmt-install --btor --confirm-agreement    # Boolector

值得做的實驗：同一個模型、同一個演算法，只換 solver，時間差多少？

這一步的意義在 SV 3 §0.1 講過——跨論文的效能比較不可靠，因為你分不清差距來自演算法還是來自 solver。現在你可以自己把這個變因固定下來，親眼看看它值多少。

5 兩個 k-induction 的旋鈕

./bin/moxichecker -m kind --no-simple-path <file>   # 關掉 simple-path 約束
./bin/moxichecker -m kind --incr-solving   <file>   # 開啟增量求解

--no-simple-path 特別值得試。k-induction 預設會加上「路徑上不重複經過同一個狀態」的約束，少了它，某些性質會證不出來（或變很慢）。

這對應教材 SV 3 §0.4 那句「很多性質不是 inductive 的」——simple-path 約束就是把歸納假設加強的方法之一。

6 換一個理論

範例按 SMT 理論分類：

examples/QF_ABV/   陣列 + 位元向量      4 個
examples/QF_LIA/   線性整數算術         8 個
examples/QF_LRA/   線性實數算術         2 個
examples/QF_NIA/   非線性整數算術       3 個
examples/QF_NRA/   非線性實數算術       4 個

非線性的那些值得特別看（QF_NIA / QF_NRA）。非線性算術的可判定性比線性差很多，所以同一個演算法在那裡的表現會明顯不同。試著把 QF_NIA 的例子跑一遍，看有幾個能在時限內得到結論。

7 作業建議

  1. 把第 3 節那張表自己跑出來，加上 QF_ABV 和 QF_NIA 各一組 reach/unreach，看結論是否一致。
  2. 挑一個逾時的組合，加大時限（例如 300 秒）看它是真的算不完，還是只是慢。
  3. 寫一句話回答：如果你只能在專案裡放一個演算法，你選哪個？在什麼前提下？
  4. 進階：讀 moxichecker/model_checking.py，那三個演算法的實作各只有幾十行——對照教材 SV 3 的四法對照表，看程式碼跟論文的描述對不對得上。

遇到問題時