[klee-dev] Klee Symbolic Pointers

[Charles Noble]

Hi all,

Is anyone aware of a feature in KLEE that will allow for a pointer to be
symbolic and also when the pointer is dereferenced it points to a specific
symbolic array? Given this example program I would like to see two paths
executed like so:

void *
memcpy (void *dest, const void *src, size_t len)
{
  char *d = dest;
  if (src == NULL) {
    return dest;
  }
  const char *s = src;
  while (len--)
    *d++ = *s++;
  return dest;
}

int main() {
    int len;
    char dest[1];
    char *src;

    klee_make_symbolic(&len, sizeof(len), "sym_len");
    klee_make_symbolic(dest, sizeof(char), "sym_dest");
    klee_make_symbolic(&src, sizeof(char*), "sym_src");

    klee_assume(len == 1);

    memcpy(dest, src, len);

    return 0;
}

EXPECTED OUTPUT:

PATH 1:
[ (1 == sym_len),
  (0 == sym_src) ]

SYM MEMORY:
sym_dest = sym_dest[0]
sym_src = sym_src[0]

PATH 2:
[ (1 == sym_len),
  !(0 == sym_src) ]

SYM MEMORY:
sym_dest = sym_src[0]
sym_src = sym_src[0]

>From what I understand of KLEE, if the src pointer is not symbolic then
there will only be a single path and if the src pointer is symbolic, then
KLEE will generate many paths when it is derefenced due to the not knowing
the which address that the symbolic pointer points to. Is there any way
that I run KLEE to generate both paths while avoiding the pointer
resolution issue?

Thanks,
Charles Noble
-------------- next part --------------
HTML attachment scrubbed and removed