Theory CFG_Def

theory CFG_Def
  imports "Voblint_VIMP.VIMP_Proc" "HOL-Library.Countable"
begin

section ‹Procedure-aware control-flow graph›

text ‹
  A ‹cfg› is an interprocedural control-flow graph over two disjoint transition
  relations, one per phenomenon:
    ▪ ‹intra› --- ordinary context-preserving flow, labelled by an ‹edge_action› that is
      a total within-context store transformer.  Executed by ‹edge_step›.
    ▪ ‹calls› --- context-crossing calls, labelled by a ‹call_action› and carrying the
      call-site, the callee entry node, and the continuation node.

  Nodes are procedure-aware: ‹FunctionEntry p› and ‹FunctionResult p› are first-class
  nodes, not keyed side slots.  There is no global exit node and no call/return matching
  side relation: a call edge already names its callee entry and its continuation, and a
  return is an ordinary intra edge into ‹FunctionResult p›.  Calls carry incompatible
  typing from intra flow, so ‹edge_step› has no call case and ‹intra› can never carry a
  call --- by typing, not by a side condition.

  Translation from VIMP to CFG and the collecting/equation layers ride on this structure.
›

subsection ‹Nodes›

datatype cfg_node =
    Statement (node_stmt: nat)
  | FunctionEntry (entry_proc: pname)
  | FunctionResult (result_proc: pname)

instance cfg_node :: countable
  by countable_datatype

text ‹The solver unknown for a program point is a CFG node.  Analysis-facing code keeps the
  short name ‹pp› for it; a return node is \<^term>‹FunctionResult p›, a callee entry
  \<^term>‹FunctionEntry p›, an ordinary location \<^term>‹Statement n›.›
type_synonym pp = cfg_node

subsection ‹Edge actions and call actions›

text ‹
  ‹edge_action› labels intra flow.  It has no call constructor: every action is a total
  store transformer within one activation, so an intra edge can never denote a call.  A
  ‹EA_Ret e p› writes the return value into ‹ret_var› in the callee's own context; its
  graph target is ‹FunctionResult p› (enforced by ‹wf_cfg›), which is why return
  summarisation is ordinary predecessor folding over ‹FunctionResult p›.

  ‹EA_Body p› labels the one edge leaving ‹FunctionEntry p›, so an activation's
  first step inside the callee is distinguishable from an ordinary ‹EA_Nop›.
  Concretely it is the identity: a VIMP procedure declares no locals beyond its
  formals, which the call already bound. It exists so that an analysis has a
  transition to attach procedure-entry work to --- Goblint runs ‹body› on
  exactly this edge --- and it carries the procedure name because that work is
  per-procedure.

  ‹call_action› labels call edges.  ‹CallEdge dst formals args› records the caller
  destination variable, the callee's formal parameter names, and the actual arguments; the
  callee identity and the continuation are the two target nodes of the ‹calls› tuple, not
  payload of the action.  Carrying ‹formals› on the edge lets the caller-side entry transfer
  ‹call_enter› bind actuals to formals without consulting a procedure table, keeping the
  trace kernel independent of the source declaration environment.
›

datatype edge_action =
    EA_Nop
  | EA_Assign   (ea_var: vname) (ea_rhs: exp)
  | EA_Special  (ea_special_op: special_call) (ea_special_dst: vname)
  | EA_Assume    (ea_cond: exp)
  | EA_AssumeNot (ea_cond: exp)
  | EA_Body     (ea_body_proc: pname)
  | EA_Ret      (ea_ret_val: "exp option") (ea_ret_proc: pname)
  | EA_Check    (ea_check_label: check_label) (ea_check_cond: exp)

datatype call_action =
    CallEdge (ce_dst: "vname option") (ce_formals: "vname list") (ce_args: "exp list")

instance edge_action :: countable
  by countable_datatype

instance call_action :: countable
  by countable_datatype

text ‹
  ‹call_info› is the call-boundary metadata an interprocedural transfer may consult: the
  caller destination, the callee, its formals, and the actual arguments.  Goblint's
  ‹Analyses.Spec› hands the same four to both halves of its return protocol --
  ‹combine_env man lval fexp f args fc au ask› and ‹combine_assign› with the identical
  argument shape -- so a transfer that only ever sees the caller and callee-exit states is
  strictly weaker than that interface.  The call site and the callee-exit point are the
  combine tree's own two program-point arguments, so they are not duplicated here.

  Goblint's ‹fexp› has no separate counterpart: VIMP calls a statically named procedure, so
  ‹ci_callee› already carries what the call expression identifies.  The callee context ‹fc›
  belongs to the routed-analysis layer rather than to a transfer-record field, and
  ‹Queries.ask› over the callee exit has none: there is no query bus.
›
record call_info =
  ci_dst     :: "vname option"
  ci_callee  :: pname
  ci_formals :: "vname list"
  ci_args    :: "exp list"

definition call_info_of :: "call_action ⇒ pname ⇒ call_info" where
  "call_info_of ca p =
     ⦇ ci_dst = ce_dst ca, ci_callee = p,
       ci_formals = ce_formals ca, ci_args = ce_args ca ⦈"

lemma call_info_of_simps [simp]:
  "ci_dst (call_info_of ca p) = ce_dst ca"
  "ci_callee (call_info_of ca p) = p"
  "ci_formals (call_info_of ca p) = ce_formals ca"
  "ci_args (call_info_of ca p) = ce_args ca"
  by (simp_all add: call_info_of_def)

subsection ‹CFG record: two relations›

text ‹
  ‹calls› is a four-place relation ‹(call_site, act, callee_entry, continuation)›: the
  callee entry and the continuation are ordinary nodes, kept explicit so no matching side
  relation is needed.  The flat (call-free) CFG is exactly the ‹calls = {}› fragment, so
  every fact quantified over ‹intra› is verbatim a flat-CFG fact.
›

record cfg =
  intra     :: "(cfg_node × edge_action × cfg_node) set"
  calls     :: "(cfg_node × call_action × cfg_node × cfg_node) set"
  cfg_entry :: cfg_node

subsection ‹Intra edge execution›

text ‹
  ‹special_step› is ‹special_call›'s own step function, factored out of ‹edge_step›
  so that extending the special-call vocabulary only touches this function (via
  ‹special_result›, shared with the source small-step semantics) and
  ‹special_step_nonempty› below, not every generic lemma stated over ‹edge_action›.
  ‹Nondet_Int› havocs the destination; ‹Min›/‹Max› write exactly one, deterministic
  value, so no single equation characterizes every ‹sc› uniformly any more --
  callers reasoning about an as-yet-unclassified ‹sc› case-split on it instead.
›

fun special_step :: "special_call ⇒ vname ⇒ store ⇒ store set" where
  "special_step sc x s = {s(x := v) |v. special_result sc s v}"

lemma special_step_nonempty [simp]: "special_step sc x s ≠ {}"
  by (cases sc) auto

text ‹‹edge_step› is the single primitive semantics of an intra action.  It is defined for
  every constructor and has no call case; guards are the only source of an empty result.›

fun edge_step :: "edge_action ⇒ store ⇒ store set" where
  "edge_step EA_Nop s = {s}"
| "edge_step (EA_Assign x a) s = {s(x := ⟦a⟧⇩e s)}"
| "edge_step (EA_Special sc x) s = special_step sc x s"
| "edge_step (EA_Assume b) s = (if truthy (⟦b⟧⇩e s) then {s} else {})"
| "edge_step (EA_AssumeNot b) s = (if truthy (⟦b⟧⇩e s) then {} else {s})"
| "edge_step (EA_Body p) s = {s}"
| "edge_step (EA_Ret e p) s =
     {s(ret_var := (case e of None ⇒ s ret_var | Some a ⇒ ⟦a⟧⇩e s))}"
| "edge_step (EA_Check l c) s = {s}"

subsection ‹Intra-only execution paths›

text ‹
  ‹intra_path› is the reflexive-transitive closure of \<^const>‹edge_step› along \<^const>‹intra›
  edges, on ‹(node, store)› pairs.  It deliberately excludes \<^const>‹calls›: an intra path
  never pushes or pops an activation, so it lifts to the collecting semantics without any
  stack-representation side condition, and to a stack-preserving CFG run at any stack.
›

text ‹One intra transition on a ‹(node, store)› pair.  ‹intra_path› is its \<^const>‹star›, so
  reflexivity, transitivity and the induction rule come from \<^theory>‹HOL-IMP.Star› rather than
  from a bespoke closure.  The name avoids ‹intra_step›, which is the ∗‹source›-level
  \<^const>‹pstep› fragment.›

definition cfg_intra_step :: "cfg ⇒ cfg_node × store ⇒ cfg_node × store ⇒ bool" where
  "cfg_intra_step g p q ⟷
     (∃a. (fst p, a, fst q) ∈ intra g ∧ snd q ∈ edge_step a (snd p))"

abbreviation intra_path :: "cfg ⇒ cfg_node × store ⇒ cfg_node × store ⇒ bool" where
  "intra_path g ≡ star (cfg_intra_step g)"

lemma cfg_intra_stepI [intro]:
  "(u, a, v) ∈ intra g ⟹ s' ∈ edge_step a s ⟹ cfg_intra_step g (u, s) (v, s')"
  by (auto simp: cfg_intra_step_def)

lemma cfg_intra_stepE [elim]:
  assumes "cfg_intra_step g (u, s) (v, s')"
  obtains a where "(u, a, v) ∈ intra g" "s' ∈ edge_step a s"
  using assms by (auto simp: cfg_intra_step_def)

lemma intra_path_single:
  "(u, a, v) ∈ intra g ⟹ s' ∈ edge_step a s ⟹ intra_path g (u, s) (v, s')"
  by (intro star_step1 cfg_intra_stepI)

lemma intra_path_nop:
  "(u, EA_Nop, v) ∈ intra g ⟹ intra_path g (u, s) (v, s)"
  by (rule intra_path_single[where a = EA_Nop]) simp_all


subsection ‹Node set (derived, not stored)›

text ‹‹cfg_nodes› is reconstructed from the endpoints of ‹intra›, every node occurring in
  ‹calls›, and ‹cfg_entry›.  It is not a record field.›

definition cfg_nodes :: "cfg ⇒ cfg_node set" where
  "cfg_nodes g =
     {u. ∃a v. (u, a, v) ∈ intra g}
     ∪ {v. ∃u a. (u, a, v) ∈ intra g}
     ∪ {u. ∃act ce after. (u, act, ce, after) ∈ calls g}
     ∪ {ce. ∃u act after. (u, act, ce, after) ∈ calls g}
     ∪ {after. ∃u act ce. (u, act, ce, after) ∈ calls g}
     ∪ {cfg_entry g}"

text ‹Whole-program completion is the entry procedure's ‹FunctionResult›.  A graph whose
  entry is not a procedure entry is never compiled; the fallback keeps the function total
  and aborts in generated code.›
definition cfg_exit :: "cfg ⇒ cfg_node" where
  "cfg_exit g =
    (case cfg_entry g of
       FunctionEntry p ⇒ FunctionResult p
     | n ⇒ Code.abort (STR ''cfg_exit: entry is not a procedure entry'') (λ_. n))"

subsection ‹Well-formedness›

text ‹‹wf_cfg› is structural only: call edges enter procedure-entry nodes; no intra edge
  enters a procedure-entry node (so a callee is reached only across a call); and a return
  action lands on the matching procedure result.  No compiler-correctness or
  source-semantic property is included.›

definition wf_cfg :: "cfg ⇒ bool" where
  "wf_cfg g ⟷
     (∀u act ce after. (u, act, ce, after) ∈ calls g ⟶ (∃p. ce = FunctionEntry p))
   ∧ (∀u a v. (u, a, v) ∈ intra g ⟶ (∀p. v ≠ FunctionEntry p))
   ∧ (∀u e p v. (u, EA_Ret e p, v) ∈ intra g ⟶ v = FunctionResult p)"

text ‹‹calls_source_unique› is a separate, optional side condition: one call edge per
  call site.  ‹wf_cfg› does not include it, and the collecting semantics never needs it ---
  both the return clause and the context semantics name an edge by its effect.  A solved
  routed table does need it, to match the edge a return reads against the one its callee
  was entered through; compiled programs satisfy it by construction.›

definition calls_source_unique :: "cfg ⇒ bool" where
  "calls_source_unique g ⟷
     (∀u ca1 ce1 af1 ca2 ce2 af2.
        (u, ca1, ce1, af1) ∈ calls g ⟶ (u, ca2, ce2, af2) ∈ calls g
        ⟶ ca1 = ca2 ∧ ce1 = ce2 ∧ af1 = af2)"

lemma calls_source_unique_edgesD:
  assumes "calls_source_unique g"
    and "(u, ca1, ce1, af1) ∈ calls g" and "(u, ca2, ce2, af2) ∈ calls g"
  shows "ca1 = ca2" and "ce1 = ce2" and "af1 = af2"
  using assms unfolding calls_source_unique_def by blast+

subsection ‹Structural invariants›

text ‹What holds of a graph's node set no matter where the graph came from: an edge's
  endpoints are nodes, and finitely many edges give finitely many nodes.  Both are read off
  the definition of ‹cfg_nodes›, which is why they need no well-formedness assumption.›
lemma intra_endpoints_in_nodes:
  assumes "(u, a, v) ∈ intra g"
  shows "u ∈ cfg_nodes g" and "v ∈ cfg_nodes g"
  using assms by (auto simp: cfg_nodes_def)

lemma call_endpoints_in_nodes:
  assumes "(u, act, ce, after) ∈ calls g"
  shows "u ∈ cfg_nodes g" and "ce ∈ cfg_nodes g" and "after ∈ cfg_nodes g"
  using assms by (auto simp: cfg_nodes_def)

text ‹Each of the five ‹cfg_nodes› disjuncts is a projection of ‹intra g› or ‹calls g›,
  so it inherits their finiteness as a finite image; the sixth is a singleton.›
lemma cfg_nodes_finite:
  assumes "finite (intra g)" and "finite (calls g)"
  shows "finite (cfg_nodes g)"
proof -
  have "{u. ∃a v. (u, a, v) ∈ intra g} = (λ(u, a, v). u) ` intra g"
    and "{v. ∃u a. (u, a, v) ∈ intra g} = (λ(u, a, v). v) ` intra g"
    by force+
  moreover
  have "{u. ∃act ce after. (u, act, ce, after) ∈ calls g} = (λ(u, act, ce, after). u) ` calls g"
    and "{ce. ∃u act after. (u, act, ce, after) ∈ calls g} = (λ(u, act, ce, after). ce) ` calls g"
    and "{after. ∃u act ce. (u, act, ce, after) ∈ calls g}
           = (λ(u, act, ce, after). after) ` calls g"
    by force+
  ultimately show ?thesis
    unfolding cfg_nodes_def using assms by simp
qed

subsection ‹Executable orders›

text ‹Structural orders make @{const sorted_list_of_set} a deterministic executable
  enumeration of intra and call relations. They affect only solver representation, not
  CFG semantics. ‹exp› already derives ‹linorder› in \<^theory>‹Voblint_VIMP.VIMP_Syntax›.›
derive linorder special_call
derive linorder edge_action
derive linorder call_action
derive linorder cfg_node

subsection ‹Executable enumeration›

text ‹Stable list views for the TD bridge: the intra and call edge sets sorted by their
  structural order. Both guard on \<^term>‹finite (intra g)›/\<^term>‹finite (calls g)›:
  every compiled graph satisfies it, so the \<^const>‹Code.abort› branch never fires in
  practice, and names the violation instead of failing on an uninformative
  \<^const>‹sorted_list_of_set› pattern-match error. Placed here rather than in the
  framework session's own equation-generation enumerations, so any consumer of this session alone
  --- a compiled graph's ‹finite_cfg› interpretation among them --- gets them for free.›

definition cfg_intra_list :: "cfg ⇒ (cfg_node × edge_action × cfg_node) list" where
  "cfg_intra_list g =
     (if finite (intra g) then sorted_list_of_set (intra g)
      else Code.abort (STR ''cfg_intra_list: infinite intra edge set'') (λ_. []))"

lemma cfg_intra_list_code [code]:
  "cfg_intra_list g = sorted_list_of_set (intra g)"
  unfolding cfg_intra_list_def by (cases "finite (intra g)") auto

definition cfg_calls_list ::
    "cfg ⇒ (cfg_node × call_action × cfg_node × cfg_node) list" where
  "cfg_calls_list g =
     (if finite (calls g) then sorted_list_of_set (calls g)
      else Code.abort (STR ''cfg_calls_list: infinite calls edge set'') (λ_. []))"

lemma cfg_calls_list_code [code]:
  "cfg_calls_list g = sorted_list_of_set (calls g)"
  unfolding cfg_calls_list_def by (cases "finite (calls g)") auto

lemma set_cfg_intra_list [simp]:
  "finite (intra g) ⟹ set (cfg_intra_list g) = intra g"
  unfolding cfg_intra_list_def by simp

lemma set_cfg_calls_list [simp]:
  "finite (calls g) ⟹ set (cfg_calls_list g) = calls g"
  unfolding cfg_calls_list_def by simp

text ‹Every \<^const>‹cfg_nodes› element, listed once: the intra endpoints, the call-site/
  callee-entry/continuation triples, and the distinguished entry, deduplicated. This is the
  canonical finite node enumeration a public per-node result table draws its key domain from,
  distinct from \<^const>‹cfg_intra_list›'s edge-indexed view.›

definition cfg_node_list :: "cfg ⇒ cfg_node list" where
  "cfg_node_list g =
     remdups
       (concat (map (λ(u, a, v). [u, v]) (cfg_intra_list g)) @
        concat (map (λ(u, act, ce, after). [u, ce, after]) (cfg_calls_list g)) @
        [cfg_entry g])"

lemma set_cfg_node_list [simp]:
  assumes "finite (intra g)" and "finite (calls g)"
  shows "set (cfg_node_list g) = cfg_nodes g"
  unfolding cfg_node_list_def cfg_nodes_def
  using set_cfg_intra_list[OF assms(1)] set_cfg_calls_list[OF assms(2)]
  by force

text ‹A ‹cfg› whose two transition relations are finite.  Bundles the two
  finiteness facts every enumeration and every compiled-graph interpretation
  needs, so a caller states one assumption instead of two, and ‹finite_nodes›
  becomes derivable rather than re-proved at each instance.›
locale finite_cfg =
  fixes g :: cfg
  assumes finite_intra [intro, simp]: "finite (intra g)"
    and finite_calls [intro, simp]: "finite (calls g)"
begin

lemma finite_nodes [simp]: "finite (cfg_nodes g)"
  by (rule cfg_nodes_finite) simp_all

end

text ‹Expressions observed by an edge, shared by diagnostics and transfer footprints.›

fun edge_expressions :: "edge_action ⇒ exp list" where
  "edge_expressions (EA_Assign x e) = [e]"
| "edge_expressions (EA_Assume e) = [e]"
| "edge_expressions (EA_AssumeNot e) = [e]"
| "edge_expressions (EA_Check l e) = [e]"
| "edge_expressions (EA_Ret (Some e) p) = [e]"
| "edge_expressions (EA_Special (Min a b) x) = [a, b]"
| "edge_expressions (EA_Special (Max a b) x) = [a, b]"
| "edge_expressions _ = []"

end