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
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
