[klee-dev] KLEE ERROR (Coreutils): failed external call: klee_init_env

[Oswaldo Olivo]

Hi,
I get an empty output from:

llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca | grep
klee_init_env


I tried recompiling UCLIBC, like the getting started tutorial says, and I
don't really get any errors after make.
However, I do get a suspicious warning :

cc1: warning: unrecognized gcc debugging option: N


The output after make looks like this:
__________________________________
./extra/scripts/conf-header.sh .config > include/bits/uClibc_config.h
cc1: warning: unrecognized gcc debugging option: N
make locale_headers
zcat extra/locale/uClibc-locale-030818.tgz | tar -xv -C extra/locale/ -f -
c8tables.h
locale_data.c
locale_mmap.h

.............
.............

CC libc/unistd/usleep.os
CC libc/misc/internals/__uClibc_main.os
CC libc/stdlib/atexit.os
STRIP -x -R .note -R .comment lib/libc.a
AR cr lib/libc.a
_________________________________

Thanks for your help.
Regards,
 Oswaldo.


On Sun, Sep 15, 2013 at 10:37 AM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> Hi,
>
> It seems that the POSIX runtime library (libkleeRuntimePOSIX.bca) is
> linked in as you would get an assertion error if it was not. However
> the call to klee_init_env() should not fail and should not be treated
> as an external.
>
> The first thing I would check is that klee_init_env is present in
> libkleeRuntimePOSIX.bca by doing
>
> $ llvm-nm Debug+Asserts/lib/libkleeRuntimePOSIX.bca/libkleeRuntimePOSIX.bca
> | grep klee_init_env
> Debug+Asserts/lib/libkleeRuntimePOSIX.bca(klee_init_env.b):
>          T klee_init_env
>
> Note I built the POSIX runtime library as debug so your output may be
> slightly different but llvm-nm should show that klee_init_env is in
> the "text section" (T). If klee_init_env is missing or is not in the
> text section (.e.g (U) undefined) then libkleeRuntimePOSIX.bca didn't
> built correctly.
>
> If libkleeRuntimePOSIX.bca did built correctly the next thing to look
> at is the linking performed by KLEE. Take a look at
> klee-last/assembly.ll . This file is generated when you run klee and
> it is the llvm bitcode module (i.e. KLEE has already done all the
> linking necessary) that klee will interpret.
>
> You should find that somewhere in user_main() a call is made to
> klee_init_env e.g.
>
> define i32 @__user_main(i32 %argc, i8** %argv) nounwind {
> entry:
>   %argcPtr = alloca i32
>   %argvPtr = alloca i8**
>   store i32 %argc, i32* %argcPtr
>   store i8** %argv, i8*** %argvPtr
>   call void @klee_init_env(i32* %argcPtr, i8*** %argvPtr)
>   ...
> }
>
> and that there is a declaration of klee_init_env in the module too
>
> define void @klee_init_env(i32* nocapture %argcPtr, i8*** nocapture
> %argvPtr) nounwind {
> entry:
>   %new_argv = alloca [1024 x i8*], align 8
>   %sym_arg_name = alloca [5 x i8], align 1
>   ....
> }
>
> Your output implies that there is no declaration of klee_init_env() in
> assembly.ll but you should check this.
>
> Hope this helps.
>
> Thanks,
> Dan Liew.
>
> On 14 September 2013 23:07, Oswaldo Olivo <ozzyo86 at gmail.com> wrote:
> > Hi,
> >
> > I have followed the steps for compiling Klee, UCLIBC, STP and Coreutils
> > given
> > in :
> >
> > http://klee.llvm.org/GetStarted.html
> >
> > and
> >
> > http://klee.llvm.org/TestingCoreutils.html
> >
> > After running the command from step 3 of the coreutils tutorial:
> >
> > klee --libc=uclibc --posix-runtime ./cat.bc --version
> >
> >
> > I get the following output, with the error "failed external call:
> > klee_init_env"  :
> > ____________________________________________
> >
> > KLEE: NOTE: Using model:
> > /home/oswaldo/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> > KLEE: output directory = "klee-out-8"
> > KLEE: WARNING: undefined reference to function: __syscall_rt_sigaction
> > KLEE: WARNING: undefined reference to function: close
> > KLEE: WARNING: undefined reference to function: close_stdout
> > KLEE: WARNING: undefined reference to function: fcntl
> > KLEE: WARNING: undefined reference to function: fstat
> > KLEE: WARNING: undefined reference to function: fstat64
> > KLEE: WARNING: undefined reference to function: full_write
> > KLEE: WARNING: undefined reference to function: ioctl
> > KLEE: WARNING: undefined reference to function: klee_div_zero_check
> > KLEE: WARNING: undefined reference to function: klee_init_env
> > KLEE: WARNING: undefined reference to function: lseek
> > KLEE: WARNING: undefined reference to function: lseek64
> > KLEE: WARNING: undefined reference to function: memmove
> > KLEE: WARNING: undefined reference to function: open
> > KLEE: WARNING: undefined reference to function: open64
> > KLEE: WARNING: undefined reference to function: quote
> > KLEE: WARNING: undefined reference to function: read
> > KLEE: WARNING: undefined reference to function: readlink
> > KLEE: WARNING: undefined reference to function: safe_read
> > KLEE: WARNING: undefined reference to function: version_etc
> > KLEE: WARNING: undefined reference to function: write
> > KLEE: WARNING: undefined reference to function: xmalloc
> > KLEE: WARNING: undefined reference to function: kill (UNSAFE)!
> > KLEE: WARNING: executable has module level assembly (ignoring)
> > KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 176221000)
> > KLEE: WARNING ONCE: calling __user_main with extra arguments.
> > KLEE: WARNING ONCE: calling external: klee_init_env(176196176, 176196064)
> > KLEE: ERROR:
> /home/oswaldo/coreutils-6.11/obj-llvm/src/../../src/cat.c:514:
> > failed external call: klee_init_env
> > KLEE: NOTE: now ignoring this error at this location
> >
> > KLEE: done: total instructions = 9336
> > KLEE: done: completed paths = 1
> > KLEE: done: generated tests = 1
> >
> > ________________________________
> >
> > Any ideas of what the problem is ?
> > Is it not loading posix libraries properly ?
> > I'm compiling this on Ubuntu 12.04.
> > Thanks,
> >  Oswaldo.
>
-------------- next part --------------
HTML attachment scrubbed and removed