big integer in condition bug

[kren1]

If I compile and run

#include <crest.h>
unsigned int a;
int main() {
    __CrestUInt(&a);
    printf("a: %d\n",a);
    if( a < 4294967295) {
        exit(0);
    }
}

with something like crestc example.c && run_crest ./example 1000 -dfs

I get

Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
a: 1058183384
Iteration 1 (0s): covered 1 branches [1 reach funs, 2 reach branches].
a: 0
Iteration 2 (0s): covered 1 branches [1 reach funs, 2 reach branches].
Prediction failed!

So what I assume is happening is that in iteration 1 a path that skips the if is meant to be taken, but a gets set to 0 for some reason, so the path with the if is taken again which causes the prediction failed. This behaviour can be observed for quite a while, for example it happens if the constant is 2294967295 and disappears by the time it is 1294967295.

Is this a real bug or some known limitation?

[jburnim]

Thanks for the bug report!

I think a few different things are going on here:

• In this example, it looks like the integer literal 4294967295 is treated by GCC as if it were -1 (because 4294967295 is too large to be represented as a signed integer). I haven't checked what the C standard says, but you can confirm what is happening with, e.g., printf("%d\n", 4294967295).

• CREST does not model arithmetic conversions/overflow/etc., but just models straightforward integer arithmetic. Given this limitation, CREST should find that there is no solution to (a < 4294967295) -- i.e., to (a < -1) because a is unsigned.

• Further, CREST generally doesn't handle numeric literals that are outside of the range of normal integers. (I don't remember if this is a planned limitation or a bug.) In particular, in instrumented code, all literals are converted to long literals, so 4294967295 becomes 4294967295L, rather than being treated as the int literal -1:

  ...
  __CrestLoad(6, (unsigned long )(& a), (long long )a);
  __CrestLoad(5, (unsigned long )0, (long long )4294967295L); 
  __CrestApply2(4, 16, (long long )((long )a < 4294967295L)); 
  #line 6
  if ((long )a < 4294967295L) {
   __CrestBranch(7, 3, 1);
   __CrestLoad(9, (unsigned long )0, (long long )0);
  #line 7
   exit(0);
  ...

• Finally, when numbers are passed to the Yices solver, they are converted to int values. This looks like a bug. In this case, it means Yices sees the constraint (a < -1) rather than (a < 4294967295L). This can cause incorrect behavior even when all numeric literals can be represented as ints -- e.g.:

  #include <crest.h>
  unsigned int a;
  int main() {
  __CrestUInt(&a);
  printf("a: %d\n",a);
  // CREST incorrectly sends this branch to Yices as the infeasible (a < -3)
  if ( (a  - 2147483646) < 2147483647) {
   exit(0);
  }
  }

  It should be possible to fix this bug by using the yices_mk_num_from_string or yices_mk_num_from_mpz functions in Yices API -- http://yices.csl.sri.com/old/capi.shtml -- when passing a value too big to be represented as an int.

[kren1]

Thanks for the response

• I don't think gcc treats 474294967295 as -1. My example is a bit confusing because I used %d instead %u so printf thinks it's printing a signed integer. Apologies for the confusion.
  printf("%u\n", 4294967295) prints 474294967295 as expected.

• Thanks for clarifying that CREST models just integer arithmetic. But I would like to point out that this bug persists even if you change 474294967295 to something much smaller like 274294967295, where there should be plenty of room to avoid overflow.

• I think your final point is consistent with the above observations. Thanks for clarifying!