Theory Slicing.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. nset (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 nset (sourcenodes (a#as)). V  Def n
    have noDef:"V  Def (sourcenode a)" 
    and all:"nset (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