[klee-dev] Query: Klee behavior with pointer de-referencing
Cristian Cadar
c.cadar at imperial.ac.uk
Wed Jan 8 18:19:23 GMT 2014
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
>
More information about the klee-dev
mailing list