diff --git a/checker/jtreg/lintoption/InstanceofLintOptionDisabled.java b/checker/jtreg/lintoption/InstanceofLintOptionDisabled.java new file mode 100644 index 000000000000..424f98c79b68 --- /dev/null +++ b/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) {} + } +} diff --git a/checker/jtreg/lintoption/InstanceofLintOptionEnabled.java b/checker/jtreg/lintoption/InstanceofLintOptionEnabled.java new file mode 100644 index 000000000000..5db7250ef722 --- /dev/null +++ b/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) {} + } +} diff --git a/checker/jtreg/lintoption/InstanceofLintOptionEnabled.out b/checker/jtreg/lintoption/InstanceofLintOptionEnabled.out new file mode 100644 index 000000000000..022fdc865176 --- /dev/null +++ b/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 diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 87830d6979aa..90f82b197e4a 100644 --- a/docs/CHANGELOG.md +++ b/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:** diff --git a/docs/manual/warnings.tex b/docs/manual/warnings.tex index e258a39f1c9b..bf4a2e6afb53 100644 --- a/docs/manual/warnings.tex +++ b/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 diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 414fd4d0e176..0bb07e6db3f8 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -215,6 +215,8 @@ protected Set createSupportedLintOptions() { lintSet.add("cast"); lintSet.add("cast:redundant"); lintSet.add("cast:unsafe"); + lintSet.add("instanceof"); + lintSet.add("instanceof:unsafe"); return lintSet; } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 5e2c0b1acf57..582ceed3e4d7 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -289,6 +289,15 @@ public class BaseTypeVisitor