Theory Backward_Domain
theory Backward_Domain
imports Nonrelational_Reachability Forward_Domain
begin
section ‹Refining an abstract state against a guard›
text ‹
A forward transfer over-approximates what an assignment does; a backward one narrows a
state against a condition that is known to hold, which is what a branch on ‹b› learns
about the stores that pass it. ‹sound_refinement› is the interface a domain
supplies for that: inverse operators for arithmetic and comparison (‹inv_less›,
‹inv_plus›, ...), each sound in the sense that every concrete pair the operator
admits before the operation is still admitted after narrowing, from which ‹afilter›
and ‹bfilter› -- the expression- and boolean-level filters -- are derived once with
their soundness and reductiveness. ‹mono_refinement› adds the
monotone operators a domain can provide on top.
This abstracts the backward-refinement operations Goblint's ‹BaseInvariant› implements
concretely for its Base analysis; Goblint has no generic module signature this locale
is a formalization of.
›
subsection ‹Backward-analysis locale›
text ‹
A semantic intersection preserves every concrete value shared by both
operands and lies below both. It need not be the lattice infimum: a domain
may normalize an empty result while its representation order still
distinguishes several empty elements. Soundness of the filters needs only
‹intersect_sound›. The lower bounds make every refinement step reductive,
so a state emptied by one step stays empty through the rest, which is what
lets the executable filter stop at the first empty step
(‹Exec_Backward›). Every domain's intersection has both, so they form one
contract; ‹mono_intersection› adds monotonicity as a separate
strengthening.
›
locale sound_intersection =
fixes intersect :: "'a::numeric_domain => 'a => 'a"
assumes intersect_sound[intro]:
"n ∈ γ a ⟹ n ∈ γ b ⟹ n ∈ γ (intersect a b)"
and intersect_reductive1[intro]: "intersect a b ≤ a"
and intersect_reductive2[intro]: "intersect a b ≤ b"
text ‹
Monotone intersection is a separate layer for the same reason as in the forward
interfaces: soundness needs only ‹sound_intersection›, while the solver's
least-solution theorem asks ‹intersect› to preserve the order in both arguments.
›
locale mono_intersection = sound_intersection +
assumes intersect_mono[intro]:
"a1 ≤ a2 ⟹ b1 ≤ b2 ⟹ intersect a1 b1 ≤ intersect a2 b2"
text ‹
The inverse operators work on abstract values alone: given the result an
operation must have produced, each narrows its operands to values that still
admit every concrete pair producing it. ‹sound_inverse_ops› states them and their
soundness with no state in sight, which is all the derived numeric queries
(‹Backward_Numeric_Queries›) read.
›
locale sound_inverse_ops = sound_intersection intersect
for intersect :: "'a::numeric_domain => 'a => 'a" +
fixes
inv_less :: "bool => 'a => 'a => 'a * 'a"
and inv_eq :: "bool => 'a => 'a => 'a * 'a"
and inv_plus :: "'a => 'a => 'a => 'a * 'a"
and inv_minus :: "'a => 'a => 'a => 'a * 'a"
and inv_times :: "'a => 'a => 'a => 'a * 'a"
assumes
inv_less_sound:
"n1 ∈ γ a1 ⟹ n2 ∈ γ a2 ⟹ (n1 < n2) = res
⟹ n1 ∈ γ (fst (inv_less res a1 a2)) ∧ n2 ∈ γ (snd (inv_less res a1 a2))"
and inv_eq_sound:
"n1 ∈ γ a1 ⟹ n2 ∈ γ a2 ⟹ (n1 = n2) = res
⟹ n1 ∈ γ (fst (inv_eq res a1 a2)) ∧ n2 ∈ γ (snd (inv_eq res a1 a2))"
and inv_plus_sound:
"n1 ∈ γ a1 ⟹ n2 ∈ γ a2 ⟹ n1 + n2 ∈ γ r
⟹ n1 ∈ γ (fst (inv_plus r a1 a2)) ∧ n2 ∈ γ (snd (inv_plus r a1 a2))"
and inv_minus_sound:
"n1 ∈ γ a1 ⟹ n2 ∈ γ a2 ⟹ n1 - n2 ∈ γ r
⟹ n1 ∈ γ (fst (inv_minus r a1 a2)) ∧ n2 ∈ γ (snd (inv_minus r a1 a2))"
and inv_times_sound:
"n1 ∈ γ a1 ⟹ n2 ∈ γ a2 ⟹ n1 * n2 ∈ γ r
⟹ n1 ∈ γ (fst (inv_times r a1 a2)) ∧ n2 ∈ γ (snd (inv_times r a1 a2))"
begin
text ‹
Projections of the five ‹inv_*_sound› assumptions above, one membership
fact per operand instead of the pair conjunction the raw assumption gives.
These, not the raw assumptions, are the ‹[intro]› rules: their conclusion
has a distinctive ‹fst (inv_* ...)›/‹snd (inv_* ...)› head, so a goal of
exactly that shape picks the matching rule directly, whereas the raw
conjunction-valued assumption would leave automation to split a conjunction
goal it did not ask for.
›
lemmas inv_less_sound_fst [intro] = inv_less_sound[THEN conjunct1]
lemmas inv_less_sound_snd [intro] = inv_less_sound[THEN conjunct2]
lemmas inv_eq_sound_fst [intro] = inv_eq_sound[THEN conjunct1]
lemmas inv_eq_sound_snd [intro] = inv_eq_sound[THEN conjunct2]
lemmas inv_plus_sound_fst [intro] = inv_plus_sound[THEN conjunct1]
lemmas inv_plus_sound_snd [intro] = inv_plus_sound[THEN conjunct2]
lemmas inv_minus_sound_fst [intro] = inv_minus_sound[THEN conjunct1]
lemmas inv_minus_sound_snd [intro] = inv_minus_sound[THEN conjunct2]
lemmas inv_times_sound_fst [intro] = inv_times_sound[THEN conjunct1]
lemmas inv_times_sound_snd [intro] = inv_times_sound[THEN conjunct2]
end
text ‹
‹sound_refinement› takes the inverse operators to pointwise states. With the
forward operations of @{locale sound_evaluator} and @{locale sound_truth_test}
it derives the guard filters ‹afilter› and ‹bfilter›, whose soundness
follows by induction. A domain that already interpreted the forward locales
(through its expression domain) is not asked for their laws again.
›
locale sound_refinement =
sound_intersection intersect + sound_evaluator gamma_state aval_abs
+ sound_truth_test tobool
+ sound_inverse_ops intersect inv_less inv_eq inv_plus inv_minus inv_times
for intersect :: "'a::numeric_domain => 'a => 'a"
and aval_abs :: "exp => 'a abs_state => 'a" ("⟦_⟧⇧♯")
and tobool :: "'a => bool option"
and inv_less :: "bool => 'a => 'a => 'a * 'a"
and inv_eq :: "bool => 'a => 'a => 'a * 'a"
and inv_plus :: "'a => 'a => 'a => 'a * 'a"
and inv_minus :: "'a => 'a => 'a => 'a * 'a"
and inv_times :: "'a => 'a => 'a => 'a * 'a"
begin
fun afilter :: "exp => 'a => 'a abs_state => 'a abs_state" where
"afilter (V x) a d = d(x := intersect a (d x))"
| "afilter (Plus e1 e2) a d =
(let (a1, a2) = inv_plus a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "afilter (Minus e1 e2) a d =
(let (a1, a2) = inv_minus a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "afilter (Times e1 e2) a d =
(let (a1, a2) = inv_times a (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "afilter _ a d = d"
text ‹
‹feasible› is the forward half of Goblint's two-phase branch handling, as a
predicate: evaluate ‹e› forward and ask whether the abstract value that
yields leaves the selected polarity possible at all. A bottom value denotes
no store, and a definite ‹tobool› answer disagreeing with ‹pol› rules the
polarity out; every other case keeps it open. Backward narrowing cannot
replace this test: a Boolean-valued subexpression in an operand position
inverts to a target ‹afilter› has no rule to push through a comparison node,
so the target is dropped and the state survives unrefined even where no state
satisfies the condition.
The leading ‹is_empty› test is not redundant with the ‹tobool› one. An
author's ‹tobool› is free to answer arbitrarily at its own domain's bottom
(every answer is vacuously sound there, since ‹gamma bot = {}›), so it need
not, and generally does not, agree across a bottom/non-bottom pair
‹d1 ≤ d2› the way ‹tobool_mono› requires. Answering ‹is_empty› directly,
ahead of ‹tobool›, sidesteps that disagreement instead of relying on it, and
is what makes ‹feasible_mono› hold.
›
definition feasible :: "exp => bool => 'a abs_state => bool" where
"feasible e pol d =
(¬ is_empty (⟦e⟧⇧♯ d) ∧ tobool (⟦e⟧⇧♯ d) ≠ Some (¬ pol))"
text ‹
Every state a concrete store witnesses is feasible for the polarity that
store takes: ‹aval_abs_sound› rules out the bottom case and ‹tobool_sound›
the disagreeing-answer case. This is what makes the gate's ‹bot› outcome
sound wherever it fires -- it fires only when no represented store exists.
›
lemma feasible_of_concrete [intro]:
assumes "s ∈ γ d" and "truthy (⟦e⟧⇩e s) = pol"
shows "feasible e pol d"
unfolding feasible_def using assms is_empty_correct tobool_sound by blast
text ‹
‹bfilter› narrows a state under an assumed truth value of ‹e›: ‹bfilter e
True› is ‹assume e›, ‹bfilter e False› is ‹assume-not e›. ‹Not›/‹And›/‹Or›
distribute structurally (De Morgan, over ‹⊔› for the disjunctive branch);
‹Less›/‹Eq› go straight through ‹inv_less›/‹inv_eq› on their two operands.
Every other constructor -- ‹N›, ‹V›, ‹Plus›, ‹Minus›, ‹Times› -- has no
Boolean-shaped narrowing operator of its own, so the fallback case reduces
truthiness to the one comparison every domain already inverts: ‹truthy
(⟦e⟧⇩e s) = res› iff ‹(⟦e⟧⇩e s = 0) = (¬ res)›, so ‹inv_eq (¬ res)›
against the abstract constant ‹0› narrows ‹e›'s own target value, and
‹afilter› propagates that target through ‹e›'s structure. This reuses
‹inv_eq›/‹afilter› rather than adding a new domain-author operator.
The two disjunctive cases -- ‹Or _ _ True› and ‹And _ _ False› -- gate each
side on ‹feasible› before joining, matching Goblint's ‹inv_exp›, which
refines the arms of a disjunction separately and drops one whose refinement
contradicts. Without the gate, a side no state satisfies still contributes
its own unrefined incoming state and the join discards what the other side
established: the empty target such a side inverts to is dropped wherever
‹afilter› has no rule for the node carrying it, so the narrowing that would
have signalled the contradiction never happens. ‹bot› is the unit of ‹⊔›,
so gating an infeasible side removes it from the join exactly.
‹feasible› is only a necessary forward gate, though: a side it approves can
still have its own ‹bfilter› recursion discover a stronger, backward-only
contradiction, landing on a witness-bottom state (@{const is_empty_state})
that need not be the literal pointwise ‹bot› -- e.g. empty at the one
location the side's own condition constrains, but still carrying whatever
‹d› already held everywhere else. Joining that raw state ∗‹pointwise›
then contributes those other, unrefined locations to the join exactly as if
the side were live, silently discarding what the other side established
there. Canonicalizing each gated side before the join (collapsing a
witness-bottom side to the literal ‹bot›, the unit of ‹⊔›) would close this,
but @{const is_empty_state} has no code equation over an infinite ‹vname›
domain, and embedding it inside ‹bfilter›'s own primitive-recursive
equations would make the whole function -- every constructor, not only
‹And›/‹Or› -- lose code-generatability with it. ‹bfilter› therefore stays
exactly this pointwise join, and the correction lives one level up, in
‹bfilter_lifted›, which does not need to code-generate.
›
fun bfilter :: "exp => bool => 'a abs_state => 'a abs_state" where
"bfilter (Less e1 e2) res d =
(let (a1, a2) = inv_less res (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "bfilter (GreaterEq e1 e2) res d =
(let (a1, a2) = inv_less (¬ res) (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "bfilter (Greater e1 e2) res d =
(let (a1, a2) = inv_less res (⟦e2⟧⇧♯ d) (⟦e1⟧⇧♯ d)
in afilter e2 a1 (afilter e1 a2 d))"
| "bfilter (LessEq e1 e2) res d =
(let (a1, a2) = inv_less (¬ res) (⟦e2⟧⇧♯ d) (⟦e1⟧⇧♯ d)
in afilter e2 a1 (afilter e1 a2 d))"
| "bfilter (Not b) res d = bfilter b (¬ res) d"
| "bfilter (And b1 b2) True d = bfilter b1 True (bfilter b2 True d)"
| "bfilter (And b1 b2) False d =
(if feasible b1 False d then bfilter b1 False d else bot)
⊔ (if feasible b2 False d then bfilter b2 False d else bot)"
| "bfilter (Or b1 b2) True d =
(if feasible b1 True d then bfilter b1 True d else bot)
⊔ (if feasible b2 True d then bfilter b2 True d else bot)"
| "bfilter (Or b1 b2) False d = bfilter b1 False (bfilter b2 False d)"
| "bfilter (Eq e1 e2) res d =
(let (a1, a2) = inv_eq res (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "bfilter (NotEq e1 e2) res d =
(let (a1, a2) = inv_eq (¬ res) (⟦e1⟧⇧♯ d) (⟦e2⟧⇧♯ d)
in afilter e1 a1 (afilter e2 a2 d))"
| "bfilter e res d =
(let (a1, a2) = inv_eq (¬ res) (⟦e⟧⇧♯ d) (⟦N 0⟧⇧♯ d)
in afilter e a1 d)"
text ‹
The state-level fact behind ‹afilter›'s ‹V› case: narrowing one location
by ‹intersect› keeps every location represented, the narrowed one because
‹intersect_sound› says so and every other because it is untouched. Named
once here so ‹afilter_sound›'s ‹V› case cites it instead of unfolding
‹gamma_state_def› and case-splitting on ‹y = x› inline.
›
lemma gamma_state_update_intersect [intro]:
assumes "s ∈ γ d" and "s x ∈ γ a"
shows "s ∈ γ (d(x := intersect a (d x)))"
using assms by (simp add: gamma_stateD gamma_stateI intersect_sound)
lemma afilter_sound [intro]:
assumes "s ∈ γ d" "⟦e⟧⇩e s ∈ γ a"
shows "s ∈ γ (afilter e a d)"
using assms proof (induction e arbitrary: a d)
case (V x)
then show ?case
unfolding afilter.simps aval.simps by (rule gamma_state_update_intersect)
next
case (Plus e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF Plus.prems(1)] by simp_all
have asum: "⟦e1⟧⇩e s + ⟦e2⟧⇩e s ∈ γ a" using Plus.prems(2) by simp
show ?case
unfolding afilter.simps Let_def case_prod_beta
using e1a e2a asum Plus.prems(1)
by (blast intro: Plus.IH)
next
case (Minus e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF Minus.prems(1)] by simp_all
have adiff: "⟦e1⟧⇩e s - ⟦e2⟧⇩e s ∈ γ a" using Minus.prems(2) by simp
show ?case
unfolding afilter.simps Let_def case_prod_beta
using e1a e2a adiff Minus.prems(1)
by (blast intro: Minus.IH)
next
case (Times e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF Times.prems(1)] by simp_all
have aprod: "⟦e1⟧⇩e s * ⟦e2⟧⇩e s ∈ γ a" using Times.prems(2) by simp
show ?case
unfolding afilter.simps Let_def case_prod_beta
using e1a e2a aprod Times.prems(1)
by (blast intro: Times.IH)
qed simp_all
text ‹
The two-operand filtering step ‹Less›/‹Eq› each apply once ‹inv_less›/
‹inv_eq› has narrowed their operand pair: filter the second operand by
its narrowed target, then the first by its narrowed target against the
result. Stated generically here, using the completed ‹afilter_sound›
rather than an induction hypothesis, so ‹bfilter_sound›'s own ‹Less›/‹Eq›
cases apply it directly instead of repeating this chaining.
›
lemma afilter_pair_sound [intro]:
assumes st: "s ∈ γ d"
and fst: "⟦e1⟧⇩e s ∈ γ (fst p)"
and snd: "⟦e2⟧⇩e s ∈ γ (snd p)"
shows "s ∈ γ (afilter e1 (fst p) (afilter e2 (snd p) d))"
proof -
have inner: "s ∈ γ (afilter e2 (snd p) d)" by (rule afilter_sound[OF st snd])
show ?thesis by (rule afilter_sound[OF inner fst])
qed
text ‹
Every constructor without its own Boolean-shaped narrowing operator --
‹N›, ‹V›, ‹Plus›, ‹Minus›, ‹Times› -- reduces ‹bfilter›'s target truth
value to an ‹inv_eq› narrowing against the abstract constant ‹0› (see
‹bfilter›'s own comment), then propagates the narrowed target through
‹afilter›. Proved once here, generically in ‹e›, so the induction below
cites it instead of repeating the same ‹inv_eq›/‹afilter_sound› chain per
arithmetic constructor.
›
lemma bfilter_default_sound:
assumes "s ∈ γ d" "truthy (⟦e⟧⇩e s) = res"
shows "s ∈ γ (afilter e (fst (inv_eq (¬ res) (⟦e⟧⇧♯ d) (⟦N 0⟧⇧♯ d))) d)"
proof -
have ea: "⟦e⟧⇩e s ∈ γ (⟦e⟧⇧♯ d)"
using aval_abs_sound[OF assms(1)] by simp
have e0: "⟦N 0⟧⇩e s ∈ γ (⟦N 0⟧⇧♯ d)"
by (rule aval_abs_sound[of s d "N 0", OF assms(1)])
have eq0: "(⟦e⟧⇩e s = ⟦N 0⟧⇩e s) = (¬ res)"
using assms(2) by auto
have "⟦e⟧⇩e s ∈ γ (fst (inv_eq (¬ res) (⟦e⟧⇧♯ d) (⟦N 0⟧⇧♯ d)))"
using inv_eq_sound[OF ea e0 eq0] by simp
then show ?thesis using afilter_sound[OF assms(1)]
by simp
qed
text ‹
Soundness of a feasibility-gated join, the shape of ‹bfilter›'s
‹And _ _ False› and ‹Or _ _ True› cases: a store taking the polarity on
one side makes that side feasible, so the gate keeps it and the join
admits the store through it.
›
lemma gated_join_sound:
fixes f1 f2 :: "'a abs_state"
assumes st: "s ∈ γ d"
and "truthy (⟦b1⟧⇩e s) = pol ∨ truthy (⟦b2⟧⇩e s) = pol"
and f1: "truthy (⟦b1⟧⇩e s) = pol ⟹ s ∈ γ f1"
and f2: "truthy (⟦b2⟧⇩e s) = pol ⟹ s ∈ γ f2"
shows "s ∈ γ ((if feasible b1 pol d then f1 else bot)
⊔ (if feasible b2 pol d then f2 else bot))"
using assms(2)
proof
assume h: "truthy (⟦b1⟧⇩e s) = pol"
have "feasible b1 pol d" by (rule feasible_of_concrete[OF st h])
with f1[OF h] show ?thesis by (simp add: gamma_state_supI1)
next
assume h: "truthy (⟦b2⟧⇩e s) = pol"
have "feasible b2 pol d" by (rule feasible_of_concrete[OF st h])
with f2[OF h] show ?thesis by (simp add: gamma_state_supI2)
qed
lemma bfilter_sound [intro]:
assumes "s ∈ γ d" "truthy (⟦e⟧⇩e s) = res"
shows "s ∈ γ (bfilter e res d)"
using assms proof (induction e arbitrary: res d)
case (Not e)
have bv': "truthy (⟦e⟧⇩e s) = (¬ res)" using Not.prems(2) by (auto split: if_splits)
from Not.IH[OF Not.prems(1) bv'] show ?case by simp
next
case (And e1 e2)
show ?case
proof (cases res)
case True
have v1: "truthy (⟦e1⟧⇩e s) = True" and v2: "truthy (⟦e2⟧⇩e s) = True"
using And.prems(2) True unfolding truthy_aval_And by simp_all
show ?thesis
using And.IH(1)[OF And.IH(2)[OF And.prems(1) v2] v1] by (simp add: True)
next
case False
then have res: "res = False" by simp
have "truthy (⟦e1⟧⇩e s) = False ∨ truthy (⟦e2⟧⇩e s) = False"
using And.prems(2) res by (auto split: if_splits)
then show ?thesis
unfolding res bfilter.simps
by (rule gated_join_sound[OF And.prems(1) _ And.IH[OF And.prems(1)]])
qed
next
case (Or e1 e2)
show ?case
proof (cases res)
case True
then have res: "res = True" by simp
have "truthy (⟦e1⟧⇩e s) = True ∨ truthy (⟦e2⟧⇩e s) = True"
using Or.prems(2) res by auto
then show ?thesis
unfolding res bfilter.simps
by (rule gated_join_sound[OF Or.prems(1) _ Or.IH[OF Or.prems(1)]])
next
case False
have v1: "truthy (⟦e1⟧⇩e s) = False" and v2: "truthy (⟦e2⟧⇩e s) = False"
using Or.prems(2) False unfolding truthy_aval_Or by simp_all
show ?thesis
using Or.IH(1)[OF Or.IH(2)[OF Or.prems(1) v2] v1] by (simp add: False)
qed
next
case (Less e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF Less.prems(1)] by simp_all
have less: "(⟦e1⟧⇩e s < ⟦e2⟧⇩e s) = res" using Less.prems(2) by (auto split: if_splits)
show ?case
unfolding bfilter.simps Let_def case_prod_beta
by (blast intro: Less.prems(1) inv_less_sound_fst[OF e1a e2a less]
inv_less_sound_snd[OF e1a e2a less])
next
case (GreaterEq e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF GreaterEq.prems(1)] by simp_all
have less: "(⟦e1⟧⇩e s < ⟦e2⟧⇩e s) = (¬ res)" using GreaterEq.prems(2) by (auto split: if_splits)
show ?case
unfolding bfilter.simps Let_def case_prod_beta
by (blast intro: GreaterEq.prems(1) inv_less_sound_fst[OF e1a e2a less]
inv_less_sound_snd[OF e1a e2a less])
next
case (Greater e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF Greater.prems(1)] by simp_all
have less: "(⟦e2⟧⇩e s < ⟦e1⟧⇩e s) = res" using Greater.prems(2) by (auto split: if_splits)
show ?case
unfolding bfilter.simps Let_def case_prod_beta
by (blast intro: Greater.prems(1) inv_less_sound_fst[OF e2a e1a less]
inv_less_sound_snd[OF e2a e1a less])
next
case (LessEq e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF LessEq.prems(1)] by simp_all
have less: "(⟦e2⟧⇩e s < ⟦e1⟧⇩e s) = (¬ res)" using LessEq.prems(2) by (auto split: if_splits)
show ?case
unfolding bfilter.simps Let_def case_prod_beta
by (blast intro: LessEq.prems(1) inv_less_sound_fst[OF e2a e1a less]
inv_less_sound_snd[OF e2a e1a less])
next
case (Eq e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF Eq.prems(1)] by simp_all
have eq: "(⟦e1⟧⇩e s = ⟦e2⟧⇩e s) = res" using Eq.prems(2) by (auto split: if_splits)
show ?case
unfolding bfilter.simps Let_def case_prod_beta
by (blast intro: Eq.prems(1) inv_eq_sound_fst[OF e1a e2a eq] inv_eq_sound_snd[OF e1a e2a eq])
next
case (NotEq e1 e2)
have e1a: "⟦e1⟧⇩e s ∈ γ (⟦e1⟧⇧♯ d)" and e2a: "⟦e2⟧⇩e s ∈ γ (⟦e2⟧⇧♯ d)"
using aval_abs_sound[OF NotEq.prems(1)] by simp_all
have eq: "(⟦e1⟧⇩e s = ⟦e2⟧⇩e s) = (¬ res)" using NotEq.prems(2) by (auto split: if_splits)
show ?case
unfolding bfilter.simps Let_def case_prod_beta
by (blast intro: NotEq.prems(1) inv_eq_sound_fst[OF e1a e2a eq] inv_eq_sound_snd[OF e1a e2a eq])
qed (simp_all only: bfilter.simps Let_def case_prod_beta bfilter_default_sound)
text ‹
‹branch_lifted› is the Goblint-aligned branch semantics: the forward
‹feasible› gate on the whole condition ahead of ‹bfilter›, matching
‹Base.branch›'s ‹eval_rv› / ‹to_bool› dead-code gate ahead of ‹invariant›.
An infeasible condition denotes ‹Bot› -- no concrete successor, matching
Goblint's ‹Deadcode› as an outer control-flow fact rather than a value of the
domain -- while every other case narrows via ‹bfilter› and returns
‹Lifted›. ‹tobool›'s definite answer, when present, is exactly ‹truthy› of
every concrete value ‹aval_abs e d› represents; ‹truthy (⟦e⟧⇩e s) = pol›
for a represented ‹s› then forces that answer to equal ‹pol›, so the ‹Bot›
case below is exercised only when no represented ‹s› exists at all.
It is the same gate ‹bfilter› applies per disjunct inside its two join cases,
here run on the whole condition -- which is what makes it a control-flow fact
rather than a narrowing.
A feasible condition's ‹bfilter› narrowing can itself still land on a
witness-bottom store (@{const is_empty_state}, without being the raw
‹Lifted›'s structural ‹Bot›): ‹feasible› is only a necessary forward gate,
and ‹bfilter›'s backward narrowing may subsequently discover a stronger
contradiction. ‹branch_lifted› therefore re-normalizes ‹bfilter›'s result
against ‹is_empty_state› (\<^const>‹normalize_lift›), matching Goblint's
‹BaseInvariant› raising ‹Deadcode› when its own refinement reaches bottom:
‹branch_lifted› is always \<^const>‹normalized_lift›
(‹branch_lifted_normalized›), so a caller can rely on structural ‹Bot›
alone rather than re-testing ‹is_empty_state› on a ‹Lifted› result.
›
text ‹
‹bfilter_lifted› is not ‹bfilter›'s wrapper: a wrapper can only test the
∗‹whole› recursion's final result for emptiness, one collapse after every
arm has already been joined pointwise, so it cannot undo pollution already
baked into that pointwise result -- the failure mode documented at
‹bfilter›'s own ‹And›/‹Or› equations. ‹bfilter_lifted› is instead an
independent primitive recursion, structurally mirroring ‹bfilter› one
constructor at a time, that canonicalizes each ‹And›/‹Or› arm (\<^const>‹Bot›
on an infeasible or witness-bottom side, the join's own identity) ∗‹before›
joining, at the ‹lifted› level, exactly where ‹bfilter› itself cannot
afford to: @{const is_empty_state} has no code equation, so embedding it in
‹bfilter›'s own equations would carry that non-executability to every
constructor, whereas ‹bfilter_lifted› is never code-generated. Every atomic
case (‹afilter›'s pointwise update has no pollution to fix) still reduces
to plain ‹bfilter›, so the two recursions agree everywhere they overlap and
cannot silently drift on those shared cases; all Boolean structure --
‹Not›, and both polarities of ‹And›/‹Or› -- is instead interpreted
recursively in the ‹lifted› carrier: ‹Not› just flips polarity and
recurses, the non-join polarity chains through \<^const>‹bind_lift› to
propagate an arm's ‹Bot› immediately, and the two join equations are the
deliberately independent pollution fix.
›
fun bfilter_lifted :: "exp => bool => 'a abs_state => 'a abs_state lifted" where
"bfilter_lifted (Not b) res d = bfilter_lifted b (¬ res) d"
| "bfilter_lifted (And b1 b2) True d =
bind (bfilter_lifted b2 True d) (bfilter_lifted b1 True)"
| "bfilter_lifted (And b1 b2) False d =
(if feasible b1 False d then bfilter_lifted b1 False d else Bot)
⊔ (if feasible b2 False d then bfilter_lifted b2 False d else Bot)"
| "bfilter_lifted (Or b1 b2) True d =
(if feasible b1 True d then bfilter_lifted b1 True d else Bot)
⊔ (if feasible b2 True d then bfilter_lifted b2 True d else Bot)"
| "bfilter_lifted (Or b1 b2) False d =
bind (bfilter_lifted b2 False d) (bfilter_lifted b1 False)"
| "bfilter_lifted (Eq e1 e2) res d = normalize_lift is_empty_state (bfilter (Eq e1 e2) res d)"
| "bfilter_lifted e res d = normalize_lift is_empty_state (bfilter e res d)"
lemma bfilter_lifted_normalized [simp]:
"normalized_lift is_empty_state (bfilter_lifted e pol d)"
proof (induction e arbitrary: pol d)
case (And b1 b2)
then show ?case
by (cases pol) (auto intro: normalized_lift_bind)
next
case (Or b1 b2)
then show ?case
by (cases pol) (auto intro: normalized_lift_bind)
qed simp_all
text ‹‹gated_join_sound› for ‹bfilter_lifted›'s join cases, against \<^const>‹Bot›.›
lemma gated_join_lifted_sound:
assumes st: "s ∈ γ d"
and "truthy (⟦b1⟧⇩e s) = pol ∨ truthy (⟦b2⟧⇩e s) = pol"
and f1: "truthy (⟦b1⟧⇩e s) = pol ⟹ s ∈ γ⇩⊥ f1"
and f2: "truthy (⟦b2⟧⇩e s) = pol ⟹ s ∈ γ⇩⊥ f2"
shows
"s ∈ γ⇩⊥ ((if feasible b1 pol d then f1 else Bot) ⊔ (if feasible b2 pol d then f2 else Bot))"
using assms(2)
proof
assume h: "truthy (⟦b1⟧⇩e s) = pol"
have "feasible b1 pol d" by (rule feasible_of_concrete[OF st h])
with f1[OF h] show ?thesis by (simp add: gamma_state_lift_supI1)
next
assume h: "truthy (⟦b2⟧⇩e s) = pol"
have "feasible b2 pol d" by (rule feasible_of_concrete[OF st h])
with f2[OF h] show ?thesis by (simp add: gamma_state_lift_supI2)
qed
lemma bfilter_lifted_sound [intro]:
assumes "s ∈ γ d" "truthy (⟦e⟧⇩e s) = res"
shows "s ∈ γ⇩⊥ (bfilter_lifted e res d)"
using assms proof (induction e arbitrary: res d)
case (Not e)
have bv': "truthy (⟦e⟧⇩e s) = (¬ res)" using Not.prems(2) by (auto split: if_splits)
from Not.IH[OF Not.prems(1) bv'] show ?case by simp
next
case (And e1 e2)
show ?case
proof (cases res)
case True
have v1: "truthy (⟦e1⟧⇩e s) = True" and v2: "truthy (⟦e2⟧⇩e s) = True"
using And.prems(2) True unfolding truthy_aval_And by simp_all
have h2: "s ∈ γ⇩⊥ (bfilter_lifted e2 True d)"
using And.IH(2)[OF And.prems(1) v2] .
have res_eq: "res = True" using True by simp
show ?thesis
unfolding res_eq bfilter_lifted.simps
using h2 v1 by (blast intro: And.IH(1))
next
case False
have "truthy (⟦e1⟧⇩e s) = False ∨ truthy (⟦e2⟧⇩e s) = False"
using And.prems(2) False by (auto split: if_splits)
from gated_join_lifted_sound[OF And.prems(1) this And.IH[OF And.prems(1)]] False
show ?thesis by (simp split del: if_split)
qed
next
case (Or e1 e2)
show ?case
proof (cases res)
case True
have "truthy (⟦e1⟧⇩e s) = True ∨ truthy (⟦e2⟧⇩e s) = True"
using Or.prems(2) True by auto
from gated_join_lifted_sound[OF Or.prems(1) this Or.IH[OF Or.prems(1)]] True
show ?thesis by (simp split del: if_split)
next
case False
have v1: "truthy (⟦e1⟧⇩e s) = False" and v2: "truthy (⟦e2⟧⇩e s) = False"
using Or.prems(2) False unfolding truthy_aval_Or by simp_all
have h2: "s ∈ γ⇩⊥ (bfilter_lifted e2 False d)"
using Or.IH(2)[OF Or.prems(1) v2] .
have res_eq: "res = False" using False by simp
show ?thesis
unfolding res_eq bfilter_lifted.simps
using h2 v1 by (blast intro: Or.IH(1))
qed
qed (simp_all only: bfilter_lifted.simps gamma_state_normalize_lift bfilter_sound)
text ‹
‹branch_lifted› is ‹branch›'s reachability wrapper, now routed through
‹bfilter_lifted› rather than raw ‹bfilter›: the top-level ‹feasible› gate is
unchanged (that is ‹branch›'s own concern, not the ‹And›/‹Or› pollution
‹bfilter_lifted› fixes), but the filtering it gates is the corrected
recursion, so ‹branch_lifted› inherits the improved precision without
restating it.
›
definition branch_lifted :: "exp => bool => 'a abs_state => 'a abs_state lifted" where
"branch_lifted e pol d = (if feasible e pol d then bfilter_lifted e pol d else Bot)"
lemma branch_lifted_normalized [simp]:
"normalized_lift is_empty_state (branch_lifted e pol d)"
unfolding branch_lifted_def by simp
lemma branch_lifted_sound [intro]:
assumes "s ∈ γ d" "truthy (⟦e⟧⇩e s) = pol"
shows "s ∈ γ⇩⊥ (branch_lifted e pol d)"
proof -
have g: "feasible e pol d" by (rule feasible_of_concrete[OF assms])
have "s ∈ γ⇩⊥ (bfilter_lifted e pol d)" by (rule bfilter_lifted_sound[OF assms])
with g show ?thesis unfolding branch_lifted_def by simp
qed
text ‹
A domain's branch operation has no room for ‹lifted›: it is one
plain-state-to-plain-state operation among several, dispatched uniformly by
the edge-action dispatcher with no ‹Bot›/‹Lifted› case at that layer.
‹branch› is ‹branch_lifted› collapsed back through \<^const>‹collapse_lift›,
so a domain can use the pollution-fixed recursion while still returning a
plain ‹abs_state›: an infeasible or witness-bottom result becomes the
plain type's own ‹bot›, exactly the value the branch operation's callers already
treat as a dead program point. This replaces the old feasible-gated-raw-
‹bfilter› ‹branch›: that definition is strictly less precise on ‹And›/
‹Or› conditions (the join-arm-pollution ‹bfilter›'s own comment
documents), and this project keeps exactly one public plain-state branch
operation rather than two of different precision.
›
definition branch :: "exp => bool => 'a abs_state => 'a abs_state" where
"branch e pol d = collapse_lift (branch_lifted e pol d)"
lemma branch_sound [intro]:
assumes "s ∈ γ d" "truthy (⟦e⟧⇩e s) = pol"
shows "s ∈ γ (branch e pol d)"
unfolding branch_def
by (rule gamma_collapse_lift[where gam = gamma_state,
OF branch_lifted_sound[OF assms] gamma_state_bot])
text ‹
‹branch› and ‹branch_lifted› denote the same concrete stores: ‹branch›
only adapts the carrier to the plain-state shape a domain's branch operation needs,
it does not lose precision relative to ‹branch_lifted›. Left bare rather
than ‹[simp]›: its right-hand side is a strictly more complex normal
form than its left, so declaring it a default rewrite would silently
block every proof that reasons about ‹branch› directly (‹branch_sound›
among them) -- cite it explicitly where the lifted view is actually
needed.
›
end
subsection ‹Conservative inverse operator›
text ‹
A domain too coarse to invert an operator (e.g. sign, which cannot narrow
either operand of a plus/minus/times from its result) instantiates that
inverse with this shared no-op: both operands pass through unchanged. The
first argument is the known result or truth value, so the same no-op serves
the arithmetic inverses and the comparison inverses. Its soundness
obligation unfolds to the operands' own membership, so each instance
discharges it with ‹inv_conservative_def›.
›
definition inv_conservative :: "'r => 'a => 'a => 'a * 'a" where
"inv_conservative r a1 a2 = (a1, a2)"
end