[klee-dev] klee_make_symbolic bug?

[Chaoqiang Zhang]

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