[klee-dev] Running Multifile Applications using Klee

[Saikat Dutta]

Hi,
Everything goes fine with wllvm according to the way you described in the
previous mail. No errors till make step. But instead of "gzip.bc" or
"gzip.o.bc" , ".gzip.o.bc" is being formed. When I use extract bc on it,
error is generated. Please help.
-Saikat


On Fri, Sep 20, 2013 at 6:11 PM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> 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
> >>
> >>
> >
>
-------------- next part --------------
HTML attachment scrubbed and removed