[klee-dev] Apply KLEE to simple Python program

[Daniel Liew]

Hi,

Your statement "as far as I know, Python was originated from C then
there possibly is a way to compile Python to C" is not correct. Python
as a language did not originate from C (although C probably inspired
some of it's syntax). Although the CPython interpreter is written in C
there are other interpreters (e.g. IronPython, PyPy and Jython) which
are not written in C. Python as a language is not tied specifically to
C.

I like the idea of symbolically executing python code but I imagine
it's going to challenging to get that working with KLEE.

Shedskin: AFAIK, KLEE cannot run C++ programs properly because it
doesn't have a standard C++ library. Support was implemented in a tool
name KLOVER ( https://www.google.co.uk/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDQQFjAA&url=http%3A%2F%2Fwww.cs.utah.edu%2F~ligd%2Fpublications%2FKLOVER-CAV11.pdf&ei=AWR9UdjkBM7FPIapgIgM&usg=AFQjCNGppURh9whe3E56ssYzUjmpVJDXcg&bvm=bv.45645796,d.ZWU
) but I don't think it's open source.

Cython: AFAIK this compiles to C code with the intention of building
shared libraries and the python module that can be called from within
python code. With that in mind I'm not sure you could use this
generated C code directly with KLEE because there will be no main()
function. You'd probably have to write some sort of program in C to
call the C code generated by Cython. I'm not 100% sure about this
though. You should just try it out.

You might want to take a look at
https://code.google.com/p/unladen-swallow/ . They took the CPython
interpreter and modified it to work with LLVM. The project doesn't
look very active though.

Regards,
Dan Liew

On 28 April 2013 17:47, Loi Luu <loi.luuthe at gmail.com> wrote:
> Dear all,
>
> I am having an idea that we can apply KLEE to automatically generate test
> cases for a simple Python program since, as far as I know, Python was
> originated from C then there possibly is a way to compile Python to C. After
> that, we can apply KLEE for the new C program.
>
> After searching for a short time, I found two tools that can do the job of
> compiling Python to C/C++ programs. One is shedkin
> https://code.google.com/p/shedskin/ and another one is Cython
> http://www.cython.org/
>
> So anyone has tried or has any comment about this idea? I would love to
> know.
>
> Thank you.
>
> --
> Loi, Luu The (Mr.)
> University of  Engineering and Technology, Vietnam National University,
> Hanoi.