[klee-dev] Strange error when compiling 'bash-4.0' using klee-gcc

[Daniel Liew]

> I got the next error messag:
>
> KLEE: ERROR: unable to load symbol(PC) while initializing globals.
>
> Could you tell me what should I do then? Thank you very much.

The error message you are seeing comes from lib/Core/Executor.cpp:568

I'm not entirely familiar with how this works but I think what is
happening is the following

- the "PC" symbol appears to be undefined (because i->isDeclaration()
is true) in bash.bc
- Because PC is undefined KLEE tries to see if the symbol is present
in the running copy of KLEE itself. For example if bash.bc has a
undefined symbol __dso_handle then the address it will get is the
__dso_handle of the KLEE executable.
- There is probably no "PC" symbol in KLEE so it fails.

To fix this you need to figure out where the PC symbol is coming from
in the bash source code and see if you can remove it from bash.bc or
support is some how within KLEE.

You should realise that the bash.bc file will have some things missing from it.

- Any external static libraries cannot be linked with it (because they
will be in a binary format and not LLVM bitcode)
- Any external dynamic libraries won't be linked in either.

Looking on my system, bash linux, it dynamically links with

linux-vdso.so.1 (0x00007fffb810b000)
libreadline.so.6 => /usr/lib/libreadline.so.6 (0x00007f5f98041000)
libncursesw.so.5 => /usr/lib/libncursesw.so.5 (0x00007f5f97ddc000)
libdl.so.2 => /usr/lib/libdl.so.2 (0x00007f5f97bd8000)
libc.so.6 => /usr/lib/libc.so.6 (0x00007f5f97830000)
/lib64/ld-linux-x86-64.so.2 (0x00007f5f9828b000)

so it is likely that your missing symbol is provided by one of these
libraries. If you can figure out which library provides that symbol
you might be able to hack KLEE by forcing it to dynamically load the
right shared libraries (i.e. [1] or dlopen() ) before KLEE tries to
initialise the globals of the LLVM bitcode program it is interpreting.

[1] http://llvm.org/docs/doxygen/html/classllvm_1_1sys_1_1DynamicLibrary.html

Hope that helps,

Dan.