Theory Example_Non_Vacuity
theory Example_Non_Vacuity
imports Example_End_To_End_Certificate
begin
section ‹The headline theorems are not vacuous›
text ‹
A theorem whose premises no configuration meets is true and says nothing. This
theory shows, for each endpoint of \<^theory>‹Voblint_CLI.Analysis_Certified›, that its
premises hold together on one concrete program, and that the conclusion is then
informative: the verdict it constrains is \<^const>‹Check_Proved› or \<^const>‹Dead›, not
\<^const>‹Check_Unknown›. It then shows five conditions to be load-bearing: the
definite verdicts in \<^const>‹verdict_stores›, the transfer obligation of the
congruence remainder, the context correlation of RETURN and the TOTAL obligation in
\<^const>‹activation_coverage›, and the pairing in \<^const>‹entry_pairs_cover›. Dropping
or weakening each admits an answer that misses a concrete exe by (elim IfSE) (blast intro: pstep.IfTrue pstep.IfFalse)+cution.
Non-vacuity is a property of the premises. It says nothing about whether
\<^const>‹pstep› models the intended language.
›
subsection ‹The two-call program›
text ‹
‹bump› is called with ‹5› and with ‹4›. Entry-state contexts keep the two
activations apart, so both checks are proved; without contexts the entry of
‹bump› joins ‹[4, 5]› and neither is.
›
definition nv_prog :: imp_prog where
"nv_prog = program {
fun bump(n) { return n + 1; }
fun main() {
a = bump(5);
b = bump(4);
__voblint_check(a == 6);
__voblint_check(b == 5);
}
}"
abbreviation nv_config :: analysis_config where
"nv_config ≡ Analysis_Config [Interval_Analysis] Globals_Warrow Ctx_EntryState
Program_Globals_Flow_Sensitive"
lemma nv_report:
"(case run_voblint nv_config nv_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved), (Statement 5, Decided Check_Proved)]
| _ ⇒ False)"
by eval
lemma nv_analysed:
obtains res where
"run_voblint nv_config nv_prog = Analysed res"
"map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved), (Statement 5, Decided Check_Proved)]"
using nv_report
by (cases "run_voblint nv_config nv_prog") auto
subsection ‹The premises, discharged›
text ‹
Each premise of the source-level endpoints, proved for ‹nv_prog›: the zero store is
initial, there are no globals, and the source run reaches the first check
(‹nv_to_check›).
›
lemma nv_init: "(λ_. 0) ∈ cinit_stores (declared_global nv_prog)"
by (simp add: cinit_stores_def)
lemma nv_no_globals: "declared_global nv_prog = (λ_. False)"
by (simp add: nv_prog_def fun_eq_iff)
lemma nv_table:
"prog_table nv_prog (STR ''bump'')
= Some ⦇formals = [STR ''n''],
body = VIMP_Proc.gcom.Return () (Some (Plus (V (STR ''n'')) (N 1)))⦈"
by (simp add: nv_prog_def prog_main_name_def)
lemma nv_main:
"main_body (prog_table nv_prog)
= VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 5])
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 4]))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6))))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''b'')) (N 5)))"
by (simp add: nv_prog_def main_body_def prog_main_name_def)
lemma nv_call:
"pcompletes (declared_global nv_prog) (prog_table nv_prog)
(VIMP_Proc.gcom.Call () (Some x) (STR ''bump'') [N k]) s (s(x := k + 1))"
using pcompletes_Call_return
[where Π = "prog_table nv_prog" and p = "STR ''bump''"
and decl = "⦇formals = [STR ''n''],
body = VIMP_Proc.gcom.Return () (Some (Plus (V (STR ''n'')) (N 1)))⦈"
and e = "Plus (V (STR ''n'')) (N 1)" and actuals = "[N k]" and dst = "Some x"
and 𝒢 = "declared_global nv_prog" and s = s,
OF nv_table]
by (simp add: nv_no_globals enter_state_def combine_env_def)
abbreviation nv_final :: store where
"nv_final ≡ (λ_. 0)(STR ''a'' := 6, STR ''b'' := 5)"
lemma nv_calls:
"pcompletes (declared_global nv_prog) (prog_table nv_prog)
(VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 5])
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 4]))
(λ_. 0) nv_final"
proof -
have c1: "pcompletes (declared_global nv_prog) (prog_table nv_prog)
(VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 5]) (λ_. 0)
((λ_. 0)(STR ''a'' := 6))"
using nv_call [where x = "STR ''a''" and k = 5 and s = "λ_. 0"] by simp
have c2: "pcompletes (declared_global nv_prog) (prog_table nv_prog)
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 4])
((λ_. 0)(STR ''a'' := 6)) nv_final"
using nv_call [where x = "STR ''b''" and k = 4 and s = "(λ_. 0)(STR ''a'' := 6)"]
by simp
show ?thesis by (rule pcompletes_Seq [OF c1 c2])
qed
text ‹The source run, stopped with the first check about to execute.›
lemma nv_to_check:
"declared_global nv_prog, prog_table nv_prog ⊢
(main_body (prog_table nv_prog), λ_. 0, []) →⇩p⇧*
(VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6)))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''b'')) (N 5))), nv_final, [])"
proof -
have "declared_global nv_prog, prog_table nv_prog ⊢
(VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Call () (Some (STR ''a'')) (STR ''bump'') [N 5])
(VIMP_Proc.gcom.Call () (Some (STR ''b'')) (STR ''bump'') [N 4]))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6))), λ_. 0, []) →⇩p⇧*
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6)), nv_final, [])"
using psteps_Seq2 [OF nv_calls] by (meson Seq1 star.step star.refl star_trans)
then show ?thesis unfolding nv_main by (rule psteps_Seq2)
qed
subsection ‹The endpoints, instantiated›
text ‹
With the premises discharged, ‹run_voblint_source_sound› and its siblings apply to
‹nv_prog› and to ‹nv_dead_prog›, and the verdicts they constrain are
‹Check_Proved› and ‹Dead›.
›
theorem nv_source_certified:
"∃res v.
run_voblint nv_config nv_prog
= Analysed res
∧ map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved),
(Statement 5, Decided Check_Proved)]
∧ nv_prog, (λ_. 0) ⊢
(VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6)))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''b'')) (N 5))),
nv_final, []) ⊳ v
∧ nv_final ∈ 𝒞⇘declared_global nv_prog,prog_cfg nv_prog,
cinit_stores (declared_global nv_prog)⇙ v
∧ nv_final ∈ ℛ⇘res⇙ v
∧ nv_final ∈ 𝒱⇘res⇙ v"
proof -
obtain res where ans: "run_voblint nv_config nv_prog
= Analysed res"
and checks: "map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved), (Statement 5, Decided Check_Proved)]"
by (rule nv_analysed)
from run_voblint_source_sound [OF nv_init nv_to_check ans]
obtain v where "nv_prog, (λ_. 0) ⊢
(VIMP_Proc.gcom.Seq
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6)))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''b'')) (N 5))),
nv_final, []) ⊳ v"
and "nv_final ∈ 𝒞⇘declared_global nv_prog,prog_cfg nv_prog,
cinit_stores (declared_global nv_prog)⇙ v"
and "nv_final ∈ ℛ⇘res⇙ v" and "nv_final ∈ 𝒱⇘res⇙ v"
by blast
with ans checks show ?thesis by - (intro exI conjI; assumption)
qed
text ‹
Read at the check: the store the run holds there reaches a listed check for
‹a == 6›, that check says \<^const>‹Check_Proved›, and the condition holds.
›
theorem nv_check_proved_sound:
"∃res. run_voblint nv_config nv_prog = Analysed res
∧ (∃chk ∈ set (report_checks res). check_exp chk = Eq (V (STR ''a'')) (N 6)
∧ nv_final ∈ 𝒞⇘declared_global nv_prog,prog_cfg nv_prog,
cinit_stores (declared_global nv_prog)⇙ (check_point chk)
∧ check_verdict chk = Decided Check_Proved
∧ truthy (⟦Eq (V (STR ''a'')) (N 6)⟧⇩e nv_final))"
proof -
obtain res where ans: "run_voblint nv_config nv_prog
= Analysed res"
and checks: "map (λchk. (check_point chk, check_verdict chk)) (report_checks res)
= [(Statement 4, Decided Check_Proved), (Statement 5, Decided Check_Proved)]"
by (rule nv_analysed)
have nc: "next_check (VIMP_Proc.gcom.Seq (VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''a'')) (N 6)))
(VIMP_Proc.gcom.Check () (0, 0) (Eq (V (STR ''b'')) (N 5)))) = Some ((0, 0), Eq (V (STR ''a'')) (N 6))"
by simp
from run_voblint_check_sound [OF nv_init nv_to_check nc ans]
obtain chk
where listed: "chk ∈ set (report_checks res)"
and re: "check_exp chk = Eq (V (STR ''a'')) (N 6)"
and mem: "nv_final ∈ 𝒞⇘declared_global nv_prog,prog_cfg nv_prog,
cinit_stores (declared_global nv_prog)⇙ (check_point chk)"
and pr: "check_verdict chk = Decided Check_Proved
⟶ truthy (⟦Eq (V (STR ''a'')) (N 6)⟧⇩e nv_final)"
by auto
have "(check_point chk, check_verdict chk)
∈ set [(Statement 4, Decided Check_Proved), (Statement 5, Decided Check_Proved)]"
unfolding checks [symmetric] using listed by auto
then have "check_verdict chk = Decided Check_Proved" by auto
with ans listed re mem pr show ?thesis by blast
qed
definition nv_dead_prog :: imp_prog where
"nv_dead_prog = program {
fun main() {
x = 1;
__voblint_check(x == 0);
if (x < 0) { __voblint_check(x == 5); } else { x = 2; }
}
}"
abbreviation nv_dead_config :: analysis_config where
"nv_dead_config ≡ Analysis_Config [Interval_Analysis] Globals_Join Ctx_None
Program_Globals_Flow_Sensitive"
lemma nv_dead_report:
"(case run_voblint nv_dead_config nv_dead_prog of
Analysed res ⇒
map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 1, Eq (V (STR ''x'')) (N 0), Decided Check_Refuted),
(Statement 3, Eq (V (STR ''x'')) (N 5), Dead)]
| _ ⇒ False)"
by eval
lemma nv_dead_analysed:
obtains res where
"run_voblint nv_dead_config nv_dead_prog = Analysed res"
"map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 1, Eq (V (STR ''x'')) (N 0), Decided Check_Refuted),
(Statement 3, Eq (V (STR ''x'')) (N 5), Dead)]"
using nv_dead_report
by (cases "run_voblint nv_dead_config nv_dead_prog") auto
theorem nv_dead_unreached:
"𝒞⇘declared_global nv_dead_prog,prog_cfg nv_dead_prog,
cinit_stores (declared_global nv_dead_prog)⇙ (Statement 3) = {}"
proof -
obtain res where ans: "run_voblint nv_dead_config nv_dead_prog
= Analysed res"
and checks: "map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 1, Eq (V (STR ''x'')) (N 0), Decided Check_Refuted),
(Statement 3, Eq (V (STR ''x'')) (N 5), Dead)]"
by (rule nv_dead_analysed)
then obtain chk where "chk ∈ set (report_checks res)" "check_point chk = Statement 3"
"check_verdict chk = Dead"
by (cases "report_checks res" rule: remdups_adj.cases) auto
with run_voblint_dead_check_unreached [OF ans] show ?thesis by metis
qed
section ‹Load-bearing conditions›
text ‹
Each subsection below drops or weakens one condition and exhibits an answer that
meets everything else yet misses a concrete execution.
›
subsection ‹Soundness alone is cheap›
text ‹
\<^const>‹verdict_stores› constrains only definite verdicts, so a report that answers
\<^const>‹Check_Unknown› at every check admits every store at every node. The
endpoint is informative because the verdicts \<^const>‹run_voblint› actually returns
above are \<^const>‹Check_Proved› and \<^const>‹Dead›.
›
definition answer_all :: "contextual_verdict ⇒ analysis_report ⇒ analysis_report" where
"answer_all vd res =
res⦇report_checks := map (λchk. chk⦇check_verdict := vd⦈) (report_checks res)⦈"
lemma unknown_everywhere_sound:
"s ∈ 𝒱⇘answer_all (Decided Check_Unknown) res⇙ v"
by (auto simp: verdict_stores_eq answer_all_def)
text ‹
An answer of \<^const>‹Check_Proved› everywhere is not sound: the store after
‹x = 1› reaches the check ‹x == 0›, which it falsifies.
›
lemma nv_dead_reaches_first_check:
"(λ_. 0)(STR ''x'' := 1)
∈ 𝒞⇘declared_global nv_dead_prog,prog_cfg nv_dead_prog,
cinit_stores (declared_global nv_dead_prog)⇙ (Statement 1)"
proof -
have intra: "intra (prog_cfg nv_dead_prog) =
{(FunctionEntry (STR ''main''), EA_Body (STR ''main''), Statement 0),
(Statement 5, EA_Ret None (STR ''main''), FunctionResult (STR ''main'')),
(Statement 1, EA_Check (0, 0) (Eq (V (STR ''x'')) (N 0)), Statement 2),
(Statement 0, EA_Assign (STR ''x'') (N 1), Statement 1),
(Statement 3, EA_Check (0, 0) (Eq (V (STR ''x'')) (N 5)), Statement 5),
(Statement 2, EA_Assume (Less (V (STR ''x'')) (N 0)), Statement 3),
(Statement 2, EA_AssumeNot (Less (V (STR ''x'')) (N 0)), Statement 4),
(Statement 4, EA_Assign (STR ''x'') (N 2), Statement 5)}"
unfolding prog_cfg_def by eval
have entry: "cfg_entry (prog_cfg nv_dead_prog) = FunctionEntry (STR ''main'')"
by (simp only: prog_cfg_def cfg_entry_compile_prog prog_main_name_def)
have e0: "(λ_. 0) ∈ 𝒞⇘declared_global nv_dead_prog,prog_cfg nv_dead_prog,
cinit_stores (declared_global nv_dead_prog)⇙ (FunctionEntry (STR ''main''))"
using node_collect_init [of "λ_. 0" "cinit_stores (declared_global nv_dead_prog)"
"declared_global nv_dead_prog" "prog_cfg nv_dead_prog"]
by (simp add: entry cinit_stores_def)
have s0: "(λ_. 0) ∈ 𝒞⇘declared_global nv_dead_prog,prog_cfg nv_dead_prog,
cinit_stores (declared_global nv_dead_prog)⇙ (Statement 0)"
by (rule node_collect_intra_step [OF e0, where a = "EA_Body (STR ''main'')"])
(auto simp: intra)
show ?thesis
by (rule node_collect_intra_step [OF s0, where a = "EA_Assign (STR ''x'') (N 1)"])
(auto simp: intra)
qed
theorem proved_everywhere_unsound:
assumes "run_voblint nv_dead_config nv_dead_prog = Analysed res"
shows "(λ_. 0)(STR ''x'' := 1)
∉ 𝒱⇘answer_all (Decided Check_Proved) res⇙ (Statement 1)"
proof -
from nv_dead_report assms
have "map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (report_checks res)
= [(Statement 1, Eq (V (STR ''x'')) (N 0), Decided Check_Refuted),
(Statement 3, Eq (V (STR ''x'')) (N 5), Dead)]"
by simp
then obtain chk where "chk ∈ set (report_checks res)" "check_point chk = Statement 1"
"check_exp chk = Eq (V (STR ''x'')) (N 0)"
by (cases "report_checks res" rule: remdups_adj.cases) auto
then show ?thesis
by (auto simp: verdict_stores_eq answer_all_def
intro!: bexI[of _ "chk⦇check_verdict := Decided Check_Proved⦈"])
qed
subsection ‹The pre-fix Goblint congruence remainder›
text ‹
Before Goblint pull request 1161, the remainder of the odd class ‹1 + 2ℤ› by the
constant ‹2› was the constant ‹1›. Any abstract remainder that answers so violates
the obligation ‹congruence_mod_sound› discharges for the shipped one: ‹-5› is
odd, and its truncating remainder by ‹2› is ‹-1›.
›
theorem prefix_congruence_mod_unsound:
assumes const: "f (mk_congruence 1 2) (mk_congruence 2 0) = mk_congruence 1 0"
shows "¬ (∀a b i j. i ∈ gamma_congruence a ⟶ j ∈ gamma_congruence b
⟶ c_mod i j ∈ gamma_congruence (f a b))"
proof
assume sound: "∀a b i j. i ∈ gamma_congruence a ⟶ j ∈ gamma_congruence b
⟶ c_mod i j ∈ gamma_congruence (f a b)"
have "c_mod (-5) 2 ∈ gamma_congruence (mk_congruence 1 0)"
using sound [rule_format, of "-5" "mk_congruence 1 2" 2 "mk_congruence 2 0"]
by (simp add: const gamma_congruence_def)
then show False by (simp add: gamma_congruence_def c_mod_def c_div_def)
qed
section ‹The paired-coverage, RETURN and TOTAL counterexamples›
text ‹
Three weakenings of ‹activation_coverage› fail: RETURN read at the caller's
context, TOTAL dropped, and entry coverage without pairing. ‹ret_prog› calls ‹f›
with ‹1› and then ‹5›.
›
definition ret_prog :: imp_prog where
"ret_prog = program {
fun f(n) { return n; }
fun main() { a = f(1); b = f(5); }
}"
lemma ret_intra:
"intra (prog_cfg ret_prog) =
{(FunctionEntry (STR ''f''), EA_Body (STR ''f''), Statement 0),
(Statement 0, EA_Ret (Some (V (STR ''n''))) (STR ''f''), FunctionResult (STR ''f'')),
(Statement 1, EA_Ret None (STR ''f''), FunctionResult (STR ''f'')),
(FunctionEntry (STR ''main''), EA_Body (STR ''main''), Statement 2),
(Statement 4, EA_Ret None (STR ''main''), FunctionResult (STR ''main''))}"
unfolding prog_cfg_def by eval
lemma ret_calls:
"calls (prog_cfg ret_prog) =
{(Statement 2, CallEdge (Some (STR ''a'')) [STR ''n''] [N 1], FunctionEntry (STR ''f''),
Statement 3),
(Statement 3, CallEdge (Some (STR ''b'')) [STR ''n''] [N 5], FunctionEntry (STR ''f''),
Statement 4)}"
unfolding prog_cfg_def by eval
lemma ret_entry: "cfg_entry (prog_cfg ret_prog) = FunctionEntry (STR ''main'')"
by (simp only: prog_cfg_def cfg_entry_compile_prog prog_main_name_def)
lemma ret_no_globals: "declared_global ret_prog = (λ_. False)"
by (simp add: ret_prog_def fun_eq_iff)
lemma ret_enter:
"call_enter (declared_global ret_prog) (CallEdge dst [STR ''n''] [e]) s
= (λ_. 0)(STR ''n'' := ⟦e⟧⇩e s)"
by (simp add: ret_no_globals call_enter_CallEdge enter_binding_def enter_frame_def fun_eq_iff)
text ‹The policy of the illustration: the callee context is the entry value of ‹n›.›
definition ret_R :: "int context_policy" where
"ret_R = context_policy_of_fun (λ_ _ es. es (STR ''n''))"
text ‹
The claim: ‹main› is covered in the initial context ‹0› up to its first call site
and nowhere after it; ‹f› is covered everywhere, but only in the contexts its
calls create.
›
definition ret_cover :: "cfg_node ⇒ int ⇒ store set" where
"ret_cover v ctx =
(if v ∈ {FunctionEntry (STR ''f''), Statement 0, FunctionResult (STR ''f'')}
then (if ctx = 0 then {} else UNIV)
else if ctx = 0 ∧ v ∈ {FunctionEntry (STR ''main''), Statement 2} then UNIV else {})"
lemma ret_weak_obligations:
shows "∀s. s ∈ cinit_stores (declared_global ret_prog)
⟶ s ∈ ret_cover (cfg_entry (prog_cfg ret_prog)) 0"
and "∀u a v c s s'. (u, a, v) ∈ intra (prog_cfg ret_prog) ⟶ s ∈ ret_cover u c
⟶ s' ∈ edge_step a s ⟶ s' ∈ ret_cover v c"
and "∀u dst pars args p cont c c' s.
(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (prog_cfg ret_prog)
⟶ s ∈ ret_cover u c
⟶ c' ∈ ret_R u c (call_info_of (CallEdge dst pars args) p) s
(call_enter (declared_global ret_prog) (CallEdge dst pars args) s)
⟶ call_enter (declared_global ret_prog) (CallEdge dst pars args) s
∈ ret_cover (FunctionEntry p) c'"
and "∀cl dst pars args p cont c1 s t.
(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (prog_cfg ret_prog)
⟶ s ∈ ret_cover cl c1 ⟶ t ∈ ret_cover (FunctionResult p) c1
⟶ combine_collect (declared_global ret_prog) dst s t ∈ ret_cover cont c1"
and "call_context_total_on ret_cover ret_R (declared_global ret_prog) (prog_cfg ret_prog)"
by (auto simp: ret_entry ret_intra ret_calls ret_cover_def ret_R_def ret_enter
call_context_total_on_def)
lemma ret_not_coverage:
"¬ activation_coverage (prog_cfg ret_prog) (cinit_stores (declared_global ret_prog)) ret_cover
ret_R 0 (declared_global ret_prog)"
proof
assume "activation_coverage (prog_cfg ret_prog) (cinit_stores (declared_global ret_prog)) ret_cover
ret_R 0 (declared_global ret_prog)"
then interpret C: activation_coverage "prog_cfg ret_prog"
"cinit_stores (declared_global ret_prog)"
ret_cover ret_R 0 "declared_global ret_prog" .
have e: "(Statement 2, CallEdge (Some (STR ''a'')) [STR ''n''] [N 1], FunctionEntry (STR ''f''),
Statement 3) ∈ calls (prog_cfg ret_prog)"
by (simp add: ret_calls)
have adm: "admits_call_context (declared_global ret_prog) (prog_cfg ret_prog) ret_R
(Statement 2) 0 (STR ''f'') (λ_. 0)
(call_enter (declared_global ret_prog)
(CallEdge (Some (STR ''a'')) [STR ''n''] [N 1]) (λ_. 0)) 1"
unfolding admits_call_context_def
by (rule exI [of _ "Some (STR ''a'')"], rule exI [of _ "[STR ''n'']"],
rule exI [of _ "[N 1]"], rule exI [of _ "Statement 3"])
(simp add: e ret_R_def ret_enter)
have "combine_collect (declared_global ret_prog) (Some (STR ''a'')) (λ_. 0) (λ_. 0)
∈ ret_cover (Statement 3) 0"
by (rule C.RETURN [OF e _ adm]) (simp_all add: ret_cover_def)
then show False by (simp add: ret_cover_def)
qed
lemma ret_f_body:
"intra_path (prog_cfg ret_prog)
(FunctionEntry (STR ''f''), (λ_. 0)(STR ''n'' := k))
(FunctionResult (STR ''f''), ((λ_. 0)(STR ''n'' := k))(ret_var := k))"
proof (rule star_trans)
show "intra_path (prog_cfg ret_prog)
(FunctionEntry (STR ''f''), (λ_. 0)(STR ''n'' := k))
(Statement 0, (λ_. 0)(STR ''n'' := k))"
by (rule intra_path_single [where a = "EA_Body (STR ''f'')"]) (auto simp: ret_intra)
next
show "intra_path (prog_cfg ret_prog)
(Statement 0, (λ_. 0)(STR ''n'' := k))
(FunctionResult (STR ''f''), ((λ_. 0)(STR ''n'' := k))(ret_var := k))"
by (rule intra_path_single [where a = "EA_Ret (Some (V (STR ''n''))) (STR ''f'')"])
(auto simp: ret_intra)
qed
lemma ret_reaches_second_call:
"(λ_. 0)(STR ''a'' := 1)
∈ 𝒞⇘declared_global ret_prog,prog_cfg ret_prog,
cinit_stores (declared_global ret_prog)⇙ (Statement 3)"
proof -
have e0: "(λ_. 0) ∈ 𝒞⇘declared_global ret_prog,prog_cfg ret_prog,
cinit_stores (declared_global ret_prog)⇙ (FunctionEntry (STR ''main''))"
using node_collect_init [of "λ_. 0" "cinit_stores (declared_global ret_prog)"
"declared_global ret_prog" "prog_cfg ret_prog"]
by (simp add: ret_entry cinit_stores_def)
have s2: "(λ_. 0) ∈ 𝒞⇘declared_global ret_prog,prog_cfg ret_prog,
cinit_stores (declared_global ret_prog)⇙ (Statement 2)"
by (rule node_collect_intra_step [OF e0, where a = "EA_Body (STR ''main'')"])
(auto simp: ret_intra)
have ce: "(Statement 2, CallEdge (Some (STR ''a'')) [STR ''n''] [N 1],
FunctionEntry (STR ''f''), Statement 3) ∈ calls (prog_cfg ret_prog)"
by (simp add: ret_calls)
have bd: "intra_path (prog_cfg ret_prog)
(FunctionEntry (STR ''f''),
call_enter (declared_global ret_prog)
(CallEdge (Some (STR ''a'')) [STR ''n''] [N 1]) (λ_. 0))
(FunctionResult (STR ''f''), ((λ_. 0)(STR ''n'' := 1))(ret_var := 1))"
using ret_f_body [where k = 1] by (simp add: ret_enter)
show ?thesis
using node_collect_call_return_step [OF s2 ce bd]
by (simp add: ret_no_globals combine_collect_def combine_env_def ret_var_def fun_eq_iff)
qed
text ‹
Reading the callee at the caller's own context: the claim meets INIT, INTRA,
CALL, the weakened RETURN and TOTAL, yet it covers no store at the second call
site in any context, although a concrete trace reaches it. So ‹b = f(5)› is
declared unreachable.
›
theorem return_at_caller_context_unsound:
"(λ_. 0)(STR ''a'' := 1)
∈ 𝒞⇘declared_global ret_prog,prog_cfg ret_prog,
cinit_stores (declared_global ret_prog)⇙ (Statement 3)
∧ (⋃c. ret_cover (Statement 3) c) = {}"
using ret_reaches_second_call by (simp add: ret_cover_def)
subsection ‹TOTAL is load-bearing›
text ‹
A resumed caller carries its own context whatever its callee carries, so the
continuation of a call is collected in the caller's bucket even when the relation
admits no callee context. Such a relation makes CALL and RETURN vacuous.
›
lemma resume_keeps_context:
assumes s: "s ∈ 𝒜⇘𝒢,adm,c0,g,S⇙ u ctx"
and ce: "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls g"
and body: "intra_path g (FunctionEntry q, call_enter 𝒢 (CallEdge dst pars args) s)
(FunctionResult q, t)"
shows "combine_collect 𝒢 dst s t ∈ 𝒜⇘𝒢,adm,c0,g,S⇙ cont ctx"
proof -
from s obtain caller where cv: "caller ∈ 𝒯⇘𝒢,g,S⇙"
and cn: "sink_node caller = u" and ck: "activation_context_rel 𝒢 adm c0 g caller ctx"
and cs: "sink_store caller = s"
by (rule activation_collect_E)
let ?entered = "Call caller [(FunctionEntry q, call_enter 𝒢 (CallEdge dst pars args) s)]"
have ev: "?entered ∈ 𝒯⇘𝒢,g,S⇙"
using valid_activation_trace.call [OF cv, where dst = dst and pars = pars and args = args
and p = q and cont = cont]
ce cn cs by simp
obtain callee where dv: "callee ∈ 𝒯⇘𝒢,g,S⇙"
and dn: "sink_node callee = FunctionResult q" and ds: "sink_store callee = t"
and dc: "caller_of callee = caller_of ?entered"
by (rule valid_activation_trace_intra_path_extend [OF _ ev]) (use body in simp_all)
let ?r = "Resume caller callee
(path_of caller @ [(cont, combine_collect 𝒢 dst (sink_store caller) (sink_store callee))])"
have rv: "?r ∈ 𝒯⇘𝒢,g,S⇙"
by (rule valid_activation_trace.ret [OF dv _ dn]) (use dc ce cn in simp_all)
have "sink_store ?r ∈ 𝒜⇘𝒢,adm,c0,g,S⇙ (sink_node ?r) ctx"
by (rule activation_collect_I [OF rv refl]) (use ck in simp)
then show ?thesis using cs ds by (simp add: sink_node_def sink_store_def)
qed
text ‹The relation that admits no context, and the claim that covers ‹main› up to its first
call site in the initial context and nothing else.›
definition tot_R :: "int context_policy" where
"tot_R u ctx ci s es = {}"
definition tot_cover :: "cfg_node ⇒ int ⇒ store set" where
"tot_cover v ctx =
(if ctx = 0 ∧ v ∈ {FunctionEntry (STR ''main''), Statement 2} then UNIV else {})"
lemma tot_weak_obligations:
shows "∀s. s ∈ cinit_stores (declared_global ret_prog)
⟶ s ∈ tot_cover (cfg_entry (prog_cfg ret_prog)) 0"
and "∀u a v c s s'. (u, a, v) ∈ intra (prog_cfg ret_prog) ⟶ s ∈ tot_cover u c
⟶ s' ∈ edge_step a s ⟶ s' ∈ tot_cover v c"
and "∀u dst pars args p cont c c' s.
(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (prog_cfg ret_prog)
⟶ s ∈ tot_cover u c
⟶ c' ∈ tot_R u c (call_info_of (CallEdge dst pars args) p) s
(call_enter (declared_global ret_prog) (CallEdge dst pars args) s)
⟶ call_enter (declared_global ret_prog) (CallEdge dst pars args) s
∈ tot_cover (FunctionEntry p) c'"
and "∀cl dst pars args p cont c1 c' p' s t es.
(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (prog_cfg ret_prog)
⟶ s ∈ tot_cover cl c1
⟶ admits_call_context (declared_global ret_prog) (prog_cfg ret_prog) tot_R
cl c1 p' s es c'
⟶ t ∈ tot_cover (FunctionResult p) c'
⟶ combine_collect (declared_global ret_prog) dst s t ∈ tot_cover cont c1"
and "¬ call_context_total_on tot_cover tot_R (declared_global ret_prog) (prog_cfg ret_prog)"
by (auto simp: ret_entry ret_intra ret_calls tot_cover_def tot_R_def admits_call_context_def
call_context_total_on_def)
text ‹
The claim meets INIT, INTRA, CALL and RETURN and fails only TOTAL. The run resumes at
the second call site in the initial context, where the claim is empty, so the
per-context conclusion of ‹activation_collect_sound› fails.
›
theorem total_dropped_unsound:
"(λ_. 0)(STR ''a'' := 1)
∈ 𝒜⇘declared_global ret_prog,tot_R,0,prog_cfg ret_prog,
cinit_stores (declared_global ret_prog)⇙ (Statement 3) 0
∧ (λ_. 0)(STR ''a'' := 1) ∉ tot_cover (Statement 3) 0"
proof
let ?S = "cinit_stores (declared_global ret_prog)"
let ?t0 = "Root [(FunctionEntry (STR ''main''), λ_. 0)]"
have v0: "?t0 ∈ 𝒯⇘declared_global ret_prog,prog_cfg ret_prog,?S⇙"
using valid_activation_trace.root
[where s = "λ_. 0" and S = ?S and 𝒢 = "declared_global ret_prog"
and g = "prog_cfg ret_prog"]
by (simp add: ret_entry cinit_stores_def)
have v1: "Root [(FunctionEntry (STR ''main''), λ_. 0), (Statement 2, λ_. 0)]
∈ 𝒯⇘declared_global ret_prog,prog_cfg ret_prog,?S⇙"
using valid_activation_trace.intra
[OF v0, where a = "EA_Body (STR ''main'')" and v = "Statement 2"
and s' = "λ_. 0"]
by (simp add: ret_intra sink_node_def sink_store_def)
have s2: "(λ_. 0) ∈ 𝒜⇘declared_global ret_prog,tot_R,0,prog_cfg ret_prog,?S⇙ (Statement 2) 0"
proof -
have "sink_store (Root [(FunctionEntry (STR ''main''), λ_. 0), (Statement 2, λ_. 0)])
∈ 𝒜⇘declared_global ret_prog,tot_R,0,prog_cfg ret_prog,?S⇙
(sink_node (Root [(FunctionEntry (STR ''main''), λ_. 0), (Statement 2, λ_. 0)])) 0"
by (rule activation_collect_I [OF v1 refl]) simp
then show ?thesis by (simp add: sink_node_def sink_store_def)
qed
have ce: "(Statement 2, CallEdge (Some (STR ''a'')) [STR ''n''] [N 1],
FunctionEntry (STR ''f''), Statement 3) ∈ calls (prog_cfg ret_prog)"
by (simp add: ret_calls)
have bd: "intra_path (prog_cfg ret_prog)
(FunctionEntry (STR ''f''),
call_enter (declared_global ret_prog)
(CallEdge (Some (STR ''a'')) [STR ''n''] [N 1]) (λ_. 0))
(FunctionResult (STR ''f''), ((λ_. 0)(STR ''n'' := 1))(ret_var := 1))"
using ret_f_body [where k = 1] by (simp add: ret_enter)
show "(λ_. 0)(STR ''a'' := 1)
∈ 𝒜⇘declared_global ret_prog,tot_R,0,prog_cfg ret_prog,?S⇙ (Statement 3) 0"
using resume_keeps_context [OF s2 ce bd]
by (simp add: ret_no_globals combine_collect_def combine_env_def ret_var_def fun_eq_iff)
show "(λ_. 0)(STR ''a'' := 1) ∉ tot_cover (Statement 3) 0"
by (simp add: tot_cover_def)
qed
subsection ‹Entry coverage must be paired›
text ‹
‹y = p(x)› with ‹fun p(a) { return a; }› and ‹x = 1›. Abstract values are
represented by their concretizations, so \<^const>‹entry_pairs_cover› is taken at
\<^const>‹id›. The answer ‹[(x > 0, a < 0), (⊥, a > 0)]› covers the caller store
with its first pair and the entered store with its second. Each pair's callee
result, ‹a› published as the return value, is combined with that pair's own
continuation; the union excludes the run's ‹y = 1›.
›
definition unpaired_answer :: "(store set × store set) list" where
"unpaired_answer =
[({t. 0 < t (STR ''x'')}, {t. t (STR ''a'') < 0}), ({}, {t. 0 < t (STR ''a'')})]"
definition pairwise_contribution :: "(store set × store set) list ⇒ store set" where
"pairwise_contribution P =
(⋃(q, e) ∈ set P.
{combine_collect (λ_. False) (Some (STR ''y'')) s0 (t(ret_var := t (STR ''a'')))
| s0 t. s0 ∈ q ∧ t ∈ e})"
theorem unpaired_entry_cover_unsound:
defines "s ≡ (λ_. 0)(STR ''x'' := 1) :: store"
and "s' ≡ (λ_. 0)(STR ''a'' := 1) :: store"
shows "s' = call_enter (λ_. False) (CallEdge (Some (STR ''y'')) [STR ''a''] [V (STR ''x'')]) s"
and "(∃(q, e) ∈ set unpaired_answer. s ∈ q)"
and "(∃(q, e) ∈ set unpaired_answer. s' ∈ e)"
and "¬ entry_pairs_cover id s s' unpaired_answer"
and "∀u ∈ pairwise_contribution unpaired_answer. u (STR ''y'') < 0"
and "combine_collect (λ_. False) (Some (STR ''y'')) s (s'(ret_var := s' (STR ''a'')))
(STR ''y'') = 1"
by (auto simp: s_def s'_def unpaired_answer_def pairwise_contribution_def
entry_pairs_cover_def call_enter_CallEdge enter_binding_def enter_frame_def
combine_collect_def combine_env_def ret_var_def fun_eq_iff)
end