I do not know the answer to that question. I know for a fact that KLEE and klee-uclibc will compile on Ubuntu 12.04 LTS because I have used it. However KLEE does compile on very new distributions (I use Arch Linux which is very new) but currently klee-uclibc won't compile on very new kernels. We hope to fix that in the near future though.
On 21 September 2013 17:40, Saikat Dutta <[email protected]> wrote: > 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
