public abstract class AbstractSlicer
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
protected static class |
AbstractSlicer.SequentInfo
The result returned by
AbstractSlicer#analyzeSequent(Node) . |
Constructor and Description |
---|
AbstractSlicer() |
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
ISymbolicEquivalenceClass es. |
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)
|
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)
|
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
Expression s into Term s. |
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 . |
public ImmutableArray<Node> slice(Node seedNode, Term term, ImmutableList<ISymbolicEquivalenceClass> sec) throws ProofInputException
seedNode
- The seed Node
to start slicing at.term
- The seed Term
.sec
- The optional ISymbolicEquivalenceClass
es to consider.ProofInputException
public ImmutableArray<Node> slice(Node seedNode, ReferencePrefix seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) throws ProofInputException
seedNode
- The seed Node
to start slicing at.seedLocation
- The seed ReferencePrefix
.sec
- The optional ISymbolicEquivalenceClass
es to consider.ProofInputException
public ImmutableArray<Node> slice(Node seedNode, Location seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) throws ProofInputException
seedNode
- The seed Node
to start slicing at.seedLocation
- The seed ReferencePrefix
.sec
- The optional ISymbolicEquivalenceClass
es to consider.ProofInputException
protected abstract ImmutableArray<Node> doSlicing(Node seedNode, Location seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) throws ProofInputException
seedNode
- The seed Node
to start slicing at.seedLocation
- The seed Location
.sec
- The optional ISymbolicEquivalenceClass
es to consider.ProofInputException
protected AbstractSlicer.SequentInfo analyzeSequent(Node node, ImmutableList<ISymbolicEquivalenceClass> sec)
Node
at the application PosInOccurrence
and computes the current this
reference.node
- The Node
to analyze.AbstractSlicer.SequentInfo
or null
if the Node
is not supported.protected void analyzeEquivalenceClasses(Services services, ImmutableList<ISymbolicEquivalenceClass> sec, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference)
ISymbolicEquivalenceClass
es.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
).protected void analyzeSequent(Services services, Sequent sequent, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference)
Sequent
for equalities specified by top level formulas.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
).protected void analyzeEquality(Services services, Term equality, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference)
Term
for aliased locations.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
).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)
#analyzeSequent(Node)
to analyze the given updates.updates
- The update Term
s 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
).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)
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map)
to analyze a given update.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
).protected void analyzeHeapUpdate(Term term, Services services, HeapLDT heapLDT, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference)
#analyzeUpdate(Term, Services, HeapLDT, Map)
to analyze a given update.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
).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
term
- The update Term
to analyze.services
- The Services
to use.heapLDT
- The HeapLDT
of the Services
.listToFill
- The result List
with Location
s to fill.ec
- The current ExecutionContext
.thisReference
- The ReferencePrefix
which is represented by this
(ThisReference
).ProofInputException
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
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix)
to analyze a given update.term
- The heap update Term
to analyze.services
- The Services
to use.heapLDT
- The HeapLDT
of the Services
.listToFill
- The result List
with Location
s to fill.thisReference
- The ReferencePrefix
which is represented by this
(ThisReference
).ProofInputException
protected void updateAliases(Services services, Location first, Location second, java.util.Map<Location,java.util.SortedSet<Location>> aliases, ReferencePrefix thisReference)
ReferencePrefix
to the alias Map
.
If required, all participating entries in the Map
are updated to ensure consistency.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
).protected java.util.SortedSet<Location> createSortedSet()
SortedSet
which ensures that the elements are sorted.SortedSet
.protected Location normalizeAlias(Services services, ReferencePrefix referencePrefix, AbstractSlicer.SequentInfo info)
ReferencePrefix
.services
- The Services
to use.referencePrefix
- The ReferencePrefix
.info
- The AbstractSlicer.SequentInfo
with the aliases and so on.protected Location normalizeAlias(Services services, Location location, AbstractSlicer.SequentInfo info)
Location
.services
- The Services
to use.location
- The Location
.info
- The AbstractSlicer.SequentInfo
with the aliases and so on.protected Access normalizeArrayIndex(Access access, AbstractSlicer.SequentInfo info)
access
- The Access
representing an array index.info
- The AbstractSlicer.SequentInfo
with the aliases and so on.protected Location computeRepresentativeAlias(Location location, java.util.Map<Location,java.util.SortedSet<Location>> aliases)
Location
.location
- The given Location
.aliases
- The available aliases.protected ReferencePrefix toReferencePrefix(SourceElement sourceElement)
ReferencePrefix
of the given SourceElement
.sourceElement
- The SourceElement
to work with.ReferencePrefix
or null
if the SourceElement
can't be represented as ReferencePrefix
.protected boolean removeRelevant(Services services, ReferencePrefix sourceElement, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info)
SourceElement
is directly or indirectly
contained (aliased) in the Set
of relevant locations.
If it is contained, the element will be removed.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.true
is relevant and was removed, false
is not relevant and nothing has changed.protected boolean removeRelevant(Services services, Location location, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info)
Location
is directly or indirectly
contained (aliased) in the Set
of relevant locations.
If it is contained, the element will be removed.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.true
is relevant and was removed, false
is not relevant and nothing has changed.protected boolean performRemoveRelevant(Services services, Location normalized, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info)
Location
is directly or indirectly
contained (aliased) in the Set
of relevant locations.
If it is contained, the element will be removed.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.true
is relevant and was removed, false
is not relevant and nothing has changed.protected Location toLocation(Services services, ReferencePrefix prefix, ExecutionContext ec, ReferencePrefix thisReference)
ReferencePrefix
into a Location
.services
- The Services
to use.prefix
- The ReferencePrefix
to convert.ec
- The current ExecutionContext
.thisReference
- The ReferencePrefix
which is represented by this
(ThisReference
).Location
representing the given ReferencePrefix
.protected ImmutableList<Access> toLocationRecursive(Services services, ReferencePrefix prefix, ExecutionContext ec, ReferencePrefix thisReference, ImmutableList<Access> children)
#toLocation(Services, ReferencePrefix, ReferencePrefix)
to recursively extract the Access
instances.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 Access
s.ImmutableList
containing all Access
s of the ReferencePrefix
in the order of access.public static ImmutableArray<Term> toTerm(Services services, ImmutableArray<Expression> expressions, ExecutionContext ec)
Expression
s into Term
s.services
- The Services
to use.expressions
- The Expression
s to convert.ec
- The current ExecutionContext
.Term
s.public static Term toTerm(Services services, Expression expression, ExecutionContext ec)
Expression
into a Term
.services
- The Services
to use.expression
- The Expression
to convert.ec
- The current ExecutionContext
.Term
.protected Location findNewAlternative(java.util.SortedSet<Location> oldAlternatives, java.util.SortedSet<Location> newAlternatives)
oldAlternatives
- The old alternatives.newAlternatives
- The new alternatives.null
if not available.public static <T> int computeFirstCommonPrefixLength(ImmutableList<ImmutableList<T>> candidates, ImmutableList<T> toCheck)
candidates
- The possible candidates.toCheck
- The ImmutableList
to check.0
if no elements are common.public static <T> boolean startsWith(ImmutableList<T> list, ImmutableList<T> prefix)
ImmutableList
starts with the given prefix.list
- The List
to check.prefix
- The prefix to check.true
the first elements in the ImmutableList
are the prefix, false
if the first elements are not equal to the prefix.