KLEE ERROR (Coreutils): failed external call: klee_init

Discussion:

KLEE ERROR (Coreutils): failed external call: klee_init_env

Oswaldo Olivo

2013-09-14 22:07:16 UTC

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.

Daniel Liew

2013-09-15 15:37:28 UTC

Permalink

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.

Post by Oswaldo Olivo
Hi,
I have followed the steps for compiling Klee, UCLIBC, STP and Coreutils
given
http://klee.llvm.org/GetStarted.html
and
http://klee.llvm.org/TestingCoreutils.html
klee --libc=uclibc --posix-runtime ./cat.bc --version
____________________________________________
/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)
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.

Oswaldo Olivo

2013-09-15 20:36:57 UTC

Permalink

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.

Post by 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
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.
%argcPtr = alloca i32
%argvPtr = alloca i8**
store i32 %argc, i32* %argcPtr
store i8** %argv, i8*** %argvPtr
...
}
and that there is a declaration of klee_init_env in the module too
%argvPtr) nounwind {
%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.

Daniel Liew

2013-09-15 20:53:12 UTC

Permalink

Post by Oswaldo Olivo
Hi,
llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca | grep
klee_init_env

I should of mentioned that the version of llvm-nm you use must be part
LLVM you built for KLEE (probably LLVM 2.9) else you get blank output.
For example if I use llvm-nm from LLVM3.3 (which is also installed on
my system) on a bitcode archive I see no output

Check that
$ llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca

gives output. If not you're **not** using the version of llvm-nm that
comes with the version of LLVM you built for KLEE.

If you do get output then you need to investigate what went wrong with
your build of the POSIX runtime library.

On my system I can do (after the runtime library is built)

$ llvm-nm ~/klee/runtime/POSIX/Debug+Asserts/klee_init_env.bc
t __get_sym_str
T klee_init_env
U klee_init_fds
U klee_make_symbolic
U klee_mark_global
U klee_prefer_cex
U klee_range
U klee_report_error
U llvm.dbg.declare
U llvm.dbg.value
U llvm.memcpy.p0i8.p0i8.i64
U malloc

If klee_init_env.bc doesn't exist then run the build again
$ cd ~klee/runtime/POSIX
$ make VERBOSE=1

Post by Oswaldo Olivo
I tried recompiling UCLIBC, like the getting started tutorial says, and I
don't really get any errors after make.
cc1: warning: unrecognized gcc debugging option: N

I see that error too, but I uclibc won't build for me right now so I
can't help there.

Hope that helps.

Thanks,
Dan Liew.

Oswaldo Olivo

2013-09-15 21:17:06 UTC

Permalink

Hi,
The problem has been solved.
You were right in the issue about there being version mismatch.
I recompiled KLEE and LLVM, and the POSIX library stopped being empty. I
was probably running
an "outdated" version of KLEE with a newly built version of LLVM 2.9.
Thank you very much.
Regards,
Oswaldo.

Post by Daniel Liew

Post by Oswaldo Olivo
Hi,
llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca | grep
klee_init_env

I should of mentioned that the version of llvm-nm you use must be part
LLVM you built for KLEE (probably LLVM 2.9) else you get blank output.
For example if I use llvm-nm from LLVM3.3 (which is also installed on
my system) on a bitcode archive I see no output
Check that
$ llvm-nm ~/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
gives output. If not you're **not** using the version of llvm-nm that
comes with the version of LLVM you built for KLEE.
If you do get output then you need to investigate what went wrong with
your build of the POSIX runtime library.
On my system I can do (after the runtime library is built)
$ llvm-nm ~/klee/runtime/POSIX/Debug+Asserts/klee_init_env.bc
t __get_sym_str
T klee_init_env
U klee_init_fds
U klee_make_symbolic
U klee_mark_global
U klee_prefer_cex
U klee_range
U klee_report_error
U llvm.dbg.declare
U llvm.dbg.value
U llvm.memcpy.p0i8.p0i8.i64
U malloc
If klee_init_env.bc doesn't exist then run the build again
$ cd ~klee/runtime/POSIX
$ make VERBOSE=1

Post by Oswaldo Olivo
I tried recompiling UCLIBC, like the getting started tutorial says, and I
don't really get any errors after make.
cc1: warning: unrecognized gcc debugging option: N

I see that error too, but I uclibc won't build for me right now so I
can't help there.
Hope that helps.
Thanks,
Dan Liew.