Tutorial: concolic execution

Concolic (concrete + symbolic) execution runs a program on real inputs while simultaneously building up the symbolic path constraint that describes why it went the way it did. Negating one branch of that constraint and solving gives you inputs that drive the program down a different path — so you can automatically discover every branch. This tutorial follows the shipped concolic.py example and drives its explorer to find the paths through a function.

The one thing operator overloading can’t do

Most of a symbolic executor can be built with ordinary Python: wrap each input in a proxy object whose arithmetic and comparison operators build a symbolic term as a side effect. The example calls this proxy Sym:

class Sym:
    __slots__ = ("v", "t")           # concrete value, symbolic term

    def __init__(self, v, t):
        self.v, self.t = v, t

    def __mul__(self, other):
        ov, ot = _split(other)
        return Sym(self.v * ov, Bin("*", self.t, ot))   # x * 2  ->  Sym(.., (x * 2))
    # ... __add__, __lt__, __gt__, __eq__, and friends similarly ...

That handles data flow. What overloading cannot intercept is control flow: when Python evaluates if x > 0:, it calls bool() on the condition and then branches — and bool() must return a real True/False, discarding the symbolic term. This is exactly the seam Pyccolo fills.

Capturing branch conditions

Pyccolo fires after_if_test and after_while_test with the value the branch is about to use, and lets the handler replace it. The tracer records the symbolic condition as a path constraint, then returns the plain concrete bool so CPython takes the same branch the concrete run would:

class ConcolicTracer(pyc.BaseTracer):
    instrument_all_files = True       # instrument the target function's file too

    @pyc.register_raw_handler(pyc.after_if_test)
    def handle_if_test(self, ret, node_id, *_, **__):
        if not isinstance(ret, Sym):
            return ret                # concrete condition: nothing to record
        self.path.append(Branch(node_id, bool(ret.v), _as_bool_term(ret.t)))
        return bool(ret.v)            # keep CPython on the concrete path

else needs no special handling — it is just the fall-through when the if records False — and Python desugars elif into a nested if, so each one gets its own event for free.

Short-circuit and / or are handled precisely with the thunk that before_boolop_arg provides (see Observe and override values): the tracer wraps each operand’s thunk so it records that operand’s term only if it is actually evaluated. On the path where x > 0 is false, the y > 0 operand of x > 0 and y > 0 is never forced, so it never enters the constraint.

The search loop

After a run, the tracer holds an ordered list of branch decisions. To reach a new path, the explore helper negates one decision, keeps the earlier ones, hands the conjunction to a solver (Z3 if installed, otherwise a small bounded brute-force search), and re-runs with the solved inputs — repeating until no new paths appear. Note tracer.instrumented(func): the target function is instrumented in place (see Tracing real programs) so its branch tests emit events.

Exploring a function

Let’s drive it. classify has four reachable paths, and concolic exploration finds all of them starting from a single seed input:

from pyccolo.examples import concolic
from pyccolo.examples.concolic import explore

results = explore(concolic.classify, {"x": 0, "y": 0})
assert {r.retval for r in results} == {
    "x<0", "x==0", "x>0, y<=x", "x>0, y>x",
}

The real power shows up when a branch is only reachable for one precise input. In needs_solver, y = x * 2 and the code checks y == 12 then x > 5 — so the "jackpot" branch is reachable only when x == 6, and the solver derives that for you:

results = explore(concolic.needs_solver, {"x": 0})
jackpot = [r.inputs for r in results if r.retval == "jackpot"]
assert jackpot == [{"x": 6}]        # solved from the path constraint, not guessed

Because y == 12 forces x == 6 and 6 > 5 always holds, the "almost" branch is unreachable — and concolic exploration simply never reports it. Short-circuit branches work too: region uses and / or in its tests, and each discovered path’s constraint reflects exactly the operands that ran.

results = explore(concolic.region, {"x": 0, "y": 0})
assert {r.retval for r in results} == {
    "has-negative", "on-axis", "quadrant-1",
}

Run python pyccolo/examples/concolic.py from the repository root to see the full demo, including the path constraint printed for each discovered path.

Where to next

Concolic execution leans on three Pyccolo features you’ve now seen: overriding a branch test’s value (Observe and override values), the short-circuit thunk of before_boolop_arg, and instrumenting an ordinary function (Tracing real programs). The watchpoint debugger is a gentler next build if the symbolic machinery here was a lot at once.