Re: [klee-dev] Adding support for another C library
On 17 October 2016 at 22:52, Marko Dimjašević wrote: > Hi Dan, > > On Mon, 2016-10-17 at 09:44 +0100, Dan Liew wrote: >> That is likely the cause error. This comes from a rather hacky >> implementation of a linker inside KLEE. >> >> I've mentioned this before that but this is something I'd like to >> remove from KLEE. I think that **all** linking (and optimization) >> should be done outside of KLEE using other tools because this would >> simplify KLEE's implementation and would be far cleaner. > > I don't agree with your root-cause reasoning in this case. I tried to > perform the same linking outside KLEE, i.e. with the llvm-link tool, yet > I got the same outcome. The "I'd like to remove..." is a side comment. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding support for another C library
Hi Dan, On Mon, 2016-10-17 at 09:44 +0100, Dan Liew wrote: > That is likely the cause error. This comes from a rather hacky > implementation of a linker inside KLEE. > > I've mentioned this before that but this is something I'd like to > remove from KLEE. I think that **all** linking (and optimization) > should be done outside of KLEE using other tools because this would > simplify KLEE's implementation and would be far cleaner. I don't agree with your root-cause reasoning in this case. I tried to perform the same linking outside KLEE, i.e. with the llvm-link tool, yet I got the same outcome. I've played more with this in the meantime, and I realized there are symbols that both Musl and KLEE POSIX runtime define (in particular, 'T' symbol entries in their symbol tables), hence the clash. What I did is to turn conflicting functions/their names in Musl to weak symbols (the GNU C extension thing), which got me a bit further, but then I ran into issues I mention below in reply to another of your comments... > However we have to live with the horrible hacks that exist right now. > To help you debug linking if you build KLEE as a debug build you can > pass `-debug-only=klee_linker` to KLEE and that should dump a bunch > more output. You can find the relevant code in > `lib/Module/ModuleUtil.cpp`. Thanks for the debugging hint! I did realize linking happens in the mentioned source file. > > If it helps, I used Musl's libc.so.bc, i.e. a dynamically linked version > > of the library in KLEE (that's what the -libc=musl parameter fetches). > > I don't think "dynamically linked" makes any sense here. You just have > LLVM bitcode. > There is no "static" or "dynamic" here. OK. What I was trying to say here is that at least with Musl, but I believe it would be the case with other (standard C) libraries, their static and dynamic counterparts don't define the same symbols and not in the same way, hence it matters if I derive a libc.so.bc or libc.a.bc. Therefore, it makes difference against what LLVM IR library one links. In my particular case, I've been struggling with getting all important C library symbols included, such as __cp_begin, fini_array_start and fini_array_end, etc. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Description: This is a digitally signed message part ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding support for another C library
Hi Marko On 16 October 2016 at 04:34, Marko Dimjašević wrote: > Hi again, > > On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote: > >> Earlier on this list there was a thread on what would be alternatives >> to >> KLEE-uClibc as the library implementation got rather old, which is >> true >> for its upstream as well, though to a lesser extent. Here I would like >> to ask how to add support for another C library implementation to >> KLEE. > > I started implementing support for the Musl C library in KLEE: > > https://github.com/mdimjasevic/klee/commit/367543b6 > > I'd like to use Musl in conjunction with the POSIX runtime. However, > when I run KLEE like this: > > $ klee -libc=musl -posix-runtime hostname.bc > > I get the following: > > KLEE: NOTE: Using musl : /home/marko/research/klee/Release > +Asserts/lib/musl.bca > KLEE: NOTE: Using model: /home/marko/research/klee/Release > +Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: ERROR: Link with library /home/marko/research/klee/Release > +Asserts/lib/libkleeRuntimePOSIX.bca failed: Linking globals named > 'access': symbol multiply defined! That is likely the cause error. This comes from a rather hacky implementation of a linker inside KLEE. I've mentioned this before that but this is something I'd like to remove from KLEE. I think that **all** linking (and optimization) should be done outside of KLEE using other tools because this would simplify KLEE's implementation and would be far cleaner. However we have to live with the horrible hacks that exist right now. To help you debug linking if you build KLEE as a debug build you can pass `-debug-only=klee_linker` to KLEE and that should dump a bunch more output. You can find the relevant code in `lib/Module/ModuleUtil.cpp`. > > How to avoid multiple symbol definitions? > > > If it helps, I used Musl's libc.so.bc, i.e. a dynamically linked version > of the library in KLEE (that's what the -libc=musl parameter fetches). I don't think "dynamically linked" makes any sense here. You just have LLVM bitcode. There is no "static" or "dynamic" here. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding support for another C library
If you haven't already seen it, Ryan Hileman's recent blog post on libc is probably relevant. http://ryanhileman.info/posts/lib43 ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Adding support for another C library
Hi again, On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote: > Earlier on this list there was a thread on what would be alternatives > to > KLEE-uClibc as the library implementation got rather old, which is > true > for its upstream as well, though to a lesser extent. Here I would like > to ask how to add support for another C library implementation to > KLEE. I started implementing support for the Musl C library in KLEE: https://github.com/mdimjasevic/klee/commit/367543b6 I'd like to use Musl in conjunction with the POSIX runtime. However, when I run KLEE like this: $ klee -libc=musl -posix-runtime hostname.bc I get the following: KLEE: NOTE: Using musl : /home/marko/research/klee/Release +Asserts/lib/musl.bca KLEE: NOTE: Using model: /home/marko/research/klee/Release +Asserts/lib/libkleeRuntimePOSIX.bca KLEE: ERROR: Link with library /home/marko/research/klee/Release +Asserts/lib/libkleeRuntimePOSIX.bca failed: Linking globals named 'access': symbol multiply defined! I haven't been able to track this down. Is this to say that libkleeRuntimePOSIX.bca has a model for the 'access' function and that this clashes with the definition of the 'access' function in Musl? How to avoid multiple symbol definitions? If it helps, I used Musl's libc.so.bc, i.e. a dynamically linked version of the library in KLEE (that's what the -libc=musl parameter fetches). -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Description: This is a digitally signed message part ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev