[klee-dev] Fwd: How to test busybox with Klee

[Jian Liu]

I try to test busybox 1.4.2 by Klee, but failed. Anybody can give some
helps. Thanks.

When select the "arp" as target by "make menconfig", I just compile the
target by the following command.

~/tmp/busybox-1.4.24$ make V=1 CC=klee-gcc LD=llvm-ld SKIP_STRIP=y
~/tmp/busybox-1.4.2 $ ~/installed/klee_static.1.22/Release+Asserts/bin/klee
--libc=uclibc --posix-runtime ./busybox_unstripped.bc arp -Ainet
errorLine: 0
KLEE: NOTE: Using model:
/home/guest/installed/klee_static.1.22/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-18"
TAP_InstrumentInstNumber : ./busybox_unstripped.bc
KLEE: WARNING: function "bind" has inline asm
KLEE: WARNING: function "listen" has inline asm
KLEE: WARNING: function "socket" has inline asm
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: klee_get_valuel
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_start(i8* %ap23), !dbg !5247
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_end(i8* %ap23), !dbg !5271
KLEE: WARNING: calling external: syscall(16, 0, 21505, 61417840)
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_start(i8* %ap23), !dbg !5247
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_end(i8* %ap23), !dbg !5271
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: __xstat64(1, 61204336, 61394288)
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_start(i8* %p12)
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_start(i8* %arg12), !dbg !5234
KLEE: WARNING: calling external: vprintf(61059024, 61923648)
busybox_unstripped.bc: !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!!!!some instruction have not been handled!!!!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\
!!!!!!!!!!!!!!   call void @llvm.va_end(i8* %arg89), !dbg !5260
applet not found!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some
instruction have not been handled!!!!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\
!!!!!!!   call void @llvm.va_end(i8* %91), !dbg !5400

!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_end(i8* %p212)
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! !!!!!some instruction have
not been handled!!!!! !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
call v\
oid @llvm.va_end(i8* %p12)

KLEE: done: total instructions = 12136
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

It seems there are some instructions can not be read by KLEE. You know
there is a bug in test case, i.e. "arp -Ainet". In another testing "ls
--version", I got the following info:

~/tmp3/busybox-1.4.2 $
 ~/installed/klee_static.1.22/Release+Asserts/bin/klee --libc=uclibc
--posix-runtime ./busybox_unstripped.bc ls --version
errorLine: 0
KLEE: NOTE: Using model:
/home/guest/installed/klee_static.1.22/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-1"
TAP_InstrumentInstNumber : ./busybox_unstripped.bc
KLEE: WARNING: function "bind" has inline asm
KLEE: WARNING: function "listen" has inline asm
KLEE: WARNING: function "socket" has inline asm
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to variable: applet_name
KLEE: WARNING: undefined reference to function: bb_show_usage
KLEE: WARNING: undefined reference to function: klee_get_valuel
KLEE: ERROR: unable to load symbol(applet_name) while initializing globals.

It seems some variables can not initialize. You know, in the above testing,
I delete some libraries, which just contain "!<arch>", cannot be read by
llvm-ld.

      Jian LIU
----
email to: gjk.liu at gmail.com


2013/2/27 Cristian Cadar <c.cadar at imperial.ac.uk>

> Hi, please send your questions directly to the klee-dev mailing list, this
> way other people might be able to answer when I am not available, and other
> users/developers could also benefit from the answers.
>
> Cristian
>
>
> On 27/02/2013 14:49, Jian Liu wrote:
>
>> Hi guys,
>>
>>         I just get the reply from Cristian. He give a simple direction
>> for our experiments. Could forward your problems to him? Cristian is now
>> the maintainer of KLEE and his advice would be valuable in the
>> community:-)
>>
>>         Chees,
>>
>>        Jian LIU
>> ----
>> Associate Professor of Institute of Software,
>> Chinese Academy of Sciences, Beijing China
>>
>> email to: gjk.liu at gmail.com <mailto:gjk.liu at gmail.com>
>>
>>
>>
>> ---------- Forwarded message ----------
>> From: *Cristian Cadar* <c.cadar at imperial.ac.uk
>> <mailto:c.cadar at imperial.ac.uk**>>
>> Date: 2013/2/27
>> Subject: Re: How to test busybox with Klee
>> To: "gjk.liu at gmail.com <mailto:gjk.liu at gmail.com>" <gjk.liu at gmail.com
>> <mailto:gjk.liu at gmail.com>>
>>
>>
>> Hi Jian,
>>
>> You should simply replace all the build commands with LLVM equivalents:
>> e.g., gcc with llvm-gcc, ld with llvm-ld, etc.
>>
>> Best,
>> Cristian
>>
>>
>> On 26/02/2013 05:44, gjk.liu at gmail.com <mailto:gjk.liu at gmail.com> wrote:
>>
>>     Hi Cristian,
>>
>>             I want test busybox 1.4.2 with Klee, just like your work in
>>     OSDI paper. But there are some errors when compiling and running
>>     steps. I want to know if you have met such problems and how to deal
>>     with them. I think we should change the Makefiles to this work. But
>>     I have no any ideas about it. Could you share your codes with me?
>>     Thanks.
>>
>>             Best,
>>
>>             Jian
>>
>>
-------------- next part --------------
HTML attachment scrubbed and removed