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 <[email protected]>wrote: > Please CC the mailing list in future as this discussion may be useful to > others. > > On 20 September 2013 05:25, Saikat Dutta <[email protected]> > 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 > > <[email protected]> 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 <[email protected]> > wrote: > >>> > >>> Wow, this is a nice tool. Thanks, Daniel! > >>> > >>> > >>> On Thu, Sep 19, 2013 at 10:22 AM, Daniel Liew > >>> <[email protected]> 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 <[email protected]> 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 > >>>> > <[email protected]> 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 <[email protected] > > > >>>> >> 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 > >>>> >>> <[email protected]> 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 > >>>> >>>> [email protected] > >>>> >>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >>>> >>>> > >>>> >>> > >>>> >>> > >>>> >>> > >>>> >>> -- > >>>> >>> Best regards, > >>>> >>> Lei Zhang > >>>> >> > >>>> >> > >>>> > > >>>> > > >>>> > > >>>> > -- > >>>> > Best regards, > >>>> > Lei Zhang > >>> > >>> > >>> > >>> > >>> -- > >>> Best regards, > >>> Lei Zhang > >> > >> > > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
