Instead of executing a program on a set of sample inputs, Symbolic Execution use symbolic values for inputs which could mean a set of classes inputs. It indicate that we needn’t execute a program with a large number of normal test cases, but choose some test cases representatives.
Now, we give a simple example:
int i = read();
if (i>0) {
i = 0;
}
print("finish");
There is a important concept called “path condition” means if you want to go through the path, you should satisfy the condition.
In our example, first we assume read() return symbolic “X”, we could find that i = X. And we meet the IF statement, what should we do? we shall check IF statement “forkable” or not. if the statement is “forkable”, we fork execution into two “parallel” execution, if not, we just go single side. The two “parallel” execution have they own “path condition”: ( true && X > 0 ) and ( true && (!X > 0) ). (true) is the original path condition.
After we find out all path conditions, we use Constraint Solver to figure out some representative values for each path conditions and use these values to test program.
In our example, Constraint Solver could figure out X = 1 for ( true && X > 0 ) and X = -1 for ( true && (!X > 0) ). These test cases obviously cover our example program. we succeed!