RelativeTesting is a dynamic symbolic execution engine for Python that automatically generates test cases achieving condition coverage. It extends PyExZ3 (by Thomas Ball, Microsoft Research) with GPT-4 fallback constraint solving, AST-based loop unfolding, string type support, and a pre-constraint mechanism for defining input constraints via AST annotations.
This project was developed as a Sabanci University graduation project (ENS 492).
RelativeTesting builds on the PyExZ3 foundation with the following additions:
- GPT-4 Fallback Constraint Solving -- When Z3 cannot solve a constraint (e.g., semantic or non-linear constraints), the system falls back to OpenAI GPT-4 to generate satisfying inputs.
- AST-Based Loop Unfolding -- Loops are transformed into sequential code via AST rewriting, enabling symbolic analysis of iterative constructs that would otherwise be difficult to explore.
- String Symbolic Execution -- Support for symbolic string parameters (
SymbolicStr), extending beyond the original integer-only symbolic types. - Pre-Constraint Mechanism -- Users can define constraints on test inputs via AST annotations, allowing more targeted test generation.
- Input-to-Function Parameter Conversion -- Automated conversion of generated inputs into function parameters for direct execution.
Dynamic symbolic execution in RelativeTesting follows these steps:
- Concrete execution on symbolic arguments. The target function is executed with symbolic arguments (
SymbolicIntegerandSymbolicStrinherit from bothSymbolicObjectand the nativeint/strtypes). This dual inheritance allows the function to run concretely while collecting symbolic information. - Branch condition interception. Python's
__bool__method is overridden to intercept all branch conditions during execution, building a constraint tree that captures the path taken through the program. - Constraint solving with Z3. The Z3 theorem prover is used as the primary solver to negate path constraints and generate new inputs that will drive execution down previously uncovered paths.
- GPT-4 fallback. When Z3 cannot solve a constraint (e.g., due to semantic or non-linear relationships), the constraint is passed to GPT-4, which attempts to produce a satisfying assignment.
- Loop unfolding via AST rewriting. Before symbolic execution, loops in the target code are unfolded into sequential if-statements using AST transformations, enabling the symbolic engine to reason about iterative behavior.
User Code --> Loader --> ExplorationEngine
|-- PathToConstraint (branch interception via __bool__)
|-- Z3Wrapper (primary solver)
|-- Openai_wrap (GPT-4 fallback)
+-- LoopUnfolding (AST preprocessing)
pyexz3.py -- CLI entry point
symbolic/ -- Core symbolic execution engine
explore.py -- ExplorationEngine
path_to_constraint.py -- Constraint tree builder
openai_wrap.py -- GPT-4 fallback solver
symbolic_types/ -- SymbolicInteger, SymbolicStr, SymbolicDict
z3_expr/ -- Z3 expression builders
AST/ -- Loop unfolding and input detection
AST_loop_unfolding/
loop_unfolding.py -- AST-based loop transformation
generator/ -- Input-to-function conversion
func_generator.py -- Parameter conversion utilities
test/ -- Test cases for symbolic execution
reports/ -- Project report
run_tests.py -- Test runner
- Make sure that you use Python 32-bit (64-bit) if-and-only-if you use the Z3 32-bit (64-bit) binaries. Testing so far has been on Python 3.2.3 and 32-bit.
- Install Python 3.2.3 (https://www.python.org/download/releases/3.2.3/)
- Install the latest "unstable" release of Z3 to directory Z3HOME from http://z3.codeplex.com/releases (click on the "Planned" link on the right to get the latest binaries for all platforms)
- Add Z3HOME\bin to PATH and PYTHONPATH
- MacOS: setup.sh for Homebrew default locations for Python and Z3; see end for MacOS specific instructions
- Optional:
- Install GraphViz utilities (http://graphviz.org/)
- Grab yourself a Brew at http://brew.sh/
- Get the newest python or python3 version:
brew install python - Have the system prefer brew python over system python:
echo export PATH='/usr/local/bin:$PATH' >> ~/.bash_profile - Get z3:
brew install homebrew/science/z3 - Clone this repository:
git clone https://github.com/thomasjball/PyExZ3.git - Set the PATH:
. PyExZ3/setup.sh(do not run the setup script in a subshell./ PyExZ3/)
Vagrant is a cross-platform tool to manage virtualized development environments. Vagrant runs on Windows, OS X, and Linux and can manage virtual machines running on VirtualBox, VMware, Docker, and Hyper-V.
- Download Vagrant.
- Install VirtualBox or configure an alternative provider.
- Run
vagrant upfrom the PyExZ3 directory. The Vagrantfile in the repository tells Vagrant to download a Debian base image, launch it with the default provider (VirtualBox), and run the scriptvagrant.shto provision the machine. - Once the provisioning is done you can SSH into the machine using
vagrant sshand PyExZ3 is ready to run. Please note that the provisioning takes a while as Git is compiled from source as Debian's Git is incompatible with CodePlex where Z3 is hosted.
By default PyExZ3 uses the Z3 to solve path predicates. Optionally, the
CVC SMT solver can be enabled with the
--cvc argument. While the two solvers offer a similar feature set, the
integration of CVC differs from Z3 in a number of ways. Most
predominately, the CVC integration uses an unbounded rational number
representation for Python numbers, converting to bit vectors only for
bitwise operations. The Z3 integration uses bounded bit vectors for all
numbers. For programs that use any significant number of bitwise
operations, the default Z3-based configuration is strongly recommended.
Additionally, CVC does not support generating models for non-linear
relationships causing a few of the included PyExZ3 test cases to fail
with a LogicException.
python run_tests.py testshould pass all testspython pyexz3.py test/FILE.pyto run a single test from the test directory
Give a Python file FILE.py as input. By default, pyexz3 expects FILE.py
to contain a function named FILE where symbolic execution will start:
python pyexz3.py test/simple.pyYou can override the default starting function with --start MAIN,
where MAIN is the name of a function in FILE:
python pyexz3.py --start=MAIN test/FILE.pyBounding the number of iterations of the path exploration is essential when
analyzing functions with loops and/or recursion. Specify a bound using the --max-iters flag:
python pyexz3.py --max-iters=42 test/binary_search.pyBy default, pyexz3 associates a symbolic integer (with initial value 0) for each
parameter of the starting function. Import from symbolic.args to get the
@concrete and @symbolic decorators that let you override the defaults on the
starting function:
from symbolic.args import *
@concrete(a=1, b=2)
@symbolic(c=3)
def startingfun(a, b, c, d):
...The @concrete decorator declares that a parameter will not be treated symbolically
and provides an initial value for the parameter. The @symbolic decorator declares
that a parameter will be treated symbolically -- the type of the associated initial
value for the argument will be used to determine the proper symbolic type (if one
exists). In the above example, parameters a and b are treated concretely and
will have initial values 1 and 2 (for all paths explored), and parameter c
will be treated as a symbolic integer input with the initial value 3 (its value
can change after the first path has been explored). Since parameter d is not
specified, it will be treated as a symbolic integer input with the initial value 0.
python run_tests.py test--graph=DOTFILE-- Generate a graph of the explored paths in DOT format.--log=LOGFILE-- Write a log of the exploration to a file.--cvc-- Use the CVC SMT solver instead of Z3.
pyexz3 prints the list of generated inputs and corresponding observed
return values to standard out. The lists of generated inputs and the corresponding
return values are returned by the exploration engine to pyexz3 where they can be
used for other purposes.
If FILE.py contains a function named expected_result, then after path
exploration is complete, the list of return values will be compared against the
list returned by expected_result. More precisely, the two lists are converted
into bags and the bags compared for equality. If a function named
expected_result_set is present instead, the lists are converted into sets and
the sets are compared for equality. List equality is too strong a criteria for
testing, since small changes to programs can lead to paths being explored in
different orders.
The location of FILE.py is added to the import path so that all imports in
FILE.py relative to that file will work.
- Python 3 -- Core language
- Z3 Theorem Prover -- Primary constraint solver
- OpenAI GPT-4 API -- Fallback constraint solver
- Python AST module -- Loop unfolding and code transformation
- astor -- AST-to-source conversion
The project report is available at:
reports/ENS 492_Progress Report-II .docx.pdf
Students:
- Gorkem Yar
- Enis Mert Kuzu
- Huseyin Alper Karadeniz
- Rebah Ozkoc
Supervisors:
- Cemal Yilmaz
- Husnu Yenigun
This project is based on PyExZ3 by Thomas Ball (Microsoft Research). The original tool and its design are described in the paper Deconstructing Dynamic Symbolic Execution.
The NICE project (http://code.google.com/p/nice-of/) provided the original symbolic execution engine for Python. Bruni, Disney, and Flanagan described encoding symbolic execution for Python in Python in their 2008 paper A Peer Architecture for Lightweight Symbolic Execution.
See copyright.txt for license information.