Theory Interval_Transfer
theory Interval_Transfer
imports
Interval_Special
"Voblint_Nonrelational.Nonrelational_Transfer"
begin
section ‹What each kind of CFG edge does to an interval store›
text ‹
An interval store gives every variable a lower and an upper bound. How an edge
of a compiled graph moves such a store is not an Interval 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 to \<^const>‹ivl_top› and binds the formals, and skip,
body entry and check observation leave the store alone. That is
\<^locale>‹sound_nonrelational_ops›, proved sound and monotone once for every
domain that gives one abstract value per variable.
What is Interval's own are the primitive choices. ‹ivl_ops› collects the
evaluator, the bound-comparison queries, \<^const>‹ivl_refine_ops› --- whose
comparison inverses make ‹x < 8› tighten ‹x›'s upper bound --- the special
calls, and \<^const>‹ivl_top›. 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_ivl›,
Interval's own ‹fun›, rather than introducing a second name for it.
›
lemma interval_check_domain:
"sound_check_query interval_less interval_eq gamma_state aval_ivl"
by unfold_locales (rule ivl_arith.aval_abs_sound)
definition ivl_ops :: "ivl nonrelational_ops" where
"ivl_ops = ⦇ n_aval = aval_ivl, n_query = ⦇q_less = interval_less, q_eq = interval_eq⦈,
n_refine = ivl_refine_ops, n_special = ivl_special_ops ⦈"
lemma ivl_ops_simps [simp]:
"n_aval ivl_ops = aval_ivl"
"q_less (n_query ivl_ops) = interval_less"
"q_eq (n_query ivl_ops) = interval_eq"
"n_refine ivl_ops = ivl_refine_ops"
"n_special ivl_ops = ivl_special_ops"
by (simp_all add: ivl_ops_def)