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ć <ma...@cs.utah.edu> . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org
signature.asc
Description: This is a digitally signed message part
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
