diff --git a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java index 60fc1572c4c0..7bb11ef77194 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanVisitor.java @@ -113,7 +113,8 @@ protected void commonAssignmentCheck( } @Override - protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected CastSafeKind isTypeCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirror exprLTAnno = exprType.getEffectiveAnnotationInHierarchy(atypeFactory.LESS_THAN_UNKNOWN); diff --git a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java index 50474671a32a..de05e2260472 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java @@ -977,9 +977,10 @@ DeclaredType typeToCheck() { } @Override - protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected CastSafeKind isTypeCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (castType.getKind().isPrimitive()) { - return true; + return CastSafeKind.SAFE; } return super.isTypeCastSafe(castType, exprType); } diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java index c35de186ba57..22d18b6d7075 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -366,9 +366,10 @@ private boolean noMustCallObligation(AnnotatedTypeMirror atm) { } @Override - protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected CastSafeKind isTypeCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (noMustCallObligation(castType) || noMustCallObligation(exprType)) { - return true; + return CastSafeKind.SAFE; } return super.isTypeCastSafe(castType, exprType); diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java index 4cc3ac4a9653..411428ad3ec7 100644 --- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java @@ -384,10 +384,11 @@ public Void visitCompoundAssignment(CompoundAssignmentTree node, Void p) { } @Override - protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected CastSafeKind isTypeCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (!atypeFactory.maybeIntegral(castType)) { // If the cast is not a number or a char, then it is legal. - return true; + return CastSafeKind.SAFE; } return super.isTypeCastSafe(castType, exprType); } diff --git a/checker/tests/lock/ChapterExamples.java b/checker/tests/lock/ChapterExamples.java index f2c76716ed4e..c571c36b5328 100644 --- a/checker/tests/lock/ChapterExamples.java +++ b/checker/tests/lock/ChapterExamples.java @@ -318,7 +318,7 @@ void someMethod() { o2 = o1; // {"lock"} and {} are not identical sets. } - @SuppressWarnings("lock:cast.unsafe") + @SuppressWarnings("lock:cast.incompatible") void someMethod2() { // A cast can be used if the user knows it is safe to do so. // However, the @SuppressWarnings must be added. @@ -564,7 +564,7 @@ public boolean compare(T[] a1, T[] a2) { private static final Object NULL_KEY = new Object(); // A guardsatisfied.location.disallowed error is issued for the cast. - @SuppressWarnings({"cast.unsafe", "guardsatisfied.location.disallowed"}) + @SuppressWarnings({"cast.incompatible", "guardsatisfied.location.disallowed"}) private static @GuardSatisfied(1) Object maskNull(@GuardSatisfied(1) Object key) { return (key == null ? (@GuardSatisfied(1) Object) NULL_KEY : key); } diff --git a/checker/tests/lock/Strings.java b/checker/tests/lock/Strings.java index c29200e1d47f..d788ebef87a1 100644 --- a/checker/tests/lock/Strings.java +++ b/checker/tests/lock/Strings.java @@ -13,7 +13,9 @@ void StringIsGBnothing( @GuardSatisfied Object o3, @GuardedByBottom Object o4) { String s1 = (String) o1; + // :: error: (cast.incompatible) String s2 = (String) o2; + // :: error: (cast.incompatible) String s3 = (String) o3; String s4 = (String) o4; // OK } diff --git a/checker/tests/signedness/CharCast.java b/checker/tests/signedness/CharCast.java index 788eb5b19ced..324a385f0fe3 100644 --- a/checker/tests/signedness/CharCast.java +++ b/checker/tests/signedness/CharCast.java @@ -8,13 +8,13 @@ void m(@SignedPositive int i) { void m1(short s) { int x = s; - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) char c = (char) x; } void m2(int i) { int x = (short) i; - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) char c = (char) x; } diff --git a/checker/tests/signedness/CharToFloat.java b/checker/tests/signedness/CharToFloat.java index 1caaea9f8f0f..44874da7161b 100644 --- a/checker/tests/signedness/CharToFloat.java +++ b/checker/tests/signedness/CharToFloat.java @@ -2,7 +2,9 @@ public class CharToFloat { void castCharacter(Object o) { + // :: error: (cast.incompatible) floatParameter((Character) o); + // :: error: (cast.incompatible) doubleParameter((Character) o); } diff --git a/checker/tests/signedness/PrimitiveCasts.java b/checker/tests/signedness/PrimitiveCasts.java index 132d430d023c..62ef25e3076d 100644 --- a/checker/tests/signedness/PrimitiveCasts.java +++ b/checker/tests/signedness/PrimitiveCasts.java @@ -3,7 +3,7 @@ public class PrimitiveCasts { void shortToChar1(short s) { - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) char c = (char) s; } diff --git a/checker/tests/signedness/WideningConversion.java b/checker/tests/signedness/WideningConversion.java index 68d2ae776ab5..f294b6da05cf 100644 --- a/checker/tests/signedness/WideningConversion.java +++ b/checker/tests/signedness/WideningConversion.java @@ -74,19 +74,19 @@ void plus() { char c; c = (char) (c1 + c2); - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) c = (char) (c1 + i2); - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) c = (char) (i1 + c2); - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) c = (char) (i1 + i2); c = (char) (c1 + c2); - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) c = (char) (c1 + si2); - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) c = (char) (si1 + c2); - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) c = (char) (si1 + si2); c = (char) (c1 + c2); 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 48e0ae1f28e2..3623ee0473a9 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -142,6 +142,7 @@ import javax.lang.model.type.DeclaredType; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; +import javax.lang.model.type.TypeVariable; import javax.lang.model.util.ElementFilter; import javax.tools.Diagnostic.Kind; @@ -2361,41 +2362,52 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } // We cannot do a simple test of casting, as isSubtypeOf requires // the input types to be subtypes according to Java. - if (!calledOnce && !isTypeCastSafe(castType, exprType)) { - checker.reportWarning( - typeCastTree, "cast.unsafe", exprType.toString(true), castType.toString(true)); + if (!calledOnce) { + CastSafeKind castResult = isTypeCastSafe(castType, exprType); + + if (castResult == CastSafeKind.WARNING) { + checker.reportWarning( + typeCastTree, + "cast.unsafe", + exprType.toString(true), + castType.toString(true)); + } else if (castResult == CastSafeKind.ERROR) { + checker.reportError( + typeCastTree, + "cast.incompatible", + exprType.toString(true), + castType.toString(true)); + } } } + /** CastSafeKind */ + protected enum CastSafeKind { + /** The cast is safe */ + SAFE, + /** The cast is illegal */ + ERROR, + /** Cannot statically verify the cast, report a warning */ + WARNING, + /** It's not an upcast */ + NOT_UPCAST, + /** It's not a downcast */ + NOT_DOWNCAST + } + /** - * Returns true if the cast is safe. - * - *
Only primary qualifiers are checked unless the command line option "checkCastElementType"
- * is supplied.
+ * Return true if it's an upcast (from the view of the qualifiers) and it's safe.
*
- * @param castType annotated type of the cast
- * @param exprType annotated type of the casted expression
- * @return true if the type cast is safe, false otherwise
+ * @param castType castType
+ * @param exprType exprType
+ * @return Can return NOT_UPCAST, WARNING or SAFE CastSafeKind.
*/
- protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) {
-
- final TypeKind castTypeKind = castType.getKind();
- if (castTypeKind == TypeKind.DECLARED) {
- // Don't issue an error if the annotations are equivalent to the qualifier upper bound
- // of the type.
- AnnotatedDeclaredType castDeclared = (AnnotatedDeclaredType) castType;
- Set Only primary qualifiers are checked unless the command line option "checkCastElementType"
+ * is supplied.
+ *
+ * @param castType annotated type of the cast
+ * @param exprType annotated type of the casted expression
+ * @return CastSafeKind if the type cast is safe, false otherwise
+ */
+ protected CastSafeKind isTypeCastSafe(
+ AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) {
+ CastSafeKind castResult = isUpcast(castType, exprType);
+
+ if (castResult
+ == CastSafeKind.NOT_UPCAST) { // not upcast, do downcast and incomparable cast check
+ castResult = isSafeDowncast(castType, exprType);
+
+ if (castResult == CastSafeKind.NOT_DOWNCAST) { // fall to incomparable cast
+ return isSafeIncomparableCast(castType, exprType);
+ } else {
+ return castResult;
+ }
+
+ } else {
+ return castResult;
+ }
}
/**
@@ -2471,7 +2596,7 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr
*/
private boolean isInvariantTypeCastSafe(
AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, AnnotationMirror top) {
- if (!isTypeCastSafe(castType, exprType)) {
+ if (isTypeCastSafe(castType, exprType) != CastSafeKind.SAFE) {
return false;
}
AnnotationMirror castTypeAnno = castType.getEffectiveAnnotationInHierarchy(top);
@@ -2523,7 +2648,7 @@ public Void visitInstanceOf(InstanceOfTree tree, Void p) {
if (variableTree.getModifiers() != null) {
AnnotatedTypeMirror variableType = atypeFactory.getAnnotatedType(variableTree);
AnnotatedTypeMirror expType = atypeFactory.getAnnotatedType(tree.getExpression());
- if (!isTypeCastSafe(variableType, expType)) {
+ if (isTypeCastSafe(variableType, expType) != CastSafeKind.SAFE) {
checker.reportWarning(tree, "instanceof.pattern.unsafe", expType, variableTree);
}
}
diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties
index 89a38bd67357..0160bb082a2d 100644
--- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties
+++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties
@@ -26,6 +26,7 @@ type.invalid.too.few.annotations=invalid type: missing annotations %s in type "%
type.invalid.annotations.on.use=invalid type: annotations %s conflict with declaration of type %s
type.invalid.super.wildcard=bounds must have the same annotations.%nsuper bound : %s%nextends bound: %s
cast.unsafe=cast from "%s" to "%s" cannot be statically verified
+cast.incompatible=incompatible typecast from "%s" to "%s"
invariant.cast.unsafe=cannot cast from "%s" to "%s"
cast.unsafe.constructor.invocation=constructor invocation cast from "%s" to "%s" cannot be statically verified
exception.parameter.invalid=invalid type in catch argument.%nfound : %s%nrequired: %s
diff --git a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java
index e379dd4d974c..db4bc6a4c09d 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java
@@ -149,6 +149,33 @@ default boolean isSubtype(
return true;
}
+ /**
+ * Tests whether all qualifiers in {@code qualifiers1} are comparable with the qualifier in the
+ * same hierarchy in {@code qualifiers2}.
+ *
+ * @param qualifiers1 set of qualifiers; exactly one per hierarchy
+ * @param qualifiers2 set of qualifiers; exactly one per hierarchy
+ * @return true iff all qualifiers in {@code qualifiers1} are comparable with qualifiers in
+ * {@code qualifiers2}
+ */
+ default boolean isComparable(
+ Collection extends AnnotationMirror> qualifiers1,
+ Collection extends AnnotationMirror> qualifiers2) {
+ assertSameSize(qualifiers1, qualifiers2);
+ for (AnnotationMirror subQual : qualifiers1) {
+ AnnotationMirror superQual = findAnnotationInSameHierarchy(qualifiers2, subQual);
+ if (superQual == null) {
+ throw new BugInCF(
+ "QualifierHierarchy: missing annotation in hierarchy %s. found: %s",
+ subQual, StringsPlume.join(",", qualifiers2));
+ }
+ if (!isSubtype(subQual, superQual) && !isSubtype(superQual, subQual)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
/**
* Returns the least upper bound (LUB) of the qualifiers {@code qualifier1} and {@code
* qualifier2}. Returns {@code null} if the qualifiers are not from the same qualifier
diff --git a/framework/tests/value/Basics.java b/framework/tests/value/Basics.java
index 05787674e976..a0926304f396 100644
--- a/framework/tests/value/Basics.java
+++ b/framework/tests/value/Basics.java
@@ -170,7 +170,7 @@ public void intCastTest(@IntVal({0, 1}) int input) {
@IntVal({0, 1, 2}) int sc = (@IntVal({0, 1, 2}) int) input;
// :: warning: (cast.unsafe)
@IntVal({1}) int uc = (@IntVal({1}) int) input;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal({2}) int bc = (@IntVal({2}) int) input;
}
diff --git a/framework/tests/value/Issue2367.java b/framework/tests/value/Issue2367.java
index f2b9e9126e87..42a4b441c182 100644
--- a/framework/tests/value/Issue2367.java
+++ b/framework/tests/value/Issue2367.java
@@ -12,13 +12,13 @@ public class Issue2367 {
// Without the `(byte)` cast, all of these produce the following javac error:
// error: incompatible types: possible lossy conversion from int to byte
- // The Value Checker's `cast.unsafe` error is analogous and is desirable.
+ // The Value Checker's `cast.incompatible` error is analogous and is desirable.
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
byte b4 = (byte) 139; // b4 == -117
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
byte b5 = (byte) -240;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
byte b6 = (byte) 251;
// Outside the signed byte range, but written as a hexadecimal literal.
@@ -29,6 +29,6 @@ public class Issue2367 {
// The program element "(byte) 0x8B" has already been converted to "(byte)139" by javac before
// the Checker Framework gets access to it.
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
byte b7 = (byte) 0x8B; // 0x8B == 137, and b4 == -117
}
diff --git a/framework/tests/value/Overflows.java b/framework/tests/value/Overflows.java
index 72b1806bca7f..36a2c0a0611b 100644
--- a/framework/tests/value/Overflows.java
+++ b/framework/tests/value/Overflows.java
@@ -4,19 +4,19 @@ public class Overflows {
static void bytes() {
byte max = Byte.MAX_VALUE;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal(-128) byte maxPlus1 = (byte) (max + 1);
}
static void chars() {
char max = Character.MAX_VALUE;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal(0) char maxPlus1 = (char) (max + 1);
}
static void shorts() {
short max = Short.MAX_VALUE;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal(-32768) short maxPlus1 = (short) (max + 1);
}
diff --git a/framework/tests/value/TypeCast.java b/framework/tests/value/TypeCast.java
index 959bb4d7c787..089b121efc9b 100644
--- a/framework/tests/value/TypeCast.java
+++ b/framework/tests/value/TypeCast.java
@@ -45,12 +45,12 @@ void otherCast() {
void rangeCast(@IntRange(from = 127, to = 128) int a, @IntRange(from = 128, to = 129) int b) {
@IntRange(from = 0, to = 128)
- // :: error: (assignment.type.incompatible) :: warning: (cast.unsafe)
+ // :: error: (assignment.type.incompatible) :: error: (cast.incompatible)
byte c = (byte) a;
// (byte) a is @IntRange(from = -128, to = 127) because of casting
@IntRange(from = -128, to = -127)
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
byte d = (byte) b;
}
}
diff --git a/framework/tests/value/Underflows.java b/framework/tests/value/Underflows.java
index 3c51eedad78d..8204eec61e58 100644
--- a/framework/tests/value/Underflows.java
+++ b/framework/tests/value/Underflows.java
@@ -3,19 +3,19 @@
public class Underflows {
static void bytes() {
byte min = Byte.MIN_VALUE;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal(127) byte maxPlus1 = (byte) (min - 1);
}
static void chars() {
char min = Character.MIN_VALUE;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal(65535) char maxPlus1 = (char) (min - 1);
}
static void shorts() {
short min = Short.MIN_VALUE;
- // :: warning: (cast.unsafe)
+ // :: error: (cast.incompatible)
@IntVal(32767) short maxPlus1 = (short) (min - 1);
}
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java
index 6f14068d61c6..061724b2f292 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java
@@ -293,6 +293,17 @@ public static boolean areSamePrimitiveTypes(TypeMirror left, TypeMirror right) {
return (left.getKind() == right.getKind());
}
+ /**
+ * Returns true iff the arguments are both the same type variables.
+ *
+ * @param v1 a type variable
+ * @param v2 a type variable
+ * @return whether the arguments are the same type variables
+ */
+ public static boolean areSameTypeVariables(TypeVariable v1, TypeVariable v2) {
+ return v1.asElement().getSimpleName() == v2.asElement().getSimpleName();
+ }
+
/// Predicates
/**