[klee-dev] Fwd: whole-program-llvm

[Zhiyi Zhang]

---------- Forwarded message ----------
From: Zhiyi Zhang <xianlingzibiying at gmail.com>
Date: Fri, Mar 20, 2015 at 4:45 PM
Subject: Re: [klee-dev] whole-program-llvm
To: Dan Liew <dan at su-root.co.uk>


Hi,

I get .bc files with your help. Thank you very much.

However , when I run echo.bc with the order *klee ./echo.bc*, the output is
as following:

*KLEE: output directory is
"/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/./klee-out-6"*
*KLEE: WARNING ONCE: function "vasnprintf" has inline asm*
*KLEE: WARNING: undefined reference to function: __ctype_b_loc*
*KLEE: WARNING: undefined reference to function: __ctype_get_mb_cur_max*
*KLEE: WARNING: undefined reference to function: __errno_location*
*KLEE: WARNING: undefined reference to function: __fpending*
*KLEE: WARNING: undefined reference to function: __overflow*
*KLEE: WARNING: undefined reference to function: atexit*
*KLEE: WARNING: undefined reference to function: bindtextdomain*
*KLEE: WARNING: undefined reference to function: dcgettext*
*KLEE: WARNING: undefined reference to function: fclose*
*KLEE: WARNING: undefined reference to function: fprintf*
*KLEE: WARNING: undefined reference to function: fputs_unlocked*
*KLEE: WARNING: undefined reference to function: fwrite*
*KLEE: WARNING: undefined reference to function: getenv*
*KLEE: WARNING: undefined reference to function: getopt_long*
*KLEE: WARNING: undefined reference to function: iswprint*
*KLEE: WARNING: undefined reference to function: mbrtowc*
*KLEE: WARNING: undefined reference to function: mbsinit*
*KLEE: WARNING: undefined reference to function: memcmp*
*KLEE: WARNING: undefined reference to variable: opterr*
*KLEE: WARNING: undefined reference to variable: optind*
*KLEE: WARNING: undefined reference to function: printf*
*KLEE: WARNING: undefined reference to function: setlocale*
*KLEE: WARNING: undefined reference to function: snprintf*
*KLEE: WARNING: undefined reference to variable: stderr*
*KLEE: WARNING: undefined reference to variable: stdout*
*KLEE: WARNING: undefined reference to function: strlen*
*KLEE: WARNING: undefined reference to function: textdomain*
*KLEE: WARNING: undefined reference to function: error (UNSAFE)!*
*KLEE: WARNING ONCE: calling external: getenv(176076616)*
*KLEE: WARNING ONCE: calling external: setlocale(6, 176076944)*
*KLEE: ERROR:
/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/../../src/echo.c:138:
external modified read-only object*
*KLEE: NOTE: now ignoring this error at this location*

*KLEE: done: total instructions = 6*
*KLEE: done: completed paths = 1*
*KLEE: done: generated tests = 1*

Then I use the order* klee --licb=uclibc --posix-runtime ./echo.bc
--sym-arg 3,*the output is as following:

*KLEE: NOTE: Using klee-uclibc :
/home/loveling10/klee/build/Release+Asserts/lib/klee-uclibc.bca*
*KLEE: NOTE: Using model:
/home/loveling10/klee/build/Release+Asserts/lib/libkleeRuntimePOSIX.bca*
*KLEE: output directory is
"/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/./klee-out-7"*
*KLEE: WARNING ONCE: function "vasnprintf" has inline asm*
*KLEE: WARNING: undefined reference to function: __ctype_b_loc*
*KLEE: WARNING: undefined reference to function: __overflow*
*KLEE: WARNING: undefined reference to function: bindtextdomain*
*KLEE: WARNING: undefined reference to function: dcgettext*
*KLEE: WARNING: undefined reference to function: textdomain*
*KLEE: WARNING: executable has module level assembly (ignoring)*
*KLEE: WARNING ONCE: calling external: syscall(54, 0, 21505, 185983048)*
*KLEE: WARNING ONCE: calling __user_main with extra arguments.*
*KLEE: WARNING ONCE: calling external: bindtextdomain(181575080, 181575016)*
*KLEE: WARNING ONCE: calling external: textdomain(181575080)*
*KLEE: WARNING ONCE: calling external: __overflow(181649140, 10)*
*KLEE: ERROR: /usr/include/i386-linux-gnu/bits/stdio.h:107: failed external
call: __overflow*
*KLEE: NOTE: now ignoring this error at this location*


*Segmentation fault (core dumped)*
Do these errors mean the klee linking still has the wrong?

Thank you very much
Zhiyi Zhang

On Thu, Mar 19, 2015 at 11:33 PM, Dan Liew <dan at su-root.co.uk> wrote:

> Hi,
>
> > Exception: Could not find ".llvm_bc" ELF section in
> > "/home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/base64"
>
> You probably didn't use whole-program-llvm for your compilation
> process if you see this message. You should check if ``make`` was
> actually using wllvm, my guess it wasn't (try ``make --just-print``)
>
> It's just a guess but you should probably be passing CC and CXX to the
> configure commands rather than just make
>
> ```
> export WLLVM_OUTPUT=DEBUG
> export CC=wllvm
> export CXX=wllvm++
>  ../configure --disable-nls CFLAGS="-g"
> make
> ```
>
> The ``export WLLVM_OUTPUT=DEBUG`` will cause wllvm to emit lots of
> debuggin information when it runs.
>
-------------- next part --------------
HTML attachment scrubbed and removed