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

Gleb Popov 6yearold at gmail.com
Fri Nov 1 06:39:29 GMT 2019


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

> Hi Gleb,
>
> According to double entries, this is a result of the large-file-system
> (LFS) support for 32bit linux systems.
> (e.g. https://users.suse.com/~aj/linux_lfs.html)
>
> All the macro magic leads to generating two different functions for open()
> in the resulting bitcode files:
> ```
> define i32 @open(i8* nonnull, i32, ...) #0 !dbg !43 { … }
> define i32 @open64(i32, i8* nonnull, i32, ...) #0 !dbg !112 { … }
> ```
> Therefore, there is no collision under linux.
>

I see, this is a valueable input, thanks!


> Best,
> Martin
>
> On 30. Oct 2019, at 10:28, Gleb Popov <6yearold at gmail.com> wrote:
>
>
>
> 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