de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.AbstractKeYlessExecutionNode<S extends SourceElement>

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode<S>

All Implemented Interfaces:

IExecutionElement, IExecutionNode<S>

Direct Known Subclasses:

ExecutionNodeReader.AbstractKeYlessBaseExecutionNode, ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode, ExecutionNodeReader.KeYlessBlockContract, ExecutionNodeReader.KeYlessBranchCondition, ExecutionNodeReader.KeYlessJoin, ExecutionNodeReader.KeYlessLoopInvariant, ExecutionNodeReader.KeYlessMethodCall, ExecutionNodeReader.KeYlessOperationContract, ExecutionNodeReader.KeYlessStart, ExecutionNodeReader.KeYlessStatement, ExecutionNodeReader.KeYlessTermination

Enclosing class:

ExecutionNodeReader

public abstract static class ExecutionNodeReader.AbstractKeYlessExecutionNode<S extends SourceElement>
extends ExecutionNodeReader.AbstractKeYlessExecutionElement
implements IExecutionNode<S>

An abstract implementation of IExecutionNode which is independent from KeY and provides such only children and default attributes.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.List<IExecutionNode<?>>	callStack The call stack.
private java.util.List<IExecutionNode<?>>	children The children.
private ImmutableList<IExecutionBlockStartNode<?>>	completedBlocks The completed blocks.
private java.util.List<IExecutionConstraint>	constraints The contained constraints.
private java.util.Map<IExecutionBlockStartNode<?>,java.lang.String>	formatedCompletedBlockConditions The formated conditions under which a block is completed.
private java.lang.String	formatedPathCondition The formated path condition.
private ImmutableList<IExecutionLink>	incomingLinks The contained incoming links.
private ImmutableList<IExecutionLink>	outgoingLinks The contained outgoing links.
private IExecutionNode<?>	parent The parent IExecutionNode.
private boolean	pathConditionChanged Is the path condition changed compared to parent?
private java.util.List<IExecutionVariable>	variables The contained variables.

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
AbstractKeYlessExecutionNode(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addCallStackEntry(IExecutionNode<?> entry) Adds the given entry to the call stack.
void	addChild(IExecutionNode<?> child) Adds the given child.
void	addCompletedBlock(IExecutionBlockStartNode<?> completedBlock, java.lang.String formatedCondition) Adds the given completed block.
void	addConstraint(IExecutionConstraint constraint) Adds the given IExecutionConstraint.
void	addIncomingLink(IExecutionLink link) Adds the incoming IExecutionLink.
void	addOutgoingLink(IExecutionLink link) Adds the outgoing IExecutionLink.
void	addVariable(IExecutionVariable variable) Adds the given IExecutionVariable.
PositionInfo	getActivePositionInfo() Returns the PositionInfo of IExecutionNode.getActiveStatement().
S	getActiveStatement() Returns the active statement which is executed in the code.
Term	getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) Returns the condition under which this node completes the code block of the given IExecutionBlockStartNode.
IExecutionNode<?>[]	getCallStack() Returns the method call stack.
IExecutionNode<?>[]	getChildren() Returns the available children.
ImmutableList<IExecutionBlockStartNode<?>>	getCompletedBlocks() Returns all code blocks completed by this IExecutionBlockStartNode.
IExecutionConstraint[]	getConstraints() Returns all available IExecutionConstraints.
ISymbolicLayout	getCurrentLayout(int configurationIndex) Returns the current memory layout which shows the memory structure before the current node in the symbolic execution tree is executed.
java.lang.String	getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode) Returns the human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.
java.lang.String	getFormatedPathCondition() Returns the human readable path condition to reach this node as string.
IExecutionLink	getIncomingLink(IExecutionNode<?> source) Returns the incoming IExecutionLink.
ImmutableList<IExecutionLink>	getIncomingLinks() Returns all available incoming links.
ISymbolicLayout	getInitialLayout(int configurationIndex) Returns the initial memory layout before the method was executed.
int	getLayoutsCount() Returns the number of memory layouts.
ImmutableList<ISymbolicEquivalenceClass>	getLayoutsEquivalenceClasses(int configurationIndex) Returns the equivalence classes of the memory layout with the given index.
PosInOccurrence	getModalityPIO() Returns the PosInOccurrence of the modality of interest including updates.
IExecutionLink	getOutgoingLink(IExecutionNode<?> target) Returns the outgoing IExecutionLink.
ImmutableList<IExecutionLink>	getOutgoingLinks() Returns all available outgoing links.
IExecutionNode<?>	getParent() Returns the parent IExecutionNode or null if the current node is the root.
Term	getPathCondition() Returns the path condition to reach this node as Term.
IExecutionVariable[]	getVariables() Returns the variable value pairs of the current state.
IExecutionVariable[]	getVariables(Term condition) Returns the variable value pairs of the current state under the given condition.
boolean	isPathConditionChanged() Checks if this node has changed the path condition of the parent.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getElementType, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

parent

private final IExecutionNode<?> parent

The parent IExecutionNode.

children

private final java.util.List<IExecutionNode<?>> children

The children.

formatedPathCondition

private final java.lang.String formatedPathCondition

The formated path condition.

pathConditionChanged

private final boolean pathConditionChanged

Is the path condition changed compared to parent?

callStack

private final java.util.List<IExecutionNode<?>> callStack

The call stack.

constraints

private final java.util.List<IExecutionConstraint> constraints

The contained constraints.

variables

private final java.util.List<IExecutionVariable> variables

The contained variables.

completedBlocks

private ImmutableList<IExecutionBlockStartNode<?>> completedBlocks

The completed blocks.

formatedCompletedBlockConditions

private final java.util.Map<IExecutionBlockStartNode<?>,java.lang.String> formatedCompletedBlockConditions

The formated conditions under which a block is completed.

outgoingLinks

private ImmutableList<IExecutionLink> outgoingLinks

The contained outgoing links.

incomingLinks

private ImmutableList<IExecutionLink> incomingLinks

The contained incoming links.

Constructor Detail

AbstractKeYlessExecutionNode

public AbstractKeYlessExecutionNode(IExecutionNode<?> parent,
                                    java.lang.String name,
                                    java.lang.String formatedPathCondition,
                                    boolean pathConditionChanged)

Constructor.

Parameters:

parent - The parent IExecutionNode.

name - The name of this node.

formatedPathCondition - The formated path condition.

pathConditionChanged - Is the path condition changed compared to parent?

Method Detail

getParent

public IExecutionNode<?> getParent()

Returns the parent IExecutionNode or null if the current node is the root.

Specified by:

getParent in interface IExecutionNode<S extends SourceElement>

Returns:

The parent IExecutionNode or null on root.

addChild

public void addChild(IExecutionNode<?> child)

Adds the given child.

Parameters:

child - The child to add.

getChildren

public IExecutionNode<?>[] getChildren()

Returns the available children.

Specified by:

getChildren in interface IExecutionNode<S extends SourceElement>

Returns:

The available children.

getPathCondition

public Term getPathCondition()
                      throws ProofInputException

Returns the path condition to reach this node as Term.

Specified by:

getPathCondition in interface IExecutionNode<S extends SourceElement>

Returns:

The path condition to reach this node as Term.

Throws:

ProofInputException

getFormatedPathCondition

public java.lang.String getFormatedPathCondition()
                                          throws ProofInputException

Returns the human readable path condition to reach this node as string.

Specified by:

getFormatedPathCondition in interface IExecutionNode<S extends SourceElement>

Returns:

The human readable path condition as string.

Throws:

ProofInputException

isPathConditionChanged

public boolean isPathConditionChanged()

Checks if this node has changed the path condition of the parent.

Specified by:

isPathConditionChanged in interface IExecutionNode<S extends SourceElement>

Returns:

true has different path condition compared to its parent, false has same path condition as parent.

addCallStackEntry

public void addCallStackEntry(IExecutionNode<?> entry)

Adds the given entry to the call stack.

Parameters:

entry - The entry to add to the call stack.

getCallStack

public IExecutionNode<?>[] getCallStack()

Returns the method call stack.

Specified by:

getCallStack in interface IExecutionNode<S extends SourceElement>

Returns:

The method call stack.

addConstraint

public void addConstraint(IExecutionConstraint constraint)

Adds the given IExecutionConstraint.

Parameters:

constraint - The IExecutionConstraint to add.

getConstraints

public IExecutionConstraint[] getConstraints()

Returns all available IExecutionConstraints.

Specified by:

getConstraints in interface IExecutionNode<S extends SourceElement>

Returns:

The available IExecutionConstraints.

addVariable

public void addVariable(IExecutionVariable variable)

Adds the given IExecutionVariable.

Parameters:

variable - The IExecutionVariable to add.

getActiveStatement

public S getActiveStatement()

Returns the active statement which is executed in the code.

Specified by:

getActiveStatement in interface IExecutionNode<S extends SourceElement>

Returns:

The active statement which is executed in the code.

getActivePositionInfo

public PositionInfo getActivePositionInfo()

Returns the PositionInfo of IExecutionNode.getActiveStatement().

Specified by:

getActivePositionInfo in interface IExecutionNode<S extends SourceElement>

Returns:

The PositionInfo of IExecutionNode.getActiveStatement().

getVariables

public IExecutionVariable[] getVariables()

Returns the variable value pairs of the current state.

Specified by:

getVariables in interface IExecutionNode<S extends SourceElement>

Returns:

The variable value pairs.

getVariables

public IExecutionVariable[] getVariables(Term condition)

Returns the variable value pairs of the current state under the given condition.

Specified by:

getVariables in interface IExecutionNode<S extends SourceElement>

Parameters:

condition - A Term specifying some additional constraints to consider.

Returns:

The variable value pairs.

getLayoutsCount

public int getLayoutsCount()
                    throws ProofInputException

Returns the number of memory layouts.

Specified by:

getLayoutsCount in interface IExecutionNode<S extends SourceElement>

Returns:

The number of memory layouts.

Throws:

ProofInputException - Occurred Exception.

getInitialLayout

public ISymbolicLayout getInitialLayout(int configurationIndex)
                                 throws ProofInputException

Returns the initial memory layout before the method was executed.

Specified by:

getInitialLayout in interface IExecutionNode<S extends SourceElement>

Parameters:

configurationIndex - The index of the memory layout.

Returns:

The initial memory layout at the given index.

Throws:

ProofInputException - Occurred Exception.

getCurrentLayout

public ISymbolicLayout getCurrentLayout(int configurationIndex)
                                 throws ProofInputException

Returns the current memory layout which shows the memory structure before the current node in the symbolic execution tree is executed.

Specified by:

getCurrentLayout in interface IExecutionNode<S extends SourceElement>

Parameters:

configurationIndex - The index of the memory layout.

Returns:

The current memory layout at the given index.

Throws:

ProofInputException - Occurred Exception.

getLayoutsEquivalenceClasses

public ImmutableList<ISymbolicEquivalenceClass> getLayoutsEquivalenceClasses(int configurationIndex)
                                                                      throws ProofInputException

Returns the equivalence classes of the memory layout with the given index.

Specified by:

getLayoutsEquivalenceClasses in interface IExecutionNode<S extends SourceElement>

Parameters:

configurationIndex - The index of the memory layout.

Returns:

The equivalence classes of the memory layout at the given index.

Throws:

ProofInputException - Occurred Exception.

getModalityPIO

public PosInOccurrence getModalityPIO()

Returns the PosInOccurrence of the modality of interest including updates.

Specified by:

getModalityPIO in interface IExecutionElement

Returns:

The PosInOccurrence of the modality of interest including updates.

getCompletedBlocks

public ImmutableList<IExecutionBlockStartNode<?>> getCompletedBlocks()

Returns all code blocks completed by this IExecutionBlockStartNode.

Specified by:

getCompletedBlocks in interface IExecutionNode<S extends SourceElement>

Returns:

All code blocks completed by this IExecutionBlockStartNode.

getBlockCompletionCondition

public Term getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
                                 throws ProofInputException

Returns the condition under which this node completes the code block of the given IExecutionBlockStartNode.

Specified by:

getBlockCompletionCondition in interface IExecutionNode<S extends SourceElement>

Parameters:

completedNode - The completed IExecutionBlockStartNode for which the condition is requested.

Returns:

The condition under which this node completes the code block of the given IExecutionBlockStartNode.

Throws:

ProofInputException

getFormatedBlockCompletionCondition

public java.lang.String getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
                                                     throws ProofInputException

Returns the human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.

Specified by:

getFormatedBlockCompletionCondition in interface IExecutionNode<S extends SourceElement>

Parameters:

completedNode - The completed IExecutionBlockStartNode for which the condition is requested.

Returns:

The human readable condition under which this node completes the code block of the given IExecutionBlockStartNode.

Throws:

ProofInputException

addCompletedBlock

public void addCompletedBlock(IExecutionBlockStartNode<?> completedBlock,
                              java.lang.String formatedCondition)

Adds the given completed block.

Parameters:

completedBlock - The completed block.

formatedCondition - The formated condition under which the block is completed.

getOutgoingLink

public IExecutionLink getOutgoingLink(IExecutionNode<?> target)

Returns the outgoing IExecutionLink.

Specified by:

getOutgoingLink in interface IExecutionNode<S extends SourceElement>

Parameters:

target - The target IExecutionNode.

Returns:

The found IExecutionLink or null if such a link is not available.

addOutgoingLink

public void addOutgoingLink(IExecutionLink link)

Adds the outgoing IExecutionLink.

Parameters:

link - The outgoing IExecutionLink to add.

getOutgoingLinks

public ImmutableList<IExecutionLink> getOutgoingLinks()

Returns all available outgoing links.

Specified by:

getOutgoingLinks in interface IExecutionNode<S extends SourceElement>

Returns:

The available outgoing links.

addIncomingLink

public void addIncomingLink(IExecutionLink link)

Adds the incoming IExecutionLink.

Parameters:

link - The incoming IExecutionLink to add.

getIncomingLink

public IExecutionLink getIncomingLink(IExecutionNode<?> source)

Returns the incoming IExecutionLink.

Specified by:

getIncomingLink in interface IExecutionNode<S extends SourceElement>

Parameters:

source - The source IExecutionNode.

Returns:

The found IExecutionLink or null if such a link is not available.

getIncomingLinks

public ImmutableList<IExecutionLink> getIncomingLinks()

Returns all available incoming links.

Specified by:

getIncomingLinks in interface IExecutionNode<S extends SourceElement>

Returns:

The available incoming links.