Theory Abs_Int2

(* Author: Tobias Nipkow *)

subsection "Backward Analysis of Expressions"

theory Abs_Int2
imports Abs_Int1

instantiation prod :: (order,order) order

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))"

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


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]: "γ  = {}"

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)


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 = (a1',a2') 
  i1  γ a1  i2  γ a2  i1+i2  γ a  i1  γ a1'  i2  γ a2'"
and inv_less': "inv_less' (i1<i2) a1 a2 = (a1',a2') 
  i1  γ a1  i2  γ a2  i1  γ a1'  i2  γ a2'"

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

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 constbot in the constV-case is important: constbot indicates that a variable has no possible values, i.e.\ that the current
program point is unreachable. But then the abstract state should collapse to
constNone. Put differently, we maintain the invariant that in an abstract
state of the form termSome s, all variables are mapped to non-constbot values. Otherwise the (pointwise) sup of two abstract states, one of
which contains constbot values, may produce too large a result, thus
making 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')
  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)
  case (Plus e1 e2) thus ?case
    using inv_plus'[OF _ aval''_correct aval''_correct]
    by (auto split: prod.split)

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
  case (Not b) thus ?case by simp
  case (And b1 b2) thus ?case
    by simp (metis And(1) And(2) in_gamma_sup_UpI)
  case (Less e1 e2) thus ?case
    apply hypsubst_thin
    apply (auto split: prod.split)
    apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')

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'])
  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


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"

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)

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(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)

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)