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

[Qiuping Yi]

Hi, Dan

Furthermore, I try to compile bash-4.0 on another machine, then I got a
different error message.

KLEE: ERROR: unable to load symbol(rl_blink_matching_paren) while
initializing globals.

But I think *'rl_blink_matching_paren'* is a variable defined by 'bash'
itself, not from any external libraries.
So perhaps these errors are not resulted by some unlinked libraries. If so,
what's wrong?





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


On Sat, Mar 29, 2014 at 1:34 PM, Qiuping Yi <yiqiuping at gmail.com> wrote:

> 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