'Cannot find linker input' reproducing coreutils experiment

[Pablo González de Aledo]

Hi, I'm trying to reproduce the coreutils experiment following
http://ccadar.github.io/klee/TestingCoreutils.html , but when I run

klee --libc=uclibc --posix-runtime ./cat.bc --version

I get the following error:

klee: error: Cannot find linker input
'/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca'

/llvm-2.9/ is my llvm installation path; I've searched inside and there's
not any libkleeRuntimePOSIX.bca there...

Is anything wrong with my setup?.

Thanks.

[Daniel Liew]

Does the folder klee/Release+Asserts/lib/ exist?

You should check the runtime is being built and that there are no errors.
I'm assuming you built KLEE inside the KLEE source directory and not
out of source.

$ cd /llvm-2.9/klee/runtime
$ make clean
$ make


On a side not there is not good reason to build KLEE inside your
llvm-2.9 folder.

Thanks,
Dan.

On 11 November 2013 16:47, Pablo González de Aledo

Post by Pablo González de Aledo
Hi, I'm trying to reproduce the coreutils experiment following
http://ccadar.github.io/klee/TestingCoreutils.html , but when I run
klee --libc=uclibc --posix-runtime ./cat.bc --version
klee: error: Cannot find linker input
'/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca'
/llvm-2.9/ is my llvm installation path; I've searched inside and there's
not any libkleeRuntimePOSIX.bca there...
Is anything wrong with my setup?.
Thanks.

[Pablo González de Aledo]

Yes, the folder klee/Release+Asserts/lib exists under /llvm-2.9/

its content is the following:

***@mint ~/coreutils-6.11/obj-llvm/src $ ls
/llvm-2.9/klee/Release+Asserts/lib/
libkleaverExpr.a libkleeBasic.a libklee-libc.a libkleeRuntest.a
libkleeRuntimeIntrinsic.a libkleeRuntimePOSIX.a
libkleaverSolver.a libkleeCore.a libkleeModule.a libkleeRuntest.so
libkleeRuntimeIntrinsic.bca libkleeSupport.a

I've checked the runtime builds without errors.

I've installed llvm in /llvm-2.9, klee in /llvm-2.9/klee and klee-uclibc in
/llvm-2.9/klee-uclibc-0.02-x64/. May be it's not the best setup?.

The most similar file to the file asked in my installation is
/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.a. Can I "ln -s"
this file to the file asked without worries?.

Thanks.

Post by Daniel Liew
Does the folder klee/Release+Asserts/lib/ exist?
You should check the runtime is being built and that there are no errors.
I'm assuming you built KLEE inside the KLEE source directory and not
out of source.
$ cd /llvm-2.9/klee/runtime
$ make clean
$ make
On a side not there is not good reason to build KLEE inside your
llvm-2.9 folder.
Thanks,
Dan.
On 11 November 2013 16:47, Pablo González de Aledo

Post by Pablo González de Aledo
Hi, I'm trying to reproduce the coreutils experiment following
http://ccadar.github.io/klee/TestingCoreutils.html , but when I run
klee --libc=uclibc --posix-runtime ./cat.bc --version
klee: error: Cannot find linker input
'/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca'
/llvm-2.9/ is my llvm installation path; I've searched inside and there's
not any libkleeRuntimePOSIX.bca there...
Is anything wrong with my setup?.
Thanks.

[Daniel Liew]

Post by Pablo González de Aledo
The most similar file to the file asked in my installation is
/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.a. Can I "ln -s" this
file to the file asked without worries?.

No you **cannot** symlink libkleeRunTimePOSIX.bca to
libkleeRunTimePOSIX.a they are in two completely different formats.
The *.bca files are LLVM bitcode archives and *.a files are archives
of native binary objects.

Can you run?

$ cd /llvm-2.9/klee
$ find . -iname '*.bca'

if your runtime is building correctly it maybe that the files are
ending up in a different folder (e.g. "Release" instead of
"Release+Asserts" which might of happened if you used the
--with-runtime= argument at configure time).

Can you also confirm that you are running the latest upstream KLEE
from GitHub ( https://github.com/ccadar/klee )?

Thanks,
Dan.

[Pablo González de Aledo]

Installing the last version from https://github.com/ccadar/klee it works
better, but I still get the following warnings

***@mint ~/coreutils-6.11/obj-llvm/src $ klee --libc=uclibc
--posix-runtime ./cat.bc --version
KLEE: NOTE: Using model:
/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-4"
KLEE: WARNING ONCE: function "vasnprintf" has inline asm
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING: undefined reference to function: signbitl
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 56353760)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: __xstat64(1, 56242880, 56514336)
KLEE: WARNING ONCE: calling external: getpagesize()
KLEE: WARNING ONCE: calling external: vprintf(56141712, 56544832)
cat (GNU coreutils) 6.11

License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

Written by Torbjorn Granlund and Richard M. Stallman.
KLEE: WARNING ONCE: calling close_stdout with extra arguments.
Copyright (C) 2008 Free Software Foundation, Inc.
KLEE: done: total instructions = 29255
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

Are they really warnings, or are they a real problem?. I suppose klee can
not propagate the symbolic values through functions that are undefined.

Thanks.

Post by Daniel Liew

Post by Pablo González de Aledo
The most similar file to the file asked in my installation is
/llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.a. Can I "ln -s"

this

Post by Pablo González de Aledo
file to the file asked without worries?.

No you **cannot** symlink libkleeRunTimePOSIX.bca to
libkleeRunTimePOSIX.a they are in two completely different formats.
The *.bca files are LLVM bitcode archives and *.a files are archives
of native binary objects.
Can you run?
$ cd /llvm-2.9/klee
$ find . -iname '*.bca'
if your runtime is building correctly it maybe that the files are
ending up in a different folder (e.g. "Release" instead of
"Release+Asserts" which might of happened if you used the
--with-runtime= argument at configure time).
Can you also confirm that you are running the latest upstream KLEE
from GitHub ( https://github.com/ccadar/klee )?
Thanks,
Dan.