[klee-dev] problem when calling Executor::runFunctionAsMain multiple times

[Zhiqiang Zhang]

Hi, there!

I'm currently hacking on Klee to add some features for my research use.
I tried to run multiple times of symbolic execution from the initial state.
It worked for the islower, regexp and get_sign examples, however I encountered
memory errors on the sort example.

I tried to figure out what happened, and I eventually found running multiple times
of runFunctionAsMain yields the same error. I guess there are some clean up issue
when runFunctionAsMain finishes.

This problem can easily be triggered by replaying multiple ktests using command
line argument "-replay-out" (even for replaying two same ktests).
The commands are as follows:

cd examples/sort
llvm-gcc -c -emit-llvm -std=c99 sort.c -I ../../include/
klee -libc=klee -allow-external-sym-calls sort.o
klee -libc=klee -replay-out=klee-out-0/test000004.ktest -replay-out=klee-out-0/test000004.ktest -allow-external-sym-calls sort.o

The output are as follows

KLEE: output directory is "/home/.../klee/klee/examples/sort/klee-out-3"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: printf
KLEE: replaying: 0x307e6e0 (16 bytes) (1/2)
KLEE: WARNING ONCE: calling external: printf(50916048, 2147483648, 1073741823, 2684354560, 2147483647)
input: [-2147483648, 1073741823, -1610612736, 2147483647]
insertion_sort: [-2147483648, -1610612736, 1073741823, 2147483647]
bubble_sort   : [-2147483648, -1610612736, 1073741823, 2147483647]
KLEE: replaying: 0x307e9c0 (16 bytes) (2/2)
input: [-2147483648, 2147483647, -2, 0]
KLEE: ERROR: /home/.../klee/klee/runtime/klee-libc/memcpy.c:17: memory error: out of bound pointer   ##### should the second replay be the same with the first one???
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 1158
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

I have dug into the source code and found that in the second run, the problem is emitted
from AddressSpace::resolveOne(const ref<ConstantExpr> &addr, ObjectPair &result).
I'm not very sure what happened here, but the address of the result of objects.lookup_previous(&hack)
seems to be very far away from the address under search. And as a consequence, the resolve
fails and returns false.  Is it possible that some data structures are not properly cleaned up after the first run?

Can you help me with this problem? Thank you very much.

Regards,
Zhiqiang