diff --git a/.gitignore b/.gitignore index cc9561bf9a8..d2710d03047 100644 --- a/.gitignore +++ b/.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 diff --git a/dataflow/build.gradle b/dataflow/build.gradle index f46d4b2fcc1..669bdb39341 100644 --- a/dataflow/build.gradle +++ b/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") diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex index 06bc9d6bedd..1a4d4cb3632 100644 --- a/dataflow/manual/content.tex +++ b/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} diff --git a/dataflow/manual/examples/ReachSimple.java b/dataflow/manual/examples/ReachSimple.java new file mode 100644 index 00000000000..cb349c355d9 --- /dev/null +++ b/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; + } +} diff --git a/dataflow/manual/examples/graphs/ReachSimple.pdf b/dataflow/manual/examples/graphs/ReachSimple.pdf new file mode 100644 index 00000000000..d656a8e64d3 Binary files /dev/null and b/dataflow/manual/examples/graphs/ReachSimple.pdf differ diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/playground/ReachingDefinitionPlayground.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/playground/ReachingDefinitionPlayground.java new file mode 100644 index 00000000000..e26502a7fd4 --- /dev/null +++ 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 + forwardAnalysis = new ForwardAnalysisImpl<>(transfer); + CFGVisualizeLauncher.generateDOTofCFG( + inputFile, outputDir, method, clazz, true, true, forwardAnalysis); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionNode.java new file mode 100644 index 00000000000..4488f47ef4f --- /dev/null +++ b/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(); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionStore.java b/dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionStore.java new file mode 100644 index 00000000000..1b66bb6965a --- /dev/null +++ b/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 { + + /** The set of reaching definitions in this store */ + private final Set 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 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 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 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 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(); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionTransfer.java b/dataflow/src/main/java/org/checkerframework/dataflow/reachingdef/ReachingDefinitionTransfer.java new file mode 100644 index 00000000000..c5e2916d24d --- /dev/null +++ b/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, + TransferInput> + implements ForwardTransferFunction { + + @Override + public ReachingDefinitionStore initialStore( + UnderlyingAST underlyingAST, @Nullable List parameters) { + return new ReachingDefinitionStore(); + } + + @Override + public RegularTransferResult visitNode( + Node n, TransferInput p) { + return new RegularTransferResult<>(null, p.getRegularStore()); + } + + @Override + public RegularTransferResult visitAssignment( + AssignmentNode n, TransferInput p) { + RegularTransferResult transferResult = + (RegularTransferResult) + 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)); + } +} diff --git a/dataflow/src/test/java/reachingdef/ReachingDefinition.java b/dataflow/src/test/java/reachingdef/ReachingDefinition.java new file mode 100644 index 00000000000..d55ce717c64 --- /dev/null +++ b/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 + forwardAnalysis = new ForwardAnalysisImpl<>(transfer); + CFGVisualizeLauncher.writeStringOfCFG(inputFile, method, clas, outputFile, forwardAnalysis); + } +} diff --git a/dataflow/tests/reachingdef/Expected.txt b/dataflow/tests/reachingdef/Expected.txt new file mode 100644 index 00000000000..471be89feb9 --- /dev/null +++ b/dataflow/tests/reachingdef/Expected.txt @@ -0,0 +1,107 @@ +2 -> 3 EACH_TO_EACH +3 -> 4 EACH_TO_EACH +4 -> 8 THEN_TO_BOTH +4 -> 10 ELSE_TO_BOTH +8 -> 11 EACH_TO_EACH +10 -> 11 EACH_TO_EACH +11 -> 0 EACH_TO_EACH + +2: +Process order: 1 +TransferInput#0 +Before: reaching definitions = none +~~~~~~~~~ + + +3: +Process order: 2 +TransferInput#1 +Before: reaching definitions = none +~~~~~~~~~ +a [ VariableDeclaration ] +1 [ IntegerLiteral ] +a = 1 [ Assignment ] +b [ VariableDeclaration ] +2 [ IntegerLiteral ] +b = 2 [ Assignment ] +c [ VariableDeclaration ] +3 [ IntegerLiteral ] +c = 3 [ Assignment ] +x [ VariableDeclaration ] +"a" [ StringLiteral ] +x = "a" [ Assignment ] +y [ VariableDeclaration ] +"b" [ StringLiteral ] +y = "b" [ Assignment ] +a [ LocalVariable ] +0 [ IntegerLiteral ] +(a > 0) [ GreaterThan ] +~~~~~~~~~ +AnalysisResult#1 +After: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b" } + +4: +Process order: 3 +TransferInput#21 +Before: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b" } +~~~~~~~~~ +ConditionalBlock: then: 8, else: 10 + +8: +Process order: 4 +TransferInput#23 +Before: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b" } +~~~~~~~~~ +d [ VariableDeclaration ] +a [ LocalVariable ] +c [ LocalVariable ] +(a + c) [ NumericalAddition ] +d = (a + c) [ Assignment ] +~~~~~~~~~ +AnalysisResult#3 +After: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b", d = (a + c) } + +10: +Process order: 5 +TransferInput#24 +Before: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b" } +~~~~~~~~~ +e [ VariableDeclaration ] +a [ LocalVariable ] +b [ LocalVariable ] +(a + b) [ NumericalAddition ] +e = (a + b) [ Assignment ] +~~~~~~~~~ +AnalysisResult#5 +After: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b", e = (a + b) } + +11: +Process order: 6 +TransferInput#38 +Before: reaching definitions = { a = 1, b = 2, c = 3, x = "a", y = "b", e = (a + b), d = (a + c) } +~~~~~~~~~ +b [ LocalVariable ] +0 [ IntegerLiteral ] +b = 0 [ Assignment ] +expression statement b = 0 [ ExpressionStatement ] +a [ LocalVariable ] +b [ LocalVariable ] +a = b [ Assignment ] +expression statement a = b [ ExpressionStatement ] +x [ LocalVariable ] +y [ LocalVariable ] +(x + y) [ StringConcatenate ] +x = (x + y) [ Assignment ] +expression statement x += y [ ExpressionStatement ] +a [ LocalVariable ] +return a [ Return ] +~~~~~~~~~ +AnalysisResult#7 +After: reaching definitions = { c = 3, y = "b", e = (a + b), d = (a + c), b = 0, a = b, x = (x + y) } + +0: +Process order: 7 +TransferInput#55 +Before: reaching definitions = { c = 3, y = "b", e = (a + b), d = (a + c), b = 0, a = b, x = (x + y) } +~~~~~~~~~ + diff --git a/dataflow/tests/reachingdef/Test.java b/dataflow/tests/reachingdef/Test.java new file mode 100644 index 00000000000..ea71b2fc492 --- /dev/null +++ b/dataflow/tests/reachingdef/Test.java @@ -0,0 +1,15 @@ +public class Test { + public int test() { + int a = 1, b = 2, c = 3; + String x = "a", y = "b"; + if (a > 0) { + int d = a + c; + } else { + int e = a + b; + } + b = 0; + a = b; + x += y; + return a; + } +}