[klee-dev] Apply KLEE to simple Python program

[Loi Luu]

Hi Daniel,

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


On Mon, Apr 29, 2013 at 1:22 AM, Daniel Liew <daniel.liew at imperial.ac.uk>wrote:

> 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.
>



-- 
Loi, Luu The (Mr.)
University of  Engineering and Technology, Vietnam National University,
Hanoi.
-------------- next part --------------
HTML attachment scrubbed and removed