proguard.analysis.cpa.algorithms

Class CpaAlgorithm

java.lang.Object

proguard.analysis.cpa.algorithms.CpaAlgorithm

All Implemented Interfaces:

Algorithm

public class CpaAlgorithm
extends java.lang.Object
implements Algorithm

This is the CPA+ Algorithm. The algorithm computes the set of reached states based on the initial content of the waitlist.

Constructor Summary

Constructors

Constructor and Description
CpaAlgorithm(ConfigurableProgramAnalysis cpa) Create an algorithm to run the specified CPA.
CpaAlgorithm(TransferRelation transferRelation, MergeOperator mergeOperator, StopOperator stopOperator, PrecisionAdjustment precisionAdjustment) Create a CPA algorithm from CPA components.

Method Summary

Modifier and Type	Method and Description
void	run(ReachedSet reachedSet, Waitlist waitlist, AbortOperator abortOperator) Algorithm from the paper is parametrized with the reached set and the waitlist.

Methods inherited from class java.lang.Object

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

Methods inherited from interface proguard.analysis.cpa.interfaces.Algorithm

run

Constructor Detail

CpaAlgorithm

public CpaAlgorithm(ConfigurableProgramAnalysis cpa)

Create an algorithm to run the specified CPA.

Parameters:

cpa - a CPA instance wrapping the transfer relation, the merge, and the stop operator, and the precision adjustment

CpaAlgorithm

public CpaAlgorithm(TransferRelation transferRelation,
                    MergeOperator mergeOperator,
                    StopOperator stopOperator,
                    PrecisionAdjustment precisionAdjustment)

Create a CPA algorithm from CPA components.

Parameters:

transferRelation - a transfer relation specifying how successor states are computed

mergeOperator - a merge operator defining how (and whether) the older AbstractState should be updated with the newly discovered AbstractState

stopOperator - a stop operator deciding whether the successor state should be added to the ReachedSet based on the content of the latter

precisionAdjustment - a precision adjustment selecting the Precision for the currently processed AbstractState considering the ReachedSet content

Method Detail

run

public void run(ReachedSet reachedSet,
                Waitlist waitlist,
                AbortOperator abortOperator)

Algorithm from the paper is parametrized with the reached set and the waitlist. Thus one can select the start point of the algorithm (e.g., for resuming the analysis). The abortOperator determines whether the analysis should end prematurely.

Specified by:

run in interface Algorithm