Quelle  Abs_Int2.thy

(* Author: Tobias Nipkow *)

subsection "Backward Analysis of Expressions"

theory Abs_Int2
imports Abs_Int1
begin

instantiation prod :: (order,order) order
begin

definition "less_eq_prod p1 p2 = (fst p1 ≤ fst p2 ∧ snd p1 ≤ snd p2)"
definition "less_prod p1 p2 = (p1 ≤ p2 ∧ ¬ p2 ≤ (p1::'a*'b))"

instance
proof (standard, goal_cases)
  case 1 show ?case by(rule less_prod_def)
next
  case 2 show ?case by(simp add: less_eq_prod_def)
next
  case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
next
  case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
qed

end


subsubsection "Extended Framework"

subclass (in bounded_lattice) semilattice_sup_top ..

locale Val_lattice_gamma = Gamma_semilattice where γ = γ
  for γ :: "'av::bounded_lattice ==> val set" +
assumes inter_gamma_subset_gamma_inf:
  "γ a1 ∩ γ a2 ⊆ γ(a1 ⊓ a2)"
and gamma_bot[simp]: "γ ⊥ = {}"
begin

lemma in_gamma_inf: "x ∈ γ a1 ==> x ∈ γ a2 ==> x ∈ γ(a1 ⊓ a2)"
by (metis IntI inter_gamma_subset_gamma_inf subsetD)

lemma gamma_inf: "γ(a1 ⊓ a2) = γ a1 ∩ γ a2"
by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
  (metis inf_le1 inf_le2 le_inf_iff mono_gamma)

end


locale Val_inv = Val_lattice_gamma where γ = γ
   for γ :: "'av::bounded_lattice ==> val set" +
fixes test_num' :: "val ==> 'av ==> bool"
and inv_plus' :: "'av ==> 'av ==> 'av ==> 'av * 'av"
and inv_less' :: "bool ==> 'av ==> 'av ==> 'av * 'av"
assumes test_num': "test_num' i a = (i ∈ γ a)"
and inv_plus': "inv_plus' a a1 a2 = (a₁',a₂') ==>
  i1 ∈ γ a1 ==> i2 ∈ γ a2 ==> i1+i2 ∈ γ a ==> i1 ∈ γ a₁' ∧ i2 ∈ γ a₂'"
and inv_less': "inv_less' (i1<i2) a1 a2 = (a₁',a₂') ==>
  i1 ∈ γ a1 ==> i2 ∈ γ a2 ==> i1 ∈ γ a₁' ∧ i2 ∈ γ a₂'"


locale Abs_Int_inv = Val_inv where γ = γ
  for γ :: "'av::bounded_lattice ==> val set"
begin

lemma in_gamma_sup_UpI:
  "s ∈ γ_o S1 ∨ s ∈ γ_o S2 ==> s ∈ γ_o(S1 ⊔ S2)"
by (metis (opaque_lifting, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)

fun aval'' :: "aexp ==> 'av st option ==> 'av" where
"aval'' e None = ⊥" |
"aval'' e (Some S) = aval' e S"

lemma aval''_correct: "s ∈ γ_o S ==> aval a s ∈ γ(aval'' a S)"
by(cases S)(auto simp add: aval'_correct split: option.splits)

subsubsection "Backward analysis"

fun inv_aval' :: "aexp ==> 'av ==> 'av st option ==> 'av st option" where
"inv_aval' (N n) a S = (if test_num' n a then S else None)" |
"inv_aval' (V x) a S = (case S of None ==> None | Some S ==>
  let a' = fun S x ⊓ a in
  if a' = ⊥ then None else Some(update S x a'))" |
"inv_aval' (Plus e1 e2) a S =
 (let (a1,a2) = inv_plus' a (aval'' e1 S) (aval'' e2 S)
  in inv_aval' e1 a1 (inv_aval' e2 a2 S))"

text‹The test for const‹bot› in the const‹V›-case is important: const‹bot› indicates that a variable has no possible values, i.e.\ that the current
  point is unreachable. But then the abstract state should collapse to
 const‹None›. Put differently, we maintain the invariant that in an abstract
  of the form term‹Some s›, all variables are mapped to non-const‹bot› values. Otherwise the (pointwise) sup of two abstract states, one of
  contains const‹bot› values, may produce too large a result, thus
  the analysis less precise.›


fun inv_bval' :: "bexp ==> bool ==> 'av st option ==> 'av st option" where
"inv_bval' (Bc v) res S = (if v=res then S else None)" |
"inv_bval' (Not b) res S = inv_bval' b (¬ res) S" |
"inv_bval' (And b1 b2) res S =
  (if res then inv_bval' b1 True (inv_bval' b2 True S)
   else inv_bval' b1 False S ⊔ inv_bval' b2 False S)" |
"inv_bval' (Less e1 e2) res S =
  (let (a1,a2) = inv_less' res (aval'' e1 S) (aval'' e2 S)
   in inv_aval' e1 a1 (inv_aval' e2 a2 S))"

lemma inv_aval'_correct: "s ∈ γ_o S ==> aval e s ∈ γ a ==> s ∈ γ_o (inv_aval' e a S)"
proof(induction e arbitrary: a S)
  case N thus ?case by simp (metis test_num')
next
  case (V x)
  obtain S' where "S = Some S'" and "s ∈ γ_s S'" using ‹s ∈ γ_o S›
    by(auto simp: in_gamma_option_iff)
  moreover hence "s x ∈ γ (fun S' x)"
    by(simp add: γ_st_def)
  moreover have "s x ∈ γ a" using V(2) by simp
  ultimately show ?case
    by(simp add: Let_def γ_st_def)
      (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
next
  case (Plus e1 e2) thus ?case
    using inv_plus'[OF _ aval''_correct aval''_correct]
    by (auto split: prod.split)
qed

lemma inv_bval'_correct: "s ∈ γ_o S ==> bv = bval b s ==> s ∈ γ_o(inv_bval' b bv S)"
proof(induction b arbitrary: S bv)
  case Bc thus ?case by simp
next
  case (Not b) thus ?case by simp
next
  case (And b1 b2) thus ?case
    by simp (metis And(1) And(2) in_gamma_sup_UpI)
next
  case (Less e1 e2) thus ?case
    apply hypsubst_thin
    apply (auto split: prod.split)
    apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
    done
qed

definition "step' = Step
  (λx e S. case S of None ==> None | Some S ==> Some(update S x (aval' e S)))
  (λb S. inv_bval' b True S)"

definition AI :: "com ==> 'av st option acom option" where
"AI c = pfp (step' ⊤) (bot c)"

lemma strip_step'[simp]: "strip(step' S c) = strip c"
by(simp add: step'_def)

lemma top_on_inv_aval': "[ top_on_opt S X; vars e ⊆ -X ] ==> top_on_opt (inv_aval' e a S) X"
by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)

lemma top_on_inv_bval': "[top_on_opt S X; vars b ⊆ -X] ==> top_on_opt (inv_bval' b r S) X"
by(induction b arbitrary: r S) (auto simp: top_on_inv_aval' top_on_sup split: prod.split)

lemma top_on_step': "top_on_acom C (- vars C) ==> top_on_acom (step' ⊤ C) (- vars C)"
unfolding step'_def
by(rule top_on_Step)
  (auto simp add: top_on_top top_on_inv_bval' split: option.split)

subsubsection "Correctness"

lemma step_step': "step (γ_o S) (γ_c C) ≤ γ_c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
  (auto simp: intro!: aval'_correct inv_bval'_correct in_gamma_update split: option.splits)

lemma AI_correct: "AI c = Some C ==> CS c ≤ γ_c C"
proof(simp add: CS_def AI_def)
  assume 1: "pfp (step' ⊤) (bot c) = Some C"
  have pfp': "step' ⊤ C ≤ C" by(rule pfp_pfp[OF 1])
  have 2: "step (γ_o ⊤) (γ_c C) ≤ γ_c C"  ― ‹transfer the pfp'›
  proof(rule order_trans)
    show "step (γ_o ⊤) (γ_c C) ≤ γ_c (step' ⊤ C)" by(rule step_step')
    show "... ≤ γ_c C" by (metis mono_gamma_c[OF pfp'])
  qed
  have 3: "strip (γ_c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
  have "lfp c (step (γ_o ⊤)) ≤ γ_c C"
    by(rule lfp_lowerbound[simplified,where f="step (γ_o ⊤)", OF 3 2])
  thus "lfp c (step UNIV) ≤ γ_c C" by simp
qed

end


subsubsection "Monotonicity"

locale Abs_Int_inv_mono = Abs_Int_inv +
assumes mono_plus': "a1 ≤ b1 ==> a2 ≤ b2 ==> plus' a1 a2 ≤ plus' b1 b2"
and mono_inv_plus': "a1 ≤ b1 ==> a2 ≤ b2 ==> r ≤ r' ==>
  inv_plus' r a1 a2 ≤ inv_plus' r' b1 b2"
and mono_inv_less': "a1 ≤ b1 ==> a2 ≤ b2 ==>
  inv_less' bv a1 a2 ≤ inv_less' bv b1 b2"
begin

lemma mono_aval':
  "S1 ≤ S2 ==> aval' e S1 ≤ aval' e S2"
by(induction e) (auto simp: mono_plus' mono_fun)

lemma mono_aval'':
  "S1 ≤ S2 ==> aval'' e S1 ≤ aval'' e S2"
apply(cases S1)
 apply simp
apply(cases S2)
 apply simp
by (simp add: mono_aval')

lemma mono_inv_aval': "r1 ≤ r2 ==> S1 ≤ S2 ==> inv_aval' e r1 S1 ≤ inv_aval' e r2 S2"
apply(induction e arbitrary: r1 r2 S1 S2)
   apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
   apply (metis mono_gamma subsetD)
  apply (metis le_bot inf_mono le_st_iff)
 apply (metis inf_mono mono_update le_st_iff)
apply(metis mono_aval'' mono_inv_plus'[simplified less_eq_prod_def] fst_conv snd_conv)
done

lemma mono_inv_bval': "S1 ≤ S2 ==> inv_bval' b bv S1 ≤ inv_bval' b bv S2"
apply(induction b arbitrary: bv S1 S2)
   apply(simp)
  apply(simp)
 apply simp
 apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2])
apply (simp split: prod.splits)
apply(metis mono_aval'' mono_inv_aval' mono_inv_less'[simplified less_eq_prod_def] fst_conv snd_conv)
done

theorem mono_step': "S1 ≤ S2 ==> C1 ≤ C2 ==> step' S1 C1 ≤ step' S2 C2"
unfolding step'_def
by(rule mono2_Step) (auto simp: mono_aval' mono_inv_bval' split: option.split)

lemma mono_step'_top: "C1 ≤ C2 ==> step' ⊤ C1 ≤ step' ⊤ C2"
by (metis mono_step' order_refl)

end

end