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 <[email protected]> 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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
