proguard.analysis.cpa.jvm.domain.memory

Class JvmMemoryLocationTransferRelation<ContentT extends AbstractState<ContentT>>

java.lang.Object

proguard.analysis.cpa.jvm.domain.memory.JvmMemoryLocationTransferRelation<ContentT>

Type Parameters:

ContentT - The content of the jvm states for the traced analysis. For example, this can be a SetAbstractState of taints for taint analysis or a ValueAbstractState for value analysis.

All Implemented Interfaces:

TransferRelation<JvmMemoryLocationAbstractState<ContentT>>

public class JvmMemoryLocationTransferRelation<ContentT extends AbstractState<ContentT>>
extends java.lang.Object
implements TransferRelation<JvmMemoryLocationAbstractState<ContentT>>

The JvmMemoryLocationTransferRelation computes the backward successors of an JvmMemoryLocationAbstractState for a given instruction. A backward successor is a memory location which may have contributed to the value of the current JvmMemoryLocation.

The transfer relation uses a BamCache containing the results of an analysis in order to calculate the successors JvmMemoryLocationAbstractState:

• If a successor is in the currently analyzed method just use the current ProgramLocationDependentReachedSet (representing the results of the back-traced analysis for the current method call with a specific entry state).
• If the current state can be the result of a method call, search for entry in the cache that can result in the current state (i.e. from the cache entries of the called methods get the ones that have as initial state the result of the ReduceOperator of the back-traced analysis for the caller abstract state and that have an exit state that results in the current state after applying the ExpandOperator of the back-traced analysis).
• If the current state is located in the entry node of a method:
  • If the call site was analyzed during the backward analysis the successor location will be the known caller.
  • Otherwise look for all potential callers in the cache (i.e. states that call the method and result in the current method after applying the ReduceOperator).

The value of the successor memory location is guaranteed to be greater than the threshold (e.g. if ContentT is a SetAbstractState we can set the threshold to SetAbstractState.bottom to guarantee we don't calculate a successor if the taint is not propagated anymore). Thus, the threshold defines the cut-off of the traces generated with JvmMemoryLocationTransferRelation.

Constructor Summary

Constructors

Constructor and Description
JvmMemoryLocationTransferRelation(ContentT threshold, BamCpa<ContentT> bamCpa, java.util.Map<Call,java.util.Set<JvmMemoryLocation>> extraTaintPropagationLocations) Create a memory location transfer relation.

Method Summary

Modifier and Type	Method and Description
java.util.Collection<JvmMemoryLocationAbstractState<ContentT>>	generateAbstractSuccessors(JvmMemoryLocationAbstractState<ContentT> abstractState, Precision precision) Returns abstract successor states of the abstractState under the selected precision.
protected java.util.List<JvmMemoryLocation>	processCall(JvmMemoryLocation memoryLocation, ConstantInstruction callInstruction, Clazz clazz, JvmCfaNode parentNode) The default implementation traces the return value back to the method arguments and the instance.

Methods inherited from class java.lang.Object

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

Constructor Detail

JvmMemoryLocationTransferRelation

public JvmMemoryLocationTransferRelation(ContentT threshold,
                                         BamCpa<ContentT> bamCpa,
                                         java.util.Map<Call,java.util.Set<JvmMemoryLocation>> extraTaintPropagationLocations)

Create a memory location transfer relation.

Parameters:

threshold - a cut-off threshold

bamCpa - the BAM cpa that was used to calculate the results in the cache

Method Detail

generateAbstractSuccessors

public java.util.Collection<JvmMemoryLocationAbstractState<ContentT>> generateAbstractSuccessors(JvmMemoryLocationAbstractState<ContentT> abstractState,
                                                                                                 Precision precision)

Description copied from interface: TransferRelation

Returns abstract successor states of the abstractState under the selected precision.

Specified by:

generateAbstractSuccessors in interface TransferRelation<JvmMemoryLocationAbstractState<ContentT extends AbstractState<ContentT>>>

processCall

protected java.util.List<JvmMemoryLocation> processCall(JvmMemoryLocation memoryLocation,
                                                        ConstantInstruction callInstruction,
                                                        Clazz clazz,
                                                        JvmCfaNode parentNode)

The default implementation traces the return value back to the method arguments and the instance. Additionally, handles extra taints' propagation if the need is identified at this call site.