See question. Is the SMT Checker in solidity a form of symbolic execution?
1 Answer
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.