Package org.checkerframework.dataflow.analysis

Class ForwardAnalysisImpl<V extends AbstractValue<V>,​S extends Store<S>,​T extends ForwardTransferFunction<V,​S>>

  • Type Parameters:
    V - the abstract value type to be tracked by the analysis
    S - the store type used in the analysis
    T - the transfer function type that is used to approximate runtime behavior
    All Implemented Interfaces:
    Analysis<V,​S,​T>, ForwardAnalysis<V,​S,​T>
    Direct Known Subclasses:
    CFAbstractAnalysis
    public class ForwardAnalysisImpl<V extends AbstractValue<V>,​S extends Store<S>,​T extends ForwardTransferFunction<V,​S>>
extends AbstractAnalysis<V,​S,​T>
implements ForwardAnalysis<V,​S,​T>
    An implementation of a forward analysis to solve a org.checkerframework.dataflow problem given a control flow graph and a forward transfer function.

    • Field Detail

      • blockCount

        protected final @Nullable java.util.IdentityHashMap<Block,​java.lang.Integer> blockCount
        Number of times each block has been analyzed since the last time widening was applied. Null if maxCountBeforeWidening is -1, which implies widening isn't used for this analysis.

      • maxCountBeforeWidening

        protected final int maxCountBeforeWidening
        Number of times a block can be analyzed before widening. -1 implies that widening shouldn't be used.

      • thenStores

        protected final java.util.IdentityHashMap<Block,​S extends Store<S>> thenStores
        Then stores before every basic block (assumed to be 'no information' if not present).

      • elseStores

        protected final java.util.IdentityHashMap<Block,​S extends Store<S>> elseStores
        Else stores before every basic block (assumed to be 'no information' if not present).

    • Constructor Detail

      • ForwardAnalysisImpl

        public ForwardAnalysisImpl​(int maxCountBeforeWidening)
        Construct an object that can perform a org.checkerframework.dataflow forward analysis over a control flow graph. When using this constructor, the transfer function is set later by the subclass, e.g., org.checkerframework.framework.flow.CFAbstractAnalysis.
        Parameters:
        maxCountBeforeWidening - number of times a block can be analyzed before widening

      • ForwardAnalysisImpl

        public ForwardAnalysisImpl​(T transferFunction)
        Construct an object that can perform a org.checkerframework.dataflow forward analysis over a control flow graph given a transfer function.
        Parameters:
        transferFunction - the transfer function

    • Method Detail

      • runAnalysisFor

        public S runAnalysisFor​(@FindDistinct
                        Node node,
                        Analysis.BeforeOrAfter preOrPost,
                        TransferInput<V,​S> blockTransferInput,
                        java.util.IdentityHashMap<Node,​V> nodeValues,
                        @Nullable java.util.Map<TransferInput<V,​S>,​java.util.IdentityHashMap<Node,​TransferResult<V,​S>>> analysisCaches)
        Description copied from interface: Analysis
        Runs the analysis again within the block of node and returns the store at the location of node. If before is true, then the store immediately before the Node node is returned. Otherwise, the store immediately after node is returned. If analysisCaches is not null, this method uses a cache. analysisCaches is a map of a block of node to the cached analysis result. If the cache for transferInput is not in analysisCaches, this method creates new cache and stores it in analysisCaches. The cache is a map of nodes to the analysis results of the nodes.
        Specified by:
        runAnalysisFor in interface Analysis<V extends AbstractValue<V>,​S extends Store<S>,​T extends ForwardTransferFunction<V,​S>>
        Parameters:
        node - the node to analyze
        preOrPost - which store to return: the store immediately before node or the store after node
        blockTransferInput - the transfer input of the block of this node
        nodeValues - abstract values of nodes
        analysisCaches - caches of analysis results
        Returns:
        the store before or after node (depends on the value of before) after running the analysis

      • addStoreBefore

        protected void addStoreBefore​(Block b,
                              @Nullable Node node,
                              S s,
                              Store.Kind kind,
                              boolean addBlockToWorklist)
        Add a store before the basic block b by merging with the existing stores for that location.
        Parameters:
        b - a basic block
        node - the node of the basic block b
        s - the store being added
        kind - the kind of store s
        addBlockToWorklist - whether the basic block b should be added back to Worklist

      • getStoreBefore

        protected @Nullable S getStoreBefore​(Block b,
                                     Store.Kind kind)
        Return the store corresponding to the location right before the basic block b.
        Parameters:
        b - a block
        kind - the kind of store which will be returned
        Returns:
        the store corresponding to the location right before the basic block b

      • getInputBefore

        protected @Nullable TransferInput<V,​S> getInputBefore​(Block b)
        Returns the transfer input corresponding to the location right before the basic block b.
        Parameters:
        b - a block
        Returns:
        the transfer input corresponding to the location right before the basic block b