Python Exploration with PySMT
This code is a substantial rewrite of the PyExZ3 (https://github.com/thomasjball/PyExZ3) symbolic execution engine for Python, now using the PySMT project (https://github.com/pysmt/pysmt).
# Install this fork of PySMT
git clone https://github.com/FedericoAureliano/pysmt.git
cd pysmt
sudo python3 setup.py install
cd ..
# Install PyExSMT
git clone https://github.com/FedericoAureliano/PyExSMT.git
cd PyExSMT
sudo python3 setup.py install
# To display graphs
sudo apt install graphvizusage: pyexsmt [-h] [--log LOGLEVEL] [--uninterp name return_type arg_types]
[--entry ENTRY] [--graph] [--summary] [--max-iters MAX_ITERS]
[--max-depth MAX_DEPTH] [--solver SOLVER]
file
def lib(x,y):
if x == 0:
return 0
else:
return x + y
return 10
def demo(in1, in2, in3):
if lib(in1, in2) > 0:
return 0
else:
return lib(in2, in3)pyexsmt --graph demo.pypyexsmt --graph --uninterp lib int [int,int] demo.pypyexsmt --graph --entry lib demo.pypyexsmt --summary demo.py
Summary:
((in1 = 0) ? ((in2 = 0) ? 0 : (in2 + in3)) : ((0 < (in1 + in2)) ? 0 : ((in2 = 0) ? 0 : (in2 + in3))))
pyexsmt --summary --uninterp lib int [int,int] demo.py
Summary:
((0 < lib(in1, in2)) ? 0 : lib(in2, in3))
pyexsmt --summary --entry lib demo.py
Summary:
((x = 0) ? 0 : (x + y))