Introduce bottom store to improve dataflow analysis

checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java

@@ -46,7 +46,19 @@ public class InitializationStore<V extends CFAbstractValue<V>, S extends Initial
      * @param sequentialSemantics should the analysis use sequential Java semantics?
      */
     public InitializationStore(CFAbstractAnalysis<V, S, ?> 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<V, S, ?> analysis, boolean sequentialSemantics, boolean isBottom) {
+        super(analysis, sequentialSemantics, isBottom);
         initializedFields = new HashSet<>(4);
         invariantFields = new HashMap<>(4);
     }

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);

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.
@@ -42,7 +45,18 @@ public class LockStore extends CFAbstractStore<CFValue, LockStore> {
     private final LockAnnotatedTypeFactory atypeFactory;
 
     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 +177,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<CFValue, LockStore, ?> viz) {
         return viz.visualizeStoreKeyVal("inConstructorOrInitializer", inConstructorOrInitializer)

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);

checker/src/main/java/org/checkerframework/checker/nullness/KeyForStore.java

@@ -6,7 +6,21 @@
 public class KeyForStore extends CFAbstractStore<KeyForValue, KeyForStore> {
     public KeyForStore(
             CFAbstractAnalysis<KeyForValue, KeyForStore, ?> 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<KeyForValue, KeyForStore, ?> analysis,
+            boolean sequentialSemantics,
+            boolean isBottom) {
+        super(analysis, sequentialSemantics, isBottom);
     }
 
     protected KeyForStore(CFAbstractStore<KeyForValue, KeyForStore> other) {

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);

checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java

@@ -30,9 +30,23 @@ public class NullnessStore extends InitializationStore<NullnessValue, NullnessSt
     public NullnessStore(
             CFAbstractAnalysis<NullnessValue, NullnessStore, ?> 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<NullnessValue, NullnessStore, ?> analysis,
+            boolean sequentialSemantics,
+            boolean isBottom) {
+        super(analysis, sequentialSemantics, isBottom);
         isPolyNullNonNull = false;
-        isPolyNullNull = false;
+        this.isPolyNullNull = false;
     }
 
     /**

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;

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;
     }
 

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;
             }
 

checker/tests/nullness/Issue293.java

@@ -45,7 +45,6 @@ void test4() throws Exception {
                 s = null;
             }
         } finally {
-            // :: error: argument.type.incompatible
             write(s);
         }
     }

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;
         }

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;
+    }
+}

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) {
 

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;
         }
     }
 

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,
     }
 
     /**

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);

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}.
      *