.. _symexec_chapter:

Symbolic Execution
=================================

Grackle executes program using symbolic execution.  Symbolic execution, like
ordinary execution, executes the program one step at a time, but with two
differences: (1) As discussed in the previous section, the variables range over
symbolic values rather than ordinary expressions; and
(2) when conditional branches are encountered, such as ``if`` statements or
``while`` loops, the simulator will need to consider multiple execution paths
if the branch may be either true or false.

As an example, consider the code below:

::

    x      = symbolic('x', 'real');
    target = symbolic('target', 'real');
    diff = 3;

    if (x > target)
      y = x - diff;
    else
      y = x + diff;
    end

    [r,c] = check_sat(abs(x-target) > diff & abs(y-target) > abs(x-target))

In this case, the condition ``x > target`` can be either true or false depending
on the values assigned to ``x`` and ``target``.  Accordingly, Grackle will
execute the script up to the ``if`` statement, and then execute both execution
paths over the state prior to the ``if`` statement.  When both paths reach the
end of their respective paths in the ``if`` statement, Grackle will **merge**
the two execution paths into a single state.  In this case, after the merge, the
assignment will map ``y`` to the expression *if (x > target) (x - 3) (x + 3)*, which
denotes the value *x - 3* if *x > target* and *x + 3* otherwise.

The post-dominator based merging stategy is particularly important for programs
with loops.  For example, in the following program, Grackle will execute
`20` paths without merging, but would need to consider 2:sup:`10` execution
paths if it did not do path merging.

::

    p = symbolic('x', 10, 1, 'logical');
    true_count = 0;
    false_count = 0;
    for i = 1:10
      if (p(i))
        true_count = true_count + 1;
      else
        false_count = false_count + 1;
      end
    end

In this case, the condition ``p(i)`` is indeterminate, and so each time it is
encountered, two execution paths are formed.  Due to our use of path-based
merging however, a single execution path is formed after execution completes.

Internally, our path-based merging strategy operates by translating the source
program into a **control flow graph**.  For each branch, Grackle computes the
**immediate post-dominator** of that branch, and uses that location as the merge
point.  This approach allows Grackle to easily deal with a variety of source
language constructs, including not just ``if`` statements, but also ``while``
and ``for`` loops, even in the presence of ``continue`` and ``break``
statements.  In this encoding each loop will effectively introduce two potential
merge points: the first is at the entry of the loop, and used when ``continue``
is called or the loop body terminates.  The second is at the loop exit, and is
targetted by ``break``.

One significant limitation of our approach is that the symbolic simulator does
not effectively deal with loops that may execute an unbounded number of times.
In this case, the post-dominator-based merging strategy will get stuck executing
the loop body.  To deal with this and other programs where merging is inappropriate,
we have introduced a built-in function :ref:`symbolic_fork_fun` which allows one
to create a path that bypasses merging.