Add UnusedAbstractValue and improve LiveVarAnalysis (#203)

Co-authored-by: Werner Dietl <wdietl@gmail.com> Co-authored-by: zcai <z44cai@uwaterloo.ca>
eisop · Apr 10, 2022 · 4a1e09d · 4a1e09d
1 parent 567084f
commit 4a1e09d
Show file tree

Hide file tree

Showing 7 changed files with 111 additions and 63 deletions.
diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex
@@ -299,6 +299,25 @@ \subsubsection{AbstractValue}
 class NullnessValue extends CFAbstractValue<NullnessValue>
 \end{verbatim}
 
+\subsubsection{UnusedAbstractValue}
+\label{sec:unused_abstract_value_class}
+
+UnusedAbstractValue, as the name suggests, is an AbstractValue that is
+not involved in any computation during dataflow analysis. This class should
+only be used as a type argument in transfer functions. It is implemented because some
+analyses do not need and do not have their own AbstractValue classes.
+
+For example, in LiveVariable analysis (\autoref{sec:live_variable}),
+we need to compute the least upper bound of successors' stores, and
+it is meaningless to further calculate the least upper bound of two
+individual live variables at a smaller granularity.
+Since there is no computation between two AbstractValues, using the UnusedAbstractValue
+is sufficient and we do not have to implement a specific AbstractValue for this analysis.
+
+\begin{verbatim}
+package org.checkerframework.dataflow.analysis;
+public final class UnusedAbstractValue implements AbstractValue<UnusedAbstractValue>
+\end{verbatim}
 
 \subsubsection{Store}
 \label{sec:store_classes}
@@ -1710,7 +1729,7 @@ \section{Example: Constant Propagation}
 
 
 \section{Example: Live Variable}
-
+\label{sec:live_variable}
 A live variable analysis for local variables and fields was implemented
 to show the backward analysis works properly. The main class is
 \code{org.checkerframework.dataflow.cfg.playground.LiveVariablePlayground}.
@@ -1729,7 +1748,7 @@ \section{Example: Live Variable}
 \textbf{The transfer function.} The transfer function \code{LiveVarTransfer}
 initializes empty stores at normal and exceptional exit blocks (because this
 is a backward transfer function). The transfer function visits assignments to
-update the information of live variables for each node in the stores.
+update the live variable values in the stores.
 
 \textbf{Example.} An example is shown in \autoref{fig:LiveSimple}.
 

diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/UnusedAbstractValue.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/UnusedAbstractValue.java
@@ -0,0 +1,23 @@
+package org.checkerframework.dataflow.analysis;
+
+import org.checkerframework.javacutil.BugInCF;
+
+/**
+ * UnusedAbstractValue is an AbstractValue that is not involved in any lub computation during
+ * dataflow analysis. For those analyses which handle lub computation at a higher level (e.g., store
+ * level), it is sufficient to use UnusedAbstractValue and unnecessary to implement another specific
+ * AbstractValue. Example analysis using UnusedAbstractValue is LiveVariable analysis. This is a
+ * workaround for issue https://github.com/eisop/checker-framework/issues/200
+ */
+public final class UnusedAbstractValue implements AbstractValue<UnusedAbstractValue> {
+
+    /** This class cannot be instantiated */
+    private UnusedAbstractValue() {
+        throw new AssertionError("Class UnusedAbstractValue cannot be instantiated.");
+    }
+
+    @Override
+    public UnusedAbstractValue leastUpperBound(UnusedAbstractValue other) {
+        throw new BugInCF("UnusedAbstractValue.leastUpperBound was called!");
+    }
+}
diff --git a/...ow/src/main/java/org/checkerframework/dataflow/cfg/playground/LiveVariablePlayground.java b/...ow/src/main/java/org/checkerframework/dataflow/cfg/playground/LiveVariablePlayground.java
@@ -2,10 +2,10 @@
 
 import org.checkerframework.dataflow.analysis.BackwardAnalysis;
 import org.checkerframework.dataflow.analysis.BackwardAnalysisImpl;
+import org.checkerframework.dataflow.analysis.UnusedAbstractValue;
 import org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher;
 import org.checkerframework.dataflow.livevariable.LiveVarStore;
 import org.checkerframework.dataflow.livevariable.LiveVarTransfer;
-import org.checkerframework.dataflow.livevariable.LiveVarValue;
 
 /** The playground of live variable analysis. */
 public class LiveVariablePlayground {
@@ -25,7 +25,7 @@ public static void main(String[] args) {
 
         // Run the analysis and create a PDF file
         LiveVarTransfer transfer = new LiveVarTransfer();
-        BackwardAnalysis<LiveVarValue, LiveVarStore, LiveVarTransfer> backwardAnalysis =
+        BackwardAnalysis<UnusedAbstractValue, LiveVarStore, LiveVarTransfer> backwardAnalysis =
                 new BackwardAnalysisImpl<>(transfer);
         CFGVisualizeLauncher.generateDOTofCFG(
                 inputFile, outputDir, method, clazz, true, true, backwardAnalysis);

diff --git a/...k/dataflow/livevariable/LiveVarValue.java → ...rk/dataflow/livevariable/LiveVarNode.java b/...k/dataflow/livevariable/LiveVarValue.java → ...rk/dataflow/livevariable/LiveVarNode.java
@@ -1,12 +1,18 @@
 package org.checkerframework.dataflow.livevariable;
 
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.analysis.AbstractValue;
+import org.checkerframework.dataflow.cfg.node.FieldAccessNode;
+import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
 import org.checkerframework.dataflow.cfg.node.Node;
-import org.checkerframework.javacutil.BugInCF;
 
-/** A live variable (which is represented by a node) wrapper turning node into abstract value. */
-public class LiveVarValue implements AbstractValue<LiveVarValue> {
+/**
+ * A LiveVarNode contains a CFG node, which can only be a LocalVariableNode or FieldAccessNode. It
+ * is used to represent the estimate of live variables at certain CFG block during dataflow
+ * analysis. We override `.equals` in this class to compare Nodes by value equality rather than
+ * reference equality. We want two different nodes with the same values (that is, the two nodes
+ * refer to the same live variable in the program) to be regarded as the same here.
+ */
+public class LiveVarNode {
 
     /**
      * A live variable is represented by a node, which can be a {@link
@@ -15,17 +21,13 @@ public class LiveVarValue implements AbstractValue<LiveVarValue> {
      */
     protected final Node liveVariable;
 
-    @Override
-    public LiveVarValue leastUpperBound(LiveVarValue other) {
-        throw new BugInCF("lub of LiveVar get called!");
-    }
-
     /**
      * Create a new live variable.
      *
      * @param n a node
      */
-    public LiveVarValue(Node n) {
+    public LiveVarNode(Node n) {
+        assert n instanceof FieldAccessNode || n instanceof LocalVariableNode;
         this.liveVariable = n;
     }
 
@@ -36,10 +38,11 @@ public int hashCode() {
 
     @Override
     public boolean equals(@Nullable Object obj) {
-        if (!(obj instanceof LiveVarValue)) {
+        if (!(obj instanceof LiveVarNode)) {
             return false;
         }
-        LiveVarValue other = (LiveVarValue) obj;
+        LiveVarNode other = (LiveVarNode) obj;
+        // We use `.equals` instead of `==` here to compare value equality.
         return this.liveVariable.equals(other.liveVariable);
     }
 

diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java b/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java
@@ -14,47 +14,47 @@
 import org.checkerframework.dataflow.expression.JavaExpression;
 import org.checkerframework.javacutil.BugInCF;
 
-import java.util.HashSet;
 import java.util.LinkedHashSet;
 import java.util.Set;
 import java.util.StringJoiner;
 
 /** A live variable store contains a set of live variables represented by nodes. */
 public class LiveVarStore implements Store<LiveVarStore> {
 
-    /** A set of live variable abstract values. */
-    private final Set<LiveVarValue> liveVarValueSet;
+    /** The set of live variables in this store */
+    private final Set<LiveVarNode> liveVarNodeSet;
 
     /** Create a new LiveVarStore. */
     public LiveVarStore() {
-        liveVarValueSet = new LinkedHashSet<>();
+        liveVarNodeSet = new LinkedHashSet<>();
     }
 
     /**
      * Create a new LiveVarStore.
      *
-     * @param liveVarValueSet a set of live variable abstract values
+     * @param liveVarNodeSet the set of live variable nodes. The parameter is captured and the
+     *     caller should not retain an alias.
      */
-    public LiveVarStore(Set<LiveVarValue> liveVarValueSet) {
-        this.liveVarValueSet = liveVarValueSet;
+    public LiveVarStore(Set<LiveVarNode> liveVarNodeSet) {
+        this.liveVarNodeSet = liveVarNodeSet;
     }
 
     /**
      * Add the information of a live variable into the live variable set.
      *
      * @param variable a live variable
      */
-    public void putLiveVar(LiveVarValue variable) {
-        liveVarValueSet.add(variable);
+    public void putLiveVar(LiveVarNode variable) {
+        liveVarNodeSet.add(variable);
     }
 
     /**
      * Remove the information of a live variable from the live variable set.
      *
      * @param variable a live variable
      */
-    public void killLiveVar(LiveVarValue variable) {
-        liveVarValueSet.remove(variable);
+    public void killLiveVar(LiveVarNode variable) {
+        liveVarNodeSet.remove(variable);
     }
 
     /**
@@ -65,7 +65,7 @@ public void killLiveVar(LiveVarValue variable) {
     public void addUseInExpression(Node expression) {
         // TODO Do we need a AbstractNodeScanner to do the following job?
         if (expression instanceof LocalVariableNode || expression instanceof FieldAccessNode) {
-            LiveVarValue liveVarValue = new LiveVarValue(expression);
+            LiveVarNode liveVarValue = new LiveVarNode(expression);
             putLiveVar(liveVarValue);
         } else if (expression instanceof UnaryOperationNode) {
             UnaryOperationNode unaryNode = (UnaryOperationNode) expression;
@@ -94,25 +94,25 @@ public boolean equals(@Nullable Object obj) {
             return false;
         }
         LiveVarStore other = (LiveVarStore) obj;
-        return other.liveVarValueSet.equals(this.liveVarValueSet);
+        return other.liveVarNodeSet.equals(this.liveVarNodeSet);
     }
 
     @Override
     public int hashCode() {
-        return this.liveVarValueSet.hashCode();
+        return this.liveVarNodeSet.hashCode();
     }
 
     @Override
     public LiveVarStore copy() {
-        return new LiveVarStore(new HashSet<>(liveVarValueSet));
+        return new LiveVarStore(new LinkedHashSet<>(liveVarNodeSet));
     }
 
     @Override
     public LiveVarStore leastUpperBound(LiveVarStore other) {
-        Set<LiveVarValue> liveVarValueSetLub =
-                new HashSet<>(this.liveVarValueSet.size() + other.liveVarValueSet.size());
-        liveVarValueSetLub.addAll(this.liveVarValueSet);
-        liveVarValueSetLub.addAll(other.liveVarValueSet);
+        Set<LiveVarNode> liveVarValueSetLub =
+                new LinkedHashSet<>(this.liveVarNodeSet.size() + other.liveVarNodeSet.size());
+        liveVarValueSetLub.addAll(this.liveVarNodeSet);
+        liveVarValueSetLub.addAll(other.liveVarNodeSet);
         return new LiveVarStore(liveVarValueSetLub);
     }
 
@@ -130,18 +130,18 @@ public boolean canAlias(JavaExpression a, JavaExpression b) {
     @Override
     public String visualize(CFGVisualizer<?, LiveVarStore, ?> viz) {
         String key = "live variables";
-        if (liveVarValueSet.isEmpty()) {
+        if (liveVarNodeSet.isEmpty()) {
             return viz.visualizeStoreKeyVal(key, "none");
         }
         StringJoiner sjStoreVal = new StringJoiner(", ");
-        for (LiveVarValue liveVarValue : liveVarValueSet) {
-            sjStoreVal.add(liveVarValue.toString());
+        for (LiveVarNode liveVar : liveVarNodeSet) {
+            sjStoreVal.add(liveVar.toString());
         }
         return viz.visualizeStoreKeyVal(key, sjStoreVal.toString());
     }
 
     @Override
     public String toString() {
-        return liveVarValueSet.toString();
+        return liveVarNodeSet.toString();
     }
 }
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarTransfer.java b/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarTransfer.java
@@ -4,6 +4,7 @@
 import org.checkerframework.dataflow.analysis.RegularTransferResult;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
+import org.checkerframework.dataflow.analysis.UnusedAbstractValue;
 import org.checkerframework.dataflow.cfg.UnderlyingAST;
 import org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor;
 import org.checkerframework.dataflow.cfg.node.AssignmentNode;
@@ -17,9 +18,9 @@
 /** A live variable transfer function. */
 public class LiveVarTransfer
         extends AbstractNodeVisitor<
-                TransferResult<LiveVarValue, LiveVarStore>,
-                TransferInput<LiveVarValue, LiveVarStore>>
-        implements BackwardTransferFunction<LiveVarValue, LiveVarStore> {
+                TransferResult<UnusedAbstractValue, LiveVarStore>,
+                TransferInput<UnusedAbstractValue, LiveVarStore>>
+        implements BackwardTransferFunction<UnusedAbstractValue, LiveVarStore> {
 
     @Override
     public LiveVarStore initialNormalExitStore(
@@ -33,26 +34,27 @@ public LiveVarStore initialExceptionalExitStore(UnderlyingAST underlyingAST) {
     }
 
     @Override
-    public RegularTransferResult<LiveVarValue, LiveVarStore> visitNode(
-            Node n, TransferInput<LiveVarValue, LiveVarStore> p) {
+    public RegularTransferResult<UnusedAbstractValue, LiveVarStore> visitNode(
+            Node n, TransferInput<UnusedAbstractValue, LiveVarStore> p) {
         return new RegularTransferResult<>(null, p.getRegularStore());
     }
 
     @Override
-    public RegularTransferResult<LiveVarValue, LiveVarStore> visitAssignment(
-            AssignmentNode n, TransferInput<LiveVarValue, LiveVarStore> p) {
-        RegularTransferResult<LiveVarValue, LiveVarStore> transferResult =
-                (RegularTransferResult<LiveVarValue, LiveVarStore>) super.visitAssignment(n, p);
+    public RegularTransferResult<UnusedAbstractValue, LiveVarStore> visitAssignment(
+            AssignmentNode n, TransferInput<UnusedAbstractValue, LiveVarStore> p) {
+        RegularTransferResult<UnusedAbstractValue, LiveVarStore> transferResult =
+                (RegularTransferResult<UnusedAbstractValue, LiveVarStore>)
+                        super.visitAssignment(n, p);
         processLiveVarInAssignment(
                 n.getTarget(), n.getExpression(), transferResult.getRegularStore());
         return transferResult;
     }
 
     @Override
-    public RegularTransferResult<LiveVarValue, LiveVarStore> visitMethodInvocation(
-            MethodInvocationNode n, TransferInput<LiveVarValue, LiveVarStore> p) {
-        RegularTransferResult<LiveVarValue, LiveVarStore> transferResult =
-                (RegularTransferResult<LiveVarValue, LiveVarStore>)
+    public RegularTransferResult<UnusedAbstractValue, LiveVarStore> visitMethodInvocation(
+            MethodInvocationNode n, TransferInput<UnusedAbstractValue, LiveVarStore> p) {
+        RegularTransferResult<UnusedAbstractValue, LiveVarStore> transferResult =
+                (RegularTransferResult<UnusedAbstractValue, LiveVarStore>)
                         super.visitMethodInvocation(n, p);
         LiveVarStore store = transferResult.getRegularStore();
         for (Node arg : n.getArguments()) {
@@ -62,10 +64,11 @@ public RegularTransferResult<LiveVarValue, LiveVarStore> visitMethodInvocation(
     }
 
     @Override
-    public RegularTransferResult<LiveVarValue, LiveVarStore> visitObjectCreation(
-            ObjectCreationNode n, TransferInput<LiveVarValue, LiveVarStore> p) {
-        RegularTransferResult<LiveVarValue, LiveVarStore> transferResult =
-                (RegularTransferResult<LiveVarValue, LiveVarStore>) super.visitObjectCreation(n, p);
+    public RegularTransferResult<UnusedAbstractValue, LiveVarStore> visitObjectCreation(
+            ObjectCreationNode n, TransferInput<UnusedAbstractValue, LiveVarStore> p) {
+        RegularTransferResult<UnusedAbstractValue, LiveVarStore> transferResult =
+                (RegularTransferResult<UnusedAbstractValue, LiveVarStore>)
+                        super.visitObjectCreation(n, p);
         LiveVarStore store = transferResult.getRegularStore();
         for (Node arg : n.getArguments()) {
             store.addUseInExpression(arg);
@@ -74,10 +77,10 @@ public RegularTransferResult<LiveVarValue, LiveVarStore> visitObjectCreation(
     }
 
     @Override
-    public RegularTransferResult<LiveVarValue, LiveVarStore> visitReturn(
-            ReturnNode n, TransferInput<LiveVarValue, LiveVarStore> p) {
-        RegularTransferResult<LiveVarValue, LiveVarStore> transferResult =
-                (RegularTransferResult<LiveVarValue, LiveVarStore>) super.visitReturn(n, p);
+    public RegularTransferResult<UnusedAbstractValue, LiveVarStore> visitReturn(
+            ReturnNode n, TransferInput<UnusedAbstractValue, LiveVarStore> p) {
+        RegularTransferResult<UnusedAbstractValue, LiveVarStore> transferResult =
+                (RegularTransferResult<UnusedAbstractValue, LiveVarStore>) super.visitReturn(n, p);
         Node result = n.getResult();
         if (result != null) {
             LiveVarStore store = transferResult.getRegularStore();
@@ -94,7 +97,7 @@ public RegularTransferResult<LiveVarValue, LiveVarStore> visitReturn(
      * @param store the live variable store
      */
     private void processLiveVarInAssignment(Node variable, Node expression, LiveVarStore store) {
-        store.killLiveVar(new LiveVarValue(variable));
+        store.killLiveVar(new LiveVarNode(variable));
         store.addUseInExpression(expression);
     }
 }
diff --git a/dataflow/src/test/java/livevar/LiveVariable.java b/dataflow/src/test/java/livevar/LiveVariable.java
@@ -2,10 +2,10 @@
 
 import org.checkerframework.dataflow.analysis.BackwardAnalysis;
 import org.checkerframework.dataflow.analysis.BackwardAnalysisImpl;
+import org.checkerframework.dataflow.analysis.UnusedAbstractValue;
 import org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher;
 import org.checkerframework.dataflow.livevariable.LiveVarStore;
 import org.checkerframework.dataflow.livevariable.LiveVarTransfer;
-import org.checkerframework.dataflow.livevariable.LiveVarValue;
 
 /** Used in liveVariableTest Gradle task to test the LiveVariable analysis. */
 public class LiveVariable {
@@ -22,7 +22,7 @@ public static void main(String[] args) {
         String outputFile = "Out.txt";
 
         LiveVarTransfer transfer = new LiveVarTransfer();
-        BackwardAnalysis<LiveVarValue, LiveVarStore, LiveVarTransfer> backwardAnalysis =
+        BackwardAnalysis<UnusedAbstractValue, LiveVarStore, LiveVarTransfer> backwardAnalysis =
                 new BackwardAnalysisImpl<>(transfer);
         CFGVisualizeLauncher.writeStringOfCFG(
                 inputFile, method, clas, outputFile, backwardAnalysis);