[klee-dev] klee_make_symbolic bug?

[Chaoqiang Zhang]

>>>> I'm guessing the stack is treated differently.
Yes, good observation. I checked and found in klee_int, the "x" variable
got different addresses for different calls. You may find it by print &x.


On Thu, Aug 14, 2014 at 8:08 AM, Mark R. Tuttle <markrtuttle at gmail.com>
wrote:

> Thanks.  I believe you.
>
> My reason for writing, though, was that Block 1 should also be using the
> same memory address for the two name strings, but it works without
> suffering from the overwrite you describe.
>
> Specifically, there is no use of the stack between the two calls to
> klee_int, so the memory used on the stack should be the same by the two
> invocations to klee_int.  I'm guessing the stack is treated differently.
>
> Thanks,
> Mark
>
>
>
> On Thu, Aug 14, 2014 at 2:18 AM, Chaoqiang Zhang <
> chaoqiang.zhang at gmail.com> wrote:
>
>> klee will reset the memory object name if you are using the same
>> variable(the same memory address), see function  SpecialFunctionHandler::handleMakeSymbolic,
>> So, in this case, your second name overwrite the first one. But the good
>> thing is that klee also has ObjectState::Array member hold another name, so
>> if you change the line 1) below inside Executor::getSymbolicSolution
>> into 2). It can output the correct name. But, I am not sure if this is the
>> right solution.
>>
>> 1) res.push_back(std::make_pair(state.symbolics[i].first->name, values[i]));
>>
>> ====>>>>>
>>
>> 2) res.push_back(std::make_pair(objects[i]->name, values[i]));
>>
>>
>>
>>
>> On Wed, Aug 13, 2014 at 1:41 PM, Mark R. Tuttle <markrtuttle at gmail.com>
>> wrote:
>>
>>> Is this a bug in how klee_make_symbolic(adr,size,name) handles the name
>>> string?
>>>
>>> I want to modify ktest-tool so complex data structures are easier to
>>> read. I want an array of integers to print in a way that looks like an
>>> array of integers.  This leads me to experiment with automating
>>> construction of names like "x[0]" and "x[1]" for klee_make_symbolic to
>>> insert into the *.ktest files.
>>>
>>> Consider the following code demo.c
>>>
>>> #include <klee/klee.h>
>>>
>>> int main(int argc, char* argv[]) {
>>>   int array[2];
>>>
>>> #if BLOCK==1
>>>   array[0] = klee_int("x[0]");
>>>   array[1] = klee_int("x[1]");
>>> #endif
>>>
>>> #if BLOCK==2
>>>   int x;
>>>   klee_make_symbolic(&x,sizeof(x),"x[0]");
>>>   array[0] = x;
>>>   klee_make_symbolic(&x,sizeof(x),"x[1]");
>>>   array[1] = x;
>>> #endif
>>>
>>> #if BLOCK==3
>>>   int x0;
>>>   klee_make_symbolic(&x0,sizeof(x0),"x[0]");
>>>   array[0] = x0;
>>>   int x1;
>>>   klee_make_symbolic(&x1,sizeof(x1),"x[1]");
>>>   array[1] = x1;
>>> #endif
>>>
>>>   return 0;
>>> }
>>>
>>> Block 1 feels like natural code for inserting symbolic integers into an
>>> array.  Block 2 feels like a natural in-lining of the klee_int function
>>> that allocates x on the stack, calls klee_make_symbolic, and returns x.
>>> Block 3 is block 2 without the reuse of x (simulating the result of x on
>>> the stack).
>>>
>>> So I expect them all to use "x[0]" and "x[1]" as the names for array[0]
>>> and  array[1], but that's not what I get running the latest KLEE with
>>> LLVM/CLANG 3.3:
>>>
>>> Block 1
>>>
>>> $LLVM/bin/clang -DBLOCK=1 -c -emit-llvm -I $KLEE/include -o demo.bc
>>> demo.c
>>> $KLEE/bin/klee demo.bc
>>> $KLEE/bin/ktest-tool klee-last/*.ktest | grep name
>>>
>>> object    0: name: 'x[0]'
>>> object    1: name: 'x[1]'
>>>
>>> Block 2
>>>
>>> $LLVM/bin/clang -DBLOCK=2 -c -emit-llvm -I $KLEE/include -o demo.bc
>>> demo.c
>>> $KLEE/bin/klee demo.bc
>>> $KLEE/bin/ktest-tool klee-last/*.ktest | grep name
>>>
>>> object    0: name: 'x[1]'
>>> object    1: name: 'x[1]'
>>>
>>> Block 3
>>>
>>> $LLVM/bin/clang -DBLOCK=3 -c -emit-llvm -I $KLEE/include -o demo.bc
>>> demo.c
>>> $KLEE/bin/klee demo.bc
>>> $KLEE/bin/ktest-tool klee-last/*.ktest | grep name
>>>
>>> object    0: name: 'x[0]'
>>> object    1: name: 'x[1]'
>>>
>>> Is this a bug or am I just doing something stupid?
>>>
>>> Thanks,
>>> Mark
>>>
>>>
>>>
>>> _______________________________________________
>>> 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