Remove division by zero error message during base invariant

[sim642]

Discovered in #1838 (comment). Should be redundant due to #1764.
Especially because this only trigger for must division by zero, not may.

It's strange because it's the only warning/error emitted during base invariant.

TODO

• Is the top-ification even necessary/useful then?

[michael-schwarz]

What would you propose instead of top? Raising deadcode? These seem to be the only sensible things we can do.

(The warning should more likely be an internal analyzer warning, I guess it can sometimes happen that during refinement of something that is actually not reachable we produce some kind of nonsensical value.)

[sim642]

What would you propose instead of top? Raising deadcode? These seem to be the only sensible things we can do.

I haven't yet thought about what exactly this is trying to achieve, but only top-ifying must zero is odd: [0,0] goes to top, but [0,1] remains [0,1] instead of also going to top for including the problematic 0.

It's the same kind of strangeness that used to be in the interval division: #1804 (comment).

[sim642]

I think @karoliineh hit this strange behavior also while looking into some ArithmeticOnBot exceptions in SV-COMP.

[karoliineh]

What would you propose instead of top? Raising deadcode? These seem to be the only sensible things we can do.

This is a philosophical question I also raised with @vesalvojdani a few days ago, it seems that the uncertainty it is rooted throughout many decisions about different analyses.

To the question of "what do bot and top mean", I got an answer from @sim642 that bot is no possible values and top is any value possible. @vesalvojdani added, that the behavior of programs in real-world should in principle correspond to these values, e.g., when there's division by 0, the program will crash and there will be no possible values: bot. However, I then noted that we handle division by 0 to top in the code:

analyzer/src/analyses/baseInvariant.ml

Lines 294 to 302 in 55c8b0d

	let warn_and_top_on_zero x =
	if ID.equal_to Z.zero x = `Eq then
	(M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
	Checks.error Checks.Category.DivisionByZero "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
	ID.top_of ikind)
	else (
	Checks.safe Checks.Category.DivisionByZero;
	x)
	in

Then we also discussed about overflows, and with an overflow, the program does not crash. However, we have these options assume_top and assume_none. With assume_top the behavior for overflows is logical to me, but with assume_none, if there is a definite overflow (i.e., all recorded values are out of range), we result in bot for the variable, and then crash every time we reach an arithmetic operation with this variable later. When I tried allowing arithmetic operations with bottoms so that they also result in bot, I got [Unsound] both branches dead for most of the cases, which is not good.

So, in a sense, bot if program would actually crash seems logical, but implementing it that way leads to not desired results (not more helpful than just crashing the analysis with exception). top seems to behave normally in most cases but then not here and if used during assume_none, the option would become in some way same with assume_top. So I am confused about the theoretical meaning and the actual behavior that happens in our analyses.

[michael-schwarz]

bot in the sense of "no values" should be propagated to the outside by raising dead code, which gets you somewhat consistent behavior I guess.

[vesalvojdani]

Yes, bot is the only thing that has some semantic interpretation consistent with refining values that survive after having warned about undefined behavior. I think the use of top for cases of undefined behavior throughout goblint dates back to me, and it has no real semantic interpretation, although it may be practically useful. I still think for a sound analyzer that the sort of pseudo-undefined behavior treatment is dangerous, and we should rather go for the warn and refine view, which specializes to no values in the definite case, or simply abort the analysis altogether.

[sim642]

There's no one-size-fits-all answer regarding UB, that's why we have options to configure them separately.
A NULL dereference or perhaps division by 0 will probably crash the program and then dead code makes sense.

But a (definite) signed overflow will not actually crash the program. Depending on the assumptions to make, assume_wraparound and assume_top are both perfectly reasonable. But assume_none making the code dead could be unsound because the program doesn't stop.

How all of it relates to the particular issue in this PR is a separate matter. Because this isn't about what happens during normal evaluation of such expression. This is about what's being done after the expression has already been evaluated (to non-bottom I think) and we're not trying to refine the variables in the arguments of such division.
The actual division by zero during forward evaluation and the warnings about it are now from #1764.

[vesalvojdani]

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]...

But if we have a forward assume none semantics, then definite division by zero should not be asked to refine at all. And if it is a potential division, we should on assume none, be able to simply remove the zero from the denominator and refine the a with the values that produce a result? If the forward semantics returns top, then returning top here would also make sense except also anything that includes the zero should return top for the refinement.