vbpf / prevail / 28864319397

87%

push

github

Fix TypeDomain::is_subsumed_by for unsatisfied type-equality classes

is_subsumed_by (backing operator<=) could report self <= other when false,
inverting the lattice order. In the equality-preservation loop, when other has
a multi-member class (type(x) == type(y)) whose first member is untracked in
self, the code only returned false if some other member was tracked, otherwise
treating the equality as satisfied. But an untracked member is an independent
top in self, so self does not enforce other's equality and is not subsumed.
A fixpoint check relying on this could declare convergence prematurely and
drop reachable states (unsound).

Return false as soon as a nontrivial equality class in other has an untracked
member in self -- the conservative, correct side. Add a TypeDomain-level
regression test (top is not subsumed by a top-typeset type equality).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CsnGgfCt3qNBW1Wk8BPPjQ
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

1 of 1 new or added line in 1 file covered. (100.0%)

9142 of 10567 relevant lines covered (86.51%)

6475820.5 hits per line