[klee-dev] KLEE usage compiler dependent ?

[Vitaly Chipounov]

Hi,

On 02.01.2013 18:31, Jonathan Neuschäfer wrote:
> AFAIK Klee should work with (almost) any bitcode that has been
> produced with a recent enough version of LLVM. So it should work with
> clang, too. For analyzing programs already compiled to machine code,
> you'd basically need a program that turns machine code back into LLVM
> bitcode. I don't know whether a production-quality program to do that
> exists, but libcpu (http://libcpu.org) might evolve into one.


Depending on your needs, a tool like RevGen [1] might be helpful. It
takes as input a binary and turns it into LLVM.
It is very experimental, but we had some success using it to remove
inline assembly from bitcode files in order to be able to run them in
KLEE. Some more insight on how it works can be found here [2].

[1]
https://github.com/dslab-epfl/s2e/blob/revgen/docs/Tools/StaticTranslator.rst
[2] http://dslab.epfl.ch/pubs/revgen.pdf

Vitaly