klee .bca files missing

[Alexandru Ionut Diaconescu]

Hello everyone !

I followed http://klee.llvm.org/GetStarted.html when installing Klee over
my LLVM 2.9 (as required), meaning :

1. Install dependencies DONE
export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/ DONE
export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/ DONE

2. Build LLVM 2.9 DONE
Install llvm-gcc DONE
Add llvm-gcc to my PATH DONE
export
PATH=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/
Download and build LLVM 2.9 DONE

3. Build STP DONE
with --with-cryptominisat2 at configuration AND make OPTIMIZE=-O2
CFLAGS_M32= install at make
ulimit -s unlimited DONE

4. Build uclibc with llvm-gcc DONE

5. svn klee DONE

6. Configure KLEE DONE
./configure --with-llvm=/home/alex/llvm2.9/llvm/
--with-stp=/home/alex/llvm2.9/llvm/stp/
--with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/
--with-llvm-build-mode=Release+Asserts --enable-posix-runtime
7. Build KLEE DONE
with ENABLE_OPTIMIZED=1
no errors, but I have the warning
"/home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries
require LLVM capable compiler but none is available ****"


However, when I am trying the tutorials, I have the segfault error :
klee: error: Cannot find linker input
'/home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'


They were not build at all during Klee compilation. Can you tell me what
can I do? Maybe my problem is related to this thread :
http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923 .

Thank you for any help !

[Alexandru Ionut Diaconescu]

Hi Daniel,

Thank you for your response.

1. uname -m gave me i686, so I am on 32b
2. yes, I have this:


configure:13234: checking for llvm-gcc
configure:13252: found /home/alex/llvmklee/llvm-gcc-
4.2-2.9-i686-linux/bin/llvm-gcc
configure:13264: result:
/home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-gcc

configure:13274: checking for llvm-g++
configure:13292: found
/home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-g++
configure:13304: result:
/home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-g++

configure:13340: checking LLVM capable compiler
configure:13358: result: llvm-gcc

What do you think I can do?

Hi Alexandru,
Can you confirm a few things for me?
1. Are you using a 32-bit version of Linux? A lot of the commands you
gave assume a 32-bit operating system. You can check by running
$ uname -m
Others have had problems when having mixed architecture builds (e.g. a
32-bit build of STP will not link with a 64-bit build of KLEE)
2. Can you check that LLVM detected your LLVM compiler (llvm-gcc) at
configure time?
To this look at the file config.log inside your LLVM build directory.
You should see a line like...
configure:13234: checking for llvm-gcc
configure:13252: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13264: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13274: checking for llvm-g++
configure:13292: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13304: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13340: checking LLVM capable compiler
configure:13358: result: llvm-gcc
configure:13363: checking tool compatibility
LLVM will still build even if llvm-gcc isn't found but KLEE will not
compile correctly if this happens.
Thanks,
Dan.
On 31 January 2013 21:07, Alexandru Ionut Diaconescu

Post by Alexandru Ionut Diaconescu
Hello everyone !
I followed http://klee.llvm.org/GetStarted.html when installing Klee

over my

Post by Alexandru Ionut Diaconescu
1. Install dependencies DONE
export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/ DONE
export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/ DONE
2. Build LLVM 2.9 DONE
Install llvm-gcc DONE
Add llvm-gcc to my PATH DONE
export

PATH=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/

Post by Alexandru Ionut Diaconescu
Download and build LLVM 2.9 DONE
3. Build STP DONE
with --with-cryptominisat2 at configuration AND make OPTIMIZE=-O2
CFLAGS_M32= install at make
ulimit -s unlimited DONE
4. Build uclibc with llvm-gcc DONE
5. svn klee DONE
6. Configure KLEE DONE
./configure --with-llvm=/home/alex/llvm2.9/llvm/
--with-stp=/home/alex/llvm2.9/llvm/stp/
--with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/
--with-llvm-build-mode=Release+Asserts --enable-posix-runtime
7. Build KLEE DONE
with ENABLE_OPTIMIZED=1
no errors, but I have the warning
"/home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries
require LLVM capable compiler but none is available ****"
klee: error: Cannot find linker input

'/home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'

Post by Alexandru Ionut Diaconescu
They were not build at all during Klee compilation. Can you tell me what

can

Post by Alexandru Ionut Diaconescu
http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923 .
Thank you for any help !
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Paul Thomson]

Try the following:
- Look at Makefile.config in the "llvm source/build directory" and
ensure that LLVMGCC is set correctly (with full path to the binary).
- Now, re-configure klee and make sure the "llvm source/build
directory" is specified (not the binary directory).
- For me, in the klee directory, I have:
-- in Makefile.config: LLVM_OBJ_ROOT is set to the "llvm source/build
directory" from previous steps.
-- in Makefile.common I have: include
$(LLVM_OBJ_ROOT)/Makefile.config, which should ensure that the LLVMGCC
variable is set correctly.

Thanks,
Paul


On 1 February 2013 14:33, Alexandru Ionut Diaconescu

Post by Alexandru Ionut Diaconescu
Hi Daniel,
Thank you for your response.
1. uname -m gave me i686, so I am on 32b
configure:13234: checking for llvm-gcc
configure:13252: found /home/alex/llvmklee/llvm-gcc-
4.2-2.9-i686-linux/bin/llvm-gcc
/home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-gcc
configure:13274: checking for llvm-g++
configure:13292: found
/home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-g++
/home/alex/llvmklee/llvm-gcc-4.2-2.9-i686-linux/bin/llvm-g++
configure:13340: checking LLVM capable compiler
configure:13358: result: llvm-gcc
What do you think I can do?

Hi Alexandru,
Can you confirm a few things for me?
1. Are you using a 32-bit version of Linux? A lot of the commands you
gave assume a 32-bit operating system. You can check by running
$ uname -m
Others have had problems when having mixed architecture builds (e.g. a
32-bit build of STP will not link with a 64-bit build of KLEE)
2. Can you check that LLVM detected your LLVM compiler (llvm-gcc) at
configure time?
To this look at the file config.log inside your LLVM build directory.
You should see a line like...
configure:13234: checking for llvm-gcc
configure:13252: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13264: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13274: checking for llvm-g++
configure:13292: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13304: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13340: checking LLVM capable compiler
configure:13358: result: llvm-gcc
configure:13363: checking tool compatibility
LLVM will still build even if llvm-gcc isn't found but KLEE will not
compile correctly if this happens.
Thanks,
Dan.
On 31 January 2013 21:07, Alexandru Ionut Diaconescu

Post by Alexandru Ionut Diaconescu
Hello everyone !
I followed http://klee.llvm.org/GetStarted.html when installing Klee
over my
1. Install dependencies DONE
export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/ DONE
export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/ DONE
2. Build LLVM 2.9 DONE
Install llvm-gcc DONE
Add llvm-gcc to my PATH DONE
export
PATH=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/
Download and build LLVM 2.9 DONE
3. Build STP DONE
with --with-cryptominisat2 at configuration AND make OPTIMIZE=-O2
CFLAGS_M32= install at make
ulimit -s unlimited DONE
4. Build uclibc with llvm-gcc DONE
5. svn klee DONE
6. Configure KLEE DONE
./configure --with-llvm=/home/alex/llvm2.9/llvm/
--with-stp=/home/alex/llvm2.9/llvm/stp/
--with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/
--with-llvm-build-mode=Release+Asserts --enable-posix-runtime
7. Build KLEE DONE
with ENABLE_OPTIMIZED=1
no errors, but I have the warning
"/home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries
require LLVM capable compiler but none is available ****"
klee: error: Cannot find linker input
'/home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'
They were not build at all during Klee compilation. Can you tell me what
can
http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923 .
Thank you for any help !
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

--
Best regards,
Alexandru Ionut Diaconescu
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Daniel Liew]

Hi Alexandru,

Can you confirm a few things for me?

1. Are you using a 32-bit version of Linux? A lot of the commands you
gave assume a 32-bit operating system. You can check by running

$ uname -m

Others have had problems when having mixed architecture builds (e.g. a
32-bit build of STP will not link with a 64-bit build of KLEE)

2. Can you check that LLVM detected your LLVM compiler (llvm-gcc) at
configure time?
To this look at the file config.log inside your LLVM build directory.
You should see a line like...
configure:13234: checking for llvm-gcc
configure:13252: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13264: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-gcc
configure:13274: checking for llvm-g++
configure:13292: found /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13304: result: /data/dev/KLEE/llvm-gcc/bin/bin//llvm-g++
configure:13340: checking LLVM capable compiler
configure:13358: result: llvm-gcc
configure:13363: checking tool compatibility

LLVM will still build even if llvm-gcc isn't found but KLEE will not
compile correctly if this happens.

Thanks,
Dan.

On 31 January 2013 21:07, Alexandru Ionut Diaconescu

Post by Alexandru Ionut Diaconescu
Hello everyone !
I followed http://klee.llvm.org/GetStarted.html when installing Klee over my
1. Install dependencies DONE
export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/ DONE
export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/ DONE
2. Build LLVM 2.9 DONE
Install llvm-gcc DONE
Add llvm-gcc to my PATH DONE
export
PATH=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/
Download and build LLVM 2.9 DONE
3. Build STP DONE
with --with-cryptominisat2 at configuration AND make OPTIMIZE=-O2
CFLAGS_M32= install at make
ulimit -s unlimited DONE
4. Build uclibc with llvm-gcc DONE
5. svn klee DONE
6. Configure KLEE DONE
./configure --with-llvm=/home/alex/llvm2.9/llvm/
--with-stp=/home/alex/llvm2.9/llvm/stp/
--with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/
--with-llvm-build-mode=Release+Asserts --enable-posix-runtime
7. Build KLEE DONE
with ENABLE_OPTIMIZED=1
no errors, but I have the warning
"/home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries
require LLVM capable compiler but none is available ****"
klee: error: Cannot find linker input
'/home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'
They were not build at all during Klee compilation. Can you tell me what can
http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923 .
Thank you for any help !
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Vijay Ganesh]

Hi All,

I am trying to create a KLEE-based lab assignment for my computer
security class. The idea is for students to get some facility in
using/possibly adding to KLEE. Any suggestions for interesting
assignments?