[klee-dev] Adding support for another C library

[Marko Dimjašević]

Hi Dan,

On Mon, 2016-10-17 at 09:44 +0100, Dan Liew wrote:
> That is likely the cause error. This comes from a rather hacky
> implementation of a linker inside KLEE.
> 
> I've mentioned this before that but this is something I'd like to
> remove from KLEE. I think that **all** linking (and optimization)
> should be done outside of KLEE using other tools because this would
> simplify KLEE's implementation and would be far cleaner.

I don't agree with your root-cause reasoning in this case. I tried to
perform the same linking outside KLEE, i.e. with the llvm-link tool, yet
I got the same outcome.

I've played more with this in the meantime, and I realized there are
symbols that both Musl and KLEE POSIX runtime define (in particular, 'T'
symbol entries in their symbol tables), hence the clash. What I did is
to turn conflicting functions/their names in Musl to weak symbols (the
GNU C extension thing), which got me a bit further, but then I ran into
issues I mention below in reply to another of your comments...


> However we have to live with the horrible hacks that exist right now.
> To help you debug linking if you build KLEE as a debug build you can
> pass `-debug-only=klee_linker` to KLEE and that should dump a bunch
> more output. You can find the relevant code in
> `lib/Module/ModuleUtil.cpp`.

Thanks for the debugging hint! I did realize linking happens in the
mentioned source file.


> > If it helps, I used Musl's libc.so.bc, i.e. a dynamically linked version
> > of the library in KLEE (that's what the -libc=musl parameter fetches).
> 
> I don't think "dynamically linked" makes any sense here. You just have
> LLVM bitcode.
> There is no "static" or "dynamic" here.

OK. What I was trying to say here is that at least with Musl, but I
believe it would be the case with other (standard C) libraries, their
static and dynamic counterparts don't define the same symbols and not in
the same way, hence it matters if I derive a libc.so.bc or libc.a.bc.
Therefore, it makes difference against what LLVM IR library one links. 

In my particular case, I've been struggling with getting all important C
library symbols included, such as __cp_begin, fini_array_start and
fini_array_end, etc.


-- 
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/20161017/514511b9/attachment.sig>