[klee-dev] Query: Klee behavior with pointer de-referencing
Paul Marinescu
paul.marinescu at imperial.ac.uk
Wed Jan 8 17:54:21 GMT 2014
As Cristian pointed in the previous reply, the answer lies in object resolution. klee does not report 3 paths, it reports 3 possible executions, all of which follow the same path. What differs between these 3 executions is the value of ptr, i.e. the object it points to.
Paul
On 8 Jan 2014, at 18:48, Sandeep <sdasgup3 at illinois.edu> wrote:
> 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
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list