Theory Live_Variables

theory Live_Variables imports Reaching_Definitions begin

― ‹We encode the Live Variables 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 ‹Live Variables Analysis›

fun use_action :: "'v action ⇒ 'v set" where
  "use_action (x ::= a) = fv_arith a"
| "use_action (Bool b) = fv_boolean b"
| "use_action Skip = {}"

fun use_edge :: "('n,'v action) edge ⇒ 'v set" where
  "use_edge (q1, α, q2) = use_action α"

definition use_edge_list :: "('n,'v action) edge list ⇒ 'v ⇒ bool" where
  "use_edge_list π x = (∃π1 π2 e. π = π1 @ [e] @ π2 ∧ 
                                  x ∈ use_edge e ∧ 
                                  (¬(∃e' ∈ set π1. x ∈ def_edge e')))"

definition use_path :: "'n list × 'v action list ⇒ 'v set" where
  "use_path π = {x. use_edge_list (LTS.transition_list π) x}"

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

interpretation LTS edges .

definition analysis_dom_LV :: "'v set" where
  "analysis_dom_LV = UNIV"

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

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

definition d_init_LV :: "'v set" where
  "d_init_LV = {}"

interpretation bw_may: analysis_BV_backward_may pg analysis_dom_LV kill_set_LV gen_set_LV d_init_LV
  using analysis_BV_backward_may.intro analysis_LV_axioms analysis_LV_def analysis_dom_LV_def 
    finite_UNIV subset_UNIV analysis_BV_backward_may_axioms_def finite_program_graph_def by metis

lemma use_edge_list_S_hat_edge_list: 
  assumes "use_edge_list π x"
  shows "x ∈ bw_may.S_hat_edge_list π d_init_LV"
  using assms
proof (induction π)
  case Nil
  then have False 
    unfolding use_edge_list_def by auto
  then show ?case
    by metis
next
  case (Cons e π)
  note Cons_inner = Cons
  from Cons(2) have "∃π1 π2 e'. e # π = π1 @ [e'] @ π2 ∧ 
                                x ∈ use_edge e' ∧ 
                                ¬ (∃e''∈set π1. x ∈ def_edge e'')"
    unfolding use_edge_list_def by auto
  then obtain π1 π2 e' where π1_π2_e'_p:
    "e # π = π1 @ [e'] @ π2"
    "x ∈ use_edge e'"
    "¬(∃e''∈set π1. x ∈ def_edge e'')"
    by auto
  then show ?case
  proof (cases π1)
    case Nil
    have "e = e'"
      using π1_π2_e'_p(1) Nil by auto
    then have x_used_a: "x ∈ use_edge e"
      using π1_π2_e'_p(2) by auto
    obtain p α q where a_split: "e = (p, α, q)"
      by (cases e)
    show ?thesis
      using x_used_a bw_may.S_hat_def a_split by (cases α) auto
  next
    case (Cons hd_π1 tl_π1)
    obtain p α q where e_split: "e' = (p, α, q)"
      by (cases e')
    have "(π = tl_π1 @ (p, α, q) # π2) ∧ x ∈ use_action α ∧ (∀e'∈set tl_π1. x ∉ def_edge e')"
      using Cons π1_π2_e'_p e_split by auto
    then have "use_edge_list π x"
      unfolding use_edge_list_def by force
    then have x_in_S_hat_π: "x ∈ bw_may.S_hat_edge_list π d_init_LV"
      using Cons_inner by auto
    have "e ∈ set π1"
      using π1_π2_e'_p(1) Cons(1) by auto
    then have x_not_def_a: "¬x ∈ def_edge e"
      using π1_π2_e'_p(3) by auto

    obtain p' α' q' where a_split: "e = (p', α', q')"
      by (cases e)

    show ?thesis
    proof (cases "x ∈ kill_set_LV e")
      case True
      show ?thesis
        using True a_split x_not_def_a by (cases α'; force)
    next
      case False
      then show ?thesis
        by (simp add: bw_may.S_hat_def x_in_S_hat_π)
    qed
  qed
qed

lemma S_hat_edge_list_use_edge_list:
  assumes "x ∈ bw_may.S_hat_edge_list π d_init_LV"
  shows "use_edge_list π x"
  using assms 
proof (induction π)
  case Nil
  then have False
    using d_init_LV_def by auto
  then show ?case
    by metis
next
  case (Cons e π)
  from Cons(2) have "x ∈ bw_may.S_hat_edge_list π d_init_LV - kill_set_LV e ∪ gen_set_LV e"
    unfolding bw_may.S_hat_edge_list.simps unfolding bw_may.S_hat_def by auto
  then show ?case
  proof
    assume a: "x ∈ bw_may.S_hat_edge_list π d_init_LV - kill_set_LV e"
    then have "x ∈ bw_may.S_hat_edge_list π d_init_LV"
      by auto
    then have "use_edge_list π x"
      using Cons by auto
    then have "∃π1 π2 e'. π = π1 @ [e'] @ π2 ∧ x ∈ use_edge e' ∧ ¬(∃e''∈set π1. x ∈ def_edge e'')"
      unfolding use_edge_list_def by auto
    then obtain π1 π2 e' where π1_π2_e'_p:
      "π = π1 @ [e'] @ π2"
      "x ∈ use_edge e'"
      "¬(∃e''∈set π1. x ∈ def_edge e'')"
      by auto
    obtain q1 α q2 where e_split: "e = (q1, α, q2)"
      by (cases e) auto
    from a have "x ∉ kill_set_LV e"
      by auto
    then have x_not_killed: "x ∉ kill_set_LV (q1, α, q2)"
      using e_split by auto
    have "use_edge_list ((q1, α, q2) # π) x"
    proof (cases α)
      case (Asg y exp)
      then have "x ∉ kill_set_LV (q1, y ::= exp, q2)"
        using x_not_killed by auto
      then have x_not_y: "x ≠ y"
        by auto
      have "(q1, y ::= exp, q2) # π = ((q1, y ::= exp, q2) # π1) @ [e'] @ π2"
        using π1_π2_e'_p by force
      moreover
      have "¬ (∃e'∈set ((q1, y ::= exp, q2) # π1). x ∈ def_edge e')"
        using π1_π2_e'_p x_not_y by force
      ultimately
      have "use_edge_list ((q1, y ::= exp, q2) # π) x"
        unfolding use_edge_list_def using π1_π2_e'_p x_not_y by metis
      then show ?thesis
        by (simp add: Asg)
    next
      case (Bool b)
      have "(q1, Bool b, q2) # π = ((q1, Bool b, q2) # π1) @ [e'] @ π2"
        using π1_π2_e'_p unfolding use_edge_list_def by auto
      moreover
      have "¬ (∃e'∈set ((q1, Bool b, q2) # π1). x ∈ def_edge e')"
        using π1_π2_e'_p unfolding use_edge_list_def by auto
      ultimately
      have "use_edge_list ((q1, Bool b, q2) # π) x"
        unfolding use_edge_list_def using π1_π2_e'_p by metis
      then show ?thesis
        using Bool by auto
    next
      case Skip
      have "(q1, Skip, q2) # π = ((q1, Skip, q2) # π1) @ [e'] @ π2"
        using π1_π2_e'_p unfolding use_edge_list_def by auto
      moreover
      have "¬ (∃e'∈set ((q1, Skip, q2) # π1). x ∈ def_edge e')"
        using π1_π2_e'_p unfolding use_edge_list_def by auto
      ultimately
      have "use_edge_list ((q1, Skip, q2) # π) x"
        unfolding use_edge_list_def using π1_π2_e'_p by metis
      then show ?thesis
        using Skip by auto
    qed
    then show "use_edge_list (e # π) x"
      using e_split by auto
  next
    assume a: "x ∈ gen_set_LV e"
    obtain p α q where a_split: "e = (p, α, q)"
      by (cases e)
    have "use_edge_list ((p, α, q) # π) x"
      using a a_split unfolding use_edge_list_def by (cases α; force)
    then show "use_edge_list (e # π) x"
      using a_split by auto
  qed
qed

lemma use_edge_list_set_S_hat_edge_list: 
  "{x. use_edge_list π x} = bw_may.S_hat_edge_list π d_init_LV"
  using use_edge_list_S_hat_edge_list S_hat_edge_list_use_edge_list by auto

lemma use_path_S_hat_path: "use_path π = bw_may.S_hat_path π d_init_LV"
  by (simp add: use_edge_list_set_S_hat_edge_list bw_may.S_hat_path_def use_path_def)

definition summarizes_LV :: "(pred, ('n,'v action,'v) cst) pred_val ⇒ bool" where
  "summarizes_LV ρ ⟷ (∀π d. π ∈ path_with_word_to end ⟶ d ∈ use_path π ⟶ 
                         ρ ⊨⇩l⇩h may⟨[Cst⇩N (start_of π), Cst⇩E d]⟩.)"

theorem LV_sound:
  assumes "ρ ⊨⇩l⇩s⇩t bw_may.ana_pg_bw_may s_BV"
  shows "summarizes_LV ρ"
proof -
  from assms have "bw_may.summarizes_bw_may ρ"
    using bw_may.sound_ana_pg_bw_may[of ρ] by auto
  then show ?thesis
    unfolding summarizes_LV_def bw_may.summarizes_bw_may_def edges_def edges_def
      end_def end_def use_path_S_hat_path by blast
qed

end

end