Boolean variables in dataflow

checker/tests/nullness/Issue406.java

@@ -0,0 +1,27 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class Issue406 {
+  static class LocalDate {}
+
+  private void testFails1(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean eitherIsNull = x1 == null || x2 == null;
+    if (eitherIsNull) return;
+    delegate(x1, x2);
+  }
+
+  private void testFails2(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean firstIsNull = x1 == null;
+    boolean secondIsNull = x2 == null;
+    if (firstIsNull || secondIsNull) return;
+    delegate(x1, x2);
+  }
+
+  private void testWorks(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    if (x1 == null || x2 == null) return;
+    delegate(x1, x2);
+  }
+
+  private void delegate(LocalDate x1, LocalDate x2) {
+    // do something
+  }
+}

checker/tests/optional/OptionalBooleanVariableFlowRefinement.java

@@ -0,0 +1,36 @@
+import java.util.List;
+import java.util.Optional;
+import org.checkerframework.checker.optional.qual.*;
+import org.checkerframework.dataflow.qual.*;
+
+@SuppressWarnings({"optional:parameter", "optional:field", "optional:collection"})
+class OptionalBooleanVariableFlowRefinement {
+
+  void validRefinementTest(Optional<String> opt) {
+    boolean optIsPresent = opt.isPresent();
+    if (optIsPresent) {
+      opt.get(); // Legal
+    }
+  }
+
+  void otherValidRefinement(OptContainer container) {
+    boolean isGetLegal =
+        container.getOptStrs().isPresent() && !container.getOptStrs().get().isEmpty();
+    if (isGetLegal) {
+      container.getOptStrs().get(); // Legal
+    }
+  }
+
+  class OptContainer {
+    private Optional<List<String>> strs;
+
+    public OptContainer(List<String> strs) {
+      this.strs = Optional.ofNullable(strs);
+    }
+
+    @Pure
+    public Optional<List<String>> getOptStrs() {
+      return this.strs;
+    }
+  }
+}

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

@@ -249,39 +249,51 @@ public void updateForMethodCall(
             || (assumePureGetters && ElementUtils.isGetter(method))
             || atypeFactory.isSideEffectFree(method));
     if (hasSideEffect) {
+      localVariableValues
+          .values()
+          .forEach(
+              v -> {
+                if (v != null && v.getThenStore() != null) {
+                  v.getThenStore().updateForSideEffect(gatypeFactory);
+                  v.getElseStore().updateForSideEffect(gatypeFactory);
+                }
+              });
+      updateForSideEffect(gatypeFactory);
+    }
 
-      boolean sideEffectsUnrefineAliases = gatypeFactory.sideEffectsUnrefineAliases;
-
-      // update local variables
-      // TODO: Also remove if any element/argument to the annotation is not
-      // isUnmodifiableByOtherCode.  Example: @KeyFor("valueThatCanBeMutated").
-      if (sideEffectsUnrefineAliases) {
-        localVariableValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
-      }
+    // store information about method call if possible
+    JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode);
+    replaceValue(methodCall, val);
+  }
 
-      // update this value
-      if (sideEffectsUnrefineAliases) {
-        thisValue = null;
-      }
+  public void updateForSideEffect(GenericAnnotatedTypeFactory<?, ?, ?, ?> gatypeFactory) {
+    boolean sideEffectsUnrefineAliases = gatypeFactory.sideEffectsUnrefineAliases;
 
-      // update field values
-      if (sideEffectsUnrefineAliases) {
-        fieldValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
-      } else {
-        // Case 2 (unassignable fields) and case 3 (monotonic fields)
-        updateFieldValuesForMethodCall(gatypeFactory);
-      }
+    // update local variables
+    // TODO: Also remove if any element/argument to the annotation is not
+    // isUnmodifiableByOtherCode.  Example: @KeyFor("valueThatCanBeMutated").
+    if (sideEffectsUnrefineAliases) {
+      localVariableValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
+    }
 
-      // update array values
-      arrayValues.clear();
+    // update this value
+    if (sideEffectsUnrefineAliases) {
+      thisValue = null;
+    }
 
-      // update method values
-      methodCallExpressions.keySet().removeIf(MethodCall::isModifiableByOtherCode);
+    // update field values
+    if (sideEffectsUnrefineAliases) {
+      fieldValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
+    } else {
+      // Case 2 (unassignable fields) and case 3 (monotonic fields)
+      updateFieldValuesForMethodCall(gatypeFactory);
     }
 
-    // store information about method call if possible
-    JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode);
-    replaceValue(methodCall, val);
+    // update array values
+    arrayValues.clear();
+
+    // update method values
+    methodCallExpressions.keySet().removeIf(MethodCall::isModifiableByOtherCode);
   }
 
   /**
@@ -300,7 +312,7 @@ public void updateForMethodCall(
    *     from the store
    */
   protected V newFieldValueAfterMethodCall(
-      FieldAccess fieldAccess, GenericAnnotatedTypeFactory<V, S, ?, ?> atypeFactory, V value) {
+      FieldAccess fieldAccess, GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory, V value) {
     // Handle unassignable fields.
     if (!fieldAccess.isAssignableByOtherCode()) {
       return value;
@@ -324,7 +336,7 @@ protected V newFieldValueAfterMethodCall(
    *     annotation
    */
   protected V newMonotonicFieldValueAfterMethodCall(
-      FieldAccess fieldAccess, GenericAnnotatedTypeFactory<V, S, ?, ?> atypeFactory, V value) {
+      FieldAccess fieldAccess, GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory, V value) {
 
     // case 3: the field has a monotonic annotation
     if (atypeFactory.getSupportedMonotonicTypeQualifiers().isEmpty()) {
@@ -369,7 +381,7 @@ protected V newMonotonicFieldValueAfterMethodCall(
    * @param atypeFactory AnnotatedTypeFactory of the associated checker
    */
   private void updateFieldValuesForMethodCall(
-      GenericAnnotatedTypeFactory<V, S, ?, ?> atypeFactory) {
+      GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory) {
     Map<FieldAccess, V> newFieldValues = new HashMap<>(CollectionsPlume.mapCapacity(fieldValues));
     for (Map.Entry<FieldAccess, V> e : fieldValues.entrySet()) {
       FieldAccess fieldAccess = e.getKey();
@@ -883,10 +895,37 @@ public void updateForAssignment(Node n, @Nullable V val) {
     JavaExpression je = JavaExpression.fromNode(n);
     if (je instanceof ArrayAccess) {
       updateForArrayAssignment((ArrayAccess) je, val);
+      localVariableValues
+          .values()
+          .forEach(
+              v -> {
+                if (v != null && v.getThenStore() != null) {
+                  v.getThenStore().updateForArrayAssignment((ArrayAccess) je, val);
+                  v.getElseStore().updateForArrayAssignment((ArrayAccess) je, val);
+                }
+              });
     } else if (je instanceof FieldAccess) {
       updateForFieldAccessAssignment((FieldAccess) je, val);
+      localVariableValues
+          .values()
+          .forEach(
+              v -> {
+                if (v != null && v.getThenStore() != null) {
+                  v.getThenStore().updateForFieldAccessAssignment((FieldAccess) je, val);
+                  v.getElseStore().updateForFieldAccessAssignment((FieldAccess) je, val);
+                }
+              });
     } else if (je instanceof LocalVariable) {
       updateForLocalVariableAssignment((LocalVariable) je, val);
+      localVariableValues
+          .values()
+          .forEach(
+              v -> {
+                if (v != null && v.getThenStore() != null) {
+                  v.getThenStore().updateForLocalVariableAssignment((LocalVariable) je, val);
+                  v.getElseStore().updateForLocalVariableAssignment((LocalVariable) je, val);
+                }
+              });
     } else {
       throw new BugInCF("Unexpected je of class " + je.getClass());
     }
@@ -1249,6 +1288,86 @@ private S upperBound(S other, boolean shouldWiden) {
     return newStore;
   }
 
+  public S merge(S other) {
+    S newStore = analysis.createEmptyStore(sequentialSemantics);
+
+    for (Map.Entry<LocalVariable, V> e : other.localVariableValues.entrySet()) {
+      // local variables that are only part of one store, but not the other are discarded, as
+      // one of store implicitly contains 'top' for that variable.
+      LocalVariable localVar = e.getKey();
+      V thisVal = localVariableValues.get(localVar);
+      if (thisVal != null) {
+        V otherVal = e.getValue();
+        V mergedVal = thisVal.mostSpecific(otherVal, null);
+        if (mergedVal != null) {
+          newStore.localVariableValues.put(localVar, mergedVal);
+        }
+      }
+    }
+
+    // information about the current object
+    {
+      V otherVal = other.thisValue;
+      V myVal = thisValue;
+      V mergedVal = myVal == null ? null : myVal.mostSpecific(otherVal, null);
+      if (mergedVal != null) {
+        newStore.thisValue = mergedVal;
+      }
+    }
+
+    for (Map.Entry<FieldAccess, V> e : other.fieldValues.entrySet()) {
+      // information about fields that are only part of one store, but not the other are
+      // discarded, as one store implicitly contains 'top' for that field.
+      FieldAccess el = e.getKey();
+      V thisVal = fieldValues.get(el);
+      if (thisVal != null) {
+        V otherVal = e.getValue();
+        V mergedVal = thisVal.mostSpecific(otherVal, null);
+        if (mergedVal != null) {
+          newStore.fieldValues.put(el, mergedVal);
+        }
+      }
+    }
+    for (Map.Entry<ArrayAccess, V> e : other.arrayValues.entrySet()) {
+      // information about arrays that are only part of one store, but not the other are
+      // discarded, as one store implicitly contains 'top' for that array access.
+      ArrayAccess el = e.getKey();
+      V thisVal = arrayValues.get(el);
+      if (thisVal != null) {
+        V otherVal = e.getValue();
+        V mergedVal = thisVal.mostSpecific(otherVal, null);
+        if (mergedVal != null) {
+          newStore.arrayValues.put(el, mergedVal);
+        }
+      }
+    }
+    for (Map.Entry<MethodCall, V> e : other.methodCallExpressions.entrySet()) {
+      // information about methods that are only part of one store, but not the other are
+      // discarded, as one store implicitly contains 'top' for that field.
+      MethodCall el = e.getKey();
+      V thisVal = methodCallExpressions.get(el);
+      if (thisVal != null) {
+        V otherVal = e.getValue();
+        V mergedVal = thisVal.mostSpecific(otherVal, null);
+        if (mergedVal != null) {
+          newStore.methodCallExpressions.put(el, mergedVal);
+        }
+      }
+    }
+    for (Map.Entry<ClassName, V> e : other.classValues.entrySet()) {
+      ClassName el = e.getKey();
+      V thisVal = classValues.get(el);
+      if (thisVal != null) {
+        V otherVal = e.getValue();
+        V mergedVal = thisVal.mostSpecific(otherVal, null);
+        if (mergedVal != null) {
+          newStore.classValues.put(el, mergedVal);
+        }
+      }
+    }
+    return newStore;
+  }
+
   private V upperBoundOfValues(V otherVal, V thisVal, boolean shouldWiden) {
     return shouldWiden ? thisVal.widenUpperBound(otherVal) : thisVal.leastUpperBound(otherVal);
   }

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

@@ -90,6 +90,7 @@
 import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.TreePathUtil;
 import org.checkerframework.javacutil.TreeUtils;
+import org.checkerframework.javacutil.TypesUtils;
 
 /**
  * The default analysis transfer function for the Checker Framework. It propagates information
@@ -768,6 +769,11 @@ public TransferResult<V, S> visitLocalVariable(LocalVariableNode n, TransferInpu
     V valueFromStore = store.getValue(n);
     V valueFromFactory = getValueFromFactory(n.getTree(), n);
     V value = moreSpecificValue(valueFromFactory, valueFromStore);
+    if (valueFromStore != null && valueFromStore.getThenStore() != null) {
+      S thenStore = in.getThenStore().merge(valueFromStore.getThenStore());
+      S elseStore = in.getElseStore().merge(valueFromStore.getElseStore());
+      return new ConditionalTransferResult<>(finishValue(value, store), thenStore, elseStore);
+    }
     return new RegularTransferResult<>(finishValue(value, store), store);
   }
 
@@ -980,6 +986,16 @@ public TransferResult<V, S> visitAssignment(AssignmentNode n, TransferInput<V, S
       }
     }
 
+    if (lhs instanceof LocalVariableNode
+        && TypesUtils.isBooleanType(lhs.getType())
+        && in.containsTwoStores()) {
+      if (ElementUtils.isEffectivelyFinal(TreeUtils.elementFromTree(lhs.getTree()))) {
+        S thenStore = in.getThenStore().copy();
+        S elseStore = in.getElseStore().copy();
+        rhsValue.addStores(thenStore, elseStore);
+      }
+    }
+
     if (n.isSynthetic() && in.containsTwoStores()) {
       // This is a synthetic assignment node created for a ternary expression. In this case
       // the `then` and `else` store are not merged.

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

@@ -11,6 +11,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.dataflow.analysis.AbstractValue;
 import org.checkerframework.dataflow.analysis.Analysis;
+import org.checkerframework.dataflow.analysis.Store;
 import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
@@ -277,7 +278,31 @@ public V mostSpecific(@Nullable V other, @Nullable V backup) {
     if (ms.error) {
       return backup;
     }
-    return analysis.createAbstractValue(mostSpecific, mostSpecifTypeMirror);
+    V mostSpecificVal = analysis.createAbstractValue(mostSpecific, mostSpecifTypeMirror);
+    if (this.getThenStore() != null) {
+      mostSpecificVal.addStores(thenStore, elseStore);
+    } else if (other.getThenStore() != null) {
+      mostSpecificVal.addStores(other.thenStore, other.elseStore);
+    }
+    return mostSpecificVal;
+  }
+
+  Store<?> thenStore;
+  Store<?> elseStore;
+
+  void addStores(Store<?> thenStore, Store<?> elseStore) {
+    this.thenStore = thenStore;
+    this.elseStore = elseStore;
+  }
+
+  @SuppressWarnings("unchecked")
+  public <S extends CFAbstractStore<V, S>> S getThenStore() {
+    return (S) thenStore;
+  }
+
+  @SuppressWarnings("unchecked")
+  public <S extends CFAbstractStore<V, S>> S getElseStore() {
+    return (S) elseStore;
   }
 
   /** Computes the most specific annotations. */
@@ -529,7 +554,13 @@ protected V upperBound(@Nullable V other, TypeMirror upperBoundTypeMirror, boole
             other.getUnderlyingType(),
             other.getAnnotations(),
             canBeMissingAnnotations(upperBoundTypeMirror));
-    return analysis.createAbstractValue(lub, upperBoundTypeMirror);
+    V upperBound = analysis.createAbstractValue(lub, upperBoundTypeMirror);
+    if (this.getThenStore() != null && other.getThenStore() != null) {
+      upperBound.addStores(
+          this.getThenStore().merge(other.getThenStore()),
+          this.getElseStore().merge(other.getElseStore()));
+    }
+    return upperBound;
   }
 
   /**