Symbolic Execution

Symbolic execution evaluates a Boolean function against a state: a set of bindings from variables to other Boolean functions. Every variable that the state knows about is replaced by what it is bound to, and every node of the function is simplified on the way back up. A variable bound to a constant disappears from the result, a variable bound to another function is replaced by it, and a variable the state has never heard of simply stays symbolic.

That is the whole idea, and it sits one level below SMT solving. The solver searches for assignments and can prove that none exist; symbolic execution only rewrites, which makes it cheap, exact and unable to answer an existence question. The two are complementary: rewrite a function down to something small, then hand what is left to the solver.

Symbolic execution lives in the hal::SMT namespace of the core API, in two classes: SymbolicState holds the bindings, and SymbolicExecution pairs a state with the evaluation itself.

Note: The direct interface is currently usable from C++ only. SymbolicExecution.evaluate() is bound to Python but raises TypeError: Unable to convert function return value to a Python type, because the binding hands out the raw C++ result type. The C++ snippets below therefore have no line-by-line Python equivalent — but everything in Where you are already using it is reachable from Python, and Doing the same thing from Python covers what to write instead.

Where you are already using it

Most people meet symbolic execution without noticing, because it is the engine underneath the everyday Boolean function operations:

• simplify_local() is nothing but symbolic execution on an empty state, applied over and over until the function stops changing. With no bindings, evaluation still simplifies every node it visits — that is where the simplification comes from.
• simplify() runs that local pass, hands the result to ABC for global rewriting, and runs the local pass again.
• evaluate(inputs) binds each variable to the constant you gave it and folds the function to a value.
• compute_truth_table() calls evaluate() once per row, which is exactly why truth tables get expensive so quickly.

So the question is not whether to use symbolic execution, but whether you want to drive it yourself.

The state

SymbolicState maps Boolean functions to Boolean functions, with get() and set():

auto A = BooleanFunction::Var("A", 1);

auto state = SMT::SymbolicState();
state.set(A.clone(), BooleanFunction::Const(1, 1));

state.get(A);                              // 0b1
state.get(BooleanFunction::Var("B", 1));   // B — unbound keys return themselves

Two properties of set() are worth knowing before you build anything on it, because neither is announced at the call site:

• Only plain variables can be keys. set() silently does nothing if the key is anything else, so binding a whole expression such as A & B is not an error — it just has no effect.
• Bindings are write-once. Setting a key that is already bound is silently ignored and the original binding survives. set(R, 0) followed by set(R, 7) leaves R bound to 0.

The second one matters for anything that looks like stepping a circuit forward, and the section on unrolling below shows the way around it.

Evaluating

SymbolicExecution owns a state and evaluates functions in it. Bind what you know and evaluate what you want to learn about:

auto A = BooleanFunction::Var("A", 1);
auto B = BooleanFunction::Var("B", 1);
auto C = BooleanFunction::Var("C", 1);

// a 2-to-1 multiplexer: A selects between B and C
auto mux = (A.clone() & B.clone()) | (~A.clone() & C.clone());

auto exec = SMT::SymbolicExecution();
exec.state.set(A.clone(), BooleanFunction::Const(1, 1));

exec.evaluate(mux).get();   // B

Tying the select input to 1 does not just substitute it, it collapses the whole function: the result is B, not (1 & B) | (!1 & C). This is the everyday use of symbolic execution in reverse engineering — fix the control signals to the mode you care about and see what the datapath actually computes in that mode. A circuit that looks impenetrable in general is often trivial once its configuration bits are pinned down.

Bindings do not have to be constants. Binding a variable to another function is substitution with simplification:

auto exec = SMT::SymbolicExecution();
exec.state.set(A.clone(), B.clone());

exec.evaluate(mux).get();   // (B | C)

An unbound variable is left alone, which is what makes the result symbolic: evaluating mux in an empty state gives mux back, simplified as far as local rewriting can take it.

Unrolling over cycles

The obvious way to model a register updating over time is to bind it, evaluate its update function, and bind the result back:

auto R   = BooleanFunction::Var("R", 8);
auto inc = BooleanFunction::Add(R.clone(), BooleanFunction::Const(1, 8), 8).get();

auto exec = SMT::SymbolicExecution();
for (int cycle = 0; cycle < 3; cycle++)
{
    auto next = exec.evaluate(inc).get();
    exec.state.set(R.clone(), next.clone());   // does nothing after the first cycle!
}

This does not work, and it fails quietly. Because bindings are write-once, R keeps the value R + 1 it was given in the first iteration, so every later cycle recomputes the same (R + 1) + 1 instead of advancing.

Carry the value forward yourself instead, and the unrolling comes out as expected:

auto current = BooleanFunction::Var("R", 8);

auto exec = SMT::SymbolicExecution();
for (int cycle = 0; cycle < 3; cycle++)
{
    current = exec.evaluate(BooleanFunction::Add(current.clone(), BooleanFunction::Const(1, 8), 8).get()).get();
}
// current = (((R + 0b00000001) + 0b00000001) + 0b00000001)

Note how the expression grows with every cycle. That is the fundamental cost of unrolling, and it is why this is a tool for a handful of cycles rather than for whole runs — the same trade-off the Sequential Symbolic Execution plugin makes at the netlist level, over real flip-flops and with Z3 expressions instead of HAL Boolean functions.

Constraints as assignments

The Constraint type of the SMT interface can also be applied to a symbolic state, which is how you state a binding as an equation rather than as a set() call:

auto R = BooleanFunction::Var("R", 8);
auto X = BooleanFunction::Var("X", 8);

auto exec = SMT::SymbolicExecution();
exec.evaluate(SMT::Constraint(BooleanFunction::Add(X.clone(), BooleanFunction::Const(1, 8), 8).get(), R.clone()));

exec.state.get(R);   // (X + 0b00000001)

Mind the direction: the second function is the one that gets bound, and the first is evaluated in the current state to produce its value. Written as Constraint(expression, variable), in other words — the opposite of how an assignment is usually written, and the opposite of the equality reading the same constraint has when you hand it to a solver, where the two sides are interchangeable.

A constraint holding a single function is treated as a condition rather than an assignment. It has to be a comparison at the top level — Eq, Slt, Sle, Ult or Ule — and anything else is rejected with an error.

Doing the same thing from Python

Until evaluate() is usable from Python, substitute() followed by simplify_local() covers the one-shot case, and gives exactly the same results:

A = hal_py.BooleanFunction.Var("A", 1)
B = hal_py.BooleanFunction.Var("B", 1)
C = hal_py.BooleanFunction.Var("C", 1)

mux = (A & B) | (~A & C)

print(mux.substitute("A", hal_py.BooleanFunction.Const(1, 1)).simplify_local())   # B
print(mux.substitute("A", B).simplify_local())                                    # (B | C)

substitute() replaces a variable by a function without simplifying, and simplify_local() is the fixed-point of symbolic execution described above — together they are the same computation, just without a state that outlives the call. Use simplify() instead when you want ABC to have a go at the result as well.

What has no Python equivalent is the state itself: binding several variables once and evaluating many functions against them, or carrying a value across cycles. SymbolicState is constructible from Python and get/set work, but without evaluate() there is nothing to hand it to.

See also

• Boolean Function — the functions being evaluated, and substitute, simplify and evaluate.
• SMT Solving — when rewriting is not enough and you need a proof or a counterexample.
• Sequential Symbolic Execution — the plugin that unrolls a real netlist across clock cycles.
• Decorators — SubgraphNetlistDecorator composes the subcircuit functions worth evaluating in the first place.