From 298df8ae4d62c2f3d5c40b97c3e682b25441d48d Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Tue, 14 Jun 2022 17:21:04 -0400 Subject: [PATCH 01/40] add downcast to cf --- .../common/basetype/BaseTypeVisitor.java | 37 +++++++++++++------ 1 file changed, 25 insertions(+), 12 deletions(-) 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 48e0ae1f28e..3cef6c0df70 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2367,6 +2367,18 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } } + /** + * Allow no incomparable cast by default. Other type systems may override this method to allow + * certain incomparable casts. + * + * @param castType castType + * @param exprType exprType + * @return always false in BaseTypeVisitor + */ + protected boolean isIncomparableCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + return false; + } + /** * Returns true if the cast is safe. * @@ -2380,21 +2392,22 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { 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 bounds = - atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); - - if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { - return true; + QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); + Set castAnnos; + + if (castTypeKind == TypeKind.DECLARED) { // Check if the downcast is valid + TypeMirror castJavaType = castType.getUnderlyingType(); + TypeMirror exprJavaType = exprType.getUnderlyingType(); + if (exprJavaType.getClass().isAssignableFrom(castJavaType.getClass())) { + if (qualifierHierarchy.isSubtype(castType.getAnnotations(), exprType.getAnnotations()) + || qualifierHierarchy.isSubtype(exprType.getAnnotations(), castType.getAnnotations())) { + return true; + } else { + return isIncomparableCastSafe(castType, exprType); + } } } - QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); - - Set castAnnos; if (!checker.hasOption("checkCastElementType")) { // checkCastElementType option wasn't specified, so only check effective annotations. castAnnos = castType.getEffectiveAnnotations(); From c4588df67637a70dcf2291f2f3368b991a13ebfe Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 15 Jun 2022 09:57:20 -0400 Subject: [PATCH 02/40] add downcast to cf --- .../common/basetype/BaseTypeVisitor.java | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) 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 3cef6c0df70..11368f515d6 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2375,7 +2375,8 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { * @param exprType exprType * @return always false in BaseTypeVisitor */ - protected boolean isIncomparableCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected boolean isIncomparableCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { return false; } @@ -2393,14 +2394,15 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr final TypeKind castTypeKind = castType.getKind(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); - Set castAnnos; if (castTypeKind == TypeKind.DECLARED) { // Check if the downcast is valid TypeMirror castJavaType = castType.getUnderlyingType(); TypeMirror exprJavaType = exprType.getUnderlyingType(); - if (exprJavaType.getClass().isAssignableFrom(castJavaType.getClass())) { - if (qualifierHierarchy.isSubtype(castType.getAnnotations(), exprType.getAnnotations()) - || qualifierHierarchy.isSubtype(exprType.getAnnotations(), castType.getAnnotations())) { + if (TypesUtils.isErasedSubtype(castJavaType, exprJavaType, types)) { + Set castAnnos = castType.getAnnotations(); + Set exprAnnos = exprType.getAnnotations(); + if (qualifierHierarchy.isSubtype(castAnnos, exprAnnos) + || qualifierHierarchy.isSubtype(exprAnnos, castAnnos)) { return true; } else { return isIncomparableCastSafe(castType, exprType); @@ -2408,6 +2410,7 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr } } + Set castAnnos; if (!checker.hasOption("checkCastElementType")) { // checkCastElementType option wasn't specified, so only check effective annotations. castAnnos = castType.getEffectiveAnnotations(); From 82740f7bb76dde9520b93435e17ba48e41e0d526 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 17 Jun 2022 13:44:54 -0400 Subject: [PATCH 03/40] add downcast/incomparable cast to cf --- .../index/inequality/LessThanVisitor.java | 3 +- .../checker/interning/InterningVisitor.java | 5 +- .../common/basetype/BaseTypeVisitor.java | 168 ++++++++++++------ 3 files changed, 121 insertions(+), 55 deletions(-) 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 60fc1572c4c..7bb11ef7719 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 50474671a32..c4f12b1ae82 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.WARNING; } return super.isTypeCastSafe(castType, exprType); } 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 11368f515d6..1d9990c5693 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2361,57 +2361,42 @@ 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 + || castResult == CastSafeKind.ERROR) { // TODO: refine the error report + checker.reportWarning( + typeCastTree, + "cast.unsafe", + exprType.toString(true), + castType.toString(true)); + } } } - /** - * Allow no incomparable cast by default. Other type systems may override this method to allow - * certain incomparable casts. - * - * @param castType castType - * @param exprType exprType - * @return always false in BaseTypeVisitor - */ - protected boolean isIncomparableCastSafe( - AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - return false; + /** CastSafeKind */ + protected enum CastSafeKind { + SAFE, + ERROR, + WARNING, + NOT_UPCAST, + NOT_DOWNCAST } /** - * Returns true if the cast is safe. + * isUpcast * - *

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 true if the type cast is safe, false otherwise + * @param castType castType + * @param exprType exprType + * @return CastSafeKind */ - protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - - final TypeKind castTypeKind = castType.getKind(); + protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); - - if (castTypeKind == TypeKind.DECLARED) { // Check if the downcast is valid - TypeMirror castJavaType = castType.getUnderlyingType(); - TypeMirror exprJavaType = exprType.getUnderlyingType(); - if (TypesUtils.isErasedSubtype(castJavaType, exprJavaType, types)) { - Set castAnnos = castType.getAnnotations(); - Set exprAnnos = exprType.getAnnotations(); - if (qualifierHierarchy.isSubtype(castAnnos, exprAnnos) - || qualifierHierarchy.isSubtype(exprAnnos, castAnnos)) { - return true; - } else { - return isIncomparableCastSafe(castType, exprType); - } - } - } - Set castAnnos; - if (!checker.hasOption("checkCastElementType")) { + TypeKind castTypeKind = castType.getKind(); + boolean flagEnabled = checker.hasOption("checkCastElementType"); + if (!flagEnabled) { // checkCastElementType option wasn't specified, so only check effective annotations. castAnnos = castType.getEffectiveAnnotations(); } else { @@ -2429,13 +2414,13 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr } if (!atypeFactory.getTypeHierarchy().isSubtype(newExprType, newCastType)) { - return false; + return CastSafeKind.ERROR; } if (newCastType.getKind() == TypeKind.ARRAY && newExprType.getKind() != TypeKind.ARRAY) { // Always warn if the cast contains an array, but the expression // doesn't, as in "(Object[]) o" where o is of type Object - return false; + return CastSafeKind.ERROR; } else if (newCastType.getKind() == TypeKind.DECLARED && newExprType.getKind() == TypeKind.DECLARED) { int castSize = ((AnnotatedDeclaredType) newCastType).getTypeArguments().size(); @@ -2445,7 +2430,7 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr // Always warn if the cast and expression contain a different number of type // arguments, e.g. to catch a cast from "Object" to "List<@NonNull Object>". // TODO: the same number of arguments actually doesn't guarantee anything. - return false; + return CastSafeKind.ERROR; } } else if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { // If both the cast type and the casted expression are type variables, then check @@ -2456,11 +2441,13 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr Set lowerBoundAnnotationsExpr = AnnotatedTypes.findEffectiveLowerBoundAnnotations( qualifierHierarchy, exprType); - return qualifierHierarchy.isSubtype( - lowerBoundAnnotationsExpr, lowerBoundAnnotationsCast) - && qualifierHierarchy.isSubtype( - exprType.getEffectiveAnnotations(), - castType.getEffectiveAnnotations()); + boolean result = + qualifierHierarchy.isSubtype( + lowerBoundAnnotationsExpr, lowerBoundAnnotationsCast) + && qualifierHierarchy.isSubtype( + exprType.getEffectiveAnnotations(), + castType.getEffectiveAnnotations()); + return result ? CastSafeKind.SAFE : CastSafeKind.ERROR; } if (castTypeKind == TypeKind.TYPEVAR) { // If the cast type is a type var, but the expression is not, then check that the @@ -2474,7 +2461,84 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr } AnnotatedTypeMirror exprTypeWidened = atypeFactory.getWidenedType(exprType, castType); - return qualifierHierarchy.isSubtype(exprTypeWidened.getEffectiveAnnotations(), castAnnos); + boolean result = + qualifierHierarchy.isSubtype(exprTypeWidened.getEffectiveAnnotations(), castAnnos); + if (result) { + return CastSafeKind.SAFE; + } else if (flagEnabled) { // when the flag is enabled and it is not an upcast, return an + // error + return CastSafeKind.ERROR; + } else { + return CastSafeKind.NOT_UPCAST; + } + } + + /** + * isSafeDowncast + * + * @param castType castType + * @param exprType exprType + * @return CastSafeKind + */ + protected CastSafeKind isSafeDowncast( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + Set castAnnos = castType.getAnnotations(); + Set exprAnnos = exprType.getAnnotations(); + QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); + + if (!qualifierHierarchy.isSubtype(castAnnos, exprAnnos)) { // not a downcast + return CastSafeKind.NOT_DOWNCAST; + } + + // check if the downcast can be statically verified + 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 bounds = + atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); + + if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { + return CastSafeKind.SAFE; + } + } + return CastSafeKind.WARNING; + } + + protected CastSafeKind isSafeIncomparableCast( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + return CastSafeKind.ERROR; + } + + /** + * Returns true if the cast is safe. + * + *

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; + } } /** @@ -2487,7 +2551,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); @@ -2539,7 +2603,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); } } From d71ead680c96cc9d34de6388025cfe9dee3466dc Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 18 Jun 2022 14:37:56 -0400 Subject: [PATCH 04/40] use getEffectiveAnnotation --- .../checker/interning/InterningVisitor.java | 2 +- .../common/basetype/BaseTypeVisitor.java | 17 +++++++++++++++-- .../checkerframework/javacutil/TypesUtils.java | 12 ++++++++++++ 3 files changed, 28 insertions(+), 3 deletions(-) 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 c4f12b1ae82..de05e226047 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java @@ -980,7 +980,7 @@ DeclaredType typeToCheck() { protected CastSafeKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (castType.getKind().isPrimitive()) { - return CastSafeKind.WARNING; + return CastSafeKind.SAFE; } return super.isTypeCastSafe(castType, exprType); } 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 1d9990c5693..f12a27927d8 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2460,9 +2460,22 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } } + // // Return a warning in this case, as compiler will not report the unchecked + // warning in + // // this case, and we cannot statically verify the subtype relation of the + // annotations. + // if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { + // TypeMirror castJavaType = castType.getUnderlyingType(); + // TypeMirror exprJavaType = exprType.getUnderlyingType(); + // if (TypesUtils.areSameTypeVariables(castJavaType, exprJavaType)) { + // return CastSafeKind.WARNING; + // } + // } + AnnotatedTypeMirror exprTypeWidened = atypeFactory.getWidenedType(exprType, castType); boolean result = qualifierHierarchy.isSubtype(exprTypeWidened.getEffectiveAnnotations(), castAnnos); + if (result) { return CastSafeKind.SAFE; } else if (flagEnabled) { // when the flag is enabled and it is not an upcast, return an @@ -2482,8 +2495,8 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro */ protected CastSafeKind isSafeDowncast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - Set castAnnos = castType.getAnnotations(); - Set exprAnnos = exprType.getAnnotations(); + Set castAnnos = castType.getEffectiveAnnotations(); + Set exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); if (!qualifierHierarchy.isSubtype(castAnnos, exprAnnos)) { // not a downcast diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index 6f14068d61c..56e2a662127 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -293,6 +293,18 @@ 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 t1 a type + * @param t2 a type + * @return whether the arguments are the same type variables + */ + public static boolean areSameTypeVariables( + TypeMirror t1, TypeMirror t2) { // TODO: a cheaper way of doing this? + return t1.toString().equals(t2.toString()); + } + /// Predicates /** From 0dec947d20865968ca04cc2c1980291a684d2928 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 18 Jun 2022 15:51:57 -0400 Subject: [PATCH 05/40] check the java type down cast --- .../checkerframework/common/basetype/BaseTypeVisitor.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 f12a27927d8..f36abf58a36 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2514,7 +2514,11 @@ protected CastSafeKind isSafeDowncast( atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { - return CastSafeKind.SAFE; + TypeMirror castJavaType = castType.getUnderlyingType(); + TypeMirror exprJavaType = exprType.getUnderlyingType(); + if (TypesUtils.isErasedSubtype(castJavaType, exprJavaType, types)) { + return CastSafeKind.SAFE; + } } } return CastSafeKind.WARNING; From f5c5d228736eac56ca4b40339e8b1712c3d13923 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 18 Jun 2022 21:55:28 -0400 Subject: [PATCH 06/40] revert typo fix, fix in another pr --- .../main/java/org/checkerframework/javacutil/TypesUtils.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index 56e2a662127..419025103b9 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -275,7 +275,7 @@ public static boolean areSameDeclaredTypes(Type.ClassType t1, Type.ClassType t2) if (t1.tsym.name != t2.tsym.name) { return false; } - return t1.toString().equals(t2.toString()); + return t1.toString().equals(t1.toString()); } /** From c91649351e4fed29b5191ef8c9fc4b6b1d121e66 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 22 Jun 2022 18:04:08 -0400 Subject: [PATCH 07/40] add incomparable cast message key --- checker/tests/lock/Strings.java | 2 ++ checker/tests/signedness/CharToFloat.java | 2 ++ .../common/basetype/BaseTypeVisitor.java | 31 +++++++++++-------- .../common/basetype/messages.properties | 1 + .../javacutil/TypesUtils.java | 9 +++--- 5 files changed, 27 insertions(+), 18 deletions(-) diff --git a/checker/tests/lock/Strings.java b/checker/tests/lock/Strings.java index c29200e1d47..d788ebef87a 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/CharToFloat.java b/checker/tests/signedness/CharToFloat.java index 1caaea9f8f0..44874da7161 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/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index f36abf58a36..cd99112b53f 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; @@ -2364,13 +2365,18 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { if (!calledOnce) { CastSafeKind castResult = isTypeCastSafe(castType, exprType); - if (castResult == CastSafeKind.WARNING - || castResult == CastSafeKind.ERROR) { // TODO: refine the error report + 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)); } } } @@ -2460,17 +2466,16 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } } - // // Return a warning in this case, as compiler will not report the unchecked - // warning in - // // this case, and we cannot statically verify the subtype relation of the - // annotations. - // if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { - // TypeMirror castJavaType = castType.getUnderlyingType(); - // TypeMirror exprJavaType = exprType.getUnderlyingType(); - // if (TypesUtils.areSameTypeVariables(castJavaType, exprJavaType)) { - // return CastSafeKind.WARNING; - // } - // } + // Return a warning in this case, as compiler will not report the unchecked warning in + // this case, and we cannot statically verify the subtype relation of the annotations. + if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { + TypeMirror castJavaType = castType.getUnderlyingType(); + TypeMirror exprJavaType = exprType.getUnderlyingType(); + if (TypesUtils.areSameTypeVariables( + (TypeVariable) castJavaType, (TypeVariable) exprJavaType)) { + return CastSafeKind.WARNING; + } + } AnnotatedTypeMirror exprTypeWidened = atypeFactory.getWidenedType(exprType, castType); boolean result = 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 89a38bd6735..55772bf918c 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=type cast incompatible 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/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index 419025103b9..ea7462c1dec 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -296,13 +296,12 @@ public static boolean areSamePrimitiveTypes(TypeMirror left, TypeMirror right) { /** * Returns true iff the arguments are both the same type variables. * - * @param t1 a type - * @param t2 a type + * @param v1 a type variable + * @param v2 a type variable * @return whether the arguments are the same type variables */ - public static boolean areSameTypeVariables( - TypeMirror t1, TypeMirror t2) { // TODO: a cheaper way of doing this? - return t1.toString().equals(t2.toString()); + public static boolean areSameTypeVariables(TypeVariable v1, TypeVariable v2) { + return v1.asElement().getSimpleName() == v2.asElement().getSimpleName(); } /// Predicates From bfa5794a7dc81efc4259691cede655c0b2760742 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 22 Jun 2022 21:23:31 -0400 Subject: [PATCH 08/40] replace some warnings with incompatible cast errors --- checker/tests/lock/ChapterExamples.java | 4 ++-- .../nullness-checkcastelementtype/Issue1315.java | 2 +- checker/tests/nullness/CastTypeVariable.java | 1 + checker/tests/nullness/CastsNullness.java | 4 ++-- checker/tests/nullness/java8inference/Issue1032.java | 2 +- checker/tests/signedness/CharCast.java | 4 ++-- checker/tests/signedness/PrimitiveCasts.java | 2 +- checker/tests/signedness/WideningConversion.java | 12 ++++++------ .../common/basetype/messages.properties | 2 +- framework/tests/value/Basics.java | 2 +- framework/tests/value/Issue2367.java | 10 +++++----- framework/tests/value/Overflows.java | 6 +++--- framework/tests/value/TypeCast.java | 4 ++-- framework/tests/value/Underflows.java | 6 +++--- 14 files changed, 31 insertions(+), 30 deletions(-) diff --git a/checker/tests/lock/ChapterExamples.java b/checker/tests/lock/ChapterExamples.java index f2c76716ed4..c571c36b532 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/nullness-checkcastelementtype/Issue1315.java b/checker/tests/nullness-checkcastelementtype/Issue1315.java index 3fb1afe1d52..76fd8fb342e 100644 --- a/checker/tests/nullness-checkcastelementtype/Issue1315.java +++ b/checker/tests/nullness-checkcastelementtype/Issue1315.java @@ -13,7 +13,7 @@ static class Box { @SuppressWarnings("unchecked") T test1(@Nullable Object p) { - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) return (T) p; } // The Nullness Checker should not issue a cast.unsafe warning, diff --git a/checker/tests/nullness/CastTypeVariable.java b/checker/tests/nullness/CastTypeVariable.java index 323ed8c0487..5364cdec637 100644 --- a/checker/tests/nullness/CastTypeVariable.java +++ b/checker/tests/nullness/CastTypeVariable.java @@ -9,6 +9,7 @@ class MyAnnotatedTypeVariable extends MyAnnotatedTypeMirror {} public class CastTypeVariable { public static V mapGetHelper( Map mappings, MyAnnotatedTypeVariable key) { + // :: warning: (cast.unsafe) V possValue = (V) mappings.get(key); // :: error: (dereference.of.nullable) possValue.addAnnotations(); diff --git a/checker/tests/nullness/CastsNullness.java b/checker/tests/nullness/CastsNullness.java index cb5deb34eec..7c468a9a711 100644 --- a/checker/tests/nullness/CastsNullness.java +++ b/checker/tests/nullness/CastsNullness.java @@ -88,9 +88,9 @@ void m() { // :: error: (assignment.type.incompatible) t = (@Nullable T) null; nt = (@Nullable T) null; - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) t = (T) null; - // :: warning: (cast.unsafe) + // :: error: (cast.incompatible) nt = (T) null; } } diff --git a/checker/tests/nullness/java8inference/Issue1032.java b/checker/tests/nullness/java8inference/Issue1032.java index b09a59413fd..273dd2779fa 100644 --- a/checker/tests/nullness/java8inference/Issue1032.java +++ b/checker/tests/nullness/java8inference/Issue1032.java @@ -16,7 +16,7 @@ public class Issue1032 { return arg.map(Issue1032::castStringToNonNull); } - @SuppressWarnings("nullness") + @SuppressWarnings("nullness", "cast.unsafe") static @NonNull T castTToNonNull(@Nullable T arg) { return (@NonNull T) arg; } diff --git a/checker/tests/signedness/CharCast.java b/checker/tests/signedness/CharCast.java index 788eb5b19ce..324a385f0fe 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/PrimitiveCasts.java b/checker/tests/signedness/PrimitiveCasts.java index 132d430d023..62ef25e3076 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 68d2ae776ab..f294b6da05c 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/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index 55772bf918c..0160bb082a2 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -26,7 +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=type cast incompatible from "%s" to "%s" +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/tests/value/Basics.java b/framework/tests/value/Basics.java index 05787674e97..a0926304f39 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 f2b9e9126e8..42a4b441c18 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 72b1806bca7..36a2c0a0611 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 959bb4d7c78..089b121efc9 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 3c51eedad78..8204eec61e5 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); } From 93a6a1a5036217242a3fc47559488ce5889cb1bb Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 25 Jun 2022 09:55:16 -0400 Subject: [PATCH 09/40] refined the approach when casting T to T --- .../Issue1315.java | 2 +- checker/tests/nullness/CastsNullness.java | 4 +- .../nullness/java8inference/Issue1032.java | 2 +- .../common/basetype/BaseTypeVisitor.java | 44 +++++++++++-------- .../framework/type/QualifierHierarchy.java | 27 ++++++++++++ 5 files changed, 56 insertions(+), 23 deletions(-) diff --git a/checker/tests/nullness-checkcastelementtype/Issue1315.java b/checker/tests/nullness-checkcastelementtype/Issue1315.java index 76fd8fb342e..3fb1afe1d52 100644 --- a/checker/tests/nullness-checkcastelementtype/Issue1315.java +++ b/checker/tests/nullness-checkcastelementtype/Issue1315.java @@ -13,7 +13,7 @@ static class Box { @SuppressWarnings("unchecked") T test1(@Nullable Object p) { - // :: error: (cast.incompatible) + // :: warning: (cast.unsafe) return (T) p; } // The Nullness Checker should not issue a cast.unsafe warning, diff --git a/checker/tests/nullness/CastsNullness.java b/checker/tests/nullness/CastsNullness.java index 7c468a9a711..cb5deb34eec 100644 --- a/checker/tests/nullness/CastsNullness.java +++ b/checker/tests/nullness/CastsNullness.java @@ -88,9 +88,9 @@ void m() { // :: error: (assignment.type.incompatible) t = (@Nullable T) null; nt = (@Nullable T) null; - // :: error: (cast.incompatible) + // :: warning: (cast.unsafe) t = (T) null; - // :: error: (cast.incompatible) + // :: warning: (cast.unsafe) nt = (T) null; } } diff --git a/checker/tests/nullness/java8inference/Issue1032.java b/checker/tests/nullness/java8inference/Issue1032.java index 273dd2779fa..b09a59413fd 100644 --- a/checker/tests/nullness/java8inference/Issue1032.java +++ b/checker/tests/nullness/java8inference/Issue1032.java @@ -16,7 +16,7 @@ public class Issue1032 { return arg.map(Issue1032::castStringToNonNull); } - @SuppressWarnings("nullness", "cast.unsafe") + @SuppressWarnings("nullness") static @NonNull T castTToNonNull(@Nullable T arg) { return (@NonNull T) arg; } 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 cd99112b53f..69383387ea6 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2401,8 +2401,8 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); Set castAnnos; TypeKind castTypeKind = castType.getKind(); - boolean flagEnabled = checker.hasOption("checkCastElementType"); - if (!flagEnabled) { + boolean checkCastElementType = checker.hasOption("checkCastElementType"); + if (!checkCastElementType) { // checkCastElementType option wasn't specified, so only check effective annotations. castAnnos = castType.getEffectiveAnnotations(); } else { @@ -2420,13 +2420,13 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } if (!atypeFactory.getTypeHierarchy().isSubtype(newExprType, newCastType)) { - return CastSafeKind.ERROR; + return CastSafeKind.WARNING; } if (newCastType.getKind() == TypeKind.ARRAY && newExprType.getKind() != TypeKind.ARRAY) { // Always warn if the cast contains an array, but the expression // doesn't, as in "(Object[]) o" where o is of type Object - return CastSafeKind.ERROR; + return CastSafeKind.WARNING; } else if (newCastType.getKind() == TypeKind.DECLARED && newExprType.getKind() == TypeKind.DECLARED) { int castSize = ((AnnotatedDeclaredType) newCastType).getTypeArguments().size(); @@ -2436,7 +2436,7 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // Always warn if the cast and expression contain a different number of type // arguments, e.g. to catch a cast from "Object" to "List<@NonNull Object>". // TODO: the same number of arguments actually doesn't guarantee anything. - return CastSafeKind.ERROR; + return CastSafeKind.WARNING; } } else if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { // If both the cast type and the casted expression are type variables, then check @@ -2453,7 +2453,7 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro && qualifierHierarchy.isSubtype( exprType.getEffectiveAnnotations(), castType.getEffectiveAnnotations()); - return result ? CastSafeKind.SAFE : CastSafeKind.ERROR; + return result ? CastSafeKind.SAFE : CastSafeKind.WARNING; } if (castTypeKind == TypeKind.TYPEVAR) { // If the cast type is a type var, but the expression is not, then check that the @@ -2469,11 +2469,19 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // Return a warning in this case, as compiler will not report the unchecked warning in // this case, and we cannot statically verify the subtype relation of the annotations. if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { - TypeMirror castJavaType = castType.getUnderlyingType(); - TypeMirror exprJavaType = exprType.getUnderlyingType(); - if (TypesUtils.areSameTypeVariables( - (TypeVariable) castJavaType, (TypeVariable) exprJavaType)) { - return CastSafeKind.WARNING; + TypeVariable castTV = (TypeVariable) castType.getUnderlyingType(); + TypeVariable exprTV = (TypeVariable) exprType.getUnderlyingType(); + if (TypesUtils.areSameTypeVariables(castTV, exprTV)) { + Set t1 = + AnnotatedTypes.findEffectiveLowerBoundAnnotations( + qualifierHierarchy, castType); + Set t2 = + AnnotatedTypes.findEffectiveAnnotations(qualifierHierarchy, exprType); + + if (!qualifierHierarchy.isSubtype(t2, t1)) { + return CastSafeKind.WARNING; + } + return CastSafeKind.SAFE; } } @@ -2483,9 +2491,10 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro if (result) { return CastSafeKind.SAFE; - } else if (flagEnabled) { // when the flag is enabled and it is not an upcast, return an + } else if (checkCastElementType) { // when the flag is enabled and it is not an upcast, + // return an // error - return CastSafeKind.ERROR; + return CastSafeKind.WARNING; } else { return CastSafeKind.NOT_UPCAST; } @@ -2504,7 +2513,8 @@ protected CastSafeKind isSafeDowncast( Set exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); - if (!qualifierHierarchy.isSubtype(castAnnos, exprAnnos)) { // not a downcast + for (int i = 0; i < castAnnos.size(); i++) {} + if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { // exists an incomparable cast return CastSafeKind.NOT_DOWNCAST; } @@ -2519,11 +2529,7 @@ protected CastSafeKind isSafeDowncast( atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { - TypeMirror castJavaType = castType.getUnderlyingType(); - TypeMirror exprJavaType = exprType.getUnderlyingType(); - if (TypesUtils.isErasedSubtype(castJavaType, exprJavaType, types)) { - return CastSafeKind.SAFE; - } + return CastSafeKind.SAFE; } } return CastSafeKind.WARNING; 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 e379dd4d974..db4bc6a4c09 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 qualifiers1, + Collection 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 From b04007c8316b49bae2f16cea3514e1ea20283008 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 25 Jun 2022 11:40:40 -0400 Subject: [PATCH 10/40] suppress some warnings --- .../checkerframework/checker/nullness/util/NullnessUtil.java | 2 ++ checker/tests/nullness/CastTypeVariable.java | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java b/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java index 88fb80e1bc5..a38da92556b 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java @@ -66,6 +66,7 @@ private NullnessUtil() { * @return the argument, casted to have the type qualifier @NonNull */ @EnsuresNonNull("#1") + @SuppressWarnings("cast.unsafe") public static @NonNull T castNonNull(@Nullable T ref) { assert ref != null : "Misuse of castNonNull: called with a null argument"; return (@NonNull T) ref; @@ -81,6 +82,7 @@ private NullnessUtil() { * @param message text to include if this method is misused * @return the argument, casted to have the type qualifier @NonNull */ + @SuppressWarnings("cast.unsafe") public static @EnsuresNonNull("#1") @NonNull T castNonNull( @Nullable T ref, String message) { assert ref != null : "Misuse of castNonNull: called with a null argument: " + message; diff --git a/checker/tests/nullness/CastTypeVariable.java b/checker/tests/nullness/CastTypeVariable.java index 5364cdec637..323ed8c0487 100644 --- a/checker/tests/nullness/CastTypeVariable.java +++ b/checker/tests/nullness/CastTypeVariable.java @@ -9,7 +9,6 @@ class MyAnnotatedTypeVariable extends MyAnnotatedTypeMirror {} public class CastTypeVariable { public static V mapGetHelper( Map mappings, MyAnnotatedTypeVariable key) { - // :: warning: (cast.unsafe) V possValue = (V) mappings.get(key); // :: error: (dereference.of.nullable) possValue.addAnnotations(); From 9b116a774bb37c22ba15d532aaba454de58482e9 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 26 Jun 2022 11:10:38 -0400 Subject: [PATCH 11/40] refine the logic to cast from T to T --- .../checker/nullness/util/NullnessUtil.java | 2 -- .../common/basetype/BaseTypeVisitor.java | 26 +++++++++++++------ 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java b/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java index a38da92556b..88fb80e1bc5 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java @@ -66,7 +66,6 @@ private NullnessUtil() { * @return the argument, casted to have the type qualifier @NonNull */ @EnsuresNonNull("#1") - @SuppressWarnings("cast.unsafe") public static @NonNull T castNonNull(@Nullable T ref) { assert ref != null : "Misuse of castNonNull: called with a null argument"; return (@NonNull T) ref; @@ -82,7 +81,6 @@ private NullnessUtil() { * @param message text to include if this method is misused * @return the argument, casted to have the type qualifier @NonNull */ - @SuppressWarnings("cast.unsafe") public static @EnsuresNonNull("#1") @NonNull T castNonNull( @Nullable T ref, String message) { assert ref != null : "Misuse of castNonNull: called with a null argument: " + message; 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 69383387ea6..4490e7c8c61 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2383,10 +2383,15 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { /** 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 } @@ -2472,16 +2477,22 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro TypeVariable castTV = (TypeVariable) castType.getUnderlyingType(); TypeVariable exprTV = (TypeVariable) exprType.getUnderlyingType(); if (TypesUtils.areSameTypeVariables(castTV, exprTV)) { - Set t1 = + Set castLower = AnnotatedTypes.findEffectiveLowerBoundAnnotations( qualifierHierarchy, castType); - Set t2 = + Set exprLower = + AnnotatedTypes.findEffectiveLowerBoundAnnotations( + qualifierHierarchy, exprType); + Set castUpper = + AnnotatedTypes.findEffectiveAnnotations(qualifierHierarchy, castType); + Set exprUpper = AnnotatedTypes.findEffectiveAnnotations(qualifierHierarchy, exprType); - if (!qualifierHierarchy.isSubtype(t2, t1)) { - return CastSafeKind.WARNING; + if (qualifierHierarchy.isSubtype(exprLower, castLower) + && qualifierHierarchy.isSubtype(exprUpper, castUpper)) { + return CastSafeKind.SAFE; } - return CastSafeKind.SAFE; + return CastSafeKind.WARNING; } } @@ -2491,9 +2502,8 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro if (result) { return CastSafeKind.SAFE; - } else if (checkCastElementType) { // when the flag is enabled and it is not an upcast, - // return an - // error + } else if (checkCastElementType) { + // when the flag is enabled, and it is not an upcast, return an error return CastSafeKind.WARNING; } else { return CastSafeKind.NOT_UPCAST; From b88949fd4173dab3a74620d94d2a377106bd8b5e Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 26 Jun 2022 19:24:07 -0400 Subject: [PATCH 12/40] add method documentation --- .../common/basetype/BaseTypeVisitor.java | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) 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 4490e7c8c61..4c7bc330d4d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2396,11 +2396,11 @@ protected enum CastSafeKind { } /** - * isUpcast + * Return true if it's an upcast (from the view of the qualifiers) and it's safe. * * @param castType castType * @param exprType exprType - * @return CastSafeKind + * @return Can return NOT_UPCAST, WARNING or SAFE CastSafeKind. */ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); @@ -2511,11 +2511,11 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } /** - * isSafeDowncast + * Return true if it's a downcast (from the view of the qualifiers) and the cast is safe. * * @param castType castType * @param exprType exprType - * @return CastSafeKind + * @return Can return SAFE, NOT_DOWNCAST or WARNING. */ protected CastSafeKind isSafeDowncast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { @@ -2545,6 +2545,14 @@ protected CastSafeKind isSafeDowncast( return CastSafeKind.WARNING; } + /** + * If it's an incomparable cast in terms of qualifiers, return ERROR by default. Subchecker can + * override this method to allow certain incomparable casts. + * + * @param castType castType + * @param exprType exprType + * @return CastSafeKind.ERROR if it's an incomparable cast. + */ protected CastSafeKind isSafeIncomparableCast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { return CastSafeKind.ERROR; From 361f487e389a5612c356f963b12b3fedc96f47a4 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 7 Aug 2022 21:44:18 -0400 Subject: [PATCH 13/40] remove useless for loop --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 1 - 1 file changed, 1 deletion(-) 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 4c7bc330d4d..3623ee0473a 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2523,7 +2523,6 @@ protected CastSafeKind isSafeDowncast( Set exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); - for (int i = 0; i < castAnnos.size(); i++) {} if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { // exists an incomparable cast return CastSafeKind.NOT_DOWNCAST; } From 874e59423883daaa9eaffc51a60ffdfc1531a0b8 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 12 Sep 2022 10:41:17 -0400 Subject: [PATCH 14/40] update mustcallvisitor, signedness visitor --- .../checkerframework/checker/mustcall/MustCallVisitor.java | 5 +++-- .../checker/signedness/SignednessVisitor.java | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) 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 c35de186ba5..22d18b6d707 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 4cc3ac4a965..411428ad3ec 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); } From deffd1d058ee9bf3057adca40314a3f25d26b3e3 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Thu, 13 Oct 2022 10:06:39 -0400 Subject: [PATCH 15/40] add one test file and improve documentation --- checker/tests/nullness/CastFromTtoT.java | 32 +++++++++++++ .../common/basetype/BaseTypeVisitor.java | 46 ++++++++++--------- 2 files changed, 57 insertions(+), 21 deletions(-) create mode 100644 checker/tests/nullness/CastFromTtoT.java diff --git a/checker/tests/nullness/CastFromTtoT.java b/checker/tests/nullness/CastFromTtoT.java new file mode 100644 index 00000000000..56ca5bca0ed --- /dev/null +++ b/checker/tests/nullness/CastFromTtoT.java @@ -0,0 +1,32 @@ +import org.checkerframework.checker.signedness.qual.*; + +import java.util.*; + +class CastFromTtoT { + T bar(@UnknownSignedness Object p) { + T x = (T) p; + return x; + } + + // Seems to have no cast, but in the instantiation, it's a downcast. + // if we use getEffectiveAnnotations, we'll see it as no cast (qualifier aspect) + // But it's fine, as compiler will warn about casting object to 'T' [unchecked warning] + void foo(CastFromTtoT<@Signed Integer> s, @UnknownSignedness Object local) { + @Signed Integer x = s.bar(local); + } + + class Inner { + T bar2(@Signed T p) { + T x = (T) p; // without a warning(guarantee) from the compiler. + return x; + } + + // Looks like an upcast, but it's a downcast. + // This time, as arugment p has type T, which is the same as the casting type + // and the compiler will not issue a warning. So we should give a warning. + void foo2(Inner<@SignednessGlb Integer> s, @Signed Integer local) { + // :: warning: (cast.unsafe) + @SignednessGlb Integer x = s.bar2(local); + } + } +} 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 7f79dbba544..2f3022a6bf0 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2387,11 +2387,14 @@ protected enum CastSafeKind { } /** - * Return true if it's an upcast (from the view of the qualifiers) and it's safe. + * Return SAFE if the typecast is an upcast (from the view of the qualifiers). * - * @param castType castType - * @param exprType exprType - * @return Can return NOT_UPCAST, WARNING or SAFE CastSafeKind. + *

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 return NOT_UPCAST, WARNING or SAFE CastSafeKind. */ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); @@ -2462,8 +2465,10 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } } - // Return a warning in this case, as compiler will not report the unchecked warning in - // this case, and we cannot statically verify the subtype relation of the annotations. + // Check when casting the expression having type T (a type variable) to type T, + // as compiler will not report the unchecked warning in this case (so we should), + // and we cannot statically verify the subtype relation of the annotations. + // See CastFromTtoT.java:20 for an example. if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { TypeVariable castTV = (TypeVariable) castType.getUnderlyingType(); TypeVariable exprTV = (TypeVariable) exprType.getUnderlyingType(); @@ -2479,6 +2484,7 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro Set exprUpper = AnnotatedTypes.findEffectiveAnnotations(qualifierHierarchy, exprType); + // return SAFE only it satisfies the below condition if (qualifierHierarchy.isSubtype(exprLower, castLower) && qualifierHierarchy.isSubtype(exprUpper, castUpper)) { return CastSafeKind.SAFE; @@ -2494,7 +2500,7 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro if (result) { return CastSafeKind.SAFE; } else if (checkCastElementType) { - // when the flag is enabled, and it is not an upcast, return an error + // when the flag is enabled, and it is not an upcast, return a warning return CastSafeKind.WARNING; } else { return CastSafeKind.NOT_UPCAST; @@ -2502,10 +2508,11 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } /** - * Return true if it's a downcast (from the view of the qualifiers) and the cast is safe. + * Determine the typecast is downcast or not. If it is, further determine it can be statically + * verified or not. * - * @param castType castType - * @param exprType exprType + * @param castType annotated type of the cast + * @param exprType annotated type of the casted expression * @return Can return SAFE, NOT_DOWNCAST or WARNING. */ protected CastSafeKind isSafeDowncast( @@ -2539,8 +2546,8 @@ protected CastSafeKind isSafeDowncast( * If it's an incomparable cast in terms of qualifiers, return ERROR by default. Subchecker can * override this method to allow certain incomparable casts. * - * @param castType castType - * @param exprType exprType + * @param castType annotated type of the cast + * @param exprType annotated type of the casted expression * @return CastSafeKind.ERROR if it's an incomparable cast. */ protected CastSafeKind isSafeIncomparableCast( @@ -2549,29 +2556,26 @@ protected CastSafeKind isSafeIncomparableCast( } /** - * Returns true if the cast is safe. - * - *

Only primary qualifiers are checked unless the command line option "checkCastElementType" - * is supplied. + * This method returns CastSafeKind.SAFE when the typecast is an upcast or a statically + * verifiable downcast. Returns CastSafeKind.WARNING and ERROR for those downcasts which cannot + * be statically verified and all incomparable casts. * * @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 + * @return CastSafeKind.SAFE if the type cast is safe, error or warning 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 + // not upcast, do downcast and incomparable cast check + if (castResult == CastSafeKind.NOT_UPCAST) { castResult = isSafeDowncast(castType, exprType); - if (castResult == CastSafeKind.NOT_DOWNCAST) { // fall to incomparable cast return isSafeIncomparableCast(castType, exprType); } else { return castResult; } - } else { return castResult; } From 4f476f24fd95346113141994197a0443416194a3 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 14 Oct 2022 09:43:09 -0400 Subject: [PATCH 16/40] move testfile to another directory --- checker/tests/{nullness => signedness}/CastFromTtoT.java | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename checker/tests/{nullness => signedness}/CastFromTtoT.java (100%) diff --git a/checker/tests/nullness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java similarity index 100% rename from checker/tests/nullness/CastFromTtoT.java rename to checker/tests/signedness/CastFromTtoT.java From f82dc77db062100a9ea22f2db128b0a1ea61bc18 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 14 Oct 2022 09:48:19 -0400 Subject: [PATCH 17/40] fix testcase --- checker/tests/signedness/CastFromTtoT.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/tests/signedness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java index 56ca5bca0ed..b4cb227303a 100644 --- a/checker/tests/signedness/CastFromTtoT.java +++ b/checker/tests/signedness/CastFromTtoT.java @@ -17,6 +17,7 @@ void foo(CastFromTtoT<@Signed Integer> s, @UnknownSignedness Object local) { class Inner { T bar2(@Signed T p) { + // :: warning: (cast.unsafe) T x = (T) p; // without a warning(guarantee) from the compiler. return x; } @@ -25,7 +26,6 @@ T bar2(@Signed T p) { // This time, as arugment p has type T, which is the same as the casting type // and the compiler will not issue a warning. So we should give a warning. void foo2(Inner<@SignednessGlb Integer> s, @Signed Integer local) { - // :: warning: (cast.unsafe) @SignednessGlb Integer x = s.bar2(local); } } From efeeea22d37563a9d71d9e1318e15073da96444c Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 17 Oct 2022 12:01:06 -0400 Subject: [PATCH 18/40] fix testcase --- checker/tests/signedness/CastFromTtoT.java | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/tests/signedness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java index b4cb227303a..01c954ade0d 100644 --- a/checker/tests/signedness/CastFromTtoT.java +++ b/checker/tests/signedness/CastFromTtoT.java @@ -3,6 +3,7 @@ import java.util.*; class CastFromTtoT { + @SuppressWarnings("unchecked") T bar(@UnknownSignedness Object p) { T x = (T) p; return x; From c34285f1632634bbe97cd92ce3e68e1f1e1f6af3 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Tue, 1 Nov 2022 16:59:47 -0400 Subject: [PATCH 19/40] improve naming in the error message --- checker/tests/lock/ChapterExamples.java | 4 ++-- checker/tests/lock/Strings.java | 4 ++-- checker/tests/signedness/CharCast.java | 4 ++-- checker/tests/signedness/CharToFloat.java | 4 ++-- checker/tests/signedness/PrimitiveCasts.java | 2 +- checker/tests/signedness/WideningConversion.java | 12 ++++++------ .../common/basetype/BaseTypeVisitor.java | 2 +- .../common/basetype/messages.properties | 2 +- framework/tests/value/Basics.java | 2 +- framework/tests/value/Issue2367.java | 10 +++++----- framework/tests/value/Overflows.java | 6 +++--- framework/tests/value/TypeCast.java | 4 ++-- framework/tests/value/Underflows.java | 6 +++--- 13 files changed, 31 insertions(+), 31 deletions(-) diff --git a/checker/tests/lock/ChapterExamples.java b/checker/tests/lock/ChapterExamples.java index c571c36b532..b2a6beb75c1 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.incompatible") + @SuppressWarnings("lock:cast.incomparable") 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.incompatible", "guardsatisfied.location.disallowed"}) + @SuppressWarnings({"cast.incomparable", "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 d788ebef87a..b9c4d8f1541 100644 --- a/checker/tests/lock/Strings.java +++ b/checker/tests/lock/Strings.java @@ -13,9 +13,9 @@ void StringIsGBnothing( @GuardSatisfied Object o3, @GuardedByBottom Object o4) { String s1 = (String) o1; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) String s2 = (String) o2; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) String s3 = (String) o3; String s4 = (String) o4; // OK } diff --git a/checker/tests/signedness/CharCast.java b/checker/tests/signedness/CharCast.java index 324a385f0fe..7884b46534b 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; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) char c = (char) x; } void m2(int i) { int x = (short) i; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) char c = (char) x; } diff --git a/checker/tests/signedness/CharToFloat.java b/checker/tests/signedness/CharToFloat.java index 44874da7161..7d67711db12 100644 --- a/checker/tests/signedness/CharToFloat.java +++ b/checker/tests/signedness/CharToFloat.java @@ -2,9 +2,9 @@ public class CharToFloat { void castCharacter(Object o) { - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) floatParameter((Character) o); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) doubleParameter((Character) o); } diff --git a/checker/tests/signedness/PrimitiveCasts.java b/checker/tests/signedness/PrimitiveCasts.java index 62ef25e3076..3c4492df3a1 100644 --- a/checker/tests/signedness/PrimitiveCasts.java +++ b/checker/tests/signedness/PrimitiveCasts.java @@ -3,7 +3,7 @@ public class PrimitiveCasts { void shortToChar1(short s) { - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) char c = (char) s; } diff --git a/checker/tests/signedness/WideningConversion.java b/checker/tests/signedness/WideningConversion.java index f294b6da05c..b4ca13e2528 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); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) c = (char) (c1 + i2); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) c = (char) (i1 + c2); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) c = (char) (i1 + i2); c = (char) (c1 + c2); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) c = (char) (c1 + si2); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) c = (char) (si1 + c2); - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) 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 2f3022a6bf0..053ba373183 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2365,7 +2365,7 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } else if (castResult == CastSafeKind.ERROR) { checker.reportError( typeCastTree, - "cast.incompatible", + "cast.incomparable", exprType.toString(true), castType.toString(true)); } 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 0160bb082a2..c55744d96d9 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -26,7 +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" +cast.incomparable=incomparable 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/tests/value/Basics.java b/framework/tests/value/Basics.java index a0926304f39..868c0334d81 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; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal({2}) int bc = (@IntVal({2}) int) input; } diff --git a/framework/tests/value/Issue2367.java b/framework/tests/value/Issue2367.java index 42a4b441c18..285d130bc35 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.incompatible` error is analogous and is desirable. + // The Value Checker's `cast.incomparable` error is analogous and is desirable. - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) byte b4 = (byte) 139; // b4 == -117 - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) byte b5 = (byte) -240; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) 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. - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) byte b7 = (byte) 0x8B; // 0x8B == 137, and b4 == -117 } diff --git a/framework/tests/value/Overflows.java b/framework/tests/value/Overflows.java index 36a2c0a0611..bf686d5da70 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; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal(-128) byte maxPlus1 = (byte) (max + 1); } static void chars() { char max = Character.MAX_VALUE; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal(0) char maxPlus1 = (char) (max + 1); } static void shorts() { short max = Short.MAX_VALUE; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal(-32768) short maxPlus1 = (short) (max + 1); } diff --git a/framework/tests/value/TypeCast.java b/framework/tests/value/TypeCast.java index 089b121efc9..67a0803852d 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) :: error: (cast.incompatible) + // :: error: (assignment.type.incompatible) :: error: (cast.incomparable) byte c = (byte) a; // (byte) a is @IntRange(from = -128, to = 127) because of casting @IntRange(from = -128, to = -127) - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) byte d = (byte) b; } } diff --git a/framework/tests/value/Underflows.java b/framework/tests/value/Underflows.java index 8204eec61e5..e955e9b729d 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; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal(127) byte maxPlus1 = (byte) (min - 1); } static void chars() { char min = Character.MIN_VALUE; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal(65535) char maxPlus1 = (char) (min - 1); } static void shorts() { short min = Short.MIN_VALUE; - // :: error: (cast.incompatible) + // :: error: (cast.incomparable) @IntVal(32767) short maxPlus1 = (short) (min - 1); } From 16d69a6e5f3decd4ad696ba9634c51b8215ecc67 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 2 Nov 2022 14:03:48 -0400 Subject: [PATCH 20/40] add comments --- checker/tests/signedness/CastFromTtoT.java | 4 +++- .../common/basetype/BaseTypeVisitor.java | 9 +++++---- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/checker/tests/signedness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java index 01c954ade0d..cc999e8c574 100644 --- a/checker/tests/signedness/CastFromTtoT.java +++ b/checker/tests/signedness/CastFromTtoT.java @@ -18,8 +18,10 @@ void foo(CastFromTtoT<@Signed Integer> s, @UnknownSignedness Object local) { class Inner { T bar2(@Signed T p) { + // without a warning from the compiler. The T in the casting expression may have + // different signedness annotation with the arugment p. // :: warning: (cast.unsafe) - T x = (T) p; // without a warning(guarantee) from the compiler. + T x = (T) p; return x; } 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 053ba373183..15892c6db83 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2465,10 +2465,11 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } } - // Check when casting the expression having type T (a type variable) to type T, - // as compiler will not report the unchecked warning in this case (so we should), - // and we cannot statically verify the subtype relation of the annotations. - // See CastFromTtoT.java:20 for an example. + // Check when casting the expression having type T (a type variable) to type T. + // As the compiler will not report the unchecked warning in this case, so we should + // do the check for our type system when the subtype relation of the instantiations of the + // two T cannot be statically verified. + // See CastFromTtoT.java:22 for an example. if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { TypeVariable castTV = (TypeVariable) castType.getUnderlyingType(); TypeVariable exprTV = (TypeVariable) exprType.getUnderlyingType(); From d7429e45f8ed12a85e60b04eba8688bb30825e2b Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 24 Feb 2023 09:22:17 -0500 Subject: [PATCH 21/40] solve field shadowing --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 1 - 1 file changed, 1 deletion(-) 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 e268d564a49..77ab6261780 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2485,7 +2485,6 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); AnnotationMirrorSet castAnnos; TypeKind castTypeKind = castType.getKind(); - boolean checkCastElementType = checker.hasOption("checkCastElementType"); if (!checkCastElementType) { // checkCastElementType option wasn't specified, so only check effective annotations. castAnnos = castType.getEffectiveAnnotations(); From 85024899ec806fc8ccf86b02c73723f992ead6a4 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 24 Feb 2023 10:11:58 -0500 Subject: [PATCH 22/40] update error messages --- checker/tests/signedness/LiteralCast.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/checker/tests/signedness/LiteralCast.java b/checker/tests/signedness/LiteralCast.java index c1ec2552c68..7c8aa588ed5 100644 --- a/checker/tests/signedness/LiteralCast.java +++ b/checker/tests/signedness/LiteralCast.java @@ -24,7 +24,7 @@ void m() { requireSigned((@Unsigned int) 2); requireSigned((int) 2); requireSigned((@m int) 2); - // :: warning: (cast.unsafe) + // :: warning: (cast.incomparable) requireSigned((@Signed int) u); // :: error: (argument.type.incompatible) requireSigned((@Unsigned int) u); @@ -33,7 +33,7 @@ void m() { // :: error: (argument.type.incompatible) requireSigned((@m int) u); requireSigned((@Signed int) s); - // :: error: (argument.type.incompatible) :: warning: (cast.unsafe) + // :: error: (argument.type.incompatible) :: warning: (cast.incomparable) requireSigned((@Unsigned int) s); requireSigned((int) s); requireSigned((@m int) s); @@ -43,14 +43,14 @@ void m() { requireUnsigned((@Unsigned int) 2); requireUnsigned((int) 2); requireUnsigned((@m int) 2); - // :: error: (argument.type.incompatible) :: warning: (cast.unsafe) + // :: error: (argument.type.incompatible) :: warning: (cast.incomparable) requireUnsigned((@Signed int) u); requireUnsigned((@Unsigned int) u); requireUnsigned((int) u); requireUnsigned((@m int) u); // :: error: (argument.type.incompatible) requireUnsigned((@Signed int) s); - // :: warning: (cast.unsafe) + // :: warning: (cast.incomparable) requireUnsigned((@Unsigned int) s); // :: error: (argument.type.incompatible) requireUnsigned((int) s); From 72e074e668627286f9acd82f0e66347691d55a54 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 24 Feb 2023 10:28:05 -0500 Subject: [PATCH 23/40] simplify branches --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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 77ab6261780..a4a6e824b47 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2658,12 +2658,10 @@ protected CastSafeKind isTypeCastSafe( castResult = isSafeDowncast(castType, exprType); if (castResult == CastSafeKind.NOT_DOWNCAST) { // fall to incomparable cast return isSafeIncomparableCast(castType, exprType); - } else { - return castResult; } - } else { return castResult; } + return castResult; } /** From 1cfd1050917f02842206dee6a5fc7bc2bc52ae4d Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 24 Feb 2023 13:42:39 -0500 Subject: [PATCH 24/40] update --- checker/tests/signedness/LiteralCast.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/checker/tests/signedness/LiteralCast.java b/checker/tests/signedness/LiteralCast.java index 7c8aa588ed5..c069536430a 100644 --- a/checker/tests/signedness/LiteralCast.java +++ b/checker/tests/signedness/LiteralCast.java @@ -24,7 +24,7 @@ void m() { requireSigned((@Unsigned int) 2); requireSigned((int) 2); requireSigned((@m int) 2); - // :: warning: (cast.incomparable) + // :: error: (cast.incomparable) requireSigned((@Signed int) u); // :: error: (argument.type.incompatible) requireSigned((@Unsigned int) u); @@ -33,7 +33,7 @@ void m() { // :: error: (argument.type.incompatible) requireSigned((@m int) u); requireSigned((@Signed int) s); - // :: error: (argument.type.incompatible) :: warning: (cast.incomparable) + // :: error: (argument.type.incompatible) :: error: (cast.incomparable) requireSigned((@Unsigned int) s); requireSigned((int) s); requireSigned((@m int) s); @@ -43,14 +43,14 @@ void m() { requireUnsigned((@Unsigned int) 2); requireUnsigned((int) 2); requireUnsigned((@m int) 2); - // :: error: (argument.type.incompatible) :: warning: (cast.incomparable) + // :: error: (argument.type.incompatible) :: error: (cast.incomparable) requireUnsigned((@Signed int) u); requireUnsigned((@Unsigned int) u); requireUnsigned((int) u); requireUnsigned((@m int) u); // :: error: (argument.type.incompatible) requireUnsigned((@Signed int) s); - // :: warning: (cast.incomparable) + // :: error: (cast.incomparable) requireUnsigned((@Unsigned int) s); // :: error: (argument.type.incompatible) requireUnsigned((int) s); From 7991a8bc453369fbbbdae0d4e37a7dcb7155f333 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Thu, 27 Apr 2023 10:49:38 -0400 Subject: [PATCH 25/40] merge with eisop master --- framework/tests/value/Issue2367.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/framework/tests/value/Issue2367.java b/framework/tests/value/Issue2367.java index 285d130bc35..ecbc03d2f95 100644 --- a/framework/tests/value/Issue2367.java +++ b/framework/tests/value/Issue2367.java @@ -23,12 +23,6 @@ public class Issue2367 { // Outside the signed byte range, but written as a hexadecimal literal. - // As a special case, the Constant Value Checker could not issue a warning when a value is - // within the signed byte range AND the value was specified in hexadecimal. - // Such a special case is not yet implemented, and I don't see how to do so. - // The program element "(byte) 0x8B" has already been converted to "(byte)139" by javac before - // the Checker Framework gets access to it. - // :: error: (cast.incomparable) byte b7 = (byte) 0x8B; // 0x8B == 137, and b4 == -117 } From fa1439ebee3e69e79b35e5d3ad95496bd31d337b Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 8 May 2023 14:16:26 -0400 Subject: [PATCH 26/40] merge code in valuevisitor --- .../common/basetype/messages.properties | 2 +- .../common/value/ValueVisitor.java | 37 ++++++++++++++----- framework/tests/value/Basics.java | 2 +- 3 files changed, 29 insertions(+), 12 deletions(-) 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 458a8081dbd..0eb6936c1c7 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -27,7 +27,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.incomparable=incomparable typecast from "%s" to "%s" +cast.incomparable=illegal 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/common/value/ValueVisitor.java b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java index c93c5213228..0ca0f5b747b 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java @@ -345,7 +345,8 @@ public Void visitTypeCast(TypeCastTree tree, Void p) { // This method returns true for (@IntVal(-1), @IntVal(255)) if the underlying type is `byte`, // but not for any other underlying type. @Override - protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected CastSafeKind isTypeCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { TypeKind castTypeKind = TypeKindUtils.primitiveOrBoxedToTypeKind(castType.getUnderlyingType()); TypeKind exprTypeKind = @@ -357,7 +358,7 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr AnnotationMirrorSet castAnnos = castType.getAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getAnnotations(); if (castAnnos.equals(exprAnnos)) { - return true; + return CastSafeKind.SAFE; } assert castAnnos.size() == 1; assert exprAnnos.size() == 1; @@ -372,13 +373,21 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr // Special-case singleton sets for speed. switch (castTypeKind) { case BYTE: - return castValues.get(0).byteValue() == exprValues.get(0).byteValue(); + return castValues.get(0).byteValue() == exprValues.get(0).byteValue() + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; case INT: - return castValues.get(0).intValue() == exprValues.get(0).intValue(); + return castValues.get(0).intValue() == exprValues.get(0).intValue() + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; case SHORT: - return castValues.get(0).shortValue() == exprValues.get(0).shortValue(); + return castValues.get(0).shortValue() == exprValues.get(0).shortValue() + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; default: - return castValues.get(0).longValue() == exprValues.get(0).longValue(); + return castValues.get(0).longValue() == exprValues.get(0).longValue() + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; } } else { switch (castTypeKind) { @@ -392,7 +401,9 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr new TreeSet( CollectionsPlume.mapList( Number::byteValue, exprValues)); - return sortedSetContainsAll(castValuesTree, exprValuesTree); + return sortedSetContainsAll(castValuesTree, exprValuesTree) + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; } case INT: { @@ -404,7 +415,9 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr new TreeSet( CollectionsPlume.mapList( Number::intValue, exprValues)); - return sortedSetContainsAll(castValuesTree, exprValuesTree); + return sortedSetContainsAll(castValuesTree, exprValuesTree) + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; } case SHORT: { @@ -416,13 +429,17 @@ protected boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirr new TreeSet( CollectionsPlume.mapList( Number::shortValue, exprValues)); - return sortedSetContainsAll(castValuesTree, exprValuesTree); + return sortedSetContainsAll(castValuesTree, exprValuesTree) + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; } default: { TreeSet castValuesTree = new TreeSet<>(castValues); TreeSet exprValuesTree = new TreeSet<>(exprValues); - return sortedSetContainsAll(castValuesTree, exprValuesTree); + return sortedSetContainsAll(castValuesTree, exprValuesTree) + ? CastSafeKind.SAFE + : CastSafeKind.ERROR; } } } diff --git a/framework/tests/value/Basics.java b/framework/tests/value/Basics.java index 868c0334d81..8b674e9bd9a 100644 --- a/framework/tests/value/Basics.java +++ b/framework/tests/value/Basics.java @@ -168,7 +168,7 @@ public void intCastTest(@IntVal({0, 1}) int input) { @IntVal({0, 1}) int c = (int) input; @IntVal({0, 1}) int ac = (@IntVal({0, 1}) int) input; @IntVal({0, 1, 2}) int sc = (@IntVal({0, 1, 2}) int) input; - // :: warning: (cast.unsafe) + // :: error: (cast.incomparable) @IntVal({1}) int uc = (@IntVal({1}) int) input; // :: error: (cast.incomparable) @IntVal({2}) int bc = (@IntVal({2}) int) input; From a15d72759858983ec296a32b90e5ae480a059619 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 3 Jul 2023 16:03:37 -0400 Subject: [PATCH 27/40] change name of the enum --- .../index/inequality/LessThanVisitor.java | 2 +- .../checker/interning/InterningVisitor.java | 4 +- .../checker/mustcall/MustCallVisitor.java | 4 +- .../checker/signedness/SignednessVisitor.java | 4 +- .../common/basetype/BaseTypeVisitor.java | 67 +++++++++---------- .../common/value/ValueVisitor.java | 36 +++++----- 6 files changed, 58 insertions(+), 59 deletions(-) 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 7bb11ef7719..a90fc478d69 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,7 @@ protected void commonAssignmentCheck( } @Override - protected CastSafeKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirror exprLTAnno = 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 ad62254107a..65c9920df41 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java @@ -978,10 +978,10 @@ DeclaredType typeToCheck() { } @Override - protected CastSafeKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (castType.getKind().isPrimitive()) { - return CastSafeKind.SAFE; + return TypecastKind.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 2b9613ce44c..82c1b948721 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -374,10 +374,10 @@ private boolean noMustCallObligation(AnnotatedTypeMirror atm) { } @Override - protected CastSafeKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (noMustCallObligation(castType) || noMustCallObligation(exprType)) { - return CastSafeKind.SAFE; + return TypecastKind.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 93d7c85c7b7..c8c0d295ced 100644 --- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java @@ -384,11 +384,11 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { } @Override - protected CastSafeKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (!atypeFactory.maybeIntegral(castType)) { // If the cast is not a number or a char, then it is legal. - return CastSafeKind.SAFE; + return TypecastKind.SAFE; } return super.isTypeCastSafe(castType, exprType); } 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 e73fd5c81ed..9499b77ce4d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2482,15 +2482,15 @@ 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 (!reported) { - CastSafeKind castResult = isTypeCastSafe(castType, exprType); + TypecastKind castResult = isTypeCastSafe(castType, exprType); - if (castResult == CastSafeKind.WARNING) { + if (castResult == TypecastKind.WARNING) { checker.reportWarning( typeCastTree, "cast.unsafe", exprType.toString(true), castType.toString(true)); - } else if (castResult == CastSafeKind.ERROR) { + } else if (castResult == TypecastKind.ERROR) { checker.reportError( typeCastTree, "cast.incomparable", @@ -2500,8 +2500,8 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } } - /** CastSafeKind */ - protected enum CastSafeKind { + /** To represent all possible kinds of typecast */ + protected enum TypecastKind { /** The cast is safe */ SAFE, /** The cast is illegal */ @@ -2522,9 +2522,9 @@ protected enum CastSafeKind { * * @param castType annotated type of the cast * @param exprType annotated type of the casted expression - * @return return NOT_UPCAST, WARNING or SAFE CastSafeKind. + * @return return NOT_UPCAST, WARNING or SAFE TypecastKind. */ - protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); AnnotationMirrorSet castAnnos; TypeKind castTypeKind = castType.getKind(); @@ -2546,13 +2546,13 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } if (!atypeFactory.getTypeHierarchy().isSubtype(newExprType, newCastType)) { - return CastSafeKind.WARNING; + return TypecastKind.WARNING; } if (newCastType.getKind() == TypeKind.ARRAY && newExprType.getKind() != TypeKind.ARRAY) { // Always warn if the cast contains an array, but the expression // doesn't, as in "(Object[]) o" where o is of type Object - return CastSafeKind.WARNING; + return TypecastKind.WARNING; } else if (newCastType.getKind() == TypeKind.DECLARED && newExprType.getKind() == TypeKind.DECLARED) { int castSize = ((AnnotatedDeclaredType) newCastType).getTypeArguments().size(); @@ -2562,7 +2562,7 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // Always warn if the cast and expression contain a different number of type // arguments, e.g. to catch a cast from "Object" to "List<@NonNull Object>". // TODO: the same number of arguments actually doesn't guarantee anything. - return CastSafeKind.WARNING; + return TypecastKind.WARNING; } } else if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { // If both the cast type and the casted expression are type variables, then check @@ -2579,7 +2579,7 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro && qualifierHierarchy.isSubtype( exprType.getEffectiveAnnotations(), castType.getEffectiveAnnotations()); - return result ? CastSafeKind.SAFE : CastSafeKind.WARNING; + return result ? TypecastKind.SAFE : TypecastKind.WARNING; } if (castTypeKind == TypeKind.TYPEVAR) { // If the cast type is a type var, but the expression is not, then check that the @@ -2615,9 +2615,9 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // return SAFE only it satisfies the below condition if (qualifierHierarchy.isSubtype(exprLower, castLower) && qualifierHierarchy.isSubtype(exprUpper, castUpper)) { - return CastSafeKind.SAFE; + return TypecastKind.SAFE; } - return CastSafeKind.WARNING; + return TypecastKind.WARNING; } } @@ -2626,12 +2626,12 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro qualifierHierarchy.isSubtype(exprTypeWidened.getEffectiveAnnotations(), castAnnos); if (result) { - return CastSafeKind.SAFE; + return TypecastKind.SAFE; } else if (checkCastElementType) { // when the flag is enabled, and it is not an upcast, return a warning - return CastSafeKind.WARNING; + return TypecastKind.WARNING; } else { - return CastSafeKind.NOT_UPCAST; + return TypecastKind.NOT_UPCAST; } } @@ -2643,14 +2643,14 @@ protected CastSafeKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro * @param exprType annotated type of the casted expression * @return Can return SAFE, NOT_DOWNCAST or WARNING. */ - protected CastSafeKind isSafeDowncast( + protected TypecastKind isSafeDowncast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirrorSet castAnnos = castType.getEffectiveAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { // exists an incomparable cast - return CastSafeKind.NOT_DOWNCAST; + return TypecastKind.NOT_DOWNCAST; } // check if the downcast can be statically verified @@ -2664,10 +2664,10 @@ protected CastSafeKind isSafeDowncast( atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { - return CastSafeKind.SAFE; + return TypecastKind.SAFE; } } - return CastSafeKind.WARNING; + return TypecastKind.WARNING; } /** @@ -2676,33 +2676,32 @@ protected CastSafeKind isSafeDowncast( * * @param castType annotated type of the cast * @param exprType annotated type of the casted expression - * @return CastSafeKind.ERROR if it's an incomparable cast. + * @return TypecastKind.ERROR if it's an incomparable cast. */ - protected CastSafeKind isSafeIncomparableCast( + protected TypecastKind isSafeIncomparableCast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - return CastSafeKind.ERROR; + return TypecastKind.ERROR; } /** - * This method returns CastSafeKind.SAFE when the typecast is an upcast or a statically - * verifiable downcast. Returns CastSafeKind.WARNING and ERROR for those downcasts which cannot - * be statically verified and all incomparable casts. + * This method returns TypecastKind.SAFE when the typecast is an upcast or a statically + * verifiable downcast. Returns TypecastKind.WARNING and ERROR for those downcasts which cannot + * be statically verified or some incomparable casts. * * @param castType annotated type of the cast * @param exprType annotated type of the casted expression - * @return CastSafeKind.SAFE if the type cast is safe, error or warning otherwise + * @return TypecastKind.SAFE if the typecast is safe, error or warning otherwise */ - protected CastSafeKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - CastSafeKind castResult = isUpcast(castType, exprType); + TypecastKind castResult = isUpcast(castType, exprType); // not upcast, do downcast and incomparable cast check - if (castResult == CastSafeKind.NOT_UPCAST) { + if (castResult == TypecastKind.NOT_UPCAST) { castResult = isSafeDowncast(castType, exprType); - if (castResult == CastSafeKind.NOT_DOWNCAST) { // fall to incomparable cast + if (castResult == TypecastKind.NOT_DOWNCAST) { // fall into incomparable cast return isSafeIncomparableCast(castType, exprType); } - return castResult; } return castResult; } @@ -2717,7 +2716,7 @@ protected CastSafeKind isTypeCastSafe( */ private boolean isInvariantTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, AnnotationMirror top) { - if (isTypeCastSafe(castType, exprType) != CastSafeKind.SAFE) { + if (isTypeCastSafe(castType, exprType) != TypecastKind.SAFE) { return false; } AnnotationMirror castTypeAnno = castType.getEffectiveAnnotationInHierarchy(top); @@ -2768,7 +2767,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) != CastSafeKind.SAFE) { + if (isTypeCastSafe(variableType, expType) != TypecastKind.SAFE) { checker.reportWarning(tree, "instanceof.pattern.unsafe", expType, variableTree); } } diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java index 0ca0f5b747b..01fae72496b 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java @@ -345,7 +345,7 @@ public Void visitTypeCast(TypeCastTree tree, Void p) { // This method returns true for (@IntVal(-1), @IntVal(255)) if the underlying type is `byte`, // but not for any other underlying type. @Override - protected CastSafeKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { TypeKind castTypeKind = TypeKindUtils.primitiveOrBoxedToTypeKind(castType.getUnderlyingType()); @@ -358,7 +358,7 @@ protected CastSafeKind isTypeCastSafe( AnnotationMirrorSet castAnnos = castType.getAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getAnnotations(); if (castAnnos.equals(exprAnnos)) { - return CastSafeKind.SAFE; + return TypecastKind.SAFE; } assert castAnnos.size() == 1; assert exprAnnos.size() == 1; @@ -374,20 +374,20 @@ protected CastSafeKind isTypeCastSafe( switch (castTypeKind) { case BYTE: return castValues.get(0).byteValue() == exprValues.get(0).byteValue() - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; case INT: return castValues.get(0).intValue() == exprValues.get(0).intValue() - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; case SHORT: return castValues.get(0).shortValue() == exprValues.get(0).shortValue() - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; default: return castValues.get(0).longValue() == exprValues.get(0).longValue() - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } } else { switch (castTypeKind) { @@ -402,8 +402,8 @@ protected CastSafeKind isTypeCastSafe( CollectionsPlume.mapList( Number::byteValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } case INT: { @@ -416,8 +416,8 @@ protected CastSafeKind isTypeCastSafe( CollectionsPlume.mapList( Number::intValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } case SHORT: { @@ -430,16 +430,16 @@ protected CastSafeKind isTypeCastSafe( CollectionsPlume.mapList( Number::shortValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } default: { TreeSet castValuesTree = new TreeSet<>(castValues); TreeSet exprValuesTree = new TreeSet<>(exprValues); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? CastSafeKind.SAFE - : CastSafeKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } } } From bfee4539dc24c37567de3d25c207de34c449375e Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 5 Jul 2023 11:25:53 -0400 Subject: [PATCH 28/40] remove daikon checkout id --- checker/bin-devel/test-daikon.sh | 2 -- 1 file changed, 2 deletions(-) diff --git a/checker/bin-devel/test-daikon.sh b/checker/bin-devel/test-daikon.sh index 92d31d06fab..d81f60e1a1f 100755 --- a/checker/bin-devel/test-daikon.sh +++ b/checker/bin-devel/test-daikon.sh @@ -14,8 +14,6 @@ source "$SCRIPTDIR"/build.sh # daikon-typecheck: 15 minutes "$SCRIPTDIR/.plume-scripts/git-clone-related" eisop-codespecs daikon -q --single-branch --depth 50 cd ../daikon -# Use a known-working commit ID. Update this in a separate PR to confirm all tests pass. -git checkout 8845c5b65f4a895c370418140dc78aa0bead1c57 git log | head -n 5 make compile if [ "$TRAVIS" = "true" ] ; then From 20d62afecc4605ae2e5922d4d8b0402ccd0e562d Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 5 Jul 2023 16:53:37 -0400 Subject: [PATCH 29/40] add daikon checkout back, as it is resolved by another pr --- checker/bin-devel/test-daikon.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/checker/bin-devel/test-daikon.sh b/checker/bin-devel/test-daikon.sh index d81f60e1a1f..92d31d06fab 100755 --- a/checker/bin-devel/test-daikon.sh +++ b/checker/bin-devel/test-daikon.sh @@ -14,6 +14,8 @@ source "$SCRIPTDIR"/build.sh # daikon-typecheck: 15 minutes "$SCRIPTDIR/.plume-scripts/git-clone-related" eisop-codespecs daikon -q --single-branch --depth 50 cd ../daikon +# Use a known-working commit ID. Update this in a separate PR to confirm all tests pass. +git checkout 8845c5b65f4a895c370418140dc78aa0bead1c57 git log | head -n 5 make compile if [ "$TRAVIS" = "true" ] ; then From 1ec438e851fd89542be1ea7ebc3e16751c199234 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Tue, 26 Sep 2023 22:49:20 -0400 Subject: [PATCH 30/40] add changelog entry --- docs/CHANGELOG.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index d762499be34..34fabdf4193 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -13,6 +13,10 @@ In this release, `nullness` continues to suppress warnings from the Initializati `nullnessnoinit` may be used to suppress warnings from the Nullness Checker only. A future release will make suppression behavior consistent with other checkers. +A new error message `cast.incomparable` will be raised if casting an expression to one target type which +does not share a subtype relationship with the expression type in the lattice. No longer issue errors +for statically verifiable downcast. + **Implementation details:** Deprecated `ObjectCreationNode#getConstructor` in favor of new `ObjectCreationNode#getTypeToInstantiate()`. @@ -26,9 +30,13 @@ Changed the return types of - `AnalysisResult#getFinalLocalValues()` to `Map`, and - `GenericAnnotatedTypeFactory#getFinalLocalValues()` to `Map`. +Refactored the implementation of `isTypeCastSafe` to categorize the kinds of a typecast, whether +it's an upcast, downcast or incomparable cast. Based on that, further determine if the typecast +is statically verifiable or not. + **Closed issues:** -eisop#297, eisop#376, eisop#532, typetools#1590. +eisop#155, eisop#297, eisop#376, eisop#532, typetools#1590. Version 3.34.0-eisop1 (May 9, 2023) From fc9ad98d57eefc492325c051b3132ffe2b7dc736 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 1 Oct 2023 20:47:43 -0400 Subject: [PATCH 31/40] Enum rename; Improve comments Co-authored-by: Werner Dietl --- .../index/inequality/LessThanVisitor.java | 2 +- .../checker/interning/InterningVisitor.java | 4 +- .../checker/mustcall/MustCallVisitor.java | 4 +- .../checker/signedness/SignednessVisitor.java | 4 +- checker/tests/signedness/CastFromTtoT.java | 2 +- docs/CHANGELOG.md | 2 +- .../common/basetype/BaseTypeVisitor.java | 62 +++++++++---------- .../common/value/ValueVisitor.java | 36 +++++------ .../javacutil/TypesUtils.java | 2 +- 9 files changed, 59 insertions(+), 59 deletions(-) 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 a90fc478d69..416fcb91caf 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,7 @@ protected void commonAssignmentCheck( } @Override - protected TypecastKind isTypeCastSafe( + protected TypeCastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirror exprLTAnno = 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 00dbcd90e71..5a2a59de9a4 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java @@ -980,10 +980,10 @@ DeclaredType typeToCheck() { } @Override - protected TypecastKind isTypeCastSafe( + protected TypeCastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (castType.getKind().isPrimitive()) { - return TypecastKind.SAFE; + return TypeCastKind.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 82c1b948721..9185dc5e9a7 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -374,10 +374,10 @@ private boolean noMustCallObligation(AnnotatedTypeMirror atm) { } @Override - protected TypecastKind isTypeCastSafe( + protected TypeCastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (noMustCallObligation(castType) || noMustCallObligation(exprType)) { - return TypecastKind.SAFE; + return TypeCastKind.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 c8c0d295ced..63f6b301920 100644 --- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java @@ -384,11 +384,11 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { } @Override - protected TypecastKind isTypeCastSafe( + protected TypeCastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (!atypeFactory.maybeIntegral(castType)) { // If the cast is not a number or a char, then it is legal. - return TypecastKind.SAFE; + return TypeCastKind.SAFE; } return super.isTypeCastSafe(castType, exprType); } diff --git a/checker/tests/signedness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java index cc999e8c574..bf421029c92 100644 --- a/checker/tests/signedness/CastFromTtoT.java +++ b/checker/tests/signedness/CastFromTtoT.java @@ -26,7 +26,7 @@ T bar2(@Signed T p) { } // Looks like an upcast, but it's a downcast. - // This time, as arugment p has type T, which is the same as the casting type + // This time, as argument p has type T, which is the same as the casting type // and the compiler will not issue a warning. So we should give a warning. void foo2(Inner<@SignednessGlb Integer> s, @Signed Integer local) { @SignednessGlb Integer x = s.bar2(local); diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index b493db5fcdd..dd1f3b78e61 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -41,7 +41,7 @@ Changed the return types of - `GenericAnnotatedTypeFactory#getFinalLocalValues()` to `Map`. Refactored the implementation of `isTypeCastSafe` to categorize the kinds of a typecast, whether -it's an upcast, downcast or incomparable cast. Based on that, further determine if the typecast +it is an upcast, downcast or incomparable cast. Based on that, further determine if the typecast is statically verifiable or not. **Closed issues:** 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 124591511eb..de2709dcea7 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2474,7 +2474,7 @@ 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 (!reported) { - TypecastKind castResult = isTypeCastSafe(castType, exprType); + TypeCastKind castResult = isTypeCastSafe(castType, exprType); if (castResult == TypecastKind.WARNING) { checker.reportWarning( @@ -2492,17 +2492,17 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } } - /** To represent all possible kinds of typecast */ - protected enum TypecastKind { - /** The cast is safe */ + /** Represents all possible kinds of typecasts. */ + protected enum TypeCastKind { + /** The cast is safe. */ SAFE, - /** The cast is illegal */ + /** The cast is illegal. */ ERROR, - /** Cannot statically verify the cast, report a warning */ + /** Cannot statically verify the cast, report a warning. */ WARNING, - /** It's not an upcast */ + /** It is not an upcast. */ NOT_UPCAST, - /** It's not a downcast */ + /** It is not a downcast. */ NOT_DOWNCAST } @@ -2516,7 +2516,7 @@ protected enum TypecastKind { * @param exprType annotated type of the casted expression * @return return NOT_UPCAST, WARNING or SAFE TypecastKind. */ - protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); AnnotationMirrorSet castAnnos; TypeKind castTypeKind = castType.getKind(); @@ -2538,13 +2538,13 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } if (!atypeFactory.getTypeHierarchy().isSubtype(newExprType, newCastType)) { - return TypecastKind.WARNING; + return TypeCastKind.WARNING; } if (newCastType.getKind() == TypeKind.ARRAY && newExprType.getKind() != TypeKind.ARRAY) { // Always warn if the cast contains an array, but the expression // doesn't, as in "(Object[]) o" where o is of type Object - return TypecastKind.WARNING; + return TypeCastKind.WARNING; } else if (newCastType.getKind() == TypeKind.DECLARED && newExprType.getKind() == TypeKind.DECLARED) { int castSize = ((AnnotatedDeclaredType) newCastType).getTypeArguments().size(); @@ -2554,7 +2554,7 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // Always warn if the cast and expression contain a different number of type // arguments, e.g. to catch a cast from "Object" to "List<@NonNull Object>". // TODO: the same number of arguments actually doesn't guarantee anything. - return TypecastKind.WARNING; + return TypeCastKind.WARNING; } } else if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { // If both the cast type and the casted expression are type variables, then check @@ -2571,7 +2571,7 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro && qualifierHierarchy.isSubtype( exprType.getEffectiveAnnotations(), castType.getEffectiveAnnotations()); - return result ? TypecastKind.SAFE : TypecastKind.WARNING; + return result ? TypeCastKind.SAFE : TypeCastKind.WARNING; } if (castTypeKind == TypeKind.TYPEVAR) { // If the cast type is a type var, but the expression is not, then check that the @@ -2607,9 +2607,9 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // return SAFE only it satisfies the below condition if (qualifierHierarchy.isSubtype(exprLower, castLower) && qualifierHierarchy.isSubtype(exprUpper, castUpper)) { - return TypecastKind.SAFE; + return TypeCastKind.SAFE; } - return TypecastKind.WARNING; + return TypeCastKind.WARNING; } } @@ -2618,12 +2618,12 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro qualifierHierarchy.isSubtype(exprTypeWidened.getEffectiveAnnotations(), castAnnos); if (result) { - return TypecastKind.SAFE; + return TypeCastKind.SAFE; } else if (checkCastElementType) { // when the flag is enabled, and it is not an upcast, return a warning - return TypecastKind.WARNING; + return TypeCastKind.WARNING; } else { - return TypecastKind.NOT_UPCAST; + return TypeCastKind.NOT_UPCAST; } } @@ -2635,14 +2635,14 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro * @param exprType annotated type of the casted expression * @return Can return SAFE, NOT_DOWNCAST or WARNING. */ - protected TypecastKind isSafeDowncast( + protected TypeCastKind isSafeDowncast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirrorSet castAnnos = castType.getEffectiveAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { // exists an incomparable cast - return TypecastKind.NOT_DOWNCAST; + return TypeCastKind.NOT_DOWNCAST; } // check if the downcast can be statically verified @@ -2656,14 +2656,14 @@ protected TypecastKind isSafeDowncast( atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { - return TypecastKind.SAFE; + return TypeCastKind.SAFE; } } - return TypecastKind.WARNING; + return TypeCastKind.WARNING; } /** - * If it's an incomparable cast in terms of qualifiers, return ERROR by default. Subchecker can + * If it is an incomparable cast in terms of qualifiers, return ERROR by default. Subchecker can * override this method to allow certain incomparable casts. * * @param castType annotated type of the cast @@ -2672,11 +2672,11 @@ protected TypecastKind isSafeDowncast( */ protected TypecastKind isSafeIncomparableCast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - return TypecastKind.ERROR; + return TypeCastKind.ERROR; } /** - * This method returns TypecastKind.SAFE when the typecast is an upcast or a statically + * This method returns TypeCastKind.SAFE when the typecast is an upcast or a statically * verifiable downcast. Returns TypecastKind.WARNING and ERROR for those downcasts which cannot * be statically verified or some incomparable casts. * @@ -2684,14 +2684,14 @@ protected TypecastKind isSafeIncomparableCast( * @param exprType annotated type of the casted expression * @return TypecastKind.SAFE if the typecast is safe, error or warning otherwise */ - protected TypecastKind isTypeCastSafe( + protected TypeCastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - TypecastKind castResult = isUpcast(castType, exprType); + TypeCastKind castResult = isUpcast(castType, exprType); // not upcast, do downcast and incomparable cast check - if (castResult == TypecastKind.NOT_UPCAST) { + if (castResult == TypeCastKind.NOT_UPCAST) { castResult = isSafeDowncast(castType, exprType); - if (castResult == TypecastKind.NOT_DOWNCAST) { // fall into incomparable cast + if (castResult == TypeCastKind.NOT_DOWNCAST) { // fall into incomparable cast return isSafeIncomparableCast(castType, exprType); } } @@ -2708,7 +2708,7 @@ protected TypecastKind isTypeCastSafe( */ private boolean isInvariantTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, AnnotationMirror top) { - if (isTypeCastSafe(castType, exprType) != TypecastKind.SAFE) { + if (isTypeCastSafe(castType, exprType) != TypeCastKind.SAFE) { return false; } AnnotationMirror castTypeAnno = castType.getEffectiveAnnotationInHierarchy(top); @@ -2759,7 +2759,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) != TypecastKind.SAFE) { + if (isTypeCastSafe(variableType, expType) != TypeCastKind.SAFE) { checker.reportWarning(tree, "instanceof.pattern.unsafe", expType, variableTree); } } diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java index 01fae72496b..ae83aab4f54 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java @@ -345,7 +345,7 @@ public Void visitTypeCast(TypeCastTree tree, Void p) { // This method returns true for (@IntVal(-1), @IntVal(255)) if the underlying type is `byte`, // but not for any other underlying type. @Override - protected TypecastKind isTypeCastSafe( + protected TypeCastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { TypeKind castTypeKind = TypeKindUtils.primitiveOrBoxedToTypeKind(castType.getUnderlyingType()); @@ -358,7 +358,7 @@ protected TypecastKind isTypeCastSafe( AnnotationMirrorSet castAnnos = castType.getAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getAnnotations(); if (castAnnos.equals(exprAnnos)) { - return TypecastKind.SAFE; + return TypeCastKind.SAFE; } assert castAnnos.size() == 1; assert exprAnnos.size() == 1; @@ -374,20 +374,20 @@ protected TypecastKind isTypeCastSafe( switch (castTypeKind) { case BYTE: return castValues.get(0).byteValue() == exprValues.get(0).byteValue() - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; case INT: return castValues.get(0).intValue() == exprValues.get(0).intValue() - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; case SHORT: return castValues.get(0).shortValue() == exprValues.get(0).shortValue() - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; default: return castValues.get(0).longValue() == exprValues.get(0).longValue() - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; } } else { switch (castTypeKind) { @@ -402,8 +402,8 @@ protected TypecastKind isTypeCastSafe( CollectionsPlume.mapList( Number::byteValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; } case INT: { @@ -416,8 +416,8 @@ protected TypecastKind isTypeCastSafe( CollectionsPlume.mapList( Number::intValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; } case SHORT: { @@ -430,16 +430,16 @@ protected TypecastKind isTypeCastSafe( CollectionsPlume.mapList( Number::shortValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; } default: { TreeSet castValuesTree = new TreeSet<>(castValues); TreeSet exprValuesTree = new TreeSet<>(exprValues); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypecastKind.SAFE - : TypecastKind.ERROR; + ? TypeCastKind.SAFE + : TypeCastKind.ERROR; } } } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index 6f3a03eaf4d..b9f215de25a 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -297,7 +297,7 @@ public static boolean areSamePrimitiveTypes(TypeMirror left, TypeMirror right) { } /** - * Returns true iff the arguments are both the same type variables. + * Returns true iff the arguments are both the same type variable. * * @param v1 a type variable * @param v2 a type variable From d06ad1fe10c3bb2890d185e2128d2578fc367125 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 1 Oct 2023 21:53:29 -0400 Subject: [PATCH 32/40] rename enum and improve comments in the test file CastFromTtoT.java --- .../index/inequality/LessThanVisitor.java | 2 +- .../checker/interning/InterningVisitor.java | 4 +- .../checker/mustcall/MustCallVisitor.java | 4 +- .../checker/signedness/SignednessVisitor.java | 4 +- checker/tests/signedness/CastFromTtoT.java | 22 +++++---- docs/CHANGELOG.md | 2 +- .../common/basetype/BaseTypeVisitor.java | 48 +++++++++---------- .../common/value/ValueVisitor.java | 36 +++++++------- 8 files changed, 64 insertions(+), 58 deletions(-) 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 416fcb91caf..a90fc478d69 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,7 @@ protected void commonAssignmentCheck( } @Override - protected TypeCastKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirror exprLTAnno = 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 5a2a59de9a4..00dbcd90e71 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java @@ -980,10 +980,10 @@ DeclaredType typeToCheck() { } @Override - protected TypeCastKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (castType.getKind().isPrimitive()) { - return TypeCastKind.SAFE; + return TypecastKind.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 9185dc5e9a7..82c1b948721 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -374,10 +374,10 @@ private boolean noMustCallObligation(AnnotatedTypeMirror atm) { } @Override - protected TypeCastKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (noMustCallObligation(castType) || noMustCallObligation(exprType)) { - return TypeCastKind.SAFE; + return TypecastKind.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 63f6b301920..c8c0d295ced 100644 --- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java @@ -384,11 +384,11 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { } @Override - protected TypeCastKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { if (!atypeFactory.maybeIntegral(castType)) { // If the cast is not a number or a char, then it is legal. - return TypeCastKind.SAFE; + return TypecastKind.SAFE; } return super.isTypeCastSafe(castType, exprType); } diff --git a/checker/tests/signedness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java index bf421029c92..b013d006f06 100644 --- a/checker/tests/signedness/CastFromTtoT.java +++ b/checker/tests/signedness/CastFromTtoT.java @@ -5,30 +5,36 @@ class CastFromTtoT { @SuppressWarnings("unchecked") T bar(@UnknownSignedness Object p) { + // Seems to have no cast in terms of the qualifier (from @UnknownSignedness to + // @UnknownSignedness), but in instantiation, it could be a downcast. + // See method foo below. It's okay not to report downcast warnings as Javac will warn about + // casting object to 'T' (unchecked warning) T x = (T) p; return x; } - // Seems to have no cast, but in the instantiation, it's a downcast. - // if we use getEffectiveAnnotations, we'll see it as no cast (qualifier aspect) - // But it's fine, as compiler will warn about casting object to 'T' [unchecked warning] void foo(CastFromTtoT<@Signed Integer> s, @UnknownSignedness Object local) { + // Here, we passed in an @UnknownSignedness object and the method signature after + // substitution is @Signed Integer bar(@UnknownSignedness Object). This makes the typecast + // discussed earlier a downcast. @Signed Integer x = s.bar(local); } class Inner { T bar2(@Signed T p) { - // without a warning from the compiler. The T in the casting expression may have - // different signedness annotation with the arugment p. + // The casting expression below looks like an upcast (in terms of the qualifier), + // but it could be a downcast in invocation (See method foo2 below for an example). + // We should report downcast warning if there is one because + // Javac doesn't warn when casting a variable from type T to T. // :: warning: (cast.unsafe) T x = (T) p; return x; } - // Looks like an upcast, but it's a downcast. - // This time, as argument p has type T, which is the same as the casting type - // and the compiler will not issue a warning. So we should give a warning. void foo2(Inner<@SignednessGlb Integer> s, @Signed Integer local) { + // Here, we passed in an @Signed integer and the method signature after + // substitution is @SignednessGlb Integer bar2(@Signed Object). This makes the typecast + // discussed in method bar2 a downcast. @SignednessGlb Integer x = s.bar2(local); } } diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index dd1f3b78e61..157510fcb0d 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -19,7 +19,7 @@ Fixed a bug in the Nullness Checker where an instance receiver is incorrectly ma a static method or field access. This could lead to new nullness errors. The static access should be changed to be through a class name. -A new error message `cast.incomparable` will be raised if casting an expression to one target type which +A new error message `cast.incomparable` will be raised if casting an expression to a target type which does not share a subtype relationship with the expression type in the lattice. No longer issue errors for statically verifiable downcast. 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 de2709dcea7..71d281c0d9c 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2474,7 +2474,7 @@ 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 (!reported) { - TypeCastKind castResult = isTypeCastSafe(castType, exprType); + TypecastKind castResult = isTypeCastSafe(castType, exprType); if (castResult == TypecastKind.WARNING) { checker.reportWarning( @@ -2493,7 +2493,7 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } /** Represents all possible kinds of typecasts. */ - protected enum TypeCastKind { + protected enum TypecastKind { /** The cast is safe. */ SAFE, /** The cast is illegal. */ @@ -2516,7 +2516,7 @@ protected enum TypeCastKind { * @param exprType annotated type of the casted expression * @return return NOT_UPCAST, WARNING or SAFE TypecastKind. */ - protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); AnnotationMirrorSet castAnnos; TypeKind castTypeKind = castType.getKind(); @@ -2538,13 +2538,13 @@ protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro } if (!atypeFactory.getTypeHierarchy().isSubtype(newExprType, newCastType)) { - return TypeCastKind.WARNING; + return TypecastKind.WARNING; } if (newCastType.getKind() == TypeKind.ARRAY && newExprType.getKind() != TypeKind.ARRAY) { // Always warn if the cast contains an array, but the expression // doesn't, as in "(Object[]) o" where o is of type Object - return TypeCastKind.WARNING; + return TypecastKind.WARNING; } else if (newCastType.getKind() == TypeKind.DECLARED && newExprType.getKind() == TypeKind.DECLARED) { int castSize = ((AnnotatedDeclaredType) newCastType).getTypeArguments().size(); @@ -2554,7 +2554,7 @@ protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // Always warn if the cast and expression contain a different number of type // arguments, e.g. to catch a cast from "Object" to "List<@NonNull Object>". // TODO: the same number of arguments actually doesn't guarantee anything. - return TypeCastKind.WARNING; + return TypecastKind.WARNING; } } else if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { // If both the cast type and the casted expression are type variables, then check @@ -2571,7 +2571,7 @@ protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro && qualifierHierarchy.isSubtype( exprType.getEffectiveAnnotations(), castType.getEffectiveAnnotations()); - return result ? TypeCastKind.SAFE : TypeCastKind.WARNING; + return result ? TypecastKind.SAFE : TypecastKind.WARNING; } if (castTypeKind == TypeKind.TYPEVAR) { // If the cast type is a type var, but the expression is not, then check that the @@ -2607,9 +2607,9 @@ protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // return SAFE only it satisfies the below condition if (qualifierHierarchy.isSubtype(exprLower, castLower) && qualifierHierarchy.isSubtype(exprUpper, castUpper)) { - return TypeCastKind.SAFE; + return TypecastKind.SAFE; } - return TypeCastKind.WARNING; + return TypecastKind.WARNING; } } @@ -2618,12 +2618,12 @@ protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro qualifierHierarchy.isSubtype(exprTypeWidened.getEffectiveAnnotations(), castAnnos); if (result) { - return TypeCastKind.SAFE; + return TypecastKind.SAFE; } else if (checkCastElementType) { // when the flag is enabled, and it is not an upcast, return a warning - return TypeCastKind.WARNING; + return TypecastKind.WARNING; } else { - return TypeCastKind.NOT_UPCAST; + return TypecastKind.NOT_UPCAST; } } @@ -2635,14 +2635,14 @@ protected TypeCastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro * @param exprType annotated type of the casted expression * @return Can return SAFE, NOT_DOWNCAST or WARNING. */ - protected TypeCastKind isSafeDowncast( + protected TypecastKind isSafeDowncast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { AnnotationMirrorSet castAnnos = castType.getEffectiveAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { // exists an incomparable cast - return TypeCastKind.NOT_DOWNCAST; + return TypecastKind.NOT_DOWNCAST; } // check if the downcast can be statically verified @@ -2656,10 +2656,10 @@ protected TypeCastKind isSafeDowncast( atypeFactory.getTypeDeclarationBounds(castDeclared.getUnderlyingType()); if (AnnotationUtils.areSame(castDeclared.getAnnotations(), bounds)) { - return TypeCastKind.SAFE; + return TypecastKind.SAFE; } } - return TypeCastKind.WARNING; + return TypecastKind.WARNING; } /** @@ -2672,11 +2672,11 @@ protected TypeCastKind isSafeDowncast( */ protected TypecastKind isSafeIncomparableCast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - return TypeCastKind.ERROR; + return TypecastKind.ERROR; } /** - * This method returns TypeCastKind.SAFE when the typecast is an upcast or a statically + * This method returns TypecastKind.SAFE when the typecast is an upcast or a statically * verifiable downcast. Returns TypecastKind.WARNING and ERROR for those downcasts which cannot * be statically verified or some incomparable casts. * @@ -2684,14 +2684,14 @@ protected TypecastKind isSafeIncomparableCast( * @param exprType annotated type of the casted expression * @return TypecastKind.SAFE if the typecast is safe, error or warning otherwise */ - protected TypeCastKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - TypeCastKind castResult = isUpcast(castType, exprType); + TypecastKind castResult = isUpcast(castType, exprType); // not upcast, do downcast and incomparable cast check - if (castResult == TypeCastKind.NOT_UPCAST) { + if (castResult == TypecastKind.NOT_UPCAST) { castResult = isSafeDowncast(castType, exprType); - if (castResult == TypeCastKind.NOT_DOWNCAST) { // fall into incomparable cast + if (castResult == TypecastKind.NOT_DOWNCAST) { // fall into incomparable cast return isSafeIncomparableCast(castType, exprType); } } @@ -2708,7 +2708,7 @@ protected TypeCastKind isTypeCastSafe( */ private boolean isInvariantTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, AnnotationMirror top) { - if (isTypeCastSafe(castType, exprType) != TypeCastKind.SAFE) { + if (isTypeCastSafe(castType, exprType) != TypecastKind.SAFE) { return false; } AnnotationMirror castTypeAnno = castType.getEffectiveAnnotationInHierarchy(top); @@ -2759,7 +2759,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) != TypeCastKind.SAFE) { + if (isTypeCastSafe(variableType, expType) != TypecastKind.SAFE) { checker.reportWarning(tree, "instanceof.pattern.unsafe", expType, variableTree); } } diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java index ae83aab4f54..01fae72496b 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueVisitor.java @@ -345,7 +345,7 @@ public Void visitTypeCast(TypeCastTree tree, Void p) { // This method returns true for (@IntVal(-1), @IntVal(255)) if the underlying type is `byte`, // but not for any other underlying type. @Override - protected TypeCastKind isTypeCastSafe( + protected TypecastKind isTypeCastSafe( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { TypeKind castTypeKind = TypeKindUtils.primitiveOrBoxedToTypeKind(castType.getUnderlyingType()); @@ -358,7 +358,7 @@ protected TypeCastKind isTypeCastSafe( AnnotationMirrorSet castAnnos = castType.getAnnotations(); AnnotationMirrorSet exprAnnos = exprType.getAnnotations(); if (castAnnos.equals(exprAnnos)) { - return TypeCastKind.SAFE; + return TypecastKind.SAFE; } assert castAnnos.size() == 1; assert exprAnnos.size() == 1; @@ -374,20 +374,20 @@ protected TypeCastKind isTypeCastSafe( switch (castTypeKind) { case BYTE: return castValues.get(0).byteValue() == exprValues.get(0).byteValue() - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; case INT: return castValues.get(0).intValue() == exprValues.get(0).intValue() - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; case SHORT: return castValues.get(0).shortValue() == exprValues.get(0).shortValue() - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; default: return castValues.get(0).longValue() == exprValues.get(0).longValue() - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } } else { switch (castTypeKind) { @@ -402,8 +402,8 @@ protected TypeCastKind isTypeCastSafe( CollectionsPlume.mapList( Number::byteValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } case INT: { @@ -416,8 +416,8 @@ protected TypeCastKind isTypeCastSafe( CollectionsPlume.mapList( Number::intValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } case SHORT: { @@ -430,16 +430,16 @@ protected TypeCastKind isTypeCastSafe( CollectionsPlume.mapList( Number::shortValue, exprValues)); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } default: { TreeSet castValuesTree = new TreeSet<>(castValues); TreeSet exprValuesTree = new TreeSet<>(exprValues); return sortedSetContainsAll(castValuesTree, exprValuesTree) - ? TypeCastKind.SAFE - : TypeCastKind.ERROR; + ? TypecastKind.SAFE + : TypecastKind.ERROR; } } } From f4ffe0760b76e190db05cfe868283c2e454ef8a3 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 2 Oct 2023 10:33:15 -0400 Subject: [PATCH 33/40] improve jovadoc --- .../checkerframework/common/basetype/BaseTypeVisitor.java | 8 ++++---- .../java/org/checkerframework/javacutil/TypesUtils.java | 7 +++++-- 2 files changed, 9 insertions(+), 6 deletions(-) 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 71d281c0d9c..cae4eeccdd2 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2588,7 +2588,7 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro // As the compiler will not report the unchecked warning in this case, so we should // do the check for our type system when the subtype relation of the instantiations of the // two T cannot be statically verified. - // See CastFromTtoT.java:22 for an example. + // See CastFromTtoT.java for an example. if (castTypeKind == TypeKind.TYPEVAR && exprType.getKind() == TypeKind.TYPEVAR) { TypeVariable castTV = (TypeVariable) castType.getUnderlyingType(); TypeVariable exprTV = (TypeVariable) exprType.getUnderlyingType(); @@ -2663,12 +2663,12 @@ protected TypecastKind isSafeDowncast( } /** - * If it is an incomparable cast in terms of qualifiers, return ERROR by default. Subchecker can - * override this method to allow certain incomparable casts. + * If it is an incomparable cast in terms of qualifiers, return ERROR. Subchecker can override + * this method to allow certain incomparable casts and can return SAFE, WARNING or ERROR. * * @param castType annotated type of the cast * @param exprType annotated type of the casted expression - * @return TypecastKind.ERROR if it's an incomparable cast. + * @return TypecastKind.ERROR. */ protected TypecastKind isSafeIncomparableCast( AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index b9f215de25a..c7fa1312b66 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -278,7 +278,7 @@ public static boolean areSameDeclaredTypes(Type.ClassType t1, Type.ClassType t2) if (t1.tsym.name != t2.tsym.name) { return false; } - return t1.toString().equals(t1.toString()); + return t1.toString().equals(t2.toString()); } /** @@ -297,7 +297,10 @@ public static boolean areSamePrimitiveTypes(TypeMirror left, TypeMirror right) { } /** - * Returns true iff the arguments are both the same type variable. + * Returns true iff the arguments are type variables with the same name. This method doesn't + * distinguish the difference of type variables having the same name but declared in different + * contexts, so we should be careful using it. Javac is able to identify the difference and + * issue an unchecked warning for the above scenario. * * @param v1 a type variable * @param v2 a type variable From ac60c2e3176358b732c2a37bbf173cbe77757738 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Tue, 3 Oct 2023 09:43:37 -0400 Subject: [PATCH 34/40] move isTypeCastSafe to an earlier position --- .../common/basetype/BaseTypeVisitor.java | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) 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 cae4eeccdd2..96dddc9feed 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2492,6 +2492,29 @@ protected void checkTypecastSafety(TypeCastTree typeCastTree) { } } + /** + * This method returns TypecastKind.SAFE when the typecast is an upcast or a statically + * verifiable downcast. Returns TypecastKind.WARNING and ERROR for those downcasts which cannot + * be statically verified or some incomparable casts. + * + * @param castType annotated type of the cast + * @param exprType annotated type of the casted expression + * @return TypecastKind.SAFE if the typecast is safe, error or warning otherwise + */ + protected TypecastKind isTypeCastSafe( + AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { + TypecastKind castResult = isUpcast(castType, exprType); + + // not upcast, do downcast and incomparable cast check + if (castResult == TypecastKind.NOT_UPCAST) { + castResult = isSafeDowncast(castType, exprType); + if (castResult == TypecastKind.NOT_DOWNCAST) { // fall into incomparable cast + return isSafeIncomparableCast(castType, exprType); + } + } + return castResult; + } + /** Represents all possible kinds of typecasts. */ protected enum TypecastKind { /** The cast is safe. */ @@ -2675,29 +2698,6 @@ protected TypecastKind isSafeIncomparableCast( return TypecastKind.ERROR; } - /** - * This method returns TypecastKind.SAFE when the typecast is an upcast or a statically - * verifiable downcast. Returns TypecastKind.WARNING and ERROR for those downcasts which cannot - * be statically verified or some incomparable casts. - * - * @param castType annotated type of the cast - * @param exprType annotated type of the casted expression - * @return TypecastKind.SAFE if the typecast is safe, error or warning otherwise - */ - protected TypecastKind isTypeCastSafe( - AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType) { - TypecastKind castResult = isUpcast(castType, exprType); - - // not upcast, do downcast and incomparable cast check - if (castResult == TypecastKind.NOT_UPCAST) { - castResult = isSafeDowncast(castType, exprType); - if (castResult == TypecastKind.NOT_DOWNCAST) { // fall into incomparable cast - return isSafeIncomparableCast(castType, exprType); - } - } - return castResult; - } - /** * Return whether or not casting the exprType to castType is legal. * From 67ba76bbb77228288410c3ab6b29ab59d067b008 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 19 Nov 2023 21:18:37 -0500 Subject: [PATCH 35/40] use new apis for the change --- .../common/basetype/BaseTypeVisitor.java | 11 +++++++--- .../framework/type/QualifierHierarchy.java | 20 +++++++++++++++++++ 2 files changed, 28 insertions(+), 3 deletions(-) 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 c32619bc8c8..7022a7c2d85 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2810,8 +2810,9 @@ protected TypecastKind isUpcast(AnnotatedTypeMirror castType, AnnotatedTypeMirro AnnotatedTypes.findEffectiveAnnotations(qualifierHierarchy, exprType); // return SAFE only it satisfies the below condition - if (qualifierHierarchy.isSubtype(exprLower, castLower) - && qualifierHierarchy.isSubtype(exprUpper, castUpper)) { + if (qualifierHierarchy.isSubtypeShallow(exprLower, exprTV, castLower, castTV) + && qualifierHierarchy.isSubtypeShallow( + exprUpper, exprTV, castUpper, castTV)) { return TypecastKind.SAFE; } return TypecastKind.WARNING; @@ -2849,7 +2850,11 @@ protected TypecastKind isSafeDowncast( AnnotationMirrorSet exprAnnos = exprType.getEffectiveAnnotations(); QualifierHierarchy qualifierHierarchy = atypeFactory.getQualifierHierarchy(); - if (!qualifierHierarchy.isComparable(castAnnos, exprAnnos)) { // exists an incomparable cast + if (!qualifierHierarchy.isComparable( + castAnnos, + castType.getUnderlyingType(), + exprAnnos, + exprType.getUnderlyingType())) { // exists an incomparable cast return TypecastKind.NOT_DOWNCAST; } 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 5975aa41a71..39cbace799d 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java +++ b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java @@ -279,6 +279,26 @@ public final boolean isSubtypeShallow( return isSubtypeShallow(subQualifiers, typeMirror, superQualifiers, typeMirror); } + /** + * 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 type1 the type associated with {@code qualifiers1} + * @param qualifiers2 set of qualifiers; exactly one per hierarchy + * @param type2 the type associated with {@code qualifiers2} + * @return true iff all qualifiers in {@code qualifiers1} are comparable with qualifiers in + * {@code qualifiers2} + */ + public boolean isComparable( + Collection qualifiers1, + TypeMirror type1, + Collection qualifiers2, + TypeMirror type2) { + return isSubtypeShallow(qualifiers1, type1, qualifiers2, type2) + || isSubtypeShallow(qualifiers2, type2, qualifiers1, type1); + } + /** * 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 From 0b785876430fe81ab9ba698b79812547bb774d05 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 19 Nov 2023 23:39:20 -0500 Subject: [PATCH 36/40] fix error messages on the test files --- checker/tests/initialization/CastInit.java | 2 +- checker/tests/signedness/CharToFloat.java | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/checker/tests/initialization/CastInit.java b/checker/tests/initialization/CastInit.java index 631b7da1bc4..dd4045c5a3f 100644 --- a/checker/tests/initialization/CastInit.java +++ b/checker/tests/initialization/CastInit.java @@ -5,7 +5,7 @@ public class CastInit { public CastInit() { @UnknownInitialization CastInit t1 = (@UnknownInitialization CastInit) this; - // :: warning: (cast.unsafe) + // :: warning: (cast.incomparable) @Initialized CastInit t2 = (@Initialized CastInit) this; } } diff --git a/checker/tests/signedness/CharToFloat.java b/checker/tests/signedness/CharToFloat.java index 7d67711db12..1caaea9f8f0 100644 --- a/checker/tests/signedness/CharToFloat.java +++ b/checker/tests/signedness/CharToFloat.java @@ -2,9 +2,7 @@ public class CharToFloat { void castCharacter(Object o) { - // :: error: (cast.incomparable) floatParameter((Character) o); - // :: error: (cast.incomparable) doubleParameter((Character) o); } From 1b8f4ab36c1c70ce1832a7b2011cd7d829daee8a Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 20 Nov 2023 09:30:07 -0500 Subject: [PATCH 37/40] fix error messages on the test files --- checker/tests/initialization/CastInit.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/tests/initialization/CastInit.java b/checker/tests/initialization/CastInit.java index dd4045c5a3f..2f0040fac05 100644 --- a/checker/tests/initialization/CastInit.java +++ b/checker/tests/initialization/CastInit.java @@ -5,7 +5,7 @@ public class CastInit { public CastInit() { @UnknownInitialization CastInit t1 = (@UnknownInitialization CastInit) this; - // :: warning: (cast.incomparable) + // :: error: (cast.incomparable) @Initialized CastInit t2 = (@Initialized CastInit) this; } } From 1b205460174d1a6342cdcb6008202209733edaf2 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Tue, 21 Nov 2023 23:31:47 -0500 Subject: [PATCH 38/40] improve document --- docs/CHANGELOG.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 82928fe27d0..524e31a5392 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,9 +3,8 @@ Version 3.39.0-eisop2 (October ??, 2023) **User-visible changes:** -A new error message `cast.incomparable` will be raised if casting an expression to a target type which -does not share a subtype relationship with the expression type in the lattice. No longer issue errors -for statically verifiable downcast. +A new error message `cast.incomparable` will be raised if the target type qualifier is neither the subtype +nor the supertype of the expression type qualifier. No longer issue errors for statically verifiable downcast. **Implementation details:** From 96ec55e7828cb12c7aa8170b5bfdf4c83b136d91 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 5 Jan 2025 12:04:20 -0500 Subject: [PATCH 39/40] Clean up --- checker/tests/signedness/CastFromTtoT.java | 6 +++--- docs/CHANGELOG.md | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/checker/tests/signedness/CastFromTtoT.java b/checker/tests/signedness/CastFromTtoT.java index b013d006f06..45f535c9846 100644 --- a/checker/tests/signedness/CastFromTtoT.java +++ b/checker/tests/signedness/CastFromTtoT.java @@ -1,6 +1,6 @@ -import org.checkerframework.checker.signedness.qual.*; - -import java.util.*; +import org.checkerframework.checker.signedness.qual.Signed; +import org.checkerframework.checker.signedness.qual.SignednessGlb; +import org.checkerframework.checker.signedness.qual.UnknownSignedness; class CastFromTtoT { @SuppressWarnings("unchecked") diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index cd08ed5eef5..c3268e96fe4 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -14,7 +14,7 @@ is statically verifiable or not. **Closed issues:** -eisop#1033. +eisop#155, eisop#1033. Version 3.42.0-eisop5 (December 20, 2024) @@ -193,7 +193,7 @@ is an enhanced switch statement. **Closed issues:** -eisop#155, eisop#609, eisop#610, eisop#612. +eisop#609, eisop#610, eisop#612. Version 3.40.0 (November 1, 2023) --------------------------------- From 875a09999d8ca6e895db0e3a54806839e1c7811f Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 5 Jan 2025 18:19:12 -0500 Subject: [PATCH 40/40] Empty commit for CI