[klee-dev] External function "mmap" can not be resolved correctly
Hi There I am using the latest klee-uclibc from homepage, it looks like that KLEE is not able to resolve "mmap" system call correctly, KLEE always aborts at the following code: void* m = mmap(0, masterLength, PROT_READ, _MAP_BASE, masterFD, 0); uint64_t* fptr = (uint64_t*)m; __attribute__((unused)) uint64_t version = le64toh(*fptr++); The "fptr" pointer can not be resolved in the executeMemoryOperation function, any idea about it? Thanks Peng ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Strange error when compiling 'bash-4.0' using klee-gcc
> 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 (0x7fffb810b000) libreadline.so.6 => /usr/lib/libreadline.so.6 (0x7f5f98041000) libncursesw.so.5 => /usr/lib/libncursesw.so.5 (0x7f5f97ddc000) libdl.so.2 => /usr/lib/libdl.so.2 (0x7f5f97bd8000) libc.so.6 => /usr/lib/libc.so.6 (0x7f5f9783) /lib64/ld-linux-x86-64.so.2 (0x7f5f9828b000) 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 klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
