klee with loops strange behaviour with similar code

Question

I have a question about how is working KLEE (symbolic execution tool) in case of loops with symbolic parameters:

int loop(int data) {
  int i, result=0;
  for (i=0;i<data ;i++){   
     result+= 1;
     //printf("result%d\n", result); //-- With this line klee give different values for data
}
   return result;
}
void main() {
  int n;
  klee_make_symbolic(&n, sizeof(int),"n");  
  int result=loop(n) ;
}

If we execute klee with this code, it give only one test-case. However, if we take out the comment of the printf(...), klee will need some type of control for stop the execution, because it will produce values for n: --max-depth= 200

I would like to understand why klee have this different behavior, that doesn't have sense for me. Why if I don't have a printf in this code, it will not produce the same values.

I discovered that it happens whend the option --optimize is used when it is not there is the same behavior. Someone know how is working the --optimize of Klee?

An another quieston about the same is, if in the paper that they have published, As I understand they said that their heuristics search will make it not be infinite (they useavoid starvation) because I have it runing doesn't stop, It is true that should finish the klee execution in case of this loop?

Thanks in advance

Answer 1

What I want to know is why this different behavior with the option --optimize. Thanks

In C/C++ there is concept of "undefined behaviour" (see: A Guide to Undefined Behavior in C and C++, Part1,Part 2,Part 3, What Every C Programmer Should Know About Undefined Behavior [#1/3],[#2/3],[#3/3]).

Overflow of signed integer is defined as undefined behaviour in order to allow compiler to do optimize stuff like this:

bool f(int x){ return x+1>x ? true : false ; }

let's think... x+1>x in normal algebra is always true, in this modulo algebra it is almost always true (except one case of overflow), so let's turn it into:

true

Such practices enables huge amount of great optimizations. (Btw. If you want to have defined behaviour when overflow, use unsigned integers - this feature is extensively used in cryptography algorithms implementations).

On the other hand, sometimes leads to surprising results, like this code:

int main(){
    int s=1, i=0;
    while (s>0) {
        ++i;
        s=2*s;
    }
    return i;
} 

Being optimised into infinite loop. It's not bug! It's powerful feature! (Again.. for defined behaviour , use unsigned).

Let's generate assembly codes for above examples:

$ g++ -O1 -S -o overflow_loop-O1.s overflow_loop.cpp
$ g++ -O2 -S -o overflow_loop-O2.s overflow_loop.cpp

Check of loop part is compiled differently:

overflow_loop-O1.s:

(...)
.L2:
    addl    $1, %eax
    cmpl    $31, %eax
    jne    .L2
(...)

overflow_loop-O2.s:

(...)
.L2:
    jmp    .L2
(...)

I would advice you to check assembly of your code on different optimisation levels (gcc -S -O0 vs gcc -S -O1...-O3). And again, nice posts about topic: [1], [2], [3], [4], [5], [6].