Add instanceof.unsafe lint option

checker/jtreg/lintoption/InstanceofLintOptionDisabled.java

@@ -0,0 +1,17 @@
+/*
+ * @test
+ * @summary Test case for instanceof lint option: -Alint=-instanceof
+ * @requires jdk.version >= 17
+ * @compile -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java -Alint=-instanceof
+ * @compile -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java -Alint=-instanceof:unsafe
+ * @compile -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java -Alint=instanceof,-instanceof:unsafe
+ */
+
+import org.checkerframework.checker.tainting.qual.Untainted;
+
+public class InstanceofLintOptionDisabled {
+    void bar(Object o) {
+        if (o instanceof @Untainted String s) {}
+        if (o instanceof @Untainted String) {}
+    }
+}

checker/jtreg/lintoption/InstanceofLintOptionEnabled.java

@@ -0,0 +1,18 @@
+/*
+ * @test
+ * Test case for instanceof lint option: -Alint=instanceof
+ * @requires jdk.version >= 17
+ * @compile/ref=InstanceofLintOptionEnabled.out -XDrawDiagnostics -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java
+ * @compile/ref=InstanceofLintOptionEnabled.out -XDrawDiagnostics -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java -Alint=instanceof
+ * @compile/ref=InstanceofLintOptionEnabled.out -XDrawDiagnostics -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java -Alint=instanceof:unsafe
+ * @compile/ref=InstanceofLintOptionEnabled.out -XDrawDiagnostics -processor org.checkerframework.checker.tainting.TaintingChecker InstanceofLintOptionEnabled.java -Alint=-instanceof,instanceof:unsafe
+ */
+
+import org.checkerframework.checker.tainting.qual.Untainted;
+
+public class InstanceofLintOptionEnabled {
+    void bar(Object o) {
+        if (o instanceof @Untainted String s) {}
+        if (o instanceof @Untainted String) {}
+    }
+}

checker/jtreg/lintoption/InstanceofLintOptionEnabled.out

@@ -0,0 +1,4 @@
+InstanceofLintOptionEnabled.java:15:15: compiler.warn.proc.messager: [instanceof.pattern.unsafe] instanceof pattern binding '@Tainted Object' to '@Untainted
+String s' cannot be statically verified.
+InstanceofLintOptionEnabled.java:16:15: compiler.warn.proc.messager: [instanceof.unsafe] '@Tainted Object' instanceof '@Untainted String' cannot be statically verified.
+2 warnings

docs/CHANGELOG.md

@@ -3,6 +3,9 @@ Version 3.49.3-eisop2 (June ??, 2025)
 
 **User-visible changes:**
 
+The `instanceof.unsafe` and `instanceof.pattern.unsafe` warnings in the Checker Framework are now controlled by lint options.
+They are enabled by default and can be disabled using `-Alint=-instanceof.unsafe` or `-Alint=-instanceof`.
+
 **Implementation details:**
 
 **Closed issues:**

docs/manual/warnings.tex

@@ -711,12 +711,11 @@
 
 \item
   \code{cast:unsafe} (default: on) warn about unsafe casts that are not
-  checked at run time, as in \code{((@NonNull String) myref)}.  Such casts
-  are generally not necessary because of type refinement
-  (Section~\ref{type-refinement}).
+  checked at run time, as in \code{((@NonNull String) myref)}.
+  Such casts are unsafe as the type qualifiers are ignored at run time.
 
 \item
-  \code{cast:redundant} (default: on) warn about redundant
+  \code{cast:redundant} (default: off) warn about redundant
   casts that are guaranteed to succeed at run time,
   as in \code{((@NonNull String) "m")}.  Such casts are not necessary,
   because the target expression of the cast already has the given type
@@ -725,6 +724,14 @@
 \item
   \code{cast} Enable or disable all cast-related warnings.
 
+\item
+  \code{instanceof:unsafe} (default: on) warn about unsafe instanceof tests
+  that are not checked at run time, as in \code{o instanceof @Untainted String}.
+  Such instanceof tests are unsafe as the type qualifiers are ignored at run time.
+
+\item
+  \code{instanceof} Enable or disable instanceof-related warnings.
+
 \item
 \begin{sloppypar}
   \code{all} Enable or disable all lint warnings, including

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

@@ -215,6 +215,8 @@ protected Set<String> createSupportedLintOptions() {
         lintSet.add("cast");
         lintSet.add("cast:redundant");
         lintSet.add("cast:unsafe");
+        lintSet.add("instanceof");
+        lintSet.add("instanceof:unsafe");
         return lintSet;
     }
 

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

@@ -289,6 +289,15 @@ public class BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
     /** True if "-AcheckEnclosingExpr" was passed on the command line. */
     private final boolean checkEnclosingExpr;
 
+    /** True if "-Alint=cast:redundant" was passed on the command line. */
+    private final boolean lintCastRedundantEnabled;
+
+    /** True unless "-Alint=-cast:unsafe" was passed on the command line. */
+    private final boolean lintCastUnsafeEnabled;
+
+    /** True unless "-Alint=-instanceof:unsafe" was passed on the command line. */
+    private final boolean lintInstanceofUnsafeEnabled;
+
     /** The tree of the enclosing method that is currently being visited, if any. */
     protected @Nullable MethodTree methodTree = null;
 
@@ -348,6 +357,9 @@ protected BaseTypeVisitor(BaseTypeChecker checker, @Nullable Factory typeFactory
                 checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure");
         assumePureGetters = checker.hasOption("assumePureGetters");
         checkCastElementType = checker.hasOption("checkCastElementType");
+        lintCastRedundantEnabled = checker.getLintOption("cast:redundant", false);
+        lintCastUnsafeEnabled = checker.getLintOption("cast:unsafe", true);
+        lintInstanceofUnsafeEnabled = checker.getLintOption("instanceof:unsafe", true);
     }
 
     /** An array containing just {@code BaseTypeChecker.class}. */
@@ -2713,9 +2725,11 @@ public Void visitNewArray(NewArrayTree tree, Void p) {
     /**
      * If the lint option "cast:redundant" is set, this method issues a warning if the cast is
      * redundant.
+     *
+     * @param typeCastTree the TypeCastTree to check
      */
     protected void checkTypecastRedundancy(TypeCastTree typeCastTree) {
-        if (!checker.getLintOption("cast:redundant", false)) {
+        if (!lintCastRedundantEnabled) {
             return;
         }
 
@@ -2729,13 +2743,13 @@ protected void checkTypecastRedundancy(TypeCastTree typeCastTree) {
 
     /**
      * Issues a warning if the given explicitly-written typecast is unsafe. Does nothing if the lint
-     * option "cast:unsafe" is not set. Only primary qualifiers are checked unless the command line
+     * option "-cast:unsafe" is set. Only primary qualifiers are checked unless the command line
      * option "checkCastElementType" is supplied.
      *
      * @param typeCastTree an explicitly-written typecast
      */
     protected void checkTypecastSafety(TypeCastTree typeCastTree) {
-        if (!checker.getLintOption("cast:unsafe", true)) {
+        if (!lintCastUnsafeEnabled) {
             return;
         }
         AnnotatedTypeMirror castType = atypeFactory.getAnnotatedType(typeCastTree);
@@ -2917,6 +2931,9 @@ public Void visitTypeCast(TypeCastTree tree, Void p) {
 
     @Override
     public Void visitInstanceOf(InstanceOfTree tree, Void p) {
+        if (!lintInstanceofUnsafeEnabled) {
+            return super.visitInstanceOf(tree, p);
+        }
         // The "reference type" is the type after "instanceof".
         Tree patternTree = InstanceOfUtils.getPattern(tree);
         if (patternTree != null) {

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -1890,7 +1890,7 @@ private String detailedMsgTextPositionString(
     //
 
     /**
-     * Determine which lint options are artive.
+     * Determine which lint options are active.
      *
      * @param options the command-line options
      * @return the active lint options