Theory CFG_Prune

theory CFG_Prune
  imports CFG_Transfer
begin

section ‹Procedure-aware structural reachability›

text ‹
  ‹cfg_succ_rel› is the derived structural dependency graph the analysis pruning and
  cone proofs run on --- not the concrete execution relation.  It has four sources,
  induced by ‹intra g› and ‹calls g›:

  ▪ INTRA: an ordinary edge ‹(u, a, v) ∈ intra g› gives ‹u → v› (ordinary flow).
  ▪ ENTRY: a call ‹(c, ca, FunctionEntry p, k) ∈ calls g› gives ‹c → FunctionEntry p› ---
    the callee entry's abstract state depends on the caller state routed through
    the analysis's own enter operation.
  ▪ ‹COMB_CALLER›: the same call gives ‹c → k› --- the continuation depends on the saved
    caller state via \<^const>‹combine_collect›.  This is not a concrete execution edge; execution
    does not skip the callee.
  ▪ ‹COMB_RESULT›: the same call gives ‹FunctionResult p → k› --- the continuation depends
    on the callee's result, \<^const>‹combine_collect›'s callee-exit argument.

  ‹c → k› and ‹FunctionResult p → k› are combine dependencies of the analysis, kept
  visibly separate from ‹intra g›.  They are never added to ‹intra g›.
›

subsection ‹The structural successor relation›

definition cfg_succ_rel :: "cfg ⇒ (cfg_node × cfg_node) set" where
  "cfg_succ_rel g =
     {(u, v) | u a v. (u, a, v) ∈ intra g}
   ∪ {(c, ce) | c ca ce k. (c, ca, ce, k) ∈ calls g}
   ∪ {(c, k) | c ca ce k. (c, ca, ce, k) ∈ calls g}
   ∪ {(FunctionResult p, k) | c ca p k. (c, ca, FunctionEntry p, k) ∈ calls g}"

lemma cfg_succ_rel_intra:
  "(u, a, v) ∈ intra g ⟹ (u, v) ∈ cfg_succ_rel g"
  unfolding cfg_succ_rel_def by blast

lemma cfg_succ_rel_entry:
  "(c, ca, ce, k) ∈ calls g ⟹ (c, ce) ∈ cfg_succ_rel g"
  unfolding cfg_succ_rel_def by blast

lemma cfg_succ_rel_comb_caller:
  "(c, ca, ce, k) ∈ calls g ⟹ (c, k) ∈ cfg_succ_rel g"
  unfolding cfg_succ_rel_def by blast

lemma cfg_succ_rel_comb_result:
  "(c, ca, FunctionEntry p, k) ∈ calls g ⟹ (FunctionResult p, k) ∈ cfg_succ_rel g"
  unfolding cfg_succ_rel_def by blast

lemma cfg_succ_rel_cases:
  assumes "(y, z) ∈ cfg_succ_rel g"
  obtains (INTRA) a where "(y, a, z) ∈ intra g"
    | (ENTRY) ca k where "(y, ca, z, k) ∈ calls g"
    | (COMB_CALLER) ca ce where "(y, ca, ce, z) ∈ calls g"
    | (COMB_RESULT) c ca p k where "(c, ca, FunctionEntry p, k) ∈ calls g"
                                   "y = FunctionResult p" "z = k"
  using assms unfolding cfg_succ_rel_def by blast

subsection ‹Reachability: reflexive-transitive closure of the successor relation›

text ‹Reachability over that successor relation.  Because the relation already relates a
  caller to its continuation and a callee result to the same continuation, this closure
  crosses procedure boundaries without any separate interprocedural notion.›
definition cfg_reaches :: "cfg ⇒ cfg_node ⇒ cfg_node ⇒ bool" where
  "cfg_reaches g v v0 ⟷ (v, v0) ∈ (cfg_succ_rel g)⇧*"

subsection ‹Reachability inside one activation›

text ‹The same closure without entering callees: a call site steps straight to its
  continuation.  These are the steps a routed equation reads backwards, so this is the
  reachability the solver's coverage argument needs.›

definition local_succ_rel :: "cfg ⇒ (cfg_node × cfg_node) set" where
  "local_succ_rel g =
     {(u, v). ∃a. (u, a, v) ∈ intra g}
     ∪ {(u, k). ∃ca q. (u, ca, FunctionEntry q, k) ∈ calls g}"

definition local_reaches :: "cfg ⇒ cfg_node ⇒ cfg_node ⇒ bool" where
  "local_reaches g u v ⟷ (u, v) ∈ (local_succ_rel g)⇧*"

lemma local_reaches_refl [simp]: "local_reaches g v v"
  by (simp add: local_reaches_def)

lemma local_reaches_trans:
  "local_reaches g u v ⟹ local_reaches g v w ⟹ local_reaches g u w"
  unfolding local_reaches_def by (rule rtrancl_trans)

lemma local_reaches_intra_step:
  "(u, a, v) ∈ intra g ⟹ local_reaches g v w ⟹ local_reaches g u w"
  unfolding local_reaches_def local_succ_rel_def
  by (rule converse_rtrancl_into_rtrancl) blast+

lemma local_reaches_comb_step:
  "(u, ca, FunctionEntry q, k) ∈ calls g ⟹ local_reaches g k w ⟹ local_reaches g u w"
  unfolding local_reaches_def local_succ_rel_def
  by (rule converse_rtrancl_into_rtrancl) blast+

lemma local_reaches_cfg_reaches:
  "local_reaches g u v ⟹ cfg_reaches g u v"
  unfolding local_reaches_def cfg_reaches_def
proof (induction rule: rtrancl_induct)
  case (step y z)
  then have "(y, z) ∈ cfg_succ_rel g"
    unfolding local_succ_rel_def by (auto simp: cfg_succ_rel_intra cfg_succ_rel_comb_caller)
  with step.IH show ?case by (rule rtrancl_into_rtrancl)
qed simp

end