Building a Tiny Symbolic Executor in Python

I have been reading and exploring a lot about symbolic execution lately. Very fascinating stuff. Reading about it is one thing, but actually implementing it is another. I decided to build a tiny symbolic executor in Python with less than 70 lines of code to get a better undersAatanding of how it actually works. I will be using the Z3 Theorem Prover to solve the constraints generated by the symbolic execution executor.

The full code is available on GitHub. Try it out and get a sense of how symbolic execution works!

What is Symbolic Execution?

Symbolic execution is a technique that is used to explore all possible paths through a program. It is used to find bugs in software by exploring all possible paths through the program. This is a very powerful technique that can be used to find bugs in complex software.

Here are some related academic papers to read if you are interested in learning more about symbolic execution:

1. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
2. A Survey of Symbolic Execution Techniques
3. Symbolic Execution for Software Testing: Three Decades Later

Building a Tiny Symbolic Executor

The provided Python implementation of a symbolic execution engine is a simplified illustration intended for educational purposes. It demonstrates the basic principles of symbolic execution, such as overriding boolean evaluations to explore different execution paths and using Microsoft's Z3 theorem prover to solve for constraints. However, it does not encapsulate the full complexity and scope of real-world symbolic execution, such as handling arbitrary data types, complex control structures, and sophisticated program semantics.

Here is my class representing the symbolic execution engine:

class TinySymbolicExecutionEngine:

    def __init__(self):
        # Initialize the Z3 solver
        # Need to have some kind of data structure to keep track of constraints
        pass

    def add_constraint(self, condition: bool | BoolRef) -> None:
        # Add a constraint to the solver
        pass

    def is_path_feasible(self) -> bool:
        # Check if the current path is feasible
        pass

    def execute_path(self, func: callable, *args: object, **kwargs: object) -> None:
        # Execute a function symbolically
        pass

    def override_bool(self):
        # Somehow override the boolean evaluation logic of Z3's BoolRef objects
        pass

Instead of actual path forking, my implementation uses a context manager and setattr. This is a simplified approach that is not as robust as actual path forking, but it is sufficient for the purposes of this demonstration.

Context Manager Explanation

The context manager, implemented as the BoolOverride nested class within the override_bool method, is important to understand. Its purpose is to temporarily override the boolean evaluation logic of Z3's BoolRef objects while a function is executed symbolically. This is achieved using the setattr function, a built-in Python method used to dynamically set an attribute of an object. In this case, setattr is employed to modify the __bool__ method of BoolRef to a custom lambda function that invokes the engine's _bool_override method. This custom function adds the evaluated condition as a constraint to the solver, enabling the exploration of different execution paths.

setattr(BoolRef, "__bool__", lambda condition: self._bool_override(condition))

def _bool_override(self, condition: BoolRef) -> bool:
    self.add_constraint(condition)
    return self.is_path_feasible()

Running the Symbolic Executor

def test_function(x, y):
    z = 2 * x
    if z == y:
        if y == x + 10:
            assert False


if __name__ == "__main__":
    engine = TinySymbolicExecutionEngine()
    x = BitVec("x", 32)
    y = BitVec("y", 32)
    engine.execute_path(test_function, x, y)

Assertion failed under: [y = 20, x = 10]