[klee-dev] Adding support for another C library

[Dan Liew]

Hi Marko

On 16 October 2016 at 04:34, Marko Dimjašević <marko at cs.utah.edu> wrote:
> Hi again,
>
> On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote:
>
>> 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.
>
> I started implementing support for the Musl C library in KLEE:
>
> https://github.com/mdimjasevic/klee/commit/367543b6
>
> I'd like to use Musl in conjunction with the POSIX runtime. However,
> when I run KLEE like this:
>
> $ klee -libc=musl -posix-runtime hostname.bc
>
> I get the following:
>
> KLEE: NOTE: Using musl : /home/marko/research/klee/Release
> +Asserts/lib/musl.bca
> KLEE: NOTE: Using model: /home/marko/research/klee/Release
> +Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: ERROR: Link with library /home/marko/research/klee/Release
> +Asserts/lib/libkleeRuntimePOSIX.bca failed: Linking globals named
> 'access': symbol multiply defined!

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.

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`.

>
> How to avoid multiple symbol definitions?
>
>
> 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.