The Symbolic Execution Debugger (SED) is a platform for interactive symbolic execution. Using KeY as symbolic execution engine, sequential Java programs specified with JML can be symbolically executed. In this evaluation the SED will be used to inspect proofs attempts. Interactive symbolic execution is not required.
The relevant knowledge for this evaluation about SED is explained in the following sections. Please read them carefully before you continue. If you are familiar with the SED, you can skip sections you know well.
Symbolic execution allows to explore all feasible execution paths of a program at once. This is achieved by using symbolic values in lieu of concrete values. Whenever the knowledge about a symbolic value is not enough to follow a single execution path, symbolic execution splits to cover all feasible execution paths. This results in a so called symbolic execution tree.
Consider for instance the following Java program.
Method equals
checks whether the given Number
instance has the same content
as the current one.
public class Number {
private int content;
/*@ requires true;
@ ensures true;
@ assignable \nothing;
@*/
public boolean equals(/*@ nullable @*/ Number n) {
if (content == n.content) {
return true;
}
else {
return false;
}
}
}
The resulting symbolic execution tree of method equals
is shown in the following figure.
The root is a start node () representing the program fragment to execute.
It also restricts the initial state according to the JML specification.
As we are interested in method
equals
, it is called next represented by a method call node ().
The if statement is supposed to split execution and thus represented as branch statement (
).
The conditions under which a branch is taken are shown as branch condition nodes (
).
In case that
n
is null
, the method returns with an uncaught NullPointerException
indicated by the exceptional method return node ().
Finally, this path terminates exceptionally shown by the exceptional termination node (
).
In case that
n
is not null
, a return statement is executed. As this statement is not supposed to split execution, a statement node () is used.
The method return nodes (
) indicate that a called method returns. Possible return values of non void methods are shown as part of the node label.
Finally, a termination node (
) indicate that an execution path terminates normally without an uncaught exception.
The blue rectangles in the figure below group related nodes like an if
statement or a method body.
A method call can be treated by inlining or by application of a method contract during symbolic execution.
Inlining of a method body as in the previous example is represented by a method call node () and later after execution of the method body by a method return (
) or exceptional method return node (
).
The following example explains the alternative to apply a method contract instead of inlining.
Method doubleValue
calls method doDoubleValue
which should be treated during symbolic execution by applying its contract.
The resulting symbolic execution tree contains a method contract node () showing the applied contract as first order formula in KeY syntax.
The optional child branch conditions indicate that execution is continued in case of normal (post) or exceptional (exceptional post) termination of the called method.
public class IntegerUtil {
public static int doubleValue(int x) throws Exception {
return doDoubleValue(x);
}
/*@ normal_behavior
@ requires x >= 0;
@ ensures \result == x + x;
@ also
@ exceptional_behavior
@ requires x < 0;
@ signals (Exception) true;
@*/
private static /*@ pure @*/ int doDoubleValue(int x) throws Exception;
}
A loop is always treated in this evaluation by applying the specified loop invariant.
Consider for instance the following example.
The loop invariant node () shows the specified loop invariant as first order formula in KeY syntax.
It also splits symbolic execution into two branches.
The Body Preserves Invariant branch represents an arbitrary loop iteration.
After execution of loop guard and loop body, the branch terminates indicated by the loop body termination node (
).
The Use Case branch continues execution after an arbitrary number of loop iterations after the loop.
public class LoopExample {
/*@ normal_behavior
@ requires x >= 0;
@ ensures \result == 0;
@*/
public static int decrease(int x) {
/*@ loop_invariant x >= 0;
@ decreasing x;
@ assignable x;
@*/
while (x > 0) {
x--;
}
return x;
}
}
Termination () and exceptional termination (
) nodes indicate by a red crossed icon if the postcondition (including assignable clause and uncaught exceptions) could not be proven to be correct.
A method contract (
) node is also marked by a red crossed icon if the precondition of the applied contract could not be proven to be correct.
Finally, a loop invariant (
) node is crossed out if the loop invariant could not be proven to hold initially and the loop body termination (
) node is crossed if the loop invariant (including decreasing and assignable clause) could not be proven to be preserved.
A symbolically executed method is correct iff
If a method could not be proven correct, possible reasons are:
The Symbolic Execution Debugger offers a new perspective named Symbolic Debug which offers everything related to symbolic execution:
Each node in the symbolic execution tree represents the state before a statement is executed. The state can be inspected after selection of the node of interest in view Variables. In contrast to a concrete execution, symbolic values are shown in column Value. Additional constraints are shown after selecting a variable in view Properties at tab Constraints.
A symbolic execution path is representative for possibly infinite concrete executions with different memory layouts. The SED allows to visualize all possible memory layouts by selecting context menu item Visualize Memory Layouts of a node.
This opens a new diagram editor in perspective State Visualization. The rectangle with rounded corners represents the current state which points to objects on the heap (rectangles). Lower compartments of objects show field variables with their symbolic values while the lower compartment of the current state shows local variables with their symbolic values. The red rectangles between arrows show the name of the represented variable/location.
The slider in the editor allows to switch between possible memory layouts while the radio buttons define if the current or the initial state before execution started is shown.
KeY tries to evaluate postconditions within a proof after symbolic execution has finished. Additionally, preconditions of applied method contracts and loop invariants are evaluated. Nodes which might be marked as unverified by a red cross (see 1.3 Proving by Symbolic Execution) provides a tab in the Properties view in which the during proof computed truth values of the formula to show are highlighted. The tab is named Postcondition on termination and exceptional termination nodes, Precondition on method call nodes and Loop Invariant on loop invariant and loop body termination nodes.
In case that the proof splits in order to evaluate the formula, for each leaf (goal) is a group composite shown named after the unique ID of the leaf.
In the example below, the proof does not split and thus only one group named Node 29 is available.
Each group shows on the left of the implication arrow ==>
the split condition and on the right the to be proven formula.
Formulas evaluated to true are colored in green, terms evaluated to false are colored in red and terms colored in yellow are never or not completely evaluated during prove.
In rare cases KeY splits the proof on a term which has nothing to do with the proven formula.
In such a case the related part in the split condition is not colored (black).
A leaf fulfills the formula to show, iff the left side of the implication arrow ==>
evaluates to false or iff the right side evaluates to true.
In the example below evaluates the left side to true, thus the only chance to fulfill the formula is to evaluate the right side also to true.
Let us inspect the terms of the conjunctions (&
) more carefully.
The term exc = null
evaluates to true which is what the specification (normal_behavior) says.
The terms PostconditionEvaluation.x = 42
and \forall ...
are not completely evaluated.
Additionally, the second &
is colored in red meaning that during prove this operator was evaluated into false (even if the result of its children is not completely evaluated).
This means the formula can not be evaluated into true and one of the orange parts (ensures and assignable clause) must be buggy.
An inspection of the termination state in view Variables shows that the value of x
is 4711
and not 42
as specified.
We found the bug.