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
