[klee-dev] Difficulty installing KLEE
Cristian Cadar
c.cadar at imperial.ac.uk
Fri Nov 8 10:59:41 GMT 2013
Thanks for your suggestions, Vijay. Releasing KLEE as a package would
be nice, but the main issue is the dependency on an old version of LLVM
(2.9 currently). We could easily create a VM, but the issues here are
(1) space, as David pointed out and (2) someone would also need to set
up a way to update it regularly. BTW, we do have a CDE package
available for download (did you try it?), but it is currently quite
outdated.
Dominic Chen has created some scripts that generate binary versions of
KLEE. However, there are still issues linking various libraries. If
anyone would like to take a look, the scripts are part of klee-buildbot
(https://github.com/ccadar/klee-buildbot).
On a different note, don't worry about DirConsistency.c and DirSeek.c,
these are fragile tests that indeed can fail. I will change them to
XFAIL (Expected to fail) shortly.
Best,
Cristian
On 07/11/2013 13:12, Vijay Ganesh wrote:
> Hi All,
>
> Having used and enjoyed earlier versions of KLEE, I recently decided to
> install this latest version of KLEE after a long time.
>
> I ran into many unexpected problems, all due to dependencies. (The KLEE
> and STP codes themselves seem to compile without any issues whatsoever.)
>
> I believe that I am not alone in my experience. I think if the KLEE team
> is able to address these installation issues, then a much broader set of
> users may be willing to experiment with KLEE. You never know which
> previously unanticipated applications users may use KLEE for, if only
> they could get beyond the installation pain.
>
> Here are some suggestions to alleviate installation issues:
>
> Packaged Virtual Machine with KLEE
> --------------------------------------------------
>
> * Is it possible to release a Linux VirtualBox or VMWare virtual
> machines with KLEE built in? This can be particularly useful for class
> projects, and get troves of new users hooked on KLEE. It can also be
> great for reproducibility of published results.
>
> sudo apt-get install klee. Anyone?
> --------------------------------------------
>
> * I know that STP is released natively with some version of OpenBSD and
> Fedora. Something similar can be done for KLEE by creating a Personal
> Package Archive (PPA) on Ubuntu. Here are some pointers:
>
> http://askubuntu.com/questions/336130/create-apt-get-install-for-own-software
>
> Cheers,
> Vijay Ganesh
> https://ece.uwaterloo.ca/~vganesh
>
>
>
> On Thu, Nov 7, 2013 at 7:44 AM, Vijay Ganesh <hellovijay at gmail.com
> <mailto:hellovijay at gmail.com>> wrote:
>
> Hi Urmas,
>
> Thanks for the link. I managed to build KLEE with uclibc. I had to
> comment out the offending lines in netlinkaccess.h. (That seems to
> be what the patch you pointed out is saying.)
>
> Having said that, I get the following unexpected failures during
> 'make check':
>
> Running /home/vganesh/work/KLEE/klee/test/Runtime/POSIX/dg.exp ...
> FAIL: /home/vganesh/work/KLEE/klee/test/Runtime/POSIX/DirConsistency.c
> Failed with exit(1) at line 2
> while running: klee --run-in=/tmp --search=random-state
> --libc=uclibc --posix-runtime --exit-on-error
> DirConsistency.c.tmp.bc --sym-files 1 1 > DirConsistency.c.tmp1.log
> KLEE: NOTE: Using model:
> /home/vganesh/work/KLEE/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-19"
> KLEE: WARNING: undefined reference to function: __xstat64
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 65250160)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> KLEE: WARNING ONCE: calling external: __xstat64(1, 65159696, 65284352)
> KLEE: WARNING ONCE: calling external: printf(65106096, 2)
> KLEE: ERROR: /home/vganesh/work/KLEE/klee/runtime/POSIX/fd.c:873:
> ASSERTION FAIL: s != (off64_t) -1
> KLEE: NOTE: now ignoring this error at this location
> EXITING ON ERROR:
> Error: ASSERTION FAIL: s != (off64_t) -1
> File: /home/vganesh/work/KLEE/klee/runtime/POSIX/fd.c
> Line: 873
> Stack:
> #0 00012920 in __fd_getdents (fd=3, dirp=65500352, count=4096)
> at /home/vganesh/work/KLEE/klee/runtime/POSIX/fd.c:873
> #1 00015288 in getdents (fd=3, dirp=65500352, nbytes=4096) at
> /home/vganesh/work/KLEE/klee/runtime/POSIX/fd_32.c:171
> #2 00001727 in readdir (dir=65435376) at
> /home/vganesh/KLEE/klee-uclibc-0.02-x64/libc/misc/dirent/readdir.c:33
> #3 00000317 in __user_main (argc=4, argv=60051728)
> #4 00001152 in __uClibc_main (main=50973840, argc=4,
> argv=60051728, app_init=0, app_fini=0, rtld_fini=0, stack_end=0) at
> /home/vganesh/work/KLEE/klee-uclibc-0.02-x64/libc/misc/internals/__uClibc_main.c:402
> #5 00009698 in main (=4, =60051728)
>
>
> FAIL: /home/vganesh/work/KLEE/klee/test/Runtime/POSIX/DirSeek.c
> Failed with exit(1) at line 2
> while running: klee --run-in=/tmp --libc=uclibc --posix-runtime
> --exit-on-error DirSeek.c.tmp2.bc --sym-files 2 2
> pos: 280
> KLEE: NOTE: Using model:
> /home/vganesh/work/KLEE/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-20"
> KLEE: WARNING: undefined reference to function: __xstat64
> KLEE: WARNING: undefined reference to function: fwrite
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 40632656)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> KLEE: WARNING ONCE: calling external: __xstat64(1, 40547328, 40667344)
> KLEE: WARNING ONCE: calling external: printf(40503952, 280)
> KLEE: ERROR: /home/vganesh/work/KLEE/klee/runtime/POSIX/fd.c:873:
> ASSERTION FAIL: s != (off64_t) -1
> KLEE: NOTE: now ignoring this error at this location
> EXITING ON ERROR:
> Error: ASSERTION FAIL: s != (off64_t) -1
> File: /home/vganesh/work/KLEE/klee/runtime/POSIX/fd.c
> Line: 873
> Stack:
> #0 00007647 in __fd_getdents (fd=3, dirp=40881344, count=4096)
> at /home/vganesh/work/KLEE/klee/runtime/POSIX/fd.c:873
> #1 00010017 in getdents (fd=3, dirp=40881344, nbytes=4096) at
> /home/vganesh/work/KLEE/klee/runtime/POSIX/fd_32.c:171
> #2 00001764 in readdir (dir=40794160) at
> /home/vganesh/KLEE/klee-uclibc-0.02-x64/libc/misc/dirent/readdir.c:33
> #3 00000291 in __user_main (argc=4, argv=34509728)
> #4 00001189 in __uClibc_main (main=30020912, argc=4,
> argv=34509728, app_init=0, app_fini=0, rtld_fini=0, stack_end=0) at
> /home/vganesh/work/KLEE/klee-uclibc-0.02-x64/libc/misc/internals/__uClibc_main.c:402
> #5 00004421 in main (=4, =34509728)
>
>
>
>
> On Mon, Nov 4, 2013 at 5:35 PM, Urmas Repinski <urrimus at hotmail.com
> <mailto:urrimus at hotmail.com>> wrote:
>
> Hi, Vijay.
>
> Try to investigate following link
>
> http://buildroot-busybox.2317881.n4.nabble.com/PATCH-RFC-Fix-avr32-build-using-internal-toolchain-td38851.html
>
> The problem described there is the same as in your case, error is
>
>
> In file included from /usr/include/linux/rtnetlink.h:6,
> from libc/inet/netlinkaccess.h:32,
> from libc/inet/if_index.c:36:
>
> There is a patch also inside the message, copy last parts of the
> message into the patch file and try to execute it.
>
> Let me know if this helps,
> Urmas Repinski
>
>
> ------------------------------------------------------------------------
> Date: Mon, 4 Nov 2013 17:06:39 -0500
> From: hellovijay at gmail.com <mailto:hellovijay at gmail.com>
> To: rsas at cs.utah.edu <mailto:rsas at cs.utah.edu>
> CC: klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> Subject: Re: [klee-dev] Difficulty installing KLEE
>
>
> Okay. I installed the linked up llvm-gcc, reconfigured llvm like
> you said and there was some progress. However, now I am getting
> a new error when I make uclibc:
>
> In file included from /usr/include/linux/rtnetlink.h:6,
> from libc/inet/netlinkaccess.h:32,
> from libc/inet/if_index.c:36:
> /usr/include/linux/if_link.h:313: error: expected
> specifier-qualifier-list before '__be16'
> make: *** [libc/inet/if_index.os] Error 1
>
> This time I am going to do a clean install from the start,
> following the steps exactly to see if that would fix the error.
>
> Cheers,
> Vijay Ganesh.
>
>
>
> On Mon, Nov 4, 2013 at 4:59 PM, Vijay Ganesh
> <hellovijay at gmail.com <mailto:hellovijay at gmail.com>> wrote:
>
> I actually did. However, I didn't install the llvm-gcc
> linked up from the KLEE website. I instead sudoed it. I then
> configured llvm, and installed it.
>
> Is it important that I didn't install llvm-gcc linked up
> from the KLEE website?
>
> Cheers,
> Vijay Ganesh.
>
>
>
> On Mon, Nov 4, 2013 at 4:50 PM, Raimondas Sasnauskas
> <rsas at cs.utah.edu <mailto:rsas at cs.utah.edu>> wrote:
>
> Vijay,
>
> Before building llvm, you have to make sure you have
> llvm-gcc in your path.
>
> To fix this issue, download and add llvm-gcc to your
> path, then
> reconfigure llvm. Not sure if rebuilding is necessary.
>
> Raimondas
>
> On 11/4/13 2:46 PM, Vijay Ganesh wrote:
> > Thanks Cristian!
> >
> > I managed to install llvm.
> >
> > Another problem. When I compile the 64bit uclibc from
> the KLEE website,
> > I get the following error. (I configured by using the
> command
> > ./configure
> --with-llvm=/path/to/llvm-top-level-directory):
> >
> > gcc-4.6: error: unrecognized option ‘--emit-llvm’
> > gcc-4.6: error: unrecognized option ‘--emit-llvm’
> > gcc-4.6: error: unrecognized option '--emit-llvm'
> > gcc-4.6: error: unrecognized option '--emit-llvm'
> > gcc-4.6: error: unrecognized option '--emit-llvm'
> > gcc-4.6: error: unrecognized option '--emit-llvm'
> > CC libcrypt/des.os
> > gcc-4.6: error: unrecognized option '--emit-llvm'
> > make: *** [libcrypt/des.os] Error 1
> >
> > -Vijay.
> >
> >
> >
> > On Mon, Nov 4, 2013 at 4:06 PM, Cristian Cadar
> <c.cadar at imperial.ac.uk <mailto:c.cadar at imperial.ac.uk>
> > <mailto:c.cadar at imperial.ac.uk
> <mailto:c.cadar at imperial.ac.uk>>> wrote:
> >
> > Hi Vijay, please see this message from Dan:
> >
> http://www.mail-archive.com/__klee-dev@imperial.ac.uk/__msg01302.html
> <http://www.mail-archive.com/__klee-dev%40imperial.ac.uk/__msg01302.html>
> <http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01302.html
> <http://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg01302.html>>
> >
> > We should add a note on the website about this.
> >
> > Best,
> > Cristian
> >
> >
> > On 04/11/2013 20:56, Vijay Ganesh wrote:
> >
> >
> > Hi All,
> >
> > I am having difficulty installing the latest
> version of KLEE, or
> > to be
> > more precise LLVM.
> >
> > I am trying out llvm 2.9. I followed the
> instructions carefully.
> > I am
> > running 64-bit Linux Mint.
> >
> > I get the following compile errors:
> >
> > make[3]: Entering directory
> >
> `/home/vganesh/llvm-2.9/lib/__ExecutionEngine/JIT'
> > llvm[3]: Compiling Intercept.cpp for
> Release+Asserts build
> > In file included from JIT.h:17:0,
> > from Intercept.cpp:18:
> >
> /home/vganesh/llvm-2.9/__include/llvm/ExecutionEngine/__ExecutionEngine.h:
> > In member function ‘virtual void*
> >
> llvm::ExecutionEngine::__getOrEmitGlobalVariable(const
> > llvm::GlobalVariable*)’:
> >
> /home/vganesh/llvm-2.9/__include/llvm/ExecutionEngine/__ExecutionEngine.h:343:45:
> > warning: cast from type ‘const
> llvm::GlobalVariable*’ to type
> > ‘llvm::GlobalValue*’ casts away qualifiers
> [-Wcast-qual]
> > Intercept.cpp: In constructor
> > ‘{anonymous}::StatSymbols::__StatSymbols()’:
> > Intercept.cpp:69:67: error: ‘lseek64’ was not
> declared in this scope
> > /bin/rm: cannot remove
> >
> ‘/home/vganesh/llvm-2.9/lib/__ExecutionEngine/JIT/Release+__Asserts/Intercept.d.tmp’:
> > No such file or directory
> > make[3]: ***
> >
> [/home/vganesh/llvm-2.9/lib/__ExecutionEngine/JIT/Release+__Asserts/Intercept.o]
> > Error 1
> > make[3]: Leaving directory
> >
> `/home/vganesh/llvm-2.9/lib/__ExecutionEngine/JIT'
> > make[2]: *** [JIT/.makeall] Error 2
> > make[2]: Leaving directory
> > `/home/vganesh/llvm-2.9/lib/__ExecutionEngine'
> > make[1]: *** [ExecutionEngine/.makeall] Error 2
> > make[1]: Leaving directory
> `/home/vganesh/llvm-2.9/lib'
> > make: *** [all] Error 1
> >
> >
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
>
> _______________________________________________ klee-dev mailing
> list klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
More information about the klee-dev
mailing list