Theory Voblint_Analysis_Parity.Parity_Transfer
theory Parity_Transfer
imports
Parity_Backward
Parity_Special
Parity_Numeric_Queries
"Voblint_Nonrelational.Nonrelational_Transfer"
begin
section ‹What each kind of CFG edge does to a parity store›
text ‹
A parity store records, for each variable, whether it is even, odd, either
(\<^const>‹PTop›) or unreachable (\<^const>‹PBot›). How an edge of a compiled graph
moves such a store is not a Parity question --- an assignment re-evaluates its
right-hand side and overwrites the target, a guard runs the backward branch, a
return writes into the return variable, procedure entry resets the callee frame
and binds the formals --- so it is \<^locale>‹sound_nonrelational_ops› that says
it, once, for every domain that gives one abstract value per variable.
What is Parity's own are the primitive choices. ‹parity_ops› collects the
evaluator, the comparison queries, \<^const>‹parity_refine_ops› --- whose
inverses let ‹x + 1 == y› with ‹y› even make ‹x› odd --- the special calls, and
\<^const>‹PTop›. The one interpretation below derives the guard filters, the
branch, the check classifier and the transfer from that bundle, and rewrites the
locale's special-call dispatch to \<^const>‹special_parity›, Parity's own ‹fun›,
rather than introducing a second name for it.
›
lemma parity_check_domain: "sound_check_query parity_less parity_eq gamma_state aval_parity"
by unfold_locales (rule parity_arith.aval_abs_sound)
definition parity_ops :: "parity nonrelational_ops" where
"parity_ops = ⦇ n_aval = aval_parity, n_query = ⦇q_less = parity_less, q_eq = parity_eq⦈,
n_refine = parity_refine_ops, n_special = parity_special_ops ⦈"
lemma parity_ops_simps [simp]:
"n_aval parity_ops = aval_parity"
"q_less (n_query parity_ops) = parity_less"
"q_eq (n_query parity_ops) = parity_eq"
"n_refine parity_ops = parity_refine_ops"
"n_special parity_ops = parity_special_ops"
by (simp_all add: parity_ops_def)