Package proguard.analysis.cpa.jvm.domain.memory

Interface TraceExtractor<T extends LatticeAbstractState<T>>

Type Parameters:

T - The type of the states contained in the JVM state. e.g., for taint analysis this would be a SetAbstractState containing the taints and for value analysis a ValueAbstractState.

public interface TraceExtractor<T extends LatticeAbstractState<T>>

This interface contains helper methods for producing witness traces.

Method Summary

Modifier and Type	Method	Description
default java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>>>	extractLinearTraces()	Returns a set of linear witness traces.
java.util.Collection<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>>	getEndPoints()	Returns endpoints or the extracted traces.
ProgramLocationDependentReachedSet<JvmCfaNode,JvmCfaEdge,JvmMemoryLocationAbstractState<JvmAbstractState<T>>,MethodSignature>	getTraceReconstructionReachedSet()	Returns the reached set of a trace extracting memory location CPA.
default java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>>	removeDuplicateProgramLocations(java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>> trace)
default void	traceExtractionIteration(java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>>> result, java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>> currentTrace)

Method Detail

extractLinearTraces

default java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>>> extractLinearTraces()

Returns a set of linear witness traces.

getEndPoints

java.util.Collection<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>> getEndPoints()

Returns endpoints or the extracted traces. Its output should be used for constructing initial states for memory location CPAs.

getTraceReconstructionReachedSet

ProgramLocationDependentReachedSet<JvmCfaNode,JvmCfaEdge,JvmMemoryLocationAbstractState<JvmAbstractState<T>>,MethodSignature> getTraceReconstructionReachedSet()

Returns the reached set of a trace extracting memory location CPA.

traceExtractionIteration

default void traceExtractionIteration(java.util.Set<java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>>> result,
                                      java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>> currentTrace)

removeDuplicateProgramLocations

default java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>> removeDuplicateProgramLocations(java.util.List<BamLocationDependentJvmMemoryLocation<JvmAbstractState<T>>> trace)