Theory Example_Analysis_Dispatch_Regression
theory Example_Analysis_Dispatch_Regression
imports
"Voblint_VIMP.VIMP_Notation" "Voblint_CLI.Analysis_Render"
begin
text ‹
\<^const>‹run_voblint› on one small program, at every axis a caller chooses: the
domain, the rule that merges contributions to side-effected globals, and the context
policy. The CLI regression groups pin verdicts across globals, calls, repeated call
sites and every selectable domain by running the generated analyzer; what stays here
pins the operation Isabelle exports, by evaluation. The certified reading of such an
answer is ‹Example_End_To_End_Certificate›.
›
subsection ‹One program, two verdicts›
text ‹
‹y := 1› then check ‹0 < y› (holds), then ‹y := 0 - 1› and check ‹0 < y›
again (fails): Interval's numeric bounds settle both checks precisely.
›
definition dispatch_demo_prog :: imp_prog where
"dispatch_demo_prog =
program {
fun main() {
y = 1;
__voblint_check(0 < y);
y = 0 - 1;
__voblint_check(0 < y);
}
}"
definition dispatch_demo_checks where
"dispatch_demo_checks D rule ctx =
(case run_voblint (Analysis_Config [D] rule ctx Program_Globals_Flow_Sensitive) dispatch_demo_prog of
Analysed res ⇒ Some (map (λchk. (check_point chk, check_exp chk, check_verdict chk))
(report_checks res))
| Malformed_Program ⇒ None)"
lemma dispatch_demo_interval_precise:
"dispatch_demo_checks Interval_Analysis Globals_Warrow Ctx_None =
Some [(Statement 1, Less (exp.N 0) (V (STR ''y'')), Lifted Check_Proved),
(Statement 3, Less (exp.N 0) (V (STR ''y'')), Lifted Check_Refuted)]"
by eval
text ‹
The rule is an argument of the solve, not of the report: a program with no side-effected
global reaches the same verdicts under every rule, at every context policy, including a
call string of length zero.
›
lemma dispatch_demo_rule_invariant:
"∀rule ∈ {Globals_Join, Globals_Per_Origin, Globals_Warrow, Globals_Warrow_Per_Origin,
Globals_Bounded_Narrowing 0, Globals_Bounded_Narrowing 5}.
∀ctx ∈ {Ctx_None, Ctx_EntryState, Ctx_CallString 0, Ctx_CallString 1}.
dispatch_demo_checks Interval_Analysis rule ctx =
dispatch_demo_checks Interval_Analysis Globals_Warrow Ctx_None"
by eval
text ‹
The call-string plan reads the table its rule names, not whichever one its domain
publishes first. Int is where that is observable: the call-string registration
‹mcp_cs_rule› of the active analyses solves an always-join table and a warrowing
one, and the two rows below are the two solves.
›
lemma dispatch_demo_call_string_reads_the_named_rule:
"(case run_voblint (Analysis_Config [Int_Analysis Refine_Fixpoint] Globals_Warrow
(Ctx_CallString 1) Program_Globals_Flow_Sensitive) dispatch_demo_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= mcp_cs_rule.verdict_report [Int_Analysis Refine_Fixpoint] 1 Globals_Warrow
(declared_global dispatch_demo_prog) dispatch_demo_prog
| _ ⇒ False)"
"(case run_voblint (Analysis_Config [Int_Analysis Refine_Fixpoint] Globals_Join
(Ctx_CallString 1) Program_Globals_Flow_Sensitive) dispatch_demo_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= mcp_cs_rule.verdict_report [Int_Analysis Refine_Fixpoint] 1 Globals_Join
(declared_global dispatch_demo_prog) dispatch_demo_prog
| _ ⇒ False)"
by eval+
text ‹
The public entry point at an entry-state configuration. Its check column and its
states come off one solved table.
›
lemma dispatch_demo_run_voblint_entry_state:
"(case run_voblint (Analysis_Config [Interval_Analysis] Globals_Warrow Ctx_EntryState
Program_Globals_Flow_Sensitive) dispatch_demo_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_verdict chk)) (report_checks res) =
[(Statement 1, Lifted Check_Proved), (Statement 3, Lifted Check_Refuted)]
∧ report_contexts res = [Report_Entry mcp_root_ctx]
∧ report_states res ≠ []
| _ ⇒ False)"
by eval
lemma dispatch_demo_run_voblint_flat:
"(case run_voblint (Analysis_Config [Interval_Analysis] Globals_Warrow Ctx_None
Program_Globals_Flow_Sensitive) dispatch_demo_prog of
Analysed res ⇒ report_contexts res = [Report_Unit]
| _ ⇒ False)"
by eval
subsection ‹What one statement makes of its state›
text ‹
‹i := 0› and ‹i := i + 1› both flow into the loop head, which stores only the
join of the two, ‹[0, 5]›. Each statement's own step survives beside its source
state: the body's assignment makes ‹[1, 5]› of the ‹[0, 4]› the guard lets
through, and the assignment before the loop makes ‹[0, 0]›.
›
definition step_demo_prog :: imp_prog where
"step_demo_prog =
program {
fun main() {
i = 0;
while (i < 5) {
i = i + 1;
}
}
}"
text ‹One variable's value at a point and after each of the point's steps, under Interval.›
fun field_value :: "vname ⇒ 'v field_state ⇒ 'v option" where
"field_value x (Field_Store bs) = map_of bs x"
| "field_value x (Field_Whole _) = None"
definition interval_value :: "vname ⇒ 'v analysis_view ⇒ 'v option" where
"interval_value x view = Option.bind (map_of view Interval_Analysis) (field_value x)"
definition step_view :: "imp_prog ⇒ vname ⇒ pp ⇒ (abstract_value option lifted
× (pp × abstract_value option lifted) list) list" where
"step_view p x v =
(case run_voblint (Analysis_Config [Interval_Analysis] Globals_Warrow Ctx_None
Program_Globals_Flow_Sensitive) p of
Analysed res ⇒
map (λst. (map_lift (interval_value x) (state_value st),
map (λ(w, s). (w, map_lift (interval_value x) s)) (state_steps st)))
(filter (λst. state_point st = v) (res_states (render_report id res)))
| _ ⇒ [])"
abbreviation step_demo_i :: "pp ⇒ (abstract_value option lifted
× (pp × abstract_value option lifted) list) list" where
"step_demo_i ≡ step_view step_demo_prog (STR ''i'')"
lemma step_demo_body_step:
"step_demo_i (Statement 2) =
[(Lifted (Some (IntervalValue (Ivl (Fin 0) (Fin 4)))),
[(Statement 1, Lifted (Some (IntervalValue (Ivl (Fin 1) (Fin 5)))))])]"
by eval
lemma step_demo_head_stores_join:
"step_demo_i (Statement 1) =
[(Lifted (Some (IntervalValue (Ivl (Fin 0) (Fin 5)))),
[(Statement 2, Lifted (Some (IntervalValue (Ivl (Fin 0) (Fin 4))))),
(Statement 3, Lifted (Some (IntervalValue (Ivl (Fin 5) (Fin 5)))))])]"
by eval
lemma step_demo_before_loop_step:
"step_demo_i (Statement 0) =
[(Lifted (Some (IntervalValue (Ivl MinInf PlusInf))),
[(Statement 1, Lifted (Some (IntervalValue (Ivl (Fin 0) (Fin 0)))))])]"
by eval
text ‹
A guard no store satisfies has no successor. Its step reads back as \<^const>‹Bot›,
as the solve's reachability lift makes it, not as a store of empty values, and the
dead branch then steps nowhere either.
›
definition dead_step_prog :: imp_prog where
"dead_step_prog =
program {
fun main() {
x = 5;
if (x < 0) {
x = 1;
}
}
}"
lemma dead_step_guard_is_bot:
"step_view dead_step_prog (STR ''x'') (Statement 1) =
[(Lifted (Some (IntervalValue (Ivl (Fin 5) (Fin 5)))),
[(Statement 2, Bot),
(Statement 4, Lifted (Some (IntervalValue (Ivl (Fin 5) (Fin 5)))))])]"
by eval
lemma dead_step_branch_steps_nowhere:
"step_view dead_step_prog (STR ''x'') (Statement 2) = [(Bot, [(Statement 4, Bot)])]"
by eval
subsection ‹One analysis asks another›
text ‹
Both guards hold only where ‹x = y›, so ‹z = 1› at the check. Interval alone
keeps ‹x› and ‹y› unbounded and assigns ‹z› the interval ‹[0, 1]›. The order
analysis alone records ‹x ≤ y› and ‹y ≤ x› but tracks no values, so it cannot
answer ‹z == 1›. Run together, Interval's assignment asks the combined state for
the value of ‹x == y›, the order analysis answers the exact integer ‹1›, and
Interval assigns ‹[1, 1]›.
›
definition coop_demo_prog :: imp_prog where
"coop_demo_prog =
program {
fun main() {
if (x <= y) {
if (y <= x) {
z = (x == y);
__voblint_check(z == 1);
}
}
}
}"
definition coop_demo_verdicts where
"coop_demo_verdicts as =
(case run_voblint (Analysis_Config as Globals_Warrow Ctx_None Program_Globals_Flow_Sensitive)
coop_demo_prog of
Analysed res ⇒ Some (map check_verdict (report_checks res))
| _ ⇒ None)"
lemma coop_demo_needs_both:
"coop_demo_verdicts [Interval_Analysis] = Some [Decided Check_Unknown]"
"coop_demo_verdicts [Order_Analysis] = Some [Decided Check_Unknown]"
"coop_demo_verdicts [Interval_Analysis, Order_Analysis] = Some [Decided Check_Proved]"
by eval+
subsection ‹A check's row carries its label›
text ‹
Two checks of ‹x == 1› with opposite verdicts: main's, where ‹x = 1›, and the
callee's, where ‹x = 2›. The compiler lays the callee out first, so the check column
lists the callee's check first. Each row keeps its own check's label, so a report that
looks rows up by label shows each verdict at its check whatever the order.
›
definition labelled_checks_prog :: imp_prog where
"labelled_checks_prog =
mk_program
[(STR ''f'',
⦇formals = [],
body = VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Assign () (STR ''x'') (exp.N 2))
(VIMP_Proc.gcom.Check () (6, 3) (exp.Eq (V (STR ''x'')) (exp.N 1)))⦈)]
(VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Assign () (STR ''x'') (exp.N 1))
(VIMP_Proc.gcom.Check () (2, 3) (exp.Eq (V (STR ''x'')) (exp.N 1))))
(VIMP_Proc.gcom.Call () None (STR ''f'') []))
[]"
lemma labelled_checks_rows:
"(case run_voblint (Analysis_Config [Interval_Analysis] Globals_Warrow Ctx_None
Program_Globals_Flow_Sensitive) labelled_checks_prog of
Analysed res ⇒
map (λchk. (check_label chk, check_verdict chk)) (report_checks res) =
[((6, 3), Lifted Check_Refuted), ((2, 3), Lifted Check_Proved)]
| _ ⇒ False)"
by eval
end