操作系统形式化验证实践教程(7) - C代码的自动验证
上一节教程不知道大家看晕了没有，其实虽然细节很多还没有讲清楚，但是从结构上大家可以看到，其实是很模式化的工作。
那么能不能让这个模式化的工作自动化起来，也能降低一点入门的学习门槛？这时就该AutoCorres工具出马了。
AutoCorres
既然回到人间，不用再看着一排的simp, vcg之类的，咱们的难度又回到第一讲加减法的时代。
先实现一个C语言实现加法的函数：
unsigned int plus(unsigned int a, unsigned int b)
{
return a + b;
}
下面开始写HOL，先引入AutoCorres：
imports
"AutoCorres.AutoCorres"
然后还是把C源文件读进来，并且install了：
external_file "plus.c"
install_C_file "plus.c"
然后给c文件autocorres一下：
autocorres "plus.c"
按照惯例locale一下：
context plus begin
实际上执行的是：
locale Plus.plus
fixes symbol_table :: "char list ⇒ 32 word"
万事俱备，我们现在已经能读懂C代码了。
通过by eval验证具体例子
先写个case验证下：
lemma "plus' 128 127 = 255"
C代码既然懂了，就直接unfold一下：
unfolding plus'_def
验证对不对，执行一下by eval，完整代码如下：
lemma "plus' 128 127 = 255"
unfolding plus'_def
by eval
演绎验证
例子只能证明在这一种情况下是正确的，但无法证明在所有情况下都正确。我们有没有办法证明所有情况下都正确呢？
可以的，我们不用by eval了，换个apply的规则就好了：
lemma plus_correct: "plus' a b = a + b"
unfolding plus'_def
apply (rule refl)
done
我们来看下目标：
proof (prove)
goal (1 subgoal):
1. a + b = a + b
这真的也没啥可以证的了。。。
自动生成定理和证明
我们乘胜追击，再来搞个最大值的：
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
生成的结果如下：
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
结果如下：
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
这种水平的验证我们暂时还写不出来，大家只要有个概念就好，后面针对常见算法的验证方法我们用到再讲。
网友评论