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ć <ma...@cs.utah.edu> . 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