[klee-dev] Running Multifile Applications using Klee

[Daniel Liew]

Please CC the mailing list in future as this discussion may be useful to others.

On 20 September 2013 05:25, Saikat Dutta <saikatdutta.pro2011 at gmail.com> wrote:
> 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
> <saikatdutta.pro2011 at gmail.com> wrote:
>>
>> Hi,
>> 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
>>
>>
>> On Fri, Sep 20, 2013 at 6:04 AM, Lei Zhang <antiagainst at gmail.com> wrote:
>>>
>>> Wow, this is a nice tool. Thanks, Daniel!
>>>
>>>
>>> On Thu, Sep 19, 2013 at 10:22 AM, Daniel Liew
>>> <daniel.liew at imperial.ac.uk> wrote:
>>>>
>>>> If 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.
>>>>
>>>> On 18 September 2013 19:57, Lei Zhang <antiagainst at gmail.com> wrote:
>>>> > gzip is also maintained by GNU, like Coreutils. So they have the same
>>>> > build
>>>> > system. The method for Coreutils works for gzip.
>>>> >
>>>> > just have a try of the following:
>>>> >
>>>> > $ 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
>>>> > <saikatdutta.pro2011 at gmail.com> wrote:
>>>> >>
>>>> >> 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
>>>> >>
>>>> >>
>>>> >> On Wed, Sep 18, 2013 at 11:51 PM, Lei Zhang <antiagainst at gmail.com>
>>>> >> wrote:
>>>> >>>
>>>> >>> Hi 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
>>>> >>> <saikatdutta.pro2011 at gmail.com> wrote:
>>>> >>>>
>>>> >>>> Hi,
>>>> >>>> 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
>>>> >>>> klee-dev at imperial.ac.uk
>>>> >>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>> >>>>
>>>> >>>
>>>> >>>
>>>> >>>
>>>> >>> --
>>>> >>> Best regards,
>>>> >>> Lei Zhang
>>>> >>
>>>> >>
>>>> >
>>>> >
>>>> >
>>>> > --
>>>> > Best regards,
>>>> > Lei Zhang
>>>
>>>
>>>
>>>
>>> --
>>> Best regards,
>>> Lei Zhang
>>
>>
>