public class BamCpa<ContentT extends AbstractState<ContentT>> extends java.lang.Object implements ConfigurableProgramAnalysis<JvmAbstractState<ContentT>>
ConfigurableProgramAnalysis for inter-procedural analysis using block abstraction
memoization as described in https://dl.acm.org/doi/pdf/10.1145/3368089.3409718, which is
defined by a domain-dependent CpaWithBamOperators that adds three operators: reduce,
expand, and rebuild. This allows an inter-procedural analysis running this CPA to be conducted by
the standard CpaAlgorithm.
A BAM CPA works on a domain-independent level and its abstract domain, merge operator, and
stop operator are defined by the domain-dependent wrapped CPA. The main feature of a BAM CPA is
its transfer relation (see BamTransferRelation for details) that is able to extend the
analysis of the wrapped CPA to the inter-procedural level.
| Constructor and Description |
|---|
BamCpa(CpaWithBamOperators<ContentT> wrappedCpa,
JvmCfa cfa,
MethodSignature mainFunction,
BamCache<ContentT> cache)
Create a BamCpa with default transfer relation.
|
BamCpa(CpaWithBamOperators<ContentT> wrappedCpa,
JvmCfa cfa,
MethodSignature mainFunction,
BamCache<ContentT> cache,
int maxCallStackDepth)
Create a BamCpa with default transfer relation with a limited call depth.
|
| Modifier and Type | Method and Description |
|---|---|
@NotNull AbortOperator |
getAbortOperator() |
BamCache<ContentT> |
getCache()
Returns the BAM cache used by the CPA.
|
JvmCfa |
getCfa()
Returns the CFA used by the CPA.
|
ExpandOperator<ContentT> |
getExpandOperator()
Returns the expand operator of the wrapped CPA.
|
TransferRelation<JvmAbstractState<ContentT>> |
getIntraproceduralTransferRelation()
Returns the transfer relation of the interprocedural CPA wrapped by the BamCpa.
|
@NotNull MergeOperator<JvmAbstractState<ContentT>> |
getMergeOperator()
Returns the merge operator of the wrapped CPA.
|
@NotNull PrecisionAdjustment |
getPrecisionAdjustment()
Returns the precision adjustment of the wrapped CPA.
|
RebuildOperator |
getRebuildOperator()
Returns the rebuild operator of the wrapped CPA.
|
ReduceOperator<ContentT> |
getReduceOperator()
Returns the reduce operator of the wrapped CPA.
|
@NotNull StopOperator<JvmAbstractState<ContentT>> |
getStopOperator()
Returns the stop operator of the wrapped CPA.
|
@NotNull BamTransferRelation<ContentT> |
getTransferRelation()
Returns the BAM transfer relation, more details in
BamTransferRelation. |
public BamCpa(CpaWithBamOperators<ContentT> wrappedCpa, JvmCfa cfa, MethodSignature mainFunction, BamCache<ContentT> 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 BamCpa(CpaWithBamOperators<ContentT> wrappedCpa, JvmCfa cfa, MethodSignature mainFunction, BamCache<ContentT> cache, int maxCallStackDepth)
wrappedCpa - a wrapped cpa with BAM operatorscfa - a control flow automatonmainFunction - the signature of a main functioncache - 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.@NotNull public @NotNull BamTransferRelation<ContentT> getTransferRelation()
BamTransferRelation.getTransferRelation in interface ConfigurableProgramAnalysis<JvmAbstractState<ContentT extends AbstractState<ContentT>>>@NotNull public @NotNull MergeOperator<JvmAbstractState<ContentT>> getMergeOperator()
getMergeOperator in interface ConfigurableProgramAnalysis<JvmAbstractState<ContentT extends AbstractState<ContentT>>>@NotNull public @NotNull StopOperator<JvmAbstractState<ContentT>> getStopOperator()
getStopOperator in interface ConfigurableProgramAnalysis<JvmAbstractState<ContentT extends AbstractState<ContentT>>>@NotNull public @NotNull PrecisionAdjustment getPrecisionAdjustment()
getPrecisionAdjustment in interface ConfigurableProgramAnalysis<JvmAbstractState<ContentT extends AbstractState<ContentT>>>@NotNull public @NotNull AbortOperator getAbortOperator()
getAbortOperator in interface ConfigurableProgramAnalysis<JvmAbstractState<ContentT extends AbstractState<ContentT>>>public ReduceOperator<ContentT> getReduceOperator()
public ExpandOperator<ContentT> getExpandOperator()
public RebuildOperator getRebuildOperator()
public JvmCfa getCfa()
public TransferRelation<JvmAbstractState<ContentT>> getIntraproceduralTransferRelation()
This transfer relation is used to analyze all non-call instructions and call instructions that cannot be analyzed inter-procedurally (e.g., because their code is not available or because the maximum analysis depth has been reached).