Theory MCP_Analyses
theory MCP_Analyses
imports MCP_Carrier
begin
section ‹The registered analyses, run as one›
text ‹
\<^theory>‹Voblint_CLI.MCP_Carrier› lays out one field per registered analysis
and states how each field runs, describes, reads back and answers. This theory
runs the active fields as one component, proves the combination sound whatever
analyses are registered, and registers it at every context policy. Every proof
here goes by cases over the registered analyses, so a new analysis in the
manifest needs nothing new here.
›
subsection ‹Each analysis on its own field›
lemma field_spec_frame:
"a ≠ b ⟹ mcp_frame (field_spec (registration_of a) 𝒢 p) (part_gamma 𝒢 b)"
by (cases a rule: analysis_domain_cases; cases b rule: analysis_domain_cases;
simp only: part_gamma.simps registration_of.simps analysis_registration.simps;
rule field_frame; simp add: lift_get_put_other)
lemma part_gamma_rd: "part_gamma 𝒢 a x = gamma_lift (val_gamma a) (map_lift (mcp_rd 𝒢) x)"
by (cases a rule: analysis_domain_cases; cases x)
(simp_all add: mcp_rd_def gamma_lift_default_st_gamma_to_fun)
subsection ‹Each analysis answers what it knows›
text ‹
While the system is solved, a field answers a query as its published value
does: from its own publication map, through the answer its analysis registers for
checks. An analysis written without a query handler thereby becomes a
provider on the combined state, as every Goblint analysis answers
‹EvalInt› from its own domain. The answer is sound for the stores the
field describes, so the handler replaces the component's own
(\<^const>‹with_qry›) without touching a transfer.
›
definition part_answer :: "(vname ⇒ bool) ⇒ analysis_domain ⇒ mcp_st lifted ⇒ channel"
where
"part_answer 𝒢 a x q =
(case x of Bot ⇒ ⊤ | Lifted r ⇒ value_answer (registration_of a) (mcp_rd 𝒢 r) q)"
lemma part_answer_sound: "s ∈ part_gamma 𝒢 a x ⟹ eval_holds q (part_answer 𝒢 a x q) s"
by (cases x) (auto simp: part_answer_def part_gamma_rd intro: value_answer_sound)
definition mcp_field ::
"(vname ⇒ bool) ⇒ imp_prog ⇒ analysis_domain ⇒ mcp_st lifted local_spec" where
"mcp_field 𝒢 p a = with_qry (λch. part_answer 𝒢 a) (field_spec (registration_of a) 𝒢 p)"
lemma mcp_field_sound:
"sound_local_spec (declared_global p) (part_gamma (declared_global p) a)
(mcp_field (declared_global p) p a)"
unfolding mcp_field_def
by (rule with_qry_sound[OF field_spec_sound]) (rule part_answer_sound)
lemma mcp_field_frame: "a ≠ b ⟹ mcp_frame (mcp_field 𝒢 p a) (part_gamma 𝒢 b)"
unfolding mcp_field_def by (rule with_qry_frame[OF field_spec_frame])
subsection ‹The active analyses, run as one›
text ‹
The combined state is unreachable as soon as one active analysis says its
field is, as Goblint's ‹MCP› raises ‹Deadcode› when one component does. The
normalization changes no concretization: a field that describes nothing
empties the intersection already.
›
definition mcp_norm :: "analysis_domain list ⇒ mcp_st lifted ⇒ mcp_st lifted" where
"mcp_norm as x =
(case x of
Bot ⇒ Bot
| Lifted r ⇒ if list_all (λa. field_live (registration_of a) r) as then x else Bot)"
lemma part_gamma_Bot [simp]: "part_gamma 𝒢 a Bot = {}"
by (cases a rule: analysis_domain_cases) simp_all
lemma part_gamma_dead:
"¬ field_live (registration_of a) r ⟹ part_gamma 𝒢 a (Lifted r) = {}"
by (cases a rule: analysis_domain_cases) simp_all
lemma mcp_gamma_norm:
"mcp_gamma (map (part_gamma 𝒢) as) (mcp_norm as x) = mcp_gamma (map (part_gamma 𝒢) as) x"
by (cases x) (auto simp: mcp_norm_def mcp_gamma_def list_all_iff dest: part_gamma_dead)
definition mcp_comp ::
"analysis_domain list ⇒ (vname ⇒ bool) ⇒ imp_prog ⇒ mcp_st lifted local_spec" where
"mcp_comp as 𝒢 p = map_local_spec (mcp_norm as) (mcp_combine (map (mcp_field 𝒢 p) as))"
theorem mcp_comp_sound:
assumes "distinct as" and "as ≠ []"
shows "sound_local_spec (declared_global p)
(mcp_gamma (map (part_gamma (declared_global p)) as))
(mcp_comp as (declared_global p) p)"
proof -
let ?gcs = "map (λa. (part_gamma (declared_global p) a,
mcp_field (declared_global p) p a)) as"
have "sound_local_spec (declared_global p) (mcp_gamma (map fst ?gcs))
(mcp_combine (map snd ?gcs))"
by (rule mcp_combine_sound)
(auto simp: mcp_field_sound assms
intro!: mcp_independent_map mcp_field_frame)
then show ?thesis
unfolding mcp_comp_def
by (intro map_local_spec_sound) (simp_all add: comp_def mcp_gamma_norm)
qed
lemma single_entry_mcp_comp: "as ≠ [] ⟹ single_entry (mcp_comp as 𝒢 p)"
unfolding mcp_comp_def mcp_field_def
by (intro single_entry_map_local_spec single_entry_mcp_combine)
(auto simp: single_entry_field_spec single_entry_with_qry)
subsection ‹What the combined state publishes›
text ‹
A solved combined state is published field by field, each through its
analysis's own publication map. Its concretization is the intersection over the
active fields, and a check is decided from the meet of the active analyses'
answers.
›
lemma mcp_gamma_rd:
"as ≠ [] ⟹ mcp_gamma (map (part_gamma 𝒢) as) x
= gamma_lift (mcp_gamma_v as) (map_lift (mcp_rd 𝒢) x)"
by (cases x) (auto simp: mcp_gamma_def mcp_gamma_v_def part_gamma_rd)
lemma mcp_gamma_v_bot: "as ≠ [] ⟹ mcp_gamma_v as ⊥ = {}"
proof -
have "val_gamma a ⊥ = {}" for a by (cases a rule: analysis_domain_cases) simp_all
then show "as ≠ [] ⟹ ?thesis" by (auto simp: mcp_gamma_v_def)
qed
definition mcp_emp :: "analysis_domain list ⇒ imp_prog ⇒ mcp_st ⇒ bool" where
"mcp_emp as p r =
list_ex (λa. field_empty (registration_of a) (declared_global_vars p) r) as"
definition mcp_empty_v :: "analysis_domain list ⇒ mcp_val ⇒ bool" where
"mcp_empty_v as v = list_ex (λa. val_empty a v) as"
lemma field_empty_rd:
"field_empty (registration_of a) (declared_global_vars p) r
= val_empty a (mcp_rd (declared_global p) r)"
by (cases a rule: analysis_domain_cases)
(simp_all add: mcp_rd_def
default_st_is_bot_for_iff[where 𝒢 = "declared_global p", OF declared_global_iff]
split: lifted.split)
lemma mcp_emp_rd: "mcp_emp as p r = mcp_empty_v as (mcp_rd (declared_global p) r)"
by (simp add: mcp_emp_def mcp_empty_v_def field_empty_rd)
lemma val_empty_gamma: "val_empty a v ⟹ val_gamma a v = {}"
by (cases a rule: analysis_domain_cases)
(auto split: lifted.splits dest: is_empty_state_gamma_state_empty)
lemma mcp_empty_v_gamma: "mcp_empty_v as v ⟹ mcp_gamma_v as v = {}"
by (auto simp: mcp_empty_v_def mcp_gamma_v_def list_ex_iff dest: val_empty_gamma)
lemma sound_emptiness_mcp: "sound_emptiness (mcp_empty_v as) (mcp_gamma_v as)"
by (rule sound_emptinessI) (rule mcp_empty_v_gamma)
text ‹
The combined test is not exact. Interval says ‹x = 2› and Parity says ‹x› is odd:
neither field is empty, so the test does not fire, yet no store satisfies both.
›
definition mcp_contradiction :: mcp_val where
"mcp_contradiction =
set_slot3 (set_slot2 (⊥ :: mcp_val) (Lifted ((⊤ :: ivl abs_state)(STR ''x'' := Ivl (Fin 2) (Fin 2)))))
(Lifted ((⊤ :: parity abs_state)(STR ''x'' := POdd)))"
lemma mcp_contradiction_not_empty:
"¬ mcp_empty_v [Interval_Analysis, Parity_Analysis] mcp_contradiction"
proof -
have "(λ_. 2) ∈ γ ((⊤ :: ivl abs_state)(STR ''x'' := Ivl (Fin 2) (Fin 2)))"
by (auto simp: gamma_state_def top_ivl_def gamma_ivl_top)
moreover have "(λ_. 1) ∈ γ ((⊤ :: parity abs_state)(STR ''x'' := POdd))"
by (auto simp: gamma_state_def gamma_parity_top)
ultimately show ?thesis
by (auto simp: mcp_empty_v_def mcp_contradiction_def is_empty_state_iff_gamma_state_empty)
qed
lemma mcp_contradiction_no_store:
"mcp_gamma_v [Interval_Analysis, Parity_Analysis] mcp_contradiction = {}"
proof (rule equals0I)
fix s
assume "s ∈ mcp_gamma_v [Interval_Analysis, Parity_Analysis] mcp_contradiction"
then have "s (STR ''x'') ∈ gamma_ivl (Ivl (Fin 2) (Fin 2))"
and "s (STR ''x'') ∈ gamma_parity POdd"
by (auto simp: mcp_gamma_v_def mcp_contradiction_def gamma_state_def
dest: spec[of _ "STR ''x''"])
then show False by (simp, presburger)
qed
lemma mcp_empty_v_not_exact:
"¬ exact_emptiness (mcp_empty_v [Interval_Analysis, Parity_Analysis])
(mcp_gamma_v [Interval_Analysis, Parity_Analysis])"
using exact_emptinessD [of _ _ mcp_contradiction] mcp_contradiction_not_empty
mcp_contradiction_no_store
by blast
definition mcp_answer :: "analysis_domain list ⇒ mcp_val ⇒ query ⇒ answer" where
"mcp_answer as v q = fold (λa r. r ⊓ value_answer (registration_of a) v q) as ⊤"
lemma mcp_answer_fold_sound:
"∀a ∈ set as. s ∈ val_gamma a v ⟹ eval_holds q r s
⟹ eval_holds q (fold (λa r. r ⊓ value_answer (registration_of a) v q) as r) s"
by (induction as arbitrary: r) (auto intro: eval_query.inf_sound value_answer_sound)
lemma mcp_answer_sound: "s ∈ mcp_gamma_v as v ⟹ eval_holds q (mcp_answer as v q) s"
unfolding mcp_answer_def mcp_gamma_v_def by (rule mcp_answer_fold_sound) auto
definition mcp_classify :: "analysis_domain list ⇒ exp ⇒ mcp_val ⇒ check_result" where
"mcp_classify as = answer_check (mcp_answer as)"
lemma mcp_classify_proved:
"mcp_classify as e v = Check_Proved ⟹ s ∈ mcp_gamma_v as v ⟹ truthy (⟦e⟧⇩e s)"
unfolding mcp_classify_def by (erule answer_check_proved) (rule mcp_answer_sound)
lemma mcp_classify_refuted:
"mcp_classify as e v = Check_Refuted ⟹ s ∈ mcp_gamma_v as v
⟹ ¬ truthy (⟦e⟧⇩e s)"
unfolding mcp_classify_def by (erule answer_check_refuted) (rule mcp_answer_sound)
text ‹
A caller activates a distinct, nonempty list of analyses. The registrations
below take any list and run it as ‹activation› normalizes it, so they hold
unconditionally; ‹activation› is the identity on every list a caller may
pass.
›
definition activation :: "analysis_domain list ⇒ analysis_domain list" where
"activation as = (if as = [] then [Int_Analysis Refine_Fixpoint] else remdups as)"
lemma activation_ne [simp]: "activation as ≠ []"
by (simp add: activation_def)
lemma distinct_activation [simp]: "distinct (activation as)"
by (simp add: activation_def)
lemma activation_id: "distinct as ⟹ as ≠ [] ⟹ activation as = as"
by (simp add: activation_def)
section ‹Registering the active analyses›
text ‹
The active analyses run through the shared pipeline once per context
policy, as one registered analysis does. What they owe the pipeline does not
depend on the policy, beyond its seeds being apart from the analysis-wide
global, so it is proved once here. Each registration leaves the activation
list and the global update rule as parameters.
›
lemma mcp_routed_dg_analysis:
fixes buffer_key :: 'k and global_of :: "'n ⇒ 'k"
assumes seed_ne: "⋀v ctx. seed v ctx ≠ buffer_key"
and seed_ne_global: "⋀v ctx n. seed v ctx ≠ global_of n"
shows "dg_analysis (mcp_comp (activation as)) (mcp_emp (activation as)) mcp_rd
(mcp_init (activation as)) buffer_key global_of seed
(TD_side_rule_Interp_solve r)
(TD_side_rule_Interp.solve_dom TYPE('k) TYPE((mcp_st lifted, mcp_st lifted) dg_state) r)
⊥ (mcp_classify (activation as)) (mcp_gamma_v (activation as))
(mcp_empty_v (activation as)) (TD_side_rule_Interp_solve_c r)
(λ𝒢 c. dg_spec_of c) (λ𝒢 d e. d) (λ𝒢 d. d) (λ𝒢 d. Bot)
(λ𝒢 p. []) (λp ci d e. d)"
proof (rule dg_analysis_whole_stateI[OF td_certified_solver],
goal_cases CompSound EnterSingle EmptyRd EmptyVSound SeedNe ClProved ClRefuted BotState
Init SeedNeGlobal)
case (CompSound p)
have eq: "mcp_gamma (map (part_gamma (declared_global p)) (activation as))
= (λd. gamma_lift (mcp_gamma_v (activation as)) (map_lift (mcp_rd (declared_global p)) d))"
by (rule ext) (rule mcp_gamma_rd[OF activation_ne])
show ?case using mcp_comp_sound[of "activation as" p] unfolding eq by simp
next
case (EnterSingle p ci d)
show ?case
using single_entryD[OF single_entry_mcp_comp[OF activation_ne],
of as "declared_global p" p
"ls_channel (mcp_comp (activation as) (declared_global p) p) d" ci "(d, d)"]
by (simp add: dg_pipeline.comp_entry_def)
next
case (EmptyRd p s) show ?case by (rule mcp_emp_rd)
next
case EmptyVSound show ?case by (rule sound_emptiness_mcp)
next
case (SeedNe v ctx) show ?case by (rule seed_ne)
next
case (ClProved e d s) then show ?case by (rule mcp_classify_proved)
next
case (ClRefuted e d s) then show ?case by (rule mcp_classify_refuted)
next
case BotState show ?case by (rule mcp_gamma_v_bot[OF activation_ne])
next
case (Init p) show ?case by (rule mcp_init_sound)
next
case (SeedNeGlobal v ctx n) show ?case by (rule seed_ne_global)
qed
subsection ‹At the unit context›
text ‹
‹mcp_rule›: the analysis with one context ‹()›, routed by ‹route_unit›. Each
registration names a solver key per program global, which this placement
never publishes at: every global lives in a point's own state.
›