Theory CFG_wf

section ‹CFG well-formedness›

theory CFG_wf imports CFG begin

subsection ‹Well-formedness of the abstract CFG›

locale CFG_wf = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')") +
  fixes Def::"'node ⇒ 'var set"
  fixes Use::"'node ⇒ 'var set"
  fixes state_val::"'state ⇒ 'var ⇒ 'val"
  assumes Entry_empty:"Def (_Entry_) = {} ∧ Use (_Entry_) = {}"
  and CFG_edge_no_Def_equal:
    "⟦valid_edge a; V ∉ Def (sourcenode a); pred (kind a) s⟧
     ⟹ state_val (transfer (kind a) s) V = state_val s V"
  and CFG_edge_transfer_uses_only_Use:
    "⟦valid_edge a; ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V;
      pred (kind a) s; pred (kind a) s'⟧
      ⟹ ∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
                                     state_val (transfer (kind a) s') V"
  and CFG_edge_Uses_pred_equal:
    "⟦valid_edge a; pred (kind a) s; 
      ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V⟧
       ⟹ pred (kind a) s'"
  and deterministic:"⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
    targetnode a ≠ targetnode a'⟧ 
  ⟹ ∃Q Q'. kind a = (Q)⇩√ ∧ kind a' = (Q')⇩√ ∧ 
             (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"

begin

lemma [dest!]: "V ∈ Use (_Entry_) ⟹ False"
by(simp add:Entry_empty)

lemma [dest!]: "V ∈ Def (_Entry_) ⟹ False"
by(simp add:Entry_empty)


lemma CFG_path_no_Def_equal:
  "⟦n -as→* n'; ∀n ∈ set (sourcenodes as). V ∉ Def n; preds (kinds as) s⟧ 
    ⟹ state_val (transfers (kinds as) s) V = state_val s V"
proof(induct arbitrary:s rule:path.induct)
  case (empty_path n)
  thus ?case by(simp add:sourcenodes_def kinds_def)
next
  case (Cons_path n'' as n' a n)
  note IH = ‹⋀s. ⟦∀n∈set (sourcenodes as). V ∉ Def n; preds (kinds as) s⟧ ⟹
            state_val (transfers (kinds as) s) V = state_val s V›
  from ‹preds (kinds (a#as)) s› have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
  from ‹∀n∈set (sourcenodes (a#as)). V ∉ Def n›
    have noDef:"V ∉ Def (sourcenode a)" 
    and all:"∀n∈set (sourcenodes as). V ∉ Def n"
    by(auto simp:sourcenodes_def)
  from ‹valid_edge a› noDef ‹pred (kind a) s›
  have "state_val (transfer (kind a) s) V = state_val s V"
    by(rule CFG_edge_no_Def_equal)
  with IH[OF all ‹preds (kinds as) (transfer (kind a) s)›] show ?case
    by(simp add:kinds_def)
qed

end


end