Boolean variables in dataflow

checker/tests/nullness/Issue406.java

@@ -0,0 +1,58 @@
+import org.checkerframework.checker.nullness.qual.NonNull;
+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 testFails1b(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean eitherIsNull = x1 == null || x2 == null;
+    if (!eitherIsNull) {
+      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 testFails2b(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean firstIsNull = x1 == null;
+    boolean secondIsNull = x2 == null;
+    if (!firstIsNull) {
+      @NonNull LocalDate z = x1;
+    }
+
+    if (firstIsNull || secondIsNull) return;
+    delegate(x1, x2);
+  }
+
+  private void test3(@Nullable LocalDate x1, @Nullable LocalDate x2) {
+    boolean firstIsNull = x1 != null;
+    boolean secondIsNull = x2 != null;
+    if (!firstIsNull || !secondIsNull) {
+      // ::  error: (argument)
+      delegate(
+          x1,
+          // ::  error: (argument)
+          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;
+    }
+  }
+}

checker/tests/resourceleak/DaikonFail.java

@@ -0,0 +1,37 @@
+import java.io.File;
+import java.io.PrintStream;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class DaikonFail {
+
+  public static @Nullable File generate_goals = null;
+  public static File diff_file = new File("InvariantFormatTest.diffs");
+
+  private boolean execute() {
+
+    boolean result = performTest();
+
+    if (generate_goals != null) {
+      try {
+        PrintStream out_fp = new PrintStream(generate_goals);
+        out_fp.close();
+      } catch (Exception e) {
+        throw new RuntimeException();
+      }
+    } else {
+      if (!result) {
+        try {
+          PrintStream diff_fp = new PrintStream(diff_file);
+          diff_fp.close();
+        } catch (Exception e) {
+        }
+        return false;
+      }
+    }
+    return true;
+  }
+
+  private boolean performTest() {
+    return false;
+  }
+}

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

@@ -9,7 +9,9 @@
 import java.util.Objects;
 import java.util.StringJoiner;
 import java.util.concurrent.atomic.AtomicLong;
+import java.util.function.BiFunction;
 import java.util.function.BinaryOperator;
+import java.util.function.Consumer;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.Name;
@@ -71,6 +73,71 @@ public abstract class CFAbstractStore<V extends CFAbstractValue<V>, S extends CF
   /** Information collected about local variables (including method parameters). */
   protected final Map<LocalVariable, V> localVariableValues;
 
+  /** Stores after boolean variable assignment. */
+  protected final Map<LocalVariable, BooleanVarStore<V, S>> booleanVarStores;
+
+  /**
+   * An object that contains the then and else store after a boolean variable assignment.
+   *
+   * @param <V> value
+   * @param <S> store
+   */
+  protected static class BooleanVarStore<
+      V extends CFAbstractValue<V>, S extends CFAbstractStore<V, S>> {
+
+    /** Then store. */
+    S thenStore;
+
+    /** Else store. */
+    S elseStore;
+
+    /**
+     * Create a then else store with copies of the provided {@code thenStore} and {@code elseStore}.
+     *
+     * @param thenStore thenStore
+     * @param elseStore elseStore
+     */
+    BooleanVarStore(S thenStore, S elseStore) {
+      this.thenStore = thenStore.copy();
+      this.elseStore = elseStore.copy();
+      thenStore.booleanVarStores.clear();
+      elseStore.booleanVarStores.clear();
+    }
+
+    /**
+     * Copy this.
+     *
+     * @return a copy of this
+     */
+    public BooleanVarStore<V, S> copy() {
+      return new BooleanVarStore<>(thenStore, elseStore);
+    }
+
+    /**
+     * Applies {@code function} to both stores.
+     *
+     * @param function that takes a store and preforms some action
+     */
+    public void applyToStores(Consumer<CFAbstractStore<V, S>> function) {
+      function.accept(thenStore);
+      function.accept(elseStore);
+    }
+
+    /**
+     * Merges this then stores with {@code other}'s then store using {@code function} and merges
+     * this else store {@code other}'s else store using {@code function}. A new {@code
+     * BooleanVarStore} is returned with the result from both merges.
+     *
+     * @param function A function that takes two stores and returns a store.
+     * @param other another {@code BooleanVarStore}
+     * @return the merge of this and other
+     */
+    public BooleanVarStore<V, S> merge(BiFunction<S, S, S> function, BooleanVarStore<V, S> other) {
+      return new BooleanVarStore<>(
+          function.apply(thenStore, other.thenStore), function.apply(elseStore, other.elseStore));
+    }
+  }
+
   /** Information collected about the current object. */
   protected V thisValue;
 
@@ -140,17 +207,18 @@ public long getUid() {
    */
   protected CFAbstractStore(CFAbstractAnalysis<V, S, ?> analysis, boolean sequentialSemantics) {
     this.analysis = analysis;
-    localVariableValues = new HashMap<>();
-    thisValue = null;
-    fieldValues = new HashMap<>();
-    methodCallExpressions = new HashMap<>();
-    arrayValues = new HashMap<>();
-    classValues = new HashMap<>();
+    this.localVariableValues = new HashMap<>();
+    this.booleanVarStores = new HashMap<>();
+    this.thisValue = null;
+    this.fieldValues = new HashMap<>();
+    this.methodCallExpressions = new HashMap<>();
+    this.arrayValues = new HashMap<>();
+    this.classValues = new HashMap<>();
     this.sequentialSemantics = sequentialSemantics;
-    assumeSideEffectFree =
+    this.assumeSideEffectFree =
         analysis.checker.hasOption("assumeSideEffectFree")
             || analysis.checker.hasOption("assumePure");
-    assumePureGetters = analysis.checker.hasOption("assumePureGetters");
+    this.assumePureGetters = analysis.checker.hasOption("assumePureGetters");
   }
 
   /**
@@ -160,15 +228,17 @@ protected CFAbstractStore(CFAbstractAnalysis<V, S, ?> analysis, boolean sequenti
    */
   protected CFAbstractStore(CFAbstractStore<V, S> other) {
     this.analysis = other.analysis;
-    localVariableValues = new HashMap<>(other.localVariableValues);
-    thisValue = other.thisValue;
-    fieldValues = new HashMap<>(other.fieldValues);
-    methodCallExpressions = new HashMap<>(other.methodCallExpressions);
-    arrayValues = new HashMap<>(other.arrayValues);
-    classValues = new HashMap<>(other.classValues);
-    sequentialSemantics = other.sequentialSemantics;
-    assumeSideEffectFree = other.assumeSideEffectFree;
-    assumePureGetters = other.assumePureGetters;
+    this.localVariableValues = new HashMap<>(other.localVariableValues);
+    this.booleanVarStores = new HashMap<>(other.booleanVarStores.size());
+    other.booleanVarStores.forEach((var, store) -> this.booleanVarStores.put(var, store.copy()));
+    this.thisValue = other.thisValue;
+    this.fieldValues = new HashMap<>(other.fieldValues);
+    this.methodCallExpressions = new HashMap<>(other.methodCallExpressions);
+    this.arrayValues = new HashMap<>(other.arrayValues);
+    this.classValues = new HashMap<>(other.classValues);
+    this.sequentialSemantics = other.sequentialSemantics;
+    this.assumeSideEffectFree = other.assumeSideEffectFree;
+    this.assumePureGetters = other.assumePureGetters;
   }
 
   /**
@@ -257,6 +327,7 @@ public void updateForMethodCall(
       // isUnmodifiableByOtherCode.  Example: @KeyFor("valueThatCanBeMutated").
       if (sideEffectsUnrefineAliases) {
         localVariableValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
+        booleanVarStores.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
       }
 
       // update this value
@@ -621,6 +692,10 @@ protected void computeNewValueAndInsert(
     if (!shouldInsert(expr, value, permitNondeterministic)) {
       return;
     }
+    for (BooleanVarStore<V, S> booleanVarStore : booleanVarStores.values()) {
+      booleanVarStore.applyToStores(
+          s -> s.computeNewValueAndInsert(expr, value, merger, permitNondeterministic));
+    }
 
     if (expr instanceof LocalVariable) {
       LocalVariable localVar = (LocalVariable) expr;
@@ -760,6 +835,7 @@ public void clearValue(JavaExpression expr) {
     if (expr instanceof LocalVariable) {
       LocalVariable localVar = (LocalVariable) expr;
       localVariableValues.remove(localVar);
+      booleanVarStores.remove(localVar);
     } else if (expr instanceof FieldAccess) {
       FieldAccess fieldAcc = (FieldAccess) expr;
       fieldValues.remove(fieldAcc);
@@ -883,10 +959,20 @@ public void updateForAssignment(Node n, @Nullable V val) {
     JavaExpression je = JavaExpression.fromNode(n);
     if (je instanceof ArrayAccess) {
       updateForArrayAssignment((ArrayAccess) je, val);
+      booleanVarStores.forEach(
+          (var, store) ->
+              store.applyToStores(s -> s.updateForArrayAssignment((ArrayAccess) je, val)));
     } else if (je instanceof FieldAccess) {
       updateForFieldAccessAssignment((FieldAccess) je, val);
+      booleanVarStores.forEach(
+          (var, store) ->
+              store.applyToStores(s -> s.updateForFieldAccessAssignment((FieldAccess) je, val)));
     } else if (je instanceof LocalVariable) {
       updateForLocalVariableAssignment((LocalVariable) je, val);
+      booleanVarStores.forEach(
+          (var, store) ->
+              store.applyToStores(
+                  s -> s.updateForLocalVariableAssignment((LocalVariable) je, val)));
     } else {
       throw new BugInCF("Unexpected je of class " + je.getClass());
     }
@@ -1132,6 +1218,20 @@ public boolean canAlias(JavaExpression a, JavaExpression b) {
     return localVariableValues.get(new LocalVariable(el));
   }
 
+  protected void insertBooleanVarStore(LocalVariable lhsExpr, BooleanVarStore<V, S> other) {
+    booleanVarStores.put(lhsExpr, other);
+  }
+
+  protected void swapBooleanVarStore() {
+    Map<LocalVariable, BooleanVarStore<V, S>> newBooleanVarStores =
+        new HashMap<>(booleanVarStores.size());
+    booleanVarStores.forEach(
+        (var, store) ->
+            newBooleanVarStores.put(var, new BooleanVarStore<>(store.elseStore, store.thenStore)));
+    booleanVarStores.clear();
+    booleanVarStores.putAll(newBooleanVarStores);
+  }
+
   /* --------------------------------------------------------- */
   /* Handling of the current object */
   /* --------------------------------------------------------- */
@@ -1186,6 +1286,24 @@ private S upperBound(S other, boolean shouldWiden) {
       }
     }
 
+    for (Map.Entry<LocalVariable, BooleanVarStore<V, S>> e : other.booleanVarStores.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();
+      BooleanVarStore<V, S> store = booleanVarStores.get(localVar);
+      if (store != null) {
+        BooleanVarStore<V, S> otherStore = e.getValue();
+        BooleanVarStore<V, S> mergedStore =
+            shouldWiden
+                ? store.merge(CFAbstractStore::widenedUpperBound, otherStore)
+                : store.merge(CFAbstractStore::leastUpperBound, otherStore);
+
+        if (mergedStore != null) {
+          newStore.booleanVarStores.put(localVar, mergedStore);
+        }
+      }
+    }
+
     // information about the current object
     {
       V otherVal = other.thisValue;
@@ -1253,6 +1371,35 @@ private V upperBoundOfValues(V otherVal, V thisVal, boolean shouldWiden) {
     return shouldWiden ? thisVal.widenUpperBound(otherVal) : thisVal.leastUpperBound(otherVal);
   }
 
+  /**
+   * Creates a new store the has all the values from both {@code this} and {@code other}. If a node
+   * have a value in both stores, then the most specific one is used.
+   *
+   * @param other another store
+   * @return a new store with values from {@code this} and {@code other}
+   */
+  public S mostSpecific(S other) {
+    S newStore = this.copy();
+    other.booleanVarStores.forEach(newStore::insertBooleanVarStore);
+    //    booleanVarStores.computeIfPresent(lhsExpr, (key, booleanVarStore) ->
+    // booleanVarStore.merge(
+    //        CFAbstractStore::mostSpecific, other));
+    other.localVariableValues.forEach(newStore::insertValue);
+    if (other.thisValue != null) {
+      if (newStore.thisValue == null) {
+        newStore.thisValue = other.thisValue;
+      } else {
+        newStore.thisValue = thisValue.mostSpecific(other.thisValue, null);
+      }
+    }
+    other.fieldValues.forEach(newStore::insertValue);
+    other.arrayValues.forEach(newStore::insertValue);
+    other.methodCallExpressions.forEach(newStore::insertValue);
+    other.classValues.forEach(newStore::insertValue);
+
+    return newStore;
+  }
+
   /**
    * Returns true iff this {@link CFAbstractStore} contains a superset of the map entries of the
    * argument {@link CFAbstractStore}. Note that we test the entry keys and values by Java equality,