[klee-dev] How to deal with loop?

[Sandeep Dasgupta]

Hello All,

I am trying to understand how KLEE symbolically executes a loop.

For that,  I tried out with the following example,
int main() {
   int i = 3 , N, sum = 0 ;

   klee_make_symbolic(&N, sizeof(N), "N");
   klee_assume(N > 1 & N < 10);

   for(i=  3 ; i< N; i++)  {
   }
   return sum;
}

I am getting 7 values for symbolic variable N (value '2' for loop exit 
and values '4, 5, 6, 7, 8, 9' for paths inside the loop).
I think what is happening here is:
For each iteration of the loop a path condition is generated like (3 < N 
for 1st iteration and 4 < N for the 2nd and soon) and KLEE is solving 
all of them.
Also it is solving for 3 >=N for the  loop exit.

Please let me know if my understanding is correct.

If this is correct, then

With the following code,

int main() {
   int i , N=10 ;

   klee_make_symbolic(&i, sizeof(i), "i");
   klee_assume(i > -1);

   for( ; i< N; i++)  {
   }
   return i;
}

I am getting 11 generated tests (10 testcases with i values 0, 1, 2, 
..., 9) for paths in the loop and 1 for the loop exit.

My question is how KLEE is working here. And how the path conditions are 
generated.
If my previous assumption is true, then it must work  like:
For each iteration of the loop a different path condition is generated 
(like i < N for 1st and 2*i < N and soon ) and if that be the case then the
conditions to be inside the loop will be 5 in number like i < 10, i < 5 
; i < 3 ; i < 2 and i < 1.

But why we are getting 9 testcases as paths inside the loop. Please explain.

-- 
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
University Of Illinois Urbana Champaign.
Room : 1218 Siebel Center for Computer Science
-------------- next part --------------
HTML attachment scrubbed and removed