[klee-dev] Can KLEE be portable?

[Daniel Liew]

Hi,

Support was recently added to KLEE so that it can be executed from any
installation location. This isn't exactly what you want because the
path is still hardcoded into KLEE but you can still use it to allow
KLEE to be portable provided it is installed in the right place.

To do this when configuring KLEE specify the install prefix. e.g.

$ ./configure --prefix=/usr/local/ --with-llvm=...
$ make
$ make install

now KLEE will be installed into "/usr/local/". You should be able to
copy this folder to other machines running the same linux distribution
and then run KLEE provided you install the folder to the same
location.

The install target copies klee-uclibc over and STP is statically
linked with KLEE so that library is does not need to be copies over.

You can check how the runtime library location is being detected by
using the following flag with Debug build

$ klee -debug-only=klee_runtime

Hope that helps.

Thanks,
Dan Liew.

On 3 January 2014 11:52, 李永超 <lyc364 at gmail.com> wrote:
> Hi,
> I am trying to move KLEE executables built on one machine to the other that
> has different environment configurations
> , for instance, distinct user name thus causing path-to-KLEE changed on that
> new machine.
> I also copy binaries of llvm, uclibc and stp(of course all of them are built
> on current machine) to the new machine.
> When run KLEE with a .bc file, it says:
>
> feiniao at feiniao-Lenovo-Product:~/Desktop/util$ ./klee BYOD.bc
> /* Normal output omitted */
> klee: error: Cannot find linker input
> '/home/qingjinlyc/IDEs/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'
> klee: ModuleUtil.cpp:51: llvm::Module* klee::linkWithLibrary(llvm::Module*,
> const string&): Assertion `0 && "linking in library failed!"' failed.
>
> I am not surprised to see this cause it is within my expectation that KLEE
> will use absolute paths to find libraries at runtime.
> However, now I just need a portable KLEE that could run on any machine
> without having to build all things around.
> How can I achieve this or anyone tell me this is totally impossible?
>
> Thanks
>
> ------------------
> Yongchao Li
> Department of Computer Science and Technology
> Nanjing University