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