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

[Nowack, Martin]

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.

Best,
Martin

On 30. Oct 2019, at 07:40, Gleb Popov <6yearold at gmail.com<mailto:6yearold at gmail.com>> wrote:



On Wed, Oct 30, 2019 at 10:37 AM Gleb Popov <6yearold at gmail.com<mailto:6yearold at gmail.com>> wrote:


On Tue, Oct 29, 2019 at 10:05 PM Cadar, Cristian <c.cadar at imperial.ac.uk<mailto: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<mailto: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<mailto: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<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed