de.uka.ilkd.key.symbolic_execution

Class ExecutionVariableExtractor

java.lang.Object

de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor

public class ExecutionVariableExtractor
extends AbstractUpdateExtractor

Extracts the current state and represents it as IExecutionVariables.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ExecutionVariableExtractor.ExtractedExecutionValue The IExecutionValue instantiated by the ExecutionVariableExtractor.
static class	ExecutionVariableExtractor.ExtractedExecutionVariable The IExecutionVariable instantiated by the ExecutionVariableExtractor.
private static class	ExecutionVariableExtractor.LocationDefinition Utility class representing a location.
private static class	ExecutionVariableExtractor.ParentDefinition Utility class representing a parent definition.
private class	ExecutionVariableExtractor.StateExecutionVariable The IExecutionVariable instantiated by the ExecutionVariableExtractor.

Nested classes/interfaces inherited from class de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

AbstractUpdateExtractor.ExecutionVariableValuePair, AbstractUpdateExtractor.ExtractLocationParameter, AbstractUpdateExtractor.NodeGoal

Field Summary

Fields

Modifier and Type	Field and Description
private Term	additionalCondition An optional additional condition.
private java.util.Map<ExecutionVariableExtractor.LocationDefinition,ExecutionVariableExtractor.StateExecutionVariable>	allStateVariables The found IExecutionVariables available via analyse().
private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter>	currentLocations The current locations.
private IExecutionNode<?>	executionNode The current IExecutionNode.
private Term	layoutTerm The layout term.
private java.util.Set<Term>	objectsToIgnore The objects to ignore.
private boolean	simplifyConditions true simplify conditions, false do not simplify conditions.

Fields inherited from class de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

modalityPio, node

Constructor Summary

Constructors

Constructor and Description
ExecutionVariableExtractor(Node node, PosInOccurrence modalityPio, IExecutionNode<?> executionNode, Term condition, boolean simplifyConditions) Constructor.

Method Summary

Modifier and Type	Method and Description
IExecutionVariable[]	analyse() Extracts the current state and represents it as IExecutionVariables.
protected void	analyzeTreeStructure(java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>> topVariables, java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap) Analyzes the tree structure of the given ExecutionVariableValuePairs.
protected void	createValues(IExecutionVariable variable, java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, AbstractUpdateExtractor.ExecutionVariableValuePair firstPair, java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap, java.util.List<IExecutionValue> valueListToFill, ImmutableList<Term> alreadyVisitedObjects) Creates the IExecutionValues of the given IExecutionVariable.
protected IExecutionVariable	createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap, ExecutionVariableExtractor.ExtractedExecutionValue parentValue, ImmutableList<Term> alreadyVisitedObjects) Creates an IExecutionVariable for the given ExecutionVariableValuePairs.
protected Pair<java.lang.Boolean,ImmutableList<Term>>	updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects, Term value) Updates the already visited objects list if required.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

collectAdditionalUpdates, collectLocationsFromHeapTerms, collectLocationsFromHeapUpdate, collectLocationsFromTerm, collectLocationsFromTerm, collectLocationsFromUpdates, computeBranchCondition, computeInitialObjectsToIgnore, computeOriginalUpdates, computeValueConditions, computeVariableValuePairs, containsImplicitProgramVariable, countOpenChildren, createLocationPredicateAndTerm, extractLocationsFromSequent, extractLocationsFromTerm, fillInitialObjectsToIgnoreRecursively, getProof, getRoot, getServices, hasFreeVariables, isImplicitProgramVariable, isParentReachedOnAllChildGoals, iterateBackOnParents, removeImplicitSubTermsFromPathCondition

Methods inherited from class java.lang.Object

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

Field Detail

executionNode

private final IExecutionNode<?> executionNode

The current IExecutionNode.

additionalCondition

private final Term additionalCondition

An optional additional condition.

layoutTerm

private final Term layoutTerm

The layout term.

currentLocations

private final java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> currentLocations

The current locations.

objectsToIgnore

private final java.util.Set<Term> objectsToIgnore

The objects to ignore.

allStateVariables

private final java.util.Map<ExecutionVariableExtractor.LocationDefinition,ExecutionVariableExtractor.StateExecutionVariable> allStateVariables

The found IExecutionVariables available via analyse().

simplifyConditions

private final boolean simplifyConditions

true simplify conditions, false do not simplify conditions.

Constructor Detail

ExecutionVariableExtractor

public ExecutionVariableExtractor(Node node,
                                  PosInOccurrence modalityPio,
                                  IExecutionNode<?> executionNode,
                                  Term condition,
                                  boolean simplifyConditions)
                           throws ProofInputException

Constructor.

Parameters:

node - The Node which provides the state.

modalityPio - The PosInOccurrence in the Node.

executionNode - The current IExecutionNode.

condition - An optional additional condition.

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

Throws:

ProofInputException - Occurred Exception

Method Detail

analyse

public IExecutionVariable[] analyse()
                             throws ProofInputException

Extracts the current state and represents it as IExecutionVariables.

Returns:

The IExecutionVariables representing the current state.

Throws:

ProofInputException - Occurred Exception.

analyzeTreeStructure

protected void analyzeTreeStructure(java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
                                    java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>> topVariables,
                                    java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap)

Analyzes the tree structure of the given ExecutionVariableValuePairs.

Parameters:

pairs - The ExecutionVariableValuePairs to analyze.

topVariables - The state locations,

contentMap - The child locations.

createVariablesValueStructure

protected IExecutionVariable createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
                                                           java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
                                                           ExecutionVariableExtractor.ExtractedExecutionValue parentValue,
                                                           ImmutableList<Term> alreadyVisitedObjects)
                                                    throws ProofInputException

Creates an IExecutionVariable for the given ExecutionVariableValuePairs.

Parameters:

pairs - The ExecutionVariableValuePairs to represent.

contentMap - The Map providing child content information.

parentValue - The optional parent IExecutionValue.

alreadyVisitedObjects - The value Terms of already visited objects on the current path in the variable-value-hierarchy.

Returns:

The created IExecutionVariable.

Throws:

ProofInputException - Occurred Exception.

createValues

protected void createValues(IExecutionVariable variable,
                            java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
                            AbstractUpdateExtractor.ExecutionVariableValuePair firstPair,
                            java.util.Map<ExecutionVariableExtractor.ParentDefinition,java.util.Map<ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
                            java.util.List<IExecutionValue> valueListToFill,
                            ImmutableList<Term> alreadyVisitedObjects)
                     throws ProofInputException

Creates the IExecutionValues of the given IExecutionVariable.

Parameters:

variable - The IExecutionVariable.

pairs - The ExecutionVariableValuePairs which provides the content.

firstPair - The first entry in the ExecutionVariableValuePairs.

contentMap - The content Map.

valueListToFill - The result List to fill.

alreadyVisitedObjects - The value Terms of already visited objects on the current path in the variable-value-hierarchy.

Throws:

ProofInputException - Occurred Exception.

updateAlreadyVisitedObjects

protected Pair<java.lang.Boolean,ImmutableList<Term>> updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects,
                                                                                  Term value)

Updates the already visited objects list if required.

Parameters:

alreadyVisitedObjects - The value Terms of already visited objects on the current path in the variable-value-hierarchy.

value - The current value.

Returns:

The new already visited objects list or the original one if the current value is not an object.