Introduce bottom store to improve dataflow analysis

checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java

@@ -48,4 +48,9 @@ public CFValue createAbstractValue(
             Set<AnnotationMirror> annotations, TypeMirror underlyingType) {
         return defaultCreateAbstractValue(this, annotations, underlyingType);
     }
+
+    @Override
+    public LockStore getBottomStore(boolean sequentialSemantics) {
+        return null;
+    }
 }

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

@@ -49,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;
+    }
 }

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<KeyForValue, KeyForStore, ?> 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) {}
+}

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

@@ -44,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;
+    }
 }

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<NullnessValue, NullnessStore, ?> 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) {}
+}

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

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<?, S, ?> viz);
+
+    /**
+     * Is this store a bottom store?
+     *
+     * @return true if this is a bottom store
+     */
+    boolean isBottom();
 }

dataflow/src/main/java/org/checkerframework/dataflow/constantpropagation/ConstantPropagationStore.java

@@ -167,4 +167,9 @@ public boolean canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b)
     public String visualize(CFGVisualizer<?, ConstantPropagationStore, ?> viz) {
         return viz.visualizeStoreKeyVal("constant propagation", null);
     }
+
+    @Override
+    public boolean isBottom() {
+        return false;
+    }
 }

dataflow/src/main/java/org/checkerframework/dataflow/livevariable/LiveVarStore.java

@@ -142,4 +142,9 @@ public String visualize(CFGVisualizer<?, LiveVarStore, ?> viz) {
     public String toString() {
         return liveVarValueSet.toString();
     }
+
+    @Override
+    public boolean isBottom() {
+        return false;
+    }
 }

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java

@@ -68,6 +68,8 @@ public abstract class CFAbstractAnalysis<
     /** Instance of the types utility. */
     protected final Types types;
 
+    protected S bottomStore;
+
     /**
      * Create a CFAbstractAnalysis.
      *
@@ -131,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}.
      *

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java

@@ -853,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);
     }
 
@@ -1060,4 +1066,9 @@ protected String internalVisualize(CFGVisualizer<V, S, ?> viz) {
         }
         return res.toString();
     }
+
+    @Override
+    public boolean isBottom() {
+        return true;
+    }
 }