Add reaching definitions analysis (opprop#181)

.gitignore

@@ -150,6 +150,8 @@ dataflow/tests/issue3447/Out.txt
 dataflow/tests/issue3447/*.class
 dataflow/tests/live-variable/Out.txt
 dataflow/tests/live-variable/*.class
+dataflow/tests/reachingdef/Out.txt
+dataflow/tests/reachingdef/*.class
 
 checker/jtreg/multipleexecutions/Main.class
 

dataflow/build.gradle

@@ -128,6 +128,7 @@ def testDataflowAnalysis(taskName, dirName, className, diff) {
 testDataflowAnalysis("busyExpressionTest", "busyexpr", "busyexpr.BusyExpression", true)
 testDataflowAnalysis("liveVariableTest", "live-variable", "livevar.LiveVariable", true)
 testDataflowAnalysis("issue3447Test", "issue3447", "livevar.LiveVariable", false)
+testDataflowAnalysis("reachingDefinitionTest", "reachingdef", "reachingdef.ReachingDefinition", true)
 
 apply from: rootProject.file("gradle-mvn-push.gradle")
 

dataflow/manual/content.tex

@@ -1782,6 +1782,31 @@ \section{Example: Very Busy Expression Analysis}
 
 \flow{BusyExprSimple}{.33}{1}{Very Busy Expression Analysis illustration. Intermediate analysis results are shown.}
 
+\section{Example: Reaching Definition Analysis}
+
+The reaching definitions for a given program point are those assignments that
+may have updated the current values of variables.
+This reaching definition analysis is a standard example of a forward analysis.
+
+\textbf{Abstract values.} A class \code{ReachingDefinitionNode} is used as an
+abstract value, which can only wrap \code{AssignmentNode}. The reaching definition analysis
+processes such values in the store.
+
+\textbf{The store.} The reaching definition store \code{ReachingDefinitionStore} has a field
+\code{reachingDefSet} which contains a set of \code{ReachingDefinitionNode}s. The store defines methods
+\code{putDef(ReachingDefinitionValue)} and \code{killDef(Node)} to add
+and kill reaching definitions.
+
+\textbf{The transfer function.} The transfer function visits \code{AssignmentNode} to
+update the information of reaching definitions in the stores. A reaching definition will
+be killed in the store when its left-hand side is same as that of the new generated value, and the new
+generated value will be added into the store.
+
+\textbf{Example.} An example is shown in \autoref{fig:ReachSimple}.
+
+\flow{ReachSimple}{.33}{1}{Simple sequential program to illustrate reaching definitions.  Intermediate analysis results are shown.}
+
+
 \section{Default Analysis}
 
 

dataflow/manual/examples/ReachSimple.java

@@ -0,0 +1,12 @@
+class Test {
+  public void test() {
+    int a = 1, b = 2, c = 3;
+    if (a > 0) {
+      int d = a + c;
+    } else {
+      int e = a + b;
+    }
+    b = 0;
+    a = b;
+  }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/playground/ReachingDefinitionPlayground.java

@@ -0,0 +1,33 @@
+package org.checkerframework.dataflow.cfg.playground;
+
+import org.checkerframework.dataflow.analysis.ForwardAnalysis;
+import org.checkerframework.dataflow.analysis.ForwardAnalysisImpl;
+import org.checkerframework.dataflow.analysis.UnusedAbstractValue;
+import org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher;
+import org.checkerframework.dataflow.reachingdef.ReachingDefinitionStore;
+import org.checkerframework.dataflow.reachingdef.ReachingDefinitionTransfer;
+
+/** The playground of reaching definition analysis. */
+public class ReachingDefinitionPlayground {
+    /**
+     * Run reaching definition analysis for a specific file and create a PDF of the CFG in the end.
+     *
+     * @param args input arguments, not used
+     */
+    public static void main(String[] args) {
+
+        /* Configuration: change as appropriate */
+        String inputFile =
+                "./dataflow/manual/examples/ReachSimple.java"; // input file name and path
+        String outputDir = "."; // output directory
+        String method = "test"; // name of the method to analyze
+        String clazz = "Test"; // name of the class to consider
+
+        // Run the analysis and create a PDF file
+        ReachingDefinitionTransfer transfer = new ReachingDefinitionTransfer();
+        ForwardAnalysis<UnusedAbstractValue, ReachingDefinitionStore, ReachingDefinitionTransfer>
+                forwardAnalysis = new ForwardAnalysisImpl<>(transfer);
+        CFGVisualizeLauncher.generateDOTofCFG(
+                inputFile, outputDir, method, clazz, true, true, forwardAnalysis);
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionNode.java

@@ -0,0 +1,49 @@
+package org.checkerframework.dataflow.reachingdef;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.cfg.node.AssignmentNode;
+
+/**
+ * A ReachingDefinitionNode contains a CFG node, which can only be a AssignmentNode. It is used to
+ * represent the estimate of a reaching definition 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 reaching definition in the program) to be regarded as the same here.
+ */
+public class ReachingDefinitionNode {
+
+    /**
+     * A reaching definition is represented by a node, which can only be a {@link
+     * org.checkerframework.dataflow.cfg.node.AssignmentNode}.
+     */
+    protected final AssignmentNode def;
+
+    /**
+     * Create a new reaching definition.
+     *
+     * @param n an assignment node
+     */
+    public ReachingDefinitionNode(AssignmentNode n) {
+        this.def = n;
+    }
+
+    @Override
+    public int hashCode() {
+        return this.def.hashCode();
+    }
+
+    @Override
+    public boolean equals(@Nullable Object obj) {
+        if (!(obj instanceof ReachingDefinitionNode)) {
+            return false;
+        }
+        ReachingDefinitionNode other = (ReachingDefinitionNode) obj;
+        // We use `.equals` instead of `==` here to compare value equality.
+        return this.def.equals(other.def);
+    }
+
+    @Override
+    public String toString() {
+        return this.def.toString();
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionStore.java

@@ -0,0 +1,122 @@
+package org.checkerframework.dataflow.reachingdef;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.analysis.Store;
+import org.checkerframework.dataflow.cfg.node.Node;
+import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer;
+import org.checkerframework.dataflow.expression.JavaExpression;
+import org.checkerframework.javacutil.BugInCF;
+
+import java.util.Iterator;
+import java.util.LinkedHashSet;
+import java.util.Set;
+import java.util.StringJoiner;
+
+/**
+ * A reaching definition store contains a set of reaching definitions represented by
+ * ReachingDefinitionNode
+ */
+public class ReachingDefinitionStore implements Store<ReachingDefinitionStore> {
+
+    /** The set of reaching definitions in this store */
+    private final Set<ReachingDefinitionNode> reachingDefSet;
+
+    /** Create a new ReachDefinitionStore. */
+    public ReachingDefinitionStore() {
+        reachingDefSet = new LinkedHashSet<>();
+    }
+
+    /**
+     * Create a new ReachDefinitionStore.
+     *
+     * @param reachingDefSet a set of reaching definition nodes. The parameter is captured and the
+     *     caller should not retain an alias.
+     */
+    public ReachingDefinitionStore(LinkedHashSet<ReachingDefinitionNode> reachingDefSet) {
+        this.reachingDefSet = reachingDefSet;
+    }
+
+    /**
+     * Remove the information of a reaching definition from the reaching definition set.
+     *
+     * @param defTarget target of a reaching definition
+     */
+    public void killDef(Node defTarget) {
+        Iterator<ReachingDefinitionNode> it = reachingDefSet.iterator();
+        while (it.hasNext()) {
+            // We use `.equals` instead of `==` here to compare value equality
+            // rather than reference equality, because if two left-hand side node
+            // have same values, we need to kill the old one and replace with the
+            // new one.
+            ReachingDefinitionNode generatedDefNode = it.next();
+            if (generatedDefNode.def.getTarget().equals(defTarget)) {
+                it.remove();
+            }
+        }
+    }
+
+    /**
+     * Add a reaching definition to the reaching definition set.
+     *
+     * @param def a reaching definition
+     */
+    public void putDef(ReachingDefinitionNode def) {
+        reachingDefSet.add(def);
+    }
+
+    @Override
+    public boolean equals(@Nullable Object obj) {
+        if (!(obj instanceof ReachingDefinitionStore)) {
+            return false;
+        }
+        ReachingDefinitionStore other = (ReachingDefinitionStore) obj;
+        return other.reachingDefSet.equals(this.reachingDefSet);
+    }
+
+    @Override
+    public int hashCode() {
+        return this.reachingDefSet.hashCode();
+    }
+
+    @Override
+    public ReachingDefinitionStore copy() {
+        return new ReachingDefinitionStore(new LinkedHashSet<>(reachingDefSet));
+    }
+
+    @Override
+    public ReachingDefinitionStore leastUpperBound(ReachingDefinitionStore other) {
+        LinkedHashSet<ReachingDefinitionNode> reachingDefSetLub =
+                new LinkedHashSet<>(this.reachingDefSet.size() + other.reachingDefSet.size());
+        reachingDefSetLub.addAll(this.reachingDefSet);
+        reachingDefSetLub.addAll(other.reachingDefSet);
+        return new ReachingDefinitionStore(reachingDefSetLub);
+    }
+
+    @Override
+    public ReachingDefinitionStore widenedUpperBound(ReachingDefinitionStore previous) {
+        throw new BugInCF("ReachingDefinitionStore.widenedUpperBound was called!");
+    }
+
+    @Override
+    public boolean canAlias(JavaExpression a, JavaExpression b) {
+        return true;
+    }
+
+    @Override
+    public String visualize(CFGVisualizer<?, ReachingDefinitionStore, ?> viz) {
+        String key = "reaching definitions";
+        if (reachingDefSet.isEmpty()) {
+            return viz.visualizeStoreKeyVal(key, "none");
+        }
+        StringJoiner sjStoreVal = new StringJoiner(", ", "{ ", " }");
+        for (ReachingDefinitionNode reachDefNode : reachingDefSet) {
+            sjStoreVal.add(reachDefNode.toString());
+        }
+        return viz.visualizeStoreKeyVal(key, sjStoreVal.toString());
+    }
+
+    @Override
+    public String toString() {
+        return "ReachingDefinitionStore: " + reachingDefSet.toString();
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionTransfer.java

@@ -0,0 +1,60 @@
+package org.checkerframework.dataflow.reachingdef;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.analysis.ForwardTransferFunction;
+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;
+import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
+import org.checkerframework.dataflow.cfg.node.Node;
+
+import java.util.List;
+
+/**
+ * The reaching definition transfer function. The transfer function processes the
+ * ReachingDefinitionNode in ReachingDefinitionStore, killing the node with same LHS and putting new
+ * generated node into the store. See dataflow manual for more details.
+ */
+public class ReachingDefinitionTransfer
+        extends AbstractNodeVisitor<
+                TransferResult<UnusedAbstractValue, ReachingDefinitionStore>,
+                TransferInput<UnusedAbstractValue, ReachingDefinitionStore>>
+        implements ForwardTransferFunction<UnusedAbstractValue, ReachingDefinitionStore> {
+
+    @Override
+    public ReachingDefinitionStore initialStore(
+            UnderlyingAST underlyingAST, @Nullable List<LocalVariableNode> parameters) {
+        return new ReachingDefinitionStore();
+    }
+
+    @Override
+    public RegularTransferResult<UnusedAbstractValue, ReachingDefinitionStore> visitNode(
+            Node n, TransferInput<UnusedAbstractValue, ReachingDefinitionStore> p) {
+        return new RegularTransferResult<>(null, p.getRegularStore());
+    }
+
+    @Override
+    public RegularTransferResult<UnusedAbstractValue, ReachingDefinitionStore> visitAssignment(
+            AssignmentNode n, TransferInput<UnusedAbstractValue, ReachingDefinitionStore> p) {
+        RegularTransferResult<UnusedAbstractValue, ReachingDefinitionStore> transferResult =
+                (RegularTransferResult<UnusedAbstractValue, ReachingDefinitionStore>)
+                        super.visitAssignment(n, p);
+        processDefinition(n, transferResult.getRegularStore());
+        return transferResult;
+    }
+
+    /**
+     * Update a reaching definition node in the store from an assignment statement.
+     *
+     * @param def the definition that should be put into the store
+     * @param store the reaching definition store
+     */
+    private void processDefinition(AssignmentNode def, ReachingDefinitionStore store) {
+        store.killDef(def.getTarget());
+        store.putDef(new ReachingDefinitionNode(def));
+    }
+}

dataflow/src/test/java/reachingdef/ReachingDefinition.java

@@ -0,0 +1,30 @@
+package reachingdef;
+
+import org.checkerframework.dataflow.analysis.ForwardAnalysis;
+import org.checkerframework.dataflow.analysis.ForwardAnalysisImpl;
+import org.checkerframework.dataflow.analysis.UnusedAbstractValue;
+import org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher;
+import org.checkerframework.dataflow.reachingdef.ReachingDefinitionStore;
+import org.checkerframework.dataflow.reachingdef.ReachingDefinitionTransfer;
+
+/** Used in reachingDefinitionsTest Gradle task to test the ReachingDefinition analysis. */
+public class ReachingDefinition {
+
+    /**
+     * The main method expects to be run in dataflow/tests/reaching-definitions directory.
+     *
+     * @param args not used
+     */
+    public static void main(String[] args) {
+
+        String inputFile = "Test.java";
+        String method = "test";
+        String clas = "Test";
+        String outputFile = "Out.txt";
+
+        ReachingDefinitionTransfer transfer = new ReachingDefinitionTransfer();
+        ForwardAnalysis<UnusedAbstractValue, ReachingDefinitionStore, ReachingDefinitionTransfer>
+                forwardAnalysis = new ForwardAnalysisImpl<>(transfer);
+        CFGVisualizeLauncher.writeStringOfCFG(inputFile, method, clas, outputFile, forwardAnalysis);
+    }
+}