Strange error when compiling 'bash-4.0' using klee-gcc

[Qiuping Yi]

Hi, everyone

I want to compile 'bash-4.0' with klee-gcc following the next commands
(like compiling coreutils http://klee.github.io/klee/TestingCoreutils.html
):

$ ../configure --disable-nls CFLAGS="-g"
$ make CC=/home/guest/installed/klee/scripts/klee-gcc

However, I encountered an error when 'make', which the following error
message:

/home/guest/installed/klee/scripts/klee-gcc -DPROGRAM='"bash"'
-DCONF_HOSTTYPE='"x86_64"' -DCONF_OSTYPE='"linux-gnu"'
-DCONF_MACHTYPE='"x86_64-unknown-linux-gnu"' -DCONF_VENDOR='"unknown"'
-DLOCALEDIR='"/usr/local/share/locale"' -DPACKAGE='"bash"' -DSHELL
-DHAVE_CONFIG_H -I. -I. -I./include -I./lib -g -o mksyntax
./mksyntax.c
*/tmp/cc1H53KR.o: file not recognized: File format not recognized*
collect2: ld returned 1 exit status
make: *** [mksyntax] Error 1

Furthermore, it's strange that the not recognized file keeping changed if I
execute 'make' again and again. For example, the second time I encounter
the next error message:

*/tmp/ccaJGvTn.o: file not recognized: File format not recognized*

BUT I found both file */tmp/cc1H53KR.o and **/tmp/ccaJGvTn.o *do not exist.

What's wrong? What should I do?

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

[Daniel Liew]

This post might be inappropriate. Click to display it.

[Qiuping Yi]

Hi, Dan Liew,

Thank you for your advice. Now I can use *wllvm *to generate bash.bc
successfully based on the next steps:

$ export LLVM_COMPILER=llvm-gcc
$ export LLVM_GCC_PREFIX=llvm-
$ cd bash-4.0
$ ./configure --disable-nls CFLAGS="-g"
$ make CC=wllvm
$ extract-bc bash

however, I cannot run klee on the generated 'bash.bc'.

when I carry out:

$ klee *--libc=uclibc --posix-runtime *./bash.sh test.sh

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.





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

Post by Daniel Liew

Post by Qiuping Yi
/home/guest/installed/klee/scripts/klee-gcc -DPROGRAM='"bash"'
-DCONF_HOSTTYPE='"x86_64"' -DCONF_OSTYPE='"linux-gnu"'
-DCONF_MACHTYPE='"x86_64-unknown-linux-gnu"' -DCONF_VENDOR='"unknown"'
-DLOCALEDIR='"/usr/local/share/locale"' -DPACKAGE='"bash"' -DSHELL
-DHAVE_CONFIG_H -I. -I. -I./include -I./lib -g -o mksyntax
./mksyntax.c
/tmp/cc1H53KR.o: file not recognized: File format not recognized
collect2: ld returned 1 exit status
make: *** [mksyntax] Error 1

It looks like the script is trying to invoke your system's native
linker to build a native executable. That won't work because
/tmp/cc1H53KR.o is probably an LLVM bitcode file so the linker does
not know what to do with it.
You probably should be using the '-c' flag so you do not invoke the
linker. This approach is really only feasible with single file
programs.

Post by Qiuping Yi
Furthermore, it's strange that the not recognized file keeping changed

if I

Post by Qiuping Yi
execute 'make' again and again. For example, the second time I encounter

the

Post by Qiuping Yi
/tmp/ccaJGvTn.o: file not recognized: File format not recognized

It's not strange at all, the compiler is creating temporary files
during the compilation process.

Post by Qiuping Yi
BUT I found both file /tmp/cc1H53KR.o and /tmp/ccaJGvTn.o do not exist.

These files are deleted automatically by the compiler because they are
temporary intermediate files.

Post by Qiuping Yi
What's wrong? What should I do?

I've already explained above what is wrong.
I do not know much about bash's build system but I would expect it to
be more complex that coreutil's. klee-gcc is a bit of a hack so you
should probably either
- Use wllvm [1]. This is also a hack but is considerably better than
klee-gcc and can link together multi file programs.
- Use LLVM gold [2] so you can link together a multi-file program to a
bitcode module.
[1] https://github.com/klee/whole-program-llvm
[2] http://llvm.org/docs/GoldPlugin.html
Thanks,
Dan Liew.

[Daniel Liew]

This post might be inappropriate. Click to display it.

[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

Post by Daniel Liew

Post by Qiuping Yi
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.

[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

Post by 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

Post by Daniel Liew

Post by Qiuping Yi
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.