Theory Call_String_Routed_Context

theory Call_String_Routed_Context
  imports
    Compiled_Routed_Equations
    "Voblint_Framework.Call_String_Context"
begin

section ‹Telling activations apart by how they were called›

text ‹
  A call string is the last ‹k› call sites on the stack. Keying an analysis by one
  means a procedure entered from two places is analysed twice, separately, instead
  of once at the join of both --- and entered from more than ‹k› levels deep, the
  oldest sites drop off and those activations merge again.

  This theory says that policy is a legal routing for the generic spine, and pays
  once, for every ‹k› and every domain, the part of that bill which depends only on
  the policy and on the shape of a compiled program:

    ▪ ‹finC› holds for every const‹compile_prog› output (‹compile_prog_finite›);
    ▪ ‹calls_unique› is call-source uniqueness for every const‹compile_prog›
      output (‹compile_prog_calls_source_unique›);
    ▪ ‹seed_ne_buffer_key› is datatype distinctness for type‹call_string_gk›;
    ▪ ‹routing_adequate›'s routing conjunct is const‹cs_route› and
      const‹cs_context› being the same closed term (‹cs_route_context_agree›),
      independently of the entered value, so every context the relation admits is the
      one const‹cs_route› computes on any alternative;
    ▪ ‹routing_total› is immediate: the graph of a function admits exactly one
      context per call.

  ‹call_fwd› and ‹comb_fwd› remain assumptions, and deliberately so: each says the solved
  variable set covers a particular routed callee entry or return continuation, which is a
  property of the program together with what the solver actually explored. An instance
  supplies them; no generic argument can.
›

definition call_string_eqs_for ::
    "nat
      ⇒ (pp × call_string, call_string_gk, unit,
           'D::bounded_semilattice_sup_bot, 'G::bounded_semilattice_sup_bot) dg_spec
      ⇒ cfg
      ⇒ 'D
      ⇒ (pp × call_string, call_string_gk, ('D, 'G) dg_state) eqsT"
where
  "call_string_eqs_for k S g initial =
     compiled_routed_eqs_for Call_String_Context.Global
       (λ_. Call_String_Context.Global) Call_String_Context.Seed (cs_route k) S g initial bot"

text ‹
  The constructor fixes the call-string routing, global and seed keys,
  compiled-program resolver, and bottom initialization. A domain supplies
  only its specification, graph, and initial local state.
›

locale call_string_routed_context =
  dg_context_activation S "λd e. γDG d (e ())" 𝒢 "compile_prog Pi ps" Global "λ_. Global"
    "cs_route k"
    "routed_call_program S (λ_. Global) Seed (static_resolve (compile_prog Pi ps)) is_bot"
    "routed_entry_seed_programs Seed"
    bot0 d0 g0 sigma vars x0 sg γM
  for S :: "(pp × cfg_node list, call_string_gk, unit, 'D::bounded_semilattice_sup_bot,
              'G::bounded_semilattice_sup_bot) dg_spec"
    and γDG :: "'D ⇒ 'G ⇒ store set"
    and 𝒢 :: "vname ⇒ bool"
    and Pi :: proc_table and ps :: "pname list"
    and k :: nat
    and bot0 d0 g0 sigma vars x0 sg
    and is_bot :: "'D ⇒ bool"
    and γM :: "'M ⇒ store set" +
  assumes is_bot_bot: "is_bot bot"
    and is_bot_sound: "⋀d gv. is_bot d ⟹ γDG d gv = {}"
    and enter_complete:
    "⋀u ctx dst pars args p cont s.
       (u, ctx) ∈ vars
       ⟹ (u, CallEdge dst pars args, FunctionEntry p, cont)
             ∈ calls (compile_prog Pi ps)
       ⟹ s ∈ γDG (dg_local (sigma (Inl (u, ctx)))) (dg_global (sigma (Inr Global)))
       ⟹ ∃pairs pub deps.
             enter_runs (enter♯ S (call_info_of (CallEdge dst pars args) p))
               (mk_dg_man (dg_local (sigma (Inl (u, ctx)))) (λ_. Global)) sigma pairs pub
           ∧ enter_deps (enter♯ S (call_info_of (CallEdge dst pars args) p))
               (mk_dg_man (dg_local (sigma (Inl (u, ctx)))) (λ_. Global)) sigma pairs deps
           ∧ entry_pairs_cover (λd. γDG d (dg_global (sigma (Inr Global)))) s
               (call_enter 𝒢 (CallEdge dst pars args) s) pairs"
    and call_fwd:
    "⋀u ctx dst pars args p cont.
       (u, ctx) ∈ vars
       ⟹ (u, CallEdge dst pars args, FunctionEntry p, cont)
             ∈ calls (compile_prog Pi ps)
       ⟹ (FunctionEntry p,
              cs_route k u ctx (dg_local (sigma (Inl (u, ctx)))) (CallEdge dst pars args))
             ∈ vars"
    and comb_fwd:
    "⋀cl c1 dst pars args p cont.
       (cl, c1) ∈ vars
       ⟹ (cl, CallEdge dst pars args, FunctionEntry p, cont)
             ∈ calls (compile_prog Pi ps)
       ⟹ (cont, c1) ∈ vars"
begin

sublocale routed: routed_context S "λd e. γDG d (e ())" 𝒢 "compile_prog Pi ps" Global
  "λ_. Global"
  "cs_route k" bot0 d0 g0 sigma vars x0 sg Seed
  "static_resolve (compile_prog Pi ps)" is_bot γM "context_policy_of_fun (cs_context k)"
proof unfold_locales
  show "finite (calls (compile_prog Pi ps))" by (simp add: compile_prog_finite)
next
  show "calls_source_unique (compile_prog Pi ps)"
    unfolding calls_source_unique_def using compile_prog_calls_source_unique by blast
next
  show "⋀p ctx. Seed p ctx ≠ Global" by simp
next
  show "is_bot bot" by (rule is_bot_bot)
next
  show "⋀d gv. is_bot d ⟹ γDG d gv = {}" by (rule is_bot_sound)
next
  fix u ctx dst pars args p cont s
  assume "(u, ctx) ∈ vars"
    and "(u, CallEdge dst pars args, FunctionEntry p, cont)
            ∈ calls (compile_prog Pi ps)"
    and "s ∈ gamma_at u ctx"
  then show "p ∈ set (static_resolve (compile_prog Pi ps) cont u
                        (CallEdge dst pars args) (dg_local (sigma (Inl (u, ctx)))))"
    by (simp add: compile_prog_finite)
next
  fix u ctx dst pars args p cont s ctx'
  assume covV: "(u, ctx) ∈ vars"
    and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont)
               ∈ calls (compile_prog Pi ps)"
    and sin: "s ∈ gamma_at u ctx"
    and Rc: "ctx' ∈ context_policy_of_fun (cs_context k) u ctx (call_info_of (CallEdge dst pars args) p)
               s (call_enter 𝒢 (CallEdge dst pars args) s)"
  have ctx': "ctx' = cs_context k u ctx (call_enter 𝒢 (CallEdge dst pars args) s)"
    using Rc by simp
  obtain pairs pub deps
    where R: "enter_runs (enter♯ S (call_info_of (CallEdge dst pars args) p))
                (man_at u ctx) sigma pairs pub"
      and D: "enter_deps (enter♯ S (call_info_of (CallEdge dst pars args) p))
                (man_at u ctx) sigma pairs deps"
      and P: "entry_pairs_cover (λd. γDG d (dg_global (sigma (Inr Global)))) s
                (call_enter 𝒢 (CallEdge dst pars args) s) pairs"
    using enter_complete[OF covV ce sin[simplified]] by blast
  from P obtain cont' entry
    where mem: "(cont', entry) ∈ set pairs"
      and ccov: "s ∈ γDG cont' (dg_global (sigma (Inr Global)))"
      and ecov: "call_enter 𝒢 (CallEdge dst pars args) s
                   ∈ γDG entry (dg_global (sigma (Inr Global)))"
    by (rule entry_pairs_coverE)
  have req: "cs_route k u ctx entry (CallEdge dst pars args) = ctx'"
    unfolding ctx' by (rule cs_route_context_agree)
  have covE: "(FunctionEntry p, ctx') ∈ vars"
    using call_fwd[OF covV ce] req by (simp add: cs_route_def)
  show "∃pairs pub deps cont' entry.
             enter_runs (enter♯ S (call_info_of (CallEdge dst pars args) p))
               (man_at u ctx) sigma pairs pub
           ∧ enter_deps (enter♯ S (call_info_of (CallEdge dst pars args) p))
               (man_at u ctx) sigma pairs deps
           ∧ (cont', entry) ∈ set pairs
           ∧ s ∈ γDG cont' (genv (λ_. Global) sigma ())
           ∧ call_enter 𝒢 (CallEdge dst pars args) s
               ∈ γDG entry (genv (λ_. Global) sigma ())
           ∧ cs_route k u ctx entry (CallEdge dst pars args) = ctx'
           ∧ (FunctionEntry p, ctx') ∈ vars"
    using R D mem ccov ecov req covE by auto
next
  fix u ctx dst pars args p cont s
  show "context_policy_of_fun (cs_context k) u ctx
                 (call_info_of (CallEdge dst pars args) p) s
                 (call_enter 𝒢 (CallEdge dst pars args) s) ≠ {}"
    by simp
next
  fix cl c1 dst pars args p cont
  assume "(cl, c1) ∈ vars"
    and "(cl, CallEdge dst pars args, FunctionEntry p, cont)
           ∈ calls (compile_prog Pi ps)"
  then show "(cont, c1) ∈ vars" by (rule comb_fwd)
next
  show "⋀p ctx v. Seed p ctx ≠ Global" by simp
qed

end

end