JvmMemoryLocationTransferRelation (ProGuardCORE)

java.lang.Object
- proguard.analysis.cpa.jvm.domain.memory.JvmMemoryLocationTransferRelation<AbstractStateT>

Type Parameters:

AbstractStateT - The type of the values of the traced analysis.

All Implemented Interfaces:

TransferRelation
```
public class JvmMemoryLocationTransferRelation<AbstractStateT extends LatticeAbstractState<AbstractStateT>>
extends java.lang.Object
implements TransferRelation
```
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 MemoryLocation.
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 AbstractStateT is a proguard.analysis.cpa.domain.taint.TaintAbstractState we can set the threshold to proguard.analysis.cpa.domain.taint.TaintAbstractState#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(AbstractStateT threshold, BamCpa<JvmCfaNode,JvmCfaEdge,MethodSignature> bamCpa)` Create a memory location transfer relation.

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`java.util.Collection<? extends AbstractState>`	`generateAbstractSuccessors(AbstractState 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)` 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(AbstractStateT threshold,
                                         BamCpa<JvmCfaNode,JvmCfaEdge,MethodSignature> bamCpa)

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<? extends AbstractState> generateAbstractSuccessors(AbstractState 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

processCall

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

The default implementation traces the return value back to the method arguments and the instance.

Class JvmMemoryLocationTransferRelation<AbstractStateT extends LatticeAbstractState<AbstractStateT>>