Theory Transfer_Algebra

theory Transfer_Algebra
  imports "Voblint_CFG.CFG_Transfer" "Voblint_Domain.Nonrelational_State"
begin

section ‹The abstract-state algebra a whole-state transfer computes in›

text ‹
  A Base-style analysis carries one pointwise abstract state per program point: a
  map from variable names to abstract values. This theory fixes the operations its
  transfer functions are assembled from -- how a call resets the callee frame and
  binds its formals, how a return merges caller against callee and publishes the
  result value -- together with their soundness and monotonicity against
  ‹gamma_state›.

  It defines no interface. What an analysis supplies to the framework is a
  ‹dg_spec›: one manager-native transfer per edge action, taking the manager and
  returning a program. This theory is the algebra those transfers compute in,
  stated once so that no whole-state domain re-proves it.

  Most of the operations themselves live lower still, in the language session,
  because they are generic in the state's codomain and the concrete semantics
  runs the very same constants: \<^const>‹combine_env›, \<^const>‹enter_frame›,
  \<^const>‹bind_formals›, \<^const>‹combine_assign› and \<^const>‹enter_binding› are
  all shared. What is genuinely new here is their meaning against a
  concretization, which is the first point at which the domain session and the
  CFG session are both in scope.
›


subsection ‹The structural environment combine›

lemma combine_env_mono:
  fixes sc1 sc2 se1 se2 :: "'a::order abs_state"
  assumes "sc1 ≤ sc2" and "se1 ≤ se2"
  shows "combine_env 𝒢 sc1 se1 ≤ combine_env 𝒢 sc2 se2"
  using assms by (auto simp: combine_env_def le_fun_def)

text ‹
  Soundness of the abstract combine: combining a caller store (sound for sc) with
  a callee-exit store (sound for se) yields a store sound for ‹combine_env 𝒢 sc se›.
  A pure ‹numeric_domain› fact -- independent of any transfer function -- reused by
  both the interprocedural constraint-system soundness and the effectful pipeline.
  ‹combine_env› is the fixed structural merge the Base call boundary uses; an
  analysis that wants a different one overrides its specification's own
  environment stage instead.
›
lemma combine_env_sound [intro]:
  fixes dc de :: "'a::numeric_domain abs_state"
  assumes sc: "s ∈ γ dc" and se: "t ∈ γ de"
  shows "combine_env 𝒢 s t ∈ γ (combine_env 𝒢 dc de)"
  using assms by (auto simp: gamma_state_def le_fun_def)

subsection ‹Generic soundness and monotonicity helpers›

text ‹The two facts a call boundary keeps re-deriving: writing one variable, and binding a
  list of formals, each preserve soundness and monotonicity.  They are stated for an
  arbitrary domain and no transfer function, so every analysis picks them up rather than
  proving its own copy.›
lemma gamma_state_upd [intro]:
  fixes d :: "'a::numeric_domain abs_state"
  assumes s: "s ∈ γ d" and v: "v ∈ γ a"
  shows "s(x := v) ∈ γ (d(x := a))"
  using s v unfolding gamma_state_def by auto

text ‹
  Binding formals preserves soundness: pointwise-sound actual values bound to the
  same formals yield a sound entry state.
›
lemma bind_formals_sound [intro]:
  fixes d :: "'a::numeric_domain abs_state"
  assumes s: "s ∈ γ d"
    and vals: "list_all2 (λv a. v ∈ γ a) vs avs"
  shows "bind_formals xs vs s ∈ γ (bind_formals xs avs d)"
  using assms apply (induction xs arbitrary: vs avs s d)
  subgoal
    by simp
  subgoal for _ _ vs avs
    by (cases vs; cases avs) (auto simp: gamma_state_upd)
  done

lemma bind_formals_mono:
  fixes d1 d2 :: "'a::order abs_state"
  assumes base: "d1 ≤ d2"
    and vals: "list_all2 (≤) avs1 avs2"
  shows "bind_formals xs avs1 d1 ≤ bind_formals xs avs2 d2"
  using assms apply (induction xs arbitrary: avs1 avs2 d1 d2)
  subgoal
    by simp
  subgoal for _ _ avs1 avs2
    by (cases avs1; cases avs2) (auto simp add: le_fun_def)
  done

subsection ‹Procedure entry: binding formals and resetting the frame›

text ‹
  Procedure entry itself is not defined here. \<^const>‹enter_frame› and
  \<^const>‹enter_binding› (\<^theory>‹Voblint_VIMP.VIMP_Proc›) are already generic in
  the state's codomain, and the concrete semantics is \<^const>‹enter_binding› at
  the reset value ‹0› and the evaluator \<^const>‹aval›
  (\<^const>‹call_enter›). An abstract domain runs the same constant at its own
  ‹top› and its own evaluator, so the two can never drift apart: there is one
  definition and two instances of it.

  What this theory adds is the pair of facts that relate those two instances --
  the concrete entered store lands in the concretization of the abstract one, and
  the abstract one is monotone. Neither is expressible below here, because
  \<^const>‹gamma_state› lives in the domain session and \<^const>‹enter_binding› in
  the language session.
›

lemma enter_frame_sound [intro]:
  fixes reset_val :: "'a::numeric_domain"
  assumes sv: "s ∈ γ d" and reset_full: "γ reset_val = UNIV"
  shows "enter_state 𝒢 s ∈ γ (enter_frame 𝒢 reset_val d)"
  unfolding gamma_state_def enter_state_def
  using gamma_stateD[OF sv] reset_full by auto

lemma enter_frame_mono:
  fixes reset_val :: "'a::order"
  assumes "d1 ≤ d2"
  shows "enter_frame 𝒢 reset_val d1 ≤ enter_frame 𝒢 reset_val d2"
  by (simp add: assms le_funD le_funI)

text ‹
  \<^const>‹bind_formals›'s own soundness and monotonicity are relational in the
  actual values, but that is not the shape a domain owns: an evaluator's
  soundness and monotonicity are pointwise in one actual. This turns the one into
  the other, so the entry lemmas below can take the fact a caller already has and
  nobody builds a \<^const>‹list_all2› by hand.
›

lemma list_all2_map_mapI [intro]:
  assumes "⋀x. x ∈ set xs ⟹ R (f x) (g x)"
  shows "list_all2 R (map f xs) (map g xs)"
  using assms by (induction xs) auto

lemma enter_binding_sound_list_all2 [intro]:
  fixes reset_val :: "'a::numeric_domain"
  assumes sv: "s ∈ γ d" and reset_full: "γ reset_val = UNIV"
    and vals: "list_all2 (λv a. v ∈ γ a)
                 (map (λe. ⟦e⟧⇩_e s) es) (map (λe. aval_abs e d) es)"
  shows "enter_binding 𝒢 0 aval xs es s
           ∈ γ (enter_binding 𝒢 reset_val aval_abs xs es d)"
  unfolding enter_binding_def enter_state_def[symmetric]
  by (rule bind_formals_sound[OF enter_frame_sound[OF sv reset_full] vals])

lemma enter_binding_sound [intro]:
  fixes reset_val :: "'a::numeric_domain"
  assumes sv: "s ∈ γ d" and reset_full: "γ reset_val = UNIV"
    and eval: "⋀e. e ∈ set es ⟹ ⟦e⟧⇩_e s ∈ γ (aval_abs e d)"
  shows "enter_binding 𝒢 0 aval xs es s
           ∈ γ (enter_binding 𝒢 reset_val aval_abs xs es d)"
proof (rule enter_binding_sound_list_all2[OF sv reset_full])
  show "list_all2 (λv a. v ∈ γ a)
          (map (λe. ⟦e⟧⇩_e s) es) (map (λe. aval_abs e d) es)"
    by (rule list_all2_map_mapI) (rule eval)
qed

lemma enter_binding_mono:
  fixes reset_val :: "'a::order"
  assumes state_le: "d1 ≤ d2"
    and eval_mono: "⋀e. e ∈ set es ⟹ aval_abs e d1 ≤ aval_abs e d2"
  shows "enter_binding 𝒢 reset_val aval_abs xs es d1
           ≤ enter_binding 𝒢 reset_val aval_abs xs es d2"
  unfolding enter_binding_def
proof (rule bind_formals_mono[OF enter_frame_mono[OF state_le]])
  show "list_all2 (≤) (map (λe. aval_abs e d1) es) (map (λe. aval_abs e d2) es)"
    by (rule list_all2_map_mapI) (rule eval_mono)
qed

text ‹
  A call site reads the formals and actuals off \<^typ>‹call_info› rather than
  passing them separately, but that projection stays at the call site: a domain
  writes ‹enter_binding 𝒢 top ev (ci_formals ci) (ci_args ci)›, exactly as the
  return side writes ‹combine⇧^♯ 𝒢 (ci_dst ci)›. No constant here wraps it.

  The caller's own continuation is not computed here either. Goblint's
  ‹Spec.enter› answers caller/callee pairs and ‹constraints.ml› hands the caller
  half on to ‹combine_env›; a specification's entry field answers the same
  pairs, so a domain that wants to drop caller facts a callee could invalidate
  --- Goblint's ‹varEq› filters its caller state by taint --- returns the
  filtered state as the continuation half of its own alternatives. Nothing in
  this algebra chooses that half: the operations below are what a whole-state
  domain computes each half ∗‹with›.
›

subsection ‹The structural return combine›

text ‹The return-value write is a single-slot update, hence monotone in both the
  written value and the state it writes into.  Any combine built over it inherits
  monotonicity from this one fact.›

lemma combine_assign_mono:
  fixes s1 s2 :: "'a::order abs_state"
  assumes v: "v1 ≤ v2" and s: "s1 ≤ s2"
  shows "combine_assign dst v1 s1 ≤ combine_assign dst v2 s2"
  using assms by (cases dst) (auto simp: le_fun_def)

text ‹
  Return combination joins caller locals with callee globals and then assigns the
  callee's @{const ret_var} to the optional destination.  The ordinary abstract
  state update publishes the result without domain-specific return machinery.
›
definition combine_collect_abs ::
    "(vname ⇒ bool) ⇒ vname option ⇒ 'a abs_state ⇒ 'a abs_state ⇒ 'a abs_state"
    ("combine⇧^♯") where
  "combine_collect_abs 𝒢 dst dc de =
     combine_assign dst (de ret_var) (combine_env 𝒢 dc de)"

lemma combine_collect_abs_mono:
  fixes dc1 dc2 de1 de2 :: "'a::order abs_state"
  assumes c: "dc1 ≤ dc2" and e: "de1 ≤ de2"
  shows "combine⇧^♯ 𝒢 dst dc1 de1 ≤ combine⇧^♯ 𝒢 dst dc2 de2"
  unfolding combine_collect_abs_def
  by (rule combine_assign_mono[OF le_funD[OF e] combine_env_mono[OF c e]])

text ‹
  The binary env-combine is the destination-free instance of the
  return-threaded combine: with no destination the return slot is not written.
  Together with the writing case these reduce the abstract combine under a
  ‹cases dst›, so no caller unfolds its definition by hand.
›
lemma combine_collect_abs_None[simp]:
  "combine⇧^♯ 𝒢 None a b = combine_env 𝒢 a b"
  by (simp add: combine_collect_abs_def)

lemma combine_collect_abs_Some[simp]:
  "combine⇧^♯ 𝒢 (Some x) a b = (combine_env 𝒢 a b)(x := b ret_var)"
  by (simp add: combine_collect_abs_def)

subsection ‹Soundness of the structural return combine›


text ‹
  Soundness of the abstract combine including result publication.  A pure
  @{class numeric_domain} fact: the destination slot is sound because the callee's
  @{const ret_var} slot is, and every other slot is handled by
  @{thm combine_env_sound}.
›
lemma combine_collect_sound [intro]:
  fixes dc de :: "'a::numeric_domain abs_state"
  assumes sc: "s ∈ γ dc" and se: "t ∈ γ de"
  shows "combine_collect 𝒢 dst s t ∈ γ (combine⇧^♯ 𝒢 dst dc de)"
  unfolding combine_collect_def combine_collect_abs_def
  using combine_env_sound[OF sc se] gamma_stateD[OF se]
  by (cases dst) (auto simp add: gamma_state_upd)

subsection ‹The C-faithful initial store set›

text ‹
  \<^const>‹cinit_stores› (\<^theory>‹Voblint_VIMP.VIMP_Globals›) is the C-faithful initial
  store set. Any analysis that uses a domain-specific abstract seed ‹s0›
  satisfying ‹cinit_stores 𝒢 ⊆ γ s0› may state its soundness
  theorem against ‹cinit_stores 𝒢› rather than ‹UNIV›, matching VIMP's
  C-like initialization semantics.›


end