操作系統形式化驗證實踐教學(7) - C程式碼的自動驗證
上一節教學不知道大家看暈了沒有，其實雖然細節很多還沒有講清楚，但是從結構上大家可以看到，其實是很模式化的工作。
那麼能不能讓這個模式化的工作自動化起來，也能降低一點入門的學習門檻？這時就該AutoCorres工具出馬了。
AutoCorres
既然回到人間，不用再看着一排的simp, vcg之類的，咱們的難度又回到第一講加減法的時代。
先實現一個C語言實現加法的函數：
unsigned int plus(unsigned int a, unsigned int b)
{
return a + b;
}
1
2
3
4
下面 下麪開始寫HOL，先引入AutoCorres：
imports
「AutoCorres.AutoCorres」
1
2
然後還是把C原始檔讀進來，並且install了：
external_file 「plus.c」
install_C_file 「plus.c」
1
2
然後給c檔案autocorres一下：
autocorres 「plus.c」
1
按照慣例locale一下：
context plus begin
1
實際上執行的是：
locale Plus.plus
fixes symbol_table :: 「char list ⇒ 32 word」
1
2
萬事俱備，我們現在已經能讀懂C程式碼了。
通過by eval驗證具體例子
先寫個case驗證下：
lemma 「plus’ 128 127 = 255」
1
C程式碼既然懂了，就直接unfold一下：
unfolding plus’_def
1
驗證對不對，執行一下by eval，完整程式碼如下：
lemma 「plus’ 128 127 = 255」
unfolding plus’_def
by eval
1
2
3
演繹驗證
例子只能證明在這一種情況下是正確的，但無法證明在所有情況下都正確。我們有沒有辦法證明所有情況下都正確呢？
可以的，我們不用by eval了，換個apply的規則就好了：
lemma plus_correct: 「plus’ a b = a + b」
unfolding plus’_def
apply (rule refl)
done
我們來看下目標：
proof (prove)
goal (1 subgoal):
這真的也沒啥可以證的了。。。
自動生成定理和證明
我們乘勝追擊，再來搞個最大值的：
unsigned max(unsigned a, unsigned b)
{
if (a <= b) {
return b;
}
return a;
}
後面沒啥驚喜的，一條龍：imports AutoCorres, external_file, install_C_file, autocorres, unfolding:
imports
「AutoCorres.AutoCorres」
begin
external_file 「simple.c」
install_C_file 「simple.c」
autocorres 「simple.c」
context simple begin
lemma 「max’ a b = max a b」
unfolding max’_def max_def
by (rule refl)
下面 下麪我們來個更強大的，自動生成定理和證明：
thm simple.max’_def simple.max’_ac_corres
1
生成的結果如下：
simple.max’ ?a ?b ≡ if ?a ≤ ?b then ?b else ?a
ac_corres (simple.lift_global_heap ∘ globals) True
simple_global_addresses.Γ ret__unsigned_’
((λs. a_’ s = ?a’) and (λs. b_’ s = ?b’) and
(λx. abs_var ?a id ?a’ ∧ abs_var ?b id ?b’) ∘
simple.lift_global_heap ∘
globals)
(L2_gets (λ_. simple.max’ ?a ?b) [’‘ret’’])
(Call max_'proc)
雖然autocorres不會知道max跟庫中的max有啥關係，但是可以生成if ?a ≤ ?b then ?b else ?a這樣的定理。
驗證並非是重複程式碼邏輯
剛纔我們看到加法還有最大值，已經都被autocorres輕鬆消解掉了，連定理和證明都可以自動生成了。
但是，實際上，形式化驗證並沒有這麼簡單。
我們看個求最大公約數的例子：
unsigned gcd(unsigned a, unsigned b)
{
unsigned c;
while (a != 0) {
c = a;
a = b % a;
b = c;
}
return b;
}
這個如何驗證？
自動生成下：
thm simple.gcd’_def simple.gcd’_ac_corres
1
結果如下：
simple.gcd’ ?a ?b ≡
do (a, b) <- whileLoop (λ(a, b) b. a ≠ 0)
(λ(a, b). return (b mod a, a))
(?a, ?b);
return b
od
ac_corres (simple.lift_global_heap ∘ globals) True
simple_global_addresses.Γ (unat ∘ ret__unsigned_’)
((λs. a_’ s = ?a’) and (λs. b_’ s = ?b’) and
(λx. abs_var ?a unat ?a’ ∧ abs_var ?b unat ?b’) ∘
simple.lift_global_heap ∘
globals)
(liftE (simple.gcd’ ?a ?b)) (Call gcd_'proc)
這重複了下實現邏輯沒錯，但是沒有體驗中最大公約數的本質。
我們來看下seL4中的實現吧：
lemma gcd_to_return [simp]:
「gcd’ a b = return (gcd a b)」
apply (subst monad_to_gets [where v=「λ_. gcd a b」])
apply (wp gcd_wp)
apply simp
apply (clarsimp simp: gcd’_def)
apply (rule empty_fail_bind)
apply (rule empty_fail_whileLoop)
apply (clarsimp simp: split_def)
apply (clarsimp simp: split_def)
apply (clarsimp simp: split_def)
done
其中，monad_to_gets是一個輔助定理：
lemma monad_to_gets:
「⟦ ⋀P. ⦃ P ⦄ f ⦃ λr s. P s ∧ r = v s ⦄!; empty_fail f ⟧ ⟹ f = gets v」
apply atomize
apply (monad_eq simp: validNF_def valid_def no_fail_def empty_fail_def)
apply (rule conjI)
apply clarsimp
apply (drule_tac x=「λs’. s = s’」 in spec)
apply clarsimp
apply force
apply clarsimp
apply (drule_tac x=「λs’. s’ = t」 in spec)
apply clarsimp
apply force
done
求最弱前置條件gcd_wp爲：
lemma gcd_wp [wp]:
「⦃ P (gcd a b) ⦄ gcd’ a b ⦃ P ⦄!」
(* Unfold definition of 「gcd’」. *)
apply (unfold gcd’_def)
(* Annoate the loop with an invariant and measure. *)
apply (subst whileLoop_add_inv [where
I=「λ(a’, b’) s. gcd a b = gcd a’ b’ ∧ P (gcd a b) s」
and M=「λ((a’, b’), s). a’」])
(* Solve using weakest-precondition. *)
apply (wp; clarsimp)
apply (metis gcd.commute gcd_red_nat)
using gt_or_eq_0 by fastforce
這種水平的驗證我們暫時還寫不出來，大家只要有個概念就好，後面針對常見演算法的驗證方法我們用到再講。