Please CC the mailing list in future as this discussion may be useful to others.
Hi Daniel,
I was able to run wllvm. make step was successful. But no .bc file was
created. When I used klee over gzip.o then it returned : "KLEE: ERROR: error
loading program './gzip': Invalid bitcode signature"
You have not read the WLLVM instructions correctly.
1. wllvm builds both LLVM bitcode and native binaries at the same
time. The linked LLVM bitcode is not produced, you must extract this
manually after compiling with wllvm like so...
# Where gzip is the native binary, will produce gzip.bc
extract-bc gzip
2. wllvm doesn't actually support llvm-gcc because it is a deprecated
compiler. However I have a branch of wllvm that does support llvm-gcc
(in a hacky way) called 'llvm-gcc'. You can find it at
https://github.com/delcypher/whole-program-llvm/tree/llvm-gcc Then set
your environment as follows
# llvm-gcc must be in your path already!
export LLVM_COMPILER=llvm-gcc
# path should contain things like llvm-nm and llvm-dis
export LLVM_COMPILER_PATH=/your/path/to/the/llvm2.9/build/Release+Asserts/bin
# Optional but useful for seeing what commands are being executed
export WLLVM_OUTPUT=DEBUG
Note it is crucial that llvm-gcc be able to perform linking but you
may find that it is unable to do so you'll see error messages like...
/usr/bin/ld: cannot find crt1.o: No such file or directory
To fix this add symbolic links to these object files in to the
llvm-gcc lib folder .e.g
$ cd /path/to/llvm-gcc/bin/lib/gcc/x86_64-unknown-linux-gnu/4.2.1
$ ln -s /usr/lib/x86_64-linux-gnu/crt1.o
$ ln -s /usr/lib/x86_64-linux-gnu/crto.o
$ ln -s /usr/lib/x86_64-linux-gnu/crti.o
Hope that helps.
Dan.
On Fri, Sep 20, 2013 at 8:55 AM, Saikat Dutta
Post by Saikat DuttaHi,
I am using llvm-2.9 and path has been set for llvm-gcc as well as klee. I
am using Linux 10.04 32 bit. I have installed everything just as mentioned
in klee's website. Also please help me set up wllvm. I tried following the
instructions given with it, but its not working.How can I use it? Need all
steps.
Thanks.
-Saikat
Post by Lei ZhangWow, this is a nice tool. Thanks, Daniel!
On Thu, Sep 19, 2013 at 10:22 AM, Daniel Liew
Post by Daniel LiewIf it helps there is a very nice tool called wllvm which acts as a
wrapper to clang which you can use to build whole programs in native
form and LLVM bitcode form.
The original author's code is at
https://github.com/travitch/whole-program-llvm
I have a fork of this which adds a bunch of features that you may find useful
https://github.com/delcypher/whole-program-llvm
Thanks,
Dan.
Post by Lei Zhanggzip is also maintained by GNU, like Coreutils. So they have the same build
system. The method for Coreutils works for gzip.
$ wget http://ftp.gnu.org/gnu/gzip/gzip-1.6.tar.xz
$ unxz ./gzip-1.6.tar.xz
$ tar xf ./gzip-1.6.tar
$ cd gzip-1.6
$ mkdir obj-llvm
$ ../configure CFLAGS="-g"
$ make CC=`which klee-gcc`
This will generate the gzip.bc without problems.
On Wed, Sep 18, 2013 at 2:35 PM, Saikat Dutta
Hi,
I was talking about multiple file programs containing multiple .c and .h
files. For klee to run it is required to compile the code with llvm-gcc. I
have used klee for single file programs. But I am not sure on how to use
klee over such multiple file applications. Will putting CC variable in the
makefile as llvm-gcc do the job? It will be best if you can send me an
example over how to do that. Please do help. I am in urgent need.
Thanks.
-Saikat
Post by Lei ZhangHi Saikat,
From my understanding, every .c file is compiled and then linked to the
final binary. By running KLEE on that binary, you are touching code in all
these source files. And you can verify that by checking the 'gcov' output.
Or maybe I didn't fully understand your concern? Could you specify your
tasks more clearly?
On Tue, Sep 17, 2013 at 2:25 PM, Saikat Dutta
Post by Saikat DuttaHi,
I am working on a research project where i need to run multiple file
programs using klee. I am actually testing the gzip utility which
contains a
number of .c and .h files. Can you help me in this regard?
Thanks.
-Saikat
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--
Best regards,
Lei Zhang
--
Best regards,
Lei Zhang
--
Best regards,
Lei Zhang