Is the solidity built-in SMT Checker a form of symbolic execution?

Question

See question. Is the SMT Checker in solidity a form of symbolic execution?

Answer 1

Yes. It is.

Symbolic Execution Primer

Symbolic Execution is a means of analyzing a program to determine what inputs cause each part of a program to execute. It will convert the program to a symbolic expression (hence its name) to figure this out.

Aka, it will attempt to convert your program to a set of logical expressions. Aka aka: Make your code math.

This is also known as "path exploration" because getting this set of logical expressions will give you a formula that relates to conditionals, or "find it's path".

Example

For example, take this function:

function f(uint256 y) public {
  uint256 z = y * 2;
  if (z == 12) {
    revert();
  } 
}

If we wanted to prove there is an input for function f such that it would never revert, we'd convert this to a mathematical expression, like such:

z == 12 && // if z == 12, the program reverts
y >= 0 && y < type(uint256).max && // y is a uint256, so it must be within the uint256 range
z >= 0 && z < type(uint256).max && // z is also a uint256
z == y * 2; // our math

In this example, we have a set of 4 boolean expressions.

SAT Solver

We can then take this set of logical expressions and dump them into a SAT Solver (A SAT Solver is not symbolic execution, but right now is a popular next step). Which for now, you can think of as a black box that takes boolean expressions and tries to find an example that "satisfies" the set. For our example above, we are looking for a input y that enables the rest of the booleans to be true.

To dump this into a SAT solver, we need to convert our math to CNF form which might look something like this:

(z <= 12 OR y < 0 OR z < 0) AND (z >= 12 OR y < 0 OR z < 0) AND (z <= 12 OR y < 0 OR z > 2y) AND (z >= 12 OR y < 0 OR z > 2y) AND (z <= 12 OR y >= 0 OR z < 0) AND (z >= 12 OR y >= 0 OR z < 0) AND (z <= 12 OR y >= 0 OR z > 2y) AND (z >= 12 OR y >= 0 OR z > 2y)

Our SAT solver will then attempt to find a contradiction in our set of booleans, by randomly setting booleans to true / false, and seeing if the rest of the equation holds.

It's different from a fuzzer, as a fuzzer tries inputs for y. Whereas a SAT Solver will try different inputs for the booleans.

Solidity SMT Checker

The solidity SMT Checker attempts to do this conversion of code -> math itself based on your assert and require statements and then runs it through a SAT solver, and therefore is a form of symbolic execution.