Learning big legacy codebases is a chore. I wish there were more tools to help me learn what is going on in an existing application. There is a lot of focus on designing and building new software, but when it comes to modifying existing ones, especially the one you did not write yourself you are kind of on your own. This motivated me to look for tools and methodologies to help understand existing code better. Methodology this short post is about is called Symbolic Dynamic Execution and it belongs to Software Analysis branch of Computer Science. Without going too much into detail, Symbolic Dynamic Execution is like reading the code and running it in your head. I will not go in depth about symbolic execution itself, I will focus on how you can use it to learn all possible states a piece of Python code can end up in - something that could one day become part of your toolkit for exploring code.

PyExZ3 is a tool for exploring Python functions

I found PyExZ3 which implements idea from paper Deconstructing Dynamic Symbolic Execution from Microsoft Research. In short this tool allows you to learn what combinations of inputs to given function will allow to reach all possible execution paths, and with what outputs. This is a software equivalent of analysing a function in maths: just like you need to know within which range the function is even defined, it is handy to know what values cause an exception in a programmatic one. Except that with PyExZ3 you can also learn all possible outputs and meaningful inputs, not just those for which the function works at all.

Example Analysis

How does it work in practice? Lets consider a following python function:

def intfuzz(a, b):
    if a == 2 :
        return 'fizz'
    if b < 2:
        return 'bar'
    if (a - b) > 2:
        return 'buzz'

This one is simple, you can run it in your head so it is a good example to demonstrate how PyExZ3 would go about evaluating it. At the same time it contains enough conditions that you might miss one possible return value (None) and not be able to immediately tell for what a and b you get buzz. Lets see the PyExZ3 output for intfuzz:

PyExZ3 (Python Exploration with Z3)
Exploring intfuzz.intfuzz
[('a', 0), ('b', 0)]
bar
[('a', 2), ('b', 0)]
fizz
[('a', 0), ('b', 2)]
None
[('a', 10), ('b', 7)]
buzz

PyExZ3 reported 4 possible outputs: bar, fizz, buzz and None. It also provided examples of concrete values for function parameters that yield given outputs. It is worth pointing out that PyExZ3 or this approach in general wont give you a full range for which the output is achieved, just one example. This is a consequence of how Z3 solver works (plus it would simply be significantly more complex, especially for types other than int).

How Does it work?!

PyExZ3 implements so called symbolic types that inherit from python primitive types. They behave exactly like normal python primitives (such as an int) except that whenever you call any of their operators (==, >, < etc) they register those comparisons along with the values they were compared against.

a == 2 
# this will call SymbolicInt operator __eq__ 
# and register that variable a was compared against 2
# PyExZ3 will also register if the comparison 
# turned out to be False or True

One execution of code along with a registry of all operator calls results in code execution path: a set of conditions that result in reaching certain point in code.

if a > 2 and b < 2:
    # if you reach this point, `a` must be higher
    # than 2 and `b` lower than 2
    # PyExZ3 stores these conditions after 
    # each execution

PyExZ3 starts scanning your function by injecting instances of symbolic implementations for function params and testing it with different values.

def fun(a:int, b:int):
    # PyExZ3 will start by plugging SymbolicInt 
    # for each of the params, with value of 0

Once it has one first execution (it does not matter what values you start with, Z3 puts 0 for int types) it will start looking fo counter-examples to this execution path by negating some of the conditions and trying again.

if a > 2 and b <2:
    return 'bar'  # we already know how to get here
    # in order to learn a new path we need to make sure to 
    # negate one of the conditions that led here. 
    # For instance make a < 2.
    # and then try again.

How can it help with legacy code?

PyExZ3 is a proof of concept, you cannot readily use it for your work. But I can imagine one could build tools using its methodology, for instance an IDE plugin that would run such exploration on every function you hover your mouse over, this could help you spot some unexpected input combinations or simply unhandled exceptions waiting to happen.