Introduce backward analysis to dataflow framework.

changelog.txt

@@ -28,6 +28,8 @@ The Nullness Checker now treats `System.getProperty()` soundly.  Use
 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:
@@ -37,6 +39,13 @@ Changed the types of some fields and methods from array to List:
  * QualifierDefaults.STANDARD_UNCHECKED_DEFAULTS_TOP
  * QualifierDefaults.STANDARD_UNCHECKED_DEFAULTS_BOTTOM
 
+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.
 

dataflow/manual/content.tex

@@ -378,7 +378,13 @@ \subsubsubsection{TransferFunction}
 package org.checkerframework.dataflow.analysis;
 interface TransferFunction<V extends AbstractValue<V>,
         S extends Store<S>>
-    extends NodeVisitor<TransferResult<A, S>, TransferInput<A, S>>
+    extends NodeVisitor<TransferResult<V, S>, TransferInput<V, S>>
+interface ForwardTransferFunction<V extends AbstractValue<V>,
+        S extends Store<S>>
+    extends TransferFunction<V, S>
+interface BackwardTransferFunction<V extends AbstractValue<V>,
+        S extends Store<S>>
+    extends TransferFunction<V, S>
 \end{verbatim}
 
 The Checker Framework defines a derived class of TransferFunction to
@@ -392,7 +398,7 @@ \subsubsubsection{TransferFunction}
         S extends CFAbstractStore<V, S>,
         T extends CFAbstractTransfer<V, S, T>>
     extends AbstractNodeVisitor<TransferResult<V, S>, TransferInput<V, S>>
-    implements TransferFunction<V, S>
+    implements ForwardTransferFunction<V, S>
 
 class CFTransfer extends CFAbstractTransfer<CFValue, CFStore, CFTransfer>
 \end{verbatim}
@@ -421,14 +427,26 @@ \subsubsection{Analysis}
 \label{sec:analysis_classes}
 
 An Analysis performs iterative dataflow analysis over a control flow
-graph using a given transfer function.  Currently only forward
+graph using a given transfer function.  Both forward and backward
 analyses are supported.
 
 \begin{verbatim}
 package org.checkerframework.dataflow.analysis;
-class Analysis<V extends AbstractValue<V>,
+interface Analysis<V extends AbstractValue<V>,
+        S extends Store<S>,
+        T extends TransferFunction<V, S>>
+abstract class AbstractAnalysis<V extends AbstractValue<V>,
+        S extends Store<S>,
+        T extends TransferFunction<V, S>>
+    implements Analysis<V, S, T>
+interface ForwardAnalysis<V extends AbstractValue<V>,
         S extends Store<S>,
-        T extends TransferFunction<A, S>>
+        T extends ForwardTransferFunction<V, S>>
+    extends Analysis<V, S, T>
+interface BackwardAnalysis<V extends AbstractValue<V>,
+        S extends Store<S>,
+        T extends BackwardTransferFunction<V, S>>
+    extends Analysis<V, S, T>
 \end{verbatim}
 
 The Checker Framework defines a derived class of Analysis for use as
@@ -441,7 +459,7 @@ \subsubsection{Analysis}
 abstract class CFAbstractAnalysis<V extends CFAbstractValue<V>,
         S extends CFAbstractStore<V, S>,
         T extends CFAbstractTransfer<V, S, T>>
-    extends Analysis<V, S, T>
+    extends ForwardAnalysisImpl<V, S, T>
 
 class CFAnalysis extends CFAbstractAnalysis<CFValue, CFStore, CFTransfer>
 \end{verbatim}
@@ -1408,13 +1426,11 @@ \subsection{Overview}
 Roughly, a dataflow analysis in the framework works as follows. Given
 the abstract syntax tree of a method, the framework computes the
 corresponding control-flow graph as described in
-\autoref{sec:cfg}. Then, a simple forward iterative algorithm is used
-to compute a fix-point, by iteratively applying a set of transfer
-functions to the nodes in the CFG\@.  (For our initial application,
-type-checking, we do not need to support backwards analyses; in the
-future, we may wish to do so.)  These transfer functions are specific
-to the particular analysis and are used to approximate the runtime
-behavior of different statements and expressions.
+\autoref{sec:cfg}. Then, a simple forward or backward iterative
+algorithm is used to compute a fix-point, by iteratively applying a
+set of transfer functions to the nodes in the CFG\@.  These transfer
+functions are specific to the particular analysis and are used to
+approximate the runtime behavior of different statements and expressions.
 
 An analysis result contains two parts: