Theory CFG_Transfer

theory CFG_Transfer
  imports CFG_Def
begin

section ‹What each kind of edge does to the store›

text ‹
  Three transfers, one per thing an edge can do.  ‹edge_collect› runs an ordinary edge on a
  whole set of stores at once, by lifting the single-store \<^const>‹edge_step› pointwise ---
  derived from the concrete step rather than restated, so the two cannot drift apart.
  ‹call_enter› builds the callee's opening store: evaluate the actuals in the caller,
  reset the locals, bind the formals.  ‹combine_collect› does the reverse at a return:
  keep the callee's globals, restore the caller's locals, and write the callee's return
  value into the destination.

  All the payload comes from the edge itself, so none of these needs the procedure table.
›

definition edge_collect :: "edge_action ⇒ store set ⇒ store set" where
  "edge_collect a S = {t. ∃s∈S. t ∈ edge_step a s}"

lemma edge_collect_simps [simp]:
  "edge_collect EA_Nop S = S"
  "edge_collect (EA_Assign x a) S = {s(x := ⟦a⟧⇩e s) | s. s ∈ S}"
  "edge_collect (EA_Special sc x) S = {t. ∃s∈S. t ∈ special_step sc x s}"
  "edge_collect (EA_Assume b) S = {s. s ∈ S ∧ truthy (⟦b⟧⇩e s)}"
  "edge_collect (EA_AssumeNot b) S = {s. s ∈ S ∧ ¬ truthy (⟦b⟧⇩e s)}"
  "edge_collect (EA_Body p) S = S"
  "edge_collect (EA_Ret e p) S =
     {s(ret_var := (case e of None ⇒ s ret_var | Some a ⇒ ⟦a⟧⇩e s)) | s. s ∈ S}"
  "edge_collect (EA_Check l c) S = S"
  unfolding edge_collect_def by (auto split: if_splits)

lemma edge_collect_single:
  "edge_collect a {s} = edge_step a s"
  by (cases a) (auto split: if_splits)

lemma edge_collect_empty_set [simp]: "edge_collect a {} = {}"
  by (cases a) auto

lemma edge_collect_mono:
  assumes "S ⊆ T"
  shows "edge_collect a S ⊆ edge_collect a T"
  using assms by (cases a) auto

subsection ‹Return-value transfer›

text ‹Return-value rehydration at the caller: write the callee's ‹ret_var› into the
  destination over the combined store (callee globals, caller locals).  It is fixed by the
  call's destination ‹dst›, which the ‹CallEdge› already records --- no side lookup.›

definition combine_collect :: "(vname ⇒ bool) ⇒ vname option ⇒ store ⇒ store ⇒ store" where
  "combine_collect 𝒢 dst s t = combine_assign dst (t ret_var) (combine_env 𝒢 s t)"

subsection ‹Call-entry transfer›

text ‹Caller-side entry transfer at a call.  The actuals are evaluated in the caller store,
  the callee locals are reset (\<^const>‹enter_state›, globals preserved), and the resulting
  values are bound to the callee formals.  All payload comes from the ‹CallEdge›, so the
  transfer needs no procedure table.  This is exactly the entered store produced by the
  source \<^const>‹pstep› ‹Call› rule.›

definition call_enter :: "(vname ⇒ bool) ⇒ call_action ⇒ store ⇒ store" where
  "call_enter 𝒢 ca s =
     (case ca of CallEdge dst pars actuals ⇒
        enter_binding 𝒢 0 aval pars actuals s)"

lemma call_enter_CallEdge:
  "call_enter 𝒢 (CallEdge dst pars actuals) s
     = bind_formals pars (map (λe. ⟦e⟧⇩e s) actuals) (enter_state 𝒢 s)"
  by (simp add: call_enter_def enter_binding_def enter_state_def)

text ‹A parameterless call is exactly \<^const>‹enter_state›: no actuals to evaluate and no
  formals to bind.›
lemma call_enter_Nil [simp]:
  "call_enter 𝒢 (CallEdge dst [] []) s = enter_state 𝒢 s"
  by (simp add: call_enter_CallEdge)

subsection ‹What an edge reads and what it may change›

text ‹An edge reads the variables of its expressions. It may change only the
  variable it assigns, and a return only its result slot.›

definition edge_reads :: "edge_action ⇒ vname list" where
  "edge_reads a = sorted_list_of_set (⋃ (exp_vnames ` set (edge_expressions a)))"

fun edge_writes :: "edge_action ⇒ vname list" where
  "edge_writes (EA_Assign x a) = [x]"
| "edge_writes (EA_Special sc x) = [x]"
| "edge_writes (EA_Ret e p) = [ret_var]"
| "edge_writes _ = []"

text ‹The frame each concrete step respects: a name outside its write set keeps
  its value. A call entry may only bind its formals, and a return takes every
  global from the callee except the destination it assigns.›

lemma edge_step_frame:
  "t ∈ edge_step a s ⟹ x ∉ set (edge_writes a) ⟹ t x = s x"
  by (cases a) (auto split: if_splits)

lemma call_enter_frame:
  "𝒢 x ⟹ x ∉ set pars ⟹ call_enter 𝒢 (CallEdge dst pars args) s x = s x"
  by (simp add: call_enter_CallEdge bind_formals_other enter_state_def)

lemma combine_collect_frame:
  "𝒢 x ⟹ dst ≠ Some x ⟹ combine_collect 𝒢 dst s t x = t x"
  by (cases dst) (auto simp: combine_collect_def)

subsection ‹Finite global footprints›

text ‹The declared globals among those names, as duplicate-free lists a
  transfer folds over to read or publish them.›

definition global_names_in :: "(vname ⇒ bool) ⇒ vname list ⇒ vname list" where
  "global_names_in G xs = remdups (filter G xs)"

lemma set_global_names_in [simp]:
  "set (global_names_in G xs) = {x ∈ set xs. G x}"
  by (simp add: global_names_in_def)

lemma distinct_global_names_in [simp]: "distinct (global_names_in G xs)"
  by (simp add: global_names_in_def)

definition globals_in_exp :: "(vname ⇒ bool) ⇒ exp ⇒ vname list" where
  "globals_in_exp G e = global_names_in G (sorted_list_of_set (exp_vnames e))"

definition edge_global_reads :: "(vname ⇒ bool) ⇒ edge_action ⇒ vname list" where
  "edge_global_reads G a = global_names_in G (edge_reads a)"

definition edge_global_writes :: "(vname ⇒ bool) ⇒ edge_action ⇒ vname list" where
  "edge_global_writes G a = global_names_in G (edge_writes a)"

definition call_global_reads :: "(vname ⇒ bool) ⇒ exp list ⇒ vname list" where
  "call_global_reads G es = global_names_in G (sorted_list_of_set (⋃ (exp_vnames ` set es)))"

lemma set_edge_global_writes [simp]:
  "set (edge_global_writes G a) = {x ∈ set (edge_writes a). G x}"
  by (simp add: edge_global_writes_def)

lemma distinct_global_footprints [simp]:
  "distinct (globals_in_exp G e)"
  "distinct (edge_global_reads G a)"
  "distinct (edge_global_writes G a)"
  "distinct (call_global_reads G es)"
  by (simp_all add: globals_in_exp_def edge_global_reads_def edge_global_writes_def
    call_global_reads_def)

end