[klee-dev] Ask for help with Error when apply KLEE to Busybox1.21.0

[Daniel Liew]

Your problem is your build of busybox has inline assembly which KLEE
cannot handle. You will need to figure out how to build busybox with
as little assembly as possible. Busybox might provide a configuration
option that allows you to use generic versions of functions instead of
architecture specific ones. I cannot help you with this.

Thanks,
Dan.

On 29 November 2013 03:45, Wang Shuai <waishuai at hotmail.com> wrote:
> On 11/28/2013 08:25 PM, Daniel Liew wrote:
>> Read the error message, the compiler doesn't work, you should read the
>> generated config.log to find out why it doesn't work.
>>
>> You can also check what happens when you try to compile a simple C program
>> $ export LLVM_COMPILER=llvm-gcc
>> $ export WLLVM_OUTPUT=debug
>> $ export LLVM_COMPILER_PATH=/home/user/llvm_and_clang/Debug+Asserts/bin
>> $ wllvm -c hello_world.c
>> $ wllvm hello_world.o -o hello_world
>>
>> Most likely something isn't configured properly.
> Hi Daniel,
>
> I was able to run wllvm and make step was successful, too. The LLVM
> bitcode" busybox_unstripped.bc" was generated after I ran "extract-bc
> busybox_unstripped" in the console. But when using KLEE to test
> "printf", I followed the instructions below:
>
> wang at wang:~/work/projects/busybox-1.21.0/obj-klee$ klee --libc=uclibc
> --posix-runtime ./busybox_unstripped.bc printf --help
> KLEE: NOTE: Using model:
> /home/wang/work/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-2"
> WARNING: this target does not support the llvm.stacksave intrinsic.
> KLEE: WARNING ONCE: function "lbb_prepare" has inline asm
> KLEE: WARNING ONCE: function "getty_main" has inline asm
> KLEE: WARNING ONCE: function "makemime_main" has inline asm
> KLEE: WARNING ONCE: function "popmaildir_main" has inline asm
> KLEE: WARNING ONCE: function "reformime_main" has inline asm
> KLEE: WARNING ONCE: function "sendmail_main" has inline asm
> KLEE: WARNING ONCE: function "conspy_main" has inline asm
> KLEE: WARNING ONCE: function "fbsplash_main" has inline asm
> KLEE: WARNING ONCE: function "less_main" has inline asm
> KLEE: WARNING ONCE: function "modprobe_main" has inline asm
> KLEE: WARNING ONCE: function "httpd_main" has inline asm
> KLEE: WARNING ONCE: function "ifenslave_main" has inline asm
> KLEE: WARNING ONCE: function "ifplugd_main" has inline asm
> KLEE: WARNING ONCE: function "nc_main" has inline asm
> KLEE: WARNING ONCE: function "netstat_main" has inline asm
> KLEE: WARNING ONCE: function "ntpd_main" has inline asm
> KLEE: WARNING ONCE: function "telnetd_main" has inline asm
> KLEE: WARNING ONCE: function "common_traceroute_main" has inline asm
> KLEE: WARNING ONCE: function "wget_main" has inline asm
> KLEE: WARNING ONCE: function "dhcprelay_main" has inline asm
> KLEE: WARNING ONCE: function "udhcp_sp_fd_set" has inline asm
> KLEE: WARNING ONCE: function "iostat_main" has inline asm
> KLEE: WARNING ONCE: function "mpstat_main" has inline asm
> KLEE: WARNING ONCE: function "nmeter_main" has inline asm
> KLEE: WARNING ONCE: function "cpuid" has inline asm
> KLEE: WARNING ONCE: function "powertop_main" has inline asm
> KLEE: WARNING ONCE: function "pstree_main" has inline asm
> KLEE: WARNING ONCE: function "svlogd_main" has inline asm
> KLEE: WARNING ONCE: function "raise_exception" has inline asm
> KLEE: WARNING ONCE: function "outstr" has inline asm
> KLEE: WARNING ONCE: function "int_on" has inline asm
> KLEE: WARNING ONCE: function "flush_stdout_stderr" has inline asm
> KLEE: WARNING ONCE: function "outcslow" has inline asm
> KLEE: WARNING ONCE: function "out1fmt" has inline asm
> KLEE: WARNING ONCE: function "fmtstr" has inline asm
> KLEE: WARNING ONCE: function "stalloc" has inline asm
> KLEE: WARNING ONCE: function "popstackmark" has inline asm
> KLEE: WARNING ONCE: function "growstackblock" has inline asm
> KLEE: WARNING ONCE: function "setvar" has inline asm
> KLEE: WARNING ONCE: function "setvarsafe" has inline asm
> KLEE: WARNING ONCE: function "unsetvar" has inline asm
> KLEE: WARNING ONCE: function "listsetvar" has inline asm
> KLEE: WARNING ONCE: function "setpwd" has inline asm
> KLEE: WARNING ONCE: function "docd" has inline asm
> KLEE: WARNING ONCE: function "setalias" has inline asm
> KLEE: WARNING ONCE: function "unalias" has inline asm
> KLEE: WARNING ONCE: function "rmaliases" has inline asm
> KLEE: WARNING ONCE: function "freejob" has inline asm
> KLEE: WARNING ONCE: function "restartjob" has inline asm
> KLEE: WARNING ONCE: function "dowait" has inline asm
> KLEE: WARNING ONCE: function "clear_traps" has inline asm
> KLEE: WARNING ONCE: function "waitforjob" has inline asm
> KLEE: WARNING ONCE: function "redirect" has inline asm
> KLEE: WARNING ONCE: function "popredir" has inline asm
> KLEE: WARNING ONCE: function "redirectsafe" has inline asm
> KLEE: WARNING ONCE: function "ash_arith" has inline asm
> KLEE: WARNING ONCE: function "recordregion" has inline asm
> KLEE: WARNING ONCE: function "removerecordregions" has inline asm
> KLEE: WARNING ONCE: function "force_int_on" has inline asm
> KLEE: WARNING ONCE: function "expbackq" has inline asm
> KLEE: WARNING ONCE: function "ifsfree" has inline asm
> KLEE: WARNING ONCE: function "expandmeta" has inline asm
> KLEE: WARNING ONCE: function "clearcmdentry" has inline asm
> KLEE: WARNING ONCE: function "delete_cmd_entry" has inline asm
> KLEE: WARNING ONCE: function "defun" has inline asm
> KLEE: WARNING ONCE: function "dotrap" has inline asm
> KLEE: WARNING ONCE: function "evaltree" has inline asm
> KLEE: WARNING ONCE: function "evalsubshell" has inline asm
> KLEE: WARNING ONCE: function "evalpipe" has inline asm
> KLEE: WARNING ONCE: function "evalfun" has inline asm
> KLEE: WARNING ONCE: function "mklocal" has inline asm
> KLEE: WARNING ONCE: function "evalcommand" has inline asm
> KLEE: WARNING ONCE: function "pushstring" has inline asm
> KLEE: WARNING ONCE: function "popstring" has inline asm
> KLEE: WARNING ONCE: function "popfile" has inline asm
> KLEE: WARNING ONCE: function "setinputfile" has inline asm
> KLEE: WARNING ONCE: function "setinputstring" has inline asm
> KLEE: WARNING ONCE: function "shiftcmd" has inline asm
> KLEE: WARNING ONCE: function "setcmd" has inline asm
> KLEE: WARNING ONCE: function "readtoken1" has inline asm
> KLEE: WARNING ONCE: function "find_command" has inline asm
> KLEE: WARNING ONCE: function "trapcmd" has inline asm
> KLEE: WARNING ONCE: function "readcmd" has inline asm
> KLEE: WARNING ONCE: function "umaskcmd" has inline asm
> KLEE: WARNING ONCE: function "ash_main" has inline asm
> KLEE: WARNING ONCE: function "hush_main" has inline asm
> KLEE: WARNING ONCE: function "syslogd_main" has inline asm
> KLEE: WARNING ONCE: function "acpid_main" has inline asm
> KLEE: WARNING ONCE: function "fdisk_main" has inline asm
> KLEE: WARNING ONCE: function "fsck_minix_main" has inline asm
> KLEE: WARNING ONCE: function "mkfs_minix_main" has inline asm
> KLEE: WARNING ONCE: function "gzip_main" has inline asm
> KLEE: WARNING ONCE: function "showkey_main" has inline asm
> KLEE: WARNING ONCE: function "test_main" has inline asm
> KLEE: WARNING ONCE: function "awk_main" has inline asm
> KLEE: WARNING ONCE: function "diff_main" has inline asm
> KLEE: WARNING ONCE: function "ed_main" has inline asm
> KLEE: WARNING ONCE: function "patch_main" has inline asm
> KLEE: WARNING ONCE: function "vi_main" has inline asm
> KLEE: WARNING ONCE: function "read_line_input" has inline asm
> KLEE: WARNING ONCE: function "__dns_lookup" has inline asm
> KLEE: WARNING: undefined reference to function: __cmsg_nxthdr
> KLEE: WARNING: undefined reference to function: __res_state
> KLEE: WARNING: undefined reference to function: __sigsetjmp
> KLEE: WARNING: undefined reference to function: __syscall_ipc
> KLEE: WARNING: undefined reference to function: __xstat64
> KLEE: WARNING: undefined reference to function: acct
> KLEE: WARNING: undefined reference to function: adjtimex
> KLEE: WARNING: undefined reference to function: alarm
> KLEE: WARNING: undefined reference to function: atan2
> KLEE: WARNING: undefined reference to function: bindresvport
> KLEE: WARNING: undefined reference to function: cos
> KLEE: WARNING: undefined reference to function: creat64
> KLEE: WARNING: undefined reference to function: delete_module
> KLEE: WARNING: undefined reference to function: ether_hostton
> KLEE: WARNING: undefined reference to function: exp
> KLEE: WARNING: undefined reference to function: fabs
> KLEE: WARNING: undefined reference to function: flock
> KLEE: WARNING: undefined reference to function: getdomainname
> KLEE: WARNING: undefined reference to function: getrpcbyname
> KLEE: WARNING: undefined reference to function: getsid
> KLEE: WARNING: undefined reference to function: init_module
> KLEE: WARNING: undefined reference to function: klogctl
> KLEE: WARNING: undefined reference to function: log
> KLEE: WARNING: undefined reference to function: malloc_trim
> KLEE: WARNING: undefined reference to function: mallopt
> KLEE: WARNING: undefined reference to function: nice
> KLEE: WARNING: undefined reference to function: personality
> KLEE: WARNING: undefined reference to function: pivot_root
> KLEE: WARNING: undefined reference to function: pmap_set
> KLEE: WARNING: undefined reference to function: pmap_unset
> KLEE: WARNING: undefined reference to function: poll
> KLEE: WARNING: undefined reference to function: pow
> KLEE: WARNING: undefined reference to function: sched_get_priority_max
> KLEE: WARNING: undefined reference to function: sched_get_priority_min
> KLEE: WARNING: undefined reference to function: sched_getparam
> KLEE: WARNING: undefined reference to function: sched_getscheduler
> KLEE: WARNING: undefined reference to function: sched_setscheduler
> KLEE: WARNING: undefined reference to function: sched_yield
> KLEE: WARNING: undefined reference to function: sendfile64
> KLEE: WARNING: undefined reference to function: siglongjmp
> KLEE: WARNING: undefined reference to function: sigsuspend
> KLEE: WARNING: undefined reference to function: sin
> KLEE: WARNING: undefined reference to function: sqrt
> KLEE: WARNING: undefined reference to function: stime
> KLEE: WARNING: undefined reference to function: sysinfo
> KLEE: WARNING: executable has module level assembly (ignoring)
> KLEE: WARNING ONCE: calling external: syscall(54, 0, 21505, 240663360)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> KLEE: WARNING ONCE: calling external: __xstat64(3, 240194008, 240675168)
> KLEE: WARNING ONCE: calling external: mallopt(4294967295, 8192)
> KLEE: ERROR: inline assembly is unsupported
> KLEE: NOTE: now ignoring this error at this location
>
> KLEE: done: total instructions = 10243
> KLEE: done: completed paths = 1
> KLEE: done: generated tests = 1
>
>
> Is my operations right? I see there is an error. I'm not sure that KLEE
> worked correctly. In the experiment, only "busybox_unstripped.bc" was
> generated unlike the test of GNU Coreutils whose each utilities had one.
> Could you tell me how to test the utilities like "printf" in busybox1.21.0?
>
>
>
>
>
>
>
>>
>> On 28 November 2013 07:59, Wang Shuai <waishuai at hotmail.com> wrote:
>>> On 11/27/2013 09:31 PM, Daniel Liew wrote:
>>>> The error message is telling you that the argparse module is missing.
>>>> This module is a command line argument parser in Python >=2.7. Because
>>>> that module is missing it probably means your version of python is
>>>> VERY OUT OF DATE (you can check your version by running python
>>>> --version) to use wllvm. If it's out of date you should upgrade!
>>>>
>>>> If you don't want to install a newer version of python then you can
>>>> try to use the older version of extract-bc that doesn't have an
>>>> argument parser (
>>>> https://github.com/travitch/whole-program-llvm/blob/1256a2e6c5e64fcac97758eeb723d2de47f3d5ce/extract-bc
>>>> ). I make no guarantees that this will work.
>>>>
>>>> Hope that helps,
>>>> Dan.
>>>     I followed your advice and changed my OS to ubuntu12.04 which has
>>> python2.7.3. But after I set up the wllvm, I tried to "CC=wllvm
>>> ./configure" in the "gzip1.6 "directory. Something was wrong:
>>>
>>> checking for a BSD-compatible install... /usr/bin/install -c
>>> checking whether build environment is sane... yes
>>> checking for a thread-safe mkdir -p... /bin/mkdir -p
>>> checking for gawk... no
>>> checking for mawk... mawk
>>> checking whether make sets $(MAKE)... yes
>>> checking whether make supports nested variables... yes
>>> checking whether make supports nested variables... (cached) yes
>>> checking for style of include used by make... GNU
>>> checking for gcc... /home/wang/work/wllvm-gcc/wllvm
>>> checking whether the C compiler works... no
>>> configure: error: in `/home/wang/work/projects/gzip-1.6':
>>> configure: error: C compiler cannot create executables
>>> See `config.log' for more details
>>>
>>> I never met this error in my previous OS. Also, LLVM_GCC works well. Why
>>> would this happen? Thank you very much.
>>>> On 27 November 2013 12:28, Wang Shuai <waishuai at hotmail.com> wrote:
>>>>> On 11/27/2013 01:52 PM, Daniel Liew wrote:
>>>>>
>>>>> Hi,
>>>>>
>>>>> I would advise using my fork [1] of wllvm instead of klee-gcc for
>>>>> building programs to LLVM bitcode.
>>>>>
>>>>> I don't quite have the same error as you when I use wllvm. Instead I see ...
>>>>>
>>>>> ```
>>>>>
>>>>> Failed: -Wl,--start-group -lm -Wl,--end-group
>>>>>
>>>>>
>>>>>                    [76/1831]
>>>>> Output of:
>>>>> wllvm -fnested-functions -Wall -Wshadow -Wwrite-strings -Wundef
>>>>> -Wstrict-prototypes -Wunused -Wunused-parameter -Wunused-function
>>>>> -Wunused-value -Wmissing-prototypes -Wmissing-declarations
>>>>> -Wno-format-security -Wdeclaration-after-statement
>>>>>    -Wold-style-definition -fno-builtin-strlen -finline-limit=0
>>>>> -fomit-frame-pointer -ffunction-sections -fdata-sections
>>>>> -fno-guess-branch-probability -funsigned-char -static-libgcc
>>>>> -falign-functions=1 -falign-jumps=1 -falign-labels=1 -falign
>>>>> -loops=1 -fno-unwind-tables -fno-asynchronous-unwind-tables -Os -o
>>>>> busybox_unstripped -Wl,--sort-common -Wl,--sort-section,alignment
>>>>> -Wl,--gc-sections -Wl,--start-group applets/built-in.o archival/lib.a
>>>>> archival/libarchive/lib.a console-to
>>>>> ols/lib.a coreutils/lib.a coreutils/libcoreutils/lib.a
>>>>> debianutils/lib.a e2fsprogs/lib.a editors/lib.a findutils/lib.a
>>>>> init/lib.a libbb/lib.a libpwdgrp/lib.a loginutils/lib.a
>>>>> mailutils/lib.a miscutils/lib.a modutils/lib.a networking/lib.a
>>>>> networking/libiproute/lib.a networking/udhcp/lib.a printutils/lib.a
>>>>> procps/lib.a runit/lib.a selinux/lib.a shell/lib.a sysklogd/lib.a
>>>>> util-linux/lib.a util-linux/volume_id/lib.a archival/built-in.o
>>>>> archival/libarchive/built-in.o console-to
>>>>> ols/built-in.o coreutils/built-in.o coreutils/libcoreutils/built-in.o
>>>>> debianutils/built-in.o e2fsprogs/built-in.o editors/built-in.o
>>>>> findutils/built-in.o init/built-in.o libbb/built-in.o
>>>>> libpwdgrp/built-in.o loginutils/built-in.o mailutils
>>>>> /built-in.o miscutils/built-in.o modutils/built-in.o
>>>>> networking/built-in.o networking/libiproute/built-in.o
>>>>> networking/udhcp/built-in.o printutils/built-in.o procps/built-in.o
>>>>> runit/built-in.o selinux/built-in.o shell/built-in.o sysklogd/b
>>>>> uilt-in.o util-linux/built-in.o util-linux/volume_id/built-in.o
>>>>> -Wl,--end-group -Wl,--start-group -lm -Wl,--end-group
>>>>> ==========
>>>>> networking/lib.a(inetd.o): In function `inetd_main':
>>>>> networking/inetd.c:(.text.inetd_main+0x261): undefined reference to
>>>>> `__FDELT'
>>>>> networking/inetd.c:(.text.inetd_main+0x275): undefined reference to
>>>>> `__FDMASK'
>>>>>
>>>>> ...
>>>>> ```
>>>>>
>>>>> The errors I have are macros that expand to something that is not used
>>>>> as a symbol (_FDELT and _FDMASK). This seems to have something to do
>>>>> with llvm-gcc and the macros FD_CLEAR, FD_ISSET, FD_SET and FD_ZERO
>>>>> (in  lib/gcc/x86_64-unknown-linux-gnu/4.2.1/include/bits/select.h ).
>>>>>
>>>>> Anyway the quick way to avoid this issue is to not build the
>>>>> networking part of busybox by running make menuconfig (you may need
>>>>> remove .config file first) and then removing the networking bits and
>>>>> saving your configuration then building.
>>>>>
>>>>> If I do this then I can successfully build busybox using wllvm with
>>>>> llvm-gcc provided I also add to CFLAGS in Makefile.flags
>>>>> -fnested-functions i.e.
>>>>>
>>>>> CFLAGS += -fnested-function
>>>>>
>>>>> Hope that helps,
>>>>> Dan Liew
>>>>>
>>>>> [1] Make sure you use llvm-gcc branch of repository
>>>>> https://github.com/delcypher/whole-program-llvm/tree/llvm-gcc
>>>>>
>>>>> On 27 November 2013 03:29, 王帅 <waishuai at hotmail.com> wrote:
>>>>>
>>>>> Hi guys,
>>>>>      Recently, I'm trying to apply KLEE to busybox1.21.0. I followed the
>>>>> subsequent steps:
>>>>>
>>>>> mkdir obj-klee
>>>>> make -w O=obj-klee defconfig
>>>>> cd obj-klee
>>>>> make CC=klee-gcc LD="llvm-ld --disable-opt" AR=llvm-ar SKIP_STRIP=y V=1
>>>>> make CC=/home/wang/work/klee/scripts/klee-gcc LD="llvm-ld --disable-opt"
>>>>> SKIP_STRIP=y V=1 AR=llvm-ar CFLAGS=-fnested-functions
>>>>>
>>>>>
>>>>>     But,an error happened:
>>>>>
>>>>> ------------------------
>>>>> -------------------------
>>>>> ------------------------
>>>>>
>>>>> Trying libraries: m
>>>>> Failed: -Wl,--start-group -lm -Wl,--end-group
>>>>> Output of:
>>>>> /home/wang/work/klee/scripts/klee-gcc -fnested-functions -o
>>>>> busybox_unstripped -Wl,--start-group applets/built-in.o archival/lib.a
>>>>> archival/libarchive/lib.a console-tools/lib.a coreutils/lib.a
>>>>> coreutils/libcoreutils/lib.a debianutils/lib.a e2fsprogs/lib.a editors/lib.a
>>>>> findutils/lib.a init/lib.a libbb/lib.a libpwdgrp/lib.a loginutils/lib.a
>>>>> mailutils/lib.a miscutils/lib.a modutils/lib.a networking/lib.a
>>>>> networking/libiproute/lib.a networking/udhcp/lib.a printutils/lib.a
>>>>> procps/lib.a runit/lib.a selinux/lib.a shell/lib.a sysklogd/lib.a
>>>>> util-linux/lib.a util-linux/volume_id/lib.a archival/built-in.o
>>>>> archival/libarchive/built-in.o console-tools/built-in.o coreutils/built-in.o
>>>>> coreutils/libcoreutils/built-in.o debianutils/built-in.o
>>>>> e2fsprogs/built-in.o editors/built-in.o findutils/built-in.o init/built-in.o
>>>>> libbb/built-in.o libpwdgrp/built-in.o loginutils/built-in.o
>>>>> mailutils/built-in.o miscutils/built-in.o modutils/built-in.o
>>>>> networking/built-in.o networking/libiproute/built-in.o
>>>>> networking/udhcp/built-in.o printutils/built-in.o procps/built-in.o
>>>>> runit/built-in.o selinux/built-in.o shell/built-in.o sysklogd/built-in.o
>>>>> util-linux/built-in.o util-linux/volume_id/built-in.o -Wl,--end-group
>>>>> -Wl,--start-group -lm -Wl,--end-group
>>>>> ==========
>>>>> llvm-ld: error: Cannot find linker input 'selinux/lib.a'
>>>>> make[2]: *** [busybox_unstripped] Error 1
>>>>> make[1]: *** [_all] Error 2
>>>>> make: *** [all] Error 2
>>>>>
>>>>>
>>>>>     When I check selinux/lib.a, the file is there, but it contains only a
>>>>> single line with: "!<arch>" . Someone can help me ? If any, could you tell
>>>>> me how to solve it? I'm really hurried with this test. Thank you very much
>>>>> for advance!
>>>>>
>>>>> Thank know for your advice! It really helps me. Busybox 1.21.0 build
>>>>> successfully. But when I wanted to use extract-bc busybox_unstripped to
>>>>> generate LLVM bitcode, another error happened
>>>>>
>>>>> Traceback (most recent call last):
>>>>>     File "/home/wang/work/wllvm-gcc/extract-bc", line 269, in <module>
>>>>>       sys.exit(main(sys.argv))
>>>>>     File "/home/wang/work/wllvm-gcc/extract-bc", line 212, in main
>>>>>       import argparse
>>>>> ImportError: No module named argparse
>>>>>
>>>>> I also tried to apply wllvm to gzip1.6. There was the same error. Why? Was
>>>>> there something wrong with my instructions?
>>>>>
>>>>> export LLVM_COMPILER=llvm-gcc
>>>>> export LLVM_COMPILER_PATH=/home/wang/work/llvm-2.9/Release+Asserts/bin
>>>>> export WLLVM_OUTPUT=DEBUG
>>>>>
>>>>> make CC=wllvm defconfig
>>>>> make CC=wllvm
>>>>> extract-bc busybox_unstripped
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>
>