Thank you again Cristian. Your suggestion didn't help me directly:
bash> cat in.c
extern const char*mpfr_get_version(void);
int main(int argc,char**argv){
return (int)mpfr_get_version();
}
bash> nm ./libmpfr.a | grep version
version.o:
0000000000000000 T mpfr_get_version
bash> llvm-gcc -emit-llvm -w -c in.c
bash> llvm-ld in.o ./libmpfr.a
bash> llvm-nm a.out.bc
T main
U mpfr_get_version
However, because of it I found out that the warning is inconsequential:
bash> klee --libc=uclibc --posix-runtime --load=/<snipped-path>/libmpfr.so
./a.out.bc
KLEE: NOTE: Using model: /<snipped-path>/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-1"
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: mpfr_get_version
KLEE: WARNING: calling external: syscall(16, 0, 21505, 41284016)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: __xstat64(1, 41156720, 41374176)
KLEE: WARNING: calling external: mpfr_get_version()
KLEE: done: total instructions = 15127
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
So I'll focus now on the assertion violation.
Thanks,
Brady J. Garvin
> Hi,
>
>
>> I'm trying to use klee on a subject that makes calls to the GMP and MPFR
>> libraries. These libraries use a lot of inline assembly, but I can
>> guarantee that their functions' arguments will always be concrete.
>> Therefore, I hoped to build GMP and MPFR as shared objects for x86_64
>> and
>> make them available to KLEE via the -load option.
>
> I think the --load option is used by LLVM to load plugins. I never tried
> it but it should work, perhaps others have experience with this option.
> Another option, which I remember worked in the past, is to use llvm-ld to
> link in the shared library too. You may use llvm-nm in this case to check
> if the symbols are defined.
>
>> However, KLEE nonetheless complains about undefined references to
>> __gmp_version, __gmpz_add, etc. It subsequently aborts with an
>> assertion
>> violation:
>>
>> Context.cpp:41: static unsigned int
>> klee::Expr::getWidthForLLVMType(const
>> llvm::Type*): Assertion `0 && "non-primitive type argument to
>> Expr::getWidthForLLVMType()\n"' failed,
>
> I think these are unrelated indeed. You can investigate further and see
> which is the type that fires this assertion and what is the width of the
> type. I suspect this is something specific to 64bit.
>
> Cristi
>
>>
>> which may be unrelated. As a sanity check, nm reports all of these
>> symbols appropriately defined and in their proper sections.
>>
>> Either I have misunderstood the -load option, or I have missed a step in
>> getting KLEE to find the symbols in the shared objects. My googling
>> thus
>> far hasn't turned up much, except that KLEE may use libffi. Any
>> corrections to my understanding or pointers to documentation would be
>> much
>> appreciated.
>>
>> Thanks,
>> Brady J. Garvin
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at keeda.stanford.edu
>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
