[klee-dev] Adding support for another C library

[Marko Dimjašević]

Hi all,

Earlier on this list there was a thread on what would be alternatives to
KLEE-uClibc as the library implementation got rather old, which is true
for its upstream as well, though to a lesser extent. Here I would like
to ask how to add support for another C library implementation to KLEE.

In particular, I am hoping Musl would be a good new C library to use:

http://www.musl-libc.org/

There is an unofficial port of Musl to an "x86_64 llvm bitcode"
architecture:

https://github.com/SRI-CSL/musllvm

which sounds just right (assuming we all use x86_64). The author of the
port took care to remove as much of assembly as possible in the LLVM IR,
which is great for KLEE.

At first I was hoping all it would take to support Musl in KLEE is to
provide Musl's libc.a(.bc) when compiling KLEE and that would be it.
However, things are not so simple.

Therefore, my  question is: what changes need to be done to KLEE so e.g.
Musl is supported? Here is what I learned by browsing KLEE's source code
and I would appreciate your feedback, e.g. if I am missing anything.

In tools/klee/main.cpp there are several places where "Libc" is
mentioned. What I guess is the key thing is to support a libc's main
function. For example, in function linkWithUclibc there is this
statement:

mainModule->getOrInsertFunction("__uClibc_main", ...)

From my understanding of how a natively compiled C program is executed
(in GNU/Linux) is that a libc's main function (e.g., "__uClibc_main" in
the KLEE-uClibc case) is the first function that gets invoked, and not
the program's main function. Therefore, I suppose KLEE plays the role of
the loader and linker in the symbolic execution land, and that it has to
prepare the environment for the program, including command line
arguments to the program under test, which is handed over to the libc's
main function.

What about the POSIX runtime? As far as I got it they're usually part of
a standard C library implementation. What has to be done in that regard?

Why do some functions from KLEE-uClibc get renamed, e.g. "__libc_open"
gets renamed to "open"?


Anything else?


I'd appreciate any thoughts on this matter.


-- 
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/20161014/9e7ee343/attachment.sig>