Spurious Overflow Warnings and Imprecision for Guards Involving Signed AND Unsigned Types

[FungOliver]

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:

//PARAM:  --enable ana.int.interval   --set ana.activated[+] apron   
#include <stdio.h>
#include <stdlib.h>
#include <time.h>


int main() {
   unsigned int length = 5;
   for ( int i = 0; i < length; i++) {
     if ( i < length + 3){
        assert( i < length+1);
     }
   }
   return 0;
}

I get the following error:

./goblint --enable warn.debug --enable dbg.regression --html  --enable ana.int.interval   --set ana.activated[+] apron    --html tests/regression/98-relational-array-oob/01-random-simple.c
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (tests/regression/98-relational-array-oob/01-random-simple.c:9:8-9:36)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (tests/regression/98-relational-array-oob/01-random-simple.c:10:10-10:24)
[Debug][Analyzer] **Invariant failed: expression (unsigned int )i < length + 3U" not understood. (tests/regression/98-relational-array-oob/01-random-simple.c:10:10-10:24)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (tests/regression/98-relational-array-oob/01-random-simple.c:11:9-11:30)
[Debug][Analyzer] Invariant failed: expression "(unsigned int )i < length + 1U" not understood. (tests/regression/98-relational-array-oob/01-random-simple.c:11:9-11:30)
[Warning][Assert] Assertion " i < length+1" is unknown. Expected: SUCCESS -> failed (tests/regression/98-relational-array-oob/01-random-simple.c:11:9-11:30)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (tests/regression/98-relational-array-oob/01-random-simple.c:9:14-9:19)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 6
  dead: 0
  total lines: 6
Writing xml to temp. file: /tmp/ocaml3807a8tmp
Time needed: 505 ms
See result/index.xml

[michael-schwarz]

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

[michael-schwarz]

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;
}

• 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 during invariant seems spurious) [CC @jerhard @sim642 (am I missing something?)]
• Fails to establish the relationship of interest in Apron

[michael-schwarz]

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.

[sim642]

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 during invariant 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.

[michael-schwarz]

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.

[sim642]

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.

[michael-schwarz]

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.

[sim642]

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.