Thanks. What is the latest ubuntu version that can run klee?
On Sat, Sep 21, 2013 at 10:07 PM, Daniel Liew <[email protected]>wrote: > Many non GNU projects use autotools so this approach will probably work > with them. Please remember that KLEE does not have a runtime C++ library so > it is unlikely you will be able to run many C++ programs. > > CMake is another common build system. You should be able to do something > similar when setting the CC flag. I'm not sure CFLAGS will work though ( > instead you might need to change the CMAKE_BUILD_TYPE variable). You will > have to experiment (cmake-gui is your friend ) > > Remember if you set WLLVM_OUTPUT=DEBUG then the command line passed to the > compiler will be shown on stderr which you can use to check that the "-g" > (debug symbols) "-O0" ( almost no optimisation ) are being passed to the > compiler > > Have fun with KLEE! > > Thanks, > Dan. > On 21 Sep 2013 15:36, "Saikat Dutta" <[email protected]> > wrote: > >> 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
