Remove warn_and_top_on_zero from BaseInvariant for division by zero

[sim642]

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):

Okay, so here specifically the question is what the backward transfer function should be for c = a / [0;0], given some value for c, how can one refine a? And what about c = a / [0;1]...

The strange thing is that the warn_and_top_on_zero code 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 triggering ArithmeticOnIntegerBot by 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_zero was added to work around them.

TODO

• sv-benchmarks

[sim642]

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_zero was added to work around them.

This is essentially reverting ae01aba. Its previous commit added the following test:

analyzer/tests/regression/27-inv_invariants/02-bot-during-condition.c

Lines 4 to 11 in df5edaa

	int tmp;
	int p_9 = 60;
	tmp = (p_9 +1) % 0;
	if ((p_9 +1) % 0) {
	tmp = 1;
	}

The test doesn't contain any checks though. But it's also not crashing after the revert.

[sim642]

On sv-benchmarks this only changes two unknowns into ArithmeticOnIntegerBot: https://goblint.cs.ut.ee/results/332-all-level01-pr-2016-after/table-generator-cmp.diff.html#/table?filter=1(0*status*(status(in(EXCEPTION%20%28IntDomain0.ArithmeticOnIntegerBot%29)),category(notIn()))).
The benchmarks seem to trigger 0 / 0 which in itself is a problem with the benchmarks maybe.

I'm not sure it's worth keeping this strange handling for that.
I think the broader issue is what's discussed in #1892: what is the result of dividing by 0? Is it top or is it assumed to not have happened?
Currently, some int domains do one, some do the other. So it matters on which int domains are active. I think it even differs by operation in the same domain (div and rem in intervals).

To properly fix this, I think we need an option like sem.int.div-by-zero with values assume_top and assume_none. Then all int domains should follow this option and we can be consistent and flexible.

[Copilot]

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_zero helper from inv_bin_int.
• Removed the b top-ification step for Div and Mod inverse computations.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[michael-schwarz]

ArithmeticOnIntegerBot

I think we should aim to get rid of this as much as possible, it is not a sensible message to report to users. Also divisions such as 0/0 can always happen due to over approximation in contexts / digests / ..., so if we accept those we are potentially blocking our path towards analyzing larger programs as that error cannot be recovered from.

[sim642]

I agree that ArithmeticOnIntegerBot indicates an internal problem that a user should never see.

Since there's no direct benefit from this PR, there's no rush to merge it. If the division by zero story is made consistent in the int domains, this should no longer cause any new exceptions. Because really, if division by zero is assumed to not have happened, then branching on it should be dead and no refinement is necessary.