From 72bedc057af194892db7f36ddbd9cc06562edabc Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 28 Sep 2021 15:47:59 -0400 Subject: [PATCH] add updated files --- .../initialization/InitializationStore.java | 14 +++- .../checker/lock/LockAnalysis.java | 5 ++ .../checker/lock/LockStore.java | 30 ++++++++- .../checker/nullness/KeyForAnalysis.java | 5 ++ .../checker/nullness/KeyForStore.java | 22 ++++++- .../checker/nullness/NullnessAnalysis.java | 5 ++ .../checker/nullness/NullnessStore.java | 18 +++++- checker/tests/formatter/FlowFormatter.java | 1 + checker/tests/index/LubIndex.java | 3 - .../initialization/TryFinallyContinue.java | 4 -- checker/tests/nullness/Issue293.java | 1 - checker/tests/nullness/Issue3622.java | 13 +--- checker/tests/nullness/flow/DeadBranch.java | 11 ++++ checker/tests/resourceleak/ACSocketTest.java | 1 - .../analysis/ForwardAnalysisImpl.java | 16 ----- .../dataflow/analysis/Store.java | 4 -- .../cfg/builder/CFGTranslationPhaseOne.java | 3 +- .../framework/flow/CFAbstractAnalysis.java | 25 ++++++++ .../framework/flow/CFAbstractStore.java | 64 ++++++++++++++++++- .../framework/flow/CFAbstractTransfer.java | 50 +++++++++++++++ .../framework/flow/CFAnalysis.java | 5 ++ .../framework/flow/CFStore.java | 22 ++++++- .../util/defaults/QualifierDefaults.java | 4 +- framework/tests/value/Basics.java | 19 ++---- framework/tests/value/MinLenLUB.java | 3 - 25 files changed, 276 insertions(+), 72 deletions(-) create mode 100644 checker/tests/nullness/flow/DeadBranch.java 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 b2134015f61..a8b76327694 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -46,7 +46,19 @@ public class InitializationStore, S extends Initial * @param sequentialSemantics should the analysis use sequential Java semantics? */ public InitializationStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); + 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); initializedFields = new HashSet<>(4); invariantFields = new HashMap<>(4); } 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 c9b1c7eaad4..568b5be17ef 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,11 @@ public LockStore createEmptyStore(boolean sequentialSemantics) { return new LockStore(this, sequentialSemantics); } + @Override + public LockStore createBottomStore(boolean sequentialSemantics) { + return new LockStore(this, sequentialSemantics, true); + } + @Override public LockStore createCopiedStore(LockStore s) { return new LockStore(this, s); 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 5cf29c162e9..65947d83b5a 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -19,10 +19,13 @@ import org.checkerframework.javacutil.AnnotationUtils; import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; import java.util.Set; 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. @@ -41,8 +44,25 @@ public class LockStore extends CFAbstractStore { private final LockAnnotatedTypeFactory atypeFactory; + /** + * Constructor to create a non-bottom LockStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + */ public LockStore(LockAnalysis analysis, boolean sequentialSemantics) { - super(analysis, 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(); } @@ -163,6 +183,14 @@ public void setInConstructorOrInitializer() { return super.getValue(expr); } + @Override + protected CFValue getBottomValue(TypeMirror type) { + AnnotationMirror guardBy = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).GUARDEDBY; + AnnotationMirror lockHeld = ((LockAnnotatedTypeFactory) analysis.getTypeFactory()).LOCKHELD; + + return analysis.createAbstractValue(new HashSet<>(Arrays.asList(lockHeld, guardBy)), type); + } + @Override protected String internalVisualize(CFGVisualizer viz) { return viz.visualizeStoreKeyVal("inConstructorOrInitializer", inConstructorOrInitializer) 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 0b82b9fb54a..6647b4b45eb 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java @@ -27,6 +27,11 @@ public KeyForStore createEmptyStore(boolean sequentialSemantics) { return new KeyForStore(this, sequentialSemantics); } + @Override + public KeyForStore createBottomStore(boolean sequentialSemantics) { + return new KeyForStore(this, sequentialSemantics); + } + @Override public KeyForStore createCopiedStore(KeyForStore store) { return new KeyForStore(store); 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..7785a88b18d 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java @@ -4,9 +4,29 @@ import org.checkerframework.framework.flow.CFAbstractStore; public class KeyForStore extends CFAbstractStore { + /** + * Constructor to create a non-bottom KeyForStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + */ public KeyForStore( CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); + 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, + boolean isBottom) { + super(analysis, sequentialSemantics, isBottom); } protected KeyForStore(CFAbstractStore 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 09ec25b47b2..1b024ed1a7c 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,11 @@ public NullnessStore createEmptyStore(boolean sequentialSemantics) { return new NullnessStore(this, sequentialSemantics); } + @Override + public NullnessStore createBottomStore(boolean sequentialSemantics) { + return new NullnessStore(this, sequentialSemantics, true); + } + @Override public NullnessStore createCopiedStore(NullnessStore s) { return new NullnessStore(s); 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 d90d56206c4..b4987fdbf36 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,23 @@ public class NullnessStore extends InitializationStore analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); + 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, + boolean isBottom) { + super(analysis, sequentialSemantics, isBottom); isPolyNullNonNull = false; - isPolyNullNull = false; + this.isPolyNullNull = false; } /** diff --git a/checker/tests/formatter/FlowFormatter.java b/checker/tests/formatter/FlowFormatter.java index a0350f625a4..6d7e641d6d5 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/TryFinallyContinue.java b/checker/tests/initialization/TryFinallyContinue.java index 6b22d5bcb04..25b7ccc903b 100644 --- a/checker/tests/initialization/TryFinallyContinue.java +++ b/checker/tests/initialization/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/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/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/checker/tests/nullness/flow/DeadBranch.java b/checker/tests/nullness/flow/DeadBranch.java new file mode 100644 index 00000000000..7360c57decc --- /dev/null +++ b/checker/tests/nullness/flow/DeadBranch.java @@ -0,0 +1,11 @@ +import org.checkerframework.checker.nullness.qual.Nullable; + +class DeadBranch { + + Object foo(@Nullable Object myObj, boolean x) { + if (true) { + myObj = new Object(); + } + return myObj; + } +} 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) { 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); 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 64c5b94396e..62269638081 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -102,6 +102,9 @@ public FieldInitialValue(FieldAccess fieldDecl, V declared, @Nullable V initiali /** 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; + /** * Create a CFAbstractAnalysis. * @@ -170,10 +173,32 @@ 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. + * + * @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); + } + 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 c1d12897af8..bffdb9adb50 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; @@ -113,6 +115,15 @@ public Map getFieldValues() { */ protected final boolean sequentialSemantics; + /** + * 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. */ private static final AtomicLong nextUid = new AtomicLong(0); /** The unique ID of this object. */ @@ -134,6 +145,18 @@ public long getUid() { * @param sequentialSemantics should the analysis use sequential Java semantics? */ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { + 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; localVariableValues = new HashMap<>(); thisValue = null; @@ -142,6 +165,10 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti arrayValues = new HashMap<>(); classValues = new HashMap<>(); this.sequentialSemantics = sequentialSemantics; + this.isBottom = isBottom; + this.bottomAnnos = new HashSet<>(); + this.bottomAnnos.addAll( + analysis.getTypeFactory().getQualifierHierarchy().getBottomAnnotations()); } /** Copy constructor. */ @@ -154,6 +181,8 @@ protected CFAbstractStore(CFAbstractStore other) { arrayValues = new HashMap<>(other.arrayValues); classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; + this.isBottom = other.isBottom; + this.bottomAnnos = other.bottomAnnos; } /** @@ -392,7 +421,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()))) { @@ -678,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()) { @@ -708,10 +739,13 @@ public void clearValue(JavaExpression expr) { * Returns the current abstract value of a Java expression, or {@code null} if no information is * available. * + * @param expr the expression to look up the value * @return the current abstract value of a Java expression, or {@code null} if no information is * 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); @@ -743,6 +777,8 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(FieldAccessNode n) { + if (isBottom) return getBottomValue(n.getType()); + JavaExpression je = JavaExpression.fromNodeFieldAccess(n); if (je instanceof FieldAccess) { return fieldValues.get((FieldAccess) je); @@ -780,6 +816,8 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(MethodInvocationNode n) { + if (isBottom) return getBottomValue(n.getType()); + JavaExpression method = JavaExpression.fromNode(n); if (method == null) { return null; @@ -796,6 +834,7 @@ public void clearValue(JavaExpression expr) { * available */ public @Nullable V getValue(ArrayAccessNode n) { + if (isBottom) return getBottomValue(n.getType()); ArrayAccess arrayAccess = JavaExpression.fromArrayAccess(n); return arrayValues.get(arrayAccess); } @@ -1056,10 +1095,12 @@ 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 */ public @Nullable V getValue(LocalVariableNode n) { + if (isBottom) return getBottomValue(n.getType()); Element el = n.getElement(); return localVariableValues.get(new LocalVariable(el)); } @@ -1077,9 +1118,20 @@ public boolean canAlias(JavaExpression a, JavaExpression b) { * is available */ public @Nullable V getValue(ThisNode n) { + if (isBottom) return getBottomValue(n.getType()); return thisValue; } + /** + * Return the bottom value for the input {@link TypeMirror} + * + * @param type the input {@link TypeMirror} + * @return the bottom value + */ + protected V getBottomValue(TypeMirror type) { + return analysis.createAbstractValue(bottomAnnos, type); + } + /* --------------------------------------------------------- */ /* Helper and miscellaneous methods */ /* --------------------------------------------------------- */ @@ -1090,13 +1142,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); } @@ -1263,7 +1321,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 8fe223befa1..0ef56f7c27a 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; @@ -19,6 +20,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; @@ -1363,6 +1365,54 @@ 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 + */ + @SuppressWarnings("interning:not.interned") + 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) { + 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); + } else { + thenStore = analysis.getBottomStore(sequentialSemantics); + elseStore = result.getElseStore(); + } + + return new ConditionalTransferResult<>( + finishValue(result.getResultValue(), thenStore, elseStore), thenStore, elseStore); + } + /** * Inserts newAnno as the value into all stores (conditional or not) in the result for node. * This is a utility method for subclasses. 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 415b234b6bf..f6e9d765047 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java @@ -28,6 +28,11 @@ public CFStore createEmptyStore(boolean sequentialSemantics) { return new CFStore(this, sequentialSemantics); } + @Override + public CFStore createBottomStore(boolean sequentialSemantics) { + return new CFStore(this, sequentialSemantics, true); + } + @Override public CFStore createCopiedStore(CFStore s) { return new CFStore(s); 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 a2c6c17e7ed..e8d79d82fec 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFStore.java @@ -3,8 +3,28 @@ /** The default store used in the Checker Framework. */ public class CFStore extends CFAbstractStore { + /** + * Constructor to create a non-bottom CFStore. + * + * @param analysis the analysis class this store belongs to + * @param sequentialSemantics should the analysis use sequential Java semantics? + */ public CFStore(CFAbstractAnalysis analysis, boolean sequentialSemantics) { - super(analysis, sequentialSemantics); + 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, + boolean isBottom) { + super(analysis, sequentialSemantics, isBottom); } /** 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)); } /** diff --git a/framework/tests/value/Basics.java b/framework/tests/value/Basics.java index 05787674e97..bd64b98a36f 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; }