A symbolic execution engine for Python
Python Objective-C C Assembly C# Java Other
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
_cache
annotation
bin
config
doc
interpreter
jit
module
objspace
rlib First commit of sypy Nov 10, 2012
rpython
tool
translator
README.md
__init__.py
conftest.py
pytest-A.cfg
pytest.ini
test_all.py
testrunner_cfg.py

README.md

Sypy: A symbolic execution engine for Python.

Sypy leverages PyPy's interpreter to interpret Python bytecode and generate constraints. These constraints are solved using Microsoft's Z3 SMT solver.

Currently Sypy generates constraints for if statements involving integer values. While booleans, longs and floats have symbolic support they have not been tested yet. Function evaluation has not been tested yet. Besides, supporting arbitrary functions is probably not a good idea.

The most appropriate way would be to determine all possible return values of a function and substitute those values in the constraints.

TODO:

The most important thing to do right now is to interleave symbolic execution code in the binary operations.