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 IExecutionNode
s 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 Sequent
s 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); // ...
AbstractOperationPO.isAddUninterpretedPredicate()
,
IExecutionNode
,
IExecutionStart
,
SymbolicExecutionStrategy
,
ExecutionNodePreorderIterator
Modifier and Type | Class and Description |
---|---|
private class |
SymbolicExecutionTreeBuilder.AnalyzerProofVisitor
This
ProofVisitor is used to transfer the proof tree in KeY
into IExecutionNode s 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 MethodFrame s. |
static class |
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions
Instances of this class are returned by
analyse()
to inform about newly completed blocks and returned methods. |
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
Node s 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 AbstractExecutionNode s,
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 and Description |
---|
SymbolicExecutionTreeBuilder(Proof proof,
boolean mergeBranchConditions,
boolean useUnicode,
boolean usePrettyPrinting,
boolean variablesAreOnlyComputedFromUpdates,
boolean simplifyConditions)
Constructor.
|
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 IExecutionNode s 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)
|
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
Node s of method calls for
which its return should be ignored. |
protected java.util.Set<Node> |
getMethodReturnsToIgnore(RuleApp ruleApp)
Returns the method
Node s of method calls for
which its return should be ignored. |
protected java.util.Set<Node> |
getMethodReturnsToIgnore(SymbolicExecutionTermLabel label)
Returns the method
Node s 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 MethodFrame s 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
IExecutionNode s 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. |
private ExecutionStart startNode
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 AbstractExecutionNode
s,
e.g. a return statement and a method return, the last node is returned.
private java.util.Map<Node,java.util.List<AbstractExecutionNode<?>>> multipleExecutionNodes
Node
is represented by multiple AbstractExecutionNode
s,
this map maps the Node
to all its representations.private java.util.Map<Node,ExecutionLoopCondition> keyNodeLoopConditionMapping
Node
of KeY's proof tree to his
execution tree model representation (IExecutionLoopCondition
) if it is available.private java.util.Map<Node,ExecutionBranchCondition> keyNodeBranchConditionMapping
Node
of KeY's proof tree to his
execution tree model representation (IExecutionBranchCondition
) if it is available.private java.util.Map<java.lang.Integer,java.util.Map<Node,ImmutableList<Node>>> methodCallStackMap
SymbolicExecutionTermLabel.getId()
used.private java.util.Map<java.lang.Integer,java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>>> afterBlockMap
SymbolicExecutionTermLabel.getId()
used.private java.util.Map<java.lang.Integer,java.util.Set<Node>> methodReturnsToIgnoreMap
Node
s of method calls which return statements should be ignored.
As key is SymbolicExecutionTermLabel.getId()
used.private IProgramVariable exceptionVariable
private final TreeSettings settings
TreeSettings
to use.private final boolean isUninterpretedPredicateUsed
true
infeasible paths are closed, false
infeasible may be open may be closed.private final java.util.Deque<java.util.Map.Entry<AbstractExecutionNode<?>,java.util.List<ExecutionBranchCondition>>> branchConditionsStack
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.public SymbolicExecutionTreeBuilder(Proof proof, boolean mergeBranchConditions, boolean useUnicode, boolean usePrettyPrinting, boolean variablesAreOnlyComputedFromUpdates, boolean simplifyConditions)
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
IExecutionVariable
s are computed according to the type structure of the visible memory.simplifyConditions
- true
simplify conditions, false
do not simplify conditions.protected void initMethodCallStack(Node root, Services services)
This method initializes #methodCallStack
in case that the
initial Sequent
contains MethodFrame
s 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.
protected java.util.Set<Node> getMethodReturnsToIgnore(RuleApp ruleApp)
Node
s of method calls for
which its return should be ignored. If not already
available an empty method Set
is created.ruleApp
- The RuleApp
which modifies a modality Term
with a SymbolicExecutionTermLabel
.Set
of Node
s to ignore its return.protected java.util.Set<Node> getMethodReturnsToIgnore(SymbolicExecutionTermLabel label)
Node
s of method calls for
which its return should be ignored. If not already
available an empty method Set
is created.label
- The SymbolicExecutionTermLabel
which provides the ID.Set
of Node
s to ignore its return.protected java.util.Set<Node> getMethodReturnsToIgnore(int id)
Node
s of method calls for
which its return should be ignored. If not already
available an empty method Set
is created.id
- The ID.Set
of Node
s to ignore its return.protected java.util.Map<Node,ImmutableList<Node>> getMethodCallStack(RuleApp ruleApp)
ruleApp
- The RuleApp
which modifies a modality Term
with a SymbolicExecutionTermLabel
.Term
with a SymbolicExecutionTermLabel
.protected java.util.Map<Node,ImmutableList<Node>> getMethodCallStack(SymbolicExecutionTermLabel label)
label
- The SymbolicExecutionTermLabel
which provides the ID.SymbolicExecutionTermLabel
.protected java.util.Map<Node,ImmutableList<Node>> getMethodCallStack(int id)
id
- The ID.public void dispose()
SymbolicExecutionTreeBuilder
instance! Later usage
is not checked and punished with exceptions.public Proof getProof()
Proof
from which the symbolic execution tree is extracted.Proof
from which the symbolic execution tree is extracted.public IExecutionStart getStartNode()
public SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions analyse()
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions
during symbolic execution.public java.util.Set<AbstractExecutionNode<?>> prune(Node node)
IExecutionNode
in the parent hierarchy of the given
Node
(including the Node itself).node
- Node
to be pruned.AbstractExecutionNode
's which where deleted.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 IExecutionNode
s 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)==>)
.
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.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).protected IExecutionBranchCondition searchDirectParentBodyPreservesInvariantBranchCondition(IExecutionNode<?> current)
IExecutionBranchCondition
representing
the 'Body Preserves Invariant' branch.current
- The IExecutionNode
to check its parent IExecutionBranchCondition
s.IExecutionBranchCondition
or null
if not available.protected boolean shouldPrune(Node node)
protected AbstractExecutionNode<?> addNodeToTreeAndUpdateParent(Node node, AbstractExecutionNode<?> parentToAddTo, AbstractExecutionNode<?> executionNode)
AbstractExecutionNode
to the symbolic execution tree
if available and returns the new parent for future detected nodes.node
- The Node
.parentToAddTo
- The parent AbstractExecutionNode
.executionNode
- The new child AbstractExecutionNode
.AbstractExecutionNode
.protected void updateCallStack(Node node, SourceElement statement)
#methodCallStack
) if the given Node
in KeY's proof tree is a method call.node
- The current Node
.statement
- The statement (SourceElement
).protected ImmutableList<Node> findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack, Node node)
protected AbstractExecutionNode<?> createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent, Node node, SourceElement statement)
IExecutionNode
)
if possible for the given Node
in KeY's proof tree.parent
- The parent IExecutionNode
.node
- The Node
in the proof tree of KeY.statement
- The actual statement (SourceElement
).IExecutionNode
or null
if the Node
should be ignored in the symbolic execution tree.protected void addToBlockMap(Node node, AbstractExecutionBlockStartNode<?> blockStartNode)
AbstractExecutionNode
add reason for a new block to the block maps.node
- The current Node
.blockStartNode
- The AbstractExecutionNode
to add.protected void addToBlockMap(Node node, AbstractExecutionBlockStartNode<?> blockStartNode, int stackSize, SourceElement... sourceElements)
AbstractExecutionNode
add reason for a new block to the block maps.node
- The current Node
.blockStartNode
- The AbstractExecutionNode
to add.secondPair
- The next element to end at.private boolean checkBlockPossibility(Node node, int expectedStackSize, SourceElement... expectedSourceElements)
Node
opens a block.node
- The current Node
.expectedStackSize
- The expected stack size.expectedSourceElements
- The expected after block SourceElement
s.false
A block is definitively not possible, true
a block is or might be possible.protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps, Node node)
Map
in the given once for the given Node
.afterBlockMaps
- The available after sblock Map
s.node
- The Node
for which the block Map
is requested.Map
or null
if not available.protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> getAfterBlockMaps(SymbolicExecutionTermLabel label)
label
- The SymbolicExecutionTermLabel
which provides the ID.SymbolicExecutionTermLabel
.protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> getAfterBlockMaps(int id)
id
- The ID.protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> updateAfterBlockMap(Node node, RuleApp ruleApp)
protected boolean isContained(ImmutableList<IExecutionNode<?>> list, Node node)
IExecutionNode
s represents the given Node
.list
- The IExecutionNode
s to check.node
- The Node
to check for.true
is contained, false
is not contained.protected boolean isAfterBlockReached(int currentStackSize, MethodFrame currentInnerMostMethodFrame, SourceElement currentActiveStatement, SymbolicExecutionTreeBuilder.JavaPair expectedPair)
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.true
after block is reached, false
after block is not reached.protected boolean isAfterBlockReached(int currentStackSize, MethodFrame currentInnerMostMethodFrame, SourceElement currentActiveStatement, int expectedStackSize, java.util.Iterator<SourceElement> expectedStatementsIterator)
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.true
after block is reached, false
after block is not reached.protected AbstractExecutionMethodReturn<?> createMehtodReturn(AbstractExecutionNode<?> parent, Node node, SourceElement statement, SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
parent
- The parent AbstractExecutionNode
.node
- The Node
which represents a method return.statement
- The currently active SourceElement
.completions
- The SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions
to update.AbstractExecutionMethodReturn
.protected boolean isNotInImplicitMethod(Node node)
Node
is not in an implicit method.node
- The Node
to check.true
is not implicit, false
is implicitprotected void initNewLoopBodyMethodCallStack(Node node)
MethodFrame
in the new modality is its method call Node
added to the new
method call stack.node
- The Node
on which the loop invariant rule is applied.protected void initNewValidiityMethodCallStack(Node node)
MethodFrame
in the new modality is its method call Node
added to the new
method call stack.node
- The Node
on which the block contract rule is applied.protected void initNewMethodCallStack(Node currentNode, PosInOccurrence childPIO)
currentNode
- The current Node
.childPIO
- The PosInOccurrence
where the modality has a new symbolic execution label counter.public boolean isUninterpretedPredicateUsed()
true
uninterpreted predicate is available, false
otherwise.protected IExecutionNode<?>[] createCallStack(Node node)
Node
.node
- The Node
.protected boolean isInImplicitMethod(Node node)
Node
handles something in an implicit method.node
- The Node
to check.true
is in implicit method, false
is not in implicit method.protected boolean hasBranchCondition(Node node)
Node
has a branch condition.node
- The Node
to check.true
has branch condition, false
has no branch condition.protected Node searchPreviousSymbolicExecutionNode(Node node)
protected void addChild(AbstractExecutionNode<?> parent, AbstractExecutionNode<?> child)
parent
- The parent to add to.child
- The child to add.public IExecutionNode<?> getBestExecutionNode(Node proofNode)
IExecutionNode
for the given proof Node
in the parent hierarchy.proofNode
- The proof Node
.IExecutionNode
or null
if not available.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 AbstractExecutionNode
s,
e.g. a return statement and a method return, the last node is returned.
proofNode
- The Node
in KeY's proof tree.IExecutionNode
representation or null
if no one is available.public static java.util.Properties createPoPropertiesToForce()
Properties
to support
symbolic execution tree extraction in a SymbolicExecutionJavaProfile
.Properties
.