public class BamTransferRelation<CfaNodeT extends CfaNode<CfaEdgeT,SignatureT>,CfaEdgeT extends CfaEdge<CfaNodeT>,SignatureT extends Signature> extends java.lang.Object implements TransferRelation
TransferRelation
extends an analysis inter-procedurally. The transfer relation applies as close as possible the algorithms described in 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 a
CpaWithBamOperators
inter-procedurally. For more details on how the transfer relation works see getAbstractSuccessors(AbstractState, Precision)
.Constructor and Description |
---|
BamTransferRelation(CpaWithBamOperators<CfaNodeT,CfaEdgeT,SignatureT> wrappedCpa,
Cfa<CfaNodeT,CfaEdgeT,SignatureT> cfa,
SignatureT mainFunction,
BamCache<SignatureT> cache)
Create a BAM transfer relation with an unlimited call stack.
|
BamTransferRelation(CpaWithBamOperators<CfaNodeT,CfaEdgeT,SignatureT> wrappedCpa,
Cfa<CfaNodeT,CfaEdgeT,SignatureT> cfa,
SignatureT mainFunction,
BamCache<SignatureT> cache,
int maxCallStackDepth,
AbortOperator abortOperator)
Create a BAM transfer relation with a specified maximum call stack depth.
|
Modifier and Type | Method and Description |
---|---|
java.util.Collection<? extends AbstractState> |
getAbstractSuccessors(AbstractState abstractState,
Precision precision)
In order to implement an inter-procedural analysis the abstract successors are calculated for the following cases:
|
BamCache<SignatureT> |
getCache()
Returns BAM cache storing analysis result for various method calls.
|
Cfa<CfaNodeT,CfaEdgeT,SignatureT> |
getCfa()
Returns the CFA used by the transfer relation.
|
int |
getMaxCallStackDepth()
Returns the maximal call stack depth.
|
protected ReachedSet |
getReachedSet()
By default the
ReachedSet used by the applyBlockAbstraction algorithm is a ProgramLocationDependentReachedSet , this method can be overridden to provide a different reached set. |
protected Waitlist |
getWaitlist()
By default the
Waitlist used by the applyBlockAbstraction algorithm is a BreadthFirstWaitlist , this method can be overridden to provide a different waitlist. |
CpaWithBamOperators<CfaNodeT,CfaEdgeT,SignatureT> |
getWrappedCpa()
Returns the wrapped domain-dependent intra-procedural CPA.
|
public BamTransferRelation(CpaWithBamOperators<CfaNodeT,CfaEdgeT,SignatureT> wrappedCpa, Cfa<CfaNodeT,CfaEdgeT,SignatureT> cfa, SignatureT mainFunction, BamCache<SignatureT> cache)
wrappedCpa
- a wrapped CPA with BAM operatorscfa
- a control flow automatonmainFunction
- the signature of the main function of an analyzed programcache
- a cache for the block abstractionspublic BamTransferRelation(CpaWithBamOperators<CfaNodeT,CfaEdgeT,SignatureT> wrappedCpa, Cfa<CfaNodeT,CfaEdgeT,SignatureT> cfa, SignatureT mainFunction, BamCache<SignatureT> cache, int maxCallStackDepth, AbortOperator abortOperator)
wrappedCpa
- a wrapped CPA with BAM operatorscfa
- a control flow automatonmainFunction
- the signature of the main function of an analyzed programcache
- a cache for the block abstractionsmaxCallStackDepth
- maximum depth of the call stack analyzed inter-procedurally.
0 means intra-procedural analysis.
< 0 means no maximum depth.abortOperator
- an abort operator used for computing block abstractionspublic java.util.Collection<? extends AbstractState> getAbstractSuccessors(AbstractState abstractState, Precision precision)
- 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 specified AbstractState
(i.e. different parameters or
global state result in a different summary). Since we have no information on the code of the target of SymbolicCall
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 an object) abstract state that has as location the next node of the Cfa
. 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.
getAbstractSuccessors
in interface TransferRelation
public int getMaxCallStackDepth()
public CpaWithBamOperators<CfaNodeT,CfaEdgeT,SignatureT> getWrappedCpa()
protected Waitlist getWaitlist()
Waitlist
used by the applyBlockAbstraction algorithm is a BreadthFirstWaitlist
, this method can be overridden to provide a different waitlist.protected ReachedSet getReachedSet()
ReachedSet
used by the applyBlockAbstraction algorithm is a ProgramLocationDependentReachedSet
, this method can be overridden to provide a different reached set.public BamCache<SignatureT> getCache()
public Cfa<CfaNodeT,CfaEdgeT,SignatureT> getCfa()