[klee-dev] Difficulty installing KLEE

Urmas Repinski urrimus at hotmail.com
Thu Nov 7 13:06:00 GMT 2013 

Hi, Vijay.

As far as i see,

This is the modifications that are suggested behind the link i had send in netlinkaccess.h file, (if to remove initial +, have no idea where it is from):
http://buildroot-busybox.2317881.n4.nabble.com/PATCH-RFC-Fix-avr32-build-using-internal-toolchain-td38851.html

diff -Nurp a/libc/inet/netlinkaccess.h b/libc/inet/netlinkaccess.h

--- a/libc/inet/netlinkaccess.h	2011-06-08 19:58:40.000000000 +0100

+++ b/libc/inet/netlinkaccess.h	2012-12-20 12:16:34.251965672 +0000

@@ -22,15 +22,8 @@

 #include <features.h>

 #include <stdint.h>

 #include <unistd.h>

-#include <sys/types.h>

-

 #if defined __ASSUME_NETLINK_SUPPORT || defined __UCLIBC_USE_NETLINK__

-#define _LINUX_TYPES_H

-typedef uint8_t __u8;

-typedef uint16_t __u16;

-typedef uint32_t __u32;

-typedef uint64_t __u64;

-typedef int32_t __s32;

+#include <asm/types.h>

 #include <linux/rtnetlink.h>

 #include <linux/netlink.h>


So i suggest not to remove lines only but to exactly remove all those lines that are required, and to add 
"#include <asm/types.h>"

too.

Lets try to implement this suggested in the link method at first, and if klee will still fail, then will try something else.

Errors during the netlinkaccess.h modifications can be source of the future errors.

Urmas Repinski.

Date: Thu, 7 Nov 2013 07:44:33 -0500
Subject: Re: [klee-dev] Difficulty installing KLEE
From: hellovijay at gmail.com
To: urrimus at hotmail.com
CC: klee-dev at imperial.ac.uk

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