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
