Theory Analysis_Report
theory Analysis_Report
imports Analysis_Run_Ctx_Sound Analysis_Render
begin
section ‹What a report claims›
text ‹
A report is read through three sets of stores at a point ‹v›. ‹𝒞 v› holds the
stores the program reaches at ‹v›. ‹ℛ⇘res⇙ v› holds the stores the report's states
at ‹v› describe, over all of its contexts. ‹𝒱⇘res⇙ v› holds the stores in which
every definite verdict the report gives at ‹v› is valid. The report is sound when
‹𝒞 v ⊆ ℛ⇘res⇙ v ⊆ 𝒱⇘res⇙ v›
and a point the report calls dead has ‹ℛ⇘res⇙ v = {}›, so no execution reaches it.
The first inclusion needs the run that built the report; the second and the dead
case follow from the report alone, once its verdicts agree with its states.
›
subsection ‹The stores a report describes›
definition report_gamma :: "analysis_report ⇒ mcp_val ⇒ store set" where
"report_gamma res = mcp_gamma_v (activation (config_analyses (report_config res)))"
definition report_classify :: "analysis_report ⇒ exp ⇒ mcp_val ⇒ check_result" where
"report_classify res = mcp_classify (activation (config_analyses (report_config res)))"
text ‹The states a report holds at a point, one per context it was solved at.›
definition report_states_at :: "analysis_report ⇒ pp ⇒ mcp_val lifted set" where
"report_states_at res v = state_value ` {st ∈ set (report_states res). state_point st = v}"
lemma finite_report_states_at [simp]: "finite (report_states_at res v)"
by (simp add: report_states_at_def)
text ‹The stores one such state describes; ‹Bot› describes none.›
abbreviation report_conc :: "analysis_report ⇒ mcp_val lifted ⇒ store set" ("γ⇘_⇙") where
"γ⇘res⇙ ≡ gamma_lift (report_gamma res)"
definition report_sem :: "analysis_report ⇒ pp ⇒ store set" ("ℛ⇘_⇙") where
"ℛ⇘res⇙ v = (⋃d ∈ report_states_at res v. γ⇘res⇙ d)"
lemma mem_report_sem [simp]:
"s ∈ ℛ⇘res⇙ v ⟷ (∃d. Lifted d ∈ report_states_at res v ∧ s ∈ report_gamma res d)"
unfolding report_sem_def
proof
assume "s ∈ (⋃dl ∈ report_states_at res v. γ⇘res⇙ dl)"
then obtain dl where "dl ∈ report_states_at res v" and "s ∈ γ⇘res⇙ dl"
by blast
then show "∃d. Lifted d ∈ report_states_at res v ∧ s ∈ report_gamma res d" by (cases dl) auto
qed (metis UN_I gamma_lift_Lifted)
lemma report_semI [intro]:
"Lifted d ∈ report_states_at res v ⟹ s ∈ report_gamma res d ⟹ s ∈ ℛ⇘res⇙ v"
unfolding report_sem_def by (rule UN_I[of "Lifted d"]) simp_all
lemma report_semE [elim]:
assumes "s ∈ ℛ⇘res⇙ v"
obtains d where "Lifted d ∈ report_states_at res v" and "s ∈ report_gamma res d"
proof -
from assms
obtain dl where "dl ∈ report_states_at res v" and "s ∈ γ⇘res⇙ dl"
unfolding report_sem_def by blast
then show ?thesis by (cases dl) (auto intro: that)
qed
text ‹
The states a report holds at a point under one of its contexts: the rows at the point
whose context index names that context.
›
definition report_states_in :: "analysis_report ⇒ pp ⇒ report_context ⇒ mcp_val lifted set"
where
"report_states_in res v rc =
state_value ` {st ∈ set (report_states res). state_point st = v
∧ state_context st < length (report_contexts res)
∧ report_contexts res ! state_context st = rc}"
text ‹The stores a report describes at a point under one context.›
definition report_context_sem :: "analysis_report ⇒ pp ⇒ report_context ⇒ store set"
where
"report_context_sem res v rc = (⋃d ∈ report_states_in res v rc. γ⇘res⇙ d)"
lemma report_states_in_subset: "report_states_in res v rc ⊆ report_states_at res v"
unfolding report_states_in_def report_states_at_def by blast
lemma report_context_sem_subset: "report_context_sem res v rc ⊆ ℛ⇘res⇙ v"
unfolding report_context_sem_def report_sem_def using report_states_in_subset by blast
subsection ‹One state per point›
text ‹
\<^const>‹report_point_join› joins the states a report holds at a point over its
contexts. Every store the report describes at the point, the joined state describes,
since each component's concretization is monotone.
›
lemma gamma_lift_state_mono: "x ≤ y ⟹ γ x ⊆ γ (y :: _ abs_state lifted)"
by (rule gamma_lift_mono[where gam = gamma_state]) (use gamma_state_mono in blast)
lemma val_gamma_mono: "v ≤ v' ⟹ val_gamma a v ⊆ val_gamma a v'"
by (cases "(a, v)" rule: val_gamma.cases)
(auto simp: less_eq_analysis_product_def
intro: gamma_lift_state_mono[THEN subsetD] gamma_relc_mono[THEN subsetD])
lemma mcp_gamma_v_mono: "v ≤ v' ⟹ mcp_gamma_v as v ⊆ mcp_gamma_v as v'"
unfolding mcp_gamma_v_def using val_gamma_mono by blast
lemma fold_sup_ge: "x ∈ set xs ∨ x ≤ acc ⟹ x ≤ fold (⊔) xs (acc :: 'a::semilattice_sup)"
by (induction xs arbitrary: acc) (auto intro: le_supI1 le_supI2)
lemma report_states_at_le_point_join: "d ∈ report_states_at res v ⟹ d ≤ report_point_join res v"
unfolding report_states_at_def report_point_join_sup by (auto intro!: fold_sup_ge)
text ‹Every store the report describes at a point, the joined state describes.›
theorem report_sem_point_join:
"ℛ⇘res⇙ v ⊆ γ⇘res⇙ (report_point_join res v)"
proof
fix s assume "s ∈ ℛ⇘res⇙ v"
then obtain d where row: "Lifted d ∈ report_states_at res v" and s: "s ∈ report_gamma res d"
by blast
have "γ⇘res⇙ (Lifted d)
⊆ γ⇘res⇙ (report_point_join res v)"
by (rule gamma_lift_mono[OF _ report_states_at_le_point_join[OF row]])
(simp add: report_gamma_def mcp_gamma_v_mono)
with s show "s ∈ γ⇘res⇙ (report_point_join res v)" by auto
qed
subsection ‹Verdicts›
text ‹
‹report_checks_at› selects the checks a report records at one program point.
›
definition report_checks_at :: "analysis_report ⇒ pp ⇒ result_check set" where
"report_checks_at res v = {c ∈ set (report_checks res). check_point c = v}"
lemma mem_report_checks_at [simp]:
"c ∈ report_checks_at res v ⟷ c ∈ set (report_checks res) ∧ check_point c = v"
by (simp add: report_checks_at_def)
text ‹
What a decided verdict says about a store: ‹Check_Proved› that the condition
holds, ‹Check_Refuted› that it fails, ‹Check_Unknown› nothing.
›
fun verdict_holds :: "check_result ⇒ exp ⇒ store ⇒ bool" where
"verdict_holds Check_Proved e s = truthy (⟦e⟧⇩e s)"
| "verdict_holds Check_Refuted e s = (¬ truthy (⟦e⟧⇩e s))"
| "verdict_holds Check_Unknown e s = True"
text ‹
The stores a check's verdict admits. A ‹Dead› check claims nothing about stores;
its claim, that the point is unreached, is ‹DEAD› below.
›
definition check_stores :: "result_check ⇒ store set" where
"check_stores c = (case check_verdict c of
Decided r ⇒ {s. verdict_holds r (check_exp c) s}
| Dead ⇒ UNIV)"
definition verdict_stores :: "analysis_report ⇒ pp ⇒ store set" ("𝒱⇘_⇙") where
"𝒱⇘res⇙ v = (⋂c ∈ report_checks_at res v. check_stores c)"
lemma verdict_stores_eq:
"𝒱⇘res⇙ v =
{s. ∀c ∈ report_checks_at res v. ∀r.
check_verdict c = Decided r ⟶ verdict_holds r (check_exp c) s}"
unfolding verdict_stores_def check_stores_def by (auto split: lifted.splits)
definition HAS_VERDICT :: "analysis_report ⇒ pp ⇒ exp ⇒ check_result ⇒ bool" where
"HAS_VERDICT res v e r ⟷
(∃c ∈ report_checks_at res v. check_exp c = e ∧ check_verdict c = Decided r)"
abbreviation PROVED :: "analysis_report ⇒ pp ⇒ exp ⇒ bool" where
"PROVED res v e ≡ HAS_VERDICT res v e Check_Proved"
abbreviation REFUTED :: "analysis_report ⇒ pp ⇒ exp ⇒ bool" where
"REFUTED res v e ≡ HAS_VERDICT res v e Check_Refuted"
abbreviation UNKNOWN :: "analysis_report ⇒ pp ⇒ exp ⇒ bool" where
"UNKNOWN res v e ≡ HAS_VERDICT res v e Check_Unknown"
lemma verdict_storesD:
"s ∈ 𝒱⇘res⇙ v ⟹ HAS_VERDICT res v e r ⟹ verdict_holds r e s"
unfolding verdict_stores_eq HAS_VERDICT_def by blast
text ‹
‹DEAD› is a property of a point, not of a condition: every state the report holds
there is \<^const>‹Bot›. The states are canonical --- the table they come from
collapses a state its emptiness test rejects to \<^const>‹Bot› --- so ‹DEAD› reads
that canonical form instead of running a test. The test is sound and incomplete
for a product of analyses, so the converse of ‹analysis_report_dead› does not hold.
›
definition DEAD :: "analysis_report ⇒ pp ⇒ bool" where
"DEAD res v ⟷ (∀d ∈ report_states_at res v. d = Bot)"
subsection ‹A consistent report›
text ‹
A report is consistent when each check's verdict is the aggregate of the
report's own classifier over the report's own states at the check's point. Every
report \<^const>‹run_voblint› returns is consistent.
›
definition consistent_report :: "analysis_report ⇒ bool" where
"consistent_report res ⟷
(∀c ∈ set (report_checks res).
check_verdict c
= aggregate_verdicts
(classify_point (report_classify res) (check_exp c)
` report_states_at res (check_point c)))"
lemma consistent_report_decided:
assumes cons: "consistent_report res"
and c: "c ∈ report_checks_at res v"
and verdict: "check_verdict c = Decided r" and known: "r ≠ Check_Unknown"
and row: "Lifted d ∈ report_states_at res v"
shows "report_classify res (check_exp c) d = r"
proof -
from c have mem: "c ∈ set (report_checks res)" and pt: "check_point c = v"
by (simp_all add: report_checks_at_def)
have agg: "aggregate_verdicts
(classify_point (report_classify res) (check_exp c) ` report_states_at res v)
= Decided r"
using cons mem verdict pt unfolding consistent_report_def by auto
from aggregate_verdicts_decided_dest[OF agg known] row
show ?thesis by fastforce
qed
subsection ‹What a consistent report claims about its own states›
text ‹
A sound classifier's verdict holds at every store its abstract value admits:
both directions of ‹sound_classifier› at once, which is what lets a report
vouch for a ‹Check_Refuted› row as much as for a ‹Check_Proved› one.
›
lemma (in sound_classifier) classify_verdict_holds:
"t ∈ gm d ⟹ verdict_holds (classify cnd d) cnd t"
by (cases "classify cnd d") (auto dest: proved refuted)
theorem analysis_report_verdicts_sound:
assumes "consistent_report res"
shows "ℛ⇘res⇙ v ⊆ 𝒱⇘res⇙ v"
proof
fix s
assume "s ∈ ℛ⇘res⇙ v"
then obtain d where row: "Lifted d ∈ report_states_at res v" and s: "s ∈ report_gamma res d"
by (rule report_semE)
show "s ∈ 𝒱⇘res⇙ v"
unfolding verdict_stores_eq
proof (intro CollectI ballI allI impI)
fix c r
assume c: "c ∈ report_checks_at res v" and verdict: "check_verdict c = Decided r"
have holds: "verdict_holds (report_classify res (check_exp c) d) (check_exp c) s"
using s unfolding report_classify_def report_gamma_def
by (rule sound_classifier.classify_verdict_holds [OF mcp_sound_classifier])
show "verdict_holds r (check_exp c) s"
proof (cases "r = Check_Unknown")
case False
with consistent_report_decided[OF assms c verdict False row] holds show ?thesis by simp
qed simp
qed
qed
corollary analysis_report_proved:
assumes "consistent_report res" and "PROVED res v e" and "s ∈ ℛ⇘res⇙ v"
shows "truthy (⟦e⟧⇩e s)"
using verdict_storesD[OF subsetD[OF analysis_report_verdicts_sound[OF assms(1)] assms(3)]
assms(2)]
by simp
corollary analysis_report_refuted:
assumes "consistent_report res" and "REFUTED res v e" and "s ∈ ℛ⇘res⇙ v"
shows "¬ truthy (⟦e⟧⇩e s)"
using verdict_storesD[OF subsetD[OF analysis_report_verdicts_sound[OF assms(1)] assms(3)]
assms(2)]
by simp
theorem analysis_report_dead: "DEAD res v ⟹ ℛ⇘res⇙ v = {}"
unfolding DEAD_def report_sem_def by auto
text ‹Read as an emptiness test on points, ‹DEAD› is sound.›
corollary sound_emptiness_DEAD: "sound_emptiness (DEAD res) ℛ⇘res⇙"
by (rule sound_emptinessI) (rule analysis_report_dead)
text ‹
It is not exact. A report holding one state at a point, the combined state
\<^const>‹mcp_contradiction› of Interval and Parity, describes no store there, yet
that state is not \<^const>‹Bot›, so the point is not ‹DEAD›. The witness is a
report, not one a run is shown to return.
›
definition contradiction_report :: "pp ⇒ analysis_report" where
"contradiction_report v =
⦇ report_config = Analysis_Config [Interval_Analysis, Parity_Analysis] Globals_Join Ctx_None
Program_Globals_Flow_Sensitive,
report_vars = [], report_cfg = undefined, report_contexts = [Report_Unit],
report_states = [⦇ state_point = v, state_context = 0, state_value = Lifted mcp_contradiction,
state_checks = [], state_diagnostics = [], state_steps = [] ⦈],
report_routes = [], report_checks = [], report_globals = [], report_diagnostics = [] ⦈"
lemma DEAD_not_exact:
"¬ exact_emptiness (DEAD (contradiction_report v)) ℛ⇘contradiction_report v⇙"
proof -
have rows: "report_states_at (contradiction_report v) v = {Lifted mcp_contradiction}"
by (auto simp: report_states_at_def contradiction_report_def)
have live: "¬ DEAD (contradiction_report v) v"
by (simp add: DEAD_def rows)
have "report_config (contradiction_report v)
= Analysis_Config [Interval_Analysis, Parity_Analysis] Globals_Join Ctx_None
Program_Globals_Flow_Sensitive"
by (simp add: contradiction_report_def)
then have empty: "ℛ⇘contradiction_report v⇙ v = {}"
using mcp_contradiction_no_store by (auto simp: rows report_gamma_def activation_id)
show ?thesis
proof
assume "exact_emptiness (DEAD (contradiction_report v)) ℛ⇘contradiction_report v⇙"
from exact_emptinessD [OF this, of v] live empty show False by simp
qed
qed
text ‹A check printed dead is one presentation of a dead point.›
lemma analysis_report_check_dead:
assumes "consistent_report res" and "c ∈ set (report_checks res)"
and "check_verdict c = Dead"
shows "DEAD res (check_point c)"
proof -
have "aggregate_verdicts
(classify_point (report_classify res) (check_exp c) ` report_states_at res (check_point c))
= Dead"
using assms unfolding consistent_report_def by auto
then have "∀d ∈ report_states_at res (check_point c).
classify_point (report_classify res) (check_exp c) d = Dead"
by (simp add: aggregate_verdicts_eq_Dead_iff)
then show ?thesis
unfolding DEAD_def by (metis classify_point.elims lifted.distinct(1))
qed
text ‹
An ‹UNKNOWN› check makes no claim about the stores, and its point is not dead: the
report holds a state there that its classifier read.
›
lemma analysis_report_unknown:
assumes "consistent_report res" and "UNKNOWN res v e"
shows "¬ DEAD res v"
proof
assume dead: "DEAD res v"
from assms(2) obtain c where c: "c ∈ set (report_checks res)" "check_point c = v"
and verdict: "check_verdict c = Decided Check_Unknown"
unfolding HAS_VERDICT_def report_checks_at_def by blast
have "∀d ∈ report_states_at res v. classify_point (report_classify res) (check_exp c) d = Dead"
using dead unfolding DEAD_def by auto
then have "aggregate_verdicts
(classify_point (report_classify res) (check_exp c) ` report_states_at res v) = Dead"
by (simp add: aggregate_verdicts_eq_Dead_iff)
with assms(1) c verdict show False unfolding consistent_report_def by auto
qed
section ‹A report built from a sound table›
text ‹
\<^const>‹report_of› lists the contexts of the table in the order of an injective
key, so it lists every one, and files every covered key as a row. Its rows at a
point are therefore exactly the table's entries there.
›
lemma ordered_by_key_set:
assumes fin: "finite S" and inj: "inj_on rank S"
shows "set (ordered_by_key rank S) = S"
proof -
have pick: "the_elem (Set.filter (λx. rank x = rank y) S) = y" if "y ∈ S" for y
proof -
have "Set.filter (λx. rank x = rank y) S = {y}"
using that inj by (auto simp: inj_on_def)
then show ?thesis by simp
qed
have "set (ordered_by_key rank S) = (λk. the_elem (Set.filter (λx. rank x = k) S)) ` rank ` S"
unfolding ordered_by_key_def using fin by simp
also have "… = S"
using pick by (force simp: image_comp)
finally show ?thesis .
qed
lemma row_in_rows:
assumes "(i, ctx) ∈ set xs" and "v ∈ set ns" and "P v ctx"
shows "f i ctx v ∈ set (concat (map (λ(i, ctx). map (f i ctx) (filter (λv. P v ctx) ns)) xs))"
using assms by force
lemma report_states_at_report_of:
assumes fin: "finite (covered_keys (run_table sr))" and inj: "inj ctx_key"
shows "report_states_at (report_of config ctx_key ctx_tag classify sr p) v
= lookup_table (run_table sr) v ` table_contexts (run_table sr) v"
proof -
define r where "r = run_table sr"
define ctxs where "ctxs = ordered_by_key ctx_key (snd ` covered_keys r)"
define nodes where "nodes = cfg_node_list (prog_cfg p)
@ sorted_list_of_set (fst ` covered_keys r - set (cfg_node_list (prog_cfg p)))"
have ctxs: "set ctxs = snd ` covered_keys r"
unfolding ctxs_def r_def
by (rule ordered_by_key_set) (use fin inj in ‹auto intro: inj_on_subset›)
have nodes: "w ∈ set nodes" if "(w, ctx) ∈ covered_keys r" for w ctx
proof (cases "w ∈ set (cfg_node_list (prog_cfg p))")
case False
with that fin show ?thesis unfolding nodes_def r_def by (force intro: rev_image_eqI)
qed (simp add: nodes_def)
have indexed: "∃i. (i, ctx) ∈ set (enumerate 0 ctxs)" if "ctx ∈ set ctxs" for ctx
proof -
from that obtain i where "i < length ctxs" and "ctxs ! i = ctx"
by (auto simp: in_set_conv_nth)
then have "(i, ctx) ∈ set (enumerate 0 ctxs)"
by (metis add_0 length_enumerate nth_enumerate_eq nth_mem)
then show ?thesis ..
qed
show ?thesis
proof (intro equalityI subsetI)
fix d
assume "d ∈ report_states_at (report_of config ctx_key ctx_tag classify sr p) v"
then show "d ∈ lookup_table (run_table sr) v ` table_contexts (run_table sr) v"
unfolding report_states_at_def report_of_def Let_def by (auto simp: table_contexts_iff)
next
fix d
assume "d ∈ lookup_table (run_table sr) v ` table_contexts (run_table sr) v"
then obtain ctx where cov: "(v, ctx) ∈ covered_keys r"
and d: "d = lookup_table r v ctx"
by (auto simp: r_def table_contexts_iff)
from cov ctxs have "ctx ∈ set ctxs" by force
then obtain i where i: "(i, ctx) ∈ set (enumerate 0 ctxs)" using indexed by blast
have w: "v ∈ set nodes" using nodes[OF cov] .
show "d ∈ report_states_at (report_of config ctx_key ctx_tag classify sr p) v"
unfolding report_states_at_def report_of_def Let_def r_def[symmetric] ctxs_def[symmetric]
nodes_def[symmetric]
apply (simp only: analysis_report.select_convs)
apply (rule image_eqI[rotated], rule CollectI, rule conjI, rule row_in_rows[OF i w])
using cov d by (simp_all add: r_def)
qed
qed
text ‹
Each entry of the table is a row of the report under its own context: the context's
index into the report's context list names it.
›
lemma report_states_in_report_of:
assumes fin: "finite (covered_keys (run_table sr))" and inj: "inj ctx_key"
and cov: "ctx ∈ table_contexts (run_table sr) v"
shows "lookup_table (run_table sr) v ctx
∈ report_states_in (report_of config ctx_key ctx_tag classify sr p) v (ctx_tag ctx)"
proof -
define r where "r = run_table sr"
define ctxs where "ctxs = ordered_by_key ctx_key (snd ` covered_keys r)"
define nodes where "nodes = cfg_node_list (prog_cfg p)
@ sorted_list_of_set (fst ` covered_keys r - set (cfg_node_list (prog_cfg p)))"
have ctxs: "set ctxs = snd ` covered_keys r"
unfolding ctxs_def r_def
by (rule ordered_by_key_set) (use fin inj in ‹auto intro: inj_on_subset›)
from cov have covk: "(v, ctx) ∈ covered_keys r" by (simp add: r_def)
have w: "v ∈ set nodes"
proof (cases "v ∈ set (cfg_node_list (prog_cfg p))")
case False
with covk fin show ?thesis unfolding nodes_def r_def by (force intro: rev_image_eqI)
qed (simp add: nodes_def)
from covk ctxs have "ctx ∈ set ctxs" by force
then obtain i where "i < length ctxs" and nth: "ctxs ! i = ctx"
by (auto simp: in_set_conv_nth)
then have i: "(i, ctx) ∈ set (enumerate 0 ctxs)" and len: "i < length ctxs"
by (auto simp: in_set_enumerate_eq)
show ?thesis
unfolding report_states_in_def report_of_def Let_def r_def[symmetric] ctxs_def[symmetric]
nodes_def[symmetric]
apply (simp only: analysis_report.select_convs)
apply (rule image_eqI[rotated], rule CollectI, rule conjI, rule row_in_rows[OF i w])
using covk len nth by (simp_all add: report_row_def Let_def r_def)
qed
lemma report_of_simps [simp]:
"report_config (report_of config ctx_key ctx_tag classify sr p) = config"
"report_cfg (report_of config ctx_key ctx_tag classify sr p) = prog_cfg p"
"report_checks (report_of config ctx_key ctx_tag classify sr p)
= result_checks_of (prog_cfg p) (run_table sr) classify"
"report_diagnostics (report_of config ctx_key ctx_tag classify sr p)
= arithmetic_diagnostics (prog_cfg p) (run_table sr) classify"
by (simp_all add: report_of_def Let_def)
text ‹
What a report built from a run of a program owes: its verdicts agree with its
states, its states cover the collecting semantics, its diagnostics name every
point where a divisor may be zero, and its check column lists the program's checks.
›
definition sound_report :: "imp_prog ⇒ analysis_report ⇒ bool" where
"sound_report p res ⟷
consistent_report res
∧ (∀v. 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v ⊆ ℛ⇘res⇙ v)
∧ (∀v s. s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v
⟶ (∀d ∈ set (report_diagnostics res). diagnostic_point d ≠ v)
⟶ arithmetic_safe_at (prog_cfg p) v s)
∧ (∀d ∈ set (report_diagnostics res). diagnostic_verdict d = Check_Refuted
⟶ (∀s ∈ ℛ⇘res⇙ (diagnostic_point d).
¬ truthy (⟦arithmetic_condition (diagnostic_obligation d)⟧⇩e s)))
∧ map (λc. (check_point c, check_label c, check_exp c)) (report_checks res)
= check_sites (prog_cfg p)"
subsection ‹Contexts under one name›
text ‹
Each context policy has a context type of its own, and the report files every
context under one type, \<^typ>‹report_context›, through an injective tag. Renaming
a policy's contexts through the tag keeps which contexts a trace carries, so the
activation buckets survive the renaming unchanged.
›
definition map_context_policy :: "('c ⇒ 'd) ⇒ 'c context_policy ⇒ 'd context_policy" where
"map_context_policy f adm u d ci s es = (⋃c ∈ f -` {d}. f ` adm u c ci s es)"
lemma admits_call_context_map_policy:
assumes inj: "inj f"
shows "admits_call_context 𝒢 g (map_context_policy f adm) u (f c) q s es d'
⟷ (∃c'. d' = f c' ∧ admits_call_context 𝒢 g adm u c q s es c')"
unfolding admits_call_context_def map_context_policy_def
using inj by (auto simp: inj_eq) blast+
lemma activation_context_rel_map_policy:
assumes inj: "inj f"
shows "activation_context_rel 𝒢 (map_context_policy f adm) (f c⇩0) g t d
⟷ (∃c. d = f c ∧ activation_context_rel 𝒢 adm c⇩0 g t c)"
proof
assume "activation_context_rel 𝒢 (map_context_policy f adm) (f c⇩0) g t d"
then show "∃c. d = f c ∧ activation_context_rel 𝒢 adm c⇩0 g t c"
proof induction
case (Root xs)
then show ?case by blast
next
case (Call caller x p es x' xs)
then obtain c where c: "x = f c" "activation_context_rel 𝒢 adm c⇩0 g caller c"
by blast
with Call.hyps(2) obtain c' where "x' = f c'"
and "admits_call_context 𝒢 g adm (sink_node caller) c p (sink_store caller) es c'"
by (auto simp: admits_call_context_map_policy [OF inj])
with c(2) show ?case by blast
next
case (Resume current x callee xs)
then show ?case by blast
qed
next
assume "∃c. d = f c ∧ activation_context_rel 𝒢 adm c⇩0 g t c"
then obtain c where d: "d = f c" and rel: "activation_context_rel 𝒢 adm c⇩0 g t c"
by blast
from rel show "activation_context_rel 𝒢 (map_context_policy f adm) (f c⇩0) g t d"
unfolding d
proof induction
case (Root xs)
then show ?case by blast
next
case (Call caller x p es x' xs)
then show ?case
by (blast intro: admits_call_context_map_policy [OF inj, THEN iffD2])
next
case (Resume current x callee xs)
then show ?case by blast
qed
qed
text ‹
What a report guarantees per context, for a policy over report contexts: every
valid activation trace carries one of the policy's contexts, and each context's
activation bucket lies in the stores the report's states for that context describe.
A context the report holds no state for at a point has an empty bucket there.
›
definition context_sound ::
"imp_prog ⇒ analysis_report ⇒ report_context context_policy ⇒ report_context ⇒ bool"
where
"context_sound p res adm rc ⟷
(∀t ∈ 𝒯⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙.
∃c. activation_context_rel (declared_global p) adm rc (prog_cfg p) t c)
∧ (∀v c. 𝒜⇘declared_global p,adm,rc,prog_cfg p,cinit_stores (declared_global p)⇙ v c
⊆ report_context_sem res v c)"
lemma context_sound_point:
"context_sound p res adm rc
⟹ 𝒜⇘declared_global p,adm,rc,prog_cfg p,cinit_stores (declared_global p)⇙ v c
⊆ ℛ⇘res⇙ v"
unfolding context_sound_def using report_context_sem_subset by blast
text ‹
The context policy a configuration runs with, under its report contexts, and the
context of ‹main›. The entry-state policy is read off the program's own solve.
›
definition run_policy :: "analysis_config ⇒ imp_prog ⇒ report_context context_policy" where
"run_policy config p =
(case config_context config of
Ctx_None ⇒
map_context_policy (λ_ :: unit. Report_Unit) (context_policy_of_fun (λu c t. ()))
| Ctx_CallString k ⇒
map_context_policy Report_Call_String
(context_policy_of_fun (λu ctx t. cs_context k u ctx t))
| Ctx_EntryState ⇒
map_context_policy Report_Entry
(case config_globals config of
Program_Globals_Flow_Sensitive ⇒
mcp_es_rule.admitted_contexts (config_analyses config) (config_rule config)
(declared_global p) p
| Program_Globals_Flow_Insensitive ⇒
mcp_split_es_rule.admitted_contexts (config_analyses config) (config_rule config)
(declared_global p) p))"
definition run_root :: "analysis_config ⇒ report_context" where
"run_root config =
(case config_context config of
Ctx_None ⇒ Report_Unit
| Ctx_CallString k ⇒ Report_Call_String []
| Ctx_EntryState ⇒ Report_Entry mcp_root_ctx)"
lemma report_of_sound:
assumes act: "activation_table p (run_table sr) gm adm rc"
and fin: "finite (covered_keys (run_table sr))" and inj: "inj ctx_key"
and tag: "inj ctx_tag"
and cl: "classify = mcp_classify (activation (config_analyses config))"
and gm: "gm = mcp_gamma_v (activation (config_analyses config))"
shows "sound_report p (report_of config ctx_key ctx_tag classify sr p)
∧ context_sound p (report_of config ctx_key ctx_tag classify sr p)
(map_context_policy ctx_tag adm) (ctx_tag rc)"
proof -
note cov = activation_table.covered [OF act]
have st: "sound_table p (run_table sr) classify gm"
by (rule sound_table.intro [OF cov]) (unfold cl gm, rule mcp_sound_classifier)
let ?res = "report_of config ctx_key ctx_tag classify sr p"
note rows = report_states_at_report_of[OF fin inj]
have cons: "consistent_report ?res"
unfolding consistent_report_def
by (auto simp: result_checks_of_def point_verdict_def rows report_classify_def cl image_comp
comp_def)
have covers: "s ∈ ℛ⇘?res⇙ v"
if "s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v" for v s
proof -
from covered_table.covers[OF cov that] obtain ctx d
where look: "lookup_table (run_table sr) v ctx = Lifted d" and s: "s ∈ gm d"
unfolding table_covers_def by blast
then have "Lifted d ∈ report_states_at ?res v"
unfolding rows by (metis image_eqI lookup_table_LiftedD)
with s show ?thesis by (auto simp: report_gamma_def gm)
qed
have safe: "arithmetic_safe_at (prog_cfg p) v s"
if "s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v"
and "∀d ∈ set (report_diagnostics ?res). diagnostic_point d ≠ v" for v s
using sound_table.arithmetic_safe[OF st _ that(1)] that(2) by simp
have refuted: "¬ truthy (⟦arithmetic_condition (diagnostic_obligation d)⟧⇩e s)"
if d: "d ∈ set (report_diagnostics ?res)" and r: "diagnostic_verdict d = Check_Refuted"
and s: "s ∈ ℛ⇘?res⇙ (diagnostic_point d)" for d s
proof -
let ?e = "arithmetic_condition (diagnostic_obligation d)"
have pv: "point_verdict (run_table sr) classify (diagnostic_point d) ?e = Decided Check_Refuted"
using arithmetic_diagnostics_refuted d r by simp
from s obtain st where row: "Lifted st ∈ report_states_at ?res (diagnostic_point d)"
and sg: "s ∈ report_gamma ?res st"
by (rule report_semE)
then obtain ctx where "lookup_table (run_table sr) (diagnostic_point d) ctx = Lifted st"
unfolding rows by force
then have "classify ?e st = Check_Refuted"
by (rule point_verdict_decided[OF pv, rotated]) simp
with sg show ?thesis
unfolding cl report_gamma_def report_of_simps by (blast dest: mcp_classify_refuted)
qed
have sr: "sound_report p ?res"
unfolding sound_report_def
using cons covers safe refuted by (auto simp: result_checks_of_sites)
have ctx: "context_sound p ?res (map_context_policy ctx_tag adm) (ctx_tag rc)"
unfolding context_sound_def
proof (intro conjI ballI allI subsetI)
fix t
assume t: "t ∈ 𝒯⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙"
from activation_table.has_context [OF act t]
show "∃c. activation_context_rel (declared_global p) (map_context_policy ctx_tag adm)
(ctx_tag rc) (prog_cfg p) t c"
by (auto simp: activation_context_rel_map_policy [OF tag])
next
fix v d s
assume "s ∈ 𝒜⇘declared_global p,map_context_policy ctx_tag adm,ctx_tag rc,prog_cfg p,
cinit_stores (declared_global p)⇙ v d"
then obtain t where t: "t ∈ 𝒯⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙"
"sink_node t = v" "sink_store t = s"
and rel: "activation_context_rel (declared_global p) (map_context_policy ctx_tag adm)
(ctx_tag rc) (prog_cfg p) t d"
unfolding activation_collect_def by blast
from rel obtain c where d: "d = ctx_tag c"
and "activation_context_rel (declared_global p) adm rc (prog_cfg p) t c"
by (auto simp: activation_context_rel_map_policy [OF tag])
with t have "s ∈ 𝒜⇘declared_global p,adm,rc,prog_cfg p,cinit_stores (declared_global p)⇙ v c"
unfolding activation_collect_def by blast
with activation_table.bucket_bound [OF act]
have "s ∈ gamma_lift gm (lookup_table (run_table sr) v c)" by blast
then obtain st where look: "lookup_table (run_table sr) v c = Lifted st" and s: "s ∈ gm st"
by (cases "lookup_table (run_table sr) v c") auto
then have "Lifted st ∈ report_states_in ?res v d"
unfolding d using report_states_in_report_of[OF fin inj lookup_table_LiftedD[OF look]]
by simp
with s show "s ∈ report_context_sem ?res v d"
unfolding report_context_sem_def by (auto simp: report_gamma_def gm intro!: bexI)
qed
show ?thesis using sr ctx by blast
qed
text ‹
The one argument that reads the context policy. Each policy's report comes from
its registration's executable solve, whose answer is the solve the registration's
soundness theorem is about; the rest is ‹report_of_sound›.
›
lemma inj_call_string_key: "inj (λctx. Key_List (map Key_Node ctx))"
by (rule injI) (simp add: inj_def)
lemma inj_entry_ctx_key: "inj (entry_ctx_key as)"
by (rule injI) (rule entry_ctx_key_inject)
lemma analysis_report_of_sound:
assumes wf: "wf_program_compile_input p"
and some: "analysis_report_of config p = Some res"
shows "sound_report p res ∧ context_sound p res (run_policy config p) (run_root config)"
proof (cases config)
case (Analysis_Config as r ctx pg)
show ?thesis
proof (cases ctx)
case Ctx_None
show ?thesis
proof (cases pg)
case Program_Globals_Flow_Sensitive
from some obtain sol where
sol: "TD_side_rule_Interp_solve_c r (mcp_rule.equations as (declared_global p) p)
(mcp_rule.root_query p) = Some sol"
and res: "res = report_of config (λ_. Key_List []) (λ_. Report_Unit)
(mcp_classify (activation as))
(mcp_rule.solved_run_of as (declared_global p) p sol) p"
by (auto simp: Analysis_Config Ctx_None Program_Globals_Flow_Sensitive
dg_pipeline.root_query_def
mcp_wrappers mcp_place_defs)
note run = mcp_rule.solve_c_run[OF sol]
have pol: "run_policy config p
= map_context_policy (λ_ :: unit. Report_Unit) (context_policy_of_fun (λu c t. ()))"
"run_root config = Report_Unit"
by (simp_all add: run_policy_def run_root_def Analysis_Config Ctx_None)
show ?thesis
unfolding res run(2) pol
by (rule report_of_sound[where rc = "()", OF _ _ _ _ _ refl])
(use mcp_rule_table[OF wf run(1)] mcp_rule.vars_finite_of_terminates[OF run(1)] in
‹simp_all add: Analysis_Config finite_solved_table_def dg_pipeline.result_def
dg_pipeline.sol_vars_def inj_def›)
next
case Program_Globals_Flow_Insensitive
from some obtain sol where
sol: "TD_side_rule_Interp_solve_c r (mcp_split_rule.equations as (declared_global p) p)
(mcp_split_rule.root_query p) = Some sol"
and res: "res = report_of config (λ_. Key_List []) (λ_. Report_Unit)
(mcp_classify (activation as))
(mcp_split_rule.solved_run_of as (declared_global p) p sol) p"
by (auto simp: Analysis_Config Ctx_None Program_Globals_Flow_Insensitive
dg_pipeline.root_query_def
mcp_wrappers mcp_place_defs)
note run = mcp_split_rule.solve_c_run[OF sol]
have pol: "run_policy config p
= map_context_policy (λ_ :: unit. Report_Unit) (context_policy_of_fun (λu c t. ()))"
"run_root config = Report_Unit"
by (simp_all add: run_policy_def run_root_def Analysis_Config Ctx_None)
show ?thesis
unfolding res run(2) pol
by (rule report_of_sound[where rc = "()", OF _ _ _ _ _ refl])
(use mcp_split_rule_table[OF wf run(1)]
mcp_split_rule.vars_finite_of_terminates[OF run(1)] in
‹simp_all add: Analysis_Config finite_solved_table_def dg_pipeline.result_def
dg_pipeline.sol_vars_def inj_def›)
qed
next
case Ctx_EntryState
show ?thesis
proof (cases pg)
case Program_Globals_Flow_Sensitive
from some obtain sol where
sol: "TD_side_rule_Interp_solve_c r (mcp_es_rule.equations as (declared_global p) p)
(mcp_es_rule.root_query p) = Some sol"
and res: "res = report_of config (entry_ctx_key (activation as)) Report_Entry
(mcp_classify (activation as))
(mcp_es_rule.solved_run_of as (declared_global p) p sol) p"
by (auto simp: Analysis_Config Ctx_EntryState Program_Globals_Flow_Sensitive
dg_pipeline.root_query_def mcp_wrappers mcp_place_defs)
note run = mcp_es_rule.solve_c_run[OF sol]
have pol: "run_policy config p
= map_context_policy Report_Entry
(mcp_es_rule.admitted_contexts as r (declared_global p) p)"
"run_root config = Report_Entry mcp_root_ctx"
by (simp_all add: run_policy_def run_root_def Analysis_Config Ctx_EntryState
Program_Globals_Flow_Sensitive)
show ?thesis
unfolding res run(2) pol
by (rule report_of_sound[OF _ _ inj_entry_ctx_key _ _ refl])
(use mcp_es_rule_table[OF wf run(1)] mcp_es_rule.vars_finite_of_terminates[OF run(1)] in
‹simp_all add: Analysis_Config finite_solved_table_def dg_pipeline.result_def
dg_pipeline.sol_vars_def inj_def›)
next
case Program_Globals_Flow_Insensitive
from some obtain sol where
sol: "TD_side_rule_Interp_solve_c r (mcp_split_es_rule.equations as (declared_global p) p)
(mcp_split_es_rule.root_query p) = Some sol"
and res: "res = report_of config (entry_ctx_key (activation as)) Report_Entry
(mcp_classify (activation as))
(mcp_split_es_rule.solved_run_of as (declared_global p) p sol) p"
by (auto simp: Analysis_Config Ctx_EntryState Program_Globals_Flow_Insensitive
dg_pipeline.root_query_def mcp_wrappers mcp_place_defs)
note run = mcp_split_es_rule.solve_c_run[OF sol]
have pol: "run_policy config p
= map_context_policy Report_Entry
(mcp_split_es_rule.admitted_contexts as r (declared_global p) p)"
"run_root config = Report_Entry mcp_root_ctx"
by (simp_all add: run_policy_def run_root_def Analysis_Config Ctx_EntryState
Program_Globals_Flow_Insensitive)
show ?thesis
unfolding res run(2) pol
by (rule report_of_sound[OF _ _ inj_entry_ctx_key _ _ refl])
(use mcp_split_es_rule_table[OF wf run(1)]
mcp_split_es_rule.vars_finite_of_terminates[OF run(1)] in
‹simp_all add: Analysis_Config finite_solved_table_def dg_pipeline.result_def
dg_pipeline.sol_vars_def inj_def›)
qed
next
case (Ctx_CallString k)
show ?thesis
proof (cases pg)
case Program_Globals_Flow_Sensitive
from some obtain sol where
sol: "TD_side_rule_Interp_solve_c r (mcp_cs_rule.equations as k (declared_global p) p)
(mcp_cs_rule.root_query p) = Some sol"
and res: "res = report_of config (λctx. Key_List (map Key_Node ctx)) Report_Call_String
(mcp_classify (activation as))
(mcp_cs_rule.solved_run_of as k (declared_global p) p sol) p"
by (auto simp: Analysis_Config Ctx_CallString Program_Globals_Flow_Sensitive
dg_pipeline.root_query_def mcp_wrappers mcp_place_defs)
note run = mcp_cs_rule.solve_c_run[OF sol]
have pol: "run_policy config p
= map_context_policy Report_Call_String
(context_policy_of_fun (λu ctx t. cs_context k u ctx t))"
"run_root config = Report_Call_String []"
by (simp_all add: run_policy_def run_root_def Analysis_Config Ctx_CallString)
show ?thesis
unfolding res run(2) pol
by (rule report_of_sound[OF _ _ inj_call_string_key _ _ refl])
(use mcp_cs_rule_table[OF wf run(1)] mcp_cs_rule.vars_finite_of_terminates[OF run(1)] in
‹simp_all add: Analysis_Config finite_solved_table_def dg_pipeline.result_def
dg_pipeline.sol_vars_def inj_def›)
next
case Program_Globals_Flow_Insensitive
from some obtain sol where
sol: "TD_side_rule_Interp_solve_c r (mcp_split_cs_rule.equations as k (declared_global p) p)
(mcp_split_cs_rule.root_query p) = Some sol"
and res: "res = report_of config (λctx. Key_List (map Key_Node ctx)) Report_Call_String
(mcp_classify (activation as))
(mcp_split_cs_rule.solved_run_of as k (declared_global p) p sol) p"
by (auto simp: Analysis_Config Ctx_CallString Program_Globals_Flow_Insensitive
dg_pipeline.root_query_def mcp_wrappers mcp_place_defs)
note run = mcp_split_cs_rule.solve_c_run[OF sol]
have pol: "run_policy config p
= map_context_policy Report_Call_String
(context_policy_of_fun (λu ctx t. cs_context k u ctx t))"
"run_root config = Report_Call_String []"
by (simp_all add: run_policy_def run_root_def Analysis_Config Ctx_CallString)
show ?thesis
unfolding res run(2) pol
by (rule report_of_sound[OF _ _ inj_call_string_key _ _ refl])
(use mcp_split_cs_rule_table[OF wf run(1)]
mcp_split_cs_rule.vars_finite_of_terminates[OF run(1)] in
‹simp_all add: Analysis_Config finite_solved_table_def dg_pipeline.result_def
dg_pipeline.sol_vars_def inj_def›)
qed
qed
qed
subsection ‹A well-formed report›
text ‹
What a reader of the report relies on beyond its verdicts: every context index
names a listed context, a point has at most one row per context, and a row's check
and obligation columns list exactly the report's checks and the graph's arithmetic
obligations at the row's point, each with the verdict of the row's own state. No
soundness theorem needs this; a renderer does.
›
definition obligations_at :: "cfg ⇒ pp ⇒ arithmetic_obligation list" where
"obligations_at g v = concat (map snd (filter (λ(u, obs). u = v) (arithmetic_sites g)))"
lemma group_lookup_arithmetic_sites:
"concat (group_lookup (group_by_key fst (Some ∘ snd) (arithmetic_sites g)) v)
= obligations_at g v"
proof -
have "List.map_filter (λx. if fst x = v then (Some ∘ snd) x else None) xs
= map snd (filter (λ(u, obs). u = v) xs)"
for xs :: "(pp × arithmetic_obligation list) list"
by (induction xs) (auto simp: List.map_filter_simps)
then show ?thesis unfolding group_lookup_group_by_key obligations_at_def by simp
qed
definition well_formed_report :: "analysis_report ⇒ bool" where
"well_formed_report res ⟷
(∀st ∈ set (report_states res). state_context st < length (report_contexts res))
∧ distinct (map (λst. (state_point st, state_context st)) (report_states res))
∧ (∀rt ∈ set (report_routes res).
route_context rt < length (report_contexts res)
∧ (∀i ∈ set (route_targets rt). i < length (report_contexts res)))
∧ (∀st ∈ set (report_states res).
state_checks st
= map (λc. (check_exp c,
classify_point (report_classify res) (check_exp c) (state_value st)))
(filter (λc. check_point c = state_point st) (report_checks res))
∧ state_diagnostics st
= map (λob. (ob,
classify_point (report_classify res) (arithmetic_condition ob)
(state_value st)))
(obligations_at (report_cfg res) (state_point st)))"
text ‹
With a consistent report, the check column is the aggregate of the rows: a check's
verdict joins the verdicts the rows at its point give its condition.
›
lemma well_formed_check_verdict:
assumes cons: "consistent_report res" and wf: "well_formed_report res"
and c: "c ∈ set (report_checks res)"
shows "check_verdict c
= aggregate_verdicts
{verdict | st verdict. st ∈ set (report_states res)
∧ state_point st = check_point c ∧ (check_exp c, verdict) ∈ set (state_checks st)}"
proof -
let ?cl = "classify_point (report_classify res) (check_exp c)"
have rows: "state_checks st
= map (λc. (check_exp c, classify_point (report_classify res) (check_exp c)
(state_value st)))
(filter (λc'. check_point c' = state_point st) (report_checks res))"
if "st ∈ set (report_states res)" for st
using wf that unfolding well_formed_report_def by blast
have "{verdict | st verdict. st ∈ set (report_states res)
∧ state_point st = check_point c ∧ (check_exp c, verdict) ∈ set (state_checks st)}
= ?cl ` report_states_at res (check_point c)"
proof (intro equalityI subsetI)
fix x
assume "x ∈ {verdict | st verdict. st ∈ set (report_states res)
∧ state_point st = check_point c ∧ (check_exp c, verdict) ∈ set (state_checks st)}"
then obtain st where st: "st ∈ set (report_states res)" and pt: "state_point st = check_point c"
and mem: "(check_exp c, x) ∈ set (state_checks st)" by blast
from mem rows[OF st] have "x = ?cl (state_value st)" by auto
with st pt show "x ∈ ?cl ` report_states_at res (check_point c)"
unfolding report_states_at_def by blast
next
fix x
assume "x ∈ ?cl ` report_states_at res (check_point c)"
then obtain st where st: "st ∈ set (report_states res)" and pt: "state_point st = check_point c"
and x: "x = ?cl (state_value st)"
unfolding report_states_at_def by blast
have "(check_exp c, x) ∈ set (state_checks st)"
unfolding rows[OF st] using c pt x by force
with st pt show "x ∈ {verdict | st verdict. st ∈ set (report_states res)
∧ state_point st = check_point c ∧ (check_exp c, verdict) ∈ set (state_checks st)}"
by blast
qed
with cons c show ?thesis unfolding consistent_report_def by simp
qed
lemma distinct_indexed_rows:
"distinct ns
⟹ distinct (concat (map (λ(i, x). map (λv. (v, i)) (filter (λv. P v x) ns))
(enumerate n xs)))"
proof (induction xs arbitrary: n)
case (Cons x xs)
have "n < i" if "(w, i) ∈ set (concat (map (λ(i, x). map (λv. (v, i)) (filter (λv. P v x) ns))
(enumerate (Suc n) xs)))" for w i
using that by (auto simp: in_set_enumerate_eq)
with Cons.IH[of "Suc n"] Cons.prems show ?case
by (fastforce simp: distinct_map inj_on_def)
qed simp
lemma map_check_exp_result_checks_of:
"map check_exp (filter (λc. check_point c = v) (result_checks_of g r classify))
= group_lookup (group_by_key (λ(u, a, w). u)
(λ(u, a, w). if is_EA_Check a then Some (ea_check_cond a) else None) (cfg_intra_list g)) v"
proof -
have "map check_exp (filter (λc. check_point c = v)
(map (λ(u, a, w). ⦇ check_point = u, check_label = ea_check_label a,
check_exp = ea_check_cond a, check_verdict = V u a ⦈)
(filter (λ(u, a, w). is_EA_Check a) es)))
= List.map_filter (λx. if (λ(u, a, w). u) x = v
then (λ(u, a, w). if is_EA_Check a then Some (ea_check_cond a)
else None) x
else None) es" for es V
by (induction es) (auto simp: List.map_filter_simps)
then show ?thesis
unfolding result_checks_of_def group_lookup_group_by_key .
qed
lemma report_of_well_formed:
assumes cl: "classify = mcp_classify (activation (config_analyses config))"
shows "well_formed_report (report_of config ctx_key ctx_tag classify sr p)"
proof -
let ?res = "report_of config ctx_key ctx_tag classify sr p"
define r where "r = run_table sr"
define g where "g = prog_cfg p"
define ctxs where "ctxs = ordered_by_key ctx_key (snd ` covered_keys r)"
define nodes where "nodes = cfg_node_list g
@ sorted_list_of_set (fst ` covered_keys r - set (cfg_node_list g))"
define checks where "checks = group_by_key (λ(u, a, w). u)
(λ(u, a, w). if is_EA_Check a then Some (ea_check_cond a) else None) (cfg_intra_list g)"
define obls where "obls = group_by_key fst (Some ∘ snd) (arithmetic_sites g)"
define steps where "steps = group_by_key (λ(u, a, w). u) (λ(u, a, w). Some (a, w))
(cfg_intra_list g)"
have classify: "report_classify ?res = classify"
by (simp add: report_classify_def cl)
have contexts: "length (report_contexts ?res) = length ctxs"
by (simp add: report_of_def Let_def ctxs_def r_def)
have states: "report_states ?res
= concat (map (λ(i, ctx). map (report_row sr classify checks obls steps i ctx)
(filter (λv. (v, ctx) ∈ covered_keys r) nodes))
(enumerate 0 ctxs))"
by (simp add: report_of_def Let_def ctxs_def r_def nodes_def g_def checks_def obls_def
steps_def)
have in_range: "state_context st < length ctxs" if "st ∈ set (report_states ?res)" for st
using that by (auto simp: states in_set_enumerate_eq)
have "distinct (cfg_node_list g)" by (simp add: cfg_node_list_def)
then have "distinct nodes"
unfolding nodes_def by (cases "finite (fst ` covered_keys r - set (cfg_node_list g))") auto
then have distinct:
"distinct (map (λst. (state_point st, state_context st)) (report_states ?res))"
using distinct_indexed_rows[of nodes "λv ctx. (v, ctx) ∈ covered_keys r" 0 ctxs]
by (simp add: states map_concat case_prod_unfold comp_def)
have routes: "route_context rt < length ctxs ∧ (∀i ∈ set (route_targets rt). i < length ctxs)"
if "rt ∈ set (report_routes ?res)" for rt
using that
by (auto simp: report_of_def Let_def ctxs_def r_def context_indices_def in_set_enumerate_eq
split: lifted.splits)
have rows: "state_checks st
= map (λc. (check_exp c, classify_point classify (check_exp c) (state_value st)))
(filter (λc. check_point c = state_point st) (report_checks ?res))
∧ state_diagnostics st
= map (λob. (ob, classify_point classify (arithmetic_condition ob)
(state_value st)))
(obligations_at g (state_point st))"
if "st ∈ set (report_states ?res)" for st
proof -
from that obtain i ctx v where st: "st = report_row sr classify checks obls steps i ctx v"
by (auto simp: states)
have "map check_exp (filter (λc. check_point c = v) (report_checks ?res))
= group_lookup checks v" (is "map check_exp ?cs = _")
by (simp add: map_check_exp_result_checks_of checks_def g_def)
moreover have "map (λc. (check_exp c, classify_point classify (check_exp c) (lookup_table r v ctx)))
?cs
= map (λcond. (cond, classify_point classify cond (lookup_table r v ctx)))
(map check_exp ?cs)"
by simp
ultimately have "map (λc. (check_exp c, classify_point classify (check_exp c) (lookup_table r v ctx)))
?cs
= map (λcond. (cond, classify_point classify cond (lookup_table r v ctx)))
(group_lookup checks v)"
by simp
moreover have "concat (group_lookup obls v) = obligations_at g v"
unfolding obls_def by (rule group_lookup_arithmetic_sites)
ultimately show ?thesis unfolding st by (auto simp: report_row_def Let_def r_def)
qed
have cfg: "report_cfg ?res = g" by (simp add: g_def)
show ?thesis
unfolding well_formed_report_def classify contexts cfg
using in_range distinct routes rows by blast
qed
lemma analysis_report_of_well_formed:
"analysis_report_of config p = Some res ⟹ well_formed_report res"
by (induct config p rule: analysis_report_of.induct) (auto intro: report_of_well_formed)
end