Theory Example_Compile_Call_Free

section ‹Call-free sources compile to a flat graph›

theory Example_Compile_Call_Free
  imports "Voblint_Compile.Compile_Wellformed"
begin

text ‹
  A \<^const>‹Call› naming a \<^const>‹special_table› entry compiles to an intra edge, not a
  \<^const>‹CallEdge›, so the syntactic condition under which a compiled graph carries no
  call edges is not ‹no Call node› but ‹no call to a compiled procedure›.
  ‹no_proc_call› below is that condition: it is what a whole-program \<^const>‹calls›-emptiness
  claim rests on, in place of evaluating the compiled set.
›

primrec no_proc_call :: "'a acom ⇒ bool" where
  "no_proc_call (SKIP _) = True"
| "no_proc_call (Assign _ x a) = True"
| "no_proc_call (Check _ l c) = True"
| "no_proc_call (Seq c1 c2) = (no_proc_call c1 ∧ no_proc_call c2)"
| "no_proc_call (If _ b c1 c2) = (no_proc_call c1 ∧ no_proc_call c2)"
| "no_proc_call (While _ b c) = no_proc_call c"
| "no_proc_call (Call _ dst q actuals) = (special_table q ≠ None)"
| "no_proc_call (Return _ e) = True"
| "no_proc_call (Restore _) = True"
| "no_proc_call (Unwind _) = True"

lemma compile_no_proc_call_K_empty:
  "compile Π p c k n = (n', en, E, K) ⟹ no_proc_call c ⟹ K = {}"
proof (induction c arbitrary: k n n' en E K)
  case (Seq c1 c2)
  from Seq.prems(1) obtain n1 en1 E1 K1 n2 en2 E2 K2 where
      c1: "compile Π p c1 (Statement (n + csize c1)) n = (n1, en1, E1, K1)"
    and c2: "compile Π p c2 k (n + csize c1) = (n2, en2, E2, K2)"
    and K: "K = K1 ∪ K2"
    by (auto simp: Let_def split: prod.splits)
  show ?case using Seq.IH(1)[OF c1] Seq.IH(2)[OF c2] Seq.prems(2) K by simp
next
  case (If i b c1 c2)
  from If.prems(1) obtain n1 en1 E1 K1 n2 en2 E2 K2 where
      c1: "compile Π p c1 k (Suc n) = (n1, en1, E1, K1)"
    and c2: "compile Π p c2 k n1 = (n2, en2, E2, K2)"
    and K: "K = K1 ∪ K2"
    by (auto simp: Let_def split: prod.splits)
  show ?case using If.IH(1)[OF c1] If.IH(2)[OF c2] If.prems(2) K by simp
next
  case (While i b c)
  from While.prems(1) obtain n1 en1 E1 K1 where
      c1: "compile Π p c (Statement n) (Suc n) = (n1, en1, E1, K1)"
    and K: "K = K1"
    by (auto simp: Let_def split: prod.splits)
  show ?case using While.IH[OF c1] While.prems(2) K by simp
next
  case (Call i dst q actuals)
  then show ?case by (auto split: option.splits)
qed auto

lemma compile_proc_no_proc_call_K_empty:
  "compile_proc Π p decl n = (n', E, K) ⟹ no_proc_call (body decl) ⟹ K = {}"
  unfolding compile_proc_def
  by (auto simp: Let_def split: prod.splits dest: compile_no_proc_call_K_empty)

lemma compile_procs_no_proc_call_K_empty:
  assumes "compile_procs Π ps n = (n', E, K)"
    and "⋀q decl. q ∈ set ps ⟹ Π q = Some decl ⟹ no_proc_call (body decl)"
  shows "K = {}"
  using compile_procs_calls_origin[OF assms(1)] assms(2) compile_proc_no_proc_call_K_empty
  by blast

theorem compile_prog_calls_empty:
  assumes main_free: "no_proc_call (main_body Π)"
      and procs_free: "⋀q decl. q ∈ set ps ⟹ Π q = Some decl ⟹ no_proc_call (body decl)"
  shows "calls (compile_prog Π ps) = {}"
proof -
  obtain n1 Eprocs Kprocs n2 Emain Kmain where
      procs: "compile_procs Π ps 0 = (n1, Eprocs, Kprocs)"
    and mainc: "compile_proc Π prog_main_name
        ⦇formals = [], body = main_body Π⦈ n1
      = (n2, Emain, Kmain)"
    and g: "calls (compile_prog Π ps) = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  show ?thesis unfolding g
    using compile_procs_no_proc_call_K_empty[OF procs procs_free]
      compile_proc_no_proc_call_K_empty[OF mainc] main_free by simp
qed

end