[klee-dev] klee_make_symbolic bug?

[Mark R. Tuttle]

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