diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex index 953ad706549..54ad26af37e 100644 --- a/dataflow/manual/content.tex +++ b/dataflow/manual/content.tex @@ -299,6 +299,25 @@ \subsubsection{AbstractValue} class NullnessValue extends CFAbstractValue \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 +\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 new file mode 100644 index 00000000000..ff6088f5500 --- /dev/null +++ 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 { + + /** 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/dataflow/src/main/java/org/checkerframework/dataflow/cfg/playground/LiveVariablePlayground.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/playground/LiveVariablePlayground.java index c2c1df0a293..291c1c0a0b4 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/playground/LiveVariablePlayground.java +++ b/dataflow/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 backwardAnalysis = + BackwardAnalysis backwardAnalysis = new BackwardAnalysisImpl<>(transfer); CFGVisualizeLauncher.generateDOTofCFG( inputFile, outputDir, method, clazz, true, true, backwardAnalysis); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarValue.java b/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarNode.java similarity index 50% rename from dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarValue.java rename to dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarNode.java index c986a93818c..18cdf010b08 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarValue.java +++ b/dataflow/src/main/java/org/checkerframework/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 { +/** + * 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 { */ 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 index 3ad1acdae5a..643bc8f1633 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java @@ -14,7 +14,6 @@ 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; @@ -22,21 +21,22 @@ /** A live variable store contains a set of live variables represented by nodes. */ public class LiveVarStore implements Store { - /** A set of live variable abstract values. */ - private final Set liveVarValueSet; + /** The set of live variables in this store */ + private final Set 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 liveVarValueSet) { - this.liveVarValueSet = liveVarValueSet; + public LiveVarStore(Set liveVarNodeSet) { + this.liveVarNodeSet = liveVarNodeSet; } /** @@ -44,8 +44,8 @@ public LiveVarStore(Set liveVarValueSet) { * * @param variable a live variable */ - public void putLiveVar(LiveVarValue variable) { - liveVarValueSet.add(variable); + public void putLiveVar(LiveVarNode variable) { + liveVarNodeSet.add(variable); } /** @@ -53,8 +53,8 @@ public void putLiveVar(LiveVarValue variable) { * * @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 liveVarValueSetLub = - new HashSet<>(this.liveVarValueSet.size() + other.liveVarValueSet.size()); - liveVarValueSetLub.addAll(this.liveVarValueSet); - liveVarValueSetLub.addAll(other.liveVarValueSet); + Set 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 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 index 2715d960cd4..fedc5e2716a 100644 --- 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, - TransferInput> - implements BackwardTransferFunction { + TransferResult, + TransferInput> + implements BackwardTransferFunction { @Override public LiveVarStore initialNormalExitStore( @@ -33,26 +34,27 @@ public LiveVarStore initialExceptionalExitStore(UnderlyingAST underlyingAST) { } @Override - public RegularTransferResult visitNode( - Node n, TransferInput p) { + 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); + public RegularTransferResult visitAssignment( + AssignmentNode n, TransferInput p) { + RegularTransferResult transferResult = + (RegularTransferResult) + super.visitAssignment(n, p); processLiveVarInAssignment( n.getTarget(), n.getExpression(), transferResult.getRegularStore()); return transferResult; } @Override - public RegularTransferResult visitMethodInvocation( - MethodInvocationNode n, TransferInput p) { - RegularTransferResult transferResult = - (RegularTransferResult) + public RegularTransferResult visitMethodInvocation( + MethodInvocationNode n, TransferInput p) { + RegularTransferResult transferResult = + (RegularTransferResult) super.visitMethodInvocation(n, p); LiveVarStore store = transferResult.getRegularStore(); for (Node arg : n.getArguments()) { @@ -62,10 +64,11 @@ public RegularTransferResult visitMethodInvocation( } @Override - public RegularTransferResult visitObjectCreation( - ObjectCreationNode n, TransferInput p) { - RegularTransferResult transferResult = - (RegularTransferResult) super.visitObjectCreation(n, p); + public RegularTransferResult visitObjectCreation( + ObjectCreationNode n, TransferInput p) { + RegularTransferResult transferResult = + (RegularTransferResult) + super.visitObjectCreation(n, p); LiveVarStore store = transferResult.getRegularStore(); for (Node arg : n.getArguments()) { store.addUseInExpression(arg); @@ -74,10 +77,10 @@ public RegularTransferResult visitObjectCreation( } @Override - public RegularTransferResult visitReturn( - ReturnNode n, TransferInput p) { - RegularTransferResult transferResult = - (RegularTransferResult) super.visitReturn(n, p); + public RegularTransferResult visitReturn( + ReturnNode n, TransferInput p) { + RegularTransferResult transferResult = + (RegularTransferResult) super.visitReturn(n, p); Node result = n.getResult(); if (result != null) { LiveVarStore store = transferResult.getRegularStore(); @@ -94,7 +97,7 @@ public RegularTransferResult 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 index 5eac329582b..e30939fa213 100644 --- 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 backwardAnalysis = + BackwardAnalysis backwardAnalysis = new BackwardAnalysisImpl<>(transfer); CFGVisualizeLauncher.writeStringOfCFG( inputFile, method, clas, outputFile, backwardAnalysis);