[klee-dev] klee_make_symbolic bug?

[Mark R. Tuttle]

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
-------------- next part --------------
HTML attachment scrubbed and removed