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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected] >>> > 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. >>>> >>> >>> >> >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
