[klee-dev] KLEE "hang" while executing a system call

[Thuan Pham]

Hi all,
I am implementing a customized search strategy for KLEE and facing a
strange problem. Although my search strategy can work quite well with some
subject programs, KLEE "hang" while testing the "paste" utility in
Coreutils 6.10. Precisely, KLEE still be alive (because it can handle
Ctrl+C to terminate and finalize the execution), however when I try to
insert some printf statements at some points, the printf functions do not
work after KLEE reach the following statement in fd.c.

r = syscall(__NR_read, f->fd, buf, count); //line 372, fd.c

Here is the information of some instructions before KLEE hang. I got them
by enabling the debug-print-instructions option. The last instruction is
the system call in fd.c

klee-uclibc/libc/string/strncmp.c:30:          249647   %0 = alloca i32
klee-uclibc/libc/stdio/fprintf.c:33:          249648   %2 = load %4**
%stream_addr, align 4, !dbg !5065
klee-uclibc/libc/string/strncmp.c:32:          249649   %toBoolnot = xor i1
%toBool, true, !dbg !5065
klee-uclibc/libc/string/strncmp.c:32:          249650   %16 = getelementptr
inbounds i8* %15, i64 1, !dbg !5065
coreutils-6.10-llvm-obj/src/../../coreutils-6.10/src/paste.c:459:
 249651   br i1 %17, label %bb, label %bb10, !dbg !5076
klee-uclibc/libc/unistd/getopt.c:768:          249652   %583 =
getelementptr inbounds %struct._getopt_data* %582, i32 0, i32 5, !dbg !5162
klee/runtime/POSIX/fd.c:372:          249653   %33 = tail call i32 (i32,
...)* @syscall(i32 3, i32 %31, i8* %24, i32 %27) nounwind, !dbg !5088

I did some initial checks and found that KLEE get stuck in the function
executeInstruction. In the main while loop of the method Executor::run
(Executor.cpp), after selecting a state to run (searcher->selectState())
and getting the next instruction (KInstruction *ki = state.pc), KLEE calls
the function executeInstruction to execute the picked instruction. However,
KLEE cannot exit from the function.

I have been working on the KLEE version committed by Dan Liew in Nov 2 2014
(50073b4689c3a1b9eefd5befddf0e15ae0d93348). LLVM version is 2.9 and I
followed every steps in the user guide at
http://klee.github.io/getting-started/

I suspect that there is some issue inside the file system model of KLEE or
in the executeInstruction function that could introduce an infinite loop
(in some corner case). Moreover, there could be an issue inside the
implementation of my search strategy. Have you ever faced this problem? Any
suggestions are appreciated.

Thank you.
Thuan
-------------- next part --------------
HTML attachment scrubbed and removed