Class BamTransferRelation<ContentT extends AbstractState<ContentT>>
- java.lang.Object
-
- proguard.analysis.cpa.bam.BamTransferRelation<ContentT>
-
- Type Parameters:
ContentT
- The content of the jvm states. For example, this can be aSetAbstractState
of taints for taint analysis or aValueAbstractState
for value analysis.
- All Implemented Interfaces:
TransferRelation<JvmAbstractState<ContentT>>
public class BamTransferRelation<ContentT extends AbstractState<ContentT>> extends java.lang.Object implements TransferRelation<JvmAbstractState<ContentT>>
ThisTransferRelation
extends an analysis inter-procedurally. The transfer relation applies as close as possible the algorithms described in {@see https://dl.acm.org/doi/pdf/10.1145/3368089.3409718}. On a high level the task of this domain-independent transfer relation is to extend the intra-procedural domain-dependent transfer relation of aCpaWithBamOperators
inter-procedurally. For more details on how the transfer relation works seegenerateAbstractSuccessors(JvmAbstractState, Precision)
.
-
-
Constructor Summary
Constructors Constructor Description BamTransferRelation(BamCpa<ContentT> bamCpa, JvmCfa cfa, MethodSignature mainFunction, BamCache<ContentT> cache)
Create a BAM transfer relation with an unlimited call stack.BamTransferRelation(BamCpa<ContentT> bamCpa, JvmCfa cfa, MethodSignature mainFunction, BamCache<ContentT> cache, int maxCallStackDepth)
Create a BAM transfer relation with a specified maximum call stack depth.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description java.util.Collection<JvmAbstractState<ContentT>>
generateAbstractSuccessors(JvmAbstractState<ContentT> abstractState, Precision precision)
In order to implement an inter-procedural analysis the abstract successors are calculated for the following cases:BamCache<ContentT>
getCache()
Returns BAM cache storing analysis result for various method calls.JvmCfa
getCfa()
Returns the CFA used by the transfer relation.protected ProgramLocationDependentReachedSet<JvmAbstractState<ContentT>>
getReachedSet()
By default, theReachedSet
used by the applyBlockAbstraction algorithm is aProgramLocationDependentReachedSet
, this method can be overridden to provide a different reached set.protected Waitlist<JvmAbstractState<ContentT>>
getWaitlist()
By default, theWaitlist
used by the applyBlockAbstraction algorithm is aBreadthFirstWaitlist
, this method can be overridden to provide a different waitlist.
-
-
-
Constructor Detail
-
BamTransferRelation
public BamTransferRelation(BamCpa<ContentT> bamCpa, JvmCfa cfa, MethodSignature mainFunction, BamCache<ContentT> cache)
Create a BAM transfer relation with an unlimited call stack.- Parameters:
bamCpa
- a BAM cpa. It wraps a CPA that is called recursively when a method call is analyzed.cfa
- a control flow automaton.mainFunction
- the signature of the main function of an analyzed program.cache
- a cache for the block abstractions.
-
BamTransferRelation
public BamTransferRelation(BamCpa<ContentT> bamCpa, JvmCfa cfa, MethodSignature mainFunction, BamCache<ContentT> cache, int maxCallStackDepth)
Create a BAM transfer relation with a specified maximum call stack depth. When the call stack meets its size limit the method call analysis is delegated to the wrapped intra-procedural transfer relation.- Parameters:
bamCpa
- a BAM cpa. It wraps a CPA that is called recursively when a method call is analyzed.cfa
- a control flow automaton.mainFunction
- the signature of the main function of an analyzed program.cache
- a cache for the block abstractions.maxCallStackDepth
- maximum depth of the call stack analyzed inter-procedurally. 0 means intra-procedural analysis. < 0 means no maximum depth.
-
-
Method Detail
-
generateAbstractSuccessors
public java.util.Collection<JvmAbstractState<ContentT>> generateAbstractSuccessors(JvmAbstractState<ContentT> abstractState, Precision precision)
In order to implement an inter-procedural analysis the abstract successors are calculated for the following cases:- Run the fixed point algorithm from the entry of the main method, continuing the analysis until a fixed point is reached (i.e. a function summary is provided for each function, also the recursive ones). If there are no recursive calls the fixed point is reached after the first iteration, while in case of recursive calls, depending on the domain-dependent transfer relation, they can be unrolled at each iteration until the fixed point is reached.
- Run the applyBlockAbstraction algorithm at every known procedure call. This algorithm takes care of retrieving the summary of the procedure from the cache (if available) or calls
CpaAlgorithm
recursively on the new function to compute and store in the cache the summary of the procedure when called from the specifiedAbstractState
(i.e. different parameters or global state result in a different summary). Since we have no information on the code of the target ofSymbolicCall
this type of calls is delegated to the intra-procedural transfer relation instead of being analyzed by the applyBlockAbstraction algorithm. The result of the block abstraction on the intra-procedural level is simply generating a successor (or successors in case there are multiple call edges, e.g. for unknown runtime type of the instance) abstract state that has as location the next node of theCfa
. The recursion can be limited at a maximum call stack size. The intra-procedural transfer relation is also applied in case the max call stack size is reached.- Apply the underlying intra-procedural transfer relation to all the other non-exit nodes in order to act as the wrapped transfer relation when procedure calls are not involved.
- Exit nodes reached are the base cases of the recursion (along with the stop operator), in this case the transfer relation returns with no successors.
- Specified by:
generateAbstractSuccessors
in interfaceTransferRelation<ContentT extends AbstractState<ContentT>>
-
getWaitlist
protected Waitlist<JvmAbstractState<ContentT>> getWaitlist()
By default, theWaitlist
used by the applyBlockAbstraction algorithm is aBreadthFirstWaitlist
, this method can be overridden to provide a different waitlist.
-
getReachedSet
protected ProgramLocationDependentReachedSet<JvmAbstractState<ContentT>> getReachedSet()
By default, theReachedSet
used by the applyBlockAbstraction algorithm is aProgramLocationDependentReachedSet
, this method can be overridden to provide a different reached set.
-
getCache
public BamCache<ContentT> getCache()
Returns BAM cache storing analysis result for various method calls.
-
getCfa
public JvmCfa getCfa()
Returns the CFA used by the transfer relation.
-
-