[klee-dev] Query: Klee behavior with pointer de-referencing

[Sandeep]

Hello Cristian,
I am the original author of the code that you looked at.

Let me explain my intention of the code (pasted below).

I am intentionally storing the addresses of xi's in a array of pointers. 
Also I am constraining x to take values 1,2 and 3.
My expectation is that only one path of the if condition got explored  
as all possible values of the symbolic variable x will make
*temp > 0.

int foo(int x, int x1, int x2, int x3, int x4) {
   int **array = (int **) malloc(4*sizeof(int *));
   array[0] = &x1;
   array[1] = &x2;
   array[2] = &x3;
   array[3] = &x4;

   int **ptr = array + x;

   int* temp =  *ptr;

   if(*temp > 0) {
     assert(1);
   } else {
     assert(0);
   }
   return *temp;
}
int main() {
   int x;

   klee_make_symbolic(&x, sizeof(x), "x");
   klee_assume((x >  0) & (x <  4));

    return foo(x,10,20,30,40);
}

But Klee is reporting three paths.

Also ktest-tool gives the following information:

ktest file : 'klee-last/test000002.ktest'
args       : ['kleetest_5.o']
num objects: 1
object    0: name: 'x'
object    0: size: 4
object    0: data: 2

ktest file : 'klee-last/test000003.ktest'
args       : ['kleetest_5.o']
num objects: 1
object    0: name: 'x'
object    0: size: 4
object    0: data: 3

ktest file : 'klee-last/test000001.ktest'
args       : ['kleetest_5.o']
num objects: 1
object    0: name: 'x'
object    0: size: 4
object    0: data: 1

Can you please explain why I am getting this result.

With Thanks
Sandeep


On 1/7/2014 12:32 PM, Cristian Cadar wrote:
> See http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg00891.html
>
> Cristian
>
> On 07/01/14 18:26, Pablo González de Aledo wrote:
>> I'm sorry, I'm not the original author but I've faced the same problem
>> before and I also don't understand why Klee does what it does.
>>
>> May be the next code is simpler, and still explains the issue.
>>
>> int main() {
>> int a;
>> int array[] = {1,2,3,4,5};
>>
>> klee_make_symbolic(&a, sizeof(a), "a");
>>
>> if(array[a] == 3)
>> return 0;
>> else
>> return 1;
>> }
>>
>> Why does Klee generate 17 solutions when only one is possible (a == 2) ?
>>
>> Thanks.
>>
>>
>>
>> 2014/1/7 Cristian Cadar <c.cadar at imperial.ac.uk
>> <mailto:c.cadar at imperial.ac.uk>>
>>
>>     I only had a brief look at your code, but it looks like you are
>>     storing the addresses of the x_i variables into the array, which is
>>     likely not what you intended.
>>
>>     Cristian
>>
>>
>>     On 18/12/13 06:39, Sandeep wrote:
>>
>>         Hello All,
>>
>>         Please consider the following program.
>>
>>         The intension of the program is to let KLEE choose a value of x
>>           so that
>>         the path (*temp <= 0) is explored and
>>         KLEE is able to figure out the value of x  (= 3) for that to
>>         happen. But
>>         in addition it is reporting two other paths for x = 1 and x =2,
>>         despite
>>         of the fact that there are  only 2 possible paths.
>>
>>         Also to add, if I call foo with
>>         foo(x, 10,20,30,40)
>>         then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path
>>         (as the
>>         path (*temp > 0) is not feasible for any value of x)
>>
>>
>>         Can anybody please give me some insight.
>>
>>                                      int foo(int x, int x1, int x2, int
>>         x3, int x4) {
>>                                         int **array = (int **)
>>                                      malloc(4*sizeof(int *));
>>                                         array[0] = &x1;
>>                                         array[1] = &x2;
>>                                         array[2] = &x3;
>>                                         array[3] = &x4;
>>
>>                                         int **ptr = array + x;
>>
>>                                         int* temp =  *ptr;
>>
>>                                         if(*temp > 0) {
>>                                           assert(1);
>>                                         } else {
>>                                           assert(0);
>>                                         }
>>                                         return *temp;
>>                                      }
>>
>>
>>                                      int main() {
>>                                         int x;
>>
>> klee_make_symbolic(&x,
>>         sizeof(x), "x");
>>                                         klee_assume((x >  0) & (x <
>>           4)); // To
>>                                      allow valid memory access on 
>> 'array'
>>                                         return foo(x,10,20,30,-1);
>>                                      }
>>
>>
>>
>>
>>         --
>>         *With Thanks and Regards,*
>>
>>         Sandeep Dasgupta
>>         Graduate ( PhD ) in Computer Science
>>         Room : 1218 Siebel Center for Computer Science
>>
>>
>>         _________________________________________________
>>         klee-dev mailing list
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>> https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>>
>>
>>     _________________________________________________
>>     klee-dev mailing list
>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>> https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>>
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>


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