[klee-dev] Running Multifile Applications using Klee

[Daniel Liew]

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 <saikatdutta.pro2011 at gmail.com> wrote:
> Thanks. What is the latest ubuntu version that can run klee?
>
>
> On Sat, Sep 21, 2013 at 10:07 PM, Daniel Liew <daniel.liew at imperial.ac.uk>
> 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" <saikatdutta.pro2011 at gmail.com>
>> 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 <daniel.liew at imperial.ac.uk>
>>> 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 <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.
>>>> >> >> >> >>
>>>> >> >> >> >>
>>>> >> >> >
>>>> >> >> >
>>>> >> >
>>>> >> >
>>>> >
>>>> >
>>>
>>>
>