public abstract class AbstractUpdateExtractor
extends java.lang.Object
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) . |
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 and Description |
---|
AbstractUpdateExtractor(Node node,
PosInOccurrence modalityPio)
Constructor.
|
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 Term s. |
protected void |
collectLocationsFromHeapUpdate(Term term,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill)
|
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)
|
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)
|
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
Goal s 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
Node s. |
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.ExtractLocationParameter s. |
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
extractLocationsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
extractLocationsFromTerm(Term term,
java.util.Set<Term> objectsToIgnore)
|
protected void |
fillInitialObjectsToIgnoreRecursively(Term term,
java.util.Set<Term> toFill)
Utility method of
#computeInitialObjectsToIgnore() which
computes the objects to ignore recursively. |
protected Proof |
getProof()
|
protected Node |
getRoot()
Returns the root
Node of the proof. |
protected Services |
getServices()
|
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
IProgramVariable s. |
protected final PosInOccurrence modalityPio
PosInOccurrence
of the modality or its updates.private int preVariableIndex
public AbstractUpdateExtractor(Node node, PosInOccurrence modalityPio)
node
- The Node
of KeY's proof tree to compute memory layouts for.modalityPio
- The PosInOccurrence
of the modality or its updates.protected Term removeImplicitSubTermsFromPathCondition(Term pathCondition)
IProgramVariable
s.pathCondition
- The path condition to check.IProgramVariable
s.protected boolean containsImplicitProgramVariable(Term term)
Term
contains an implicit IProgramVariable
.term
- The Term
to check.true
Term
contains implicit IProgramVariable
, false
Term
contains no implicit IProgramVariable
.protected boolean isImplicitProgramVariable(ProgramVariable var)
ProgramVariable
is implicit.var
- The ProgramVariable
to check.true
ProgramVariable
is implicit, false
ProgramVariable
is not implicit or null
.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.
ignoreExceptionVariable
- Ignore exception variable?ignoreOldStateVariables
- Ignore old state variables?protected void fillInitialObjectsToIgnoreRecursively(Term term, java.util.Set<Term> toFill)
#computeInitialObjectsToIgnore()
which
computes the objects to ignore recursively.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 Term
s 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 Term
s.
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 Set
s updateCreatedObjectsToFill
/
updateValueObjectsToFill
.
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.ProofInputException
- Occurred Exception.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 Term
s 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 Term
s.
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 Set
s updateCreatedObjectsToFill
/
updateValueObjectsToFill
.
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.ProofInputException
- Occurred Exception.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 Term
s 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 Term
s.
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 Set
s updateCreatedObjectsToFill
/
updateValueObjectsToFill
.
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.ProofInputException
- Occurred Exception.protected boolean hasFreeVariables(Term term)
Term
has free variables.term
- The Term
to check.true
has free variables, false
does not have free variables.protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> extractLocationsFromSequent(Sequent sequent, java.util.Set<Term> objectsToIgnore) throws ProofInputException
Sequent
the Term
s 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 Term
s.sequent
- The Sequent
to extract locations from.objectsToIgnore
- The objects to ignore.ProofInputException
- Occurred Exception.protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> extractLocationsFromTerm(Term term, java.util.Set<Term> objectsToIgnore) throws ProofInputException
Term
the Term
s 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 Term
s.term
- The Term
to extract locations from.objectsToIgnore
- The objects to ignore.ProofInputException
- Occurred Exception.protected void collectLocationsFromTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill, Term term, java.util.Set<Term> objectsToIgnore) throws ProofInputException
extractLocationsFromTerm(Term, Set)
which
recursively extracts the locations.toFill
- The result Set
to fill.term
- The current Term
.objectsToIgnore
- The objects to ignore.ProofInputException
- Occurred Exception.protected void collectLocationsFromHeapTerms(Term selectTerm, Term variableTerm, HeapLDT heapLDT, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill, java.util.Set<Term> objectsToIgnore) throws ProofInputException
AbstractUpdateExtractor.ExtractLocationParameter
location from the heap Term
s.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.ProofInputException
- Occurred Exception.protected Term createLocationPredicateAndTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> valueSelectParameter)
Term
which can be used to compute the
values defined by the given AbstractUpdateExtractor.ExtractLocationParameter
s.valueSelectParameter
- The AbstractUpdateExtractor.ExtractLocationParameter
s to compute in the created Term
.Term
which computes the values of the given AbstractUpdateExtractor.ExtractLocationParameter
s.protected Node getRoot()
Node
of the proof.Node
of the proof.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.
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.AbstractUpdateExtractor.ExecutionVariableValuePair
s.ProofInputException
- Occurred Exception.protected java.util.List<Term> collectAdditionalUpdates()
protected ImmutableList<Term> computeOriginalUpdates(PosInOccurrence pio, boolean currentLayout)
pio
- The PosInOccurrence
.currentLayout
- Is current layout?protected java.util.Map<Goal,Term> computeValueConditions(java.util.Set<Goal> valueGoals, java.util.Map<Node,Term> branchConditionCache, boolean simplifyConditions) throws ProofInputException
Goal
s 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:
Goal
s have to be all Goal
s of the side
proof providing the same value. This means that other branches/goals
of the side proof result in different branches.
Node
s starting at the
Goal
s 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 Goal
s will meet at their
common parents.
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 Goal
s
provide different values.
Goal
is the path condition computed.
The path condition is the conjunction over all found branch
conditions contributing to the value.
valueGoals
- All Goal
s 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.Map
which contains for each Goal
the computed path condition consisting of only required splits.ProofInputException
- Occurred Exceptionprotected boolean isParentReachedOnAllChildGoals(Node currentNode, java.util.List<AbstractUpdateExtractor.NodeGoal> branchLeafs)
AbstractUpdateExtractor.NodeGoal
has
reached the given Node
.currentNode
- The current Node
to check.branchLeafs
- The AbstractUpdateExtractor.NodeGoal
on which backward iteration was performed.true
All AbstractUpdateExtractor.NodeGoal
s have passed the given Node
, false
if at least one AbstractUpdateExtractor.NodeGoal
has not passed the given Node
.protected AbstractUpdateExtractor.NodeGoal iterateBackOnParents(AbstractUpdateExtractor.NodeGoal nodeToStartAt, boolean force)
AbstractUpdateExtractor.NodeGoal
until the first parent with at least two open
branches has been found.nodeToStartAt
- The AbstractUpdateExtractor.NodeGoal
to start parent backward iteration at.force
- true
first parent is not checked, false
also first parent is checked.null
if the root has been reached.protected Term computeBranchCondition(Node node, java.util.Map<Node,Term> branchConditionCache, boolean simplifyConditions) throws ProofInputException
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.ProofInputException
- Occurred Exception.