Theory Example_Interval_DG_IP_Flagship
theory Example_Interval_DG_IP_Flagship
imports
Example_Interval_DG_Flagship
begin
section ‹The context-insensitive (monovariant) interval flagship›
text ‹
This is the non-context IP baseline: every call to ‹twice› is analyzed
under a single, shared abstract state at ‹FunctionEntry (STR ''twice'')›,
regardless of which call site reached it. It is the flagship the
context-sensitive sibling ‹Example_Interval_DG_Ctx_Flagship› sharpens by
routing on the entered argument's abstract value -- so run this file first to
see the precision loss two calls to the same procedure with different
arguments incur when their entry states are forced to join, then compare
against the routed variant.
›
definition twice_program :: imp_prog where
"twice_program = program {
fun twice(p) { return p + p; }
fun main() { x = twice(3); y = twice(10); }
}"
definition twice_pi :: proc_table where "twice_pi = prog_table twice_program"
definition twice_procs :: "pname list" where "twice_procs = prog_procs twice_program"
definition twice_main :: "VIMP_Proc.com" where "twice_main = prog_main twice_program"
text ‹The storage classifier: ‹twice_program› declares no globals, so ‹twice_gs›
classifies every variable this chain touches as local, matching the
‹declared_global› pattern used by every other flagship rather than
the retired convention that read a name starting with ‹G› as global.›
abbreviation twice_gs :: "vname ⇒ bool" where
"twice_gs ≡ declared_global twice_program"
definition twice_cfg :: cfg where
"twice_cfg = compile_prog twice_pi twice_procs"
text ‹
The compiled CFG. Procedure ‹twice› runs between
‹FunctionEntry (STR ''twice'')› and ‹FunctionResult (STR ''twice'')›: the body's ‹return p + p›
publishes through ‹EA_Ret› at statement ‹0›. ‹twice› never falls through, so the
continuation-passing compiler reserves no epilogue edge --- statement ‹1› is an
unused index, not a node of the compiled graph. ‹main› occupies statements ‹2..4›:
‹2› is the first call site, continuing directly at ‹3›, which is also the second
call site, continuing at ‹4›. Both call edges name the same callee entry
‹FunctionEntry (STR ''twice'')› --- this is the monovariant (single-context) view.
›
interpretation twice: compiled_cfg twice_pi twice_procs twice_cfg
by (unfold_locales; unfold twice_cfg_def; simp add: compile_prog_finite)
text ‹The two call edges' shape, computed directly from ‹twice_cfg›: each call site ‹u›
pins down its destination variable, callee, arguments, and continuation. Exported for the
routed/context-sensitive sibling ‹Example_Interval_DG_Ctx_Collect›, which case-splits on
the same two call sites.›
lemma twice_calls_shape:
"∀(u, ca, ce, cont) ∈ calls twice_cfg.
case ca of CallEdge dst pars args ⇒
(case ce of FunctionEntry p ⇒
(u = Statement 2 ∧ dst = Some (STR ''x'') ∧ pars = [(STR ''p'')]
∧ args = [VIMP_Syntax.N 3]
∧ p = (STR ''twice'') ∧ cont = Statement 3) ∨
(u = Statement 3 ∧ dst = Some (STR ''y'') ∧ pars = [(STR ''p'')]
∧ args = [VIMP_Syntax.N 10]
∧ p = (STR ''twice'') ∧ cont = Statement 4)
| _ ⇒ True)"
unfolding twice_cfg_def by eval
text ‹Each call site has exactly one outgoing edge.›
lemma twice_calls_unique_site:
"∀(u1, ca1, ce1, k1) ∈ calls twice_cfg. ∀(u2, ca2, ce2, k2) ∈ calls twice_cfg.
u1 = u2 ⟶ ca1 = ca2 ∧ ce1 = ce2 ∧ k1 = k2"
unfolding twice_cfg_def by eval
lemma twice_cfg_prog_cfg: "twice_cfg = prog_cfg twice_program"
by (simp add: twice_cfg_def twice_pi_def twice_procs_def prog_cfg_def)
subsection ‹The analysis, and its equation system at this program›
text ‹The analysis is the one ‹Example_Interval_DG_Flagship› runs: Interval at the
unit context, solved with the joining global rule \<^const>‹Globals_Join›.
Both call sites publish into the one seed
‹Activation_Seed (FunctionEntry (STR ''twice'')) ()›, which is the monovariant view.›
definition twice_eqs ::
"pp × unit
⇒ (pp × unit, (unit, unit) global_unknown,
(ivl default_st lifted, ivl default_st lifted) dg_state) strategy_tree" where
"twice_eqs = interval_rule.equations twice_gs twice_program"
lemma twice_terminates_c:
"TD_side_rule_Interp_solve_c Globals_Join twice_eqs (cfg_exit twice_cfg, ()) ≠ None"
by eval
lemma twice_terminates: "interval_rule.terminates Globals_Join twice_gs twice_program"
unfolding interval_rule.terminates_code
using TD_side_rule_Interp.solve_dom_of_solve_c[OF twice_terminates_c]
by (simp add: twice_eqs_def twice_cfg_prog_cfg)
subsection ‹Inspecting the certified result›
text ‹The published state at a program point, at the one unit context.›
abbreviation twice_at :: "pp ⇒ ivl abs_state" where
"twice_at ≡ interval_rule.state_at Globals_Join twice_gs twice_program ()"
lemma twice_p_at_entry:
"twice_at (FunctionEntry (STR ''twice'')) (STR ''p'')
= Ivl (Fin 3) (Fin 10)"
by eval
lemma twice_ret_at_exit:
"twice_at (FunctionResult (STR ''twice''))
(STR ''#ret'') = Ivl (Fin 6) (Fin 20)"
by eval
lemma twice_x_computed:
"twice_at (Statement 3) (STR ''x'')
= Ivl (Fin 6) (Fin 20)"
by eval
lemma twice_y_computed:
"twice_at (Statement 4) (STR ''y'')
= Ivl (Fin 6) (Fin 20)"
by eval
subsection ‹Source-level soundness›
text ‹
‹twice_source_run_sound›: every store a source run of ‹twice› reaches lies in the
concretization of ‹twice_at› at the matching CFG node. ‹twice_wf› discharges
the compile-input premise.
›
lemma twice_main_body [simp]: "main_body twice_pi = twice_main"
by (simp add: main_body_def prog_main_name_def twice_pi_def twice_program_def
twice_main_def)
lemma twice_wf: "wf_compile_input twice_gs twice_pi twice_procs"
unfolding wf_compile_input_def
by (auto simp: wf_compile_input_simps
twice_pi_def twice_procs_def twice_main_def twice_program_def
split: if_splits option.splits)
theorem twice_source_run_sound:
assumes run: "twice_gs, twice_pi ⊢ (twice_main, s, []) →⇩p⇧* src'"
and init: "s ∈ cinit_stores twice_gs"
shows "∃v t stk. twice_pi, twice_cfg, prog_main_name ⊢ src' ≈ (v, t, stk)
∧ t ∈ γ (twice_at v)"
proof -
obtain residual t frs where src': "src' = (residual, t, frs)" by (cases src')
have run':
"twice_gs, prog_table twice_program ⊢ (main_body (prog_table twice_program), s, []) →⇩p⇧* (residual, t, frs)"
using run[unfolded src'] by (simp flip: twice_pi_def)
have wf: "wf_compile_input twice_gs (prog_table twice_program) (prog_procs twice_program)"
using twice_wf by (simp add: twice_pi_def twice_procs_def)
have unit_route: "⋀u ctx d ca s. route_unit u ctx d ca = enterc_unit u ctx s" by simp
have cert:
"∃v stk. twice_pi, twice_cfg, prog_main_name ⊢ (residual, t, frs) ≈ (v, t, stk)
∧ t ∈ γ (twice_at v)"
using interval_rule.fun_route_source_sound[OF unit_route wf twice_terminates init run']
by (simp add: twice_cfg_prog_cfg twice_pi_def)
show ?thesis using cert src' by blast
qed
end