Apply KLEE to simple Python program

[Loi Luu]

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.

[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

Post by Loi Luu
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.

[Loi Luu]

Hi Daniel,

Thank you for your help, I will try with Cpython and unladen-swallow.

Post by 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

Post by Loi Luu
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

Post by Loi Luu
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

Post by Loi Luu
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.

[g***@public.gmane.org]

Hello,

Post by Loi Luu
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
(...)
So anyone has tried or has any comment about this idea? I would love to
know.

The question is:
* Do you want to symbolically analyse python interpreter running given
python code ?
Or
* Do you want to symbolically analyse python code ?

If first option: KLEE sounds like good candidate.

If second option:
It might be overkill, showing you interesting properties that apply
only to given interpreter... but still, it should be possible.

Cheers,
Greg

[Loi Luu]

Hi Greg,

Yes, what I want is the second option. However, I haven't got your point
about the first one, can you explain more about it?

Thanks,

Post by g***@public.gmane.org
Hello,

Post by Loi Luu
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
(...)
So anyone has tried or has any comment about this idea? I would love to
know.

* Do you want to symbolically analyse python interpreter running given
python code ?
Or
* Do you want to symbolically analyse python code ?
If first option: KLEE sounds like good candidate.
It might be overkill, showing you interesting properties that apply
only to given interpreter... but still, it should be possible.
Cheers,
Greg

[g***@public.gmane.org]

Hi Loi,

Post by Loi Luu
Yes, what I want is the second option. However, I haven't got your point
about the first one, can you explain more about it?

If you want second option , I am afraid you might need to create your
own solution.

If you want first, you will achieve it by symbolically executing
python interpreter running you code.

Cheers,
Greg