3.21.2 infers wrong type for locals assigned to by conditional expression

[amalloy]

After upgrading from 3.20.0 to 3.21.1, I discovered the following issue in some of our source files, which also reproduces in 3.21.2.

Command

./checker-framework-3.21.2/checker/bin/javac \
  -processor org.checkerframework.checker.nullness.NullnessChecker \
  T.java

Inputs

File: ./T.java:

import java.util.function.Function;
import org.checkerframework.checker.nullness.qual.Nullable;

class T {
  interface PromptViewModel {
    boolean isPending();
    @Nullable PromptButtonViewModel getConfirmationButton();
  }
  interface PromptButtonViewModel {
    @Nullable ConfirmationPopupViewModel getConfirmationPopup();
  }
  interface ConfirmationPopupViewModel {
    boolean isShowingConfirmation();
  }

  static final Function<PromptViewModel, Boolean> IS_PENDING_OR_SHOWING_CONFIRMATION =
      (viewModel) -> {
        PromptButtonViewModel prompt = viewModel.getConfirmationButton();
        ConfirmationPopupViewModel popup = prompt != null ? prompt.getConfirmationPopup() : null;
        return viewModel.isPending() || (popup != null && popup.isShowingConfirmation());
      };

  boolean f(PromptViewModel viewModel) {
    PromptButtonViewModel prompt = viewModel.getConfirmationButton();
    ConfirmationPopupViewModel popup = prompt != null ? prompt.getConfirmationPopup() : null;
    return viewModel.isPending() || (popup != null && popup.isShowingConfirmation());
  }
}

Output

T.java:19: error: [conditional] incompatible types in conditional expression.
        ConfirmationPopupViewModel popup = prompt != null ? prompt.getConfirmationPopup() : null;
                                                                                       ^
  found   : @Initialized @Nullable ConfirmationPopupViewModel
  required: @Initialized @NonNull ConfirmationPopupViewModel
T.java:19: error: [conditional] incompatible types in conditional expression.
        ConfirmationPopupViewModel popup = prompt != null ? prompt.getConfirmationPopup() : null;
                                                                                            ^
  found   : null (NullType)
  required: @Initialized @NonNull ConfirmationPopupViewModel
2 errors

Note that the errors are both in the definition of IS_PENDING_OR_SHOWING_CONFIRMATION; none of them are in the definition of f, which should have the same nullness implications.

Expectation

I expected no error. The checker framework should infer that, since popup may be assigned a null value, its type is @Nullable. This is fine, since it is checked before use. More generally, I would expect the same behavior for the method f as for the lambda with the same body.

We speculated that the checker might somehow be confused about lambdas, since the erroneous case occurs in a lambda. But wrapping the body of f with a lambda does not reproduce the issue. My current guess is that, because a field is initialized with a lambda, the checker is tricked into thinking that the lambda's local variables are actually fields, for which it does not wish to infer nullability. But I wasn't able to narrow the reproduction case down sufficiently to prove this.

[smillst]

Thanks for the report! I can reproduce this and it is a problem with lambda confusion. Below is discussion of the what more precisely is happening.

#5000 added a synthetic variable for conditional variables:

checker-framework/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

Lines 2436 to 2437 in ed70606

	VariableTree condExprVarTree =
	treeBuilder.buildVariableDecl(exprType, uniqueName("condExpr"), findOwner(), null);

The call to findOwner() in that code finds the class as the "owner" which causes the synthetic variable to be a field rather than a local variable. The default for fields is @NonNull, so that's why there's an error. (This is a problem with all synthetic variables not just ones created for conditional expressions.)

In a case with a conditional expression in a lambda in a field, the owner of any synthetic variables should be the static initializer if the field is static or the instance initializer if the field is an instance fields. I'm not sure how to get this element.

The following code in CFAbstractTransfer#initialStore may be of use.

    // Try to find an enclosing initializer block.
        // Would love to know if there was a better way.
        // Find any enclosing element of the lambda (using trees).
        // Then go up the elements to find an initializer element (which can't be found with the
        // tree).
        TreePath loopTree = factory.getPath(lambda.getLambdaTree()).getParentPath();
        Element anEnclosingElement = null;
        while (loopTree.getLeaf() != enclosingTree) {
          Element sym = TreeUtils.elementFromTree(loopTree.getLeaf());
          if (sym != null) {
            anEnclosingElement = sym;
            break;
          }
          loopTree = loopTree.getParentPath();
        }
        while (anEnclosingElement != null
            && !anEnclosingElement.equals(TreeUtils.elementFromTree(enclosingTree))) {
          if (anEnclosingElement.getKind() == ElementKind.INSTANCE_INIT
              || anEnclosingElement.getKind() == ElementKind.STATIC_INIT) {
            enclosingElement = anEnclosingElement;
            break;
          }
          anEnclosingElement = anEnclosingElement.getEnclosingElement();
        }
      }