[klee-dev] KLEE unable to load a symbol

[Marko Dimjašević]

Dear KLEE users and devs,

I've noticed others had issues with KLEE saying it is unable to load a
symbol:

http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000017.html
https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01252.html

To the former Cristian Cadar replied: "[M]ost likely you have not
compiled all libraries used by vim to LLVM bitcode.", where a user was
trying to use KLEE on vim.

Can someone explain a bit more why this error is happening?

I'm trying to analyze Debian packages with KLEE and I ran into the same
issue. For example, I see the error when I try to run KLEE on 'vim'
compiled from a Debian package.

I tried to run KLEE on the apt-sortpkgs utility as well and I get the
same kind of error:

KLEE: ERROR: unable to load symbol(_config) while initializing globals.

Note I build packages from their source, hence whatever libraries a
package may have, they will be compiled to LLVM IR and hopefully linked
together with WLLVM.

I see the error gets reported when KLEE is in lib/Core/Executor.cpp.
However, with my current familiarity with KLEE's source code, I'm
unable to explain to myself why this happens.

I ran it with KLEE 1.2.0 and KLEE-uClibc 1.0.0 with .bc files compiled
with LLVM 3.4. Here is how I run KLEE:

  klee -max-time=30 -libc=uclibc --posix-runtime apt-sortpkgs.bc


If needed, I will provide .bc files of programs for which the error is
reported.

I'd like to understand why this is happening as I'm expecting it might
be quite common for many other packages too.


-- 
Regards,
Marko Dimjašević <marko at cs.utah.edu> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160526/d245ee3d/attachment.sig>