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 <[email protected]
<mailto:[email protected]>> 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 <[email protected]
<mailto:[email protected]>> 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: [email protected] <mailto:[email protected]>
To: [email protected] <mailto:[email protected]>
CC: [email protected] <mailto:[email protected]>
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
<[email protected] <mailto:[email protected]>> 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
<[email protected] <mailto:[email protected]>> 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
<[email protected] <mailto:[email protected]>
> <mailto:[email protected]
<mailto:[email protected]>>> wrote:
>
> Hi Vijay, please see this message from Dan:
>
http://www.mail-archive.com/[email protected]/__msg01302.html
<http://www.mail-archive.com/__klee-dev%40imperial.ac.uk/__msg01302.html>
<http://www.mail-archive.com/[email protected]/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
> [email protected] <mailto:[email protected]>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing
list [email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
