[klee-dev] Query: Klee behavior with pointer de-referencing
Sandeep Dasgupta
sdasgup3 at illinois.edu
Tue Jan 14 22:55:20 GMT 2014
Thanks a lot Cristian. Appreciate your help.
On 01/08/2014 12:19 PM, Cristian Cadar wrote:
> Indeed. You have a double-dereference there, and KLEE cannot reason
> symbolically about this, so it's forking into all possible cases
> (alternatively it could choose only one option). There is a
> discussion about double-dereferences in the paper describing KLEE's
> predecessor EXE
> (http://www.doc.ic.ac.uk/~cristic/papers/exe-tissec-08.pdf).
>
> Cristian
>
> On 08/01/14 17:54, Paul Marinescu wrote:
>> 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
>> <mailto: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 <mailto: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
>>
>
> _______________________________________________
> 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
More information about the klee-dev
mailing list