de.uka.ilkd.key.symbolic_execution

Class SymbolicLayoutExtractor

java.lang.Object

de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

de.uka.ilkd.key.symbolic_execution.SymbolicLayoutExtractor

Direct Known Subclasses:

ExecutionNodeSymbolicLayoutExtractor

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:

1. Compute possible equivalence classes which leads to different memory layouts via analyse().
   1. Compute path condition from root to the node for which memory layouts should be build.
   2. Compute locations (values/associations of objects and state) to show later in initial and current memory layouts. Initial locations are extracted from path condition and conditions of node's sequent. Current locations are all initial locations plus locations defined in updates of node's sequent. The location of the exc variable and backup of initial method arguments and the heap of the initial proof obligation are ignored. Objects of updates created during symbolic execution and objects of the right site of updates are also collected.
   3. Compute objects which should be checked for equality (aliasing). The Set consists of objects from path condition, objects on the right side of updates, objects in conditions of node's antecedent and null.
   4. Create a site proof which starts in a modified version of the root node. It contains the given path condition as additional antecedent and the modality with he java code is removed. Cut rules are applied to this sequent for each possible combination of two different objects. Each goal represents a memory layout and the applied cuts in each goal represents the equality classes.
   5. Create a predicate which is used to compute the objects, values and associations of an initial/a current memory layout. Objects are represented as expressions like 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.
2. Compute a concrete initial or current memory layout when they are requested the first time via #lazyComputeLayout(Node, ImmutableSet, Term, Set, ImmutableList, Term, String).
   1. Start side proof based on node's sequent for a current memory layout or root's sequent for an initial memory layout. The sequent is modified by adding the pre updates and on initial memory layouts also the path condition. The equivalence classes are added and the modality is replaced with the predicate to compute objects, values and associations.
   2. Extract values from the predicate.
   3. Create new ISymbolicLayout and fill it with objects, values and associations from the extracted values of the side proof.

Author:

Martin Hentschel

See Also:

ISymbolicLayout, ExecutionNodeSymbolicLayoutExtractor

Nested Class Summary

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 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.

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

modalityPio, node

Constructor Summary

Constructors

Constructor and Description
SymbolicLayoutExtractor(Node node, PosInOccurrence modalityPio, boolean useUnicode, boolean usePrettyPrinting, boolean simplifyConditions) Constructor.

Method Summary

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 ExecutionVariableValuePairs.
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 Terms 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 ISymbolicEquivalenceClasses, because there is no guarantee that the strategy evaluates each aliased location to the same symbolic value.

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

settings

private final IModelSettings settings

The used IModelSettings.

appliedCutsPerLayout

private java.util.List<ImmutableSet<Term>> appliedCutsPerLayout

Contains the applied cuts of each possible memory layout. An applied cut is represented as Term of the from equals(obj1, obj2) or not(equals(obj1, obj2)).

currentLayouts

private java.util.Map<java.lang.Integer,ISymbolicLayout> currentLayouts

Contains the current memory layouts accessible via getCurrentLayout(int).

currentLocations

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

The ExtractLocationParameter instances used to compute a current memory layout.

initialLayouts

private java.util.Map<java.lang.Integer,ISymbolicLayout> initialLayouts

Contains the initial memory layouts accessible via getInitialLayout(int).

initialLocations

private java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> initialLocations

The ExtractLocationParameter instances used to compute an initial memory layout.

layoutsEquivalentClasses

private java.util.Map<java.lang.Integer,ImmutableList<ISymbolicEquivalenceClass>> layoutsEquivalentClasses

Contains the equivalent classes accessible via getEquivalenceClasses(int).

objectsToIgnore

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.

updates

private ImmutableList<Term> updates

The updates to consider.

Constructor Detail

SymbolicLayoutExtractor

public SymbolicLayoutExtractor(Node node,
                               PosInOccurrence modalityPio,
                               boolean useUnicode,
                               boolean usePrettyPrinting,
                               boolean simplifyConditions)

Constructor.

Parameters:

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.

Method Detail

analyse

public void analyse()
             throws ProofInputException

Computes the possible memory layouts.

This is the prerequisite to access equivalence classes, initial and current states.

Throws:

ProofInputException - Occurred Exception.

extractInitialUpdates

protected ImmutableList<Term> extractInitialUpdates()

Computes the initial updates to consider.

Returns:

The initial updates to consider.

sortTerms

protected java.util.Set<Term> sortTerms(java.util.Set<Term> terms)

Sorts the given Terms alphabetically.

Parameters:

terms - The Terms to sort.

Returns:

The sorted Terms.

filterOutObjectsToIgnore

protected java.util.Set<Term> filterOutObjectsToIgnore(java.util.Set<Term> objectsToFilter,
                                                       java.util.Set<Term> objectsToIgnore)
                                                throws ProofInputException

Filters out the objects from the second Set in the first Set.

Parameters:

objectsToFilter - The Set to filter.

objectsToIgnore - The Set with the objects to filter out.

Returns:

A new Set which contains all objects of the first Set which are not contained in the second Set.

Throws:

ProofInputException

createSequentForEquivalenceClassComputation

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.

Returns:

The created Sequent to use for equivalence class computation.

applyCutRules

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.

Parameters:

starter - The ProofStarter which provides the side proof.

symbolicObjects - The symbolic objects to compute equivalence classes for.

updates - The updates to consider.

applyCut

protected void applyCut(ProofStarter starter,
                        Term term,
                        int maxProofSteps)

Applies one single cut rule for the given Term.

Parameters:

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.

extractAppliedCutsFromGoals

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 ImmutableSets. Each Term has the form equals(obj1, obj2) or not(equals(obj1, obj2))

Parameters:

proof - The Proof which provides the Goals to extract memory layouts from.

Returns:

Each entry in the list represents a equivalence class memory layout. For each object pair checked via cut rules application exists one entry in the Set of the form equals(obj1, obj2) or not(equals(obj1, obj2)).

Throws:

ProofInputException - Occurred Exception.

extractAppliedCutsSet

protected ImmutableSet<Term> extractAppliedCutsSet(Node goalnode,
                                                   Node root)
                                            throws ProofInputException

Extracts the applied cut rules in the given Node. Each cut rule is represented as Term of the form equals(obj1, obj2) or not(equals(obj1, obj2)).

Parameters:

goalnode - The current Node.

root - The root Node.

Returns:

The applied cut rules.

Throws:

ProofInputException - Occurred Exception.

isAnalysed

public boolean isAnalysed()

Checks if analyse() was already executed.

Returns:

true analyse() was executed, false analyse() was not executed.

getLayoutsCount

public int getLayoutsCount()

Returns the number of available memory layouts.

Attention: Requires that analyse() was executed.

Returns:

The number of available memory layouts.

getInitialLayout

public ISymbolicLayout getInitialLayout(int layoutIndex)
                                 throws ProofInputException

Returns the initial memory layout at the given index.

Attention: Requires that analyse() was executed.

Parameters:

layoutIndex - The index of the initial memory layout.

Returns:

The initial memory layout at the given index.

Throws:

ProofInputException - Occurred Exception

computeInitialStateName

protected java.lang.String computeInitialStateName()

Computes the state name of an initial memory layout.

Returns:

The state name of an initial memory layout.

getCurrentLayout

public ISymbolicLayout getCurrentLayout(int layoutIndex)
                                 throws ProofInputException

Returns the current memory layout at the given index.

Attention: Requires that analyse() was executed.

Parameters:

layoutIndex - The index of the current memory layout.

Returns:

The current memory layout at the given index.

Throws:

ProofInputException - Occurred Exception

computeCurrentStateName

protected java.lang.String computeCurrentStateName()

Computes the state name of a current memory layout.

Returns:

The state name of a current memory layout.

getLayout

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

Helper method of getInitialLayout(int) and getCurrentLayout(int) to lazily compute and get a memory layout.

Parameters:

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.

Returns:

The lazily computed memory layout.

Throws:

ProofInputException - Occurred Exception.

lazyComputeLayout

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.

Parameters:

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.

Returns:

The created memory layout.

Throws:

ProofInputException - Occurred Exception.

updateLocationsAccordingtoEquivalentClass

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 ISymbolicEquivalenceClasses, because there is no guarantee that the strategy evaluates each aliased location to the same symbolic value.

Parameters:

locations - The available ExtractLocationParameters.

equivalentClasses - The available ISymbolicEquivalenceClasses.

Returns:

The updated ExtractLocationParameters.

collectObjectsFromSequent

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

Collects all objects which are used in the conditions of the Sequent.

Parameters:

sequent - The Sequent which provides the conditions to collect objects from.

objectsToIgnore - Objects which should be excluded in the result.

Returns:

The found objects.

Throws:

ProofInputException - Occurred Exception.

collectSymbolicObjectsFromTerm

protected java.util.Set<Term> collectSymbolicObjectsFromTerm(Term term,
                                                             java.util.Set<Term> objectsToIgnore)
                                                      throws ProofInputException

Collects all objects which are used in the given Term.

Parameters:

term - The Term to collect objects in.

objectsToIgnore - Objects which should be excluded in the result.

Returns:

The found objects.

Throws:

ProofInputException - Occurred Exception.

getEquivalenceClasses

public ImmutableList<ISymbolicEquivalenceClass> getEquivalenceClasses(int layoutIndex)

Returns the equivalence class of the memory layout defined by the index.

Attention: Requires that analyse() was executed.

Parameters:

layoutIndex - The index of the memory layout to get its equivalence classes.

Returns:

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

lazyComputeEquivalenzClasses

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.

Parameters:

appliedCuts - The applied cut rules.

Returns:

The created ISymbolicEquivalenceClass instances.

findEquivalentClass

protected ISymbolicEquivalenceClass findEquivalentClass(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
                                                        Term term)

Searches the ISymbolicEquivalenceClass from the given one which contains the given Term.

Parameters:

equivalentClasses - The available ISymbolicEquivalenceClass to search in.

term - The Term to search.

Returns:

The found ISymbolicEquivalenceClass which contains the given Term or null if no one was found.

createLayoutFromExecutionVariableValuePairs

protected ISymbolicLayout createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
                                                                      java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
                                                                      java.lang.String stateName)
                                                               throws ProofInputException

Creates an ISymbolicLayout which shows the objects, values and associations defined by the given ExecutionVariableValuePairs.

Parameters:

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.

Returns:

The created ISymbolicLayout with the given content.

Throws:

ProofInputException - Occurred Exception.

createObjectForTerm

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.

Parameters:

objects - The already available SymbolicObjects.

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.