Unsound congruence domain arithmetic

[sim642]

I inspected the first ERROR (both branches dead) result after #1579 on sv-benchmarks and it lead to unsound congruence domain arithmetic which presents itself as both branches dead in a reduced sv-benchmarks program (in this PR). It's from a hardness task, and those make up 72 of the 81 cases from a nightly run. I didn't check others because they might all be for the same reason.

In particular, the unsound operations are visible from this tracing output:

%%% congruence: mul : 4294967295 1+3ℤ -> ℤ 
%%% congruence: add : 3ℤ ℤ -> ℤ
%%% congruence: sub : 3ℤ 1+3ℤ -> ℤ
%%% congruence: mul : 4294967295 2 -> 8589934590 
%%% congruence: add : 3ℤ 8589934590 -> 3ℤ
%%% congruence: sub : 3ℤ 2 -> 3ℤ
%%% congruence: meet 2 ℤ -> 2
%%% congruence: meet 1+3ℤ 3ℤ -> ⟂

For context, this is about sub being implemented as https://github.com/goblint/analyzer/blob/060004cc2fcb4a655c4d7b90718e19adfb9c2c36/src/cdomain/value/cdomains/intDomain.ml#L3129 where neg involves a mul: https://github.com/goblint/analyzer/blob/060004cc2fcb4a655c4d7b90718e19adfb9c2c36/src/cdomain/value/cdomains/intDomain.ml#L3102

In fact, there are multiple problems visible here:

1. The subtractions are obviously unsound: 3ℤ - (1+3ℤ) = ℤ (should be 2+3ℤ?) and 3ℤ - 2 = 3ℤ (should be 1+3ℤ?). I'm not sure if this is unsound because of the indirect definition of sub or what.
2. The negation via multiplication by -1 (which is 4294967295 by unsigned wrap-around) gives a constant with is out of bounds of the type: 4294967295 * 2 = 8589934590. Seems like this result should also be reduced modulo 4294967296.

There's a normalize function in the congruence domain, but the arithmetic operations don't seem to call it in all cases.

[michael-schwarz]

Nice catch, I guess the warning is immediately starting to pay off! It's impressive this hasn't lead to unsound results anywhere. I guess it is because congruences are not enabled that often by the autotuner.

The subtractions are obviously unsound: 3ℤ - (1+3ℤ) = ℤ (should be 2+3ℤ?) and 3ℤ - 2 = 3ℤ (should be 1+3ℤ?).

Iirc, there is some problem to be considered for when things become negative... But I would have to check that again.

[sim642]

Iirc, there is some problem to be considered for when things become negative... But I would have to check that again.

That might explain some of this because subtraction involves two cases:

1. Things like 5 - 3 which remain non-negative.
2. Things like 5 - 10 which go negative and wrap around with unsigned types, additionally modulo some power of 2.

Since congruences are unaware of intervals, they cannot distinguish the two (this has also come up in #1156) and must account for both. Thus, 3ℤ - (1+3ℤ) = ℤ should be fine and sound (it's just top). But 3ℤ - 2 = 3ℤ still is unsound, even for no-wrap cases.

Although addition should also have two cases: normal and wrap modulo power of 2. I wonder if add is even sound then. It's starting to look like our congruences won't be able to find out anything like this, unless the values are constants (but then we don't need congruences in the first place).

[michael-schwarz]

It's starting to look like our congruences won't be able to find out anything like this

We might want to think about feeding back interval information somehow.

[michael-schwarz]

Does this now also fix the case from #1671?

[jerhard]

Does this now also fix the case from https://github.com/goblint/analyzer/issues/1671?

Yes, it does, I also merged master with the Bitfielddomain in here and added the test case as 37/16.

Thus, this fixes #1671.