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