Boolean variables in dataflow

azure-pipelines.yml

@@ -23,7 +23,7 @@ jobs:
   dependsOn:
    - junit_jdk21
    - nonjunit_jdk21
-   - inference_part1_jdk21
+   #- inference_part1_jdk21
    - inference_part2_jdk21
    - typecheck_part1_jdk21
    - typecheck_part2_jdk21

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

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

@@ -249,39 +249,73 @@ 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());
-      }
-
-      // update this value
-      if (sideEffectsUnrefineAliases) {
-        thisValue = null;
-      }
+    // store information about method call if possible
+    JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode);
+    replaceValue(methodCall, val);
+  }
 
-      // update field values
-      if (sideEffectsUnrefineAliases) {
-        fieldValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
-      } else {
-        // Case 2 (unassignable fields) and case 3 (monotonic fields)
-        updateFieldValuesForMethodCall(gatypeFactory);
-      }
+  /**
+   * Remove any information that might not be valid any more after a method call, and add
+   * information guaranteed by the method.
+   *
+   * <ol>
+   *   <li>If the method is side-effect-free (as indicated by {@link
+   *       org.checkerframework.dataflow.qual.SideEffectFree} or {@link
+   *       org.checkerframework.dataflow.qual.Pure}), then no information needs to be removed.
+   *   <li>Otherwise, all information about field accesses {@code a.f} needs to be removed, except
+   *       if the method {@code n} cannot modify {@code a.f}. This unmodifiability property holds if
+   *       {@code a} is a local variable or {@code this}, and {@code f} is final, or if {@code a.f}
+   *       has a {@link MonotonicQualifier} in the current store. Subclasses can change this
+   *       behavior by overriding {@link #newFieldValueAfterMethodCall(FieldAccess,
+   *       GenericAnnotatedTypeFactory, CFAbstractValue)}.
+   *   <li>Furthermore, if the field has a monotonic annotation, then its information can also be
+   *       kept.
+   * </ol>
+   *
+   * Furthermore, if the method is deterministic, we store its result {@code val} in the store.
+   *
+   * @param gatypeFactory the type factory of the associated checker
+   */
+  protected void updateForSideEffect(GenericAnnotatedTypeFactory<?, ?, ?, ?> 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());
+    }
 
-      // 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 +334,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 +358,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 +403,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();
@@ -487,7 +521,17 @@ protected void insertOrRefine(
       return;
     }
     computeNewValueAndInsert(
-        expr, newValue, CFAbstractValue<V>::greatestLowerBound, permitNondeterministic);
+        expr,
+        newValue,
+        (v1, v2) -> {
+          if (v1 == null) {
+            return v2;
+          } else if (v2 == null) {
+            return v1;
+          }
+          return v1.greatestLowerBound(v2);
+        },
+        permitNondeterministic);
   }
 
   /** Returns true if {@code expr} can be stored in this store. */
@@ -622,6 +666,29 @@ protected void computeNewValueAndInsert(
       return;
     }
 
+    localVariableValues
+        .values()
+        .forEach(
+            v -> {
+              if (v != null && v.getThenStore() != null) {
+                v.getThenStore().computeNewValueAndInsertImpl(expr, value, merger);
+                v.getElseStore().computeNewValueAndInsertImpl(expr, value, merger);
+              }
+            });
+
+    computeNewValueAndInsertImpl(expr, value, merger);
+  }
+
+  /**
+   * Inserts the result of applying {@code merger} to {@code value} and the previous value for
+   * {@code expr}.
+   *
+   * @param expr the JavaExpression
+   * @param value the value of the JavaExpression
+   * @param merger the function used to merge {@code value} and the previous value of {@code expr}
+   */
+  /*package-private*/ void computeNewValueAndInsertImpl(
+      JavaExpression expr, @Nullable V value, BinaryOperator<V> merger) {
     if (expr instanceof LocalVariable) {
       LocalVariable localVar = (LocalVariable) expr;
       V oldValue = localVariableValues.get(localVar);
@@ -883,10 +950,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());
     }
@@ -1253,6 +1347,32 @@ private V upperBoundOfValues(V otherVal, V thisVal, boolean shouldWiden) {
     return shouldWiden ? thisVal.widenUpperBound(otherVal) : thisVal.leastUpperBound(otherVal);
   }
 
+  /**
+   * Creates a new store that has all the values from both {@code this} and {@code other}. If a node
+   * has 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 merge(S other) {
+    S newStore = this.copy();
+
+    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,