Theory SSA_CFG_code

(*  Title:      SSA_CFG_code.thy
    Author:     Denis Lohner, Sebastian Ullrich
*)

theory SSA_CFG_code imports
  SSA_CFG
  Mapping_Exts
  "HOL-Library.Product_Lexorder"
begin

definition Union_of :: "('a ⇒ 'b set) ⇒ 'a set ⇒ 'b set"
  where "Union_of f A ≡ ⋃(f ` A)"

lemma Union_of_alt_def: "Union_of f A = (⋃x ∈ A. f x)"
  unfolding Union_of_def by simp

type_synonym ('node, 'val) phis_code = "('node × 'val, 'val list) mapping"

context CFG_base begin
  definition addN :: "'g ⇒ 'node ⇒ ('var, 'node set) mapping ⇒ ('var, 'node set) mapping"
    where "addN g n ≡ fold (λv. Mapping.map_default v {} (insert n)) (sorted_list_of_set (uses g n))"
  definition "addN' g n = fold (λv m. m(v ↦ case_option {n} (insert n) (m v))) (sorted_list_of_set (uses g n))"

  lemma addN_transfer [transfer_rule]:
    "rel_fun (=) (rel_fun (=) (rel_fun (pcr_mapping (=) (=)) (pcr_mapping (=) (=)))) addN' addN"
    unfolding addN_def [abs_def] addN'_def [abs_def]
      Mapping.map_default_def [abs_def] Mapping.default_def
  apply (auto simp: mapping.pcr_cr_eq rel_fun_def cr_mapping_def)
  apply transfer
  apply (rule fold_cong)
    apply simp
   apply simp
  apply (intro ext)
  by auto

  definition "useNodes_of g = fold (addN g) (αn g) Mapping.empty"
  lemmas useNodes_of_code = useNodes_of_def [unfolded addN_def [abs_def]]
  declare useNodes_of_code [code]

  lemma lookup_useNodes_of':
    assumes [simp]: "⋀n. finite (uses g n)"
    shows "Mapping.lookup (useNodes_of g) v =
    (if (∃n ∈ set (αn g). v ∈ uses g n) then Some {n ∈ set (αn g). v ∈ uses g n} else None)"
  proof -
    { fix m n xs v
      have "Mapping.lookup (fold (λv. Mapping.map_default (v::'var) {} (insert (n::'node))) xs m) v=
        (case Mapping.lookup m v of None ⇒ (if v ∈ set xs then Some {n} else None)
          | Some N ⇒ (if v ∈ set xs then Some (insert n N) else Some N))"
      by (induction xs arbitrary: m) (auto simp: Mapping_lookup_map_default split: option.splits)
    }
    note addN_conv = this [of n "sorted_list_of_set (uses g n)" for g n, folded addN_def, simplified]
    { fix xs m v
      have "Mapping.lookup (fold (addN g) xs m) v = (case Mapping.lookup m v of None ⇒ if (∃n∈set xs. v ∈ uses g n) then Some {n∈set xs. v ∈ uses g n} else None
        | Some N ⇒ Some ({n∈set xs. v ∈ uses g n} ∪ N))"
      by (induction xs arbitrary: m) (auto split: option.splits simp: addN_conv)
    }
    note this [of "αn g" Mapping.empty, simp]
    show ?thesis unfolding useNodes_of_def
      by (auto split: option.splits simp: lookup_empty)
  qed
end

context CFG begin
  lift_definition useNodes_of' :: "'g ⇒ ('var, 'node set) mapping"
  is "λg v. if (∃n ∈ set (αn g). v ∈ uses g n) then Some {n ∈ set (αn g). v ∈ uses g n} else None" .

  lemma useNodes_of': "useNodes_of' = useNodes_of"
  proof
    fix g
    { fix m n xs
      have "fold (λv m. m(v::'var ↦ case m v of None ⇒ {n::'node} | Some x ⇒ insert n x)) xs m =
        (λv. case m v of None ⇒ (if v ∈ set xs then Some {n} else None)
          | Some N ⇒ (if v ∈ set xs then Some (insert n N) else Some N))"
      by (induction xs arbitrary: m)(auto split: option.splits)
    }
    note addN'_conv = this [of n "sorted_list_of_set (uses g n)" for g n, folded addN'_def, simplified]
    { fix xs m
      have "fold (addN' g) xs m = (λv. case m v of None ⇒ if (∃n∈set xs. v ∈ uses g n) then Some {n∈set xs. v ∈ uses g n} else None
        | Some N ⇒ Some ({n∈set xs. v ∈ uses g n} ∪ N))"
      by (induction xs arbitrary: m) (auto 4 4 split: option.splits if_splits simp: addN'_conv intro!: ext)
    }
    note this [of "αn g" Map.empty, simp]
    show "useNodes_of' g = useNodes_of g"
    unfolding mmap_def useNodes_of_def
    by (transfer fixing: g) auto
  qed

  declare useNodes_of'.transfer [unfolded useNodes_of', transfer_rule]

  lemma lookup_useNodes_of: "Mapping.lookup (useNodes_of g) v =
    (if (∃n ∈ set (αn g). v ∈ uses g n) then Some {n ∈ set (αn g). v ∈ uses g n} else None)"
  by clarsimp (transfer'; auto)

end

context CFG_SSA_base begin
  definition phis_addN
  where "phis_addN g n = fold (λv. Mapping.map_default v {} (insert n)) (case_option [] id (phis g n))"

  definition phidefNodes where [code]:
    "phidefNodes g = fold (λ(n,v). Mapping.update v n) (sorted_list_of_set (dom (phis g))) Mapping.empty"

  lemma keys_phidefNodes:
    assumes "finite (dom (phis g))"
    shows "Mapping.keys (phidefNodes g) = snd ` dom (phis g)"
  proof -
    { fix xs m x
      have "fold (λ(a,b) m. m(b ↦ a)) (xs::('node × 'val) list) m x = (if x ∈ snd ` set xs then (Some ∘ fst) (last [(b,a)←xs. a = x]) else m x)"
      by (induction xs arbitrary: m) (auto split: if_splits simp: filter_empty_conv intro: rev_image_eqI)
    }
    from this [of "sorted_list_of_set (dom (phis g))" Map.empty] assms
    show ?thesis
    unfolding phidefNodes_def keys_dom_lookup
    by (transfer fixing: g phis) (auto simp: dom_def intro: rev_image_eqI)
  qed

  definition phiNodes_of :: "'g ⇒ ('val, ('node × 'val) set) mapping"
  where "phiNodes_of g = fold (phis_addN g) (sorted_list_of_set (dom (phis g))) Mapping.empty"

  lemma lookup_phiNodes_of:
  assumes [simp]: "finite (dom (phis g))"
  shows "Mapping.lookup (phiNodes_of g) v =
    (if (∃n ∈ dom (phis g). v ∈ set (the (phis g n))) then Some {n ∈ dom (phis g). v ∈ set (the (phis g n))} else None)"
  proof -
  {
    fix m n xs v
    have "Mapping.lookup (fold (λv. Mapping.map_default v {} (insert (n::'node × 'val))) xs (m::('val, ('node × 'val) set) mapping)) v =
      (case Mapping.lookup m v of None ⇒ (if v ∈ set xs then Some {n} else None)
        | Some N ⇒ (if v ∈ set xs then Some (insert n N) else Some N))"
    by (induction xs arbitrary: m) (auto simp: Mapping_lookup_map_default split: option.splits)
  }
  note phis_addN_conv = this [of n "case_option [] id (phis g n)" for n, folded phis_addN_def]
  {
    fix xs m v
    have "Mapping.lookup (fold (phis_addN g) xs m) v =
      (case Mapping.lookup m v of None ⇒ if (∃n ∈ set xs. v ∈ set (case_option [] id (phis g n))) then Some {n ∈ set xs. v ∈ set (case_option [] id (phis g n))} else None
        | Some N ⇒ Some ({n ∈ set xs. v ∈ set (case_option [] id (phis g n))} ∪ N))"
    by (induction xs arbitrary: m) (auto simp: phis_addN_conv split: option.splits if_splits)+
  }
  note this [of "sorted_list_of_set (dom (phis g))", simp]
  show ?thesis
    unfolding phiNodes_of_def
  by (force split: option.splits simp: lookup_empty)
  qed

  lemmas phiNodes_of_code = phiNodes_of_def [unfolded phis_addN_def [abs_def]]
  declare phiNodes_of_code [code]

lemma phis_transfer [transfer_rule]:
  includes lifting_syntax
  shows "((=) ===> pcr_mapping (=) (=)) phis (λg. Mapping.Mapping (phis g))"
  by (auto simp: mapping.pcr_cr_eq rel_fun_def cr_mapping_def Mapping.Mapping_inverse)

end

context CFG_SSA begin
  declare lookup_phiNodes_of [OF phis_finite, simp]
  declare keys_phidefNodes [OF phis_finite, simp]
end

locale CFG_SSA_ext_base = CFG_SSA_base αe αn invar inEdges' Entry "defs" "uses" phis
  for αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set"
    and αn :: "'g ⇒ 'node list"
    and invar :: "'g ⇒ bool"
    and inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list"
    and Entry :: "'g ⇒ 'node"
    and "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set"
    and "uses" :: "'g ⇒ 'node ⇒ 'val set"
    and phis :: "'g ⇒ ('node, 'val) phis"
begin
  abbreviation "cache g f ≡ Mapping.tabulate (αn g) f"

  lemma lookup_cache[simp]: "n ∈ set (αn g) ⟹ Mapping.lookup (cache g f) n = Some (f n)"
  by transfer (auto simp: Map.map_of_map_restrict)

  lemma lookup_cacheD [dest]: "Mapping.lookup (cache g f) x = Some y ⟹ y = f x"
  by transfer (auto simp: Map.map_of_map_restrict restrict_map_def split: if_splits)

  lemma lookup_cache_usesD: "Mapping.lookup (cache g (uses g)) n = Some vs ⟹ vs = uses g n"
  by blast
end

definition[simp]: "usesOf m n ≡ case_option {} id (Mapping.lookup m n)"

locale CFG_SSA_ext = CFG_SSA_ext_base  αe αn invar inEdges' Entry "defs" "uses" phis
  + CFG_SSA αe αn invar inEdges' Entry "defs" "uses" phis
  for αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set"
    and αn :: "'g ⇒ 'node list"
    and invar :: "'g ⇒ bool"
    and inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list"
    and Entry :: "'g ⇒ 'node"
    and "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set"
    and "uses" :: "'g ⇒ 'node ⇒ 'val set"
    and phis :: "'g ⇒ ('node, 'val) phis"
begin
  lemma usesOf_cache[abs_def, simp]: "usesOf (cache g (uses g)) n = uses g n"
  by (auto simp: uses_in_αn dest: lookup_cache_usesD split: option.split)
end

locale CFG_SSA_base_code = CFG_SSA_ext_base αe αn invar inEdges' Entry "defs" "usesOf ∘ uses" "λg. Mapping.lookup (phis g)"
  for αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set"
    and αn :: "'g ⇒ 'node list"
    and invar :: "'g ⇒ bool"
    and inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list"
    and Entry :: "'g ⇒ 'node"
    and "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set"
    and "uses" :: "'g ⇒ ('node, 'val set) mapping"
    and phis :: "'g ⇒ ('node, 'val) phis_code"
begin
  declare phis_transfer [simplified, transfer_rule]

  lemma phiDefs_code [code]:
  "phiDefs g n = snd ` Set.filter (λ(n',v). n' = n) (Mapping.keys (phis g))"
    unfolding phiDefs_def
    by transfer (auto 4 3 intro: rev_image_eqI simp: Set.filter_def)

  lemmas phiUses_code [code] = phiUses_def [folded Union_of_alt_def]
  declare allUses_def [code]
  lemmas allVars_code [code] = allVars_def [folded Union_of_alt_def]
end

locale CFG_SSA_code = CFG_SSA_base_code  αe αn invar inEdges' Entry "defs" "uses" phis
  + CFG_SSA_ext αe αn invar inEdges' Entry "defs" "usesOf ∘ uses" "λg. Mapping.lookup (phis g)"
  for αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set"
    and αn :: "'g ⇒ 'node list"
    and invar :: "'g ⇒ bool"
    and inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list"
    and Entry :: "'g ⇒ 'node"
    and "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set"
    and "uses" :: "'g ⇒ ('node, 'val set) mapping"
    and phis :: "'g ⇒ ('node, 'val) phis_code"


definition "the_trivial v vs = (case (foldl (λ(good,v') w. if w = v then (good,v')
      else case v' of Some v' ⇒ (good ∧ w = v', Some v')
        | None ⇒ (good, Some w))
    (True, None) vs)
  of (False, _) ⇒ None | (True,v) ⇒ v)"

lemma the_trivial_Nil [simp]: "the_trivial x [] = None"
  unfolding the_trivial_def by simp

lemma the_trivialI:
  assumes "set vs ⊆ {v, v'}"
    and "v' ≠ v"
  shows "the_trivial v vs = (if set vs ⊆ {v} then None else Some v')"
proof -
  { fix vx
    have "⟦ set vs ⊆ {v, v'}; v' ≠ v; vx ∈ {None, Some v'} ⟧
    ⟹ (case foldl (λ(good, v') w.
                    if w = v then (good, v')
                    else case v' of None ⇒ (good, Some w) | Some v' ⇒ (good ∧ w = v', Some v'))
           (True, vx) vs of
     (True, x) ⇒ x | (False, x) ⇒ None) = (if set vs ⊆ {v} then vx else Some v')"
    by (induction vs arbitrary: vx; case_tac vx; auto)
  }
  with assms show ?thesis unfolding the_trivial_def by simp
qed

lemma the_trivial_conv:
  shows "the_trivial v vs = (if ∃v' ∈ set vs. v' ≠ v ∧ set vs - {v'} ⊆ {v} then Some (THE v'. v' ∈ set vs ∧ v' ≠ v ∧ set vs - {v'} ⊆ {v}) else None)"
proof -
  { fix b a vs
    have "a ≠ v
       ⟹ foldl (λ(good, v') w.
                     if w = v then (good, v')
                     else case v' of None ⇒ (good, Some w) | Some v' ⇒ (good ∧ w = v', Some v'))
            (b, Some a) vs =
           (b ∧ set vs ⊆ {v, a}, Some a)"
     by (induction vs arbitrary: b; clarsimp)
  }
  note this[simp]
  { fix b vx
    have "⟦ vx ∈ insert None (Some ` set vs); case_option True (λvx. vx ≠ v) vx ⟧
    ⟹ foldl (λ(good, v') w.
                    if w = v then (good, v')
                    else case v' of None ⇒ (good, Some w) | Some v' ⇒ (good ∧ w = v', Some v'))
        (b, vx) vs = (b ∧ (case vx of Some w ⇒ set vs ⊆ {v, w} | None ⇒ ∃w. set vs ⊆ {v, w}),
        (case vx of Some w ⇒ Some w | None ⇒ if (∃v'∈set vs. v' ≠ v) then Some (hd (filter (λv'. v' ≠ v) vs)) else None))"
    by (induction vs arbitrary: b vx; auto)
  }
  hence "the_trivial v vs = (if ∃v' ∈ set vs. v' ≠ v ∧ set vs - {v'} ⊆ {v} then Some (hd (filter (λv'. v' ≠ v) vs)) else None)"
    unfolding the_trivial_def by (auto split: bool.splits)
  thus ?thesis
  apply (auto split: if_splits)
  apply (rule the_equality [THEN sym])
   by (thin_tac "P" for P, (induction vs; auto))+
qed

lemma the_trivial_SomeE:
  assumes "the_trivial v vs = Some v'"
  obtains "v ≠ v'" and "set vs = {v'}" | "v ≠ v'" and "set vs = {v,v'}"
using assms
apply atomize_elim
apply (subst(asm) the_trivial_conv)
apply (split if_splits; simp)
by (subgoal_tac "(THE v'. v' ∈ set vs ∧ v' ≠ v ∧ set vs - {v'} ⊆ {v}) = hd (filter (λv'. v' ≠ v) vs)")
  (fastforce simp: set_double_filter_hd set_single_hd set_minus_one)+

locale CFG_SSA_wf_base_code = CFG_SSA_base_code αe αn invar inEdges' Entry "defs" "uses" phis
  + CFG_SSA_wf_base αe αn invar inEdges' Entry "defs" "usesOf ∘ uses" "λg. Mapping.lookup (phis g)"
  for αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set"
    and αn :: "'g ⇒ 'node list"
    and invar :: "'g ⇒ bool"
    and inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list"
    and Entry :: "'g ⇒ 'node"
    and "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set"
    and "uses" :: "'g ⇒ ('node, 'val set) mapping"
    and phis :: "'g ⇒ ('node, 'val) phis_code"
begin
  definition [code]:
    "trivial_code (v::'val) vs = (the_trivial v vs ≠ None)"
  definition[code]: "trivial_phis g = Set.filter (λ(n,v). trivial_code v (the (Mapping.lookup (phis g) (n,v)))) (Mapping.keys (phis g))"
  definition [code]: "redundant_code g = (trivial_phis g ≠ {})"
end

locale CFG_SSA_wf_code = CFG_SSA_code αe αn invar inEdges' Entry "defs" "uses" phis
  + CFG_SSA_wf_base_code αe αn invar inEdges' Entry "defs" "uses" phis
  + CFG_SSA_wf αe αn invar inEdges' Entry "defs" "usesOf ∘ uses" "λg. Mapping.lookup (phis g)"
  for αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set"
    and αn :: "'g ⇒ 'node list"
    and invar :: "'g ⇒ bool"
    and inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list"
    and Entry :: "'g ⇒ 'node"
    and "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set"
    and "uses" :: "'g ⇒ ('node, 'val set) mapping"
    and phis :: "'g ⇒ ('node, 'val) phis_code"
begin
  lemma trivial_code:
    "phi g v = Some vs ⟹ trivial g v = trivial_code v vs"
  unfolding trivial_def trivial_code_def
  apply (auto split: option.splits simp: isTrivialPhi_def)
    apply (clarsimp simp: the_trivial_conv split: if_splits)
   apply (clarsimp simp: the_trivial_conv split: if_splits)
  apply (erule the_trivial_SomeE)
   apply simp
   apply (rule phiArg_in_allVars; auto simp: phiArg_def)
  apply (rename_tac v')
  apply (rule_tac x=v' in bexI)
   apply simp
  apply (rule phiArg_in_allVars; auto simp: phiArg_def)
  done

  lemma trivial_phis:
    "trivial_phis g = {(n,v). Mapping.lookup (phis g) (n,v) ≠ None ∧ trivial g v}"
  unfolding trivial_phis_def Set.filter_def
  apply (auto simp add: phi_def keys_dom_lookup)
   apply (subst trivial_code)
    apply (auto simp: image_def trivial_in_allVars phis_phi)
  apply (frule trivial_phi)
  apply (auto simp add: trivial_code phi_def[symmetric] phis_phi)
  done

  lemma redundant_code:
    "redundant g = redundant_code g"
  unfolding redundant_def redundant_code_def trivial_phis[of g]
  apply (auto simp: image_def trivial_in_allVars)
  apply (frule trivial_phi)
  apply (auto simp: phi_def)
  done

  lemma trivial_code_mapI:
  "⟦ trivial_code v vs; f ` (set vs - {v}) ≠ {v} ; f v = v ⟧ ⟹ trivial_code v (map f vs)"
  unfolding trivial_code_def the_trivial_conv
    by (auto split: if_splits)

  lemma trivial_code_map_conv:
    "f v = v ⟹ trivial_code v (map f vs) ⟷ (∃v'∈set vs. f v' ≠ v ∧ (f ` set vs) - {f v'} ⊆ {v})"
    unfolding trivial_code_def the_trivial_conv
    by auto

end

locale CFG_SSA_Transformed_code = ssa: CFG_SSA_wf_code αe αn invar inEdges' Entry "defs" "uses" phis
   +
   CFG_SSA_Transformed αe αn invar inEdges' Entry oldDefs oldUses "defs" "usesOf ∘ uses" "λg. Mapping.lookup (phis g)" var
for
  αe :: "'g ⇒ ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ⇒ 'node list" and
  invar :: "'g ⇒ bool" and
  inEdges' :: "'g ⇒ 'node ⇒ ('node × 'edgeD) list" and
  Entry::"'g ⇒ 'node" and
  oldDefs :: "'g ⇒ 'node ⇒ 'var::linorder set" and
  oldUses :: "'g ⇒ 'node ⇒ 'var set" and
  "defs" :: "'g ⇒ 'node ⇒ 'val::linorder set" and
  "uses" :: "'g ⇒ ('node, 'val set) mapping" and
  phis :: "'g ⇒ ('node, 'val) phis_code" and
  var :: "'g ⇒ 'val ⇒ 'var"
+
assumes dom_uses_in_graph: "Mapping.keys (uses g) ⊆ set (αn g)"

end