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↪⇘p⇙fs; (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'↩⇘p⇙f'; (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↪⇘p⇙fs; (p,ins,outs) ∈ set procs; V ∈ set ins⟧
⟹ V ∈ Def (targetnode a)"
and call_source_Def_empty:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ 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↩⇘p⇙f; (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↪⇘p⇙fs; (p,ins,outs) ∈ set procs⟧
⟹ length fs = length ins"
and CFG_call_determ:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; 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↪⇘p⇙fs; 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'↩⇘p⇙f'; (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↪⇘p⇙fs" 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↪⇘p⇙fs› ‹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↪⇘p⇙fs" 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↪⇘p⇙fs› ‹(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↪⇘p⇙fs›
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↪⇘p⇙fs› ‹(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↪⇘p⇙fs› params
show ?thesis by simp
qed
lemma CFG_call_edge_no_param:
assumes "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" 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↪⇘p⇙fs› ‹(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↪⇘p⇙fs› show ?thesis by simp
qed
lemma CFG_return_edge_param_out:
assumes "valid_edge a" and "kind a = Q↩⇘p⇙f" 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↩⇘p⇙f› ‹(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↩⇘p⇙f› ‹(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↩⇘p⇙f› ‹(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↩⇘p⇙f› ‹(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 -as→⇘sl⇙* 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↪⇘p⇙fs"
by(fastforce dest!:only_call_get_return_edges)
with ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
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↪⇘p⇙fs› obtain ins outs
where "(p,ins,outs) ∈ set procs" by(fastforce dest!:callee_in_procs)
from ‹kind a = Q:r↪⇘p⇙fs› obtain cfx where "transfer (kind a) s = cfx#cf#cfs"
by simp
moreover
from ‹n -as→⇘sl⇙* 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'↩⇘p⇙f'› ‹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. ⟦∀a∈set as. intra_kind (kind a);
∀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 ‹∀a∈set (a#as). intra_kind (kind a)›
have "intra_kind (kind a)" and all':"∀a∈set 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 ‹∀a∈set (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 ‹∀a∈set (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↪⇘p⇙fs› ‹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 ‹∀a∈set (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↩⇘p⇙f› 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↩⇘p⇙f› 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 -as→⇘sl⇙* n'" and "preds (kinds as) (cf#cfs)"
and "length cfs = length cfs'"
shows "preds (kinds as) (cf#cfs')"
proof -
from ‹n -as→⇘sl⇙* 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