Theory Example_Sign_DG_Overlapping_Enter
theory Example_Sign_DG_Overlapping_Enter
imports
"Voblint_Analysis_Sign.Sign_Analyses"
"Voblint_VIMP.VIMP_Notation"
begin
unbundle default_st_syntax
section ‹One concrete call, two overlapping entry alternatives, two contexts›
text ‹
A call's entry transfer answers a ∗‹list› of (continuation, callee entry)
alternatives, and the entry-state route selects one context per alternative. When two
alternatives both cover the same concrete call, that call is represented under two
contexts at once. This theory builds exactly that situation on the stock executable Sign
specification by overriding \<^const>‹dgs_enter› alone: alternative 1 enters the callee
exactly (the formal ‹a› is \<^const>‹SPos›, the continuation's ‹x› untouched), alternative 2
enters it with every formal forgotten to \<^const>‹STop› ∗‹and› forgets the continuation's
own ‹x› to \<^const>‹STop› too. The concrete call with ‹x = 1› lies in both entries and both
continuations, and the route sends the two entries to ‹[SPos]› and ‹[STop]›.
Reusing ‹x› itself (rather than an artificial marker) keeps the pairing of a continuation
with its entry observable per alternative --- alternative 1 answers ‹(x, y) = (SPos, SPos)›,
alternative 2 answers ‹(STop, STop)› --- while also making each alternative's continuation
a genuine, sound description of the caller's state: ‹STop› covers whatever ‹x› actually is,
so both alternatives cover the one real caller store, and the routed context locale's
totality obligation holds honestly rather than vacuously.
The executable half pins the solved table: two alternatives stay distinguishable through
the whole call/combine machinery, and each is read back and joined correctly. The
soundness half shows the same thing relationally: the existing generic routed soundness
bridge (\<^theory>‹Voblint_Exec.Routed_Exec_Refinement›) already supports list-valued,
non-deterministic entry without any change to it --- this example is what supplies and
discharges the corresponding non-deterministic entry obligations for the first time, and
goes on to show the one concrete caller activation genuinely admitted under both
‹[SPos]› and ‹[STop]› via ‹ov_R›.
›
subsection ‹The program and its graph›
definition ov_program :: imp_prog where
"ov_program = program {
fun p(a) { return a; }
fun main() { x = 1; y = p(x); }
}"
abbreviation ov_gs :: "vname ⇒ bool" where
"ov_gs ≡ declared_global ov_program"
definition ov_pi :: proc_table where "ov_pi = prog_table ov_program"
definition ov_procs :: "pname list" where "ov_procs = prog_procs ov_program"
definition ov_cfg :: cfg where
"ov_cfg = compile_prog ov_pi ov_procs"
definition ov_ep :: "sign default_st ⇒ bool" where
"ov_ep = default_st_is_bot_for (declared_global_vars ov_program)"
abbreviation p_entry :: cfg_node where "p_entry ≡ FunctionEntry (STR ''p'')"
abbreviation p_result :: cfg_node where "p_result ≡ FunctionResult (STR ''p'')"
abbreviation ov_ca :: call_action where
"ov_ca ≡ CallEdge (Some (STR ''y'')) [(STR ''a'')] [V (STR ''x'')]"
text ‹Node layout, computed rather than assumed: ‹p›'s ‹return a› is ‹Statement 0›;
‹main› assigns at ‹Statement 2›, calls at ‹Statement 3›, continues at ‹Statement 4›.›
lemma ov_calls_shape:
"∀(u, ca, ce, cont) ∈ calls ov_cfg.
u = Statement 3 ∧ ca = ov_ca ∧ ce = p_entry ∧ cont = Statement 4"
unfolding ov_cfg_def ov_pi_def ov_procs_def ov_program_def by eval
lemma ov_call_edge:
"(Statement 3, ov_ca, p_entry, Statement 4) ∈ calls ov_cfg"
unfolding ov_cfg_def ov_pi_def ov_procs_def ov_program_def by eval
subsection ‹The overriding entry transfer›
text ‹
‹ov_enter› returns two overlapping alternatives per call, built from
‹forget_formals› and ‹forget_var›.
›
definition forget_formals ::
"(vname ⇒ bool) ⇒ call_info ⇒ sign default_st ⇒ sign default_st" where
"forget_formals 𝒢 ci s =
foldl (λs f. s⟨location_of 𝒢 f := STop⟩) s (ci_formals ci)"
definition forget_var ::
"(vname ⇒ bool) ⇒ vname ⇒ sign ⇒ sign default_st lifted ⇒ sign default_st lifted" where
"forget_var 𝒢 v w = map_lift (λs. s⟨location_of 𝒢 v := w⟩)"
text ‹Alternative 1 is the stock singleton entry, continuation untouched. Alternative 2
forgets the formals on entry ∗‹and› forgets the caller's own ‹x› in its continuation to
\<^const>‹STop›: a real, sound weakening (‹STop› covers whatever ‹x› actually was), not an
artificial tag on a name the program never uses. Every store in alternative 1's entry is
in alternative 2's, so the two overlap; every store covered by alternative 1's
continuation is covered by alternative 2's too (‹STop› is the top of the lattice), so both
continuations cover the one real caller state --- the totality this override must satisfy
is not vacuous.›
definition ov_enter ::
"(vname ⇒ bool) ⇒ (sign default_st ⇒ bool) ⇒ call_info
⇒ sign default_st lifted ⇒ sign default_st lifted enter_result list" where
"ov_enter 𝒢 ep ci d =
(let entered = transfer_lift ep (generic_enter_st_for sign_ops 𝒢 ci) d
in [(d, entered),
(forget_var 𝒢 (STR ''x'') STop d, map_lift (forget_formals 𝒢 ci) entered)])"
definition ov_spec ::
"(vname ⇒ bool) ⇒ (sign default_st ⇒ bool)
⇒ (pp × sign list, (unit, sign list) global_unknown, unit,
sign default_st lifted, sign default_st lifted) dg_spec" where
"ov_spec 𝒢 ep = (sign_tf.spec_exec 𝒢 ep)
⦇ dgs_enter := (λci. local_enter_transfer (ov_enter 𝒢 ep ci)) ⦈"
lemmas [code] = ov_spec_def[unfolded sign_tf.spec_exec_def]
text ‹Only the entry differs; every other field is \<^const>‹sign_tf.spec_exec›'s.›
lemma dg_spec_step_ov_spec [simp]:
"dg_spec_step (ov_spec 𝒢 ep) a = dg_spec_step (sign_tf.spec_exec 𝒢 ep) a"
by (cases a) (simp_all add: ov_spec_def)
lemma dgs_combine_env_ov_spec [simp]:
"combine_env⇧♯ (ov_spec 𝒢 ep) = combine_env⇧♯ (sign_tf.spec_exec 𝒢 ep)"
by (simp add: ov_spec_def)
lemma dgs_combine_assign_ov_spec [simp]:
"combine_assign⇧♯ (ov_spec 𝒢 ep) = combine_assign⇧♯ (sign_tf.spec_exec 𝒢 ep)"
by (simp add: ov_spec_def)
lemma dgs_enter_ov_spec [simp]:
"enter⇧♯ (ov_spec 𝒢 ep) ci = local_enter_transfer (ov_enter 𝒢 ep ci)"
by (simp add: ov_spec_def)
lemma dgs_query_ov_spec [simp]:
"dgs_query (ov_spec 𝒢 ep) = dgs_query (sign_tf.spec_exec 𝒢 ep)"
by (simp add: ov_spec_def)
text ‹The override runs its continuation once wherever the stock specification
does: only the entry changed, and it answers its alternatives outright.›
lemma dg_spec_wf_ov_spec [intro, simp]: "dg_spec_wf (ov_spec 𝒢 ep)"
proof (unfold dg_spec_wf_def, intro conjI allI impI)
show "sp_wf (dg_spec_step (ov_spec 𝒢 ep) a ((mk_dg_man d unknown_of)⦇man_ask := A⦈))"
if "∀q. sp_wf (A q)" for a d unknown_of A
using that by (simp add: dg_spec_wf_step_ask[OF sign_tf.dg_spec_wf_spec_exec])
next
show "sp_wf (dgs_query (ov_spec 𝒢 ep) ((mk_dg_man d unknown_of)⦇man_ask := A⦈) q)"
if "∀q. sp_wf (A q)" for d unknown_of A q
using that by (simp add: dg_spec_wf_query[OF sign_tf.dg_spec_wf_spec_exec])
next
fix ci d unknown_of
show "sp_wf (enter⇧♯ (ov_spec 𝒢 ep) ci (mk_dg_man d unknown_of))"
by (simp add: local_enter_transfer_def)
next
fix ci d unknown_of ex
show "sp_wf (dg_spec_combine_transfer (ov_spec 𝒢 ep) ci (mk_dg_man d unknown_of) ex)"
unfolding dg_spec_combine_transfer_def dgs_combine_env_ov_spec dgs_combine_assign_ov_spec
by (simp add: sign_tf.spec_exec_def exec_dg_spec_def
local_combine_transfer_def)
qed
text ‹Entry is absent from \<^locale>‹analysis_contract›, so the override inherits the
stock specification's contract outright.›
lemma analysis_contract_ov_spec:
assumes exact: "⋀s. ep s = is_empty_state (ρ⇘𝒢⇙ s)"
shows "analysis_contract (ov_spec 𝒢 ep) (λd _. γ (ρ⇘𝒢⇙ d)) 𝒢"
proof -
interpret stock: analysis_contract "sign_tf.spec_exec 𝒢 ep" "(λd _. γ (ρ⇘𝒢⇙ d))" 𝒢
by (rule sign_tf.sound_exec[OF exact])
show ?thesis
proof (unfold_locales, goal_cases)
case 1 show ?case by (rule dg_spec_wf_ov_spec)
next
case (2 d d' g g') then show ?case by (rule stock.gammaDG_mono)
next
case (3 a τ src key)
show ?case using stock.step_sound by (simp add: dg_spec_edge_program_def)
next
case (4 s dc key τ t de ci)
show ?case using stock.combine_sound[where ci = ci and q = dc and r = de
and τ = τ and key = key, OF 4(1) 4(2)]
by (simp add: dg_spec_combine_transfer_def)
qed
qed
subsection ‹The routed equation system, solved›
text ‹The entry-state registration's construction of \<^const>‹dg_pipeline.equations›
at the overriding specification: same generator, same route, same buffered seed
protocol, same plain-join solver.›
definition ov_eqs ::
"(pp × sign list, (unit, sign list) global_unknown,
(sign default_st lifted, sign default_st lifted) dg_state) eqsT" where
"ov_eqs =
routed_node_rhs_buffered intra_predecessor_addr_list call_site_list (λ_. Analysis_Global ())
(exec_formals_route ov_gs)
(λctx' src a. dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ()))
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot))
(routed_entry_seed_programs Activation_Seed)
ov_cfg Bot (Lifted cinit_sign_st) Bot"
definition ov_sol ::
"(pp × sign list) set ×
(pp × sign list + (unit, sign list) global_unknown
⇒ (sign default_st lifted, sign default_st lifted) dg_state)" where
"ov_sol = TD_side_always_join_Interp_solve ov_eqs (cfg_exit ov_cfg, [])"
definition ov_result :: "(sign list, sign abs_state) solved_table" where
"ov_result = Solved_Table (fst ov_sol)
(λv ctx. ρ⇘ov_gs⇙ (canonicalize_lift ov_ep (dg_local (snd ov_sol (Inl (v, ctx))))))"
abbreviation ov_read :: "cfg_node ⇒ sign list ⇒ vname ⇒ sign lifted" where
"ov_read v ctx x ≡ map_lift (λst. st x) (lookup_table ov_result v ctx)"
abbreviation ov_seed :: "sign list ⇒ vname ⇒ sign lifted" where
"ov_seed ctx x ≡ map_lift (λs. ρ⇘ov_gs⇙ s x)
(dg_local (snd ov_sol (Inr (Activation_Seed p_entry ctx))))"
lemmas ov_unfold = ov_result_def ov_sol_def ov_eqs_def ov_cfg_def ov_pi_def ov_procs_def
ov_ep_def ov_program_def
definition ov_alt_answer :: "nat ⇒ sign default_st lifted" where
"ov_alt_answer i =
(let caller = dg_local (snd ov_sol (Inl (Statement 3, [])));
alts = ov_enter ov_gs ov_ep (call_info_of ov_ca (STR ''p'')) caller
in dg_local (traverse_program
(routed_call_alternative_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ())
Activation_Seed (exec_formals_route ov_gs) (λd. d = Bot)
[] ov_ca (Statement 3) (STR ''p'') (alts ! i))
(snd ov_sol)))"
abbreviation ov_alt_read :: "nat ⇒ vname ⇒ sign lifted" where
"ov_alt_read i x ≡
map_lift (λs. ρ⇘ov_gs⇙ s x) (ov_alt_answer i)"
definition ov_caller_store :: store where
"ov_caller_store = (λ_. 0)(STR ''x'' := 1)"
text ‹The solver result is evaluated once. Every executable observation below is a
logical projection of this snapshot, so adding a witness does not rerun the equation
system.›
lemma ov_solution_snapshot_raw:
"(let sol = ov_sol;
result = Solved_Table (fst sol)
(λv ctx. ρ⇘ov_gs⇙
(canonicalize_lift ov_ep (dg_local (snd sol (Inl (v, ctx))))));
read = (λv ctx x. map_lift (λst. st x) (lookup_table result v ctx));
seed = (λctx x. map_lift (λs. ρ⇘ov_gs⇙ s x)
(dg_local (snd sol (Inr (Activation_Seed p_entry ctx)))));
alt_answer = (λi.
let caller = dg_local (snd sol (Inl (Statement 3, [])));
alts = ov_enter ov_gs ov_ep (call_info_of ov_ca (STR ''p'')) caller
in dg_local (traverse_program
(routed_call_alternative_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ())
Activation_Seed (exec_formals_route ov_gs) (λd. d = Bot)
[] ov_ca (Statement 3) (STR ''p'') (alts ! i))
(snd sol)))
in TD_side_always_join_Interp_solve_c ov_eqs (cfg_exit ov_cfg, []) ≠ None
∧ table_contexts result p_entry = {[SPos], [STop]}
∧ table_contexts result (Statement 3) = {[]}
∧ seed [SPos] (STR ''a'') = Lifted SPos
∧ seed [STop] (STR ''a'') = Lifted STop
∧ read p_entry [SPos] (STR ''a'') = Lifted SPos
∧ read p_entry [STop] (STR ''a'') = Lifted STop
∧ read p_result [SPos] ret_var = Lifted SPos
∧ read p_result [STop] ret_var = Lifted STop
∧ map_lift (λs. ρ⇘ov_gs⇙ s (STR ''y''))
(alt_answer 0) = Lifted SPos
∧ map_lift (λs. ρ⇘ov_gs⇙ s (STR ''x''))
(alt_answer 0) = Lifted SPos
∧ map_lift (λs. ρ⇘ov_gs⇙ s (STR ''y''))
(alt_answer 1) = Lifted STop
∧ map_lift (λs. ρ⇘ov_gs⇙ s (STR ''x''))
(alt_answer 1) = Lifted STop
∧ read (Statement 4) [] (STR ''x'') = Lifted STop
∧ read (Statement 4) [] (STR ''y'') = Lifted STop
∧ dg_local (snd sol (Inl (Statement 3, []))) =
default_st_set_lift (Lifted cinit_sign_st)
(location_of ov_gs (STR ''x'')) SPos
∧ exec_formals_route ov_gs (Statement 3) []
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd sol (Inl (Statement 3, []))))) ov_ca = [SPos]
∧ forget_var ov_gs (STR ''x'') STop
(dg_local (snd sol (Inl (Statement 3, [])))) =
default_st_set_lift (Lifted cinit_sign_st)
(location_of ov_gs (STR ''x'')) STop
∧ exec_formals_route ov_gs (Statement 3) []
(map_lift (forget_formals ov_gs (call_info_of ov_ca (STR ''p'')))
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd sol (Inl (Statement 3, [])))))) ov_ca = [STop]
∧ (∀(u, ctx) ∈ fst sol. ∀(u', a, v) ∈ intra ov_cfg.
u = u' ⟶ (v, ctx) ∈ fst sol)
∧ (∀(cl, ctx) ∈ fst sol. ∀(cl', ca, ce, cont) ∈ calls ov_cfg.
cl = cl' ⟶ (cont, ctx) ∈ fst sol)
∧ (∀(u, ctx) ∈ fst sol. u = Statement 3 ⟶
(∀(cont', entry) ∈ set (ov_enter ov_gs ov_ep
(call_info_of ov_ca (STR ''p'')) (dg_local (snd sol (Inl (u, ctx))))).
(p_entry, exec_formals_route ov_gs u ctx entry ov_ca) ∈ fst sol)))"
unfolding ov_sol_def ov_eqs_def ov_cfg_def ov_pi_def ov_procs_def ov_ep_def ov_program_def
by eval
lemma ov_solution_snapshot:
"TD_side_always_join_Interp_solve_c ov_eqs (cfg_exit ov_cfg, []) ≠ None
∧ table_contexts ov_result p_entry = {[SPos], [STop]}
∧ table_contexts ov_result (Statement 3) = {[]}
∧ ov_seed [SPos] (STR ''a'') = Lifted SPos
∧ ov_seed [STop] (STR ''a'') = Lifted STop
∧ ov_read p_entry [SPos] (STR ''a'') = Lifted SPos
∧ ov_read p_entry [STop] (STR ''a'') = Lifted STop
∧ ov_read p_result [SPos] ret_var = Lifted SPos
∧ ov_read p_result [STop] ret_var = Lifted STop
∧ ov_alt_read 0 (STR ''y'') = Lifted SPos
∧ ov_alt_read 0 (STR ''x'') = Lifted SPos
∧ ov_alt_read 1 (STR ''y'') = Lifted STop
∧ ov_alt_read 1 (STR ''x'') = Lifted STop
∧ ov_read (Statement 4) [] (STR ''x'') = Lifted STop
∧ ov_read (Statement 4) [] (STR ''y'') = Lifted STop
∧ dg_local (snd ov_sol (Inl (Statement 3, []))) =
default_st_set_lift (Lifted cinit_sign_st)
(location_of ov_gs (STR ''x'')) SPos
∧ exec_formals_route ov_gs (Statement 3) []
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, []))))) ov_ca = [SPos]
∧ forget_var ov_gs (STR ''x'') STop
(dg_local (snd ov_sol (Inl (Statement 3, [])))) =
default_st_set_lift (Lifted cinit_sign_st)
(location_of ov_gs (STR ''x'')) STop
∧ exec_formals_route ov_gs (Statement 3) []
(map_lift (forget_formals ov_gs (call_info_of ov_ca (STR ''p'')))
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, [])))))) ov_ca = [STop]
∧ (∀(u, ctx) ∈ fst ov_sol. ∀(u', a, v) ∈ intra ov_cfg.
u = u' ⟶ (v, ctx) ∈ fst ov_sol)
∧ (∀(cl, ctx) ∈ fst ov_sol. ∀(cl', ca, ce, cont) ∈ calls ov_cfg.
cl = cl' ⟶ (cont, ctx) ∈ fst ov_sol)
∧ (∀(u, ctx) ∈ fst ov_sol. u = Statement 3 ⟶
(∀(cont', entry) ∈ set (ov_enter ov_gs ov_ep
(call_info_of ov_ca (STR ''p''))
(dg_local (snd ov_sol (Inl (u, ctx))))).
(p_entry, exec_formals_route ov_gs u ctx entry ov_ca) ∈ fst ov_sol))"
using ov_solution_snapshot_raw
unfolding ov_result_def ov_alt_answer_def Let_def
by blast
lemma ov_terminates_c:
"TD_side_always_join_Interp_solve_c ov_eqs (cfg_exit ov_cfg, []) ≠ None"
using ov_solution_snapshot by (elim conjE)
subsection ‹1. One call, two contexts›
text ‹
The single call to ‹p› seeds two callee contexts, ‹[SPos]› and ‹[STop]›, one
per alternative.
›
lemma ov_two_contexts:
"table_contexts ov_result p_entry = {[SPos], [STop]}"
using ov_solution_snapshot by meson
lemma ov_two_contexts_card:
"card (table_contexts ov_result p_entry) = 2"
unfolding ov_two_contexts by simp
text ‹‹main› itself runs only under the root context.›
lemma ov_caller_root_only:
"table_contexts ov_result (Statement 3) = {[]}"
using ov_solution_snapshot by blast+
subsection ‹2. Each seed carries its own alternative's entry›
text ‹
The seed at ‹[SPos]› holds the exact argument; the seed at ‹[STop]› holds the
forgotten one.
›
lemma ov_seed_exact:
"ov_seed [SPos] (STR ''a'') = Lifted SPos"
using ov_solution_snapshot by blast
lemma ov_seed_forgotten:
"ov_seed [STop] (STR ''a'') = Lifted STop"
using ov_solution_snapshot by blast+
text ‹The callee's entry unknown is exactly its seed: the seed read-back is its only
predecessor.›
lemma ov_entry_reads_seed:
"ov_read p_entry [SPos] (STR ''a'') = Lifted SPos"
"ov_read p_entry [STop] (STR ''a'') = Lifted STop"
using ov_solution_snapshot by blast+
subsection ‹3. Each activation returns what it was entered with, and stays paired›
text ‹
Each callee context returns the sign it was entered with, and each alternative's
combine pairs that result with its own continuation.
›
lemma ov_result_exact:
"ov_read p_result [SPos] ret_var = Lifted SPos"
using ov_solution_snapshot by blast+
lemma ov_result_forgotten:
"ov_read p_result [STop] ret_var = Lifted STop"
using ov_solution_snapshot by blast+
text ‹
Continuation/entry correlation, observed per alternative. The joined table cannot show
it: Sign is non-relational, so the join of ‹{(SPos, SPos), (STop, STop)}› at ‹(x, y)› is
the same ‹(STop, STop)› as the join of the swapped pairing. Traversing each alternative's
own tree against the solved table does show it: alternative 1's combine writes ‹y› from
the exact callee (\<^const>‹SPos›) into its own untouched continuation (‹x = SPos›),
alternative 2's writes ‹y› from the forgotten callee (\<^const>‹STop›) into its own
forgotten continuation (‹x = STop›).
›
lemma ov_alt1_pairing:
"ov_alt_read 0 (STR ''y'') = Lifted SPos"
"ov_alt_read 0 (STR ''x'') = Lifted SPos"
using ov_solution_snapshot by blast+
lemma ov_alt2_pairing:
"ov_alt_read 1 (STR ''y'') = Lifted STop"
"ov_alt_read 1 (STR ''x'') = Lifted STop"
using ov_solution_snapshot by blast+
subsection ‹4. The continuation holds the join of both alternatives›
text ‹Both ‹x› and ‹y› join to \<^const>‹STop›: alternative 2 forgets ‹x› in its own
continuation as well as ‹a› in its entry, so the imprecision this override costs shows up
on both variables once the two alternatives join --- exactly what the relational bucket
semantics below must account for instead of hiding.›
lemma ov_continuation_join:
"ov_read (Statement 4) [] (STR ''x'') = Lifted STop"
"ov_read (Statement 4) [] (STR ''y'') = Lifted STop"
using ov_solution_snapshot by blast+
subsection ‹5. Negative: an empty entry list cannot cover a live caller›
text ‹The concrete caller store at the call site has ‹x = 1› and every global
initialized to ‹0›.›
lemma ov_empty_pairs_never_cover:
"¬ entry_pairs_cover (λd' :: sign default_st lifted. γ (ρ⇘ov_gs⇙ d')) ov_caller_store
(call_enter ov_gs ov_ca ov_caller_store) []"
by simp
text ‹What the missing obligation would let through. With ‹enter⇧♯› answering ‹[]›, the
solver seeds no callee, materializes no context at ‹p›, and leaves the continuation
\<^const>‹Bot› --- although the concrete run reaches it. A relation admitting no context for
this call would produce the same empty buckets; conditional totality is what rules it out.›
definition ov_empty_spec ::
"(pp × sign list, (unit, sign list) global_unknown, unit,
sign default_st lifted, sign default_st lifted) dg_spec" where
"ov_empty_spec = (sign_tf.spec_exec ov_gs ov_ep)
⦇ dgs_enter := (λci. local_enter_transfer (λd. [])) ⦈"
lemmas [code] = ov_empty_spec_def[unfolded sign_tf.spec_exec_def]
definition ov_empty_eqs ::
"(pp × sign list, (unit, sign list) global_unknown,
(sign default_st lifted, sign default_st lifted) dg_state) eqsT" where
"ov_empty_eqs =
routed_node_rhs_buffered intra_predecessor_addr_list call_site_list (λ_. Analysis_Global ())
(exec_formals_route ov_gs)
(λctx' src a. dg_spec_edge_program ov_empty_spec a src (λ_. Analysis_Global ()))
(routed_call_program ov_empty_spec (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot))
(routed_entry_seed_programs Activation_Seed)
ov_cfg Bot (Lifted cinit_sign_st) Bot"
definition ov_empty_sol ::
"(pp × sign list) set ×
(pp × sign list + (unit, sign list) global_unknown
⇒ (sign default_st lifted, sign default_st lifted) dg_state)" where
"ov_empty_sol = TD_side_always_join_Interp_solve ov_empty_eqs (cfg_exit ov_cfg, [])"
lemmas ov_empty_unfold = ov_empty_sol_def ov_empty_eqs_def ov_empty_spec_def ov_cfg_def
ov_pi_def ov_procs_def ov_ep_def ov_program_def
lemma ov_empty_solution_snapshot_raw:
"(let sol = ov_empty_sol
in TD_side_always_join_Interp_solve_c ov_empty_eqs (cfg_exit ov_cfg, []) ≠ None
∧ (∀(v, ctx) ∈ fst sol. v ≠ p_entry)
∧ dg_local (snd sol (Inl (Statement 4, []))) = Bot)"
unfolding ov_empty_unfold sign_tf.spec_exec_def
by eval
lemma ov_empty_solution_snapshot:
"TD_side_always_join_Interp_solve_c ov_empty_eqs (cfg_exit ov_cfg, []) ≠ None
∧ (∀(v, ctx) ∈ fst ov_empty_sol. v ≠ p_entry)
∧ dg_local (snd ov_empty_sol (Inl (Statement 4, []))) = Bot"
using ov_empty_solution_snapshot_raw
unfolding Let_def
by blast
lemma ov_empty_terminates_c:
"TD_side_always_join_Interp_solve_c ov_empty_eqs (cfg_exit ov_cfg, []) ≠ None"
using ov_empty_solution_snapshot by blast
lemma ov_empty_no_callee_context:
"∀(v, ctx) ∈ fst ov_empty_sol. v ≠ p_entry"
using ov_empty_solution_snapshot by blast
lemma ov_empty_continuation_bot:
"dg_local (snd ov_empty_sol (Inl (Statement 4, []))) = Bot"
using ov_empty_solution_snapshot by blast
lemma ov_call_site_dg_local_probe:
"dg_local (snd ov_sol (Inl (Statement 3, [])))
= default_st_set_lift (Lifted cinit_sign_st) (location_of ov_gs (STR ''x'')) SPos"
using ov_solution_snapshot by blast+
lemma ov_call_site_reader:
"ρ⇘ov_gs⇙ (dg_local (snd ov_sol (Inl (Statement 3, []))))
= Lifted ((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := SPos))"
unfolding ov_call_site_dg_local_probe default_st_set_lift_def
by (simp add: is_bottom_sign_def)
lemma ov_caller_store_covered:
"ov_caller_store ∈ γ (ρ⇘ov_gs⇙ (dg_local (snd ov_sol (Inl (Statement 3, [])))))"
unfolding gamma_lift_default_st_gamma_to_fun ov_call_site_reader
gamma_lift_Lifted gamma_state_def
proof (rule CollectI, rule allI)
fix y
show "ov_caller_store y
∈ γ (((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := SPos)) y)"
by (cases "y = STR ''x''")
(simp_all add: default_st_to_fun_initial gamma_sign_top ov_caller_store_def)
qed
lemma ov_alt1_route:
"exec_formals_route ov_gs (Statement 3) []
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, [])))))
ov_ca = [SPos]"
using ov_solution_snapshot by blast
lemma ov_entry1_not_empty_probe:
"¬ ov_ep
(enter_frame_D_default_st STop
cinit_sign_st⟨location_of ov_gs (STR ''x'') := SPos⟩)
⟨location_of ov_gs (STR ''a'') := SPos⟩"
by eval
lemma ov_entry1_dg_local_exact:
"transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, []))))
= Lifted
(enter_frame_D_default_st STop
cinit_sign_st⟨location_of ov_gs (STR ''x'') := SPos⟩)
⟨location_of ov_gs (STR ''a'') := SPos⟩"
unfolding ov_call_site_dg_local_probe default_st_set_lift_def
by (simp add: generic_enter_st_for_def top_sign_def bind_formals_default_st_singleton
is_bottom_sign_def normalize_lift_def ov_entry1_not_empty_probe)
lemma ov_entry1_reader:
"map_lift ρ⇘ov_gs⇙
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, [])))))
= Lifted ((enter_frame ov_gs STop
((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := SPos)))
(STR ''a'' := SPos))"
unfolding ov_entry1_dg_local_exact by simp
lemma ov_entry2_reader:
"map_lift ρ⇘ov_gs⇙
(map_lift (forget_formals ov_gs (call_info_of ov_ca (STR ''p'')))
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, []))))))
= Lifted ((enter_frame ov_gs STop
((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := SPos)))
(STR ''a'' := STop))"
unfolding forget_formals_def ov_entry1_dg_local_exact by simp
lemma ov_cont2_dg_local_probe:
"forget_var ov_gs (STR ''x'') STop (dg_local (snd ov_sol (Inl (Statement 3, []))))
= default_st_set_lift (Lifted cinit_sign_st) (location_of ov_gs (STR ''x'')) STop"
using ov_solution_snapshot by blast
lemma ov_cont2_reader:
"map_lift ρ⇘ov_gs⇙
(forget_var ov_gs (STR ''x'') STop (dg_local (snd ov_sol (Inl (Statement 3, [])))))
= Lifted (((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := STop)))"
unfolding ov_cont2_dg_local_probe default_st_set_lift_def
by (simp add: is_bottom_sign_def)
lemma ov_cont2_covered:
"ov_caller_store
∈ γ (ρ⇘ov_gs⇙ (forget_var ov_gs (STR ''x'') STop (dg_local (snd ov_sol (Inl (Statement 3, []))))))"
unfolding gamma_lift_default_st_gamma_to_fun ov_cont2_reader
gamma_lift_Lifted gamma_state_def
proof (rule CollectI, rule allI)
fix y
show "ov_caller_store y
∈ γ (((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := STop)) y)"
by (cases "y = STR ''x''")
(simp_all add: default_st_to_fun_initial gamma_sign_top ov_caller_store_def)
qed
lemma ov_entry1_covered:
"call_enter ov_gs ov_ca ov_caller_store
∈ γ (ρ⇘ov_gs⇙ (transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, []))))))"
unfolding gamma_lift_default_st_gamma_to_fun ov_entry1_reader
gamma_lift_Lifted gamma_state_def
proof (rule CollectI, rule allI)
fix y
show "call_enter ov_gs ov_ca ov_caller_store y
∈ γ (((enter_frame ov_gs STop
((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := SPos)))
(STR ''a'' := SPos)) y)"
by (cases "y = STR ''a''")
(simp_all add: call_enter_CallEdge ov_caller_store_def gamma_sign_top
default_st_to_fun_initial)
qed
lemma ov_entry2_covered:
"call_enter ov_gs ov_ca ov_caller_store
∈ γ (ρ⇘ov_gs⇙ (map_lift (forget_formals ov_gs (call_info_of ov_ca (STR ''p'')))
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, [])))))))"
unfolding gamma_lift_default_st_gamma_to_fun ov_entry2_reader
gamma_lift_Lifted gamma_state_def
proof (rule CollectI, rule allI)
fix y
show "call_enter ov_gs ov_ca ov_caller_store y
∈ γ (((enter_frame ov_gs STop
((ρ⇘ov_gs⇙ cinit_sign_st)(STR ''x'' := SPos)))
(STR ''a'' := STop)) y)"
by (cases "y = STR ''a''")
(simp_all add: call_enter_CallEdge ov_caller_store_def gamma_sign_top
default_st_to_fun_initial)
qed
lemma ov_alt2_route:
"exec_formals_route ov_gs (Statement 3) []
(map_lift (forget_formals ov_gs (call_info_of ov_ca (STR ''p'')))
(transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs (call_info_of ov_ca (STR ''p'')))
(dg_local (snd ov_sol (Inl (Statement 3, []))))))
ov_ca = [STop]"
using ov_solution_snapshot by blast
subsection ‹Soundness through the relational context layer›
text ‹
\<^const>‹routed_entry_context_rel› at \<^const>‹ov_enter›: the relation this instance keys
its collecting semantics by. None of the crux corollaries below is stateable with the
retired functional selector, whose singleton premise this override deliberately breaks.
›
abbreviation ov_R :: "sign list context_policy" where
"ov_R ≡ routed_entry_context_rel (ov_enter ov_gs ov_ep) (λd _. γ (ρ⇘ov_gs⇙ d)) (snd ov_sol)
(λ_::unit. Analysis_Global ()) (exec_formals_route ov_gs)"
text ‹An abbreviation is transparent to unification, but ‹meson› needs an explicit
rewrite rule to fold a fully applied ‹routed_entry_context_rel› instance back into
‹ov_R›; this lemma is that rule.›
lemma ov_R_eq:
"ov_R = ov_R"
by (rule refl)
lemma ov_exact: "ov_ep s = is_empty_state (ρ⇘ov_gs⇙ s)"
unfolding ov_ep_def by (rule default_st_is_bot_for_iff) simp
lemma ov_fwd_closed_all:
"∀(u, ctx) ∈ fst ov_sol. ∀(u', a, v) ∈ intra ov_cfg. u = u' ⟶ (v, ctx) ∈ fst ov_sol"
using ov_solution_snapshot by meson
lemma ov_fwd_ok:
assumes "(u, ctx) ∈ fst ov_sol" and "(u, a, v) ∈ intra ov_cfg"
shows "(v, ctx) ∈ fst ov_sol"
using ov_fwd_closed_all assms by fastforce
lemma ov_comb_fwd_closed_all:
"∀(cl, c1) ∈ fst ov_sol. ∀(cl', ca, ce, cont) ∈ calls ov_cfg. cl = cl' ⟶ (cont, c1) ∈ fst ov_sol"
using ov_solution_snapshot by meson
lemma ov_comb_fwd_ok:
assumes "(cl, c1) ∈ fst ov_sol" and "(cl, ca, ce, cont) ∈ calls ov_cfg"
shows "(cont, c1) ∈ fst ov_sol"
using ov_comb_fwd_closed_all assms by fastforce
text ‹The routed destination an admitted entry points at is already in the solved table.
Bounded by \<^term>‹fst ov_sol› and ‹set (ov_enter ov_gs ov_ep ci d)› (both finite), so
‹eval› decides it directly instead of symbolically rewriting the whole solved table.›
lemma ov_enter_fwd_at_call:
"∀(u, ctx) ∈ fst ov_sol. u = Statement 3 ⟶
(∀(cont', entry) ∈ set (ov_enter ov_gs ov_ep (call_info_of ov_ca (STR ''p''))
(dg_local (snd ov_sol (Inl (u, ctx))))).
(p_entry, exec_formals_route ov_gs u ctx entry ov_ca) ∈ fst ov_sol)"
using ov_solution_snapshot by blast+
lemma ov_pp_st:
"part_post_solution ov_eqs (cfg_exit ov_cfg, []) (snd ov_sol) (fst ov_sol)"
using TD_side_always_join_Interp.part_post_solution_of_solve_c[OF ov_terminates_c]
unfolding ov_sol_def by simp
lemma ov_intra_side_free:
"sides_of_program (dg_spec_edge_program (ov_spec ov_gs ov_ep) a src g) τ z = bot"
unfolding dg_spec_edge_program_def dg_spec_step_ov_spec sign_tf.spec_exec_def
by (simp add: dg_spec_step_exec_dg_spec)
lemma dg_spec_combine_transfer_ov_spec [simp]:
"dg_spec_combine_transfer (ov_spec 𝒢 ep) ci m exit
= dg_spec_combine_transfer (sign_tf.spec_exec 𝒢 ep) ci m exit"
by (simp add: dg_spec_combine_transfer_def)
lemma ov_cmb_side_free_at_analysis_global:
"sides_of_program (routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) route ctx ca cc v) sigma (Inr (Analysis_Global ())) = bot"
proof (rule routed_call_program_side_free_at_buffer_key[OF dg_spec_wf_ov_spec])
show "⋀ci d pairs pub. enter_runs (enter⇧♯ (ov_spec ov_gs ov_ep) ci)
(mk_dg_man d (λ_. Analysis_Global ())) sigma pairs pub ⟹ pub (Inr (Analysis_Global ())) = bot"
unfolding dgs_enter_ov_spec
by (auto simp: bot_fun_def dest: enter_runs_local_pub_bot)
next
show "⋀ci d. ∃pairs pub. enter_runs (enter⇧♯ (ov_spec ov_gs ov_ep) ci)
(mk_dg_man d (λ_. Analysis_Global ())) sigma pairs pub"
unfolding dgs_enter_ov_spec by blast
next
show "⋀ci d de z. sides_of_rhs (sp_compile_with (λx. DG x bot)
(dg_spec_combine_transfer (ov_spec ov_gs ov_ep) ci
(mk_dg_man d (λ_. Analysis_Global ())) de))
sigma z = bot"
by (simp add: sign_tf.spec_exec_def dg_spec_combine_transfer_exec_dg_spec
sp_compile_with_def local_combine_transfer_def sp_return_def bot_dg_state_def)
next
show "⋀p ctx'. Activation_Seed (FunctionEntry p) ctx' ≠ Analysis_Global ()"
by simp
qed
text ‹The buffered post-solution reconciled with the unbuffered generator the routed
locale is stated over. Only the entry differs from \<^const>‹sign_tf.spec_exec›, and none of the
bridge's side-freeness obligations inspect what \<^const>‹dgs_enter› answers with --- they
hold for any list of alternatives, exactly as \<^theory>‹Voblint_Exec.Routed_Exec_Refinement›
discharges them once for every deterministic instance.›
lemma ov_pp_routed:
"part_post_solution
(routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. Analysis_Global ())
(exec_formals_route ov_gs)
(λctx' src a. dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ()))
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot))
(routed_entry_seed_programs Activation_Seed)
ov_cfg Bot (Lifted cinit_sign_st) Bot)
(cfg_exit ov_cfg, []) (snd ov_sol) (fst ov_sol)"
proof (rule part_post_solution_routed_node_rhs_buffered
[where it_c =
"λctx' src a.
dg_spec_edge_program (ov_spec ov_gs ov_ep) a src
(λ_. Analysis_Global ())"
and cmb_c = "routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot)"])
show "⋀c' w. ∀p ∈ set (routed_contribution_programs
intra_predecessor_addr_list call_site_list (exec_formals_route ov_gs)
(λctx' src a. dg_spec_edge_program (ov_spec ov_gs ov_ep) a src
(λ_. Analysis_Global ()))
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot))
(routed_entry_seed_programs Activation_Seed) ov_cfg c' w). sp_wf p"
by (rule routed_contribution_programs_wf)
(auto intro: sp_wf_dg_spec_edge_program[OF dg_spec_wf_ov_spec]
sp_wf_routed_call_program[OF dg_spec_wf_ov_spec])
next
show "⋀c' w. ∀p ∈ set (routed_contribution_programs
intra_predecessor_addr_list call_site_list (exec_formals_route ov_gs)
(λctx' src a. dg_spec_edge_program (ov_spec ov_gs ov_ep) a src
(λ_. Analysis_Global ()))
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot))
(routed_entry_seed_programs Activation_Seed) ov_cfg c' w). sp_wf p"
by (rule routed_contribution_programs_wf)
(auto intro: sp_wf_dg_spec_edge_program[OF dg_spec_wf_ov_spec]
sp_wf_routed_call_program[OF dg_spec_wf_ov_spec])
next
show "⋀c' src a τ. edge_out (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ()) τ
= edge_out (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ()) τ"
by (rule refl)
next
show "⋀c' src a τ. dg_local (sides_of_program
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ())) τ
(Inr (Analysis_Global ()))) = bot"
by (simp add: ov_intra_side_free bot_dg_state_def)
next
show "⋀c' src a τ. dg_global (traverse_program
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ())) τ)
= dg_global (sides_of_program
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ())) τ
(Inr (Analysis_Global ())))"
by (simp add: ov_intra_side_free dg_spec_edge_program_def sign_tf.spec_exec_def
dg_spec_step_exec_dg_spec bot_dg_state_def)
next
show "⋀c' src a τ. sides_of_program
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ())) τ
(Inr (Analysis_Global ())) = bot"
by (rule ov_intra_side_free)
next
show "⋀c' src a τ z. z ≠ Inr (Analysis_Global ()) ⟹
sides_of_program
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ())) τ z
= sides_of_program
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src
(λ_. Analysis_Global ())) τ z"
by (rule refl)
next
show "⋀c' src a τ. dep_program τ
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ()))
= dep_program τ
(dg_spec_edge_program (ov_spec ov_gs ov_ep) a src (λ_. Analysis_Global ()))"
by (rule refl)
next
show "⋀c' ca cc ex τ. dg_local (traverse_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ)
= dg_local (traverse_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ)"
by (rule refl)
next
show "⋀c' ca cc ex τ. dg_local (sides_of_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ
(Inr (Analysis_Global ()))) = bot"
by (simp add: ov_cmb_side_free_at_analysis_global bot_dg_state_def del: unit_abs_eta_conv)
next
show "⋀c' ca cc ex τ. dg_global (traverse_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ)
= dg_global (sides_of_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ
(Inr (Analysis_Global ())))"
by (simp add: routed_call_program_global_free ov_cmb_side_free_at_analysis_global
bot_dg_state_def del: unit_abs_eta_conv)
next
show "⋀c' ca cc ex τ. sides_of_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ
(Inr (Analysis_Global ())) = bot"
by (rule ov_cmb_side_free_at_analysis_global)
next
show "⋀c' ca cc ex τ z. z ≠ Inr (Analysis_Global ()) ⟹
sides_of_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ z
= sides_of_program
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ())
Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex) τ z"
by (rule refl)
next
show "⋀c' ca cc ex τ. dep_program τ
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex)
= dep_program τ
(routed_call_program (ov_spec ov_gs ov_ep) (λ_. Analysis_Global ()) Activation_Seed
(static_resolve ov_cfg) (λd. d = Bot) (exec_formals_route ov_gs) c' ca cc ex)"
by (rule refl)
next
show "⋀c' w τ z x. x ∈ set (routed_entry_seed_programs Activation_Seed
(exec_formals_route ov_gs) c' w) ⟹ sides_of_program x τ z = bot"
by (rule routed_entry_seed_programs_free)
next
show "⋀c' w τ x. x ∈ set (routed_entry_seed_programs Activation_Seed
(exec_formals_route ov_gs) c' w) ⟹ dg_global (traverse_program x τ) = bot"
by (rule routed_entry_seed_programs_local_only)
qed (rule ov_pp_st[unfolded ov_eqs_def])
interpretation ov_core: analysis_contract "ov_spec ov_gs ov_ep" "(λd _. γ (ρ⇘ov_gs⇙ d))" ov_gs
by (rule analysis_contract_ov_spec[OF ov_exact])
text ‹The routed context locale, fully interpreted: every alternative's continuation is a
sound description of the caller (‹EnterTotal›), the routed table reflects whichever
alternative a concrete relational admission points at (‹EnterCover›), and a return
leaves the continuation covered at the caller's own context (‹CombFwd›).›
ov_routed: routed_context
"ov_spec ov_gs ov_ep" "(λd _. γ (ρ⇘ov_gs⇙ d))" ov_gs ov_cfg "Analysis_Global ()"
"λ_. Analysis_Global ()" "exec_formals_route ov_gs" Bot "Lifted cinit_sign_st" Bot
"snd ov_sol" "fst ov_sol" "(cfg_exit ov_cfg, [])"
"solved_local_reader (fst ov_sol) (snd ov_sol)" Activation_Seed
"static_resolve ov_cfg" "λd. d = Bot"
"gamma_lift (default_st_gamma ov_gs)" ov_R
proof (rule routed_context.intro
[OF dg_context_activation.intro[OF analysis_contract_ov_spec[OF ov_exact]]],
unfold_locales, goal_cases CmbWf ExtraWf FinE PP SgCov SgUncov Fwd FinC CallsUnique
SeedUnknown SeedNeGlobal IsBotBot IsBotSound ResolveSound EnterCover EnterTotal CombFwd)
case CmbWf show ?case by (rule sp_wf_routed_call_program[OF dg_spec_wf_ov_spec])
next
case ExtraWf then show ?case by (rule sp_wf_routed_entry_seed_programs)
next
case FinE show ?case unfolding ov_cfg_def by (simp add: compile_prog_finite)
next
case PP show ?case by (rule post_bounded_of_part_post_solution[OF ov_pp_routed])
next
case (SgCov v ctx)
thus ?case by (simp add: solved_local_reader_def gamma_lift_default_st_gamma_to_fun
declared_global_def[abs_def])
next
case (SgUncov v ctx)
thus ?case by (simp add: solved_local_reader_def)
next
case (Fwd u a v ctx)
show ?case by (rule ov_fwd_ok [OF Fwd(1) Fwd(3)])
next
case FinC show ?case unfolding ov_cfg_def by (simp add: compile_prog_finite)
next
case CallsUnique show ?case
unfolding ov_cfg_def calls_source_unique_def using compile_prog_calls_source_unique
by blast
next
case (SeedUnknown p ctx) show ?case by simp
next
case (SeedNeGlobal p ctx v) show ?case by simp
next
case IsBotBot show ?case by simp
next
case (IsBotSound d gv) then show ?case by simp
next
case (ResolveSound u ctx dst pars args p cont s)
thus ?case unfolding ov_cfg_def by (simp add: compile_prog_finite)
next
case (EnterCover u ctx dst pars args p cont s ctx')
note ce = EnterCover(2) and Rc = EnterCover(4)
let ?ci = "call_info_of (CallEdge dst pars args) p"
let ?d = "dg_local (snd ov_sol (Inl (u, ctx)))"
obtain cont' entry
where mem: "(cont', entry) ∈ set (ov_enter ov_gs ov_ep ?ci ?d)"
and ccov:
"s ∈ γ (ρ⇘ov_gs⇙ cont')"
and ecov: "call_enter ov_gs (CallEdge dst pars args) s
∈ γ (ρ⇘ov_gs⇙ entry)"
and req: "ctx' = exec_formals_route ov_gs u ctx entry (CallEdge dst pars args)"
using routed_entry_context_relE[OF Rc] by (auto simp: declared_global_def[abs_def])
have Rr: "enter_runs (enter⇧♯ (ov_spec ov_gs ov_ep) ?ci) (mk_dg_man ?d (λ_. Analysis_Global ()))
(snd ov_sol) (ov_enter ov_gs ov_ep ?ci ?d) bot"
by (simp add: enter_runs_local_enter_transfer_mk_dg_man)
have D: "enter_deps (enter⇧♯ (ov_spec ov_gs ov_ep) ?ci) (mk_dg_man ?d (λ_. Analysis_Global ()))
(snd ov_sol) (ov_enter ov_gs ov_ep ?ci ?d) {}"
by (simp add: enter_deps_local_enter_transfer_mk_dg_man)
have upin: "u = Statement 3" and caeq: "CallEdge dst pars args = ov_ca"
and ceeq: "FunctionEntry p = p_entry"
using ov_calls_shape ce by auto
have peq: "p = STR ''p''" using ceeq by simp
have fwd: "(FunctionEntry p, ctx') ∈ fst ov_sol"
proof -
have mm: "(u, ctx) ∈ fst ov_sol" using EnterCover(1) .
have "(p_entry, exec_formals_route ov_gs u ctx entry ov_ca) ∈ fst ov_sol"
using ov_enter_fwd_at_call mm upin mem[unfolded caeq peq] by blast
then show ?thesis unfolding req caeq ceeq by simp
qed
show ?case using Rr D mem ccov ecov req fwd by blast
next
case (EnterTotal u ctx dst pars args p cont s)
let ?ci = "call_info_of (CallEdge dst pars args) p"
let ?d = "dg_local (snd ov_sol (Inl (u, ctx)))"
show ?case
proof (rule routed_entry_context_rel_total)
show "entry_pairs_cover
(λd'. γ (ρ⇘ov_gs⇙ d'))
s (call_enter ov_gs (CallEdge dst pars args) s) (ov_enter ov_gs ov_ep ?ci ?d)"
unfolding ov_enter_def Let_def
using sign_tf.entry_cover_exec[OF ov_exact EnterTotal(3), where ci = ?ci]
unfolding entry_pairs_cover_def by auto
qed
next
case (CombFwd cl c1 dst pars args p cont)
thus ?case by (rule ov_comb_fwd_ok)
qed
lemma ov_pos_context_admitted:
"[SPos] ∈ ov_R (Statement 3) []
(call_info_of ov_ca (STR ''p''))
ov_caller_store
(call_enter ov_gs ov_ca ov_caller_store)"
proof -
let ?ci = "call_info_of ov_ca (STR ''p'')"
let ?d = "dg_local (snd ov_sol (Inl (Statement 3, [])))"
let ?entry = "transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs ?ci) ?d"
have mem: "(?d, ?entry) ∈ set (ov_enter ov_gs ov_ep ?ci ?d)"
unfolding ov_enter_def Let_def by simp
have caedge: "CallEdge (ci_dst ?ci) (ci_formals ?ci) (ci_args ?ci) = ov_ca"
by simp
show ?thesis
using routed_entry_context_relI[
where alts = "ov_enter ov_gs ov_ep" and γ⇩D⇩G = "(λd _. γ (ρ⇘ov_gs⇙ d))"
and sigma = "snd ov_sol" and global_of = "λ_::unit. Analysis_Global ()"
and route = "exec_formals_route ov_gs" and u = "Statement 3" and ctx = "[]",
OF mem
ov_caller_store_covered
ov_entry1_covered,
unfolded caedge, unfolded ov_alt1_route]
by (meson ov_R_eq)
qed
lemma ov_top_context_admitted:
"[STop] ∈ ov_R (Statement 3) []
(call_info_of ov_ca (STR ''p''))
ov_caller_store
(call_enter ov_gs ov_ca ov_caller_store)"
proof -
let ?ci = "call_info_of ov_ca (STR ''p'')"
let ?d = "dg_local (snd ov_sol (Inl (Statement 3, [])))"
let ?cont2 = "forget_var ov_gs (STR ''x'') STop ?d"
let ?entry1 = "transfer_lift ov_ep (generic_enter_st_for sign_ops ov_gs ?ci) ?d"
let ?entry2 = "map_lift (forget_formals ov_gs ?ci) ?entry1"
have mem: "(?cont2, ?entry2) ∈ set (ov_enter ov_gs ov_ep ?ci ?d)"
unfolding ov_enter_def Let_def by simp
have caedge: "CallEdge (ci_dst ?ci) (ci_formals ?ci) (ci_args ?ci) = ov_ca"
by simp
show ?thesis
using routed_entry_context_relI[
where alts = "ov_enter ov_gs ov_ep" and γ⇩D⇩G = "(λd _. γ (ρ⇘ov_gs⇙ d))"
and sigma = "snd ov_sol" and global_of = "λ_::unit. Analysis_Global ()"
and route = "exec_formals_route ov_gs" and u = "Statement 3" and ctx = "[]",
OF mem
ov_cont2_covered
ov_entry2_covered,
unfolded caedge, unfolded ov_alt2_route]
by (meson ov_R_eq)
qed
lemma ov_two_contexts_admitted:
"[SPos] ∈ ov_R (Statement 3) [] (call_info_of ov_ca (STR ''p''))
ov_caller_store (call_enter ov_gs ov_ca ov_caller_store)
∧ [STop] ∈ ov_R (Statement 3) [] (call_info_of ov_ca (STR ''p''))
ov_caller_store (call_enter ov_gs ov_ca ov_caller_store)
∧ [SPos] ≠ [STop]"
using ov_pos_context_admitted ov_top_context_admitted by simp
subsection ‹What this shows›
text ‹
Proven, executably: the call/combine machinery keeps two overlapping alternatives
distinguishable end to end --- each is read back through its own continuation
(‹ov_alt1_pairing›/‹ov_alt2_pairing›) and reaches two distinct contexts at ‹p_entry›
(‹ov_two_contexts›), something the retired functional selector, whose singleton
premise this override deliberately breaks, could not even state.
Proven, relationally: the existing generic routed soundness bridge
(\<^theory>‹Voblint_Exec.Routed_Exec_Refinement›) already supports list-valued,
non-deterministic entry without any change to it --- ‹ov_pp_routed› discharges the full
buffered/unbuffered reconciliation for this override, since none of its side-freeness
obligations inspect what the entry list contains, only that it is
\<^const>‹local_enter_transfer›-shaped, which ‹ov_enter› already is. This example supplies
and discharges the corresponding non-deterministic entry obligations
(‹routed_context›'s ‹EnterCover›/‹EnterTotal›/‹CombFwd›) for the first time,
and ‹ov_two_contexts_admitted› above names the one concrete call transition that genuinely
admits the callee activation under both ‹[SPos]› and ‹[STop]› via ‹ov_R› --- not merely that
two contexts exist somewhere in the abstract table, but that this call's own admitted-context
relation holds for both. The caller itself stays at its own context, ‹[]›; it is the callee
activation this one call reaches that is admitted under two contexts at once.
Negative: an empty entry list admits no context at all for this call, so the seed
never covers the live caller --- ‹ov_empty_pairs_never_cover› above is exactly the
missing obligation \<^const>‹call_context_total_on› rules out.
›
unbundle no default_st_syntax
end