Theory Compile_Regression

theory Compile_Regression
  imports "Voblint_Compile.Compile_Invariants"
begin

section ‹Compiler regressions›

text ‹
  Two facts about the edges ‹compile› emits, moved out of ‹Compile_Invariants›: nothing
  in the core uses them, and the build is what keeps them true.
›

subsection ‹Returns and self-calls›

text ‹Both branches of a conditional return keep their own result edge, and a self-call of
  an ordinary procedure is a call edge into its own entry.›
theorem compile_multi_return_converge:
  assumes "compile Π p (If () b (Return () e1) (Return () e2)) k n = (n', en, E, K)"
  shows "(∃j. (Statement j, EA_Ret e1 p, FunctionResult p) ∈ E)
       ∧ (∃j. (Statement j, EA_Ret e2 p, FunctionResult p) ∈ E)"
  using compile_return_edge[OF assms, of e1] compile_return_edge[OF assms, of e2] by simp

text ‹A self-call targets the procedure's own entry node; its call site is an ordinary
  statement node and its continuation is the caller's own next program point.  Restricted to
  ‹p› classified as an ordinary procedure: a self-call \<^const>‹special_table› classifies
  instead sits on an intra edge, not a \<^const>‹CallEdge›.›
theorem compile_self_call_edge:
  assumes "special_table p = None"
  shows "(Statement n, CallEdge None (call_formals Π p) [], FunctionEntry p, k)
           ∈ snd (snd (snd (compile Π p (Call () None p []) k n)))"
  using assms by simp

end