12
Sep

Symbolic Execution Debugger (SED)


Welcome to the presentation of the Symbolic
Execution Debugger. We will present three examples highlighting
typical application scenarios of the tool. The first one is simple and designed to explain
symbolic execution and how the debugger
performs it. Symbolic execution means to execute a
program with symbolic values instead of
concrete values. This allows us to discover all feasible program
execution paths simultaneously. The debugger allows to start execution directly
at any method or even at a single statement. Because symbolic values are used, there is no
need to find input values, which bring execution
to the point of interest. All to be done is to select the element of
interest and to start debugging via context menu
item ‘Debug As, Symbolic Execution Debugger’. Switch next into the ‘Symbolic Debug’
perspective which provides all relevant views for
symbolic execution. Execution can be done stepwise or resumed
until a defined breakpoint is reached. Let’s do it stepwise and have a closer look on
how symbolic execution works. The root is always a start node representing the
program fragment to execute. We are interested in method equals, which we
call now by performing a ‘step into’. The next step is to execute the first statement. Before we do it, let us inspect the current
symbolic state shown in view ‘Variables’. Here, the Java this reference is named self and
has an instance field content. Both are assigned with symbolic values named
after them. At this point we know nothing about parameter
n. It can be null or a reference to an existing
object. If multiple values are possible, the tool shows
the condition under which a value is valid. In case that n points to an object, then there is
again the instance field content. The exception variable is used by the debugger
to identify if an execution path terminates
normally or with an uncaught exception. Now we continue symbolic execution with the if-
statement. We have not enough knowledge about the
symbolic state to follow a single path. Consequently, symbolic execution splits into
several branches to cover all feasible execution
paths. The result is a so called symbolic execution
tree. The conditions under which each path is taken
are shown as branch condition nodes. The right branch is taken, if n is null. In this case a NullPointerException is thrown
and execution terminates with this uncaught
exception. Otherwise the if-condition may evaluate either to
true or to false. For the else branch, when instance variable
content of self and n has different values, the
return statement is executed next. Now the end of method equals is reached and
false is returned as method result. Finally, execution terminates normally without a
thrown exception. The then branch is taken when instance variable
content of self and n has the same value. Rather than executing the then branch stepwise,
we click on ‘Resume’ to finish execution. Compared to the else branch, we can see that
true is returned instead of false. Additional details about the selected node are
shown in the ‘Properties’ view. For instance, the path condition restricts the
initial state to ensure that the current path is
taken. Here, n has to be not null and the content of self
and n has to be the same. This can also be seen in the symbolic state. n can’t be null anymore and both content fields
of n and self have the same value. But what about n and self? The path condition is fulfilled if both are different
objects with the same value, but also if both
point to the same object. Aliasing is a common source of bugs… …and the Symbolic Execution Debugger allows
to visualize all possible memory layouts of the
current state. Simply, click on ‘Visualize Memory Layouts’
and switch to the ‘State Visualization’
perspective. The opened editor shows a symbolic object
diagram similar to an UML object diagram. The root node represents a state. Its local variables point to objects on the heap. Here, both objects are different, but have the
same content. We can switch to an alternative memory layout
in which n and self point to the same object. No other non-isomorphic memory layouts exist. It is also possible to inspect the initial memory
layout before execution started. Here it is the same, because nothing was
changed in the current execution path. Before we continue with the next example, let
us clean up the debugging session. First we close the editor and second we
terminate and remove it. We will use the Symbolic Execution Debugger
now in a more realistic example to locate the
origin of a bug. Imagine a large application and a user reports
that she experienced a StackOverflowError. It seems that method sort calls itself recursively
until the stack is full. Using a traditional debugger, we would have to
find input values to reproduce the failure first;… …as already done in order to demonstrate the
error. In the traditional setting, we could set a
breakpoint at the beginning of method sort to
suspend execution. From this point on, we would execute the
method stepwise to comprehend the situation. A time consuming and tedious task. Using the Symbolic Execution Debugger, we
can do better because execution can start
directly at method sort. Also in the symbolic setting we control
execution until we find something unexpected. First method sort is called. The first and only statement calls then the
helper method. This requires to access numbers.length which
splits execution into two branches as array may
be null. But in an actual program run the
NullPointerException is not possible. This is ensured by assert statements of the
constructor. Symbolic execution starts in an arbitrary state
and this kind of knowledge is not available by
default. But we can add it as precondition to the debug
configuration. Just specify that numbers is not null and that
numbers.length is greater or equal to one. To use the new precondition, we need to restart
our debugging session. And we start over again as before. First sort is called… …which invokes the helper method. This time execution does not split anymore… …and the if statement will be executed next. Surprisingly, symbolic execution does not split. This means that the then branch is always
executed. Missing expected splits or unexpected splits
may indicate a bug in the source code. Further inspection shows that the if guard is
indeed erroneous. So let us correct it. It should be a lesser-than comparison. After terminating the debugging sessions, … …we can execute the application again and see
that the bug is gone. In the last example we use the Symbolic
Execution Debugger to review our code… …and to demonstrate how specifications can be
used during symbolic execution. Method indexOf returns the first array index
accepted by the filter. Filter is an interface for which no concrete
implementation is available. The behavior of a program is specified using the
Java Modeling Language (JML). The method contract specifies that the method
can be called in any state and ensures that no
exception will be thrown. Observe that the method contract of indexOf is
incomplete, but still sufficient for debugging. Its method contract requires only that the
invariant of parameter filter is satisfied. Loops are unrolled by default during symbolic
execution. Loop invariants can be applied instead to
guarantee a finite symbolic execution tree… …even if the number of loop iteration has no
fixed bound. A loop invariant is a formula, which has to be
preserved by any loop iteration. To find a suitable loop invariant can be a difficult
task. However, for debugging loop invariants can be
much weaker than required for verification. Before we start debugging, we modify the debug
configuration to use the method contract. The method’s precondition restricts the initial
state, while the fulfillment of the postcondition is
checked in each termination node. So let’s start. If we would resume execution, the loop would be
unrolled once and execution would stop
because no Filter implementation is available. To avoid this, we configure the symbolic
execution engine to apply contracts and loop
invariants instead. Resume execution results in a finite symbolic
execution tree, which covers the complete
program behavior. Let’s have a closer look at the symbolic
execution tree. The loop is dealt with by applying its loop
invariant. This splits execution into two branches. The ‘Body Preserves Invariant’ branch
represents an arbitrary loop iteration. Improving the layout and readability of the
conditions is future work. However, we can see by the red crossed
termination icon that the loop invariant is not
preserved. The index variable i is not increased when an
element is accepted. This breaks the termination condition of the loop
invariant. The debugger like interface allows to easily
comprehend specified loop invariants… … and in particular to understand why they
might not be satisfied by a program. A huge help when verifying programs. At last, the ‘Use Case’ branch continues
execution after the loop. Although the loop invariant is not preserved, we
can spot another problem. Inspecting the return nodes, we can see that the
loop counter variable i is returned instead of the
found index. Did you get interested in the Symbolic
Execution Debugger? If yes, try it out. The debugger is available as an Eclipse plug-in
and compatible with Eclipse 3.7 Indigo or newer. The required update sites and additional
information about the tool are available at
www.key-project.org. Thank you for watching the presentation of the
Symbolic Execution Debugger.

Tags: , , , ,

One Comment

Leave a Reply

Your email address will not be published. Required fields are marked *