de.uka.ilkd.key.symbolic_execution

Class SymbolicExecutionTreeBuilder

java.lang.Object

de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder

public class SymbolicExecutionTreeBuilder
extends java.lang.Object

Instances of this class are used to extract the symbolic execution tree from a normal KeY's proof tree. The requirement is that the proof contains a predicate which is not evaluable to filter invalid execution tree paths. The easiest way to achieve this is to use a FunctionalOperationContractPO (addUninterpretedPredicate = true) instance as proof obligation to instantiate a Proof from.

A symbolic execution tree consists of IExecutionNodes which represents the executed statements and other Java constructs. The root of a symbolic execution tree is an IExecutionStart which is available via getProof().

Some assumptions about how Sequents in the proof tree looks like are required to extract the symbolic execution tree. To make sure that they hold (otherwise exceptions are thrown) it is required to execute the SymbolicExecutionStrategy in KeY's auto mode and not to apply rules manually or to use other strategies.

The symbolic execution tree is not updated automatically when KeY's proof tree has changed. The update must be started manually via analyse(). In this case the proof tree will be analyzed and the execution tree model created or updated if it already exist.

Proof trees and also symbolic execution trees are very large even in small programs. For this reason it is not possible to iterate over the tree via recursive method calls. Instead, an instance of ExecutionNodePreorderIterator should be used to iterate over a symbolic execution tree.

The following snippet shows the basic usage of this class to extract an symbolic execution tree:

 
 Proof proof; // Create proof with proof obligation FunctionalOperationContractPO and set addUninterpretedPredicate to true
 // Start KeY's auto mode with SymbolicExecutionStrategy to do the proof
 SymbolicExecutionTreeBuilder builder = new SymbolicExecutionTreeBuilder(proof);
 builder.analyse(); // Create initial symbolic execution tree
 // Iterate over symbolic execution tree and print it into the console
 ExecutionNodePreorderIterator iter = new ExecutionNodePreorderIterator(builder.getStartNode);
 while (iter.hasNext() {
    IExecutionNode next = iter.next();
    System.out.println(next.getName());
 }
 // Continue proof by starting KeY's auto mode again with SymbolicExecutionStrategy
 builder.analyse(); // Create initial symbolic execution tree
 // Iterate again over the symbolic execution tree
 iter = new ExecutionNodePreorderIterator(builder.getStartNode);
 // ...
 

Author:

Martin Hentschel

See Also:

AbstractOperationPO.isAddUninterpretedPredicate(), IExecutionNode, IExecutionStart, SymbolicExecutionStrategy, ExecutionNodePreorderIterator

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	SymbolicExecutionTreeBuilder.AnalyzerProofVisitor This ProofVisitor is used to transfer the proof tree in KeY into IExecutionNodes which forms the symbolic execution tree.
protected static class	SymbolicExecutionTreeBuilder.JavaPair Utility class to group a call stack size with an ImmutableList of SourceElement with the elements of interest.
private static class	SymbolicExecutionTreeBuilder.MethodFrameCounterJavaASTVisitor Utility class used in initNewLoopBodyMethodCallStack(Node) to compute the number of available MethodFrames.
static class	SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions Instances of this class are returned by analyse() to inform about newly completed blocks and returned methods.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<java.lang.Integer,java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>>>	afterBlockMap Contains the possible statements after a code block of interest for each tracked symbolic execution modality.
private java.util.Deque<java.util.Map.Entry<AbstractExecutionNode<?>,java.util.List<ExecutionBranchCondition>>>	branchConditionsStack Branch conditions (ExecutionBranchCondition) are only applied to the execution tree model if they have at least one child.
private IProgramVariable	exceptionVariable Contains the exception variable which is used to check if the executed program in proof terminates normally.
private boolean	isUninterpretedPredicateUsed true infeasible paths are closed, false infeasible may be open may be closed.
private java.util.Map<Node,ExecutionBranchCondition>	keyNodeBranchConditionMapping Maps a branch condition of a Node of KeY's proof tree to his execution tree model representation (IExecutionBranchCondition) if it is available.
private java.util.Map<Node,ExecutionLoopCondition>	keyNodeLoopConditionMapping Maps a loop condition of a Node of KeY's proof tree to his execution tree model representation (IExecutionLoopCondition) if it is available.
private java.util.Map<Node,AbstractExecutionNode<?>>	keyNodeMapping Maps a Node of KeY's proof tree to his execution tree model representation if it is available.
private java.util.Map<java.lang.Integer,java.util.Map<Node,ImmutableList<Node>>>	methodCallStackMap Contains the method call stacks for each tracked symbolic execution modality.
private java.util.Map<java.lang.Integer,java.util.Set<Node>>	methodReturnsToIgnoreMap Contains Nodes of method calls which return statements should be ignored.
private java.util.Map<Node,java.util.List<AbstractExecutionNode<?>>>	multipleExecutionNodes In case a Node is represented by multiple AbstractExecutionNodes, this map maps the Node to all its representations.
private Proof	proof The Proof from which the symbolic execution tree is extracted.
private TreeSettings	settings The TreeSettings to use.
private ExecutionStart	startNode The start node of the symbolic execution tree.

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionTreeBuilder(Proof proof, boolean mergeBranchConditions, boolean useUnicode, boolean usePrettyPrinting, boolean variablesAreOnlyComputedFromUpdates, boolean simplifyConditions) Constructor.

Method Summary

Modifier and Type	Method and Description
protected void	addChild(AbstractExecutionNode<?> parent, AbstractExecutionNode<?> child) Adds the child to the parent.
protected AbstractExecutionNode<?>	addNodeToTreeAndUpdateParent(Node node, AbstractExecutionNode<?> parentToAddTo, AbstractExecutionNode<?> executionNode) Adds the new created AbstractExecutionNode to the symbolic execution tree if available and returns the new parent for future detected nodes.
protected void	addToBlockMap(Node node, AbstractExecutionBlockStartNode<?> blockStartNode) Adds the given AbstractExecutionNode add reason for a new block to the block maps.
protected void	addToBlockMap(Node node, AbstractExecutionBlockStartNode<?> blockStartNode, int stackSize, SourceElement... sourceElements) Adds the given AbstractExecutionNode add reason for a new block to the block maps.
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions	analyse() This method must be called programmatically to update the symbolic execution tree.
protected AbstractExecutionNode<?>	analyzeNode(Node node, AbstractExecutionNode<?> parentToAddTo, SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions) Analyzes the given Proof and his contained proof tree by filling the start node getStartNode() with IExecutionNodes which are instantiated if a Node in KeY's proof tree applies a rule of symbolic execution.
private boolean	checkBlockPossibility(Node node, int expectedStackSize, SourceElement... expectedSourceElements) Checks if it possible that the current Node opens a block.
protected IExecutionNode<?>[]	createCallStack(Node node) Computes the method call stack of the given Node.
protected AbstractExecutionNode<?>	createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent, Node node, SourceElement statement) Creates a new execution tree model representation (IExecutionNode) if possible for the given Node in KeY's proof tree.
protected AbstractExecutionMethodReturn<?>	createMehtodReturn(AbstractExecutionNode<?> parent, Node node, SourceElement statement, SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions) Creates an method return node.
static java.util.Properties	createPoPropertiesToForce() Returns the minimal required PO Properties to support symbolic execution tree extraction in a SymbolicExecutionJavaProfile.
void	dispose() Frees all resources.
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>	findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps, Node node) Searches the relevant after block Map in the given once for the given Node.
protected Node	findMethodCallNode(Node currentNode, RuleApp ruleApp) Finds the Node in the proof tree of KeY which has called the method that is now executed or returned in the Node.
protected ImmutableList<Node>	findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack, Node node)
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>>	getAfterBlockMaps(int id) Returns the after block map used for the given ID.
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>>	getAfterBlockMaps(SymbolicExecutionTermLabel label) Returns the after block map.
IExecutionNode<?>	getBestExecutionNode(Node proofNode) Returns the best matching IExecutionNode for the given proof Node in the parent hierarchy.
IExecutionNode<?>	getExecutionNode(Node proofNode) Searches the IExecutionNode which represents the given Node of KeY's proof tree.
protected java.util.Map<Node,ImmutableList<Node>>	getMethodCallStack(int id) Returns the method call stack used for the given ID.
protected java.util.Map<Node,ImmutableList<Node>>	getMethodCallStack(RuleApp ruleApp) Returns the method call stack.
protected java.util.Map<Node,ImmutableList<Node>>	getMethodCallStack(SymbolicExecutionTermLabel label) Returns the method call stack.
protected java.util.Set<Node>	getMethodReturnsToIgnore(int id) Returns the method Nodes of method calls for which its return should be ignored.
protected java.util.Set<Node>	getMethodReturnsToIgnore(RuleApp ruleApp) Returns the method Nodes of method calls for which its return should be ignored.
protected java.util.Set<Node>	getMethodReturnsToIgnore(SymbolicExecutionTermLabel label) Returns the method Nodes of method calls for which its return should be ignored.
Proof	getProof() Returns the Proof from which the symbolic execution tree is extracted.
IExecutionStart	getStartNode() Returns the start node of the symbolic execution tree.
protected boolean	hasBranchCondition(Node node) Checks if the given Node has a branch condition.
protected void	initMethodCallStack(Node root, Services services) This method initializes #methodCallStack in case that the initial Sequent contains MethodFrames in its modality.
protected void	initNewLoopBodyMethodCallStack(Node node) This method initializes the method call stack of loop body modalities with the values from the original call stack.
protected void	initNewMethodCallStack(Node currentNode, PosInOccurrence childPIO) Initializes a new method call stack.
protected void	initNewValidiityMethodCallStack(Node node) This method initializes the method call stack of validity modalities with the values from the original call stack.
protected boolean	isAfterBlockReached(int currentStackSize, MethodFrame currentInnerMostMethodFrame, SourceElement currentActiveStatement, int expectedStackSize, java.util.Iterator<SourceElement> expectedStatementsIterator) Checks if the after block condition is fulfilled.
protected boolean	isAfterBlockReached(int currentStackSize, MethodFrame currentInnerMostMethodFrame, SourceElement currentActiveStatement, SymbolicExecutionTreeBuilder.JavaPair expectedPair) Checks if the after block condition is fulfilled.
protected boolean	isContained(ImmutableList<IExecutionNode<?>> list, Node node) Checks if one of the give IExecutionNodes represents the given Node.
protected boolean	isInImplicitMethod(Node node) Checks if the given Node handles something in an implicit method.
protected boolean	isNotInImplicitMethod(Node node) Checks if the given Node is not in an implicit method.
boolean	isUninterpretedPredicateUsed() Checks if the uninterpreted predicate is available or not.
java.util.Set<AbstractExecutionNode<?>>	prune(Node node) Prunes the symbolic execution tree at the first IExecutionNode in the parent hierarchy of the given Node (including the Node itself).
protected IExecutionBranchCondition	searchDirectParentBodyPreservesInvariantBranchCondition(IExecutionNode<?> current) Searches the direct parent IExecutionBranchCondition representing the 'Body Preserves Invariant' branch.
protected Node	searchPreviousSymbolicExecutionNode(Node node) Searches the first node in the parent hierarchy (including the given node) which executes a statement.
protected boolean	shouldPrune(Node node)
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>	updateAfterBlockMap(Node node, RuleApp ruleApp) Updates the after block maps when a symbolic execution tree node is detected.
protected void	updateCallStack(Node node, SourceElement statement) Updates the call stack (#methodCallStack) if the given Node in KeY's proof tree is a method call.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

proof

private Proof proof

The Proof from which the symbolic execution tree is extracted.

startNode

private ExecutionStart startNode

The start node of the symbolic execution tree.

keyNodeMapping

private java.util.Map<Node,AbstractExecutionNode<?>> keyNodeMapping

Maps a Node of KeY's proof tree to his execution tree model representation if it is available.

In case that the Node is represented by multiple AbstractExecutionNodes, e.g. a return statement and a method return, the last node is returned.

multipleExecutionNodes

private java.util.Map<Node,java.util.List<AbstractExecutionNode<?>>> multipleExecutionNodes

In case a Node is represented by multiple AbstractExecutionNodes, this map maps the Node to all its representations.

keyNodeLoopConditionMapping

private java.util.Map<Node,ExecutionLoopCondition> keyNodeLoopConditionMapping

Maps a loop condition of a Node of KeY's proof tree to his execution tree model representation (IExecutionLoopCondition) if it is available.

keyNodeBranchConditionMapping

private java.util.Map<Node,ExecutionBranchCondition> keyNodeBranchConditionMapping

Maps a branch condition of a Node of KeY's proof tree to his execution tree model representation (IExecutionBranchCondition) if it is available.

methodCallStackMap

private java.util.Map<java.lang.Integer,java.util.Map<Node,ImmutableList<Node>>> methodCallStackMap

Contains the method call stacks for each tracked symbolic execution modality. As key is SymbolicExecutionTermLabel.getId() used.

afterBlockMap

private java.util.Map<java.lang.Integer,java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>>> afterBlockMap

Contains the possible statements after a code block of interest for each tracked symbolic execution modality. As key is SymbolicExecutionTermLabel.getId() used.

methodReturnsToIgnoreMap

private java.util.Map<java.lang.Integer,java.util.Set<Node>> methodReturnsToIgnoreMap

Contains Nodes of method calls which return statements should be ignored. As key is SymbolicExecutionTermLabel.getId() used.

exceptionVariable

private IProgramVariable exceptionVariable

Contains the exception variable which is used to check if the executed program in proof terminates normally.

settings

private final TreeSettings settings

The TreeSettings to use.

isUninterpretedPredicateUsed

private final boolean isUninterpretedPredicateUsed

true infeasible paths are closed, false infeasible may be open may be closed.

branchConditionsStack

private final java.util.Deque<java.util.Map.Entry<AbstractExecutionNode<?>,java.util.List<ExecutionBranchCondition>>> branchConditionsStack

Branch conditions (ExecutionBranchCondition) are only applied to the execution tree model if they have at least one child. For this reason they are added to the model in #completeTree() after the whole proof tree of KeY was analyzed via #visit(Proof, Node). The adding of ExecutionBranchCondition to the model must be done from leaf nodes to the root, but in correct child order. This Deque forms the order in that the ExecutionBranchCondition must be applied. The contained List makes sure that the children are applied in the same order as they occur in KeY's proof tree.

Constructor Detail

SymbolicExecutionTreeBuilder

public SymbolicExecutionTreeBuilder(Proof proof,
                                    boolean mergeBranchConditions,
                                    boolean useUnicode,
                                    boolean usePrettyPrinting,
                                    boolean variablesAreOnlyComputedFromUpdates,
                                    boolean simplifyConditions)

Constructor.

Parameters:

proof - The Proof to extract the symbolic execution tree from.

mergeBranchConditions - true merge branch conditions which means that a branch condition never contains another branch condition or false allow that branch conditions contains branch conditions.

useUnicode - true use unicode characters, false do not use unicode characters.

usePrettyPrinting - true use pretty printing, false do not use pretty printing.

variablesAreOnlyComputedFromUpdates - true IExecutionVariable are only computed from updates, false IExecutionVariables are computed according to the type structure of the visible memory.

simplifyConditions - true simplify conditions, false do not simplify conditions.

Method Detail

initMethodCallStack

protected void initMethodCallStack(Node root,
                                   Services services)

This method initializes #methodCallStack in case that the initial Sequent contains MethodFrames in its modality.

This is required because if a block of statements is executed instead of a method the initial Sequent contains also a MethodFrame. This initial MethodFrame is required to simulate an execution context which is required to access class members.

Parameters:

root - The root Node with the initial Sequent.

services - The Services to use.

getMethodReturnsToIgnore

protected java.util.Set<Node> getMethodReturnsToIgnore(RuleApp ruleApp)

Returns the method Nodes of method calls for which its return should be ignored. If not already available an empty method Set is created.

Parameters:

ruleApp - The RuleApp which modifies a modality Term with a SymbolicExecutionTermLabel.

Returns:

The Set of Nodes to ignore its return.

getMethodReturnsToIgnore

protected java.util.Set<Node> getMethodReturnsToIgnore(SymbolicExecutionTermLabel label)

Returns the method Nodes of method calls for which its return should be ignored. If not already available an empty method Set is created.

Parameters:

label - The SymbolicExecutionTermLabel which provides the ID.

Returns:

The Set of Nodes to ignore its return.

getMethodReturnsToIgnore

protected java.util.Set<Node> getMethodReturnsToIgnore(int id)

Returns the method Nodes of method calls for which its return should be ignored. If not already available an empty method Set is created.

Parameters:

id - The ID.

Returns:

The Set of Nodes to ignore its return.

getMethodCallStack

protected java.util.Map<Node,ImmutableList<Node>> getMethodCallStack(RuleApp ruleApp)

Returns the method call stack. If not already available an empty method call stack is created.

Parameters:

ruleApp - The RuleApp which modifies a modality Term with a SymbolicExecutionTermLabel.

Returns:

The method call stack of the ID of the modified modality Term with a SymbolicExecutionTermLabel.

getMethodCallStack

protected java.util.Map<Node,ImmutableList<Node>> getMethodCallStack(SymbolicExecutionTermLabel label)

Returns the method call stack. If not already available an empty method call stack is created.

Parameters:

label - The SymbolicExecutionTermLabel which provides the ID.

Returns:

The method call stack of the ID of the given SymbolicExecutionTermLabel.

getMethodCallStack

protected java.util.Map<Node,ImmutableList<Node>> getMethodCallStack(int id)

Returns the method call stack used for the given ID. If not already available an empty method call stack is created.

Parameters:

id - The ID.

Returns:

The method call stack of the given ID.

dispose

public void dispose()

Frees all resources. If this method is called it is no longer possible to use the SymbolicExecutionTreeBuilder instance! Later usage is not checked and punished with exceptions.

getProof

public Proof getProof()

Returns the Proof from which the symbolic execution tree is extracted.

Returns:

The Proof from which the symbolic execution tree is extracted.

getStartNode

public IExecutionStart getStartNode()

Returns the start node of the symbolic execution tree.

Returns:

The start node of the symbolic execution tree.

analyse

public SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions analyse()

This method must be called programmatically to update the symbolic execution tree. The first call will create the initial tree and further call will update the existing tree.

Returns:

The detected SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions during symbolic execution.

prune

public java.util.Set<AbstractExecutionNode<?>> prune(Node node)

Prunes the symbolic execution tree at the first IExecutionNode in the parent hierarchy of the given Node (including the Node itself).

Parameters:

node - Node to be pruned.

Returns:

The AbstractExecutionNode's which where deleted.

analyzeNode

protected AbstractExecutionNode<?> analyzeNode(Node node,
                                               AbstractExecutionNode<?> parentToAddTo,
                                               SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)

Analyzes the given Proof and his contained proof tree by filling the start node getStartNode() with IExecutionNodes which are instantiated if a Node in KeY's proof tree applies a rule of symbolic execution.

Attention : A correct pruning requires at the moment that the Taclet Option "runtimeExceptions" is set to "runtimeExceptions:allow". Alternatively it is required to modify rule assignment_to_reference_array_component in file javaRules.key by uncommenting \add (!(#v=null) & lt(#se, length(#v)) & geq(#se,0) & arrayStoreValid(#v, #se0)==>).

Parameters:

node - The Node to analyze.

parentToAddTo - The parent IExecutionNode to add the created execution tree model representation (IExecutionNode) of the given Node to.

completions - The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions to update.

Returns:

The IExecutionNode to which children of the current Node should be added. If no execution tree model representation was created the return value is identical to the given one (parentToAddTo).

searchDirectParentBodyPreservesInvariantBranchCondition

protected IExecutionBranchCondition searchDirectParentBodyPreservesInvariantBranchCondition(IExecutionNode<?> current)

Searches the direct parent IExecutionBranchCondition representing the 'Body Preserves Invariant' branch.

Parameters:

current - The IExecutionNode to check its parent IExecutionBranchConditions.

Returns:

The found IExecutionBranchCondition or null if not available.

shouldPrune

protected boolean shouldPrune(Node node)

addNodeToTreeAndUpdateParent

protected AbstractExecutionNode<?> addNodeToTreeAndUpdateParent(Node node,
                                                                AbstractExecutionNode<?> parentToAddTo,
                                                                AbstractExecutionNode<?> executionNode)

Adds the new created AbstractExecutionNode to the symbolic execution tree if available and returns the new parent for future detected nodes.

Parameters:

node - The Node.

parentToAddTo - The parent AbstractExecutionNode.

executionNode - The new child AbstractExecutionNode.

Returns:

The new parent AbstractExecutionNode.

updateCallStack

protected void updateCallStack(Node node,
                               SourceElement statement)

Updates the call stack (#methodCallStack) if the given Node in KeY's proof tree is a method call.

Parameters:

node - The current Node.

statement - The statement (SourceElement).

findMethodCallStack

protected ImmutableList<Node> findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
                                                  Node node)

createExecutionTreeModelRepresentation

protected AbstractExecutionNode<?> createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent,
                                                                          Node node,
                                                                          SourceElement statement)

Creates a new execution tree model representation (IExecutionNode) if possible for the given Node in KeY's proof tree.

Parameters:

parent - The parent IExecutionNode.

node - The Node in the proof tree of KeY.

statement - The actual statement (SourceElement).

Returns:

The created IExecutionNode or null if the Node should be ignored in the symbolic execution tree.

addToBlockMap

protected void addToBlockMap(Node node,
                             AbstractExecutionBlockStartNode<?> blockStartNode)

Adds the given AbstractExecutionNode add reason for a new block to the block maps.

Parameters:

node - The current Node.

blockStartNode - The AbstractExecutionNode to add.

addToBlockMap

protected void addToBlockMap(Node node,
                             AbstractExecutionBlockStartNode<?> blockStartNode,
                             int stackSize,
                             SourceElement... sourceElements)

Adds the given AbstractExecutionNode add reason for a new block to the block maps.

Parameters:

node - The current Node.

blockStartNode - The AbstractExecutionNode to add.

secondPair - The next element to end at.

checkBlockPossibility

private boolean checkBlockPossibility(Node node,
                                      int expectedStackSize,
                                      SourceElement... expectedSourceElements)

Checks if it possible that the current Node opens a block.

Parameters:

node - The current Node.

expectedStackSize - The expected stack size.

expectedSourceElements - The expected after block SourceElements.

Returns:

false A block is definitively not possible, true a block is or might be possible.

findAfterBlockMap

protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
                                                                                                                  Node node)

Searches the relevant after block Map in the given once for the given Node.

Parameters:

afterBlockMaps - The available after sblock Maps.

node - The Node for which the block Map is requested.

Returns:

The found after block Map or null if not available.

getAfterBlockMaps

protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> getAfterBlockMaps(SymbolicExecutionTermLabel label)

Returns the after block map. If not already available an empty block map is created.

Parameters:

label - The SymbolicExecutionTermLabel which provides the ID.

Returns:

The after block map of the ID of the given SymbolicExecutionTermLabel.

getAfterBlockMaps

protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> getAfterBlockMaps(int id)

Returns the after block map used for the given ID. If not already available an empty block map is created.

Parameters:

id - The ID.

Returns:

The after block map of the given ID.

updateAfterBlockMap

protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> updateAfterBlockMap(Node node,
                                                                                                                    RuleApp ruleApp)

Updates the after block maps when a symbolic execution tree node is detected.

Parameters:

node - The Node which is a symbolic execution tree node.

ruleApp - The RuleApp to consider.

Returns:

The now completed blocks.

isContained

protected boolean isContained(ImmutableList<IExecutionNode<?>> list,
                              Node node)

Checks if one of the give IExecutionNodes represents the given Node.

Parameters:

list - The IExecutionNodes to check.

node - The Node to check for.

Returns:

true is contained, false is not contained.

isAfterBlockReached

protected boolean isAfterBlockReached(int currentStackSize,
                                      MethodFrame currentInnerMostMethodFrame,
                                      SourceElement currentActiveStatement,
                                      SymbolicExecutionTreeBuilder.JavaPair expectedPair)

Checks if the after block condition is fulfilled.

Parameters:

currentStackSize - The current stack size.

currentInnerMostMethodFrame - The current inner most MethodFrame.

currentActiveStatement - The current active statement.

expectedPair - The SymbolicExecutionTreeBuilder.JavaPair specifying the after block statements.

Returns:

true after block is reached, false after block is not reached.

isAfterBlockReached

protected boolean isAfterBlockReached(int currentStackSize,
                                      MethodFrame currentInnerMostMethodFrame,
                                      SourceElement currentActiveStatement,
                                      int expectedStackSize,
                                      java.util.Iterator<SourceElement> expectedStatementsIterator)

Checks if the after block condition is fulfilled.

Parameters:

currentStackSize - The current stack size.

currentInnerMostMethodFrame - The current inner most MethodFrame.

currentActiveStatement - The current active statement.

expectedStackSize - The expected stack size.

expectedStatementsIterator - An Iterator with the expected after block statements.

Returns:

true after block is reached, false after block is not reached.

createMehtodReturn

protected AbstractExecutionMethodReturn<?> createMehtodReturn(AbstractExecutionNode<?> parent,
                                                              Node node,
                                                              SourceElement statement,
                                                              SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)

Creates an method return node.

Parameters:

parent - The parent AbstractExecutionNode.

node - The Node which represents a method return.

statement - The currently active SourceElement.

completions - The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions to update.

Returns:

The created AbstractExecutionMethodReturn.

isNotInImplicitMethod

protected boolean isNotInImplicitMethod(Node node)

Checks if the given Node is not in an implicit method.

Parameters:

node - The Node to check.

Returns:

true is not implicit, false is implicit

initNewLoopBodyMethodCallStack

protected void initNewLoopBodyMethodCallStack(Node node)

This method initializes the method call stack of loop body modalities with the values from the original call stack. For each MethodFrame in the new modality is its method call Node added to the new method call stack.

Parameters:

node - The Node on which the loop invariant rule is applied.

initNewValidiityMethodCallStack

protected void initNewValidiityMethodCallStack(Node node)

This method initializes the method call stack of validity modalities with the values from the original call stack. For each MethodFrame in the new modality is its method call Node added to the new method call stack.

Parameters:

node - The Node on which the block contract rule is applied.

initNewMethodCallStack

protected void initNewMethodCallStack(Node currentNode,
                                      PosInOccurrence childPIO)

Initializes a new method call stack.

Parameters:

currentNode - The current Node.

childPIO - The PosInOccurrence where the modality has a new symbolic execution label counter.

isUninterpretedPredicateUsed

public boolean isUninterpretedPredicateUsed()

Checks if the uninterpreted predicate is available or not.

Returns:

true uninterpreted predicate is available, false otherwise.

createCallStack

protected IExecutionNode<?>[] createCallStack(Node node)

Computes the method call stack of the given Node.

Parameters:

node - The Node.

Returns:

The computed method call stack.

findMethodCallNode

protected Node findMethodCallNode(Node currentNode,
                                  RuleApp ruleApp)

Finds the Node in the proof tree of KeY which has called the method that is now executed or returned in the Node.

Parameters:

currentNode - The Node for that the method call Node is needed.

Returns:

The found call Node or null if no one was found.

isInImplicitMethod

protected boolean isInImplicitMethod(Node node)

Checks if the given Node handles something in an implicit method.

Parameters:

node - The Node to check.

Returns:

true is in implicit method, false is not in implicit method.

hasBranchCondition

protected boolean hasBranchCondition(Node node)

Checks if the given Node has a branch condition.

Parameters:

node - The Node to check.

Returns:

true has branch condition, false has no branch condition.

searchPreviousSymbolicExecutionNode

protected Node searchPreviousSymbolicExecutionNode(Node node)

Searches the first node in the parent hierarchy (including the given node) which executes a statement.

Parameters:

node - The Node to start search in.

Returns:

The found Node with the symbolic statement or null if no one was found.

addChild

protected void addChild(AbstractExecutionNode<?> parent,
                        AbstractExecutionNode<?> child)

Adds the child to the parent.

Parameters:

parent - The parent to add to.

child - The child to add.

getBestExecutionNode

public IExecutionNode<?> getBestExecutionNode(Node proofNode)

Returns the best matching IExecutionNode for the given proof Node in the parent hierarchy.

Parameters:

proofNode - The proof Node.

Returns:

The best matching IExecutionNode or null if not available.

getExecutionNode

public IExecutionNode<?> getExecutionNode(Node proofNode)

Searches the IExecutionNode which represents the given Node of KeY's proof tree.

In case that the Node is represented by multiple AbstractExecutionNodes, e.g. a return statement and a method return, the last node is returned.

Parameters:

proofNode - The Node in KeY's proof tree.

Returns:

The IExecutionNode representation or null if no one is available.

createPoPropertiesToForce

public static java.util.Properties createPoPropertiesToForce()

Returns the minimal required PO Properties to support symbolic execution tree extraction in a SymbolicExecutionJavaProfile.

Returns:

The minimal required PO Properties.