Open FungOliver opened 10 months ago
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
int main() {
unsigned int length = 5;
int i = 0;
int top;
if(top) {
i = 10;
}
if(i < length + 3) //NOWARN
{
__goblint_check(i <= 8);
i = 8;
}
}
One problem is spurious overflow warnings here: We warn about a possible underflow in this snippet.
The original example from this issue works without any hitch with #1406 and #1408.
This example though still
//PARAM: --enable ana.int.interval
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
int main() {
int top;
unsigned int length = 20;
unsigned int blub = 5;
if(top) {
blub = 10;
}
for (int i = 0; i < length; i++) {
if (i < blub + 3) //NOWARN
{
}
}
return 0;
}
invariant
while trying to perform the HC4-Revise algorithm): It would seem like any actual warnings should be produced during forward evaluation, so flagging things during invariant
seems spurious) [CC @jerhard @sim642 (am I missing something?)]void main() {
int top;
unsigned int blub = 5;
if(top) {
blub = 10;
}
int topi;
if(topi < blub+1) {
// Fails
__goblint_check(topi < blub + 3);
}
unsigned int topu;
if(topu < blub+1) {
// Works
__goblint_check(topu < blub + 3);
}
}
This highlights the issue where we are weaker for the signed
variable topi
than for unsigned
variable topu
.
Produces a warning for the comparison (from
invariant
while trying to perform the HC4-Revise algorithm): It would seem like any actual warnings should be produced during forward evaluation, so flagging things duringinvariant
seems spurious)
That sounds right because backward evaluation doesn't happen in the concrete, so the program cannot be wrong there.
It would be interesting to know what exact operation is still causing that. Outright disabling all warnings during invariant
would be to crude.
It would be interesting to know what exact operation is still causing that.
It is an ID.sub
operation. It would be possible to patch this but this would require equipping every operation with a ~suppress_ovwarn
argument as in #1406. I think that is quite ugly, so I think I will make a PR to solve it with a global flag and try that on for size.
It would be possible to patch this but this would require equipping every operation with a
~suppress_ovwarn
argument as in #1406. I think that is quite ugly, so I think I will make a PR to solve it with a global flag and try that on for size.
The clean solution would be to move overflow warnings out of the domains entirely. Some IntDomain
things already return some kind of overflow_info
. If all operations did that, then warnings can be generated somewhere in the base analysis instead and none of the suppress_ovwarn
arguments would be needed in the domains.
This would also avoid all the duplication MaySignedOverflow
query now has. It could simply do the evaluation and check the returned overflow_info
instead of replicating the overflow check from the domains.
It could also improve our overflow analysis precision when relational analyses are activated. Currently overflow warnings are hard-coded into the interval domain, but that doesn't have to be the case.
Yes, that would be possible and most likely the cleaner solution. It however requires quite some refactoring work, that I cannot commit time to right now (or in the next 2 months). Maybe we should make an issue for it?
I think in absence of such a general fix, this here is the next best thing and at least a step in the right direction.
Other than a clean general fix, did #1411 fix everything here? If so, then we can close this and open a separate issue about the cleanup/refactoring.
EDIT: Ah no, #1408 still refers to this as well.
When comparing a signed integer with an unsigned integer and a constant in a loop. Goblint fails to parse those expressions:
In the following example:
I get the following error: