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

[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


On Mon, Mar 24, 2014 at 7:49 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> > /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.
>
> > 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
>
> It's not strange at all, the compiler is creating temporary files
> during the compilation process.
>
> > 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.
>
> > 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.
>
-------------- next part --------------
HTML attachment scrubbed and removed