de.uka.ilkd.key.symbolic_execution.slicing

Class AbstractSlicer

java.lang.Object

de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer

Direct Known Subclasses:

AbstractBackwardSlicer

public abstract class AbstractSlicer
extends java.lang.Object

Defines the basic functionality for slicing algorithms.

Author:

Martin Hentschel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected static class	AbstractSlicer.SequentInfo The result returned by AbstractSlicer#analyzeSequent(Node).

Constructor Summary

Constructors

Constructor and Description
AbstractSlicer()

Method Summary

Modifier and Type	Method and Description
protected void	analyzeEquality(Services services, Term equality, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference) Analyzes the given equality Term for aliased locations.
protected void	analyzeEquivalenceClasses(Services services, ImmutableList<ISymbolicEquivalenceClass> sec, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference) Analyzes the gievn ISymbolicEquivalenceClasses.
protected void	analyzeHeapUpdate(Term term, Services services, HeapLDT heapLDT, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference) Recursive utility method used by #analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update.
protected AbstractSlicer.SequentInfo	analyzeSequent(Node node, ImmutableList<ISymbolicEquivalenceClass> sec) Computes the aliases specified by the updates of the current Node at the application PosInOccurrence and computes the current this reference.
protected void	analyzeSequent(Services services, Sequent sequent, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference) Analyzes the given Sequent for equalities specified by top level formulas.
protected void	analyzeUpdate(Term term, Services services, HeapLDT heapLDT, java.util.Map<Location,java.util.SortedSet<Location>> aliases, java.util.Map<ProgramVariable,Term> localValues, ExecutionContext ec, ReferencePrefix thisReference) Recursive utility method used by #analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update.
protected void	analyzeUpdates(ImmutableList<Term> updates, Services services, HeapLDT heapLDT, java.util.Map<Location,java.util.SortedSet<Location>> aliases, java.util.Map<ProgramVariable,Term> localValues, ExecutionContext ec, ReferencePrefix thisReference) Utility method used by #analyzeSequent(Node) to analyze the given updates.
static <T> int	computeFirstCommonPrefixLength(ImmutableList<ImmutableList<T>> candidates, ImmutableList<T> toCheck) Computes the length of a common prefix.
protected Location	computeRepresentativeAlias(Location location, java.util.Map<Location,java.util.SortedSet<Location>> aliases) Computes the representative alias of the given Location.
protected java.util.SortedSet<Location>	createSortedSet() Creates a SortedSet which ensures that the elements are sorted.
protected abstract ImmutableArray<Node>	doSlicing(Node seedNode, Location seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) Performs the slicing.
protected Location	findNewAlternative(java.util.SortedSet<Location> oldAlternatives, java.util.SortedSet<Location> newAlternatives) Returns the first found alternative which is still valid.
protected void	listModifiedHeapLocations(Term term, Services services, HeapLDT heapLDT, java.util.List<Location> listToFill, ReferencePrefix thisReference, java.util.Set<Location> relevantLocations, Node node) Recursive utility method used by #listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update.
protected void	listModifiedLocations(Term term, Services services, HeapLDT heapLDT, java.util.List<Location> listToFill, ExecutionContext ec, ReferencePrefix thisReference, java.util.Set<Location> relevantLocations, Node node) Recursive method to list all modified Locations in the given Term.
protected Location	normalizeAlias(Services services, Location location, AbstractSlicer.SequentInfo info) Returns the representative alias for the given Location.
protected Location	normalizeAlias(Services services, ReferencePrefix referencePrefix, AbstractSlicer.SequentInfo info) Returns the representative alias for the given ReferencePrefix.
protected Access	normalizeArrayIndex(Access access, AbstractSlicer.SequentInfo info) Normalizes the given array index.
protected boolean	performRemoveRelevant(Services services, Location normalized, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info) Checks if the given Location is directly or indirectly contained (aliased) in the Set of relevant locations.
protected boolean	removeRelevant(Services services, Location location, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info) Checks if the given Location is directly or indirectly contained (aliased) in the Set of relevant locations.
protected boolean	removeRelevant(Services services, ReferencePrefix sourceElement, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info) Checks if the given SourceElement is directly or indirectly contained (aliased) in the Set of relevant locations.
ImmutableArray<Node>	slice(Node seedNode, Location seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) Computes the slice.
ImmutableArray<Node>	slice(Node seedNode, ReferencePrefix seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) Computes the slice.
ImmutableArray<Node>	slice(Node seedNode, Term term, ImmutableList<ISymbolicEquivalenceClass> sec) Computes the slice.
static <T> boolean	startsWith(ImmutableList<T> list, ImmutableList<T> prefix) Checks if the given ImmutableList starts with the given prefix.
protected Location	toLocation(Services services, ReferencePrefix prefix, ExecutionContext ec, ReferencePrefix thisReference) Converts the given ReferencePrefix into a Location.
static Location	toLocation(Services services, Term term) Converts the given Term into a Location.
protected ImmutableList<Access>	toLocationRecursive(Services services, ReferencePrefix prefix, ExecutionContext ec, ReferencePrefix thisReference, ImmutableList<Access> children) Utility method used by #toLocation(Services, ReferencePrefix, ReferencePrefix) to recursively extract the Access instances.
protected ReferencePrefix	toReferencePrefix(SourceElement sourceElement) Computes the ReferencePrefix of the given SourceElement.
static Term	toTerm(Services services, Expression expression, ExecutionContext ec) Converts the given Expression into a Term.
static ImmutableArray<Term>	toTerm(Services services, ImmutableArray<Expression> expressions, ExecutionContext ec) Converts the given Expressions into Terms.
protected void	updateAliases(Services services, Location first, Location second, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference) Adds the found alias consisting of first and second ReferencePrefix to the alias Map.

Methods inherited from class java.lang.Object

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

Constructor Detail

AbstractSlicer

public AbstractSlicer()

Method Detail

slice

public ImmutableArray<Node> slice(Node seedNode,
                                  Term term,
                                  ImmutableList<ISymbolicEquivalenceClass> sec)
                           throws ProofInputException

Computes the slice.

Parameters:

seedNode - The seed Node to start slicing at.

term - The seed Term.

sec - The optional ISymbolicEquivalenceClasses to consider.

Returns:

The computed slice.

Throws:

ProofInputException

slice

public ImmutableArray<Node> slice(Node seedNode,
                                  ReferencePrefix seedLocation,
                                  ImmutableList<ISymbolicEquivalenceClass> sec)
                           throws ProofInputException

Computes the slice.

Parameters:

seedNode - The seed Node to start slicing at.

seedLocation - The seed ReferencePrefix.

sec - The optional ISymbolicEquivalenceClasses to consider.

Returns:

The computed slice.

Throws:

ProofInputException

slice

public ImmutableArray<Node> slice(Node seedNode,
                                  Location seedLocation,
                                  ImmutableList<ISymbolicEquivalenceClass> sec)
                           throws ProofInputException

Computes the slice.

Parameters:

seedNode - The seed Node to start slicing at.

seedLocation - The seed ReferencePrefix.

sec - The optional ISymbolicEquivalenceClasses to consider.

Returns:

The computed slice.

Throws:

ProofInputException

doSlicing

protected abstract ImmutableArray<Node> doSlicing(Node seedNode,
                                                  Location seedLocation,
                                                  ImmutableList<ISymbolicEquivalenceClass> sec)
                                           throws ProofInputException

Performs the slicing.

Parameters:

seedNode - The seed Node to start slicing at.

seedLocation - The seed Location.

sec - The optional ISymbolicEquivalenceClasses to consider.

Returns:

The computed slice.

Throws:

ProofInputException

analyzeSequent

protected AbstractSlicer.SequentInfo analyzeSequent(Node node,
                                                    ImmutableList<ISymbolicEquivalenceClass> sec)

Computes the aliases specified by the updates of the current Node at the application PosInOccurrence and computes the current this reference.

Parameters:

node - The Node to analyze.

Returns:

The computed AbstractSlicer.SequentInfo or null if the Node is not supported.

analyzeEquivalenceClasses

protected void analyzeEquivalenceClasses(Services services,
                                         ImmutableList<ISymbolicEquivalenceClass> sec,
                                         java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                                         ReferencePrefix thisReference)

Analyzes the gievn ISymbolicEquivalenceClasses.

Parameters:

services - The Services to use.

sec - The ISymbolicEquivalenceClass to analyze.

aliases - The alias Map to fill.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

analyzeSequent

protected void analyzeSequent(Services services,
                              Sequent sequent,
                              java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                              ReferencePrefix thisReference)

Analyzes the given Sequent for equalities specified by top level formulas.

Parameters:

services - The Services to use.

sequent - The Sequent to analyze.

aliases - The alias Map to fill.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

analyzeEquality

protected void analyzeEquality(Services services,
                               Term equality,
                               java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                               ReferencePrefix thisReference)

Analyzes the given equality Term for aliased locations.

Parameters:

services - The Services to use.

equality - The equality Term to analyze.

aliases - The alias Map to fill.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

analyzeUpdates

protected void analyzeUpdates(ImmutableList<Term> updates,
                              Services services,
                              HeapLDT heapLDT,
                              java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                              java.util.Map<ProgramVariable,Term> localValues,
                              ExecutionContext ec,
                              ReferencePrefix thisReference)

Utility method used by #analyzeSequent(Node) to analyze the given updates.

Parameters:

updates - The update Terms to analyze.

services - The Services to use.

heapLDT - The HeapLDT of the Services.

aliases - The alias Map to fill.

localValues - The local values to fill.

ec - The current ExecutionContext.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

analyzeUpdate

protected void analyzeUpdate(Term term,
                             Services services,
                             HeapLDT heapLDT,
                             java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                             java.util.Map<ProgramVariable,Term> localValues,
                             ExecutionContext ec,
                             ReferencePrefix thisReference)

Recursive utility method used by #analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update.

Parameters:

term - The update Term to analyze.

services - The Services to use.

heapLDT - The HeapLDT of the Services.

aliases - The alias Map to fill.

localValues - The local values to fill.

ec - The current ExecutionContext.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

analyzeHeapUpdate

protected void analyzeHeapUpdate(Term term,
                                 Services services,
                                 HeapLDT heapLDT,
                                 java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                                 ReferencePrefix thisReference)

Recursive utility method used by #analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update.

Parameters:

term - The heap update Term to analyze.

services - The Services to use.

heapLDT - The HeapLDT of the Services.

aliases - The alias Map to fill.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

listModifiedLocations

protected void listModifiedLocations(Term term,
                                     Services services,
                                     HeapLDT heapLDT,
                                     java.util.List<Location> listToFill,
                                     ExecutionContext ec,
                                     ReferencePrefix thisReference,
                                     java.util.Set<Location> relevantLocations,
                                     Node node)
                              throws ProofInputException

Recursive method to list all modified Locations in the given Term.

Parameters:

term - The update Term to analyze.

services - The Services to use.

heapLDT - The HeapLDT of the Services.

listToFill - The result List with Locations to fill.

ec - The current ExecutionContext.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

Throws:

ProofInputException

listModifiedHeapLocations

protected void listModifiedHeapLocations(Term term,
                                         Services services,
                                         HeapLDT heapLDT,
                                         java.util.List<Location> listToFill,
                                         ReferencePrefix thisReference,
                                         java.util.Set<Location> relevantLocations,
                                         Node node)
                                  throws ProofInputException

Recursive utility method used by #listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update.

Parameters:

term - The heap update Term to analyze.

services - The Services to use.

heapLDT - The HeapLDT of the Services.

listToFill - The result List with Locations to fill.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

Throws:

ProofInputException

updateAliases

protected void updateAliases(Services services,
                             Location first,
                             Location second,
                             java.util.Map<Location,java.util.SortedSet<Location>> aliases,
                             ReferencePrefix thisReference)

Adds the found alias consisting of first and second ReferencePrefix to the alias Map. If required, all participating entries in the Map are updated to ensure consistency.

Parameters:

services - The Services to use.

first - The first alias.

second - The second alias.

aliases - The alias Map to update.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

createSortedSet

protected java.util.SortedSet<Location> createSortedSet()

Creates a SortedSet which ensures that the elements are sorted.

Returns:

The new created SortedSet.

normalizeAlias

protected Location normalizeAlias(Services services,
                                  ReferencePrefix referencePrefix,
                                  AbstractSlicer.SequentInfo info)

Returns the representative alias for the given ReferencePrefix.

Parameters:

services - The Services to use.

referencePrefix - The ReferencePrefix.

info - The AbstractSlicer.SequentInfo with the aliases and so on.

Returns:

The representative alias.

normalizeAlias

protected Location normalizeAlias(Services services,
                                  Location location,
                                  AbstractSlicer.SequentInfo info)

Returns the representative alias for the given Location.

Parameters:

services - The Services to use.

location - The Location.

info - The AbstractSlicer.SequentInfo with the aliases and so on.

Returns:

The representative alias.

normalizeArrayIndex

protected Access normalizeArrayIndex(Access access,
                                     AbstractSlicer.SequentInfo info)

Normalizes the given array index.

Parameters:

access - The Access representing an array index.

info - The AbstractSlicer.SequentInfo with the aliases and so on.

Returns:

The normalized array access.

computeRepresentativeAlias

protected Location computeRepresentativeAlias(Location location,
                                              java.util.Map<Location,java.util.SortedSet<Location>> aliases)

Computes the representative alias of the given Location.

Parameters:

location - The given Location.

aliases - The available aliases.

Returns:

The representative alias.

toReferencePrefix

protected ReferencePrefix toReferencePrefix(SourceElement sourceElement)

Computes the ReferencePrefix of the given SourceElement.

Parameters:

sourceElement - The SourceElement to work with.

Returns:

The ReferencePrefix or null if the SourceElement can't be represented as ReferencePrefix.

removeRelevant

protected boolean removeRelevant(Services services,
                                 ReferencePrefix sourceElement,
                                 java.util.Set<Location> relevantLocations,
                                 AbstractSlicer.SequentInfo info)

Checks if the given SourceElement is directly or indirectly contained (aliased) in the Set of relevant locations. If it is contained, the element will be removed.

Parameters:

services - The Services to use.

sourceElement - The SourceElement to check.

relevantLocations - The Set with locations of interest.

info - The AbstractSlicer.SequentInfo with the aliases and so on.

Returns:

true is relevant and was removed, false is not relevant and nothing has changed.

removeRelevant

protected boolean removeRelevant(Services services,
                                 Location location,
                                 java.util.Set<Location> relevantLocations,
                                 AbstractSlicer.SequentInfo info)

Checks if the given Location is directly or indirectly contained (aliased) in the Set of relevant locations. If it is contained, the element will be removed.

Parameters:

services - The Services to use.

location - The Location to check.

relevantLocations - The Set with locations of interest.

info - The AbstractSlicer.SequentInfo with the aliases and so on.

Returns:

true is relevant and was removed, false is not relevant and nothing has changed.

performRemoveRelevant

protected boolean performRemoveRelevant(Services services,
                                        Location normalized,
                                        java.util.Set<Location> relevantLocations,
                                        AbstractSlicer.SequentInfo info)

Checks if the given Location is directly or indirectly contained (aliased) in the Set of relevant locations. If it is contained, the element will be removed.

Parameters:

services - The Services to use.

normalized - The Location to check.

relevantLocations - The Set with locations of interest.

info - The AbstractSlicer.SequentInfo with the aliases and so on.

Returns:

true is relevant and was removed, false is not relevant and nothing has changed.

toLocation

protected Location toLocation(Services services,
                              ReferencePrefix prefix,
                              ExecutionContext ec,
                              ReferencePrefix thisReference)

Converts the given ReferencePrefix into a Location.

Parameters:

services - The Services to use.

prefix - The ReferencePrefix to convert.

ec - The current ExecutionContext.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

Returns:

The Location representing the given ReferencePrefix.

toLocationRecursive

protected ImmutableList<Access> toLocationRecursive(Services services,
                                                    ReferencePrefix prefix,
                                                    ExecutionContext ec,
                                                    ReferencePrefix thisReference,
                                                    ImmutableList<Access> children)

Utility method used by #toLocation(Services, ReferencePrefix, ReferencePrefix) to recursively extract the Access instances.

Parameters:

services - The Services to use.

prefix - The ReferencePrefix to work with.

ec - The current ExecutionContext.

thisReference - The ReferencePrefix which is represented by this (ThisReference).

children - The already known child Accesss.

Returns:

An ImmutableList containing all Accesss of the ReferencePrefix in the order of access.

toTerm

public static ImmutableArray<Term> toTerm(Services services,
                                          ImmutableArray<Expression> expressions,
                                          ExecutionContext ec)

Converts the given Expressions into Terms.

Parameters:

services - The Services to use.

expressions - The Expressions to convert.

ec - The current ExecutionContext.

Returns:

The created Terms.

toTerm

public static Term toTerm(Services services,
                          Expression expression,
                          ExecutionContext ec)

Converts the given Expression into a Term.

Parameters:

services - The Services to use.

expression - The Expression to convert.

ec - The current ExecutionContext.

Returns:

The created Term.

toLocation

public static Location toLocation(Services services,
                                  Term term)

Converts the given Term into a Location.

Parameters:

services - The Services to use.

term - The Term to convert.

Returns:

The Location or null if the Term could not be represented as Location.

findNewAlternative

protected Location findNewAlternative(java.util.SortedSet<Location> oldAlternatives,
                                      java.util.SortedSet<Location> newAlternatives)

Returns the first found alternative which is still valid.

Parameters:

oldAlternatives - The old alternatives.

newAlternatives - The new alternatives.

Returns:

The found alternative or null if not available.

computeFirstCommonPrefixLength

public static <T> int computeFirstCommonPrefixLength(ImmutableList<ImmutableList<T>> candidates,
                                                     ImmutableList<T> toCheck)

Computes the length of a common prefix.

Parameters:

candidates - The possible candidates.

toCheck - The ImmutableList to check.

Returns:

The common prefix length which is 0 if no elements are common.

startsWith

public static <T> boolean startsWith(ImmutableList<T> list,
                                     ImmutableList<T> prefix)

Checks if the given ImmutableList starts with the given prefix.

Parameters:

list - The List to check.

prefix - The prefix to check.

Returns:

true the first elements in the ImmutableList are the prefix, false if the first elements are not equal to the prefix.