[klee-dev] Difficulty installing KLEE
Vijay Ganesh
hellovijay at gmail.com
Thu Nov 7 13:12:40 GMT 2013
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> 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>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
>> To: rsas at cs.utah.edu
>> CC: 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>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>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>> 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@imperial.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
>> > 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
>>
>>
>>
>>
>> _______________________________________________ klee-dev mailing list
>> 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
>>
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list