Symbolic execution: Difference between revisions

Revision as of 19:03, 23 September 2022

Revision as of 07:16, 3 November 2022

Line 21:

During a normal execution ("concrete" execution), the program would read a concrete input value (e.g., 5) and assign it to <code>y</code>. Execution would then proceed with the multiplication and the conditional branch, which would evaluate to false and print <code>OK</code>.

During symbolic execution, the program reads a symbolic value (e.g., <code>λ</code>) and assigns it to <code>y</code>. The program would then proceed with the multiplication and assign <code>λ * 2</code> to <code>z</code>. When reaching the <code>if</code> statement, it would evaluate <code>λ * 2 == 12</code>. At this point of the program, <code>λ</code> could take any value, and symbolic execution can therefore proceed along both branches, by "forking" two paths. Each path gets assigned a copy of the program state at the branch instruction as well as a path constraint. In this example, the path constraint is <code>λ * 2 == 12</code> for the <code>thenif</code> branch and <code>λ * 2 != 12</code> for the <code>else</code> branch. Both paths can be symbolically executed independently. When paths terminate (e.g., as a result of executing <code>fail()</code> or simply exiting), symbolic execution computes a concrete value for <code>λ</code> by solving the accumulated path constraints on each path. These concrete values can be thought of as concrete test cases that can, e.g., help developers reproduce bugs. In this example, the [[constraint solver]] would determine that in order to reach the <code>fail()</code> statement, <code>λ</code> would need to equal 6.

==Limitations==