[klee-dev] Running Multifile Applications using Klee

[Daniel Liew]

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 <saikatdutta.pro2011 at gmail.com> 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 <daniel.liew at imperial.ac.uk>
> 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 <daniel.liew at imperial.ac.uk>
>> 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 <saikatdutta.pro2011 at gmail.com>
>> > 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
>> >> <daniel.liew at imperial.ac.uk>
>> >> wrote:
>> >>>
>> >>> On 20 September 2013 17:15, Saikat Dutta
>> >>> <saikatdutta.pro2011 at gmail.com>
>> >>> 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.
>> >>
>> >>
>
>