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
