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 new LockBottomStore(this, sequentialSemantics);
+    }
 }

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

@@ -0,0 +1,116 @@
+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<AnnotationMirror> 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) {}
+}

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,117 @@
+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<AnnotationMirror> bottomAnnos;
+
+    public KeyForBottomStore(
+            CFAbstractAnalysis<KeyForValue, KeyForStore, ?> 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) {}
+}

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,118 @@
+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<AnnotationMirror> bottomAnnos;
+
+    public NullnessBottomStore(
+            CFAbstractAnalysis<NullnessValue, NullnessStore, ?> 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) {}
+}

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;