Theory Available_Expressions

theory Available_Expressions imports Reaching_Definitions begin

― ‹We encode the Available 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 ‹Available Expressions›

fun ae_arith :: "'v arith ⇒ 'v arith set" where
  "ae_arith (Integer i) = {}"
| "ae_arith (Arith_Var v) = {}"
| "ae_arith (Arith_Op a1 opr a2) = ae_arith a1 ∪ ae_arith a1 ∪ {Arith_Op a1 opr a2}"
| "ae_arith (Minus a) = ae_arith a"

lemma finite_ae_arith: "finite (ae_arith a)"
  by (induction a) auto

fun ae_boolean :: "'v boolean ⇒ 'v arith set" where
  "ae_boolean true = {}"
| "ae_boolean false = {}"
| "ae_boolean (Rel_Op a1 opr a2) = ae_arith a1 ∪ ae_arith a2"
| "ae_boolean (Bool_Op b1 opr b2) = ae_boolean b1 ∪ ae_boolean b2"
| "ae_boolean (Neg b) = ae_boolean b"

lemma finite_ae_boolean: "finite (ae_boolean b)"
  using finite_ae_arith by (induction b) auto

fun aexp_action :: "'v action ⇒ 'v arith set" where
  "aexp_action (x ::= a) = ae_arith a"
| "aexp_action (Bool b) = ae_boolean b"
| "aexp_action Skip = {}"

lemma finite_aexp_action: "finite (aexp_action α)"
  using finite_ae_arith finite_ae_boolean by (cases α) auto

fun aexp_edge :: "('n,'v action) edge ⇒ 'v arith set" where
  "aexp_edge (q1, α, q2) = aexp_action α"

lemma finite_aexp_edge: "finite (aexp_edge (q1, α, q2))"
  using finite_aexp_action by auto

fun aexp_pg :: "('n,'v action) program_graph ⇒ 'v arith set" where
  "aexp_pg pg = ⋃(aexp_edge ` (fst pg))"

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

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


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

interpretation LTS edges .

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

lemma finite_analysis_dom_AE: "finite analysis_dom_AE"
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_AE_def using edges_def by force 
qed

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

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

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

interpretation fw_must: analysis_BV_forward_must pg analysis_dom_AE kill_set_AE gen_set_AE d_init_AE
  using analysis_BV_forward_must.intro analysis_AE_axioms analysis_AE_def
    d_init_AE_def empty_subsetI finite_analysis_dom_AE analysis_BV_forward_must_axioms.intro
  by metis

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

lemma empty_inter_fv_arith_def_edge:
  assumes "aexp_edge_list (π @ [e]) a"
  shows "fv_arith a ∩ def_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 ([e'] @ π2). fv_arith a ∩ def_edge e'' = {})"
    unfolding aexp_edge_list_def by auto
  from this(1) have "e ∈ set ([e'] @ π2)"
    by (metis append_is_Nil_conv last_appendR last_in_set snoc_eq_iff_butlast) 
  then show "fv_arith a ∩ def_edge e = {}"
    using π1_π2_e'_p(3) by auto
qed

lemma aexp_edge_list_append_singleton:
  assumes "aexp_edge_list (π @ [e]) a"
  shows "aexp_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 ([e'] @ π2). fv_arith a ∩ def_edge e'' = {})"
    unfolding aexp_edge_list_def by auto
  from this(1) have "e ∈ set ([e'] @ π2)"
    by (metis append_is_Nil_conv last_appendR last_in_set snoc_eq_iff_butlast)
  then have "e = e' ∨ e ∈ set π2"
    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 π2"
    then have "π = π1 @ [e'] @ (butlast π2)"
      by (metis π1_π2_e'_p(1) append_is_Nil_conv butlast_append butlast_snoc 
          in_set_conv_decomp_first)
    moreover
    have "a ∈ aexp_edge e'"
      by (simp add: π1_π2_e'_p(2))
    moreover
    have "(∀e''∈set ([e'] @ butlast π2). fv_arith a ∩ def_edge e'' = {})"
      by (metis π1_π2_e'_p(3) butlast.simps(1) butlast_append in_set_butlastD)
    ultimately
    have "aexp_edge_list π a"
      unfolding aexp_edge_list_def by blast
    then show ?thesis
      by auto
  qed
qed

lemma gen_set_AE_subset_aexp_edge:
  assumes "a ∈ gen_set_AE e"
  shows "a ∈ aexp_edge e"
proof -
  obtain q α q' where "e = (q, α, q')"
    by (cases e)
  then show ?thesis
    using assms by (cases α) auto
qed

lemma empty_inter_fv_arith_def_edge':
  assumes "a ∈ gen_set_AE e"
  shows "fv_arith a ∩ def_edge e = {}"
proof -
  obtain q α q' where "e = (q, α, q')"
    by (cases e)
  then show ?thesis
    using assms by (cases α) auto
qed

lemma empty_inter_fv_arith_def_edge'':
  assumes "a ∉ kill_set_AE e"
  shows "fv_arith a ∩ def_edge e = {}"
proof -
  obtain q α q' where "e = (q, α, q')"
    by (cases e)
  then show ?thesis
    using assms by (cases α) auto
qed

lemma S_hat_edge_list_aexp_edge_list: 
  assumes "a ∈ fw_must.S_hat_edge_list π d_init_AE"
  shows "aexp_edge_list π a"
  using assms 
proof (induction π rule: rev_induct)
  case Nil
  then show ?case 
    unfolding d_init_AE_def by auto
next
  case (snoc e π)
  from snoc(2) have "a ∈ (fw_must.S_hat_edge_list π d_init_AE - kill_set_AE e) ∨ a ∈ gen_set_AE e"
    using fw_must.S_hat_def by auto
  then show ?case
  proof 
    assume a_S_hat: "a ∈ fw_must.S_hat_edge_list π d_init_AE - kill_set_AE e"
    then have "aexp_edge_list π a"
      using snoc by auto
    moreover
    from a_S_hat have "a ∉ kill_set_AE e"
      by auto
    then have "fv_arith a ∩ def_edge e = {}"
      using empty_inter_fv_arith_def_edge'' by auto
    ultimately show "aexp_edge_list (π @ [e]) a"
      unfolding aexp_edge_list_def by force
  next
    assume a_gen: "a ∈ gen_set_AE e"
    then have "a ∈ aexp_edge e"
      using gen_set_AE_subset_aexp_edge by auto
    moreover
    from a_gen have "(fv_arith a ∩ def_edge e = {})"
      using empty_inter_fv_arith_def_edge' by auto
    ultimately
    show "aexp_edge_list (π @ [e]) a"
      unfolding aexp_edge_list_def
      by (metis append_Nil2 empty_iff empty_set insert_iff list.set(2)) 
  qed
qed

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

lemma gen_set_AE_AE_iff_fv_arith_def_edge_disjoint_and_aexp_edge:
  "a ∈ aexp_edge e ∧ fv_arith a ∩ def_edge e = {} ⟷ a ∈ gen_set_AE e"
proof -
  obtain q α q' where e_split: "e = (q, α, q')"
    by (cases e)
  then show ?thesis
    by (cases α) auto
qed

lemma aexp_edge_list_S_hat_edge_list': 
  assumes "aexp_edge_list π a"
  shows "a ∈ fw_must.S_hat_edge_list π d_init_AE"
  using assms
proof (induction π rule: rev_induct)
  case Nil
  then have False 
    unfolding aexp_edge_list_def by auto
  then show ?case
    by metis
next
  case (snoc e π)
  have fvae: "fv_arith a ∩ def_edge e = {}"
    using snoc(2) empty_inter_fv_arith_def_edge by metis

  have "aexp_edge_list π a ∨ a ∈ aexp_edge e"
    using snoc(2)
    by (simp add: aexp_edge_list_append_singleton)
  then show ?case
  proof
    assume "aexp_edge_list π a"
    then have "a ∈ fw_must.S_hat_edge_list π d_init_AE"
      using snoc by auto
    moreover
    have "a ∉ kill_set_AE e"
      using fvae not_kill_set_AE_iff_fv_arith_def_edge_disjoint by auto
    ultimately
    show ?case
      using fw_must.S_hat_def by auto
  next
    assume "a ∈ aexp_edge e"
    then have "a ∈ gen_set_AE e"
      using fvae gen_set_AE_AE_iff_fv_arith_def_edge_disjoint_and_aexp_edge by metis
    then show ?case
      using fw_must.S_hat_def by auto
  qed
qed

lemma aexp_edge_list_S_hat_edge_list_iff: 
  "aexp_edge_list π a ⟷ a ∈ fw_must.S_hat_edge_list π d_init_AE"
  using S_hat_edge_list_aexp_edge_list aexp_edge_list_S_hat_edge_list' by blast

lemma aexp_path_S_hat_path_iff: 
  "a ∈ aexp_path π ⟷ a ∈ fw_must.S_hat_path π d_init_AE"
  using S_hat_edge_list_aexp_edge_list aexp_edge_list_S_hat_edge_list' aexp_path_def fw_must.S_hat_path_def by blast

definition summarizes_AE :: "(pred, ('n, 'a, 'v arith) cst) pred_val ⇒ bool" where
   "summarizes_AE ρ ⟷
     (∀q d.
         ρ ⊨⇩l⇩h must⟨[q, d]⟩. ⟶
          (∀π. π ∈ path_with_word_from_to start (the_Node⇩i⇩d q) ⟶ (the_Elem⇩i⇩d d) ∈ aexp_path π))"

theorem AE_sound:
  assumes "ρ ⊨⇩l⇩s⇩t (fw_must.ana_pg_fw_must) s_BV"
  shows "summarizes_AE ρ"
proof -
  from assms have "fw_must.summarizes_fw_must ρ"
    using fw_must.sound_ana_pg_fw_must by auto
  then show ?thesis
    unfolding summarizes_AE_def fw_must.summarizes_fw_must_def edges_def edges_def
      end_def end_def aexp_path_S_hat_path_iff start_def start_def by force
qed

end

end