[klee-dev] Difficulty installing KLEE
David Lightstone
david.lightstone at prodigy.net
Thu Nov 7 14:30:10 GMT 2013
Reply within body of original
Dave Lightstone
From: klee-dev-bounces at imperial.ac.uk
[mailto:klee-dev-bounces at imperial.ac.uk] On Behalf Of Vijay Ganesh
Sent: Thursday, November 07, 2013 8:13 AM
To: klee
Subject: Re: [klee-dev] Difficulty installing KLEE
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.
Freescale certainly uses a VMWare Player strategy to distribute LTIB with
some of their evaluation boards.
Certainly a Linux virtual machine having KLEE pre-installed is possible. I
use such an environment.
Distributing that environment will be a rather slow process. My installation
is a least 5 gig (Klee currently is on my archive drive at home, so I cannot
give accurate size estimates). Without a high bandwidth Internet connection
download time can easily be measured in days.
sudo apt-get install klee. Anyone?
I am not familiar with the means for generating apt-get installable
packages, so I cannot comment here.
I have send my build scripts out a couple of times. I suspect that
maintaining a couple of reference scripts will be far easier.
The difficulties which I have observed in building KLEE have been primarily
related to environmental dependencies, and the shared LLVM make files.
A good listing of those dependencies probably will go a long way toward
resolving the install problems.
Getting the interaction between the environment and the LLVM shared make
files is probably the key precondition for a successful build.
A hack out the installation build style (which I originally tried, and you
apparently have recently tried) is definitely not a good idea
Installing additional packages after building LLVM can lead to state
depended failures. KLEE relies upon the LLVM build to detect the state of
installed packages and environment. Each time a package is installed that
state evaluation ceases to be valid. Mortal human beings not being aware of
this coupling tend to experience build failure of the form - ".. but I have
installed package XXX,"
--------------------------------------------
* 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-softwar
e
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_ma
in.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_ma
in.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-usi
ng-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%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:34
3: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/Intercep
t.d.tmp':
> No such file or directory
> make[3]: ***
>
[/home/vganesh/llvm-2.9/lib/__ExecutionEngine/JIT/Release+__Asserts/Intercep
t.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