Hi Daniel,
Here is something weird when klee runs with clone(). First, if I run
fork() at the program, klee works quite well. However, if I run clone() in
the program, and do not use the CLONE_VM flag (the cloned child process does
not share address space with parent), klee will not crash but the output is
"*failed external call: clone*". If I use the CLONE_VM flag, klee will
crash.
I have modified a function code in klee as below, and the output I got
is pretty weird (i.e., *true* and *false* both exist within single call to
the *runProtectedCall()* function). The modified source code
(ExternalDispatcher.cpp), my testcase (islower.c), and the full
output (output.txt) are attached. The testcase runs quite well if I compile
it natively with gcc.
--------------------------------------------------------------------------------------------------------------------------------
output:
KLEE: WARNING: calling external: clone(151821976, 3083198472, 0, 0)
Heming ExternalDispatcher::runProtectedCall *enter*
*Heming ExternalDispatcher::runProtectedCall true
Heming ExternalDispatcher::runProtectedCall false*
Heming ExternalDispatcher::runProtectedCall *exit*
KLEE: ERROR: /home/heming/defens/rcs-modules/klee/Debug/bin/islower.c:25:
*failed
external call: clone
*KLEE: NOTE: now ignoring this error at this location
Heming ExternalDispatcher::runProtectedCall *exit*
--------------------------------------------------------------------------------------------------------------------------------
modified a function code in klee:
bool ExternalDispatcher::runProtectedCall(Function *f, uint64_t *args) {
*printf("Heming ExternalDispatcher::runProtectedCall enter\n");*
struct sigaction segvAction, segvActionOld;
bool res;
if (!f)
return false;
std::vector<GenericValue> gvArgs;
gTheArgsP = args;
segvAction.sa_handler = 0;
memset(&segvAction.sa_mask, 0, sizeof(segvAction.sa_mask));
segvAction.sa_flags = SA_SIGINFO;
segvAction.sa_sigaction = ::sigsegv_handler;
sigaction(SIGSEGV, &segvAction, &segvActionOld);
if (setjmp(escapeCallJmpBuf)) {
*printf("Heming ExternalDispatcher::runProtectedCall false\n");
* res = false;
} else {
*printf("Heming ExternalDispatcher::runProtectedCall true\n");
* executionEngine->runFunction(f, gvArgs);
res = true;
}
*printf("Heming ExternalDispatcher::runProtectedCall exit\n");*
sigaction(SIGSEGV, &segvActionOld, 0);
return res;
}
--
Regards,
Heming Cui
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20091125/9d8af830/attachment.html
-------------- next part --------------
heming at debug:~/defens/rcs-modules/klee/Debug/bin$ klee islower.o
KLEE: output directory = "klee-out-63"
KLEE: WARNING: undefined reference to function: clone
KLEE: WARNING: undefined reference to function: perror
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: sleep
KLEE: WARNING: calling external: clone(151821976, 3083198472, 0, 0)
Heming ExternalDispatcher::runProtectedCall enter
Heming ExternalDispatcher::runProtectedCall true
Heming ExternalDispatcher::runProtectedCall false
Heming ExternalDispatcher::runProtectedCall exit
KLEE: ERROR: /home/heming/defens/rcs-modules/klee/Debug/bin/islower.c:25:
failed external call: clone
KLEE: NOTE: now ignoring this error at this location
Heming ExternalDispatcher::runProtectedCall exit
KLEE: done: total instructions = 29
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
KLEE: WARNING: calling external: printf(152117768, 19657)
Heming ExternalDispatcher::runProtectedCall enter
Heming ExternalDispatcher::runProtectedCall true
daemon pid = 19657
Heming ExternalDispatcher::runProtectedCall exit
KLEE: done: total instructions = 45
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ExternalDispatcher.cpp
Type: application/octet-stream
Size: 8235 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20091125/9d8af830/attachment.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: islower.c
Type: application/octet-stream
Size: 683 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20091125/9d8af830/attachment-0001.obj
