Theory Very_Busy_Expressions

theory Very_Busy_Expressions imports Available_Expressions begin

― ‹We encode the Very Busy Expressions analysis into Datalog. First we define the analysis, then
    we encode it into Datalog using our Bit-Vector Framework locale. We also prove 
    the encoding correct. ›

section ‹Very Busy Expressions›

definition vbexp_edge_list :: "('n,'v action) edge list ⇒ 'v arith ⇒ bool" where
  "vbexp_edge_list π a = (∃π1 π2 e. π = π1 @ [e] @ π2 ∧ a ∈ aexp_edge e ∧ (∀e' ∈ set π1. fv_arith a ∩ def_edge e' = {}))"

definition vbexp_path :: "'n list × 'v action list ⇒ 'v arith set" where
  "vbexp_path π = {a. vbexp_edge_list (LTS.transition_list π) a}"

locale analysis_VB = finite_program_graph pg 
  for pg :: "('n::finite,'v::finite action) program_graph"
begin

interpretation LTS edges .

definition analysis_dom_VB :: "'v arith set" where
  "analysis_dom_VB = aexp_pg pg"

lemma finite_analysis_dom_VB: "finite analysis_dom_VB"
proof -
  have "finite (⋃ (aexp_edge ` edges))"
    by (metis aexp_edge.elims finite_UN finite_aexp_edge finite_program_graph_axioms 
        finite_program_graph_def)
  then show ?thesis
    unfolding analysis_dom_VB_def edges_def by auto
qed
 
fun kill_set_VB :: "('n,'v action) edge ⇒ 'v arith set" where
  "kill_set_VB (q⇩o, x ::= a, q⇩s) = {a'. x ∈ fv_arith a'}"
| "kill_set_VB (q⇩o, Bool b, q⇩s) = {}"
| "kill_set_VB (v, Skip, vc) = {}"

fun gen_set_VB :: "('n,'v action) edge ⇒ 'v arith set" where
  "gen_set_VB (q⇩o, x ::= a, q⇩s) = ae_arith a"
| "gen_set_VB (q⇩o, Bool b, q⇩s) = ae_boolean b"
| "gen_set_VB (v, Skip, vc) = {}"

definition d_init_VB :: "'v arith set" where
  "d_init_VB = {}"

interpretation bw_must: analysis_BV_backward_must pg analysis_dom_VB kill_set_VB gen_set_VB d_init_VB
  using analysis_VB_axioms analysis_VB_def
  by (metis analysis_BV_backward_must_axioms_def analysis_BV_backward_must_def bot.extremum 
      d_init_VB_def finite_analysis_dom_VB)

lemma aexp_edge_list_S_hat_edge_list: 
  assumes "a ∈ aexp_edge (q, α, q')"
  assumes "fv_arith a ∩ def_edge (q, α, q') = {}"
  shows "a ∈ bw_must.S_hat (q, α, q') R"
  using assms unfolding bw_must.S_hat_def by (cases α) auto

lemma empty_inter_fv_arith_def_edge:
  assumes "vbexp_edge_list (e # π) a"
  shows "fv_arith a ∩ def_edge e = {} ∨ a ∈ aexp_edge e"
proof -
  from assms(1) obtain π1 π2 e' where π1_π2_e'_p:
    "e # π = π1 @ [e'] @ π2"
    "a ∈ aexp_edge e'"
    "(∀e''∈set π1. fv_arith a ∩ def_edge e'' = {})"
    unfolding vbexp_edge_list_def by auto
  from this(1) have "e ∈ set (π1 @ [e'])"
    by (metis append_self_conv2 hd_append2 list.sel(1) list.set_sel(1) snoc_eq_iff_butlast) 
  then have "e ∈ set π1 ∨ e = e'"
    by auto
  then show "fv_arith a ∩ def_edge e = {} ∨ a ∈ aexp_edge e"
  proof
    assume "e ∈ set π1"
    then have "fv_arith a ∩ def_edge e = {}" 
      using π1_π2_e'_p(3) by auto
    then show "fv_arith a ∩ def_edge e = {} ∨ a ∈ aexp_edge e" 
       by auto
  next
    assume "e = e'"
    then have "a ∈ aexp_edge e"
      using π1_π2_e'_p(2) by auto 
    then show "fv_arith a ∩ def_edge e = {}  ∨ a ∈ aexp_edge e"
      by auto 
  qed
qed

lemma vbexp_edge_list_Cons:
  assumes "vbexp_edge_list (e # π) a"
  shows "vbexp_edge_list π a ∨ a ∈ aexp_edge e"
proof -
  from assms(1) obtain π1 π2 e' where π1_π2_e'_p:
    "e # π = π1 @ [e'] @ π2"
    "a ∈ aexp_edge e'"
    "(∀e''∈set π1. fv_arith a ∩ def_edge e'' = {})"
    unfolding vbexp_edge_list_def by auto
  from this(1) have "e ∈ set (π1 @ [e'])"
    by (metis append_assoc hd_append2 list.sel(1) list.set_sel(1) snoc_eq_iff_butlast)
  then have "e = e' ∨ e ∈ set π1"
    by auto
  then show ?thesis
  proof
    assume "e = e'"
    then have "a ∈ aexp_edge e"
      using π1_π2_e'_p by auto
    then show ?thesis 
      by auto
  next
    assume "e ∈ set π1"
    then have "π = tl π1 @ [e'] @ π2"
      using π1_π2_e'_p by (metis equals0D list.sel(3) set_empty tl_append2) 
    moreover
    have "a ∈ aexp_edge e'"
      by (simp add: π1_π2_e'_p(2))
    moreover
    have "(∀e''∈ set (tl π1). fv_arith a ∩ def_edge e'' = {})"
      by (metis π1_π2_e'_p(3) list.set_sel(2) tl_Nil)
    ultimately
    have "vbexp_edge_list π a"
      unfolding vbexp_edge_list_def by metis
    then show ?thesis
      by auto
  qed
qed

lemma gen_set_VB_is_aexp_edge:
  "a ∈ gen_set_VB e ⟷ a ∈ aexp_edge e"
proof -
  obtain q α q' where e_split: "e = (q, α, q')"
    by (cases e)
  then show ?thesis
    by (cases α) auto
qed

lemma empty_inter_fv_arith_def_edge'':
  "a ∉ kill_set_VB e ⟷ fv_arith a ∩ def_edge e = {}"
proof -
  obtain q α q' where e_split: "e = (q, α, q')"
    by (cases e)
  then show ?thesis
    by (cases α) auto
qed

lemma S_hat_edge_list_aexp_edge_list: 
  assumes "a ∈ bw_must.S_hat_edge_list π d_init_VB"
  shows "vbexp_edge_list π a"
  using assms
proof (induction π)
  case Nil
  then show ?case 
    unfolding d_init_VB_def by auto
next
  case (Cons e π)
  from Cons(2) have "a ∈ (bw_must.S_hat_edge_list π d_init_VB - kill_set_VB e) ∨ a ∈ gen_set_VB e"
    using bw_must.S_hat_def by auto
  then show ?case
  proof 
    assume a_S_hat: "a ∈ bw_must.S_hat_edge_list π d_init_VB - kill_set_VB e"
    then have "vbexp_edge_list π a"
      using Cons by auto
    moreover
    from a_S_hat have "a ∉ kill_set_VB e"
      by auto
    then have "fv_arith a ∩ def_edge e = {}"
      using empty_inter_fv_arith_def_edge'' by auto
    ultimately show "vbexp_edge_list (e # π) a"
      unfolding vbexp_edge_list_def by (metis Cons_eq_appendI set_ConsD)
  next
    assume a_gen: "a ∈ gen_set_VB e"
    then have "a ∈ aexp_edge e"
      using gen_set_VB_is_aexp_edge by auto
    then show "vbexp_edge_list (e # π) a"
      unfolding vbexp_edge_list_def by (metis append_Cons append_Nil empty_iff empty_set)
  qed
qed

lemma aexp_edge_list_S_hat_edge_list': 
  assumes "vbexp_edge_list π a"
  shows "a ∈ bw_must.S_hat_edge_list π d_init_VB"
  using assms
proof (induction π)
  case Nil
  then have False 
    unfolding vbexp_edge_list_def by auto
  then show ?case
    by metis
next
  case (Cons e π)
  have fvae: "fv_arith a ∩ def_edge e = {} ∨ a ∈ aexp_edge e"
    using Cons(2) empty_inter_fv_arith_def_edge by force

  have "vbexp_edge_list π a ∨ a ∈ aexp_edge e"
    using Cons(2)
    by (simp add: vbexp_edge_list_Cons)
  then show ?case
  proof
    assume "vbexp_edge_list π a"
    then have "a ∈ bw_must.S_hat_edge_list π d_init_VB"
      using Cons by auto
    moreover
    have "a ∉ kill_set_VB e ∨ a ∈ gen_set_VB e"
      using fvae empty_inter_fv_arith_def_edge'' gen_set_VB_is_aexp_edge by auto
    ultimately
    show ?case
      using bw_must.S_hat_def by auto
  next
    assume "a ∈ aexp_edge e"
    then have "a ∈ gen_set_VB e"
      using fvae empty_inter_fv_arith_def_edge'' gen_set_VB_is_aexp_edge by auto
    then show ?case
      using bw_must.S_hat_def by auto
  qed
qed

lemma vbexp_edge_list_S_hat_edge_list_iff: 
  "vbexp_edge_list π a ⟷ a ∈ bw_must.S_hat_edge_list π d_init_VB"
  using S_hat_edge_list_aexp_edge_list aexp_edge_list_S_hat_edge_list' by blast

lemma vbexp_path_S_hat_path_iff: 
  "a ∈ vbexp_path π ⟷ a ∈ bw_must.S_hat_path π d_init_VB"
  by (simp add: bw_must.S_hat_path_def vbexp_edge_list_S_hat_edge_list_iff vbexp_path_def)

definition summarizes_VB where
  "summarizes_VB ρ ⟷
     (∀q d.
         ρ ⊨⇩l⇩h must⟨[q, d]⟩. ⟶
          (∀π. π ∈ path_with_word_from_to (the_Node⇩i⇩d q) end ⟶ the_Elem⇩i⇩d d ∈ vbexp_path π))"

theorem VB_sound:
  assumes "ρ ⊨⇩l⇩s⇩t (bw_must.ana_pg_bw_must) s_BV"
  shows "summarizes_VB ρ"
proof -
  from assms have "bw_must.summarizes_bw_must ρ"
    using bw_must.sound_ana_pg_bw_must by auto
  then show ?thesis
    unfolding summarizes_VB_def bw_must.summarizes_bw_must_def edges_def edges_def
      end_def end_def vbexp_path_S_hat_path_iff start_def start_def by force
qed

end

end