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

[Daniel Liew]

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.