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 <[email protected]<mailto:[email protected]>> wrote: On Wed, Oct 30, 2019 at 10:37 AM Gleb Popov <[email protected]<mailto:[email protected]>> wrote: On Tue, Oct 29, 2019 at 10:05 PM Cadar, Cristian <[email protected]<mailto:[email protected]>> 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 > [email protected]<mailto:[email protected]> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
