Introduce backward analysis to dataflow framework.

changelog.txt

@@ -25,22 +25,35 @@ The Nullness Checker now treats `System.getProperty()` soundly.  Use
 `-Alint=permitClearProperty` to disable special treatment of
 `System.getProperty()` and to permit undefining built-in system properties.
 
+Add support for class qualifier parameters.  See "Class qualifier parameters"
+section in the manual.
+
 The Dataflow Framework now also supports backward analysis.
 
 Implementation details:
- * Changed the types of some fields and methods from array to List:
+
+* Changed the types of some fields and methods from array to List:
    QualifierDefaults.validLocationsForUncheckedCodeDefaults()
    QualifierDefaults.STANDARD_CLIMB_DEFAULTS_TOP
    QualifierDefaults.STANDARD_CLIMB_DEFAULTS_BOTTOM
    QualifierDefaults.STANDARD_UNCHECKED_DEFAULTS_TOP
    QualifierDefaults.STANDARD_UNCHECKED_DEFAULTS_BOTTOM
- * Dataflow Framework: Analysis is now an interface, added AbstractAnalysis,
+* Dataflow Framework: Analysis is now an interface, added AbstractAnalysis,
    ForwardAnalysis, ForwardTransferFunction, ForwardAnalysisImpl,
    BackwardAnalysis, BackwardTransferFunction, BackwardAnalysisImpl.
    Existing code is easy to adapt:
      `extends Analysis<V, S, T>` => `extends ForwardAnalysisImpl<V, S, T>`
      `implements TransferFunction<V, S>` => `implements ForwardTransferFunction<V, S>`
 
+In AbstractQualifierPolymorphism, use AnnotationMirrors instead of sets of
+annotation mirrors.
+
+Renamed meta-annotation SuppressWarningsKeys to SuppressWarningsPrefix.
+Renamed SourceChecker#getSuppressWarningsKeys(...) to getSuppressWarningsPrefixes.
+Renamed SubtypingChecker#getSuppressWarningsKeys to getSuppressWarningsPrefixes.
+
+Removed methods and classes marked deprecated in release 3.3.0 or earlier.
+
 ---------------------------------------------------------------------------
 
 Version 3.4.1, June 1, 2020

dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java

@@ -307,7 +307,9 @@ public IdentityHashMap<Node, V> getNodeValues() {
     }
 
     /**
-     * Call the transfer function for node {@code node}, and set that node as current node first.
+     * Call the transfer function for node {@code node}, and set that node as current node first. Be
+     * careful that {@code store} may be shared between nodes in a block. Passing a copied store to
+     * avoid the accident changing.
      *
      * @param node the given node
      * @param store the transfer input

dataflow/src/main/java/org/checkerframework/dataflow/analysis/Analysis.java

@@ -59,18 +59,22 @@ enum Direction {
     /**
      * Runs the analysis again within the block of {@code node} and returns the store at the
      * location of {@code node}. If {@code before} is true, then the store immediately before the
-     * {@link Node} {@code node} is returned. Otherwise, the store after {@code node} is returned.
-     * If {@code analysisCaches} is not null, this method uses a cache. {@code analysisCaches} is a
-     * map of a block of node to the cached analysis result. If the cache for {@code transferInput}
-     * is not in {@code analysisCaches}, this method create new cache and store it in {@code
-     * analysisCaches}. The cache is a map of a node to the analysis result of the node.
+     * {@link Node} {@code node} is returned. Otherwise, the store immediately after {@code node} is
+     * returned. If {@code analysisCaches} is not null, this method uses a cache. {@code
+     * analysisCaches} is a map of a block of node to the cached analysis result. If the cache for
+     * {@code transferInput} is not in {@code analysisCaches}, this method creates new cache and
+     * stores it in {@code analysisCaches}. The cache is a map of nodes to the analysis results of
+     * the nodes.
      *
      * @param node the node to analyze
-     * @param before the boolean value to indicate which store to return
+     * @param before the boolean value to indicate which store to return (if it is true, return the
+     *     store immediately before {@code node}; otherwise, the store after {@code node} is
+     *     returned)
      * @param transferInput the transfer input of the block of this node
      * @param nodeValues abstract values of nodes
      * @param analysisCaches caches of analysis results
-     * @return the store at the location of node after running the analysis
+     * @return the store before or after {@code node} (depends on the value of {@code before}) after
+     *     running the analysis
      */
     S runAnalysisFor(
             Node node,

dataflow/src/main/java/org/checkerframework/dataflow/analysis/AnalysisResult.java

@@ -8,7 +8,6 @@
 import java.util.Map;
 import java.util.Set;
 import javax.lang.model.element.Element;
-import javax.swing.*;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.dataflow.cfg.block.Block;
 import org.checkerframework.dataflow.cfg.block.ExceptionBlock;
@@ -133,7 +132,7 @@ public void combine(AnalysisResult<V, S> other) {
      * Merge all entries from otherTreeLookup into treeLookup. Merge sets if already present.
      *
      * @param treeLookup a map from abstract syntax trees to sets of nodes
-     * @param otherTreeLookup another treeLookup waiting for being merged into {@code treeLookup}
+     * @param otherTreeLookup another treeLookup that will be merged into {@code treeLookup}
      */
     private static void mergeTreeLookup(
             IdentityHashMap<Tree, Set<Node>> treeLookup,
@@ -394,8 +393,11 @@ public S getStoreAfter(Block bb) {
      * is returned.
      *
      * @param node the node to analyze
-     * @param before the boolean value to indicate which store to return
-     * @return the store at the location of node after running the analysis
+     * @param before the boolean value to indicate which store to return (if it is true, return the
+     *     store immediately before {@code node}; otherwise, the store after {@code node} is
+     *     returned)
+     * @return the store before or after {@code node} (depends on the value of {@code before}) after
+     *     running the analysis
      */
     protected @Nullable S runAnalysisFor(Node node, boolean before) {
         Block block = node.getBlock();
@@ -410,21 +412,24 @@ public S getStoreAfter(Block bb) {
     /**
      * Runs the analysis again within the block of {@code node} and returns the store at the
      * location of {@code node}. If {@code before} is true, then the store immediately before the
-     * {@link Node} {@code node} is returned. Otherwise, the store after {@code node} is returned.
-     * If {@code analysisCaches} is not null, this method uses a cache. {@code analysisCaches} is a
-     * map to a cache for analysis result from an input of the block of the node. If the cache for
-     * {@code transferInput} is not in {@code analysisCaches}, this method create new cache and
-     * store it in {@code analysisCaches}. The cache is a map from a node to the analysis result of
-     * the node.
+     * {@link Node} {@code node} is returned. Otherwise, the store immediately after {@code node} is
+     * returned. If {@code analysisCaches} is not null, this method uses a cache. {@code
+     * analysisCaches} is a map of a block of node to the cached analysis result. If the cache for
+     * {@code transferInput} is not in {@code analysisCaches}, this method creates new cache and
+     * stores it in {@code analysisCaches}. The cache is a map of nodes to the analysis results of
+     * the nodes.
      *
      * @param <V> the abstract value type to be tracked by the analysis
      * @param <S> the store type used in the analysis
-     * @param node a node
-     * @param before indicate before or after the node
+     * @param node the node to analyze
+     * @param before the boolean value to indicate which store to return (if it is true, return the
+     *     store immediately before {@code node}; otherwise, the store after {@code node} is
+     *     returned)
      * @param transferInput a transfer input
      * @param nodeValues {@link #nodeValues}
      * @param analysisCaches {@link #analysisCaches}
-     * @return store immediately before or after the given node
+     * @return the store before or after {@code node} (depends on the value of {@code before}) after
+     *     running the analysis
      */
     public static <V extends AbstractValue<V>, S extends Store<S>> S runAnalysisFor(
             Node node,

dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java

@@ -33,6 +33,8 @@ public class BackwardAnalysisImpl<
                 T extends BackwardTransferFunction<V, S>>
         extends AbstractAnalysis<V, S, T> implements BackwardAnalysis<V, S, T> {
 
+    // TODO: Add widening support like what the forward analysis does.
+
     /** Out stores after every basic block (assumed to be 'no information' if not present). */
     protected final IdentityHashMap<Block, S> outStores;
 
@@ -342,7 +344,9 @@ public S runAnalysisFor(
                             if (n == node && !before) {
                                 return store.getRegularStore();
                             }
-                            TransferResult<V, S> transferResult = callTransferFunction(n, store);
+                            // Copy the store to preserve to change the state in {@link #inputs}
+                            TransferResult<V, S> transferResult =
+                                    callTransferFunction(n, store.copy());
                             if (n == node) {
                                 return transferResult.getRegularStore();
                             }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/AbstractCFGVisualizer.java

@@ -249,18 +249,17 @@ protected List<Node> addBlockContent(Block bb) {
     }
 
     /**
-     * Visualize the transfer input before a block.
+     * Visualize the transfer input before the given block.
      *
      * @param bb the block
      * @param analysis the current analysis
      * @param escapeString the escape String for the special need of visualization, e.g., "\\l" for
      *     {@link DOTCFGVisualizer} to keep line left-justification, "\n" for {@link
      *     StringCFGVisualizer} to simply add a new line
-     * @return the String representation of the transfer input of the block
+     * @return the visualization of the transfer input before the given block
      */
     protected String visualizeBlockTransferInputBeforeHelper(
             Block bb, Analysis<V, S, T> analysis, String escapeString) {
-
         if (analysis == null) {
             throw new BugInCF(
                     "analysis must be non-null when visualizing the transfer input of a block.");
@@ -302,14 +301,14 @@ protected String visualizeBlockTransferInputBeforeHelper(
     }
 
     /**
-     * Visualize the transfer input after the block.
+     * Visualize the transfer input after the given block.
      *
-     * @param bb the block
+     * @param bb the given block
      * @param analysis the current analysis
      * @param escapeString the escape String for the special need of visualization, e.g., "\\l" for
      *     {@link DOTCFGVisualizer} to keep line left-justification, "\n" for {@link
      *     StringCFGVisualizer} to simply add a new line
-     * @return the String representation of the transfer input of the block
+     * @return the visualization of the transfer input after the given block
      */
     protected String visualizeBlockTransferInputAfterHelper(
             Block bb, Analysis<V, S, T> analysis, String escapeString) {