Exploring the same branch twice

[kren1]

Given this program:

unsigned int a, b;

int main() {
  __CrestUInt(&a);
  if( a < 1 || a > 1) {
    exit(0);
  }
  (-1 > a ) || b;

  printf("g_4: %d\n", a);
}

I would expect crest to explore 3 branches, printing "g_4: 1" once, however I get:

Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 2 branches [1 reach funs, 8 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 3 (0s): covered 5 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 4 (0s): covered 5 branches [1 reach funs, 8 reach branches].
Prediction failed!

[jburnim]

I believe this is the same issue as https://github.com/jburnim/crest/issues/6 .

In comparing an integer (-1) to an unsigned integer (a) in C++, both operands are converted to be unsigned. Because of this, it looks like part of CIL or CREST's instrumentation is transforming the expression -1 > a to the equivalent 4294967295u > a. (You can see this if you put the above example in test.c, run crestc on it, then examine the instrumented C code crest.cil.c.) This constant 429496729u is then incorrectly sent to Yices as -1 because of the bug in https://github.com/jburnim/crest/issues/6 .

[jburnim]

With the bug fix, there is no prediction failure on this example:

$ ../bin/run_crest ./test 100 -dfs
Iteration 0 (0s): covered 0 branches [0 reach funs, 0 reach branches].
Iteration 1 (0s): covered 2 branches [1 reach funs, 8 reach branches].
Iteration 2 (0s): covered 3 branches [1 reach funs, 8 reach branches].
g_4: 1
Iteration 3 (0s): covered 5 branches [1 reach funs, 8 reach branches].

(The exploration ends at this point because the remaining branches are all infeasible.)