public class SymbolicLayoutExtractor extends AbstractUpdateExtractor
Instances of this class can be used to compute memory layouts
(objects with values and associations to other objects on the heap together
with objects and associations to objects on the current state of the stack)
which a given Node
of KeY's proof tree can have based on
equivalence classes (aliasing) of objects.
Such memory layouts are named current memory layouts. It is also possible
to compute how the heap and stack was when the proof was started. Such
memory layouts are named initial memory layouts.
Example program:
public class Example {
private int value;
private Example next;
public static int main(Example e) {
e.value = 1;
e.next.value = 2;
return e.value + e.next.value; // Current node in KeY's proof tree
}
}
If the symbolic execution stops at the return statement,
two memory layouts are possible. In the first case refers
e
and e.next
to different objects (result is 3
).
In the second case refers both to the same object (result is 4
).
That both objects can't be null
is ensured by the path condition from root to the current node in KeY's proof tree.
The following code snippet shows how to use this class:
SymbolicLayoutExtractor e = new SymbolicLayoutExtractor(node);
e.analyse();
for (int i = 0; i < e.getLayoutsCount(); i++) {
ImmutableList<ISymbolicEquivalenceClass> equivalenceClasses = e.getEquivalenceClasses(i);
ISymbolicLayout initial = e.getInitialLayout(i);
ISymbolicLayout current = e.getCurrentLayout(i);
}
Rough description of the implemented algorithm:
analyse()
.
e
or e.next
. The problem is that in a current memory layout the
object structure might have changed and e.next
is a different object compared to the initial memory layout.
To solve this issue is an additional update is used which stores each object in a temporary program variable, e.g.
pre0 = e
, pre1 = e.next
. This makes sure that the objects are the same in initial and current memory layouts.
#lazyComputeLayout(Node, ImmutableSet, Term, Set, ImmutableList, Term, String)
.
ISymbolicLayout
and fill it with objects, values and associations from the extracted values of the side proof.
ISymbolicLayout
,
ExecutionNodeSymbolicLayoutExtractor
AbstractUpdateExtractor.ExecutionVariableValuePair, AbstractUpdateExtractor.ExtractLocationParameter, AbstractUpdateExtractor.NodeGoal
Modifier and Type | Field and Description |
---|---|
private java.util.List<ImmutableSet<Term>> |
appliedCutsPerLayout
Contains the applied cuts of each possible memory layout.
|
private java.util.Map<java.lang.Integer,ISymbolicLayout> |
currentLayouts
Contains the current memory layouts accessible via
getCurrentLayout(int) . |
private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
currentLocations
The
ExtractLocationParameter instances used to compute a current memory layout. |
private java.util.Map<java.lang.Integer,ISymbolicLayout> |
initialLayouts
Contains the initial memory layouts accessible via
getInitialLayout(int) . |
private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
initialLocations
The
ExtractLocationParameter instances used to compute an initial memory layout. |
private java.util.Map<java.lang.Integer,ImmutableList<ISymbolicEquivalenceClass>> |
layoutsEquivalentClasses
Contains the equivalent classes accessible via
getEquivalenceClasses(int) . |
private java.util.Set<Term> |
objectsToIgnore
Contains objects which should be ignored in the state because they
are created during symbolic execution or part of the proof obligation.
|
private IModelSettings |
settings
The used
IModelSettings . |
private ImmutableList<Term> |
updates
The updates to consider.
|
modalityPio, node
Constructor and Description |
---|
SymbolicLayoutExtractor(Node node,
PosInOccurrence modalityPio,
boolean useUnicode,
boolean usePrettyPrinting,
boolean simplifyConditions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
analyse()
Computes the possible memory layouts.
|
protected void |
applyCut(ProofStarter starter,
Term term,
int maxProofSteps)
Applies one single cut rule for the given
Term . |
protected void |
applyCutRules(ProofStarter starter,
java.util.Set<Term> symbolicObjects,
ImmutableList<Term> updates)
Applies cut rules to the given side proofs to compute equivalence classes.
|
protected java.util.Set<Term> |
collectObjectsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
Collects all objects which are used in the conditions of the
Sequent . |
protected java.util.Set<Term> |
collectSymbolicObjectsFromTerm(Term term,
java.util.Set<Term> objectsToIgnore)
Collects all objects which are used in the given
Term . |
protected java.lang.String |
computeCurrentStateName()
Computes the state name of a current memory layout.
|
protected java.lang.String |
computeInitialStateName()
Computes the state name of an initial memory layout.
|
protected ISymbolicLayout |
createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.lang.String stateName)
Creates an
ISymbolicLayout which shows the objects,
values and associations defined by the given ExecutionVariableValuePair s. |
protected void |
createObjectForTerm(java.util.Map<Term,SymbolicObject> objects,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
SymbolicLayout result,
Term objectTerm)
Creates for the object defined by the given
Term an SymbolicObject instance if not already available. |
protected Sequent |
createSequentForEquivalenceClassComputation()
Creates a
Sequent which is used to compute equivalence classes. |
protected java.util.List<ImmutableSet<Term>> |
extractAppliedCutsFromGoals(Proof proof)
Extracts the possible memory layouts from the given side proof.
|
protected ImmutableSet<Term> |
extractAppliedCutsSet(Node goalnode,
Node root)
Extracts the applied cut rules in the given
Node . |
protected ImmutableList<Term> |
extractInitialUpdates()
Computes the initial updates to consider.
|
protected java.util.Set<Term> |
filterOutObjectsToIgnore(java.util.Set<Term> objectsToFilter,
java.util.Set<Term> objectsToIgnore)
Filters out the objects from the second
Set in the first Set . |
protected ISymbolicEquivalenceClass |
findEquivalentClass(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
Term term)
Searches the
ISymbolicEquivalenceClass from the given one
which contains the given Term . |
ISymbolicLayout |
getCurrentLayout(int layoutIndex)
Returns the current memory layout at the given index.
|
ImmutableList<ISymbolicEquivalenceClass> |
getEquivalenceClasses(int layoutIndex)
Returns the equivalence class of the memory layout defined by the index.
|
ISymbolicLayout |
getInitialLayout(int layoutIndex)
Returns the initial memory layout at the given index.
|
protected ISymbolicLayout |
getLayout(java.util.Map<java.lang.Integer,ISymbolicLayout> confiurationsMap,
int layoutIndex,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
java.lang.String stateName,
boolean currentLayout)
Helper method of
getInitialLayout(int) and
getCurrentLayout(int) to lazily compute and get a memory layout. |
int |
getLayoutsCount()
Returns the number of available memory layouts.
|
boolean |
isAnalysed()
Checks if
analyse() was already executed. |
protected ImmutableList<ISymbolicEquivalenceClass> |
lazyComputeEquivalenzClasses(ImmutableSet<Term> appliedCuts)
Computes the equivalence classes from the given applied cut rules
lazily when
getEquivalenceClasses(int) is called the first time. |
protected ISymbolicLayout |
lazyComputeLayout(ImmutableSet<Term> layout,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.lang.String stateName,
boolean currentLayout)
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean) . |
protected java.util.Set<Term> |
sortTerms(java.util.Set<Term> terms)
Sorts the given
Term s alphabetically. |
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
updateLocationsAccordingtoEquivalentClass(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses)
Replaces the parent of each
ExtractLocationParameter according
to the ISymbolicEquivalenceClass es, because there is no guarantee
that the strategy evaluates each aliased location to the same symbolic value. |
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
private final IModelSettings settings
IModelSettings
.private java.util.List<ImmutableSet<Term>> appliedCutsPerLayout
Term
of the from
equals(obj1, obj2)
or not(equals(obj1, obj2))
.private java.util.Map<java.lang.Integer,ISymbolicLayout> currentLayouts
getCurrentLayout(int)
.private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> currentLocations
ExtractLocationParameter
instances used to compute a current memory layout.private java.util.Map<java.lang.Integer,ISymbolicLayout> initialLayouts
getInitialLayout(int)
.private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> initialLocations
ExtractLocationParameter
instances used to compute an initial memory layout.private java.util.Map<java.lang.Integer,ImmutableList<ISymbolicEquivalenceClass>> layoutsEquivalentClasses
getEquivalenceClasses(int)
.private java.util.Set<Term> objectsToIgnore
private ImmutableList<Term> updates
public SymbolicLayoutExtractor(Node node, PosInOccurrence modalityPio, boolean useUnicode, boolean usePrettyPrinting, boolean simplifyConditions)
node
- The Node
of KeY's proof tree to compute memory layouts for.modalityPio
- The PosInOccurrence
of the modality or its updates.useUnicode
- true
use unicode characters, false
do not use unicode characters.usePrettyPrinting
- true
use pretty printing, false
do not use pretty printing.simplifyConditions
- true
simplify conditions, false
do not simplify conditions.public void analyse() throws ProofInputException
Computes the possible memory layouts.
This is the prerequisite to access equivalence classes, initial and current states.
ProofInputException
- Occurred Exception.protected ImmutableList<Term> extractInitialUpdates()
protected java.util.Set<Term> sortTerms(java.util.Set<Term> terms)
Term
s alphabetically.protected java.util.Set<Term> filterOutObjectsToIgnore(java.util.Set<Term> objectsToFilter, java.util.Set<Term> objectsToIgnore) throws ProofInputException
Set
in the first Set
.objectsToFilter
- The Set
to filter.objectsToIgnore
- The Set
with the objects to filter out.Set
which contains all objects of the first Set
which are not contained in the second Set
.ProofInputException
protected Sequent createSequentForEquivalenceClassComputation()
Creates a Sequent
which is used to compute equivalence classes.
The created Sequent
is the Sequent
of AbstractUpdateExtractor.node
without the modality.
Sequent
to use for equivalence class computation.protected void applyCutRules(ProofStarter starter, java.util.Set<Term> symbolicObjects, ImmutableList<Term> updates)
Applies cut rules to the given side proofs to compute equivalence classes.
For each possible combination (without identity and ignoring the order) of the given objects is one cut performed.
starter
- The ProofStarter
which provides the side proof.symbolicObjects
- The symbolic objects to compute equivalence classes for.updates
- The updates to consider.protected void applyCut(ProofStarter starter, Term term, int maxProofSteps)
Term
.starter
- The ProofStarter
to apply cut rule in.term
- The Term
to cut out.maxProofSteps
- The maximal number of proof steps applied after cut via auto mode.protected java.util.List<ImmutableSet<Term>> extractAppliedCutsFromGoals(Proof proof) throws ProofInputException
Extracts the possible memory layouts from the given side proof.
Each open Goal
of the proof results in its own memory layout.
The applied cuts per memory layout are represented as Term
stored in the ImmutableSet
s. Each Term
has the form
equals(obj1, obj2)
or not(equals(obj1, obj2))
proof
- The Proof
which provides the Goal
s to extract memory layouts from.Set
of the form equals(obj1, obj2)
or not(equals(obj1, obj2))
.ProofInputException
- Occurred Exception.protected ImmutableSet<Term> extractAppliedCutsSet(Node goalnode, Node root) throws ProofInputException
Node
. Each cut
rule is represented as Term
of the form equals(obj1, obj2)
or not(equals(obj1, obj2))
.goalnode
- The current Node
.root
- The root Node
.ProofInputException
- Occurred Exception.public boolean isAnalysed()
analyse()
was already executed.public int getLayoutsCount()
Returns the number of available memory layouts.
Attention: Requires that analyse()
was executed.
public ISymbolicLayout getInitialLayout(int layoutIndex) throws ProofInputException
Returns the initial memory layout at the given index.
Attention: Requires that analyse()
was executed.
layoutIndex
- The index of the initial memory layout.ProofInputException
- Occurred Exceptionprotected java.lang.String computeInitialStateName()
public ISymbolicLayout getCurrentLayout(int layoutIndex) throws ProofInputException
Returns the current memory layout at the given index.
Attention: Requires that analyse()
was executed.
layoutIndex
- The index of the current memory layout.ProofInputException
- Occurred Exceptionprotected java.lang.String computeCurrentStateName()
protected ISymbolicLayout getLayout(java.util.Map<java.lang.Integer,ISymbolicLayout> confiurationsMap, int layoutIndex, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations, java.lang.String stateName, boolean currentLayout) throws ProofInputException
getInitialLayout(int)
and
getCurrentLayout(int)
to lazily compute and get a memory layout.confiurationsMap
- The map which contains already computed memory layouts.layoutIndex
- The index of the memory layout to lazily compute and return.locations
- The locations to compute in side proof.stateName
- The name of the state.currentLayout
- true
current layout, false
initial layout.ProofInputException
- Occurred Exception.protected ISymbolicLayout lazyComputeLayout(ImmutableSet<Term> layout, java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations, ImmutableList<ISymbolicEquivalenceClass> equivalentClasses, java.lang.String stateName, boolean currentLayout) throws ProofInputException
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean)
.
Finally, the last step is to create the ISymbolicLayout
instance
and to fill it with the values/associations defined by ExecutionVariableValuePair
instances.
layout
- The memory layout terms.locations
- The locations to compute in side proof.equivalentClasses
- The equivalence classes defined by the memory layout terms.stateName
- The name of the state.currentLayout
- true
current layout, false
initial layout.ProofInputException
- Occurred Exception.protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> updateLocationsAccordingtoEquivalentClass(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations, ImmutableList<ISymbolicEquivalenceClass> equivalentClasses)
ExtractLocationParameter
according
to the ISymbolicEquivalenceClass
es, because there is no guarantee
that the strategy evaluates each aliased location to the same symbolic value.locations
- The available ExtractLocationParameter
s.equivalentClasses
- The available ISymbolicEquivalenceClass
es.ExtractLocationParameter
s.protected java.util.Set<Term> collectObjectsFromSequent(Sequent sequent, java.util.Set<Term> objectsToIgnore) throws ProofInputException
Sequent
.sequent
- The Sequent
which provides the conditions to collect objects from.objectsToIgnore
- Objects which should be excluded in the result.ProofInputException
- Occurred Exception.protected java.util.Set<Term> collectSymbolicObjectsFromTerm(Term term, java.util.Set<Term> objectsToIgnore) throws ProofInputException
Term
.term
- The Term
to collect objects in.objectsToIgnore
- Objects which should be excluded in the result.ProofInputException
- Occurred Exception.public ImmutableList<ISymbolicEquivalenceClass> getEquivalenceClasses(int layoutIndex)
Returns the equivalence class of the memory layout defined by the index.
Attention: Requires that analyse()
was executed.
layoutIndex
- The index of the memory layout to get its equivalence classes.protected ImmutableList<ISymbolicEquivalenceClass> lazyComputeEquivalenzClasses(ImmutableSet<Term> appliedCuts)
Computes the equivalence classes from the given applied cut rules
lazily when getEquivalenceClasses(int)
is called the first time.
Each entry in the given ImmutableSet
is of the form
equals(obj1, obj2)
or not(equals(obj1, obj2))
.
An ISymbolicEquivalenceClass
is only created for objects which
are equal. Objects which are equal to no other one are not represented
in an ISymbolicEquivalenceClass
. This makes sure that each
ISymbolicEquivalenceClass
contains at least two objects and
that the result is empty if all objects are not equal to each other.
appliedCuts
- The applied cut rules.ISymbolicEquivalenceClass
instances.protected ISymbolicEquivalenceClass findEquivalentClass(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses, Term term)
ISymbolicEquivalenceClass
from the given one
which contains the given Term
.equivalentClasses
- The available ISymbolicEquivalenceClass
to search in.term
- The Term
to search.ISymbolicEquivalenceClass
which contains the given Term
or null
if no one was found.protected ISymbolicLayout createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses, java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.lang.String stateName) throws ProofInputException
ISymbolicLayout
which shows the objects,
values and associations defined by the given ExecutionVariableValuePair
s.equivalentClasses
- The used ISymbolicEquivalenceClass
instances of the memory layout.pairs
- Provides the available objects, their values and associations together with the variables and association of the state.stateName
- The name of the state.ISymbolicLayout
with the given content.ProofInputException
- Occurred Exception.protected void createObjectForTerm(java.util.Map<Term,SymbolicObject> objects, ImmutableList<ISymbolicEquivalenceClass> equivalentClasses, SymbolicLayout result, Term objectTerm)
Term
an SymbolicObject
instance if not already available.objects
- The already available SymbolicObject
s.equivalentClasses
- The available ISymbolicEquivalenceClass
.result
- The SymbolicLayout
to add the SymbolicObject
to.objectTerm
- The Term
which represents the Object
a SymbolicObject
should be created for.