Theory CFG_wf

section ‹CFG well-formedness›

theory CFG_wf imports CFG begin

locale CFG_wf = CFG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node  'pname"
  and get_return_edges :: "'edge  'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname" +
  fixes Def::"'node  'var set"
  fixes Use::"'node  'var set"
  fixes ParamDefs::"'node  'var list"
  fixes ParamUses::"'node  'var set list"
  assumes Entry_empty:"Def (_Entry_) = {}  Use (_Entry_) = {}"
  and ParamUses_call_source_length:
    "valid_edge a; kind a = Q:r↪⇘pfs; (p,ins,outs)  set procs
     length(ParamUses (sourcenode a)) = length ins"
  and distinct_ParamDefs:"valid_edge a  distinct (ParamDefs (targetnode a))"
  and ParamDefs_return_target_length:
    "valid_edge a; kind a = Q'↩⇘pf'; (p,ins,outs)  set procs
     length(ParamDefs (targetnode a)) = length outs"
  and ParamDefs_in_Def:
    "valid_node n; V  set (ParamDefs n)  V  Def n"
  and ins_in_Def:
    "valid_edge a; kind a = Q:r↪⇘pfs; (p,ins,outs)  set procs; V  set ins
     V  Def (targetnode a)"
  and call_source_Def_empty:
    "valid_edge a; kind a = Q:r↪⇘pfs  Def (sourcenode a) = {}"
  and ParamUses_in_Use:
    "valid_node n; V  Union (set (ParamUses n))  V  Use n"
  and outs_in_Use:
    "valid_edge a; kind a = Q↩⇘pf; (p,ins,outs)  set procs; V  set outs 
     V  Use (sourcenode a)"
  and CFG_intra_edge_no_Def_equal:
    "valid_edge a; V  Def (sourcenode a); intra_kind (kind a); pred (kind a) s
     state_val (transfer (kind a) s) V = state_val s V"
  and CFG_intra_edge_transfer_uses_only_Use:
    "valid_edge a; V  Use (sourcenode a). state_val s V = state_val s' V;
      intra_kind (kind a); 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; snd (hd s) = snd (hd s');
      V  Use (sourcenode a). state_val s V = state_val s' V; length s = length s'
     pred (kind a) s'"
  and CFG_call_edge_length:
    "valid_edge a; kind a = Q:r↪⇘pfs; (p,ins,outs)  set procs
     length fs = length ins"
  and CFG_call_determ:
    "valid_edge a; kind a = Q:r↪⇘pfs; valid_edge a'; kind a' = Q':r'↪⇘p'fs';
      sourcenode a = sourcenode a'; pred (kind a) s; pred (kind a') s
     a = a'"
  and CFG_call_edge_params:
    "valid_edge a; kind a = Q:r↪⇘pfs; i < length ins; 
      (p,ins,outs)  set procs; pred (kind a) s; pred (kind a) s';
      V  (ParamUses (sourcenode a))!i. state_val s V = state_val s' V
     (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"  
  and CFG_return_edge_fun:
    "valid_edge a; kind a = Q'↩⇘pf'; (p,ins,outs)  set procs
      f' vmap vmap' = vmap'(ParamDefs (targetnode a) [:=] map vmap outs)"
  and deterministic:"valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
    targetnode a  targetnode a'; intra_kind (kind a); intra_kind (kind a') 
     Q Q'. kind a = (Q)  kind a' = (Q')  
             (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))"

begin


lemma CFG_equal_Use_equal_call:
  assumes "valid_edge a" and "kind a = Q:r↪⇘pfs" and "valid_edge a'"
  and "kind a' = Q':r'↪⇘p'fs'" and "sourcenode a = sourcenode a'"
  and "pred (kind a) s" and "pred (kind a') s'" 
  and "snd (hd s) = snd (hd s')" and "length s = length s'"
  and "V  Use (sourcenode a). state_val s V = state_val s' V"
  shows "a = a'"
proof -
  from valid_edge a pred (kind a) s snd (hd s) = snd (hd s')
    V  Use (sourcenode a). state_val s V = state_val s' V length s = length s'
  have "pred (kind a) s'" by(rule CFG_edge_Uses_pred_equal)
  with valid_edge a kind a = Q:r↪⇘pfs valid_edge a' kind a' = Q':r'↪⇘p'fs'
    sourcenode a = sourcenode a' pred (kind a') s'
  show ?thesis by -(rule CFG_call_determ)
qed


lemma CFG_call_edge_param_in:
  assumes "valid_edge a" and "kind a = Q:r↪⇘pfs" and "i < length ins"
  and "(p,ins,outs)  set procs" and "pred (kind a) s" and "pred (kind a) s'"
  and "V  (ParamUses (sourcenode a))!i. state_val s V = state_val s' V"
  shows "state_val (transfer (kind a) s) (ins!i) = 
         state_val (transfer (kind a) s') (ins!i)"
proof -
  from assms have params:"(params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"
    by(rule CFG_call_edge_params)
  from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
  have [simp]:"(THE ins. outs. (p,ins,outs)  set procs) = ins"
    by(rule formal_in_THE)
  from pred (kind a) s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from pred (kind a) s' obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
    by(cases s') auto
  from kind a = Q:r↪⇘pfs
  have eqs:"fst (hd (transfer (kind a) s)) = (Map.empty(ins [:=] params fs (fst cf)))"
    "fst (hd (transfer (kind a) s')) = (Map.empty(ins [:=] params fs (fst cf')))"
    by simp_all
  from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
  have "length fs = length ins" by(rule CFG_call_edge_length)
  from (p,ins,outs)  set procs have "distinct ins" by(rule distinct_formal_ins)
  with i < length ins length fs = length ins
  have "(Map.empty(ins [:=] params fs (fst cf))) (ins!i) = (params fs (fst cf))!i"
    "(Map.empty(ins [:=] params fs (fst cf'))) (ins!i) = (params fs (fst cf'))!i"
    by(fastforce intro:fun_upds_nth)+
  with eqs kind a = Q:r↪⇘pfs params
  show ?thesis by simp
qed


lemma CFG_call_edge_no_param:
  assumes "valid_edge a" and "kind a = Q:r↪⇘pfs" and "V  set ins"
  and "(p,ins,outs)  set procs" and "pred (kind a) s"
  shows "state_val (transfer (kind a) s) V = None"
proof -
  from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
  have [simp]:"(THE ins. outs. (p,ins,outs)  set procs) = ins"
    by(rule formal_in_THE)
  from pred (kind a) s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from V  set ins have "(Map.empty(ins [:=] params fs (fst cf))) V = None"
    by(auto dest:fun_upds_notin)
  with kind a = Q:r↪⇘pfs show ?thesis by simp
qed



lemma CFG_return_edge_param_out:
  assumes "valid_edge a" and "kind a = Q↩⇘pf" and "i < length outs"
  and "(p,ins,outs)  set procs" and "state_val s (outs!i) = state_val s' (outs!i)"
  and "s = cf#cfx#cfs" and "s' = cf'#cfx'#cfs'"
  shows "state_val (transfer (kind a) s) ((ParamDefs (targetnode a))!i) =
         state_val (transfer (kind a) s') ((ParamDefs (targetnode a))!i)"
proof -
  from valid_edge a kind a = Q↩⇘pf (p,ins,outs)  set procs
  have [simp]:"(THE outs. ins. (p,ins,outs)  set procs) = outs"
    by(rule formal_out_THE)
  from valid_edge a kind a = Q↩⇘pf (p,ins,outs)  set procs s = cf#cfx#cfs
  have transfer:"fst (hd (transfer (kind a) s)) = 
    (fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf) outs)"
    by(fastforce intro:CFG_return_edge_fun)
  from valid_edge a kind a = Q↩⇘pf (p,ins,outs)  set procs s' = cf'#cfx'#cfs'
  have transfer':"fst (hd (transfer (kind a) s')) = 
    (fst cfx')(ParamDefs (targetnode a) [:=] map (fst cf') outs)"
    by(fastforce intro:CFG_return_edge_fun)
  from state_val s (outs!i) = state_val s' (outs!i) i < length outs
    s = cf#cfx#cfs s' = cf'#cfx'#cfs'
  have "(fst cf) (outs!i) = (fst cf') (outs!i)" by simp
  from valid_edge a have "distinct (ParamDefs (targetnode a))"
    by(fastforce intro:distinct_ParamDefs)
  from valid_edge a kind a = Q↩⇘pf (p,ins,outs)  set procs
  have "length(ParamDefs (targetnode a)) = length outs"
    by(fastforce intro:ParamDefs_return_target_length)
  with i < length outs distinct (ParamDefs (targetnode a))
  have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf) outs)
    ((ParamDefs (targetnode a))!i) = (map (fst cf) outs)!i" 
    and "(fst cfx')(ParamDefs (targetnode a) [:=] map (fst cf') outs)
             ((ParamDefs (targetnode a))!i) = (map (fst cf') outs)!i"
    by(fastforce intro:fun_upds_nth)+
  with transfer transfer' (fst cf) (outs!i) = (fst cf') (outs!i) i < length outs
  show ?thesis by simp
qed


lemma CFG_slp_no_Def_equal:
  assumes "n -assl* n'" and "valid_edge a" and "a'  get_return_edges a"
  and "V  set (ParamDefs (targetnode a'))" and "preds (kinds (a#as@[a'])) s"
  shows "state_val (transfers (kinds (a#as@[a'])) s) V = state_val s V"
proof -
  from valid_edge a a'  get_return_edges a 
  obtain Q r p fs where "kind a = Q:r↪⇘pfs"
    by(fastforce dest!:only_call_get_return_edges)
  with valid_edge a a'  get_return_edges a obtain Q' f' where "kind a' = Q'↩⇘pf'"
    by(fastforce dest!:call_return_edges)
  from valid_edge a a'  get_return_edges a have "valid_edge a'"
    by(rule get_return_edges_valid)
  from preds (kinds (a#as@[a'])) s obtain cf cfs where [simp]:"s = cf#cfs"
    by(cases s,auto simp:kinds_def)
  from valid_edge a kind a = Q:r↪⇘pfs obtain ins outs 
    where "(p,ins,outs)  set procs" by(fastforce dest!:callee_in_procs)
  from kind a = Q:r↪⇘pfs obtain cfx where "transfer (kind a) s = cfx#cf#cfs"
    by simp
  moreover
  from n -assl* n' obtain cfx' 
    where "transfers (kinds as) (cfx#cf#cfs) = cfx'#cf#cfs"
    by(fastforce elim:slp_callstack_length_equal)
  moreover
  from kind a' = Q'↩⇘pf' valid_edge a' (p,ins,outs)  set procs
  have "fst (hd (transfer (kind a') (cfx'#cf#cfs))) = 
    (fst cf)(ParamDefs (targetnode a') [:=] map (fst cfx') outs)"
    by(simp,simp only:formal_out_THE,fastforce intro:CFG_return_edge_fun)
  ultimately have "fst (hd (transfers (kinds (a#as@[a'])) s)) = 
    (fst cf)(ParamDefs (targetnode a') [:=] map (fst cfx') outs)"
    by(simp add:kinds_def transfers_split)
  with V  set (ParamDefs (targetnode a')) show ?thesis
    by(simp add:fun_upds_notin)
qed



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

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


lemma CFG_intra_path_no_Def_equal:
  assumes "n -asι* n'" and "n  set (sourcenodes as). V  Def n"
  and "preds (kinds as) s"
  shows "state_val (transfers (kinds as) s) V = state_val s V"
proof -
  from n -asι* n' have "n -as→* n'" and "a  set as. intra_kind (kind a)"
    by(simp_all add:intra_path_def)
  from this n  set (sourcenodes as). V  Def n preds (kinds as) s
  have "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. aset as. intra_kind (kind a); 
                    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 aset (a#as). intra_kind (kind a)
    have "intra_kind (kind a)" and all':"aset as. intra_kind (kind a)"
      by auto
    from valid_edge a noDef intra_kind (kind a) pred (kind a) s
    have "state_val (transfer (kind a) s) V = state_val s V"
     by -(rule CFG_intra_edge_no_Def_equal)
    with IH[OF all' all preds (kinds as) (transfer (kind a) s)] show ?case
      by(simp add:kinds_def)
  qed
  thus ?thesis by blast
qed


lemma slpa_preds:
  "same_level_path_aux cs as; s = cfsx@cf#cfs; s' = cfsx@cf#cfs'; 
    length cfs = length cfs'; a  set as. valid_edge a; length cs = length cfsx; 
    preds (kinds as) s
   preds (kinds as) s'"
proof(induct arbitrary:s s' cf cfsx rule:slpa_induct)
  case (slpa_empty cs) thus ?case by(simp add:kinds_def)
next
  case (slpa_intra cs a as)
  note IH = s s' cf cfsx. s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; a  set as. valid_edge a; length cs = length cfsx; 
    preds (kinds as) s  preds (kinds as) s'
  from aset (a#as). valid_edge a have "valid_edge a"
    and "a  set as. valid_edge a" by simp_all
  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)
  show ?case
  proof(cases cfsx)
    case Nil
    with length cs = length cfsx have "length cs = length []" by simp
    from Nil s = cfsx@cf#cfs s' = cfsx@cf#cfs' intra_kind (kind a) 
    obtain cfx where "transfer (kind a) s = []@cfx#cfs"
      and "transfer (kind a) s' = []@cfx#cfs'"
      by(cases "kind a",auto simp:kinds_def intra_kind_def)
    from IH[OF this length cfs = length cfs' a  set as. valid_edge a
      length cs = length [] preds (kinds as) (transfer (kind a) s)]
    have "preds (kinds as) (transfer (kind a) s')" .
    moreover
    from Nil valid_edge a pred (kind a) s s = cfsx@cf#cfs s' = cfsx@cf#cfs'
      length cfs = length cfs'
    have "pred (kind a) s'" by(fastforce intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  next
    case (Cons x xs)
    with s = cfsx@cf#cfs s' = cfsx@cf#cfs' intra_kind (kind a)
    obtain cfx where "transfer (kind a) s = (cfx#xs)@cf#cfs"
      and "transfer (kind a) s' = (cfx#xs)@cf#cfs'"
      by(cases "kind a",auto simp:kinds_def intra_kind_def)
    from IH[OF this length cfs = length cfs' a  set as. valid_edge a _ 
      preds (kinds as) (transfer (kind a) s)] length cs = length cfsx Cons
    have "preds (kinds as) (transfer (kind a) s')" by simp
    moreover
    from Cons valid_edge a pred (kind a) s s = cfsx@cf#cfs s' = cfsx@cf#cfs'
      length cfs = length cfs' 
    have "pred (kind a) s'" by(fastforce intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  qed
next
  case (slpa_Call cs a as Q r p fs)
  note IH = s s' cf cfsx. s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; a  set as. valid_edge a; length (a#cs) = length cfsx;
    preds (kinds as) s  preds (kinds as) s'
  from aset (a#as). valid_edge a have "valid_edge a"
    and "a  set as. valid_edge a" by simp_all
  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 kind a = Q:r↪⇘pfs s = cfsx@cf#cfs s' = cfsx@cf#cfs' obtain cfx
    where "transfer (kind a) s = (cfx#cfsx)@cf#cfs"
    and "transfer (kind a) s' = (cfx#cfsx)@cf#cfs'" by(cases cfsx) auto
  from IH[OF this length cfs = length cfs' a  set as. valid_edge a _ 
    preds (kinds as) (transfer (kind a) s)] length cs = length cfsx
  have "preds (kinds as) (transfer (kind a) s')" by simp
  moreover
  from valid_edge a pred (kind a) s s = cfsx@cf#cfs s' = cfsx@cf#cfs'
    length cfs = length cfs' have "pred (kind a) s'" 
    by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
  ultimately show ?case by(simp add:kinds_def)
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = s s' cf cfsx. s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; a  set as. valid_edge a; length cs' = length cfsx; 
    preds (kinds as) s  preds (kinds as) s'
  from aset (a#as). valid_edge a have "valid_edge a"
    and "a  set as. valid_edge a" by simp_all
  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)
  show ?case
  proof(cases cs')
    case Nil
    with cs = c'#cs' s = cfsx@cf#cfs s' = cfsx@cf#cfs'
      length cs = length cfsx 
    obtain cf' where "s = cf'#cf#cfs" and "s' = cf'#cf#cfs'" by(cases cfsx) auto
    with kind a = Q↩⇘pf obtain cf'' where "transfer (kind a) s = []@cf''#cfs"
      and "transfer (kind a) s' = []@cf''#cfs'" by auto
    from IH[OF this length cfs = length cfs' a  set as. valid_edge a _ 
      preds (kinds as) (transfer (kind a) s)] Nil
    have "preds (kinds as) (transfer (kind a) s')" by simp
    moreover
    from valid_edge a pred (kind a) s s = cfsx@cf#cfs s' = cfsx@cf#cfs'
      length cfs = length cfs'  have "pred (kind a) s'" 
      by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  next
    case (Cons cx csx)
    with cs = c'#cs' length cs = length cfsx s = cfsx@cf#cfs s' = cfsx@cf#cfs'
    obtain x x' xs where "s = (x#x'#xs)@cf#cfs" and "s' = (x#x'#xs)@cf#cfs'"
      and "length xs = length csx"
      by(cases cfsx,auto,case_tac list,fastforce+)
    with kind a = Q↩⇘pf obtain cf' where "transfer (kind a) s = (cf'#xs)@cf#cfs"
      and "transfer (kind a) s' = (cf'#xs)@cf#cfs'"
      by fastforce
    from IH[OF this length cfs = length cfs' a  set as. valid_edge a _ 
      preds (kinds as) (transfer (kind a) s)] Cons length xs = length csx
    have "preds (kinds as) (transfer (kind a) s')" by simp
    moreover
    from valid_edge a pred (kind a) s s = cfsx@cf#cfs s' = cfsx@cf#cfs'
      length cfs = length cfs'  have "pred (kind a) s'" 
      by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  qed
qed


lemma slp_preds:
  assumes "n -assl* n'" and "preds (kinds as) (cf#cfs)" 
  and "length cfs = length cfs'"
  shows "preds (kinds as) (cf#cfs')"
proof -
  from n -assl* n' have "n -as→* n'" and "same_level_path_aux [] as"
    by(simp_all add:slp_def same_level_path_def)
  from n -as→* n' have "a  set as. valid_edge a" by(rule path_valid_edges)
  with same_level_path_aux [] as preds (kinds as) (cf#cfs) 
    length cfs = length cfs'
  show ?thesis by(fastforce elim!:slpa_preds)
qed
end


end