Theory Voblint_Compile.Compile_Invariants

theory Compile_Invariants
  imports Compile_Wellformed "Voblint_VIMP.VIMP_Program" "Voblint_CFG.CFG_Prune"
begin

section ‹What a program must satisfy, and what its graph then satisfies›

text ‹
  Two things live here.  ‹wf_compile_input› is the contract a source program has to meet
  before it is worth compiling: the procedure names are distinct, the entry procedure is
  declared and takes no arguments, and every body is a well-formed source command.
  ‹wf_program_compile_input_exec› is the executable form of that contract, and the check
  the command-line tool actually runs --- the contract itself quantifies over the whole
  procedure table, which no generated code can enumerate, so the executable form walks the
  declaration list instead and is proved sufficient.

  The remaining results are about the graph that comes out: a source \<^const>‹Return›
  compiles to an edge into its own \<^term>‹FunctionResult›, every statement index is listed
  in source post-order (‹prog_stmt_post_order›) so a report can name its source command,
  and the entry node reaches the exit.
›

subsection ‹Compiler input well-formedness›

text ‹‹prog_main_name› names the distinguished entry procedure, declared in ‹Π› with an
  empty formal list; ‹main_body Π› reads its body back out.  The callee list ‹ps› enumerates
  the other declared procedures (‹dom Π› minus ‹prog_main_name›), so the entry's nodes never
  collide with a callee's, yet ‹FunctionEntry prog_main_name› is an ordinary activation of a
  declared procedure like any other.›
definition wf_compile_input ::
  "(vname => bool) => 'a ptable => pname list => bool" where
  "wf_compile_input 𝒢 Π ps ⟷
     distinct ps ∧
     set ps = {p. Π p ~= None} - {prog_main_name} ∧
     prog_main_name ∉ set ps ∧
     wf_source_program 𝒢 Π"

text ‹The leaf definitions an executable instance unfolds to decide the contract.  No
  abstract proof unfolds them, so they only ever fire under ‹unfolding wf_compile_input_simps›.›
declare
  reserved_ret_var_def [wf_compile_input_simps]
  source_exp_def [wf_compile_input_simps]
  valid_formal_def [wf_compile_input_simps]
  value_providing_def [wf_compile_input_simps]
  special_table_def [wf_compile_input_simps]
  special_pname_nondet_int_def [wf_compile_input_simps]
  special_pname_min_def [wf_compile_input_simps]
  special_pname_max_def [wf_compile_input_simps]
  ret_var_def [wf_compile_input_simps]
  prog_main_name_def [wf_compile_input_simps]
  main_body_def [wf_compile_input_simps]

lemma wf_compile_inputD:
  assumes "wf_compile_input 𝒢 Π ps"
  shows "reserved_ret_var 𝒢" and "Π prog_main_name = Some ⦇formals = [], body = (main_body Π)⦈"
    and "wf_source_com Π (main_body Π)" and "no_return (main_body Π)"
    and "Π p = Some decl ⟹ wf_proc_decl 𝒢 Π decl"
    and "Π p = Some decl ⟹ special_table p = None"
    and "source_pi Π" and "source_com (main_body Π)"
    and "distinct ps" and "set ps = {p. Π p ≠ None} - {prog_main_name}"
    and "prog_main_name ∉ set ps"
  using wf_source_programD
    assms[unfolded wf_compile_input_def] by auto

lemmas wf_compile_input_reserved_ret_var [dest] = wf_compile_inputD(1)

abbreviation wf_program_compile_input :: "imp_prog ⇒ bool" where
  "wf_program_compile_input p ≡
    wf_compile_input (declared_global p) (prog_table p) (prog_procs p)"

subsection ‹An executable, sufficient reformulation›

text ‹
  ‹wf_source_program›'s two ‹∀p. Π p = ... ⟶ ...› conjuncts range over
  ‹Π :: pname => proc_decl option›'s entire (unbounded) function domain, so
  \<^const>‹wf_program_compile_input› cannot be exported/evaluated as literally
  stated -- Isabelle's code generator has nothing to enumerate a function's
  domain against. ‹proc_rep› is always finite in practice (‹prog_table p =
  map_of (proc_rep p)›), so both conjuncts are provably implied by the
  corresponding ‹list_all› check over ‹proc_rep p› directly: every entry
  ‹proc_rep p› actually lists is checked, which is at least as strong as
  checking only the ones ‹map_of› would resolve a lookup to.

  ‹wf_program_compile_input_exec› only needs to be ∗‹sufficient› for the CLI
  well-formedness gate to be sound (never silently accepting a source program
  \<^const>‹wf_program_compile_input› would reject) -- not a decision procedure
  complete in the other direction, which ‹map_of›'s first-occurrence-wins
  semantics on a ‹proc_rep› with a shadowed duplicate key would make
  materially harder to establish for no operational benefit here.
›

definition wf_program_compile_input_exec :: "imp_prog => bool" where
  "wf_program_compile_input_exec p ⟷
     (let procs = proc_rep p; 𝒢 = declared_global p; pi = map_of procs
      in reserved_ret_var 𝒢 ∧
         distinct (prog_procs p) ∧
         set (prog_procs p) = set (map fst procs) - {prog_main_name} ∧
         prog_main_name ∉ set (prog_procs p) ∧
         pi prog_main_name = Some (⦇formals = [], body = prog_main p⦈) ∧
         wf_source_com pi (prog_main p) ∧ no_return (prog_main p) ∧
         list_all (λ(_, decl). wf_proc_decl 𝒢 pi decl) procs ∧
         list_all (λ(q, _). special_table q = None) procs)"

lemma wf_program_compile_input_exec_sound:
  assumes "wf_program_compile_input_exec p"
  shows "wf_program_compile_input p"
proof -
  define procs where "procs = proc_rep p"
  define 𝒢 where "𝒢 = declared_global p"
  define pi where "pi = map_of procs"
  have pi_eq: "pi = prog_table p"
    unfolding pi_def procs_def prog_table_def ..
  from assms have h:
    "reserved_ret_var 𝒢"
    "distinct (prog_procs p)"
    "set (prog_procs p) = set (map fst procs) - {prog_main_name}"
    "prog_main_name ∉ set (prog_procs p)"
    "pi prog_main_name = Some (⦇formals = [], body = prog_main p⦈)"
    "wf_source_com pi (prog_main p)"
    "no_return (prog_main p)"
    "list_all (λ(_, decl). wf_proc_decl 𝒢 pi decl) procs"
    "list_all (λ(q, _). special_table q = None) procs"
    unfolding wf_program_compile_input_exec_def procs_def 𝒢_def pi_def Let_def
    by simp_all
  have domain: "set (map fst procs) = {q. pi q ≠ None}"
    unfolding pi_def by (induction procs) auto
  have every_decl: "⋀q decl. pi q = Some decl ⟹ wf_proc_decl 𝒢 pi decl"
  proof -
    fix q decl assume "pi q = Some decl"
    then have "(q, decl) ∈ set procs" unfolding pi_def by (rule map_of_SomeD)
    with h(8) show "wf_proc_decl 𝒢 pi decl" by (auto simp: list_all_iff)
  qed
  have every_special: "⋀q. pi q ≠ None ⟹ special_table q = None"
  proof -
    fix q assume "pi q ≠ None"
    then    obtain decl where "(q, decl) ∈ set procs"
      using domain by force
    with h(9) show "special_table q = None" by (auto simp: list_all_iff)
  qed
  have main_eq: "main_body pi = prog_main p" using pi_eq by simp
  have wf_source_program: "wf_source_program 𝒢 pi"
    unfolding wf_source_program_def main_eq
    using h(1) h(5) h(6) h(7) every_decl every_special by blast
  have wf_compile_input: "wf_compile_input 𝒢 pi (prog_procs p)"
    unfolding wf_compile_input_def
    using h(2) h(3) h(4) wf_source_program
    using domain by blast
  show ?thesis
    unfolding 𝒢_def[symmetric] pi_eq[symmetric] using wf_compile_input .
qed

text ‹\<^const>‹compile_prog› takes a \<^typ>‹proc_table› and a \<^typ>‹pname list›, so a
  domain holding only an \<^typ>‹imp_prog› needs the two-projection wrapper below.  The entry
  name is \<^const>‹prog_main_name› and its body is looked up, so neither is threaded through
  as a parameter.  This is also the name the OCaml export publishes: a second wrapper for
  the export alone would put the same function in the generated module twice.›

definition prog_cfg :: "imp_prog => cfg" where
  "prog_cfg p = compile_prog (prog_table p) (prog_procs p)"

subsection ‹Syntactic occurrence predicates›

text ‹‹returns_in› asks a purely syntactic question -- does this command contain a
  ‹Return› of exactly this expression -- which is the shape the compiler lemmas below need.
  They induct over the source command, so their hypothesis has to be readable off the
  syntax rather than off the graph the compiler produced from it.›
fun returns_in :: "exp option ⇒ 'a acom ⇒ bool" where
  "returns_in e (Return i e') = (e = e')"
| "returns_in e (Seq c1 c2) = (returns_in e c1 ∨ returns_in e c2)"
| "returns_in e (If i _ c1 c2) = (returns_in e c1 ∨ returns_in e c2)"
| "returns_in e (While i _ c) = returns_in e c"
| "returns_in e _ = False"

subsection ‹Return edges and call-freeness›

text ‹Every source ‹Return e› in procedure ‹p› compiles to an intra edge that
  reaches ‹FunctionResult p› through ‹EA_Ret e p›.›
lemma compile_return_edge:
  "compile Π p c k n = (n', en, E, K) ⟹ returns_in e c
   ⟹ ∃j. (Statement j, EA_Ret e p, FunctionResult p) ∈ E"
proof (induction c arbitrary: k n n' en E K rule: gcom.induct)
  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 E: "E = E1 ∪ E2"
    by (auto simp: Let_def split: prod.splits)
  from Seq.prems(2) have "returns_in e c1 ∨ returns_in e c2" by simp
  then show ?case using Seq.IH(1)[OF c1] Seq.IH(2)[OF c2] E by auto
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 E: "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else en1),
                  (Statement n, EA_AssumeNot b, if is_SKIP c2 then k else en2)}
                  ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
    by (auto split: prod.splits)
  from If.prems(2) have "returns_in e c1 ∨ returns_in e c2" by simp
  then show ?case using If.IH(1)[OF c1] If.IH(2)[OF c2] E
    by (auto split: if_splits)
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 E: "E = {(Statement n, EA_Assume b, en1), (Statement n, EA_AssumeNot b, k)} ∪ E1"
    by (auto split: prod.splits)
  from While.prems(2) have "returns_in e c" by simp
  then show ?case using While.IH[OF c1] E by auto
next
  case (Return i e') then show ?case by (auto split: if_splits)
qed auto

subsection ‹Public compiler invariants›

text ‹A ‹Return› fragment ignores its continuation: it emits its result edge and nothing
  else, so no node exists to carry a control flow the source does not have.›
theorem compile_Return_ignores_continuation:
  "compile Π p (Return i e) k n = compile Π p (Return i e) k' n"
  by simp

section ‹Where each statement index came from in the source›

text ‹A source position is nowhere in the compiled graph, yet a report has to name one.
  What follows supplies the missing link in two steps: an enumeration of the statement
  indices a fragment allocates, ordered the way a front end completes its reductions, and
  the lemmas pinning that enumeration to the compiler's own allocation.›
subsection ‹Statement order in the source›

text ‹
  Which \<^const>‹Statement› index \<^const>‹compile› gives each command of a fragment, listed in
  the order a bottom-up parser completes the commands: a reduction finishes only once its
  whole right-hand side has been read, so an ‹if› is listed after both its branches and a
  loop after its body.  Every clause allocates the same index its \<^const>‹compile›
  counterpart does: a leaf takes ‹n›; \<^const>‹Seq› hands ‹c2› the counter ‹c1› ends at;
  \<^const>‹If› and \<^const>‹While› take ‹n› for the guard and start the body at ‹Suc n›.
  A front end that records one position per reduction can pair its ‹k›th position with
  this list's ‹k›th index without reproducing \<^const>‹compile›'s counter arithmetic.
›

fun com_stmt_post_order :: "nat ⇒ 'a acom ⇒ cfg_node list" where
  "com_stmt_post_order n (SKIP i) = [Statement n]"
| "com_stmt_post_order n (Assign i x a) = [Statement n]"
| "com_stmt_post_order n (Check i l c) = [Statement n]"
| "com_stmt_post_order n (Seq c1 c2) =
     com_stmt_post_order n c1 @ com_stmt_post_order (n + csize c1) c2"
| "com_stmt_post_order n (If i b c1 c2) =
     com_stmt_post_order (Suc n) c1 @ com_stmt_post_order (Suc n + csize c1) c2
       @ [Statement n]"
| "com_stmt_post_order n (While i b c) = com_stmt_post_order (Suc n) c @ [Statement n]"
| "com_stmt_post_order n (Call i dst q actuals) = [Statement n]"
| "com_stmt_post_order n (Return i e) = [Statement n]"
| "com_stmt_post_order n (Restore i) = [Statement n]"
| "com_stmt_post_order n (Unwind i) = [Statement n]"

text ‹The enumeration has one entry per index the fragment allocates: a shorter or
  longer list would silently misalign every position after it.›

lemma length_com_stmt_post_order [simp]: "length (com_stmt_post_order n c) = csize c"
  by (induction c arbitrary: n) auto

text ‹
  \<^const>‹com_stmt_post_order› answers this for one fragment given the counter it
  starts at. A whole program needs those starting counters, and they are not a
  fragment-local fact: \<^const>‹compile_procs› lays the procedures out one after another
  and \<^const>‹compile_prog› compiles ‹main› after all of them, whatever order the source
  wrote them in.

  ‹procs_stmt_next› below is that layout and nothing else --- each declared procedure
  advances the counter past its body and past the one index \<^const>‹compile_proc›
  reserves for the epilogue. Undeclared names advance it by nothing, matching the
  clause \<^const>‹compile_procs› skips.
›

fun procs_stmt_next :: "'a ptable ⇒ pname list ⇒ nat ⇒ nat" where
  "procs_stmt_next Π [] n = n"
| "procs_stmt_next Π (p # ps) n =
     (case Π p of
        None ⇒ procs_stmt_next Π ps n
      | Some decl ⇒ procs_stmt_next Π ps (Suc (n + csize (body decl))))"

text ‹
  Each definition paired with the statement indices its body owns, in the order a
  bottom-up parser finishes them. ‹main› comes last because that is where
  \<^const>‹compile_prog› compiles it, not because of where it appears in the source ---
  which is exactly why a front end cannot pair a flat position list against the program
  and must group by definition first.
›

fun defs_stmt_post_order ::
  "'a ptable ⇒ pname list ⇒ nat ⇒ (pname × cfg_node list) list"
where
  "defs_stmt_post_order Π [] n = []"
| "defs_stmt_post_order Π (p # ps) n =
     (case Π p of
        None ⇒ defs_stmt_post_order Π ps n
      | Some decl ⇒
          (p, com_stmt_post_order n (body decl))
            # defs_stmt_post_order Π ps (Suc (n + csize (body decl))))"

definition prog_stmt_post_order :: "imp_prog ⇒ (pname × cfg_node list) list" where
  "prog_stmt_post_order p =
     defs_stmt_post_order (prog_table p) (prog_procs p) 0
       @ [(prog_main_name,
           com_stmt_post_order (procs_stmt_next (prog_table p) (prog_procs p) 0)
             (prog_main p))]"

section ‹Connectivity of a compiled graph›

text ‹A compiled fragment's entry reaches its continuation or its procedure result along
  the structural successor relation.  Nothing downstream consumes this: a routed D/G
  system's own coverage witness is ‹vars_cover_exec›, decided per node from whether a
  caller actually published a seed, not from graph reachability.  This connectivity fact
  is instead what pins the transparent \<^const>‹Restore›/\<^const>‹Unwind› encoding ---
  emitting nothing for those clauses would make them dead ends and force a
  \<^const>‹source_com› hypothesis onto the whole-program statement.›

text ‹The fragment-relative forms the compiler inductions use: an edge of a fragment
  included in the graph.›
lemma local_reaches_intra_sub:
  "(u, a, v) ∈ E ⟹ E ⊆ intra g ⟹ local_reaches g u v"
  by (auto intro: local_reaches_intra_step)

lemma local_reaches_comb_caller_sub:
  "(c, ca, FunctionEntry q, k) ∈ K ⟹ K ⊆ calls g ⟹ local_reaches g c k"
  by (auto intro: local_reaches_comb_step)

subsection ‹Compiled entry reaches its exit or its procedure result›

text ‹A fragment's entry leads to its continuation or, along an explicit \<^const>‹Return›
  edge, to the enclosing procedure's \<^term>‹FunctionResult›.  Both stay inside the
  activation, so the statement is about \<^const>‹local_reaches›.›
lemma compile_reaches:
  assumes "compile Π p c k n = (n', en, E, K)" and "E ⊆ intra g" and "K ⊆ calls g"
  shows "local_reaches g en k ∨ local_reaches g en (FunctionResult p)"
  using assms
proof (induction c arbitrary: k n n' en E K)
  case (Seq c1 c2)
  from Seq.prems(1) obtain n1 E1 K1 n2 E2 K2 where
      c1: "compile Π p c1 (Statement (n + csize c1)) n = (n1, Statement n, E1, K1)"
    and c2: "compile Π p c2 k (n + csize c1) = (n2, Statement (n + csize c1), E2, K2)"
    and res: "en = Statement n" "E = E1 ∪ E2" "K = K1 ∪ K2"
    by (rule compile_SeqE)
  have h1: "local_reaches g (Statement n) (Statement (n + csize c1))
            ∨ local_reaches g (Statement n) (FunctionResult p)"
    using Seq.IH(1)[OF c1] Seq.prems res by auto
  have h2: "local_reaches g (Statement (n + csize c1)) k
            ∨ local_reaches g (Statement (n + csize c1)) (FunctionResult p)"
    using Seq.IH(2)[OF c2] Seq.prems res by auto
  from h1 h2 show ?case unfolding res(1) by (blast intro: local_reaches_trans)
next
  case (If i b c1 c2)
  from If.prems(1) obtain n1 E1 K1 E2 K2 where
      c1: "compile Π p c1 k (Suc n) = (n1, Statement (Suc n), E1, K1)"
    and res: "en = Statement n"
      "E = {(Statement n, EA_Assume b, if is_SKIP c1 then k else Statement (Suc n)),
            (Statement n, EA_AssumeNot b,
              if is_SKIP c2 then k else Statement (Suc n + csize c1))}
            ∪ (if is_SKIP c1 then {} else E1) ∪ (if is_SKIP c2 then {} else E2)"
      "K = K1 ∪ K2"
    by (rule compile_IfE)
  have b1: "local_reaches g (Statement n) (if is_SKIP c1 then k else Statement (Suc n))"
    using res(2) If.prems(2) by (blast intro: local_reaches_intra_sub)
  show ?case
  proof (cases "is_SKIP c1")
    case True with b1 res(1) show ?thesis by simp
  next
    case False
    have "local_reaches g (Statement (Suc n)) k
          ∨ local_reaches g (Statement (Suc n)) (FunctionResult p)"
      using If.IH(1)[OF c1] If.prems res False by auto
    with b1 False show ?thesis unfolding res(1) by (auto intro: local_reaches_trans)
  qed
qed (auto simp: Let_def split: prod.splits option.splits
     intro: local_reaches_intra_sub local_reaches_comb_caller_sub)

lemma compile_proc_reaches_result:
  assumes "compile_proc Π p decl n = (n', E, K)"
      and "E ⊆ intra g" "K ⊆ calls g"
  shows "local_reaches g (FunctionEntry p) (FunctionResult p)"
proof -
  let ?r = "n + csize (body decl)"
  obtain Eb where
      body: "compile Π p (body decl) (Statement ?r) n = (?r, Statement n, Eb, K)"
    and E_eq: "E = insert (FunctionEntry p, EA_Body p, Statement n)
                     (insert (Statement ?r, EA_Ret None p, FunctionResult p) Eb)"
    by (rule compile_procE[OF assms(1)])
  have Ebg: "Eb ⊆ intra g" using E_eq assms(2) by auto
  have entry: "local_reaches g (FunctionEntry p) (Statement n)"
    using E_eq assms(2) by (blast intro: local_reaches_intra_sub)
  have epi: "local_reaches g (Statement ?r) (FunctionResult p)"
    using E_eq assms(2) by (blast intro: local_reaches_intra_sub)
  from compile_reaches[OF body Ebg assms(3)] entry epi show ?thesis
    by (blast intro: local_reaches_trans)
qed

theorem compile_prog_entry_cfg_reaches_exit:
  "cfg_reaches (compile_prog Π ps)
     (cfg_entry (compile_prog Π ps)) (cfg_exit (compile_prog Π ps))"
proof -
  obtain n1 Eprocs Kprocs n2 Emain Kmain where
      cmain: "compile_proc Π prog_main_name ⦇formals = [], body = (main_body Π)⦈ n1
                = (n2, Emain, Kmain)"
    and g: "intra (compile_prog Π ps) = Eprocs ∪ Emain"
           "calls (compile_prog Π ps) = Kprocs ∪ Kmain"
    by (rule compile_prog_intra_split)
  have "cfg_reaches (compile_prog Π ps)
          (FunctionEntry prog_main_name) (FunctionResult prog_main_name)"
    using g by (intro local_reaches_cfg_reaches compile_proc_reaches_result[OF cmain]) auto
  then show ?thesis by simp
qed

end