[klee-dev] Fwd: klee_make_symbolic bug?

[Chaoqiang Zhang]

>>> calling into klee_int() will cause KLEE to enter the klee_int()
>>> function and a variable on klee_int's stack is used as the address of
>>> the symbolic. Even if klee_int() was inlined this would still work
correctly
More specifically, the variable "x" in klee_int is actually allocated with
malloc under klee vm instead of automatic memory allocation like standard
machine. see Executor::executeAlloc-> MemoryManager::allocate call chain. I
am also thinking if we can assume klee_int can always give you different
addresses, what if two malloc give you the same address if there are some
free between them. please correct me if I am wrong




On Thu, Aug 14, 2014 at 10:08 AM, Daniel Liew <daniel.liew at imperial.ac.uk>
wrote:

> On 14 August 2014 16:08, Mark R. Tuttle <markrtuttle at gmail.com> wrote:
> > 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.
>
> But the string you pass into klee_int() specifies the string name for
> that symbolic and that is exactly what you are observing.
>
> > 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.
>
> No. klee_int() is part of KLEE's runtime and can be seen at [1]
>
> calling into klee_int() will cause KLEE to enter the klee_int()
> function and a variable on klee_int's stack is used as the address of
> the symbolic. Even if klee_int() was inlined this would still work
> correctly.
>
> [1] https://github.com/klee/klee/blob/master/runtime/Intrinsic/klee_int.c
>
> You might find it informative to look at the LLVM IR that is actually
> being executed (look at klee-last/assembly.ll).
>
> Thanks,
> Dan.
>
-------------- next part --------------
HTML attachment scrubbed and removed