de.uka.ilkd.key.symbolic_execution.slicing

Class AbstractBackwardSlicer

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.slicing.AbstractBackwardSlicer

Direct Known Subclasses:

ThinBackwardSlicer

public abstract class AbstractBackwardSlicer
extends AbstractSlicer

Provides a basic implementation of backward slicing algorithms.

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer

AbstractSlicer.SequentInfo

Constructor Summary

Constructors

Constructor and Description
AbstractBackwardSlicer()

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	accept(Node node, Node previousChild, Services services, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info, SourceElement activeStatement) Decides if the given Node is part of the slice or not.
ImmutableArray<Node>	doSlicing(Node seedNode, Location seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) Performs the slicing.
protected java.util.Set<Location>	updateOutdatedLocations(Services services, java.util.Set<Location> oldLocationsToUpdate, java.util.Map<Location,java.util.SortedSet<Location>> newAliases, java.util.Map<Location,java.util.SortedSet<Location>> oldAliases, Location outdatedPrefix, ReferencePrefix thisReference) Updates the outdated locations.
protected void	updateRelevantLocations(ProgramElement read, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info, Services services) Updates the relevant locations.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer

analyzeEquality, analyzeEquivalenceClasses, analyzeHeapUpdate, analyzeSequent, analyzeSequent, analyzeUpdate, analyzeUpdates, computeFirstCommonPrefixLength, computeRepresentativeAlias, createSortedSet, findNewAlternative, listModifiedHeapLocations, listModifiedLocations, normalizeAlias, normalizeAlias, normalizeArrayIndex, performRemoveRelevant, removeRelevant, removeRelevant, slice, slice, slice, startsWith, toLocation, toLocation, toLocationRecursive, toReferencePrefix, toTerm, toTerm, updateAliases

Methods inherited from class java.lang.Object

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

Constructor Detail

AbstractBackwardSlicer

public AbstractBackwardSlicer()

Method Detail

doSlicing

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

Performs the slicing.

Specified by:

doSlicing in class AbstractSlicer

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

accept

protected abstract boolean accept(Node node,
                                  Node previousChild,
                                  Services services,
                                  java.util.Set<Location> relevantLocations,
                                  AbstractSlicer.SequentInfo info,
                                  SourceElement activeStatement)
                           throws ProofInputException

Decides if the given Node is part of the slice or not.

Parameters:

node - The Node to check.

previousChild - The previously visited child Node or null the first time.

services - The Services to use.

relevantLocations - The relevant locations.

info - The SequentInfo with the aliases and so on.

activeStatement - The currently active statement.

Returns:

true Node should be part of slice, false Node should not be part of slice.

Throws:

ProofInputException

updateRelevantLocations

protected void updateRelevantLocations(ProgramElement read,
                                       java.util.Set<Location> relevantLocations,
                                       AbstractSlicer.SequentInfo info,
                                       Services services)

Updates the relevant locations.

Parameters:

read - The Expression which provides new relevant locations.

relevantLocations - The relevant locations to update.

info - The SequentInfo with the aliases and so on.

services - The Services to use.

updateOutdatedLocations

protected java.util.Set<Location> updateOutdatedLocations(Services services,
                                                          java.util.Set<Location> oldLocationsToUpdate,
                                                          java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
                                                          java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
                                                          Location outdatedPrefix,
                                                          ReferencePrefix thisReference)

Updates the outdated locations. This means that locations with the given prefix are replaced with another previously (old) available alternative.

Parameters:

services - The Services to use.

oldLocationsToUpdate - The locations to update.

newAliases - The new aliases.

oldAliases - The old aliases.

outdatedPrefix - The prefix of outdated locations.

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

Returns:

The updated locations.