Theory Voblint_Examples_Interval.Example_Interval_DG_Flagship
section ‹Flagship: interval analysis of a counting loop, executed and certified on the D/G spine›
text ‹
A bounded counting loop is compiled to a CFG, the D/G framework turns that graph into
an equation system, the verified solver computes an interval solution for it inside
Isabelle, and the context-insensitive analysis turns that solution into a statement
about every VIMP run of the source:
‹flagship_source_run_sound› bounds every store a run reaches by the published state at
its matched program point. The bound is informative --- ‹x in [0,20]› at the loop head,
‹[0,19]› in the body, ‹[20,20]› on exit --- and ‹flagship_head_bound_proper› exhibits a
store it rejects.
The analysis is Interval's production registration at the unit context,
‹interval_rule›, with the joining global rule ‹Globals_Join›.
‹Example_Interval_DG_IP_Flagship› runs the same analysis on a program with
calls.
›
theory Example_Interval_DG_Flagship
imports
"Voblint_Analysis_Interval.Interval_Analyses"
"Voblint_VIMP.VIMP_Notation"
"Voblint_Examples_CFG.Example_Compile_Call_Free"
begin
subsection ‹The VIMP source program›
text ‹
A bounded counting loop: initialise ‹x› to ‹0›, increment while ‹x < 20›. On
exit ‹x = 20›. No procedures, no globals; ‹x› is a single flow-sensitive local.
The analysis must ∗‹discover› the bound, not assume it. The regression
‹tests/regression/02-control-flow/precision/11-bounded_loop_guard_refines_body.vimp›
pins the same loop's head, body and exit values through the CLI.
›
definition flagship_prog :: imp_prog where
"flagship_prog = program { fun main() { x = 0; while (x < 20) { x = x + 1; } } }"
text ‹The storage classifier: ‹flagship_prog› declares no globals, so ‹flagship_gs›
classifies ‹x› as local.›
abbreviation flagship_gs :: "vname ⇒ bool" where
"flagship_gs ≡ declared_global flagship_prog"
subsection ‹CFG construction›
text ‹
The source compiles to an interprocedural CFG by ‹compile_prog›. The whole program is
the body of ‹main›, so it runs between ‹FunctionEntry (STR ''main'')› and
‹FunctionResult (STR ''main'')›; inside, ‹x := 0› falls directly into the loop head ‹1› (the
continuation-passing compiler needs no separate join node), the guard ‹x < 20› branches
to body ‹2› or exit ‹3›, and the increment at ‹2› jumps back to ‹1›.
›
definition flagship_pi :: proc_table where
"flagship_pi = prog_table flagship_prog"
definition flagship_cfg :: cfg where
"flagship_cfg = compile_prog flagship_pi (prog_procs flagship_prog)"
interpretation flagship: compiled_cfg flagship_pi "prog_procs flagship_prog" flagship_cfg
by (unfold_locales; unfold flagship_cfg_def; simp add: compile_prog_finite)
lemma flagship_calls: "calls flagship_cfg = {}"
unfolding flagship_cfg_def flagship_pi_def
by (rule compile_prog_calls_empty)
(simp_all add: flagship_prog_def main_body_def prog_main_name_def)
lemma flagship_cfg_prog_cfg: "flagship_cfg = prog_cfg flagship_prog"
by (simp add: flagship_cfg_def flagship_pi_def prog_cfg_def)
subsection ‹Equation generation and the executable solve›
text ‹
The solver --- pointwise interval warrowing at the loop head for termination ---
∗‹computes› a solution. Termination is a code-generated ▩‹by eval› fact;
the solution is not written by hand.
›
definition flagship_eqs ::
"pp × unit
⇒ (pp × unit, (unit, unit) global_unknown,
(ivl default_st lifted, ivl default_st lifted) dg_state) strategy_tree" where
"flagship_eqs = interval_rule.equations flagship_gs flagship_prog"
lemma flagship_terminates_c:
"TD_side_rule_Interp_solve_c Globals_Join flagship_eqs (cfg_exit flagship_cfg, ()) ≠ None"
by eval
lemma flagship_terminates: "interval_rule.terminates Globals_Join flagship_gs flagship_prog"
unfolding interval_rule.terminates_code
using TD_side_rule_Interp.solve_dom_of_solve_c[OF flagship_terminates_c]
by (simp add: flagship_eqs_def flagship_cfg_prog_cfg)
subsection ‹Inspecting the certified result›
text ‹The published state at a program point, at the one unit context.›
abbreviation flagship_at :: "pp ⇒ ivl abs_state" where
"flagship_at ≡ interval_rule.state_at Globals_Join flagship_gs flagship_prog ()"
lemma flagship_head_computed:
"flagship_at (Statement 1) (STR ''x'')
= Ivl (Fin 0) (Fin 20)"
by eval
lemma flagship_body_computed:
"flagship_at (Statement 2) (STR ''x'')
= Ivl (Fin 0) (Fin 19)"
by eval
lemma flagship_exit_computed:
"flagship_at (Statement 3) (STR ''x'')
= Ivl (Fin 20) (Fin 20)"
by eval
subsection ‹Source-level soundness›
text ‹
‹interval_rule.fun_route_source_sound› turns the single ▩‹by eval› solver
success ‹flagship_terminates_c› into a source-level guarantee: every reachable VIMP
store is bounded by the interval state published at its matched program point,
under the one context ‹()› the unit route names.
›
lemma flagship_wf:
"wf_compile_input flagship_gs flagship_pi (prog_procs flagship_prog)"
unfolding wf_compile_input_def
by (auto simp: wf_compile_input_simps flagship_pi_def flagship_prog_def split: if_splits)
theorem flagship_source_run_sound:
assumes run:
"flagship_gs, flagship_pi ⊢ (prog_main flagship_prog, s, []) →⇩p⇧* (residual, t, frs)"
and init: "s ∈ cinit_stores flagship_gs"
shows "∃v stk. flagship_pi, flagship_cfg, prog_main_name ⊢ (residual, t, frs) ≈ (v, t, stk)
∧ t ∈ γ (flagship_at v)"
proof -
have run':
"flagship_gs, prog_table flagship_prog ⊢ (main_body (prog_table flagship_prog), s, []) →⇩p⇧* (residual, t, frs)"
using run by (simp add: flagship_pi_def)
have wf: "wf_compile_input flagship_gs (prog_table flagship_prog) (prog_procs flagship_prog)"
using flagship_wf by (simp add: flagship_pi_def)
have unit_route: "⋀u ctx d ca s. route_unit u ctx d ca = enterc_unit u ctx s" by simp
show ?thesis
using interval_rule.fun_route_source_sound[OF unit_route wf flagship_terminates init run']
by (simp add: flagship_cfg_prog_cfg flagship_pi_def)
qed
text ‹
❙‹The bound is proper.› The published loop-head state constrains ‹x› to exactly
‹[0,20]› and rejects, e.g., a store with ‹x = 100›. The guarantee therefore says
something --- it is not the trivial ‹γ ⊤ = UNIV›.
›
theorem flagship_head_bound_proper:
"(λ_. 100) ∉ γ (flagship_at (Statement 1))"
proof
assume "(λ_. 100) ∈ γ (flagship_at (Statement 1))"
then have "(100::int) ∈ γ (flagship_at (Statement 1)
(STR ''x''))"
by (simp add: gamma_state_def)
then show False using flagship_head_computed by simp
qed
end