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

[Qiuping Yi]

hi, Dan Liew,

Now I change Makefile to assign llvm-ld as the linker, so I can get the
*find.bc* without error. But I still get the error "*failed external call:
fstatat*". I checked that function 'fstatat' is defined in <sys/stat.h>. So
how should I link the function?

In your previous email, you said I can explicitly link libraries, can I
link some library for solving this problem? Do you thin this error is
similar with the before one*(**KLEE: ERROR: unable to load symbol(PC) while
initializing globals.)*

I am so sorry that I  bother you so much with several emails.

Best regards to you!



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


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

> Hi, Dan
>
> I found similar errors when I test findutil. I compile findutil as follow:
>
> $ ./configure --disable-nls CFLAGS="-g"
> $ make CC=wllvm
>
> Then I encounter an error:
> /home/guest/installed/wllvm/whole-program-llvm/wllvm  -g   -o test-dirname
> test-dirname.o ../gnulib/lib/libgnulib.a
> test-dirname.o: file not recognized: File format not recognized
>
> SO, next I execute:
> $ cd tests/
> $ llvm-ld -o test-dirname test-dirname.o ../gnulib/lib/libgnulib.a
>
> Then, continue "make CC=wllvm", next I encountered the next error:
>
> /home/guest/installed/wllvm/whole-program-llvm/wllvm  -g   -o regexprops
> regexprops.o regextype.o ../gnulib/lib/libgnulib.a
> regexprops.o: file not recognized: File format not recognized
>
> SO, next I execute:
> $ cd lib
> $ llvm-ld -o regexprops regexprops.o regextype.o ../gnulib/lib/libgnulib.a
>
> Then, continue "make CC=wllvm", next I encountered the next error:
>
> /home/guest/installed/wllvm/whole-program-llvm/wllvm  -g   -o find
> ftsfind.o ./libfindtools.a ../lib/libfind.a ../gnulib/lib/libgnulib.a  -lrt
> ftsfind.o: file not recognized: File format not recognized
>
> SO, next I execute:
> $ cd find
> $ llvm-ld -o find ftsfind.o ./libfindtools.a ../lib/libfind.a
> ../gnulib/lib/libgnulib.a ( *at this step, I ignore '-lrt' *).
>
> At last, I got find.bc under dir 'find/', *however* when I tested find.bc
> file with KLEE, I encountered *"failed external call"* error.
>
> Does the previous compile process wrong?
>
>
>
>
> --------------------------------------------
> Qiuping Yi
> Institute Of Software
> Chinese Academy of Sciences
>
>
> On Sat, Mar 29, 2014 at 2:06 PM, Qiuping Yi <yiqiuping at gmail.com> wrote:
>
>> 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