Re: [klee-dev] Adding support for another C library

[Dan Liew]

On 17 October 2016 at 22:52, Marko Dimjašević  wrote:
> 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.

The "I'd like to remove..." is a side comment.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [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ć  .   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

Re: [klee-dev] Adding support for another C library

[Dan Liew]

Hi Marko

On 16 October 2016 at 04:34, Marko Dimjašević  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.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Adding support for another C library

[David Manouchehri]

If you haven't already seen it, Ryan Hileman's recent blog post on libc is
probably relevant.

http://ryanhileman.info/posts/lib43
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Adding support for another C library

[Marko Dimjašević]

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!


I haven't been able to track this down. Is this to say that
libkleeRuntimePOSIX.bca has a model for the 'access' function and that
this clashes with the definition of the 'access' function in Musl?

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

-- 
Regards,
Marko Dimjašević  .   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