From 7e91f469e4484ee7092c99942662767fc5a8bd2c Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 1 Apr 2021 12:23:36 -0400 Subject: [PATCH 01/23] initial bottom-store implementation --- .../checker/lock/LockAnalysis.java | 17 ++- .../checker/nullness/KeyForAnalysis.java | 18 ++- .../checker/nullness/KeyForBottomStore.java | 104 ++++++++++++++++ .../checker/nullness/NullnessAnalysis.java | 18 ++- .../checker/nullness/NullnessBottomStore.java | 112 ++++++++++++++++++ checker/tests/nullness/flow/DeadBranch.java | 11 ++ .../dataflow/analysis/Store.java | 7 ++ .../ConstantPropagationStore.java | 10 +- .../dataflow/livevariable/LiveVarStore.java | 12 +- .../framework/flow/CFAbstractAnalysis.java | 27 +++-- .../framework/flow/CFAbstractStore.java | 33 ++++-- .../framework/flow/CFAbstractTransfer.java | 78 ++++++------ .../framework/flow/CFAnalysis.java | 16 ++- .../framework/flow/CFBottomStore.java | 104 ++++++++++++++++ 14 files changed, 490 insertions(+), 77 deletions(-) create mode 100644 checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java create mode 100644 checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java create mode 100644 checker/tests/nullness/flow/DeadBranch.java create mode 100644 framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java index 8c0a7072862..fb4c9f11ec2 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java @@ -1,16 +1,18 @@ package org.checkerframework.checker.lock; -import java.util.List; -import java.util.Set; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeMirror; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.flow.CFAbstractAnalysis; import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFValue; import org.checkerframework.javacutil.Pair; +import java.util.List; +import java.util.Set; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeMirror; + /** * The analysis class for the lock type system. * @@ -46,4 +48,9 @@ public CFValue createAbstractValue( Set annotations, TypeMirror underlyingType) { return defaultCreateAbstractValue(this, annotations, underlyingType); } + + @Override + public LockStore getBottomStore(boolean sequentialSemantics) { + return null; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java index 7125cb110a0..bdd1312f9e5 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java @@ -1,14 +1,16 @@ package org.checkerframework.checker.nullness; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFAbstractValue; +import org.checkerframework.javacutil.Pair; + import java.util.List; import java.util.Set; + import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeMirror; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.flow.CFAbstractAnalysis; -import org.checkerframework.framework.flow.CFAbstractValue; -import org.checkerframework.javacutil.Pair; /** Boiler plate code to glue together all the parts the KeyFor dataflow classes. */ public class KeyForAnalysis extends CFAbstractAnalysis { @@ -47,4 +49,12 @@ public KeyForValue createAbstractValue( } return new KeyForValue(this, annotations, underlyingType); } + + @Override + public KeyForStore getBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = new KeyForBottomStore(this, sequentialSemantics); + } + return bottomStore; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java new file mode 100644 index 00000000000..d1bae0cc9f7 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java @@ -0,0 +1,104 @@ +package org.checkerframework.checker.nullness; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.analysis.FlowExpressions; +import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; +import org.checkerframework.dataflow.cfg.node.FieldAccessNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.type.AnnotatedTypeFactory; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeMirror; + +public class KeyForBottomStore extends KeyForStore { + public KeyForBottomStore( + CFAbstractAnalysis analysis, boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + } + + @Override + public boolean isBottom() { + return true; + } + + @Override + public KeyForStore copy() { + // throw new BugInCF("Copying of bottom store is not allowed."); + return this; + } + + /** The LUB of a bottom store and a second store is the second store */ + @Override + public KeyForStore leastUpperBound(KeyForStore other) { + return other; + } + + @Override + public KeyForStore widenedUpperBound(KeyForStore previous) { + return previous; + } + + @Override + public boolean equals(@Nullable Object o) { + return this == o; + } + + @Nullable @Override + public KeyForValue getValue(FlowExpressions.Receiver expr) { + return null; + } + + @Nullable @Override + public KeyForValue getValue(FieldAccessNode n) { + return null; + } + + @Nullable @Override + public KeyForValue getValue(MethodInvocationNode n) { + return null; + } + + @Nullable @Override + public KeyForValue getValue(ArrayAccessNode n) { + return null; + } + + @Nullable @Override + public KeyForValue getValue(LocalVariableNode n) { + return null; + } + + @Nullable @Override + public KeyForValue getValue(ThisLiteralNode n) { + return null; + } + + @Override + public void updateForMethodCall( + MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, KeyForValue val) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} + + @Override + public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, @Nullable KeyForValue value) {} + + @Override + public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} + + @Override + public void replaceValue(FlowExpressions.Receiver r, @Nullable KeyForValue value) {} + + @Override + public void clearValue(FlowExpressions.Receiver r) {} + + @Override + public void updateForAssignment(Node n, @Nullable KeyForValue val) {} +} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java index ce08388f053..6216ea8ec08 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java @@ -1,14 +1,16 @@ package org.checkerframework.checker.nullness; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFAbstractValue; +import org.checkerframework.javacutil.Pair; + import java.util.List; import java.util.Set; + import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeMirror; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.flow.CFAbstractAnalysis; -import org.checkerframework.framework.flow.CFAbstractValue; -import org.checkerframework.javacutil.Pair; /** * The analysis class for the non-null type system (serves as factory for the transfer function, @@ -42,4 +44,12 @@ public NullnessValue createAbstractValue( } return new NullnessValue(this, annotations, underlyingType); } + + @Override + public NullnessStore getBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = new NullnessBottomStore(this, sequentialSemantics); + } + return bottomStore; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java new file mode 100644 index 00000000000..1b990b14a2e --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java @@ -0,0 +1,112 @@ +package org.checkerframework.checker.nullness; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.analysis.FlowExpressions; +import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; +import org.checkerframework.dataflow.cfg.node.FieldAccessNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; +import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.type.AnnotatedTypeFactory; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeMirror; + +public class NullnessBottomStore extends NullnessStore { + private final AnnotationMirror NONNULL; + + public NullnessBottomStore( + CFAbstractAnalysis analysis, + boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + NONNULL = ((NullnessAnnotatedTypeFactory) analysis.getTypeFactory()).NONNULL; + } + + @Override + public boolean isBottom() { + return true; + } + + @Override + public NullnessStore copy() { + // throw new BugInCF("Copying of bottom store is not allowed."); + return this; + } + + /** The LUB of a bottom store and a second store is the second store */ + @Override + public NullnessStore leastUpperBound(NullnessStore other) { + return other; + } + + @Override + public NullnessStore widenedUpperBound(NullnessStore previous) { + return previous; + } + + @Override + public boolean equals(@Nullable Object o) { + return this == o; + } + + @Nullable @Override + public NullnessValue getValue(FlowExpressions.Receiver expr) { + return analysis.createSingleAnnotationValue(NONNULL, expr.getType()); + } + + private NullnessValue getBottomValue(Node n) { + return analysis.createSingleAnnotationValue(NONNULL, n.getType()); + } + + @Nullable @Override + public NullnessValue getValue(FieldAccessNode n) { + return getBottomValue(n); + } + + @Nullable @Override + public NullnessValue getValue(MethodInvocationNode n) { + return getBottomValue(n); + } + + @Nullable @Override + public NullnessValue getValue(ArrayAccessNode n) { + return getBottomValue(n); + } + + @Nullable @Override + public NullnessValue getValue(LocalVariableNode n) { + return getBottomValue(n); + } + + @Nullable @Override + public NullnessValue getValue(ThisLiteralNode n) { + return getBottomValue(n); + } + + @Override + public void updateForMethodCall( + MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, NullnessValue val) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} + + @Override + public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, @Nullable NullnessValue value) {} + + @Override + public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} + + @Override + public void replaceValue(FlowExpressions.Receiver r, @Nullable NullnessValue value) {} + + @Override + public void clearValue(FlowExpressions.Receiver r) {} + + @Override + public void updateForAssignment(Node n, @Nullable NullnessValue val) {} +} diff --git a/checker/tests/nullness/flow/DeadBranch.java b/checker/tests/nullness/flow/DeadBranch.java new file mode 100644 index 00000000000..2cf35900e17 --- /dev/null +++ b/checker/tests/nullness/flow/DeadBranch.java @@ -0,0 +1,11 @@ +import org.checkerframework.checker.nullness.qual.Nullable; + +public class IfTrue { + + Object foo(@Nullable Object myObj, boolean x) { + if (x) { + myObj = new Object(); + } + return myObj; + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java index 4c9dbad162b..fa8ee3923c6 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java @@ -92,4 +92,11 @@ public static enum FlowRule { * @return the String representation of this store */ String visualize(CFGVisualizer viz); + + /** + * Is this store a bottom store? + * + * @return true if this is a bottom store + */ + boolean isBottom(); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java b/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java index 2bec0c692d5..9e67c7b8500 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java @@ -1,7 +1,5 @@ package org.checkerframework.dataflow.constantpropagation; -import java.util.HashMap; -import java.util.Map; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.FlowExpressions; import org.checkerframework.dataflow.analysis.Store; @@ -10,6 +8,9 @@ import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.Node; +import java.util.HashMap; +import java.util.Map; + public class ConstantPropagationStore implements Store { /** Information about variables gathered so far. */ @@ -166,4 +167,9 @@ public boolean canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b) public String visualize(CFGVisualizer viz) { return viz.visualizeStoreKeyVal("constant propagation", null); } + + @Override + public boolean isBottom() { + return false; + } } 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 976ac38271c..8dfe2dabb90 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java @@ -1,8 +1,5 @@ package org.checkerframework.dataflow.livevariable; -import java.util.HashSet; -import java.util.Set; -import java.util.StringJoiner; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.FlowExpressions.Receiver; import org.checkerframework.dataflow.analysis.Store; @@ -17,6 +14,10 @@ import org.checkerframework.dataflow.cfg.node.UnaryOperationNode; import org.checkerframework.javacutil.BugInCF; +import java.util.HashSet; +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 { @@ -141,4 +142,9 @@ public String visualize(CFGVisualizer viz) { public String toString() { return liveVarValueSet.toString(); } + + @Override + public boolean isBottom() { + return false; + } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index 999545467a1..b677413d5d5 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -1,13 +1,5 @@ package org.checkerframework.framework.flow; -import java.util.List; -import java.util.Set; -import javax.annotation.processing.ProcessingEnvironment; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeKind; -import javax.lang.model.type.TypeMirror; -import javax.lang.model.util.Types; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.ForwardAnalysisImpl; @@ -23,6 +15,16 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.Pair; +import java.util.List; +import java.util.Set; + +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; +import javax.lang.model.util.Types; + /** * {@link CFAbstractAnalysis} is an extensible org.checkerframework.dataflow analysis for the * Checker Framework that tracks the annotations using a flow-sensitive analysis. It uses an {@link @@ -66,6 +68,8 @@ public abstract class CFAbstractAnalysis< /** Instance of the types utility. */ protected final Types types; + protected S bottomStore; + /** * Create a CFAbstractAnalysis. * @@ -129,6 +133,13 @@ public T createTransferFunction() { */ public abstract S createEmptyStore(boolean sequentialSemantics); + /** + * Create the unique shared instance of bottom store for the underlying type system + * + * @return the bottom store instance of the appropriate type + */ + public abstract S getBottomStore(boolean sequentialSemantics); + /** * Returns an identical copy of the store {@code s}. * diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index b2c185de657..e8427cf1917 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -1,15 +1,5 @@ package org.checkerframework.framework.flow; -import java.util.HashMap; -import java.util.Iterator; -import java.util.List; -import java.util.Map; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; -import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.Name; -import javax.lang.model.type.TypeMirror; -import javax.lang.model.util.Types; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.FlowExpressions; import org.checkerframework.dataflow.analysis.FlowExpressions.ArrayAccess; @@ -38,6 +28,18 @@ import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.Pair; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Name; +import javax.lang.model.type.TypeMirror; +import javax.lang.model.util.Types; + /** * A store for the checker framework analysis tracks the annotations of memory locations such as * local variables and fields. @@ -851,13 +853,19 @@ public S copy() { return analysis.createCopiedStore((S) this); } + @SuppressWarnings("unchecked") @Override public S leastUpperBound(S other) { + if (this.isBottom()) return other; + if (other != null && other.isBottom()) return (S) this; return upperBound(other, false); } + @SuppressWarnings("unchecked") @Override public S widenedUpperBound(S previous) { + if (this.isBottom()) return previous; + if (previous != null && previous.isBottom()) return (S) this; return upperBound(previous, true); } @@ -1058,4 +1066,9 @@ protected String internalVisualize(CFGVisualizer viz) { } return res.toString(); } + + @Override + public boolean isBottom() { + return true; + } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 5f68c62d5de..d3f3b1bc118 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -6,20 +6,7 @@ import com.sun.source.tree.VariableTree; import com.sun.source.util.TreePath; import com.sun.tools.javac.code.Symbol.ClassSymbol; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; -import javax.lang.model.element.ElementKind; -import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.VariableElement; -import javax.lang.model.type.TypeMirror; + import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.ConditionalTransferResult; import org.checkerframework.dataflow.analysis.FlowExpressions; @@ -36,28 +23,7 @@ import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda; import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGMethod; import org.checkerframework.dataflow.cfg.UnderlyingAST.Kind; -import org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor; -import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; -import org.checkerframework.dataflow.cfg.node.AssignmentNode; -import org.checkerframework.dataflow.cfg.node.CaseNode; -import org.checkerframework.dataflow.cfg.node.ClassNameNode; -import org.checkerframework.dataflow.cfg.node.ConditionalNotNode; -import org.checkerframework.dataflow.cfg.node.EqualToNode; -import org.checkerframework.dataflow.cfg.node.FieldAccessNode; -import org.checkerframework.dataflow.cfg.node.LambdaResultExpressionNode; -import org.checkerframework.dataflow.cfg.node.LocalVariableNode; -import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.NarrowingConversionNode; -import org.checkerframework.dataflow.cfg.node.Node; -import org.checkerframework.dataflow.cfg.node.NotEqualNode; -import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; -import org.checkerframework.dataflow.cfg.node.ReturnNode; -import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode; -import org.checkerframework.dataflow.cfg.node.StringConversionNode; -import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode; -import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; -import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode; -import org.checkerframework.dataflow.cfg.node.WideningConversionNode; +import org.checkerframework.dataflow.cfg.node.*; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -76,6 +42,22 @@ import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeMirror; + /** * The default analysis transfer function for the Checker Framework propagates information through * assignments and uses the {@link AnnotatedTypeFactory} to provide checker-specific logic how to @@ -675,14 +657,16 @@ public TransferResult visitThisLiteral(ThisLiteralNode n, TransferInput visitTernaryExpression( TernaryExpressionNode n, TransferInput p) { TransferResult result = super.visitTernaryExpression(n, p); - S store = result.getRegularStore(); + S thenStore = result.getThenStore(); + S elseStore = result.getElseStore(); V thenValue = p.getValueOfSubNode(n.getThenOperand()); V elseValue = p.getValueOfSubNode(n.getElseOperand()); V resultValue = null; if (thenValue != null && elseValue != null) { resultValue = thenValue.leastUpperBound(elseValue); } - return new RegularTransferResult<>(finishValue(resultValue, store), store); + V finishedValue = finishValue(resultValue, thenStore, elseStore); + return new ConditionalTransferResult<>(finishedValue, thenStore, elseStore); } /** Reverse the role of the 'thenStore' and 'elseStore'. */ @@ -1208,4 +1192,22 @@ public TransferResult visitStringConversion( result.setResultValue(p.getValueOfSubNode(n.getOperand())); return result; } + + @Override + public TransferResult visitBooleanLiteral( + BooleanLiteralNode n, TransferInput vsTransferInput) { + S thenStore, elseStore; + + TransferResult result = super.visitBooleanLiteral(n, vsTransferInput); + if (n.getValue()) { + thenStore = result.getThenStore(); + elseStore = analysis.getBottomStore(sequentialSemantics); + } else { + thenStore = analysis.getBottomStore(sequentialSemantics); + elseStore = result.getElseStore(); + } + + return new ConditionalTransferResult<>( + finishValue(result.getResultValue(), thenStore, elseStore), thenStore, elseStore); + } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java index 4cd38083c17..04109f2ab60 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java @@ -1,13 +1,15 @@ package org.checkerframework.framework.flow; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.javacutil.Pair; + import java.util.List; import java.util.Set; + import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeMirror; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; -import org.checkerframework.javacutil.Pair; /** The default org.checkerframework.dataflow analysis used in the Checker Framework. */ public class CFAnalysis extends CFAbstractAnalysis { @@ -24,6 +26,14 @@ public CFStore createEmptyStore(boolean sequentialSemantics) { return new CFStore(this, sequentialSemantics); } + @Override + public CFStore getBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = new CFBottomStore(this, sequentialSemantics); + } + return bottomStore; + } + @Override public CFStore createCopiedStore(CFStore s) { return new CFStore(this, s); diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java new file mode 100644 index 00000000000..c3d513cb2dd --- /dev/null +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java @@ -0,0 +1,104 @@ +package org.checkerframework.framework.flow; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.analysis.FlowExpressions; +import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; +import org.checkerframework.dataflow.cfg.node.FieldAccessNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; +import org.checkerframework.framework.type.AnnotatedTypeFactory; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeMirror; + +public final class CFBottomStore extends CFStore { + + public CFBottomStore( + CFAbstractAnalysis analysis, boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + } + + @Override + public CFStore copy() { + // throw new BugInCF("Copying of bottom store is not allowed."); + return this; + } + + /** The LUB of a bottom store and a second store is the second store */ + @Override + public CFStore leastUpperBound(CFStore other) { + return other; + } + + @Override + public CFStore widenedUpperBound(CFStore previous) { + return previous; + } + + @Override + public boolean isBottom() { + return true; + } + + @Override + public boolean equals(@Nullable Object o) { + return this == o; + } + + @Nullable @Override + public CFValue getValue(FlowExpressions.Receiver expr) { + return null; + } + + @Nullable @Override + public CFValue getValue(FieldAccessNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(MethodInvocationNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(ArrayAccessNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(LocalVariableNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(ThisLiteralNode n) { + return null; + } + + @Override + public void updateForMethodCall( + MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} + + @Override + public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} + + @Override + public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} + + @Override + public void replaceValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} + + @Override + public void clearValue(FlowExpressions.Receiver r) {} + + @Override + public void updateForAssignment(Node n, @Nullable CFValue val) {} +} From 0122edfa2bedec7b26523746b09ff3e97f2e345c Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 6 Jul 2021 11:56:18 -0400 Subject: [PATCH 02/23] undo import * --- .../framework/flow/CFAbstractTransfer.java | 23 ++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index d3f3b1bc118..ef85a627594 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -23,7 +23,28 @@ import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGLambda; import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGMethod; import org.checkerframework.dataflow.cfg.UnderlyingAST.Kind; -import org.checkerframework.dataflow.cfg.node.*; +import org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor; +import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; +import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.CaseNode; +import org.checkerframework.dataflow.cfg.node.ClassNameNode; +import org.checkerframework.dataflow.cfg.node.ConditionalNotNode; +import org.checkerframework.dataflow.cfg.node.EqualToNode; +import org.checkerframework.dataflow.cfg.node.FieldAccessNode; +import org.checkerframework.dataflow.cfg.node.LambdaResultExpressionNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.NarrowingConversionNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.NotEqualNode; +import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; +import org.checkerframework.dataflow.cfg.node.ReturnNode; +import org.checkerframework.dataflow.cfg.node.StringConcatenateAssignmentNode; +import org.checkerframework.dataflow.cfg.node.StringConversionNode; +import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode; +import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; +import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode; +import org.checkerframework.dataflow.cfg.node.WideningConversionNode; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; From c276efae16d42ecd9762d42767c9a2c680743ef7 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 4 Aug 2021 03:29:15 -0400 Subject: [PATCH 03/23] fix compile error --- .../org/checkerframework/framework/flow/CFAbstractTransfer.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index ef85a627594..56f5368e612 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -26,6 +26,7 @@ import org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor; import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.BooleanLiteralNode; import org.checkerframework.dataflow.cfg.node.CaseNode; import org.checkerframework.dataflow.cfg.node.ClassNameNode; import org.checkerframework.dataflow.cfg.node.ConditionalNotNode; From cceadf788180a984c06ee43d98412c705ad2f27d Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 4 Aug 2021 05:36:51 -0400 Subject: [PATCH 04/23] fix bug --- checker/tests/nullness/flow/DeadBranch.java | 4 ++-- .../org/checkerframework/framework/flow/CFAbstractStore.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/checker/tests/nullness/flow/DeadBranch.java b/checker/tests/nullness/flow/DeadBranch.java index 2cf35900e17..7360c57decc 100644 --- a/checker/tests/nullness/flow/DeadBranch.java +++ b/checker/tests/nullness/flow/DeadBranch.java @@ -1,9 +1,9 @@ import org.checkerframework.checker.nullness.qual.Nullable; -public class IfTrue { +class DeadBranch { Object foo(@Nullable Object myObj, boolean x) { - if (x) { + if (true) { myObj = new Object(); } return myObj; diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index e8427cf1917..c9cbeb364ad 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -1069,6 +1069,6 @@ protected String internalVisualize(CFGVisualizer viz) { @Override public boolean isBottom() { - return true; + return false; } } From 81c805907cd4de5e9c7d3be7dfa0068144d58145 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 4 Aug 2021 22:22:21 -0400 Subject: [PATCH 05/23] add lock bottom store; remove FPs involving if(true/false) --- .../checker/lock/LockAnalysis.java | 2 +- .../checker/lock/LockBottomStore.java | 103 ++++++++++++++++++ checker/tests/formatter/FlowFormatter.java | 1 + checker/tests/index/LubIndex.java | 3 - .../fbc/TryFinallyContinue.java | 4 - framework/tests/value/Basics.java | 19 +--- framework/tests/value/MinLenLUB.java | 3 - 7 files changed, 109 insertions(+), 26 deletions(-) create mode 100644 checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java index fb4c9f11ec2..86cd115e8cf 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java @@ -51,6 +51,6 @@ public CFValue createAbstractValue( @Override public LockStore getBottomStore(boolean sequentialSemantics) { - return null; + return new LockBottomStore(this, sequentialSemantics); } } diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java new file mode 100644 index 00000000000..5860b10bf2f --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java @@ -0,0 +1,103 @@ +package org.checkerframework.checker.lock; + +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.analysis.FlowExpressions; +import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; +import org.checkerframework.dataflow.cfg.node.FieldAccessNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.framework.type.AnnotatedTypeFactory; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeMirror; + +public class LockBottomStore extends LockStore { + public LockBottomStore(LockAnalysis analysis, boolean sequentialSemantics) { + super(analysis, sequentialSemantics); + } + + @Override + public boolean isBottom() { + return true; + } + + @Override + public LockStore copy() { + // throw new BugInCF("Copying of bottom store is not allowed."); + return this; + } + + /** The LUB of a bottom store and a second store is the second store */ + @Override + public LockStore leastUpperBound(LockStore other) { + return other; + } + + @Override + public LockStore widenedUpperBound(LockStore previous) { + return previous; + } + + @Override + public boolean equals(@Nullable Object o) { + return this == o; + } + + @Nullable @Override + public CFValue getValue(FlowExpressions.Receiver expr) { + return null; + } + + @Nullable @Override + public CFValue getValue(FieldAccessNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(MethodInvocationNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(ArrayAccessNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(LocalVariableNode n) { + return null; + } + + @Nullable @Override + public CFValue getValue(ThisLiteralNode n) { + return null; + } + + @Override + public void updateForMethodCall( + MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} + + @Override + public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} + + @Override + public void insertValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} + + @Override + public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} + + @Override + public void replaceValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} + + @Override + public void clearValue(FlowExpressions.Receiver r) {} + + @Override + public void updateForAssignment(Node n, @Nullable CFValue val) {} +} diff --git a/checker/tests/formatter/FlowFormatter.java b/checker/tests/formatter/FlowFormatter.java index cc6ad68a57e..11bd26d44de 100644 --- a/checker/tests/formatter/FlowFormatter.java +++ b/checker/tests/formatter/FlowFormatter.java @@ -29,6 +29,7 @@ public static void main(String... p) { if (false) { nullAssign = "%s"; } + // :: error: (format.string.invalid) f.format(nullAssign, "string"); // :: error: (assignment.type.incompatible) @Format({ConversionCategory.GENERAL}) String err0 = unqual; diff --git a/checker/tests/index/LubIndex.java b/checker/tests/index/LubIndex.java index 202fa55e0dd..6a92abdb779 100644 --- a/checker/tests/index/LubIndex.java +++ b/checker/tests/index/LubIndex.java @@ -10,7 +10,6 @@ public static void MinLen(int @MinLen(10) [] arg, int @MinLen(4) [] arg2) { } else { arr = arg2; } - // :: error: (assignment.type.incompatible) int @MinLen(10) [] res = arr; int @MinLen(4) [] res2 = arr; // :: error: (assignment.type.incompatible) @@ -24,10 +23,8 @@ public static void Bottom(int @BottomVal [] arg, int @MinLen(4) [] arg2) { } else { arr = arg2; } - // :: error: (assignment.type.incompatible) int @MinLen(10) [] res = arr; int @MinLen(4) [] res2 = arr; - // :: error: (assignment.type.incompatible) int @BottomVal [] res3 = arr; } diff --git a/checker/tests/initialization/fbc/TryFinallyContinue.java b/checker/tests/initialization/fbc/TryFinallyContinue.java index 67eb4ce470a..b40d73f61c7 100644 --- a/checker/tests/initialization/fbc/TryFinallyContinue.java +++ b/checker/tests/initialization/fbc/TryFinallyContinue.java @@ -6,7 +6,6 @@ String testWhile1() { String ans = "x"; while (true) { if (true) { - // :: error: (return.type.incompatible) return ans; } if (true) { @@ -41,7 +40,6 @@ String testWhile3(boolean cond) { OUTER: while (true) { if (true) { - // :: error: (return.type.incompatible) return ans; } @@ -66,7 +64,6 @@ String testFor1() { String ans = "x"; for (; ; ) { if (true) { - // :: error: (return.type.incompatible) return ans; } if (true) { @@ -101,7 +98,6 @@ String testFor3(boolean cond) { OUTER: for (; ; ) { if (true) { - // :: error: (return.type.incompatible) return ans; } diff --git a/framework/tests/value/Basics.java b/framework/tests/value/Basics.java index 9fb28e3bb7c..4435860da59 100644 --- a/framework/tests/value/Basics.java +++ b/framework/tests/value/Basics.java @@ -100,9 +100,7 @@ public void IntegerTest( if (true) { a = y; } - @IntRange(from = 15, to = 30) - // :: error: (assignment.type.incompatible) - Integer test4 = a; + @IntRange(from = 15, to = 30) Integer test4 = a; @IntRange(from = 3, to = 30) Integer test5 = a; /* IntRange + IntVal */ @@ -117,9 +115,7 @@ public void IntegerTest( if (true) { a = y; } - @IntRange(from = 1, to = 30) - // :: error: (assignment.type.incompatible) - Integer test8 = a; + @IntRange(from = 1, to = 30) Integer test8 = a; @IntRange(from = 0, to = 30) Integer test9 = a; } @@ -141,9 +137,7 @@ public void intTest(@IntRange(from = 3, to = 4) int x, @IntRange(from = 20, to = if (true) { a = y; } - @IntRange(from = 15, to = 30) - // :: error: (assignment.type.incompatible) - int test4 = a; + @IntRange(from = 15, to = 30) int test4 = a; @IntRange(from = 3, to = 30) int test5 = a; /* IntRange + IntVal */ @@ -158,9 +152,7 @@ public void intTest(@IntRange(from = 3, to = 4) int x, @IntRange(from = 20, to = if (true) { a = y; } - @IntRange(from = 1, to = 30) - // :: error: (assignment.type.incompatible) - int test8 = a; + @IntRange(from = 1, to = 30) int test8 = a; @IntRange(from = 0, to = 30) int test9 = a; } @@ -186,7 +178,6 @@ public void IntDoubleTest( if (true) { a = dv1; } - // :: error: (assignment.type.incompatible) @DoubleVal({4.0, 5.0}) double test1 = a; @DoubleVal({0.0, 1.0, 2.0, 3.0, 4.0, 5.0}) double test2 = a; @@ -198,7 +189,6 @@ public void IntDoubleTest( if (true) { a = dv1; } - // :: error: (assignment.type.incompatible) test1 = a; test2 = a; @@ -207,7 +197,6 @@ public void IntDoubleTest( if (true) { a = dv1; } - // :: error: (assignment.type.incompatible) @DoubleVal({4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0, 12.0}) double test5 = a; @UnknownVal double test6 = a; } diff --git a/framework/tests/value/MinLenLUB.java b/framework/tests/value/MinLenLUB.java index c8e71267682..9a90c661f43 100644 --- a/framework/tests/value/MinLenLUB.java +++ b/framework/tests/value/MinLenLUB.java @@ -9,7 +9,6 @@ public static void MinLen(int @MinLen(10) [] arg, int @MinLen(4) [] arg2) { } else { arr = arg2; } - // :: error: (assignment.type.incompatible) int @MinLen(10) [] res = arr; int @MinLen(4) [] res2 = arr; // :: error: (assignment.type.incompatible) @@ -23,10 +22,8 @@ public static void Bottom(int @BottomVal [] arg, int @MinLen(4) [] arg2) { } else { arr = arg2; } - // :: error: (assignment.type.incompatible) int @MinLen(10) [] res = arr; int @MinLen(4) [] res2 = arr; - // :: error: (assignment.type.incompatible) int @BottomVal [] res3 = arr; } From 887a888a75ecd4d4f2a5dc1803c99ec9a8cfa925 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 5 Aug 2021 03:50:41 -0400 Subject: [PATCH 06/23] NullnessBottom.getValue returns two qualifiers --- .../checker/nullness/NullnessBottomStore.java | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java index 1b990b14a2e..0c956050430 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java @@ -10,18 +10,24 @@ import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; import org.checkerframework.framework.flow.CFAbstractAnalysis; import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.QualifierHierarchy; + +import java.util.HashSet; +import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeMirror; public class NullnessBottomStore extends NullnessStore { - private final AnnotationMirror NONNULL; + private final Set bottomAnnos; public NullnessBottomStore( CFAbstractAnalysis analysis, boolean sequentialSemantics) { super(analysis, sequentialSemantics); - NONNULL = ((NullnessAnnotatedTypeFactory) analysis.getTypeFactory()).NONNULL; + QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); + bottomAnnos = new HashSet<>(); + bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); } @Override @@ -53,11 +59,11 @@ public boolean equals(@Nullable Object o) { @Nullable @Override public NullnessValue getValue(FlowExpressions.Receiver expr) { - return analysis.createSingleAnnotationValue(NONNULL, expr.getType()); + return analysis.createAbstractValue(bottomAnnos, expr.getType()); } private NullnessValue getBottomValue(Node n) { - return analysis.createSingleAnnotationValue(NONNULL, n.getType()); + return analysis.createAbstractValue(bottomAnnos, n.getType()); } @Nullable @Override From 9af8f2e33050f462d729ec302fa7a4c9a807066e Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 5 Aug 2021 04:43:08 -0400 Subject: [PATCH 07/23] xxxBottomStore.getValue returns abstract value with bottom annotations --- .../checker/lock/LockBottomStore.java | 25 ++++++++++++++----- .../checker/nullness/KeyForBottomStore.java | 25 ++++++++++++++----- .../checker/nullness/NullnessBottomStore.java | 16 ++++++------ .../framework/flow/CFBottomStore.java | 24 +++++++++++++----- 4 files changed, 64 insertions(+), 26 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java index 5860b10bf2f..7a15c993f6b 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java @@ -10,13 +10,22 @@ import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; import org.checkerframework.framework.flow.CFValue; import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.QualifierHierarchy; + +import java.util.HashSet; +import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeMirror; public class LockBottomStore extends LockStore { + private final Set bottomAnnos; + public LockBottomStore(LockAnalysis analysis, boolean sequentialSemantics) { super(analysis, sequentialSemantics); + QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); + bottomAnnos = new HashSet<>(); + bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); } @Override @@ -46,34 +55,38 @@ public boolean equals(@Nullable Object o) { return this == o; } + private CFValue getBottomValue(TypeMirror type) { + return analysis.createAbstractValue(bottomAnnos, type); + } + @Nullable @Override public CFValue getValue(FlowExpressions.Receiver expr) { - return null; + return getBottomValue(expr.getType()); } @Nullable @Override public CFValue getValue(FieldAccessNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(MethodInvocationNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(ArrayAccessNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(LocalVariableNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(ThisLiteralNode n) { - return null; + return getBottomValue(n.getType()); } @Override diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java index d1bae0cc9f7..2931bcf024c 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java @@ -10,14 +10,23 @@ import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; import org.checkerframework.framework.flow.CFAbstractAnalysis; import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.QualifierHierarchy; + +import java.util.HashSet; +import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeMirror; public class KeyForBottomStore extends KeyForStore { + private final Set bottomAnnos; + public KeyForBottomStore( CFAbstractAnalysis analysis, boolean sequentialSemantics) { super(analysis, sequentialSemantics); + QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); + bottomAnnos = new HashSet<>(); + bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); } @Override @@ -47,34 +56,38 @@ public boolean equals(@Nullable Object o) { return this == o; } + private KeyForValue getBottomValue(TypeMirror type) { + return analysis.createAbstractValue(bottomAnnos, type); + } + @Nullable @Override public KeyForValue getValue(FlowExpressions.Receiver expr) { - return null; + return getBottomValue(expr.getType()); } @Nullable @Override public KeyForValue getValue(FieldAccessNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public KeyForValue getValue(MethodInvocationNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public KeyForValue getValue(ArrayAccessNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public KeyForValue getValue(LocalVariableNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public KeyForValue getValue(ThisLiteralNode n) { - return null; + return getBottomValue(n.getType()); } @Override diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java index 0c956050430..98eaae43276 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java @@ -59,36 +59,36 @@ public boolean equals(@Nullable Object o) { @Nullable @Override public NullnessValue getValue(FlowExpressions.Receiver expr) { - return analysis.createAbstractValue(bottomAnnos, expr.getType()); + return getBottomValue(expr.getType()); } - private NullnessValue getBottomValue(Node n) { - return analysis.createAbstractValue(bottomAnnos, n.getType()); + private NullnessValue getBottomValue(TypeMirror type) { + return analysis.createAbstractValue(bottomAnnos, type); } @Nullable @Override public NullnessValue getValue(FieldAccessNode n) { - return getBottomValue(n); + return getBottomValue(n.getType()); } @Nullable @Override public NullnessValue getValue(MethodInvocationNode n) { - return getBottomValue(n); + return getBottomValue(n.getType()); } @Nullable @Override public NullnessValue getValue(ArrayAccessNode n) { - return getBottomValue(n); + return getBottomValue(n.getType()); } @Nullable @Override public NullnessValue getValue(LocalVariableNode n) { - return getBottomValue(n); + return getBottomValue(n.getType()); } @Nullable @Override public NullnessValue getValue(ThisLiteralNode n) { - return getBottomValue(n); + return getBottomValue(n.getType()); } @Override diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java index c3d513cb2dd..f679322ad39 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java @@ -9,15 +9,23 @@ import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.QualifierHierarchy; + +import java.util.HashSet; +import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeMirror; public final class CFBottomStore extends CFStore { + private final Set bottomAnnos; public CFBottomStore( CFAbstractAnalysis analysis, boolean sequentialSemantics) { super(analysis, sequentialSemantics); + QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); + bottomAnnos = new HashSet<>(); + bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); } @Override @@ -47,34 +55,38 @@ public boolean equals(@Nullable Object o) { return this == o; } + private CFValue getBottomValue(TypeMirror type) { + return analysis.createAbstractValue(bottomAnnos, type); + } + @Nullable @Override public CFValue getValue(FlowExpressions.Receiver expr) { - return null; + return getBottomValue(expr.getType()); } @Nullable @Override public CFValue getValue(FieldAccessNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(MethodInvocationNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(ArrayAccessNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(LocalVariableNode n) { - return null; + return getBottomValue(n.getType()); } @Nullable @Override public CFValue getValue(ThisLiteralNode n) { - return null; + return getBottomValue(n.getType()); } @Override From 0a4adad89af5ff40be1cab8b9359277bdf4d2aef Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 5 Aug 2021 07:27:01 -0400 Subject: [PATCH 08/23] remove @Nullable on xxxBottomStore.getValue --- .../checker/lock/LockBottomStore.java | 12 ++++++------ .../checker/nullness/KeyForBottomStore.java | 12 ++++++------ .../checker/nullness/NullnessBottomStore.java | 12 ++++++------ .../framework/flow/CFBottomStore.java | 12 ++++++------ 4 files changed, 24 insertions(+), 24 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java index 7a15c993f6b..06a5dac4ea7 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java @@ -59,32 +59,32 @@ private CFValue getBottomValue(TypeMirror type) { return analysis.createAbstractValue(bottomAnnos, type); } - @Nullable @Override + @Override public CFValue getValue(FlowExpressions.Receiver expr) { return getBottomValue(expr.getType()); } - @Nullable @Override + @Override public CFValue getValue(FieldAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(MethodInvocationNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(ArrayAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(LocalVariableNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(ThisLiteralNode n) { return getBottomValue(n.getType()); } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java index 2931bcf024c..173edf12abf 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java @@ -60,32 +60,32 @@ private KeyForValue getBottomValue(TypeMirror type) { return analysis.createAbstractValue(bottomAnnos, type); } - @Nullable @Override + @Override public KeyForValue getValue(FlowExpressions.Receiver expr) { return getBottomValue(expr.getType()); } - @Nullable @Override + @Override public KeyForValue getValue(FieldAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public KeyForValue getValue(MethodInvocationNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public KeyForValue getValue(ArrayAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public KeyForValue getValue(LocalVariableNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public KeyForValue getValue(ThisLiteralNode n) { return getBottomValue(n.getType()); } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java index 98eaae43276..ef7818335a4 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java @@ -57,7 +57,7 @@ public boolean equals(@Nullable Object o) { return this == o; } - @Nullable @Override + @Override public NullnessValue getValue(FlowExpressions.Receiver expr) { return getBottomValue(expr.getType()); } @@ -66,27 +66,27 @@ private NullnessValue getBottomValue(TypeMirror type) { return analysis.createAbstractValue(bottomAnnos, type); } - @Nullable @Override + @Override public NullnessValue getValue(FieldAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public NullnessValue getValue(MethodInvocationNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public NullnessValue getValue(ArrayAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public NullnessValue getValue(LocalVariableNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public NullnessValue getValue(ThisLiteralNode n) { return getBottomValue(n.getType()); } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java index f679322ad39..94836570769 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java @@ -59,32 +59,32 @@ private CFValue getBottomValue(TypeMirror type) { return analysis.createAbstractValue(bottomAnnos, type); } - @Nullable @Override + @Override public CFValue getValue(FlowExpressions.Receiver expr) { return getBottomValue(expr.getType()); } - @Nullable @Override + @Override public CFValue getValue(FieldAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(MethodInvocationNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(ArrayAccessNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(LocalVariableNode n) { return getBottomValue(n.getType()); } - @Nullable @Override + @Override public CFValue getValue(ThisLiteralNode n) { return getBottomValue(n.getType()); } From 6775dfa997ffd580ffc14c498e10a4679c00febc Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 5 Aug 2021 12:59:42 -0400 Subject: [PATCH 09/23] fix bug --- .../framework/flow/CFAbstractValue.java | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java index ef967673ab3..43f2d9aa171 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java @@ -333,6 +333,14 @@ protected void visitNeitherAnnotationExistsInBothSets( @Override protected void visitAnnotationExistInOneSet( AnnotationMirror anno, AnnotatedTypeVariable atv, AnnotationMirror top) { + AnnotationMirror backup = getBackUpAnnoIn(top); + if (atv == null) { + if (backup != null) { + mostSpecific.add(backup); + } + return; + } + QualifierHierarchy hierarchy = analysis.getTypeFactory().getQualifierHierarchy(); AnnotationMirror upperBound = atv.getEffectiveAnnotationInHierarchy(top); @@ -347,11 +355,8 @@ protected void visitAnnotationExistInOneSet( // no anno is more specific than anno } else if (hierarchy.isSubtype(anno, lowerBound)) { mostSpecific.add(anno); - } else { - AnnotationMirror backup = getBackUpAnnoIn(top); - if (backup != null) { - mostSpecific.add(backup); - } + } else if (backup != null) { + mostSpecific.add(backup); } } } From 68b238b31bd60d32367b784955b318b17cac17a6 Mon Sep 17 00:00:00 2001 From: d367wang Date: Mon, 9 Aug 2021 13:58:25 -0400 Subject: [PATCH 10/23] make bottom-store logic coherent to CFAbstract classes --- .../checker/lock/LockAnalysis.java | 13 +- .../checker/lock/LockBottomStore.java | 116 ----------------- .../checker/lock/LockStore.java | 5 + .../checker/nullness/KeyForAnalysis.java | 16 +-- .../checker/nullness/KeyForBottomStore.java | 117 ----------------- .../checker/nullness/KeyForStore.java | 7 ++ .../checker/nullness/NullnessAnalysis.java | 16 +-- .../checker/nullness/NullnessBottomStore.java | 118 ------------------ .../checker/nullness/NullnessStore.java | 8 ++ .../dataflow/analysis/Store.java | 7 -- .../ConstantPropagationStore.java | 5 - .../dataflow/livevariable/LiveVarStore.java | 5 - .../framework/flow/CFAbstractAnalysis.java | 3 +- .../framework/flow/CFAbstractStore.java | 23 ++-- .../framework/flow/CFAbstractTransfer.java | 4 +- .../framework/flow/CFAnalysis.java | 4 +- .../framework/flow/CFBottomStore.java | 116 ----------------- .../framework/flow/CFStore.java | 7 ++ 18 files changed, 71 insertions(+), 519 deletions(-) delete mode 100644 checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java delete mode 100644 checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java delete mode 100644 checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java delete mode 100644 framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java index 86cd115e8cf..4dc286a851e 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java @@ -38,6 +38,14 @@ public LockStore createEmptyStore(boolean sequentialSemantics) { return new LockStore(this, sequentialSemantics); } + @Override + public LockStore createBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = new LockStore(this, sequentialSemantics, true); + } + return bottomStore; + } + @Override public LockStore createCopiedStore(LockStore s) { return new LockStore(this, s); @@ -48,9 +56,4 @@ public CFValue createAbstractValue( Set annotations, TypeMirror underlyingType) { return defaultCreateAbstractValue(this, annotations, underlyingType); } - - @Override - public LockStore getBottomStore(boolean sequentialSemantics) { - return new LockBottomStore(this, sequentialSemantics); - } } diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java deleted file mode 100644 index 06a5dac4ea7..00000000000 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockBottomStore.java +++ /dev/null @@ -1,116 +0,0 @@ -package org.checkerframework.checker.lock; - -import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.dataflow.analysis.FlowExpressions; -import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; -import org.checkerframework.dataflow.cfg.node.FieldAccessNode; -import org.checkerframework.dataflow.cfg.node.LocalVariableNode; -import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.Node; -import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; -import org.checkerframework.framework.flow.CFValue; -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.QualifierHierarchy; - -import java.util.HashSet; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.type.TypeMirror; - -public class LockBottomStore extends LockStore { - private final Set bottomAnnos; - - public LockBottomStore(LockAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); - bottomAnnos = new HashSet<>(); - bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); - } - - @Override - public boolean isBottom() { - return true; - } - - @Override - public LockStore copy() { - // throw new BugInCF("Copying of bottom store is not allowed."); - return this; - } - - /** The LUB of a bottom store and a second store is the second store */ - @Override - public LockStore leastUpperBound(LockStore other) { - return other; - } - - @Override - public LockStore widenedUpperBound(LockStore previous) { - return previous; - } - - @Override - public boolean equals(@Nullable Object o) { - return this == o; - } - - private CFValue getBottomValue(TypeMirror type) { - return analysis.createAbstractValue(bottomAnnos, type); - } - - @Override - public CFValue getValue(FlowExpressions.Receiver expr) { - return getBottomValue(expr.getType()); - } - - @Override - public CFValue getValue(FieldAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(MethodInvocationNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(ArrayAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(LocalVariableNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(ThisLiteralNode n) { - return getBottomValue(n.getType()); - } - - @Override - public void updateForMethodCall( - MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} - - @Override - public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} - - @Override - public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} - - @Override - public void replaceValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} - - @Override - public void clearValue(FlowExpressions.Receiver r) {} - - @Override - public void updateForAssignment(Node n, @Nullable CFValue val) {} -} diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 997be56949f..a92557fc7d0 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -44,6 +44,11 @@ public LockStore(LockAnalysis analysis, boolean sequentialSemantics) { this.atypeFactory = (LockAnnotatedTypeFactory) analysis.getTypeFactory(); } + public LockStore(LockAnalysis analysis, boolean sequentialSemantics, boolean isBottom) { + super(analysis, sequentialSemantics, isBottom); + this.atypeFactory = (LockAnnotatedTypeFactory) analysis.getTypeFactory(); + } + /** Copy constructor. */ public LockStore(LockAnalysis analysis, CFAbstractStore other) { super(other); diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java index bdd1312f9e5..e25be6859d2 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java @@ -35,6 +35,14 @@ public KeyForStore createEmptyStore(boolean sequentialSemantics) { return new KeyForStore(this, sequentialSemantics); } + @Override + public KeyForStore createBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = new KeyForStore(this, sequentialSemantics, true); + } + return bottomStore; + } + @Override public KeyForStore createCopiedStore(KeyForStore store) { return new KeyForStore(store); @@ -49,12 +57,4 @@ public KeyForValue createAbstractValue( } return new KeyForValue(this, annotations, underlyingType); } - - @Override - public KeyForStore getBottomStore(boolean sequentialSemantics) { - if (bottomStore == null) { - bottomStore = new KeyForBottomStore(this, sequentialSemantics); - } - return bottomStore; - } } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java deleted file mode 100644 index 173edf12abf..00000000000 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForBottomStore.java +++ /dev/null @@ -1,117 +0,0 @@ -package org.checkerframework.checker.nullness; - -import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.dataflow.analysis.FlowExpressions; -import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; -import org.checkerframework.dataflow.cfg.node.FieldAccessNode; -import org.checkerframework.dataflow.cfg.node.LocalVariableNode; -import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.Node; -import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; -import org.checkerframework.framework.flow.CFAbstractAnalysis; -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.QualifierHierarchy; - -import java.util.HashSet; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.type.TypeMirror; - -public class KeyForBottomStore extends KeyForStore { - private final Set bottomAnnos; - - public KeyForBottomStore( - CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); - bottomAnnos = new HashSet<>(); - bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); - } - - @Override - public boolean isBottom() { - return true; - } - - @Override - public KeyForStore copy() { - // throw new BugInCF("Copying of bottom store is not allowed."); - return this; - } - - /** The LUB of a bottom store and a second store is the second store */ - @Override - public KeyForStore leastUpperBound(KeyForStore other) { - return other; - } - - @Override - public KeyForStore widenedUpperBound(KeyForStore previous) { - return previous; - } - - @Override - public boolean equals(@Nullable Object o) { - return this == o; - } - - private KeyForValue getBottomValue(TypeMirror type) { - return analysis.createAbstractValue(bottomAnnos, type); - } - - @Override - public KeyForValue getValue(FlowExpressions.Receiver expr) { - return getBottomValue(expr.getType()); - } - - @Override - public KeyForValue getValue(FieldAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public KeyForValue getValue(MethodInvocationNode n) { - return getBottomValue(n.getType()); - } - - @Override - public KeyForValue getValue(ArrayAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public KeyForValue getValue(LocalVariableNode n) { - return getBottomValue(n.getType()); - } - - @Override - public KeyForValue getValue(ThisLiteralNode n) { - return getBottomValue(n.getType()); - } - - @Override - public void updateForMethodCall( - MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, KeyForValue val) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} - - @Override - public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, @Nullable KeyForValue value) {} - - @Override - public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} - - @Override - public void replaceValue(FlowExpressions.Receiver r, @Nullable KeyForValue value) {} - - @Override - public void clearValue(FlowExpressions.Receiver r) {} - - @Override - public void updateForAssignment(Node n, @Nullable KeyForValue val) {} -} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java index 75f09cb88db..5cac977968f 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java @@ -9,6 +9,13 @@ public KeyForStore( super(analysis, sequentialSemantics); } + public KeyForStore( + CFAbstractAnalysis analysis, + boolean sequentialSemantics, + boolean isBottom) { + super(analysis, sequentialSemantics, isBottom); + } + protected KeyForStore(CFAbstractStore other) { super(other); } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java index 6216ea8ec08..284171c0d20 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java @@ -31,6 +31,14 @@ public NullnessStore createEmptyStore(boolean sequentialSemantics) { return new NullnessStore(this, sequentialSemantics); } + @Override + public NullnessStore createBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = new NullnessStore(this, sequentialSemantics, true); + } + return bottomStore; + } + @Override public NullnessStore createCopiedStore(NullnessStore s) { return new NullnessStore(s); @@ -44,12 +52,4 @@ public NullnessValue createAbstractValue( } return new NullnessValue(this, annotations, underlyingType); } - - @Override - public NullnessStore getBottomStore(boolean sequentialSemantics) { - if (bottomStore == null) { - bottomStore = new NullnessBottomStore(this, sequentialSemantics); - } - return bottomStore; - } } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java deleted file mode 100644 index ef7818335a4..00000000000 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessBottomStore.java +++ /dev/null @@ -1,118 +0,0 @@ -package org.checkerframework.checker.nullness; - -import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.dataflow.analysis.FlowExpressions; -import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; -import org.checkerframework.dataflow.cfg.node.FieldAccessNode; -import org.checkerframework.dataflow.cfg.node.LocalVariableNode; -import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.Node; -import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; -import org.checkerframework.framework.flow.CFAbstractAnalysis; -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.QualifierHierarchy; - -import java.util.HashSet; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.type.TypeMirror; - -public class NullnessBottomStore extends NullnessStore { - private final Set bottomAnnos; - - public NullnessBottomStore( - CFAbstractAnalysis analysis, - boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); - bottomAnnos = new HashSet<>(); - bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); - } - - @Override - public boolean isBottom() { - return true; - } - - @Override - public NullnessStore copy() { - // throw new BugInCF("Copying of bottom store is not allowed."); - return this; - } - - /** The LUB of a bottom store and a second store is the second store */ - @Override - public NullnessStore leastUpperBound(NullnessStore other) { - return other; - } - - @Override - public NullnessStore widenedUpperBound(NullnessStore previous) { - return previous; - } - - @Override - public boolean equals(@Nullable Object o) { - return this == o; - } - - @Override - public NullnessValue getValue(FlowExpressions.Receiver expr) { - return getBottomValue(expr.getType()); - } - - private NullnessValue getBottomValue(TypeMirror type) { - return analysis.createAbstractValue(bottomAnnos, type); - } - - @Override - public NullnessValue getValue(FieldAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public NullnessValue getValue(MethodInvocationNode n) { - return getBottomValue(n.getType()); - } - - @Override - public NullnessValue getValue(ArrayAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public NullnessValue getValue(LocalVariableNode n) { - return getBottomValue(n.getType()); - } - - @Override - public NullnessValue getValue(ThisLiteralNode n) { - return getBottomValue(n.getType()); - } - - @Override - public void updateForMethodCall( - MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, NullnessValue val) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} - - @Override - public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, @Nullable NullnessValue value) {} - - @Override - public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} - - @Override - public void replaceValue(FlowExpressions.Receiver r, @Nullable NullnessValue value) {} - - @Override - public void clearValue(FlowExpressions.Receiver r) {} - - @Override - public void updateForAssignment(Node n, @Nullable NullnessValue val) {} -} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java index c4595b2310f..dc01abb3417 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java @@ -22,6 +22,14 @@ public NullnessStore( isPolyNullNull = false; } + public NullnessStore( + CFAbstractAnalysis analysis, + boolean sequentialSemantics, + boolean isBottom) { + super(analysis, sequentialSemantics); + this.isPolyNullNull = false; + } + public NullnessStore(NullnessStore s) { super(s); isPolyNullNull = s.isPolyNullNull; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java index fa8ee3923c6..4c9dbad162b 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java @@ -92,11 +92,4 @@ public static enum FlowRule { * @return the String representation of this store */ String visualize(CFGVisualizer viz); - - /** - * Is this store a bottom store? - * - * @return true if this is a bottom store - */ - boolean isBottom(); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java b/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java index 9e67c7b8500..39918b900c3 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java @@ -167,9 +167,4 @@ public boolean canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b) public String visualize(CFGVisualizer viz) { return viz.visualizeStoreKeyVal("constant propagation", null); } - - @Override - public boolean isBottom() { - return false; - } } 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 8dfe2dabb90..2f53cf44a88 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java @@ -142,9 +142,4 @@ public String visualize(CFGVisualizer viz) { public String toString() { return liveVarValueSet.toString(); } - - @Override - public boolean isBottom() { - return false; - } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index b677413d5d5..24406ade542 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -68,6 +68,7 @@ public abstract class CFAbstractAnalysis< /** Instance of the types utility. */ protected final Types types; + /** The singleton of bottom store in dataflow analysis for a specific type system */ protected S bottomStore; /** @@ -138,7 +139,7 @@ public T createTransferFunction() { * * @return the bottom store instance of the appropriate type */ - public abstract S getBottomStore(boolean sequentialSemantics); + public abstract S createBottomStore(boolean sequentialSemantics); /** * Returns an identical copy of the store {@code s}. diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index c9cbeb364ad..6e56e6b6e66 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -95,11 +95,19 @@ public abstract class CFAbstractStore, S extends CF */ protected final boolean sequentialSemantics; + /** Is the store for unreachable code branch? */ + protected final boolean isBottom; + /* --------------------------------------------------------- */ /* Initialization */ /* --------------------------------------------------------- */ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { + this(analysis, sequentialSemantics, false); + } + + protected CFAbstractStore( + CFAbstractAnalysis analysis, boolean sequentialSemantics, boolean isBottom) { this.analysis = analysis; localVariableValues = new HashMap<>(); thisValue = null; @@ -108,6 +116,7 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti arrayValues = new HashMap<>(); classValues = new HashMap<>(); this.sequentialSemantics = sequentialSemantics; + this.isBottom = isBottom; } /** Copy constructor. */ @@ -120,6 +129,7 @@ protected CFAbstractStore(CFAbstractStore other) { arrayValues = new HashMap<>(other.arrayValues); classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; + this.isBottom = other.isBottom; } /** @@ -856,16 +866,16 @@ public S copy() { @SuppressWarnings("unchecked") @Override public S leastUpperBound(S other) { - if (this.isBottom()) return other; - if (other != null && other.isBottom()) return (S) this; + if (this.isBottom) return other; + if (other != null && other.isBottom) return (S) this; return upperBound(other, false); } @SuppressWarnings("unchecked") @Override public S widenedUpperBound(S previous) { - if (this.isBottom()) return previous; - if (previous != null && previous.isBottom()) return (S) this; + if (this.isBottom) return previous; + if (previous != null && previous.isBottom) return (S) this; return upperBound(previous, true); } @@ -1066,9 +1076,4 @@ protected String internalVisualize(CFGVisualizer viz) { } return res.toString(); } - - @Override - public boolean isBottom() { - return false; - } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 56f5368e612..644fcac8864 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1223,9 +1223,9 @@ public TransferResult visitBooleanLiteral( TransferResult result = super.visitBooleanLiteral(n, vsTransferInput); if (n.getValue()) { thenStore = result.getThenStore(); - elseStore = analysis.getBottomStore(sequentialSemantics); + elseStore = analysis.createBottomStore(sequentialSemantics); } else { - thenStore = analysis.getBottomStore(sequentialSemantics); + thenStore = analysis.createBottomStore(sequentialSemantics); elseStore = result.getElseStore(); } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java index 04109f2ab60..5140b26df86 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java @@ -27,9 +27,9 @@ public CFStore createEmptyStore(boolean sequentialSemantics) { } @Override - public CFStore getBottomStore(boolean sequentialSemantics) { + public CFStore createBottomStore(boolean sequentialSemantics) { if (bottomStore == null) { - bottomStore = new CFBottomStore(this, sequentialSemantics); + bottomStore = new CFStore(this, sequentialSemantics, true); } return bottomStore; } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java deleted file mode 100644 index 94836570769..00000000000 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFBottomStore.java +++ /dev/null @@ -1,116 +0,0 @@ -package org.checkerframework.framework.flow; - -import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.dataflow.analysis.FlowExpressions; -import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; -import org.checkerframework.dataflow.cfg.node.FieldAccessNode; -import org.checkerframework.dataflow.cfg.node.LocalVariableNode; -import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.Node; -import org.checkerframework.dataflow.cfg.node.ThisLiteralNode; -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.QualifierHierarchy; - -import java.util.HashSet; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.type.TypeMirror; - -public final class CFBottomStore extends CFStore { - private final Set bottomAnnos; - - public CFBottomStore( - CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - QualifierHierarchy qualifierHierarchy = analysis.getTypeFactory().getQualifierHierarchy(); - bottomAnnos = new HashSet<>(); - bottomAnnos.addAll(qualifierHierarchy.getBottomAnnotations()); - } - - @Override - public CFStore copy() { - // throw new BugInCF("Copying of bottom store is not allowed."); - return this; - } - - /** The LUB of a bottom store and a second store is the second store */ - @Override - public CFStore leastUpperBound(CFStore other) { - return other; - } - - @Override - public CFStore widenedUpperBound(CFStore previous) { - return previous; - } - - @Override - public boolean isBottom() { - return true; - } - - @Override - public boolean equals(@Nullable Object o) { - return this == o; - } - - private CFValue getBottomValue(TypeMirror type) { - return analysis.createAbstractValue(bottomAnnos, type); - } - - @Override - public CFValue getValue(FlowExpressions.Receiver expr) { - return getBottomValue(expr.getType()); - } - - @Override - public CFValue getValue(FieldAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(MethodInvocationNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(ArrayAccessNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(LocalVariableNode n) { - return getBottomValue(n.getType()); - } - - @Override - public CFValue getValue(ThisLiteralNode n) { - return getBottomValue(n.getType()); - } - - @Override - public void updateForMethodCall( - MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, AnnotationMirror a) {} - - @Override - public void insertOrRefine(FlowExpressions.Receiver r, AnnotationMirror newAnno) {} - - @Override - public void insertValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} - - @Override - public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) {} - - @Override - public void replaceValue(FlowExpressions.Receiver r, @Nullable CFValue value) {} - - @Override - public void clearValue(FlowExpressions.Receiver r) {} - - @Override - public void updateForAssignment(Node n, @Nullable CFValue val) {} -} diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java index d0f7cc18ce1..e04e02760e5 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java @@ -7,6 +7,13 @@ public CFStore(CFAbstractAnalysis analysis, boolean sequent super(analysis, sequentialSemantics); } + public CFStore( + CFAbstractAnalysis analysis, + boolean sequentialSemantics, + boolean isBottom) { + super(analysis, sequentialSemantics, isBottom); + } + public CFStore( CFAbstractAnalysis analysis, CFAbstractStore other) { From d6ddb829ce7fd6bade62e554af307a9ca214d9d0 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 26 Aug 2021 22:43:05 -0400 Subject: [PATCH 11/23] adapt expected files --- docs/examples/MavenExample/Makefile | 2 +- docs/examples/fenum-extension/Expected.txt | 30 +++++++++++----------- docs/examples/units-extension/Expected.txt | 4 +-- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/docs/examples/MavenExample/Makefile b/docs/examples/MavenExample/Makefile index 0848faa604c..a250c76ab7d 100644 --- a/docs/examples/MavenExample/Makefile +++ b/docs/examples/MavenExample/Makefile @@ -13,7 +13,7 @@ all: mvn -B -fn compile > Out.txt 2>&1 # TODO JDK16: Temporary hack to skip running under JDK > 11. This test gets a hard-coded version of the Checker Framework from Maven Central, and that version doesn't work on JDK 16 (until the next release after this line is committed!). [ ${JAVA_VER} -gt 11 ] || \ - (grep -qF "MavenExample.java:[29,29] error: [assignment] incompatible types in assignment." Out.txt || (echo "FAILURE. Here is file Out.txt:" && cat Out.txt && echo "End of file Out.txt." && false)) + (grep -qF "MavenExample.java:[30,29] error: [assignment] incompatible types in assignment." Out.txt || (echo "FAILURE. Here is file Out.txt:" && cat Out.txt && echo "End of file Out.txt." && false)) clean: mvn -q clean diff --git a/docs/examples/fenum-extension/Expected.txt b/docs/examples/fenum-extension/Expected.txt index 0a61874eae1..31d55845248 100644 --- a/docs/examples/fenum-extension/Expected.txt +++ b/docs/examples/fenum-extension/Expected.txt @@ -1,64 +1,64 @@ -FenumDemo.java:19: error: [assignment.type.incompatible] incompatible types in assignment. +FenumDemo.java:20: error: [assignment.type.incompatible] incompatible types in assignment. @Fenum("B") int state2 = TestStatic.ACONST1; // Incompatible fenums forbidden! ^ found : @Fenum("A") int required: @Fenum("B") int -FenumDemo.java:28: error: [assignment.type.incompatible] incompatible types in assignment. +FenumDemo.java:29: error: [assignment.type.incompatible] incompatible types in assignment. state1 = 4; // Direct use of value forbidden! ^ found : @FenumUnqualified int required: @Fenum("A") int -FenumDemo.java:29: error: [assignment.type.incompatible] incompatible types in assignment. +FenumDemo.java:30: error: [assignment.type.incompatible] incompatible types in assignment. state1 = TestStatic.BCONST1; // Incompatible fenums forbidden! ^ found : @Fenum("B") int required: @Fenum("A") int -FenumDemo.java:32: error: [argument.type.incompatible] incompatible argument for parameter p of fenumArg. +FenumDemo.java:33: error: [argument.type.incompatible] incompatible argument for parameter p of fenumArg. fenumArg(5); // Direct use of value forbidden! ^ found : @FenumUnqualified int required: @Fenum("A") int -FenumDemo.java:33: error: [argument.type.incompatible] incompatible argument for parameter p of fenumArg. +FenumDemo.java:34: error: [argument.type.incompatible] incompatible argument for parameter p of fenumArg. fenumArg(TestStatic.BCONST1); // Incompatible fenums forbidden! ^ found : @Fenum("B") int required: @Fenum("A") int -FenumDemo.java:36: error: [assignment.type.incompatible] incompatible types in assignment. +FenumDemo.java:37: error: [assignment.type.incompatible] incompatible types in assignment. state3 = 8; ^ found : @FenumUnqualified int required: @MyFenum int -FenumDemo.java:37: error: [assignment.type.incompatible] incompatible types in assignment. +FenumDemo.java:38: error: [assignment.type.incompatible] incompatible types in assignment. state3 = TestStatic.ACONST2; // Incompatible fenums forbidden! ^ found : @Fenum("A") int required: @MyFenum int -FenumDemo.java:40: error: [argument.type.incompatible] incompatible argument for parameter p of myFenumArg. +FenumDemo.java:41: error: [argument.type.incompatible] incompatible argument for parameter p of myFenumArg. myFenumArg(8); // Direct use of value forbidden! ^ found : @FenumUnqualified int required: @MyFenum int -FenumDemo.java:41: error: [argument.type.incompatible] incompatible argument for parameter p of myFenumArg. +FenumDemo.java:42: error: [argument.type.incompatible] incompatible argument for parameter p of myFenumArg. myFenumArg(TestStatic.BCONST2); // Incompatible fenums forbidden! ^ found : @Fenum("B") int required: @MyFenum int -FenumDemo.java:54: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @Fenum("B") int +FenumDemo.java:55: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @Fenum("B") int if (TestStatic.ACONST1 < TestStatic.BCONST2) {} ^ -FenumDemo.java:56: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @Fenum("B") int +FenumDemo.java:57: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @Fenum("B") int if (TestStatic.ACONST1 == TestStatic.BCONST2) {} ^ -FenumDemo.java:58: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @MyFenum int +FenumDemo.java:59: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @MyFenum int if (TestStatic.ACONST1 >= TestStatic.CCONST2) {} ^ -FenumDemo.java:61: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @FenumUnqualified int +FenumDemo.java:62: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("A") int and @FenumUnqualified int if (TestStatic.ACONST1 < 5) {} ^ -FenumDemo.java:63: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("B") int and @FenumUnqualified int +FenumDemo.java:64: error: [binary.type.incompatible] binary operation between incompatible fenums: @Fenum("B") int and @FenumUnqualified int if (TestStatic.BCONST1 > 5) {} ^ -FenumDemo.java:65: error: [binary.type.incompatible] binary operation between incompatible fenums: @MyFenum int and @FenumUnqualified int +FenumDemo.java:66: error: [binary.type.incompatible] binary operation between incompatible fenums: @MyFenum int and @FenumUnqualified int if (TestStatic.CCONST1 == 5) {} ^ 15 errors diff --git a/docs/examples/units-extension/Expected.txt b/docs/examples/units-extension/Expected.txt index 24af6a52cca..7cd1074cddb 100644 --- a/docs/examples/units-extension/Expected.txt +++ b/docs/examples/units-extension/Expected.txt @@ -1,9 +1,9 @@ -UnitsExtensionDemo.java:14: error: [assignment.type.incompatible] incompatible types in assignment. +UnitsExtensionDemo.java:15: error: [assignment.type.incompatible] incompatible types in assignment. frq = 5; ^ found : @UnknownUnits int required: @Hz int -UnitsExtensionDemo.java:67: error: [assignment.type.incompatible] incompatible types in assignment. +UnitsExtensionDemo.java:68: error: [assignment.type.incompatible] incompatible types in assignment. @Hz int badTernaryAssign = seconds > 10 ? hertz : kilohertz; ^ found : @Frequency int From 080ff481a75d741e8d3c60f46b8b8352677f427d Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 16 Sep 2021 15:29:44 -0400 Subject: [PATCH 12/23] remove BOTH_TO_THEN and BOTH_TO_ELSE --- checker/tests/nullness/Issue3622.java | 13 +------------ .../dataflow/analysis/ForwardAnalysisImpl.java | 16 ---------------- .../dataflow/analysis/Store.java | 4 ---- .../cfg/builder/CFGTranslationPhaseOne.java | 3 +-- 4 files changed, 2 insertions(+), 34 deletions(-) diff --git a/checker/tests/nullness/Issue3622.java b/checker/tests/nullness/Issue3622.java index 7c078232705..903963e0fca 100644 --- a/checker/tests/nullness/Issue3622.java +++ b/checker/tests/nullness/Issue3622.java @@ -73,10 +73,7 @@ public boolean equals(@Nullable Object obj9) { public class ImmutableIntList4 { @Override - @SuppressWarnings( - "contracts.conditional.postcondition.not.satisfied" // TODO: `if` needs the - // BOTH_TO_THEN treatment that ?: gets. - ) + @SuppressWarnings("contracts.conditional.postcondition.not.satisfied") public boolean equals(@Nullable Object obj4) { boolean b; if (obj4 instanceof ImmutableIntList4) { @@ -91,10 +88,6 @@ public boolean equals(@Nullable Object obj4) { public class ImmutableIntList5 { @Override - @SuppressWarnings( - "contracts.conditional.postcondition.not.satisfied" // TODO: Need special treatment - // for true and false boolean literals (cut off dead parts of graph). - ) public boolean equals(@Nullable Object obj5) { return true ? obj5 instanceof ImmutableIntList5 : obj5 instanceof ImmutableIntList5; } @@ -103,10 +96,6 @@ public boolean equals(@Nullable Object obj5) { public class ImmutableIntList6 { @Override - @SuppressWarnings( - "contracts.conditional.postcondition.not.satisfied" // TODO: Need special treatment - // for true and false boolean literals (cut off dead parts of graph). - ) public boolean equals(@Nullable Object obj6) { return true ? obj6 instanceof ImmutableIntList6 : false; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java index 884ecd19423..af421524249 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java @@ -461,22 +461,6 @@ protected void propagateStoresTo( Store.Kind.ELSE, addToWorklistAgain); break; - case BOTH_TO_THEN: - addStoreBefore( - succ, - node, - currentInput.getRegularStore(), - Store.Kind.THEN, - addToWorklistAgain); - break; - case BOTH_TO_ELSE: - addStoreBefore( - succ, - node, - currentInput.getRegularStore(), - Store.Kind.ELSE, - addToWorklistAgain); - break; } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java index 656ced5dc9d..fd2287dcf06 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/Store.java @@ -39,10 +39,6 @@ public static enum FlowRule { THEN_TO_THEN, /** Else store flows to the else of successor. Then store is ignored. */ ELSE_TO_ELSE, - /** Both stores flow to the then of successor. */ - BOTH_TO_THEN, - /** Both stores flow to the else of successor. */ - BOTH_TO_ELSE, } /** diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index ee077d94cdc..806be444fc0 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -2278,12 +2278,11 @@ public Node visitConditionalExpression(ConditionalExpressionTree tree, Void p) { addLabelForNextNode(trueStart); Node trueExpr = scan(tree.getTrueExpression(), p); trueExpr = conditionalExprPromotion(trueExpr, exprType); - extendWithExtendedNode(new UnconditionalJump(merge, FlowRule.BOTH_TO_THEN)); + extendWithExtendedNode(new UnconditionalJump(merge)); addLabelForNextNode(falseStart); Node falseExpr = scan(tree.getFalseExpression(), p); falseExpr = conditionalExprPromotion(falseExpr, exprType); - extendWithExtendedNode(new UnconditionalJump(merge, FlowRule.BOTH_TO_ELSE)); addLabelForNextNode(merge); Node node = new TernaryExpressionNode(tree, condition, trueExpr, falseExpr); From d70186b01c7d615abcb526bc4a0522da52c3edd4 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 17 Sep 2021 13:23:07 -0400 Subject: [PATCH 13/23] fix bug and refactor --- .../initialization/InitializationStore.java | 4 +-- .../checker/lock/LockAnalysis.java | 5 +--- .../checker/lock/LockStore.java | 3 +- .../checker/nullness/KeyForAnalysis.java | 5 +--- .../checker/nullness/KeyForStore.java | 2 +- .../checker/nullness/NullnessAnalysis.java | 5 +--- .../checker/nullness/NullnessStore.java | 4 +-- .../framework/flow/CFAbstractAnalysis.java | 7 +++++ .../framework/flow/CFAbstractStore.java | 29 ++++++++++++++++++- .../framework/flow/CFAbstractTransfer.java | 4 +-- .../framework/flow/CFAnalysis.java | 5 +--- .../framework/flow/CFStore.java | 2 +- 12 files changed, 46 insertions(+), 29 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java index 438363aaa15..eff01b8a60f 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -46,9 +46,7 @@ public class InitializationStore, S extends Initial * @param sequentialSemantics should the analysis use sequential Java semantics? */ public InitializationStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - initializedFields = new HashSet<>(4); - invariantFields = new HashMap<>(4); + this(analysis, sequentialSemantics, false); } public InitializationStore( diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java index a50d6783db1..568b5be17ef 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java @@ -40,10 +40,7 @@ public LockStore createEmptyStore(boolean sequentialSemantics) { @Override public LockStore createBottomStore(boolean sequentialSemantics) { - if (bottomStore == null) { - bottomStore = new LockStore(this, sequentialSemantics, true); - } - return bottomStore; + return new LockStore(this, sequentialSemantics, true); } @Override diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 5fcea3dc13a..45c51273467 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -42,8 +42,7 @@ public class LockStore extends CFAbstractStore { private final LockAnnotatedTypeFactory atypeFactory; public LockStore(LockAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - this.atypeFactory = (LockAnnotatedTypeFactory) analysis.getTypeFactory(); + this(analysis, sequentialSemantics, false); } public LockStore(LockAnalysis analysis, boolean sequentialSemantics, boolean isBottom) { diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java index abb67583b20..6647b4b45eb 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java @@ -29,10 +29,7 @@ public KeyForStore createEmptyStore(boolean sequentialSemantics) { @Override public KeyForStore createBottomStore(boolean sequentialSemantics) { - if (bottomStore == null) { - bottomStore = new KeyForStore(this, sequentialSemantics, true); - } - return bottomStore; + return new KeyForStore(this, sequentialSemantics); } @Override diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java index 5cac977968f..10645948620 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java @@ -6,7 +6,7 @@ public class KeyForStore extends CFAbstractStore { public KeyForStore( CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); + this(analysis, sequentialSemantics, false); } public KeyForStore( diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java index c6b9acf233b..1b024ed1a7c 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java @@ -33,10 +33,7 @@ public NullnessStore createEmptyStore(boolean sequentialSemantics) { @Override public NullnessStore createBottomStore(boolean sequentialSemantics) { - if (bottomStore == null) { - bottomStore = new NullnessStore(this, sequentialSemantics, true); - } - return bottomStore; + return new NullnessStore(this, sequentialSemantics, true); } @Override diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java index b7e37840eb9..25e408c87dd 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java @@ -30,9 +30,7 @@ public class NullnessStore extends InitializationStore analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); - isPolyNullNonNull = false; - isPolyNullNull = false; + this(analysis, sequentialSemantics, false); } public NullnessStore( diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index 8a361df7057..ec47e099ed2 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -184,6 +184,13 @@ public T createTransferFunction() { */ public abstract S createBottomStore(boolean sequentialSemantics); + public S getBottomStore(boolean sequentialSemantics) { + if (bottomStore == null) { + bottomStore = createBottomStore(sequentialSemantics); + } + return bottomStore; + } + /** * Returns an identical copy of the store {@code s}. * diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index 0d394505d31..b0228e7cd64 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -32,10 +32,12 @@ import org.plumelib.util.UniqueId; import java.util.HashMap; +import java.util.HashSet; import java.util.Iterator; import java.util.List; import java.util.Map; import java.util.Objects; +import java.util.Set; import java.util.StringJoiner; import java.util.concurrent.atomic.AtomicLong; import java.util.function.BinaryOperator; @@ -116,6 +118,8 @@ public Map getFieldValues() { /** Is the store for unreachable code branch? */ protected final boolean isBottom; + protected final Set bottomAnnos; + /** The unique ID for the next-created object. */ private static final AtomicLong nextUid = new AtomicLong(0); /** The unique ID of this object. */ @@ -151,6 +155,9 @@ protected CFAbstractStore( classValues = new HashMap<>(); this.sequentialSemantics = sequentialSemantics; this.isBottom = isBottom; + this.bottomAnnos = new HashSet<>(); + this.bottomAnnos.addAll( + analysis.getTypeFactory().getQualifierHierarchy().getBottomAnnotations()); } /** Copy constructor. */ @@ -164,6 +171,7 @@ protected CFAbstractStore(CFAbstractStore other) { classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; this.isBottom = other.isBottom; + this.bottomAnnos = other.bottomAnnos; } /** @@ -753,6 +761,8 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(FieldAccessNode n) { + if (isBottom) return getBottomValue(n); + JavaExpression je = JavaExpression.fromNodeFieldAccess(n); if (je instanceof FieldAccess) { return fieldValues.get((FieldAccess) je); @@ -790,6 +800,8 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(MethodInvocationNode n) { + if (isBottom) return getBottomValue(n); + JavaExpression method = JavaExpression.fromNode(n); if (method == null) { return null; @@ -806,6 +818,7 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(ArrayAccessNode n) { + if (isBottom) return getBottomValue(n); ArrayAccess arrayAccess = JavaExpression.fromArrayAccess(n); return arrayValues.get(arrayAccess); } @@ -1070,6 +1083,7 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * available */ public @Nullable V getValue(LocalVariableNode n) { + if (isBottom) return getBottomValue(n); Element el = n.getElement(); return localVariableValues.get(new LocalVariable(el)); } @@ -1087,9 +1101,20 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * is available */ public @Nullable V getValue(ThisNode n) { + if (isBottom) return getBottomValue(n); return thisValue; } + /** + * Return the bottom value for the input node + * + * @param node the input {@link Node} + * @return the bottom value + */ + private V getBottomValue(Node node) { + return analysis.createAbstractValue(bottomAnnos, node.getType()); + } + /* --------------------------------------------------------- */ /* Helper and miscellaneous methods */ /* --------------------------------------------------------- */ @@ -1279,7 +1304,9 @@ public String visualize(CFGVisualizer viz) { @SuppressWarnings("unchecked") CFGVisualizer castedViz = (CFGVisualizer) viz; String internal = internalVisualize(castedViz); - if (internal.trim().isEmpty()) { + if (isBottom) { + return this.getClassAndUid() + " - Bottom"; + } else if (internal.trim().isEmpty()) { return this.getClassAndUid() + "()"; } else { return this.getClassAndUid() + "(" + viz.getSeparator() + internal + ")"; diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 760147291b0..745b3d27cfb 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1372,9 +1372,9 @@ public TransferResult visitBooleanLiteral( TransferResult result = super.visitBooleanLiteral(n, vsTransferInput); if (n.getValue()) { thenStore = result.getThenStore(); - elseStore = analysis.createBottomStore(sequentialSemantics); + elseStore = analysis.getBottomStore(sequentialSemantics); } else { - thenStore = analysis.createBottomStore(sequentialSemantics); + thenStore = analysis.getBottomStore(sequentialSemantics); elseStore = result.getElseStore(); } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java index 250db12905e..f6e9d765047 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java @@ -30,10 +30,7 @@ public CFStore createEmptyStore(boolean sequentialSemantics) { @Override public CFStore createBottomStore(boolean sequentialSemantics) { - if (bottomStore == null) { - bottomStore = new CFStore(this, sequentialSemantics, true); - } - return bottomStore; + return new CFStore(this, sequentialSemantics, true); } @Override diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java index 2c8d110613b..35503ebf140 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java @@ -4,7 +4,7 @@ public class CFStore extends CFAbstractStore { public CFStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); + this(analysis, sequentialSemantics, false); } public CFStore( From 5b616d3b051cbaff2b13e2e04a63ab21830ee37a Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 21 Sep 2021 20:00:28 -0400 Subject: [PATCH 14/23] hack CFAbastractValue.combineOneAnnotation --- .../org/checkerframework/framework/flow/CFAbstractValue.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java index 87c57945b08..651f5a0456b 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java @@ -359,6 +359,10 @@ private AnnotationMirror getBackUpAnnoIn(AnnotationMirror top) { AnnotationMirror top, boolean canCombinedSetBeMissingAnnos) { + if (typeVar == null) { + return getBackUpAnnoIn(top); + } + QualifierHierarchy hierarchy = analysis.getTypeFactory().getQualifierHierarchy(); AnnotationMirror upperBound = typeVar.getEffectiveAnnotationInHierarchy(top); From e83dea755b7052c2b3de9ea50308a395390b29a4 Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 21 Sep 2021 23:12:11 -0400 Subject: [PATCH 15/23] only use bottom store when the boolean literal is a condition on its own --- checker/tests/nullness/Issue293.java | 1 - .../framework/flow/CFAbstractTransfer.java | 34 +++++++++++++++++-- 2 files changed, 32 insertions(+), 3 deletions(-) diff --git a/checker/tests/nullness/Issue293.java b/checker/tests/nullness/Issue293.java index c17ab75fe76..f1ae6c1c038 100644 --- a/checker/tests/nullness/Issue293.java +++ b/checker/tests/nullness/Issue293.java @@ -45,7 +45,6 @@ void test4() throws Exception { s = null; } } finally { - // :: error: argument.type.incompatible write(s); } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 745b3d27cfb..d30632df613 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1,6 +1,7 @@ package org.checkerframework.framework.flow; import com.sun.source.tree.ClassTree; +import com.sun.source.tree.ConditionalExpressionTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; @@ -1364,12 +1365,41 @@ public TransferResult visitStringConversion( return result; } + /** + * Check if the given tree is a condition (in if/while/...) + * + * @param tree input tree + * @return ture if the given tree is a condition + */ + boolean isCondition(ExpressionTree tree) { + TreePath path = analysis.getTypeFactory().getPath(tree); + do { + path = path.getParentPath(); + } while (path != null && path.getLeaf().getKind() == Tree.Kind.PARENTHESIZED); + + Tree parentTree = path.getLeaf(); + + // Is it necessary to consider `x = true ? y : z` + if (parentTree.getKind() == Tree.Kind.CONDITIONAL_EXPRESSION) { + return ((ConditionalExpressionTree) parentTree).getCondition() == tree; + } + + return parentTree.getKind() == Tree.Kind.IF + || parentTree.getKind() == Tree.Kind.WHILE_LOOP + || parentTree.getKind() == Tree.Kind.DO_WHILE_LOOP + || parentTree.getKind() == Tree.Kind.FOR_LOOP; + } + @Override public TransferResult visitBooleanLiteral( BooleanLiteralNode n, TransferInput vsTransferInput) { - S thenStore, elseStore; - TransferResult result = super.visitBooleanLiteral(n, vsTransferInput); + + if (!isCondition(n.getTree())) { + return result; + } + + S thenStore, elseStore; if (n.getValue()) { thenStore = result.getThenStore(); elseStore = analysis.getBottomStore(sequentialSemantics); From ea69c0a748daf944ff4b81a1e245a1fd52b4a654 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 22 Sep 2021 08:30:51 -0400 Subject: [PATCH 16/23] suppress intern error --- .../org/checkerframework/framework/flow/CFAbstractTransfer.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index d30632df613..0ef56f7c27a 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1371,6 +1371,7 @@ public TransferResult visitStringConversion( * @param tree input tree * @return ture if the given tree is a condition */ + @SuppressWarnings("interning:not.interned") boolean isCondition(ExpressionTree tree) { TreePath path = analysis.getTypeFactory().getPath(tree); do { From 2e032275d93fe14dc18ca322a1ee8624a95f14a3 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 22 Sep 2021 09:14:31 -0400 Subject: [PATCH 17/23] adapt expected error --- checker/tests/resourceleak/ACSocketTest.java | 1 - 1 file changed, 1 deletion(-) diff --git a/checker/tests/resourceleak/ACSocketTest.java b/checker/tests/resourceleak/ACSocketTest.java index e6f3440a081..11d77a47ce1 100644 --- a/checker/tests/resourceleak/ACSocketTest.java +++ b/checker/tests/resourceleak/ACSocketTest.java @@ -127,7 +127,6 @@ void replaceVarWithNull(String address, int port, boolean b, boolean c) { void ownershipTransfer(String address, int port) { Socket s1 = null; try { - // :: error: required.method.not.called s1 = new Socket(address, port); } catch (IOException e) { From 74083177381e149ad934ae507aa1de6eac51a8f0 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 22 Sep 2021 21:41:49 -0400 Subject: [PATCH 18/23] change bottom value for lock type system --- .../org/checkerframework/checker/lock/LockStore.java | 9 +++++++++ .../checkerframework/framework/flow/CFAbstractStore.java | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 45c51273467..a246fadda92 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -3,6 +3,7 @@ import org.checkerframework.checker.lock.LockAnnotatedTypeFactory.SideEffectAnnotation; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; import org.checkerframework.dataflow.expression.ArrayAccess; import org.checkerframework.dataflow.expression.ClassName; @@ -19,6 +20,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import java.util.ArrayList; +import java.util.Collections; import java.util.Set; import javax.lang.model.element.AnnotationMirror; @@ -167,6 +169,13 @@ public void setInConstructorOrInitializer() { return super.getValue(expr); } + @Override + protected CFValue getBottomValue(Node node) { + AnnotationMirror guardSatisfied = + ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).GUARDSATISFIED; + return analysis.createAbstractValue(Collections.singleton(guardSatisfied), node.getType()); + } + @Override protected String internalVisualize(CFGVisualizer viz) { return viz.visualizeStoreKeyVal("inConstructorOrInitializer", inConstructorOrInitializer) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index b0228e7cd64..f69468975e5 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -1111,7 +1111,7 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * @param node the input {@link Node} * @return the bottom value */ - private V getBottomValue(Node node) { + protected V getBottomValue(Node node) { return analysis.createAbstractValue(bottomAnnos, node.getType()); } From 44c97a7e742edb8f9e7c1b507c27a9a846189868 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 23 Sep 2021 08:14:18 -0400 Subject: [PATCH 19/23] fix bug in bottom store, to resolve the must-call case --- .../checker/lock/LockStore.java | 6 +++--- .../framework/flow/CFAbstractStore.java | 20 ++++++++++--------- 2 files changed, 14 insertions(+), 12 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index a246fadda92..6459acae141 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -3,7 +3,6 @@ import org.checkerframework.checker.lock.LockAnnotatedTypeFactory.SideEffectAnnotation; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; import org.checkerframework.dataflow.expression.ArrayAccess; import org.checkerframework.dataflow.expression.ClassName; @@ -25,6 +24,7 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.type.TypeMirror; /** * The Lock Store behaves like CFAbstractStore but requires the ability to insert exact annotations. @@ -170,10 +170,10 @@ public void setInConstructorOrInitializer() { } @Override - protected CFValue getBottomValue(Node node) { + protected CFValue getBottomValue(TypeMirror type) { AnnotationMirror guardSatisfied = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).GUARDSATISFIED; - return analysis.createAbstractValue(Collections.singleton(guardSatisfied), node.getType()); + return analysis.createAbstractValue(Collections.singleton(guardSatisfied), type); } @Override diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index f69468975e5..ea5a056db4b 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -730,6 +730,8 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(JavaExpression expr) { + if (isBottom) return getBottomValue(expr.getType()); + if (expr instanceof LocalVariable) { LocalVariable localVar = (LocalVariable) expr; return localVariableValues.get(localVar); @@ -761,7 +763,7 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(FieldAccessNode n) { - if (isBottom) return getBottomValue(n); + if (isBottom) return getBottomValue(n.getType()); JavaExpression je = JavaExpression.fromNodeFieldAccess(n); if (je instanceof FieldAccess) { @@ -800,7 +802,7 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(MethodInvocationNode n) { - if (isBottom) return getBottomValue(n); + if (isBottom) return getBottomValue(n.getType()); JavaExpression method = JavaExpression.fromNode(n); if (method == null) { @@ -818,7 +820,7 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(ArrayAccessNode n) { - if (isBottom) return getBottomValue(n); + if (isBottom) return getBottomValue(n.getType()); ArrayAccess arrayAccess = JavaExpression.fromArrayAccess(n); return arrayValues.get(arrayAccess); } @@ -1083,7 +1085,7 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * available */ public @Nullable V getValue(LocalVariableNode n) { - if (isBottom) return getBottomValue(n); + if (isBottom) return getBottomValue(n.getType()); Element el = n.getElement(); return localVariableValues.get(new LocalVariable(el)); } @@ -1101,18 +1103,18 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * is available */ public @Nullable V getValue(ThisNode n) { - if (isBottom) return getBottomValue(n); + if (isBottom) return getBottomValue(n.getType()); return thisValue; } /** - * Return the bottom value for the input node + * Return the bottom value for the input {@link TypeMirror} * - * @param node the input {@link Node} + * @param type the input {@link TypeMirror} * @return the bottom value */ - protected V getBottomValue(Node node) { - return analysis.createAbstractValue(bottomAnnos, node.getType()); + protected V getBottomValue(TypeMirror type) { + return analysis.createAbstractValue(bottomAnnos, type); } /* --------------------------------------------------------- */ From a6509e50f95a9508ff38640b3efa6ad5dce03588 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 23 Sep 2021 12:50:42 -0400 Subject: [PATCH 20/23] adapt bottom value for lock type system --- .../org/checkerframework/checker/lock/LockStore.java | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 6459acae141..e1facca8c92 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -19,7 +19,8 @@ import org.checkerframework.javacutil.AnnotationUtils; import java.util.ArrayList; -import java.util.Collections; +import java.util.Arrays; +import java.util.HashSet; import java.util.Set; import javax.lang.model.element.AnnotationMirror; @@ -171,9 +172,10 @@ public void setInConstructorOrInitializer() { @Override protected CFValue getBottomValue(TypeMirror type) { - AnnotationMirror guardSatisfied = - ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).GUARDSATISFIED; - return analysis.createAbstractValue(Collections.singleton(guardSatisfied), type); + AnnotationMirror guardBy = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).GUARDEDBY; + AnnotationMirror lockHeld = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).LOCKHELD; + + return analysis.createAbstractValue(new HashSet<>(Arrays.asList(lockHeld, guardBy)), type); } @Override From 9041117447d3f94bbc8ab57f3fadba877bc56303 Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 28 Sep 2021 09:35:30 -0400 Subject: [PATCH 21/23] no insertion to bottom store --- .../org/checkerframework/framework/flow/CFAbstractStore.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index ea5a056db4b..077261ddf73 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -410,7 +410,7 @@ public final void insertOrRefinePermitNondeterministic( */ protected void insertOrRefine( JavaExpression expr, AnnotationMirror newAnno, boolean permitNondeterministic) { - if (!canInsertJavaExpression(expr)) { + if (!canInsertJavaExpression(expr) || isBottom) { return; } if (!(permitNondeterministic || expr.isDeterministic(analysis.getTypeFactory()))) { From 40a27ca33c5ba2364cf943d121ab7ba9b11997ba Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 28 Sep 2021 11:10:27 -0400 Subject: [PATCH 22/23] add javadoc --- .../initialization/InitializationStore.java | 7 +++++++ .../checkerframework/checker/lock/LockStore.java | 7 +++++++ .../checker/nullness/KeyForStore.java | 7 +++++++ .../checker/nullness/NullnessStore.java | 7 +++++++ .../framework/flow/CFAbstractAnalysis.java | 10 +++++++++- .../framework/flow/CFAbstractStore.java | 16 +++++++++++++++- .../checkerframework/framework/flow/CFStore.java | 7 +++++++ 7 files changed, 59 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java index eff01b8a60f..a8b76327694 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -49,6 +49,13 @@ public InitializationStore(CFAbstractAnalysis analysis, boolean sequent this(analysis, sequentialSemantics, false); } + /** + * Creates a new InitializationStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @param isBottom is the store a bottom store? + */ public InitializationStore( CFAbstractAnalysis analysis, boolean sequentialSemantics, boolean isBottom) { super(analysis, sequentialSemantics, isBottom); diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index e1facca8c92..c856d5e5b76 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -48,6 +48,13 @@ public LockStore(LockAnalysis analysis, boolean sequentialSemantics) { this(analysis, sequentialSemantics, false); } + /** + * Constructor for LockStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @param isBottom is the store a bottom store? + */ public LockStore(LockAnalysis analysis, boolean sequentialSemantics, boolean isBottom) { super(analysis, sequentialSemantics, isBottom); this.atypeFactory = (LockAnnotatedTypeFactory) analysis.getTypeFactory(); diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java index 10645948620..2bdf4e45f13 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java @@ -9,6 +9,13 @@ public KeyForStore( this(analysis, sequentialSemantics, false); } + /** + * Constructor for KeyForStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @param isBottom is the store a bottom store? + */ public KeyForStore( CFAbstractAnalysis analysis, boolean sequentialSemantics, diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java index 25e408c87dd..b4987fdbf36 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java @@ -33,6 +33,13 @@ public NullnessStore( this(analysis, sequentialSemantics, false); } + /** + * Constructor for NullnessStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @param isBottom is the store a bottom store? + */ public NullnessStore( CFAbstractAnalysis analysis, boolean sequentialSemantics, diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index ec47e099ed2..62269638081 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -173,17 +173,25 @@ public T createTransferFunction() { /** * Returns an empty store of the appropriate type. * + * @param sequentialSemantics should the analysis use sequential Java semantics? * @return an empty store of the appropriate type */ public abstract S createEmptyStore(boolean sequentialSemantics); /** - * Create the unique shared instance of bottom store for the underlying type system + * Create the unique shared instance of bottom store for the underlying type system. * + * @param sequentialSemantics should the analysis use sequential Java semantics? * @return the bottom store instance of the appropriate type */ public abstract S createBottomStore(boolean sequentialSemantics); + /** + * Get the singleton of the bottom store corresponding to the type. + * + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @return the shared instance of bottom store for the underyling type system + */ public S getBottomStore(boolean sequentialSemantics) { if (bottomStore == null) { bottomStore = createBottomStore(sequentialSemantics); diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index 077261ddf73..411ed9ff22c 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -115,9 +115,13 @@ public Map getFieldValues() { */ protected final boolean sequentialSemantics; - /** Is the store for unreachable code branch? */ + /** + * Is the store a bottom store (a special store that only exists in dead branches and yields + * bottom types to avoid false positive)? + */ protected final boolean isBottom; + /** The bottom annotations for the current type system. */ protected final Set bottomAnnos; /** The unique ID for the next-created object. */ @@ -144,6 +148,13 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti this(analysis, sequentialSemantics, false); } + /** + * Creates a new CFAbstractStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @param isBottom is the store a bottom store? + */ protected CFAbstractStore( CFAbstractAnalysis analysis, boolean sequentialSemantics, boolean isBottom) { this.analysis = analysis; @@ -696,6 +707,8 @@ public void replaceValue(JavaExpression expr, @Nullable V value) { /** * Remove any knowledge about the expression {@code expr} (correctly deciding where to remove * the information depending on the type of the expression {@code expr}). + * + * @param expr the expression of which the value is to be cleared */ public void clearValue(JavaExpression expr) { if (expr.containsUnknown()) { @@ -1081,6 +1094,7 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * Returns the current abstract value of a local variable, or {@code null} if no information is * available. * + * @param n the local variable to look up in this store * @return the current abstract value of a local variable, or {@code null} if no information is * available */ diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java index 35503ebf140..57acab4c1c0 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java @@ -7,6 +7,13 @@ public CFStore(CFAbstractAnalysis analysis, boolean sequent this(analysis, sequentialSemantics, false); } + /** + * Constructor for CFStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + * @param isBottom is the store a bottom store? + */ public CFStore( CFAbstractAnalysis analysis, boolean sequentialSemantics, From a131f413f36dc19fe131531e184c60f3aba9aa0d Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 28 Sep 2021 11:28:58 -0400 Subject: [PATCH 23/23] apply default to void methodreturns --- .../org/checkerframework/framework/flow/CFAbstractValue.java | 4 ---- .../framework/util/defaults/QualifierDefaults.java | 4 +--- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java index 651f5a0456b..87c57945b08 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java @@ -359,10 +359,6 @@ private AnnotationMirror getBackUpAnnoIn(AnnotationMirror top) { AnnotationMirror top, boolean canCombinedSetBeMissingAnnos) { - if (typeVar == null) { - return getBackUpAnnoIn(top); - } - QualifierHierarchy hierarchy = analysis.getTypeFactory().getQualifierHierarchy(); AnnotationMirror upperBound = typeVar.getEffectiveAnnotationInHierarchy(top); diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java index 2d713db7b99..6fc7d53eb3e 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java +++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java @@ -20,7 +20,6 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedNoType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedUnionType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; @@ -843,8 +842,7 @@ protected boolean shouldBeAnnotated( // || type.getKind() == TypeKind.EXECUTABLE || type.getKind() == TypeKind.NONE || type.getKind() == TypeKind.WILDCARD - || (type.getKind() == TypeKind.TYPEVAR && !applyToTypeVar) - || type instanceof AnnotatedNoType); + || (type.getKind() == TypeKind.TYPEVAR && !applyToTypeVar)); } /**