Hi Paul, Do you mean that the error of "out of bound" at line 160 in host.c is a false positive? Yunfei said to me there are many similar errors in his testing of wget and most of them are related to string operations. If it is true, we should doubt the precision of KLEE for string operations.
Best, Jian 在 2011-10-27，22:19，Paul Marinescu <[email protected]> 写道： > Hi, > Most likely this is an invalid memory access which doesn't show up when > running the program natively (which is what klee-replay does). > > Best, > Paul > > On 26/10/11 04:15, [email protected] wrote: >> Hi, >> Now, I am studying klee and use it to test some programs. >> I test wget and find a bug, but there is something I can't understand >> clearly. >> the step I do the experiments is listed as below: >> >> 1) I compiler the wget program and get wget.bc file. >> then >> 2)yun@yun-pc:~/wget-1.5.3/obj/src$ klee --libc=uclibc --posix-runtime >> ./wget.bc >> www.google.com >> the output of klee show that there is a bug in host.c file because of >> bound of >> out of bound pointer. >> >> *********************************************************************************************************** >> yun@yun-pc:~/wget-1.5.3/obj/src$ klee --libc=uclibc --posix-runtime ./wget.bc >> www.google.com >> [00000.036] Cloud9: Debug: Using Klee path /home/yun/cloud/cloud9 >> [00000.036] Cloud9: Debug: Using uClibc path /home/yun/cloud/uclibc >> [00000.121] Cloud9: Debug: Using uClibc path /home/yun/cloud/uclibc >> [00000.122] Cloud9: Debug: Using Klee path /home/yun/cloud/cloud9 >> KLEE: NOTE: Using model: >> /home/yun/cloud/cloud9/Release+Asserts/lib/libkleeRuntimePOSIX.bca >> [00000.199] Cloud9: Debug: Using Klee path /home/yun/cloud/cloud9 >> KLEE: output directory = "klee-out-0" >> [00000.199] Cloud9: Info: Instrumentation started >> WARNING: this target does not support the llvm.stacksave intrinsic. >> KLEE: WARNING: function "iwrite" has inline asm >> KLEE: WARNING: function "iread" has inline asm >> KLEE: WARNING: function "acceptport" has inline asm >> KLEE: WARNING: undefined reference to function: __ctype_b_loc >> KLEE: WARNING: undefined reference to function: __ctype_tolower_loc >> KLEE: WARNING: undefined reference to function: __ctype_toupper_loc >> KLEE: WARNING: undefined reference to function: __libc_fcntl >> KLEE: WARNING: undefined reference to function: bindtextdomain >> KLEE: WARNING: undefined reference to function: dcgettext >> KLEE: WARNING: undefined reference to function: gethostbyaddr >> KLEE: WARNING: undefined reference to function: gethostbyname >> KLEE: WARNING: undefined reference to function: snprintf >> KLEE: WARNING: undefined reference to function: textdomain >> KLEE: WARNING: undefined reference to function: kill (UNSAFE)! >> KLEE: WARNING: calling external: stat(140052474042240, 140052474050912) >> KLEE: WARNING: calling external: syscall(5, 1, 140052474054304) >> KLEE: WARNING: calling external: snprintf(140052474048704, 16, >> 140052474048832, >> 140052474048896, 0) >> KLEE: WARNING: _ioctl_file: operation not supported on symbolic files >> KLEE: WARNING: calling __user_main298 with extra arguments. >> KLEE: WARNING: calling __user_main with extra arguments. >> KLEE: WARNING: calling external: bindtextdomain(140052473969440, >> 140052473969504) >> KLEE: WARNING: calling external: textdomain(140052473969440) >> KLEE: WARNING: signal: silently ignoring >> KLEE: WARNING: calling external: __ctype_toupper_loc() >> Attempting to open: /etc/TZ >> --17:03:26-- http://www.google.com:80/ >> => `index.html.3' >> KLEE: WARNING: calling external: dcgettext(0, 140052473950368, 5) >> Connecting to www.google.com:80... KLEE: WARNING: calling external: >> gethostbyname(140052474229248) >> KLEE: ERROR: /home/yun/cloud/wget-1.5.3/obj/src/../../src/host.c:160: memory >> error: >> out of bound pointer >> KLEE: NOTE: now ignoring this error at this location >> [00001.008] Cloud9: Debug: Code coverage is 0/0 (local) and 0/0 >> (global)... >> >> KLEE: done: total instructions = 247972 >> KLEE: done: completed paths = 3 >> KLEE: done: generated tests = 1 >> [00002.001] Cloud9: Info: Instrumentation interrupted. Stopping. >> ************************************************************************************************************* >> >> 3) yun@yun-pc:~/wget-1.5.3/obj/src$ klee-replay ./wget >> ./klee-last/test000001.ktest >> the output of klee show that there is no error and the execution of >> program is >> normal >> ************************************************************************************************************** >> yun@yun-pc:~/wget-1.5.3/obj/src$ klee-replay ./wget >> ./klee-last/test000001.ktest >> WARNING: klee_assume(0)! >> klee-replay: TEST CASE: ./klee-last/test000001.ktest >> klee-replay: ARGS: "./wget" "www.google.com" >> --11:16:21-- http://www.google.com:80/ >> => `index.html.3' >> Connecting to www.google.com:80... connected! >> HTTP request sent, awaiting response... 302 Found >> Location: >> http://www.google.com.hk/url?sa=p&hl=zh-CN&pref=hkredirect&pval=yes&q=http://www.google.com.hk/&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg >> [following] >> --11:16:21-- >> http://www.google.com.hk:80/url?sa=p&hl=zh-CN&pref=hkredirect&pval=yes&q=http%3A/www.google.com.hk/&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg >> => `&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg' >> Connecting to www.google.com.hk:80... connected! >> HTTP request sent, awaiting response... 200 OK >> Length: unspecified [text/html] >> >> 0K -> . >> >> 11:16:21 (1.10 MB/s) - >> `&ust=1319599011889039&usg=AFQjCNE2wsk6e-Y-pUCHPK7GX-HOg_0AWg' saved [1155] >> >> klee-replay: EXIT STATUS: NORMAL (0 seconds) >> *************************************************************************************************************** >> >> So I think this is a false bug report or there is something else I don't >> understand >> it clearly >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
