de.uka.ilkd.key.symbolic_execution

Class AbstractUpdateExtractor

java.lang.Object

de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

Direct Known Subclasses:

ExecutionVariableExtractor, SymbolicLayoutExtractor

public abstract class AbstractUpdateExtractor
extends java.lang.Object

Provides the basic functionality to extract values from updates.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	AbstractUpdateExtractor.ExecutionVariableValuePair Represents a location (value or association of a given object/state) in a concrete memory layout of the initial or current state.
class	AbstractUpdateExtractor.ExtractLocationParameter Instances of this class provides the Term which are required to compute a location (value or association of a given object/state).
protected static class	AbstractUpdateExtractor.NodeGoal Utility class used by AbstractUpdateExtractor#computeValueConditions(Set, Map).

Field Summary

Fields

Modifier and Type	Field and Description
protected PosInOccurrence	modalityPio The PosInOccurrence of the modality or its updates.
protected Node	node Contains the Node of KeY's proof tree to compute memory layouts for.
private int	preVariableIndex An incremented number used to give each pre value an unique name.

Constructor Summary

Constructors

Constructor and Description
AbstractUpdateExtractor(Node node, PosInOccurrence modalityPio) Constructor.

Method Summary

Modifier and Type	Method and Description
protected java.util.List<Term>	collectAdditionalUpdates() Collects additional updates.
protected void	collectLocationsFromHeapTerms(Term selectTerm, Term variableTerm, HeapLDT heapLDT, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill, java.util.Set<Term> objectsToIgnore) Collects the AbstractUpdateExtractor.ExtractLocationParameter location from the heap Terms.
protected void	collectLocationsFromHeapUpdate(Term term, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill, java.util.Set<Term> updateCreatedObjectsToFill, java.util.Set<Term> updateValueObjectsToFill) Computes for each location (value/association of an object) used in the the given heap update Term the Terms which allows to compute the object itself and the value of the value/association.
protected void	collectLocationsFromTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill, Term term, java.util.Set<Term> objectsToIgnore) Utility method of extractLocationsFromTerm(Term, Set) which recursively extracts the locations.
protected void	collectLocationsFromTerm(Term updateTerm, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill, java.util.Set<Term> updateCreatedObjectsToFill, java.util.Set<Term> updateValueObjectsToFill, java.util.Set<Term> objectsToIgnore) Computes for each location (value/association of an object) used in the the given Term the Terms which allows to compute the object itself and the value of the value/association.
protected void	collectLocationsFromUpdates(Sequent sequent, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill, java.util.Set<Term> updateCreatedObjectsToFill, java.util.Set<Term> updateValueObjectsToFill, java.util.Set<Term> objectsToIgnore) Computes for each location (value/association of an object) used in the updates of the given Sequent the Terms which allows to compute the object itself and the value of the value/association.
protected Term	computeBranchCondition(Node node, java.util.Map<Node,Term> branchConditionCache, boolean simplifyConditions) Computes the branch condition if not already present in the cache and stores it in the cache.
protected java.util.Set<Term>	computeInitialObjectsToIgnore(boolean ignoreExceptionVariable, boolean ignoreOldStateVariables) Computes objects which should be ignored in the state because they are part of the proof obligation and not of the source code.
protected ImmutableList<Term>	computeOriginalUpdates(PosInOccurrence pio, boolean currentLayout) Computes the original updates.
protected java.util.Map<Goal,Term>	computeValueConditions(java.util.Set<Goal> valueGoals, java.util.Map<Node,Term> branchConditionCache, boolean simplifyConditions) This method computes for all given Goals representing the same value their path conditions.
protected java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair>	computeVariableValuePairs(Term layoutCondition, Term layoutTerm, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations, boolean currentLayout, boolean simplifyConditions) The method starts a side proof with the given arguments to compute the values and objects of the requested memory layout.
protected boolean	containsImplicitProgramVariable(Term term) Checks if the given Term contains an implicit IProgramVariable.
protected int	countOpenChildren(Node node) Counts the number of open child Nodes.
protected Term	createLocationPredicateAndTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> valueSelectParameter) Creates a predicate and a Term which can be used to compute the values defined by the given AbstractUpdateExtractor.ExtractLocationParameters.
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter>	extractLocationsFromSequent(Sequent sequent, java.util.Set<Term> objectsToIgnore) Computes for each location (value/association of an object) used in the given Sequent the Terms which allows to compute the object itself and the value of the value/association.
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter>	extractLocationsFromTerm(Term term, java.util.Set<Term> objectsToIgnore) Computes for each location (value/association of an object) used in the given Term the Terms which allows to compute the object itself and the value of the value/association.
protected void	fillInitialObjectsToIgnoreRecursively(Term term, java.util.Set<Term> toFill) Utility method of #computeInitialObjectsToIgnore() which computes the objects to ignore recursively.
protected Proof	getProof() Returns the Proof of the analyzed Node.
protected Node	getRoot() Returns the root Node of the proof.
protected Services	getServices() Returns the Services of the analyzed Node.
protected boolean	hasFreeVariables(Term term) Checks if the given Term has free variables.
protected boolean	isImplicitProgramVariable(ProgramVariable var) Checks if the given ProgramVariable is implicit.
protected boolean	isParentReachedOnAllChildGoals(Node currentNode, java.util.List<AbstractUpdateExtractor.NodeGoal> branchLeafs) Checks if parent backward iteration on all given AbstractUpdateExtractor.NodeGoal has reached the given Node.
protected AbstractUpdateExtractor.NodeGoal	iterateBackOnParents(AbstractUpdateExtractor.NodeGoal nodeToStartAt, boolean force) Performs a backward iteration on the parents starting at the given AbstractUpdateExtractor.NodeGoal until the first parent with at least two open branches has been found.
protected Term	removeImplicitSubTermsFromPathCondition(Term pathCondition) Removes all conditions from the given path condition which contains implicit IProgramVariables.

Methods inherited from class java.lang.Object

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

Field Detail

node

protected final Node node

Contains the Node of KeY's proof tree to compute memory layouts for.

modalityPio

protected final PosInOccurrence modalityPio

The PosInOccurrence of the modality or its updates.

preVariableIndex

private int preVariableIndex

An incremented number used to give each pre value an unique name.

Constructor Detail

AbstractUpdateExtractor

public AbstractUpdateExtractor(Node node,
                               PosInOccurrence modalityPio)

Constructor.

Parameters:

node - The Node of KeY's proof tree to compute memory layouts for.

modalityPio - The PosInOccurrence of the modality or its updates.

Method Detail

removeImplicitSubTermsFromPathCondition

protected Term removeImplicitSubTermsFromPathCondition(Term pathCondition)

Removes all conditions from the given path condition which contains implicit IProgramVariables.

Parameters:

pathCondition - The path condition to check.

Returns:

The new path condition without conditions which uses implicit IProgramVariables.

containsImplicitProgramVariable

protected boolean containsImplicitProgramVariable(Term term)

Checks if the given Term contains an implicit IProgramVariable.

Parameters:

term - The Term to check.

Returns:

true Term contains implicit IProgramVariable, false Term contains no implicit IProgramVariable.

isImplicitProgramVariable

protected boolean isImplicitProgramVariable(ProgramVariable var)

Checks if the given ProgramVariable is implicit.

Parameters:

var - The ProgramVariable to check.

Returns:

true ProgramVariable is implicit, false ProgramVariable is not implicit or null.

computeInitialObjectsToIgnore

protected java.util.Set<Term> computeInitialObjectsToIgnore(boolean ignoreExceptionVariable,
                                                            boolean ignoreOldStateVariables)

Computes objects which should be ignored in the state because they are part of the proof obligation and not of the source code.

By default the set will contain the exc variable and the backup of arguments and the heap.

Parameters:

ignoreExceptionVariable - Ignore exception variable?

ignoreOldStateVariables - Ignore old state variables?

Returns:

The objects to ignore.

fillInitialObjectsToIgnoreRecursively

protected void fillInitialObjectsToIgnoreRecursively(Term term,
                                                     java.util.Set<Term> toFill)

Utility method of #computeInitialObjectsToIgnore() which computes the objects to ignore recursively.

Parameters:

term - The current Term.

toFill - The Set with Terms to ignore to fill.

collectLocationsFromUpdates

protected void collectLocationsFromUpdates(Sequent sequent,
                                           java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
                                           java.util.Set<Term> updateCreatedObjectsToFill,
                                           java.util.Set<Term> updateValueObjectsToFill,
                                           java.util.Set<Term> objectsToIgnore)
                                    throws ProofInputException

Computes for each location (value/association of an object) used in the updates of the given Sequent the Terms which allows to compute the object itself and the value of the value/association. The result is a Set of AbstractUpdateExtractor.ExtractLocationParameter which contains the computed Terms.

Objects which are created in the heap during symbolic execution and all objects which are used on the right side of associations are also collected and stored in the Sets updateCreatedObjectsToFill/ updateValueObjectsToFill.

Parameters:

sequent - The Sequent which provides the updates to extract locations from.

locationsToFill - The location Set to fill.

updateCreatedObjectsToFill - The new created object Set to fill.

updateValueObjectsToFill - The Set with objects used on right side of updates to fill.

objectsToIgnore - The objects to ignore.

Throws:

ProofInputException - Occurred Exception.

collectLocationsFromTerm

protected void collectLocationsFromTerm(Term updateTerm,
                                        java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
                                        java.util.Set<Term> updateCreatedObjectsToFill,
                                        java.util.Set<Term> updateValueObjectsToFill,
                                        java.util.Set<Term> objectsToIgnore)
                                 throws ProofInputException

Computes for each location (value/association of an object) used in the the given Term the Terms which allows to compute the object itself and the value of the value/association. The result is a Set of AbstractUpdateExtractor.ExtractLocationParameter which contains the computed Terms.

Objects which are created in the heap during symbolic execution and all objects which are used on the right side of associations are also collected and stored in the Sets updateCreatedObjectsToFill/ updateValueObjectsToFill.

Parameters:

updateTerm - The Term which provides the update to extract locations from.

locationsToFill - The location Set to fill.

updateCreatedObjectsToFill - The new created object Set to fill.

updateValueObjectsToFill - The Set with objects used on right side of updates to fill.

objectsToIgnore - The objects to ignore.

Throws:

ProofInputException - Occurred Exception.

collectLocationsFromHeapUpdate

protected void collectLocationsFromHeapUpdate(Term term,
                                              java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
                                              java.util.Set<Term> updateCreatedObjectsToFill,
                                              java.util.Set<Term> updateValueObjectsToFill)
                                       throws ProofInputException

Computes for each location (value/association of an object) used in the the given heap update Term the Terms which allows to compute the object itself and the value of the value/association. The result is a Set of AbstractUpdateExtractor.ExtractLocationParameter which contains the computed Terms.

Objects which are created in the heap during symbolic execution and all objects which are used on the right side of associations are also collected and stored in the Sets updateCreatedObjectsToFill/ updateValueObjectsToFill.

Parameters:

term - The Term which provides the heap update to extract locations from.

locationsToFill - The location Set to fill.

updateCreatedObjectsToFill - The new created object Set to fill.

updateValueObjectsToFill - The Set with objects used on right side of updates to fill.

Throws:

ProofInputException - Occurred Exception.

hasFreeVariables

protected boolean hasFreeVariables(Term term)

Checks if the given Term has free variables.

Parameters:

term - The Term to check.

Returns:

true has free variables, false does not have free variables.

extractLocationsFromSequent

protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> extractLocationsFromSequent(Sequent sequent,
                                                                                                      java.util.Set<Term> objectsToIgnore)
                                                                                               throws ProofInputException

Computes for each location (value/association of an object) used in the given Sequent the Terms which allows to compute the object itself and the value of the value/association. The result is a Set of AbstractUpdateExtractor.ExtractLocationParameter which contains the computed Terms.

Parameters:

sequent - The Sequent to extract locations from.

objectsToIgnore - The objects to ignore.

Returns:

The found locations.

Throws:

ProofInputException - Occurred Exception.

extractLocationsFromTerm

protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> extractLocationsFromTerm(Term term,
                                                                                                   java.util.Set<Term> objectsToIgnore)
                                                                                            throws ProofInputException

Computes for each location (value/association of an object) used in the given Term the Terms which allows to compute the object itself and the value of the value/association. The result is a Set of AbstractUpdateExtractor.ExtractLocationParameter which contains the computed Terms.

Parameters:

term - The Term to extract locations from.

objectsToIgnore - The objects to ignore.

Returns:

The found locations.

Throws:

ProofInputException - Occurred Exception.

collectLocationsFromTerm

protected void collectLocationsFromTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
                                        Term term,
                                        java.util.Set<Term> objectsToIgnore)
                                 throws ProofInputException

Utility method of extractLocationsFromTerm(Term, Set) which recursively extracts the locations.

Parameters:

toFill - The result Set to fill.

term - The current Term.

objectsToIgnore - The objects to ignore.

Throws:

ProofInputException - Occurred Exception.

collectLocationsFromHeapTerms

protected void collectLocationsFromHeapTerms(Term selectTerm,
                                             Term variableTerm,
                                             HeapLDT heapLDT,
                                             java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
                                             java.util.Set<Term> objectsToIgnore)
                                      throws ProofInputException

Collects the AbstractUpdateExtractor.ExtractLocationParameter location from the heap Terms.

Parameters:

selectTerm - The parent Term.

variableTerm - The Term with the ProgramVariable.

heapLDT - The HeapLDT to use.

toFill - The result Set to fill.

objectsToIgnore - The objects to ignore.

Throws:

ProofInputException - Occurred Exception.

createLocationPredicateAndTerm

protected Term createLocationPredicateAndTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> valueSelectParameter)

Creates a predicate and a Term which can be used to compute the values defined by the given AbstractUpdateExtractor.ExtractLocationParameters.

Parameters:

valueSelectParameter - The AbstractUpdateExtractor.ExtractLocationParameters to compute in the created Term.

Returns:

The created Term which computes the values of the given AbstractUpdateExtractor.ExtractLocationParameters.

getProof

protected Proof getProof()

Returns the Proof of the analyzed Node.

Returns:

The Proof of the analyzed Node.

getRoot

protected Node getRoot()

Returns the root Node of the proof.

Returns:

The root Node of the proof.

getServices

protected Services getServices()

Returns the Services of the analyzed Node.

Returns:

The Services of the analyzed Node.

computeVariableValuePairs

protected java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> computeVariableValuePairs(Term layoutCondition,
                                                                                                      Term layoutTerm,
                                                                                                      java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
                                                                                                      boolean currentLayout,
                                                                                                      boolean simplifyConditions)
                                                                                               throws ProofInputException

The method starts a side proof with the given arguments to compute the values and objects of the requested memory layout. The AbstractUpdateExtractor.ExecutionVariableValuePair together with the memory layout term defines how to access the side proof result.

The next step is the result extraction from side proof which results in a Set of AbstractUpdateExtractor.ExecutionVariableValuePair instances. Each instance defines a value or association of a parent object or the state itself.

Parameters:

layoutCondition - An optional condition to consider.

layoutTerm - The result term to use in side proof.

locations - The locations to compute in side proof.

currentLayout - true current layout, false initial layout.

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

Returns:

The computed AbstractUpdateExtractor.ExecutionVariableValuePairs.

Throws:

ProofInputException - Occurred Exception.

collectAdditionalUpdates

protected java.util.List<Term> collectAdditionalUpdates()

Collects additional updates.

Returns:

The additional updates.

computeOriginalUpdates

protected ImmutableList<Term> computeOriginalUpdates(PosInOccurrence pio,
                                                     boolean currentLayout)

Computes the original updates.

Parameters:

pio - The PosInOccurrence.

currentLayout - Is current layout?

Returns:

The original updates.

computeValueConditions

protected java.util.Map<Goal,Term> computeValueConditions(java.util.Set<Goal> valueGoals,
                                                          java.util.Map<Node,Term> branchConditionCache,
                                                          boolean simplifyConditions)
                                                   throws ProofInputException

This method computes for all given Goals representing the same value their path conditions. A computed path condition consists only of the branch conditions which contribute to the value. Branch conditions of splits which does not contribute to the value are ignored.

The implemented algorithm works as follows:

1. The given Goals have to be all Goals of the side proof providing the same value. This means that other branches/goals of the side proof result in different branches.
2. A backward iteration on the parent Nodes starting at the Goals is performed until the first parent with at least two open children has been found. The iteration is only performed on one goal (or the Node it stops last) at a time. The iteration is always performed on the Node with the highest serial number to ensure that different Goals will meet at their common parents.
3. When the iteration of all children of a Node has met, the branch conditions are computed if the split contributes to the value. A split contributes to a value if at least one branch is not reached by backward iteration meaning that its Goals provide different values.
4. The backward iteration ends when the root is reached.
5. Finally, for each Goal is the path condition computed. The path condition is the conjunction over all found branch conditions contributing to the value.

Parameters:

valueGoals - All Goals of the side proof which provide the same value (result).

branchConditionCache - A cache of already computed branch conditions.

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

Returns:

A Map which contains for each Goal the computed path condition consisting of only required splits.

Throws:

ProofInputException - Occurred Exception

isParentReachedOnAllChildGoals

protected boolean isParentReachedOnAllChildGoals(Node currentNode,
                                                 java.util.List<AbstractUpdateExtractor.NodeGoal> branchLeafs)

Checks if parent backward iteration on all given AbstractUpdateExtractor.NodeGoal has reached the given Node.

Parameters:

currentNode - The current Node to check.

branchLeafs - The AbstractUpdateExtractor.NodeGoal on which backward iteration was performed.

Returns:

true All AbstractUpdateExtractor.NodeGoals have passed the given Node, false if at least one AbstractUpdateExtractor.NodeGoal has not passed the given Node.

iterateBackOnParents

protected AbstractUpdateExtractor.NodeGoal iterateBackOnParents(AbstractUpdateExtractor.NodeGoal nodeToStartAt,
                                                                boolean force)

Performs a backward iteration on the parents starting at the given AbstractUpdateExtractor.NodeGoal until the first parent with at least two open branches has been found.

Parameters:

nodeToStartAt - The AbstractUpdateExtractor.NodeGoal to start parent backward iteration at.

force - true first parent is not checked, false also first parent is checked.

Returns:

The first found parent with at least two open child branches or null if the root has been reached.

countOpenChildren

protected int countOpenChildren(Node node)

Counts the number of open child Nodes.

Parameters:

node - The Node to count its open children.

Returns:

The number of open child Nodes.

computeBranchCondition

protected Term computeBranchCondition(Node node,
                                      java.util.Map<Node,Term> branchConditionCache,
                                      boolean simplifyConditions)
                               throws ProofInputException

Computes the branch condition if not already present in the cache and stores it in the cache. If the condition is already present in the cache it is returned from it.

Parameters:

node - The Node to compute its branch condition.

branchConditionCache - The cache of already computed branch conditions.

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

Returns:

The computed branch condition.

Throws:

ProofInputException - Occurred Exception.