Remove warn_and_top_on_zero from BaseInvariant for division by zero#2016
Remove warn_and_top_on_zero from BaseInvariant for division by zero#2016sim642 wants to merge 1 commit into
warn_and_top_on_zero from BaseInvariant for division by zero#2016Conversation
This is essentially reverting ae01aba. Its previous commit added the following test: The test doesn't contain any checks though. But it's also not crashing after the revert. |
|
On sv-benchmarks this only changes two unknowns into I'm not sure it's worth keeping this strange handling for that. To properly fix this, I think we need an option like |
There was a problem hiding this comment.
Pull request overview
This PR continues the work from #1892 by removing the warn_and_top_on_zero “top-ification” workaround in BaseInvariant’s backward refinement for integer Div and Mod, relying on the integer domains’ existing behavior for division/remainder with zero divisors.
Changes:
- Removed the
warn_and_top_on_zerohelper frominv_bin_int. - Removed the
btop-ification step forDivandModinverse computations.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
This is the continuation of #1892 regarding the top-ification aspect.
I tried to just remove it and no tests fail. But I'll see on sv-benchmarks if this actually matters sometime.
Question
In #1892 (comment):
The strange thing is that the
warn_and_top_on_zerocode is about the second argument, not the first one.And it looks like it just tries to avoid a definite division by zero in the calculations that follow, e.g.
ID.div a b. But doing so isn't actually a problem: once we're doing the refinement, we've already forward-evaluated that exact calculation with the zero divisor without issues. I don't think the abstract division operator in int domains should fail because of that.Also note that the second argument (without top-ification) would still be, e.g.,
[0,0], not bottom. So it's not triggeringArithmeticOnIntegerBotby doing that.Maybe some git archeology is needed for this code. Perhaps it was added at a time when the division operators in int domains had problems with doing this and
warn_and_top_on_zerowas added to work around them.TODO