Thanks .. its working :) ....can the same procedure be followed for non-GNU applications?
On Sat, Sep 21, 2013 at 5:28 PM, Daniel Liew <[email protected]>wrote: > Oops. I appear to have mislead you. KLEE can execute gzip.bc . The > problem is by default the gzip build system tells llvm-gcc to optimise > the code (-O2). You need to tell llvm-gcc to not optimise the code > (this seems to prevent the llvm.objectsize.*) intrinsic from being > used. You can do this by forcing the value of CFLAGS at configure time > like so... > > $ cd gzip-1.6 > $ make clean > $ CC=wllvm CFLAGS="-O0 -g" ./configure > $ make > $ extract-bc gzip > > Now > $ klee --libc=uclibc --posix-runtime gzip.bc --help > > Works. > > Hope that helps. > > Dan. > > On 21 September 2013 12:01, Saikat Dutta <[email protected]> > wrote: > > Ok....Dead End then....Thanks for your help a lot. You were very patient > > throughout. Let me know if theres any development in this ! > > Thanks. > > -Saikat > > > > > > On Sat, Sep 21, 2013 at 4:25 PM, Daniel Liew <[email protected] > > > > wrote: > >> > >> One possible workaround is to use an older version of LLVM and > >> llvm-gcc (I think you would need to use llvm-2.6) that doesn't > >> generate that intrinsic. I give no guarantees that this would work as > >> I have not tried using KLEE with this older version. > >> > >> I've added an issue to the KLEE issue tracker on your behalf ( > >> https://github.com/ccadar/klee/issues/33 ). There are no guarantees > >> that this will be fixed. > >> > >> If you need this to work **now** you need to implement support for > >> this intrinsic yourself. > >> > >> On 21 September 2013 11:42, Saikat Dutta <[email protected] > > > >> wrote: > >> > I got the same message: > >> > LLVM ERROR: Code generator does not support intrinsic function > >> > 'llvm.objectsize.i32'! > >> > So theres no existing solution to this? > >> > > >> > > >> > On Sat, Sep 21, 2013 at 3:40 PM, Daniel Liew > >> > <[email protected]> > >> > wrote: > >> >> > >> >> You're done. gzip.bc is a single LLVM module that is equivalent to > the > >> >> gzip binary. Now you just need to run KLEE on it. > >> >> > >> >> e.g. > >> >> > >> >> $ klee --libc=uclibc --posix-runtime gzip.bc --help > >> >> KLEE: NOTE: Using model: > >> >> > /data/dev/KLEE/klee/bin-dbg/Release+Asserts/lib/libkleeRuntimePOSIX.bca > >> >> KLEE: output directory = "klee-out-1" > >> >> LLVM ERROR: Code generator does not support intrinsic function > >> >> 'llvm.objectsize.i64'! > >> >> > >> >> I should note that this does not work on my machine because of > missing > >> >> support for a particular LLVM intrinsic function. You'll need to add > >> >> support for it: > >> >> http://llvm.org/docs/LangRef.html#llvm-objectsize-intrinsic > >> >> > >> >> A developer recently added support for another intrinsic so you could > >> >> use this as an example ( https://github.com/ccadar/klee/pull/27 ) > >> >> > >> >> If you get it working please consider contributing your code back to > >> >> the project so others can benefit. > >> >> > >> >> Thanks, > >> >> Dan Liew. > >> >> > >> >> > >> >> On 21 September 2013 10:36, Saikat Dutta > >> >> <[email protected]> > >> >> wrote: > >> >> > I upgraded to python 2.7 > >> >> > "extract-bc gzip" produced gzip.bc > >> >> > what to do next? > >> >> > > >> >> > > >> >> > On Sat, Sep 21, 2013 at 2:20 PM, Daniel Liew > >> >> > <[email protected]> > >> >> > wrote: > >> >> >> > >> >> >> Oh I forgot to mention that if you really don't feel like > upgrading > >> >> >> you could just modify the extract-bc python script by removing the > >> >> >> use > >> >> >> of argparse from the main() function and setting > >> >> >> > >> >> >> inputFile = sys.argv[1] > >> >> >> > >> >> >> On 20 September 2013 17:58, Daniel Liew < > [email protected]> > >> >> >> wrote: > >> >> >> > Your python install is too old (the argparse module was > introduced > >> >> >> > in > >> >> >> > python2.7) you need python 2.7 or later. You can find your > current > >> >> >> > python version by running > >> >> >> > > >> >> >> > $ python --version > >> >> >> > > >> >> >> > I think you said you were using Ubuntu 10.04 in which case the > >> >> >> > python > >> >> >> > version is probably 2.6.5 . Unless you have a good reason to be > >> >> >> > running such an old version of python (or Ubuntu for that > matter) > >> >> >> > you > >> >> >> > should upgrade. > >> >> >> > > >> >> >> > > >> >> >> > On 20 September 2013 17:50, Saikat Dutta > >> >> >> > <[email protected]> > >> >> >> > wrote: > >> >> >> >> Hi, > >> >> >> >> At the "extract-bc gzip" stage following error is produced: > >> >> >> >> > >> >> >> >> Traceback (most recent call last): > >> >> >> >> File > >> >> >> >> > >> >> >> >> > >> >> >> >> > >> >> >> >> > "/home/saikat/Downloads/llvm_new/whole-program-llvm-llvm-gcc/extract-bc", > >> >> >> >> line 269, in <module> > >> >> >> >> sys.exit(main(sys.argv)) > >> >> >> >> File > >> >> >> >> > >> >> >> >> > >> >> >> >> > >> >> >> >> > "/home/saikat/Downloads/llvm_new/whole-program-llvm-llvm-gcc/extract-bc", > >> >> >> >> line 212, in main > >> >> >> >> import argparse > >> >> >> >> ImportError: No module named argparse > >> >> >> >> > >> >> >> >> > >> >> >> >> > >> >> >> >> > >> >> >> >> > >> >> >> >> > >> >> >> >> On Fri, Sep 20, 2013 at 10:09 PM, Daniel Liew > >> >> >> >> <[email protected]> > >> >> >> >> wrote: > >> >> >> >>> > >> >> >> >>> On 20 September 2013 17:15, Saikat Dutta > >> >> >> >>> <[email protected]> > >> >> >> >>> wrote: > >> >> >> >>> > Hi, > >> >> >> >>> > Everything goes fine with wllvm according to the way you > >> >> >> >>> > described > >> >> >> >>> > in > >> >> >> >>> > the > >> >> >> >>> > previous mail. No errors till make step. > >> >> >> >>> > >> >> >> >>> If you don't tell us what the errors are we will **not** be > able > >> >> >> >>> to > >> >> >> >>> help you. If you see an error tell us what it is. > >> >> >> >>> > >> >> >> >>> > But instead of "gzip.bc" or > >> >> >> >>> > "gzip.o.bc" , ".gzip.o.bc" is being formed. > >> >> >> >>> > >> >> >> >>> .gzip.o.bc is a LLVM bitcode file that corresponds to the > gzip.o > >> >> >> >>> object file (this mostly likely corresponds with gzip.c) . It > is > >> >> >> >>> **not** the finally linked executable. You are only supposed > to > >> >> >> >>> run > >> >> >> >>> extract-bc on the the finally linked executable (or on static > >> >> >> >>> libraries) **not** on object files. > >> >> >> >>> > >> >> >> >>> I just tried this and it works fine. You should run extract-bc > >> >> >> >>> on > >> >> >> >>> the > >> >> >> >>> "gzip" executable. > >> >> >> >>> > >> >> >> >>> # I assume you have llvm-gcc in your path and it was the > >> >> >> >>> pre-built > >> >> >> >>> binary llvm-gcc 4.2 > >> >> >> >>> > >> >> >> >>> $ export LLVM_COMPILER=llvm-gcc > >> >> >> >>> $ export WLLVM_OUTPUT=WARNING > >> >> >> >>> $ export > >> >> >> >>> > >> >> >> >>> > >> >> >> >>> > LLVM_COMPILER_PATH=/your/path/to/the/llvm2.9/build/Release+Asserts/bin > >> >> >> >>> $ wget http://ftp.gnu.org/gnu/gzip/gzip-1.6.tar.xz > >> >> >> >>> $ tar -xvf gzip-1.6.tar.xz > >> >> >> >>> $ cd gzip-1.6 > >> >> >> >>> $ CC=wllvm ./configure > >> >> >> >>> $ make -j4 > >> >> >> >>> $ extract-bc gzip > >> >> >> >>> > >> >> >> >>> # gzip.bc will now be in the current directory > >> >> >> >>> > >> >> >> >>> > When I use extract bc on it, > >> >> >> >>> > error is generated. Please help. > >> >> >> >>> > -Saikat > >> >> >> >>> > >> >> >> >>> Again... If there is an error message tell us what it is. > >> >> >> >>> > >> >> >> >>> Hope that helps. > >> >> >> >>> > >> >> >> >>> Dan. > >> >> >> >> > >> >> >> >> > >> >> > > >> >> > > >> > > >> > > > > > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
