[klee-dev] libc function "open" is defined in POSIX runtime

Gleb Popov 6yearold at gmail.com
Wed Oct 30 10:28:49 GMT 2019


On Wed, Oct 30, 2019 at 2:20 PM Nowack, Martin <m.nowack at imperial.ac.uk>
wrote:

> Hi Gleb,
>
> There are two major building blocks:
>
> First, the built libc does *not* contain library calls that are
> intercepted by the POSIX layer.
> It’s on my list to eventually change this. Most of the patches in
> klee-uclibc just comment out those functions or redirect internally used
> function calls to wrapper of those functions to the actual function.
>
> Second, libraries are archives with different object files. Every object
> file is loaded as a separate module and there might be dependencies between
> objects (e.g. calls).
> The point of the looping is that starting from your application which you
> would like to test, you load and pull in all required object files
> transitively by linking with their module.
> The final result is much smaller than linking the whole library as a big
> module blob. This makes the start-up phase of KLEE much smaller and has an
> impact on the execution as well.
>

This became a bit clearer, thanks.

Can you comment regarding duplicate definition of "open" in
libkleeRuntimePOSIX.bca?


> Best,
> Martin
>
> On 30. Oct 2019, at 07:40, Gleb Popov <6yearold at gmail.com> wrote:
>
>
>
> On Wed, Oct 30, 2019 at 10:37 AM Gleb Popov <6yearold at gmail.com> wrote:
>
>>
>>
>> On Tue, Oct 29, 2019 at 10:05 PM Cadar, Cristian <c.cadar at imperial.ac.uk>
>> wrote:
>>
>>> Hi Gleb,
>>>
>>> We applied various changes to uclibc to make it work with KLEE, so I
>>> think taking a look at those patches would help.  I don't recall the
>>> details, but based on a quick search, I think this patch might be
>>> relevant:
>>>
>>> https://github.com/klee/klee-uclibc/commit/7231f48dd8e2f9f15f721a77639d7eeea6efd38f
>>>
>>> This PR from Martin might also be useful:
>>> https://github.com/klee/klee/pull/483
>>> Look in particular at linkWithMusllibc()
>>>
>>> I would welcome changes to KLEE to make it easier to plug in other libc
>>> implementations.
>>>
>>> Best,
>>> Cristian
>>>
>>
>> Thanks for pointers. However, some debugging brought me to a strange loop
>> in klee::linkModules() function of Module/ModuleUtils.cpp:
>>
>> while (true) {
>>   ...
>>   bool merged = false;
>>   for (auto &module : modules) {
>>      ...
>>      linkTwoModules(composite.get(), std::move(module), errorMsg));
>>   }
>>   ...
>> }
>>
>> If I understand it right, it exits the loop only when there are no
>> undefined symbols left, but I don't see how linking the same set of modules
>> over and over again can help if we actually have some missing symbol.
>>
>> What am I missing there?
>>
>
> Ok, this boiled down to runtime/POSIX/fd_32.c and runtime/POSIX/fd_64.c
> both having "open" definition. This is what causes linking error. I wonder
> why this works on Linux. Any pointers?
>
>
>>
>>> On 26/10/2019 18:50, Gleb Popov wrote:
>>> > Hello.
>>> >
>>> > I'm trying to make KLEE support FreeBSD libc instead of uclibc. When I
>>> > run KLEE with my libc.bca, I get the following error:
>>> >
>>> > error: Linking globals named 'open': symbol multiply defined!
>>> >
>>> > It turned out that POSIX runtime contains definition of "open"
>>> function,
>>> > as well as FreeBSD libc do. How to handle this properly?
>>> >
>>> > _______________________________________________
>>> > klee-dev mailing list
>>> > klee-dev at imperial.ac.uk
>>> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>> >
>>> _______________________________________________
>>> klee-dev mailing list
>>> klee-dev at imperial.ac.uk
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list