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

[Qiuping Yi]

Hi, Dan

Did you mean you can successfully run bash.bc with klee?
I found bash indeed use PC(and BC, UP), but I think I cannot simply remove
them.

Now I want to try the second advice, but how should I confirm which dynamic
libraries are missing,
and then how to link them?  Could you give me more detail steps. Thank you
very much.


--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences


On Thu, Mar 27, 2014 at 6:49 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> > 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.
>
-------------- next part --------------
HTML attachment scrubbed and removed