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

Gleb Popov 6yearold at gmail.com
Wed Oct 30 07:40:24 GMT 2019


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
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list