Type check and refine binding patterns.

checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java

@@ -399,22 +399,22 @@ public Void visitIf(IfTree node, Void p) {
   }
 
   @Override
-  public Void visitInstanceOf(InstanceOfTree node, Void p) {
+  public Void visitInstanceOf(InstanceOfTree tree, Void p) {
     // The "reference type" is the type after "instanceof".
-    Tree refTypeTree = node.getType();
+    Tree refTypeTree = tree.getType();
     if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) {
       List<? extends AnnotationMirror> annotations =
           TreeUtils.annotationsFromTree((AnnotatedTypeTree) refTypeTree);
       if (AnnotationUtils.containsSame(annotations, NULLABLE)) {
-        checker.reportError(node, "instanceof.nullable");
+        checker.reportError(tree, "instanceof.nullable");
       }
       if (AnnotationUtils.containsSame(annotations, NONNULL)) {
-        checker.reportWarning(node, "instanceof.nonnull.redundant");
+        checker.reportWarning(tree, "instanceof.nonnull.redundant");
         // Don't call super because it will issue an incorrect instanceof.unsafe warning.
         return null;
       }
     }
-    return super.visitInstanceOf(node, p);
+    return super.visitInstanceOf(tree, p);
   }
 
   /**

checker/tests/tainting/java17/TaintingBindingVariable.java

@@ -0,0 +1,25 @@
+// @below-java17-jdk-skip-test
+import org.checkerframework.checker.tainting.qual.Untainted;
+
+public class TaintingBindingVariable {
+
+  void bar(@Untainted Object o) {
+    if (o instanceof @Untainted String s) {
+      @Untainted String f = s;
+    }
+    if (o instanceof String s) {
+      @Untainted String f2 = s;
+    }
+  }
+
+  void bar2(Object o) {
+    // :: warning: (instanceof.pattern.unsafe)
+    if (o instanceof @Untainted String s) {
+      @Untainted String f = s;
+    }
+    if (o instanceof String s) {
+      // :: error: (assignment)
+      @Untainted String f2 = s;
+    }
+  }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

@@ -506,8 +506,8 @@ public Node scan(Tree tree, Void p) {
       // Must use String comparison to support compiling on JDK 11 and earlier.
       //     Features added between JDK 12 and JDK 17 inclusive.
       switch (tree.getKind().name()) {
-          // case "BINDING_PATTERN":
-          //  return visitBindingPattern17(path.getLeaf(), p);
+        case "BINDING_PATTERN":
+          return visitBindingPattern17(path.getLeaf(), p);
         case "SWITCH_EXPRESSION":
           return visitSwitchExpression17(tree, p);
         case "YIELD":
@@ -545,6 +545,23 @@ public Node visitSwitchExpression17(Tree switchExpressionTree, Void p) {
     return switchBuilder.build();
   }
 
+  /**
+   * Visit a BindingPatternTree
+   *
+   * @param bindingPatternTree a BindingPatternTree, typed as Tree to be backward-compatible
+   * @param p parameter
+   * @return the result of visiting the binding pattern tree
+   */
+  public Node visitBindingPattern17(Tree bindingPatternTree, Void p) {
+    ClassTree enclosingClass = TreePathUtil.enclosingClass(getCurrentPath());
+    TypeElement classElem = TreeUtils.elementFromDeclaration(enclosingClass);
+    Node receiver = new ImplicitThisNode(classElem.asType());
+    VariableTree varTree = TreeUtils.bindingPatternTreeGetVariable(bindingPatternTree);
+    LocalVariableNode varNode = new LocalVariableNode(varTree, receiver);
+    extendWithNode(varNode);
+    return varNode;
+  }
+
   /* --------------------------------------------------------- */
   /* Nodes and Labels Management */
   /* --------------------------------------------------------- */
@@ -3629,7 +3646,11 @@ public Node visitTypeParameter(TypeParameterTree tree, Void p) {
   public Node visitInstanceOf(InstanceOfTree tree, Void p) {
     Node operand = scan(tree.getExpression(), p);
     TypeMirror refType = TreeUtils.typeOf(tree.getType());
-    InstanceOfNode node = new InstanceOfNode(tree, operand, refType, types);
+    Tree binding = TreeUtils.instanceOfGetPattern(tree);
+    LocalVariableNode bindingNode =
+        (LocalVariableNode) ((binding == null) ? null : scan(binding, p));
+
+    InstanceOfNode node = new InstanceOfNode(tree, operand, bindingNode, refType, types);
     extendWithNode(node);
     return node;
   }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/InstanceOfNode.java

@@ -27,24 +27,66 @@ public class InstanceOfNode extends Node {
   /** The tree associated with this node. */
   protected final InstanceOfTree tree;
 
+  /** The node of the binding variable if one exists. */
+  protected final @Nullable LocalVariableNode bindingVariable;
+
   /** For Types.isSameType. */
   protected final Types types;
 
-  /** Create an InstanceOfNode. */
+  /**
+   * Create an InstanceOfNode.
+   *
+   * @param tree instanceof tree
+   * @param operand the expression in the instanceof tree
+   * @param refType the type in the instanceof
+   * @param types types util
+   */
   public InstanceOfNode(Tree tree, Node operand, TypeMirror refType, Types types) {
+    this(tree, operand, null, refType, types);
+  }
+
+  /**
+   * Create an InstanceOfNode.
+   *
+   * @param tree instanceof tree
+   * @param operand the expression in the instanceof tree
+   * @param bindingVariable the binding variable or null if there is none
+   * @param refType the type in the instanceof
+   * @param types types util
+   */
+  public InstanceOfNode(
+      Tree tree,
+      Node operand,
+      @Nullable LocalVariableNode bindingVariable,
+      TypeMirror refType,
+      Types types) {
     super(types.getPrimitiveType(TypeKind.BOOLEAN));
     assert tree.getKind() == Tree.Kind.INSTANCE_OF;
     this.tree = (InstanceOfTree) tree;
     this.operand = operand;
     this.refType = refType;
     this.types = types;
+    this.bindingVariable = bindingVariable;
   }
 
   public Node getOperand() {
     return operand;
   }
 
-  /** The reference type being tested against. */
+  /**
+   * Returns the binding variable for this instanceof, or null if one does not exist.
+   *
+   * @return the binding variable for this instanceof, or null if one does not exist
+   */
+  public @Nullable LocalVariableNode getBindingVariable() {
+    return bindingVariable;
+  }
+
+  /**
+   * The reference type being tested against.
+   *
+   * @return the reference type
+   */
   public TypeMirror getRefType() {
     return refType;
   }
@@ -61,7 +103,12 @@ public <R, P> R accept(NodeVisitor<R, P> visitor, P p) {
 
   @Override
   public String toString() {
-    return "(" + getOperand() + " instanceof " + TypesUtils.simpleTypeName(getRefType()) + ")";
+    return "("
+        + getOperand()
+        + " instanceof "
+        + TypesUtils.simpleTypeName(getRefType())
+        + (bindingVariable == null ? "" : " " + getBindingVariable())
+        + ")";
   }
 
   @Override

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -2383,19 +2383,33 @@ public Void visitTypeCast(TypeCastTree node, Void p) {
   }
 
   @Override
-  public Void visitInstanceOf(InstanceOfTree node, Void p) {
+  public Void visitInstanceOf(InstanceOfTree tree, Void p) {
     // The "reference type" is the type after "instanceof".
-    Tree refTypeTree = node.getType();
-    validateTypeOf(refTypeTree);
-    if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) {
-      AnnotatedTypeMirror refType = atypeFactory.getAnnotatedType(refTypeTree);
-      AnnotatedTypeMirror expType = atypeFactory.getAnnotatedType(node.getExpression());
-      if (atypeFactory.getTypeHierarchy().isSubtype(refType, expType)
-          && !refType.getAnnotations().equals(expType.getAnnotations())) {
-        checker.reportWarning(node, "instanceof.unsafe", expType, refType);
+    Tree patternTree = TreeUtils.instanceOfGetPattern(tree);
+    if (patternTree != null) {
+      VariableTree variableTree = TreeUtils.bindingPatternTreeGetVariable(patternTree);
+      validateTypeOf(variableTree);
+      if (variableTree.getModifiers() != null) {
+        AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedType(variableTree);
+        AnnotatedTypeMirror expType = atypeFactory.getAnnotatedType(tree.getExpression());
+        if (!atypeFactory.getTypeHierarchy().isSubtype(expType, variableType)) {
+          checker.reportWarning(tree, "instanceof.pattern.unsafe", expType, variableTree);
+        }
+      }
+    } else {
+      Tree refTypeTree = tree.getType();
+      validateTypeOf(refTypeTree);
+      if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) {
+        AnnotatedTypeMirror refType = atypeFactory.getAnnotatedType(refTypeTree);
+        AnnotatedTypeMirror expType = atypeFactory.getAnnotatedType(tree.getExpression());
+        if (atypeFactory.getTypeHierarchy().isSubtype(refType, expType)
+            && !refType.getAnnotations().equals(expType.getAnnotations())) {
+          checker.reportWarning(tree, "instanceof.unsafe", expType, refType);
+        }
       }
     }
-    return super.visitInstanceOf(node, p);
+
+    return super.visitInstanceOf(tree, p);
   }
 
   /**

framework/src/main/java/org/checkerframework/common/basetype/messages.properties

@@ -115,5 +115,6 @@ field.invariant.not.subtype.superclass=the qualifier for field %s is not a subty
 
 invalid.annotation.location.bytecode=found annotation in unexpected location in bytecode on element: %s %nUse -AignoreInvalidAnnotationLocations to suppress this warning
 instanceof.unsafe='%s' instanceof '%s' cannot be statically verified.
+instanceof.pattern.unsafe= instanceof pattern binding "%s" to "%s" cannot be statically verified.
 
 anno.on.irrelevant=Annotation %s is not applicable to %s

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

@@ -969,6 +969,15 @@ public TransferResult<V, S> visitInstanceOf(InstanceOfNode node, TransferInput<V
         return new RegularTransferResult<>(result.getResultValue(), in.getRegularStore());
       }
     }
+    // TODO: Should this be an else if?
+    if (node.getBindingVariable() != null) {
+      JavaExpression expr = JavaExpression.fromNode(node.getBindingVariable());
+      AnnotatedTypeMirror expType =
+          analysis.atypeFactory.getAnnotatedType(node.getTree().getExpression());
+      for (AnnotationMirror anno : expType.getAnnotations()) {
+        in.getRegularStore().insertOrRefine(expr, anno);
+      }
+    }
     return result;
   }