[klee-dev] Running Multifile Applications using Klee

[Daniel Liew]

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 <saikatdutta.pro2011 at gmail.com> 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 <daniel.liew at imperial.ac.uk>
> 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 <saikatdutta.pro2011 at gmail.com>
>> 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
>> > <daniel.liew at imperial.ac.uk>
>> > 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
>> >> <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.
>> >> >> >>
>> >> >> >>
>> >> >
>> >> >
>> >
>> >
>
>