From bb3094a05d2ed55ef5102ed24d16d85fde522113 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 12 Oct 2024 14:11:23 -0700 Subject: [PATCH 1/3] Support DefaultQualifiers that do not apply to subpackages (#149) Co-authored-by: Chris Povirk Co-authored-by: Werner Dietl --- .../framework/qual/DefaultQualifier.java | 10 ++ .../UpperBoundAnnotatedTypeFactory.java | 3 +- .../checker/mustcall/MustCallVisitor.java | 3 +- .../cfg/builder/CFGTranslationPhaseOne.java | 3 +- docs/CHANGELOG.md | 4 + .../framework/source/SourceChecker.java | 3 +- .../framework/type/AnnotatedTypeFactory.java | 18 +- .../framework/util/AnnotatedTypes.java | 3 +- .../framework/util/defaults/Default.java | 32 +++- .../util/defaults/QualifierDefaults.java | 166 +++++++++++++----- .../InvocationTypeInference.java | 6 +- .../typeinference8/constraint/Typing.java | 3 +- .../h1h2checker/pkg1/PackageDefaulting.java | 23 +++ .../tests/h1h2checker/pkg1/package-info.java | 14 ++ .../pkg1/pkg2/PackageDefaulting.java | 22 +++ 15 files changed, 248 insertions(+), 65 deletions(-) create mode 100644 framework/tests/h1h2checker/pkg1/PackageDefaulting.java create mode 100644 framework/tests/h1h2checker/pkg1/package-info.java create mode 100644 framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java index ef783ca9a85..9664fc2c38a 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java @@ -26,6 +26,9 @@ *   class MyClass { ... } * * + *

Defaults on a package also apply to subpackages, unless the {@code applyToSubpackages} field + * is set to false. + * *

This annotation currently has no effect in stub files. * * @see org.checkerframework.framework.qual.TypeUseLocation @@ -63,6 +66,13 @@ */ TypeUseLocation[] locations() default {TypeUseLocation.ALL}; + /** + * When used on a package, whether the defaults should also apply to subpackages. + * + * @return whether the default should be inherited by subpackages + */ + boolean applyToSubpackages() default true; + /** * A wrapper annotation that makes the {@link DefaultQualifier} annotation repeatable. * diff --git a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java index a32d7640ec5..9dbc8f893fc 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/index/upperbound/UpperBoundAnnotatedTypeFactory.java @@ -642,7 +642,8 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, AnnotatedTypeMi @Override public Void visitBinary(BinaryTree tree, AnnotatedTypeMirror type) { // This implementation does NOT call getAnnotatedType on the left or right operands. - // Doing so would lead to re-examination of subexpressions many times (which is too slow). + // Doing so would lead to re-examination of subexpressions many times (which is too + // slow). // A few small rules for addition/subtraction by 0/1, etc. if (TreeUtils.isStringConcatenation(tree)) { 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 f5711cc42e0..8da9b7af298 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -263,7 +263,8 @@ protected boolean skipReceiverSubtypeCheck( // If you think of the receiver of the method call as an implicit parameter, it has some // MustCall type. For example, consider the method call: // void foo(@MustCall("bar") ThisClass this) - // If we now call o.foo() where o has @MustCall({"bar, baz"}), the receiver subtype check would + // If we now call o.foo() where o has @MustCall({"bar, baz"}), the receiver subtype check + // would // throw an error, since o is not a subtype of @MustCall("bar"). However, since foo cannot // take ownership of its receiver, it does not matter what it 'thinks' the @MustCall methods // of the receiver are. Hence, it is always sound to skip this check. diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 8bb453ac57c..1eeeaacf053 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -2739,7 +2739,8 @@ public Node visitConditionalExpression(ConditionalExpressionTree tree, Void p) { Tree parent = TreePathUtil.getContextForPolyExpression(getCurrentPath()); if (parent != null) { exprType = TreeUtils.typeOf(parent); - // exprType is null when the condition is non-atomic, e.g.: x.isEmpty() ? null : null + // exprType is null when the condition is non-atomic, e.g.: x.isEmpty() ? null : + // null } if (parent == null || exprType == null) { exprType = TypesUtils.getObjectTypeMirror(env); diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 4f3fd2804a7..c2d562f0d8d 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,10 @@ Version 3.48.2 (November 1, 2024) **User-visible changes:** +`DefaultQualifier` supports the new `applyToSubpackages` annotation attribute +to decide whether a default should also apply to subpackages. To preserve the +current behavior, the default is `true`. + **Implementation details:** **Closed issues:** diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 61c6dac6d7e..dba01035d8c 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -1253,7 +1253,8 @@ public void typeProcess(TypeElement e, TreePath p) { // All other messages are printed immediately. This includes errors issued because the // checker threw an exception. - // Update errsOnLastExit for all checkers, so that no matter which one is run next, its test of + // Update errsOnLastExit for all checkers, so that no matter which one is run next, its test + // of // whether a Java error occurred is correct. Context context = ((JavacProcessingEnvironment) processingEnv).getContext(); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 26ff32eb39a..bcf1955e451 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -2464,9 +2464,12 @@ protected ParameterizedExecutableType methodFromUse( } if (typeArguments.inferenceCrash && tree instanceof MethodInvocationTree) { - // If inference crashed, then the return type will not be the correct Java type. This can - // cause crashes elsewhere in the framework. To avoid those crashes, create an ATM with the - // correct Java type and default annotations. (If inference crashes an error will be issued + // If inference crashed, then the return type will not be the correct Java type. This + // can + // cause crashes elsewhere in the framework. To avoid those crashes, create an ATM with + // the + // correct Java type and default annotations. (If inference crashes an error will be + // issued // in the BaseTypeVisitor.) TypeMirror type = TreeUtils.typeOf(tree); AnnotatedTypeMirror returnType = AnnotatedTypeMirror.createType(type, this, false); @@ -2855,9 +2858,12 @@ protected ParameterizedExecutableType constructorFromUse( stubTypes.injectRecordComponentType(types, ctor, con); if (typeArguments.inferenceCrash) { - // If inference crashed, then the return type will not be the correct Java type. This can - // cause crashes elsewhere in the framework. To avoid those crashes, create an ATM with the - // correct Java type and default annotations. (If inference crashes an error will be issued + // If inference crashed, then the return type will not be the correct Java type. This + // can + // cause crashes elsewhere in the framework. To avoid those crashes, create an ATM with + // the + // correct Java type and default annotations. (If inference crashes an error will be + // issued // in the BaseTypeVisitor.) TypeMirror typeTM = TreeUtils.typeOf(tree); AnnotatedTypeMirror returnType = AnnotatedTypeMirror.createType(typeTM, this, false); diff --git a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java index 8a32cb9f7f7..022e4b7e5ab 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -900,7 +900,8 @@ public static AnnotatedTypeMirror annotatedGLB( if (type2.getKind() == TypeKind.TYPEVAR) { return type2; } - // I think the only way error happens is when one of the types is a typevarible, but just in + // I think the only way error happens is when one of the types is a typevarible, but + // just in // case, just return type1. return type1; } diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/Default.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/Default.java index 87069d811dc..e517cbb431f 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/defaults/Default.java +++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/Default.java @@ -21,25 +21,40 @@ public class Default implements Comparable { /** The type use location. */ public final TypeUseLocation location; + /** Whether the default should be inherited by subpackages. */ + public final boolean applyToSubpackages; + /** * Construct a Default object. * * @param anno the default annotation mirror * @param location the type use location + * @param applyToSubpackages whether the default should be inherited by subpackages */ - public Default(AnnotationMirror anno, TypeUseLocation location) { + public Default( + final AnnotationMirror anno, + final TypeUseLocation location, + final boolean applyToSubpackages) { this.anno = anno; this.location = location; + this.applyToSubpackages = applyToSubpackages; } @Override public int compareTo(Default other) { int locationOrder = location.compareTo(other.location); - if (locationOrder == 0) { - return AnnotationUtils.compareAnnotationMirrors(anno, other.anno); - } else { + if (locationOrder != 0) { return locationOrder; } + int annoOrder = AnnotationUtils.compareAnnotationMirrors(anno, other.anno); + if (annoOrder != 0) { + return annoOrder; + } + if (applyToSubpackages == other.applyToSubpackages) { + return 0; + } else { + return applyToSubpackages ? 1 : -1; + } } @Override @@ -57,11 +72,16 @@ public boolean equals(@Nullable Object thatObj) { @Override public int hashCode() { - return Objects.hash(anno, location); + return Objects.hash(anno, location, applyToSubpackages); } @Override public String toString() { - return "( " + location.name() + " => " + anno + " )"; + return "( " + + location.name() + + " => " + + anno + + (applyToSubpackages ? "applies to subpackages" : "") + + " )"; } } diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java index a5dd1e34dd9..ae4ab85d78c 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java +++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java @@ -90,6 +90,9 @@ public class QualifierDefaults { /** The locations() element/field of a @DefaultQualifier annotation. */ protected final ExecutableElement defaultQualifierLocationsElement; + /** The applyToSubpackages() element/field of a @DefaultQualifier annotation. */ + protected final ExecutableElement defaultQualifierApplyToSubpackagesElement; + /** The value() element/field of a @DefaultQualifier.List annotation. */ protected final ExecutableElement defaultQualifierListValueElement; @@ -189,6 +192,8 @@ public QualifierDefaults(Elements elements, AnnotatedTypeFactory atypeFactory) { TreeUtils.getMethod(DefaultQualifier.class, "value", 0, processingEnv); this.defaultQualifierLocationsElement = TreeUtils.getMethod(DefaultQualifier.class, "locations", 0, processingEnv); + this.defaultQualifierApplyToSubpackagesElement = + TreeUtils.getMethod(DefaultQualifier.class, "applyToSubpackages", 0, processingEnv); this.defaultQualifierListValueElement = TreeUtils.getMethod(DefaultQualifier.List.class, "value", 0, processingEnv); } @@ -272,13 +277,29 @@ public void addClimbStandardDefaults() { } /** - * Sets the default annotations. A programmer may override this by writing the @DefaultQualifier + * Adds a default annotation. A programmer may override this by writing the @DefaultQualifier * annotation on an element. + * + * @param absoluteDefaultAnno the default annotation mirror + * @param location the type use location + * @param applyToSubpackages whether the default should be inherited by subpackages */ public void addCheckedCodeDefault( - AnnotationMirror absoluteDefaultAnno, TypeUseLocation location) { + AnnotationMirror absoluteDefaultAnno, TypeUseLocation location, boolean applyToSubpackages) { checkDuplicates(checkedCodeDefaults, absoluteDefaultAnno, location); - checkedCodeDefaults.add(new Default(absoluteDefaultAnno, location)); + checkedCodeDefaults.add(new Default(absoluteDefaultAnno, location, applyToSubpackages)); + } + + /** + * Adds a default annotation that also applies to subpackages, if applicable. A programmer may + * override this by writing the @DefaultQualifier annotation on an element. + * + * @param absoluteDefaultAnno the default annotation mirror + * @param location the type use location + */ + public void addCheckedCodeDefault( + AnnotationMirror absoluteDefaultAnno, TypeUseLocation location) { + addCheckedCodeDefault(absoluteDefaultAnno, location, true); } /** @@ -286,13 +307,25 @@ public void addCheckedCodeDefault( * * @param uncheckedDefaultAnno the default annotation mirror * @param location the type use location + * @param applyToSubpackages whether the default should be inherited by subpackages */ public void addUncheckedCodeDefault( - AnnotationMirror uncheckedDefaultAnno, TypeUseLocation location) { + AnnotationMirror uncheckedDefaultAnno, TypeUseLocation location, boolean applyToSubpackages) { checkDuplicates(uncheckedCodeDefaults, uncheckedDefaultAnno, location); checkIsValidUncheckedCodeLocation(uncheckedDefaultAnno, location); + uncheckedCodeDefaults.add(new Default(uncheckedDefaultAnno, location, applyToSubpackages)); + } - uncheckedCodeDefaults.add(new Default(uncheckedDefaultAnno, location)); + /** + * Add a default annotation for unchecked elements that also applies to subpackages, if + * applicable. + * + * @param uncheckedDefaultAnno the default annotation mirror + * @param location the type use location + */ + public void addUncheckedCodeDefault( + AnnotationMirror uncheckedDefaultAnno, TypeUseLocation location) { + addUncheckedCodeDefault(uncheckedDefaultAnno, location, true); } /** Sets the default annotation for unchecked elements, with specific locations. */ @@ -317,6 +350,16 @@ public void addCheckedCodeDefaults( * @param elementDefaultAnno the default to set * @param location the location to apply the default to */ + /* + * TODO(cpovirk): This method looks dangerous for a type system to call early: If it "adds" a + * default for an Element before defaultsAt runs for that Element, that looks like it would + * prevent any @DefaultQualifier or similar annotation from having any effect (because + * defaultsAt would short-circuit after discovering that an entry already exists for the + * Element). Maybe this method should run defaultsAt before inserting its own entry? Or maybe + * it's too early to run defaultsAt? Or maybe we'd see new problems in existing code because + * we'd start running checkDuplicates to look for overlap between the @DefaultQualifier defaults + * and addElementDefault defaults? + */ public void addElementDefault( Element elem, AnnotationMirror elementDefaultAnno, TypeUseLocation location) { DefaultSet prevset = elementDefaults.get(elem); @@ -325,7 +368,8 @@ public void addElementDefault( } else { prevset = new DefaultSet(); } - prevset.add(new Default(elementDefaultAnno, location)); + // TODO: expose applyToSubpackages + prevset.add(new Default(elementDefaultAnno, location, true)); elementDefaults.put(elem, prevset); } @@ -352,7 +396,8 @@ private void checkDuplicates( "Only one qualifier from a hierarchy can be the default. Existing: " + previousDefaults + " and new: " - + new Default(newAnno, newLoc)); + // TODO: expose applyToSubpackages + + new Default(newAnno, newLoc, true)); } } @@ -585,9 +630,13 @@ private void applyDefaults(Tree tree, AnnotatedTypeMirror type) { defaultQualifierLocationsElement, TypeUseLocation.class, defaultQualifierValueDefault); + boolean applyToSubpackages = + AnnotationUtils.getElementValue( + dq, defaultQualifierApplyToSubpackagesElement, Boolean.class, true); + DefaultSet ret = new DefaultSet(); for (TypeUseLocation loc : locations) { - ret.add(new Default(anno, loc)); + ret.add(new Default(anno, loc, applyToSubpackages)); } return ret; } else { @@ -653,55 +702,40 @@ private DefaultSet defaultsAt(Element elt) { return elementDefaults.get(elt); } - DefaultSet qualifiers = null; - - { - AnnotationMirror dqAnno = atypeFactory.getDeclAnnotation(elt, DefaultQualifier.class); - - if (dqAnno != null) { - qualifiers = new DefaultSet(); - Set p = fromDefaultQualifier(dqAnno); - - if (p != null) { - qualifiers.addAll(p); - } - } - } - - { - AnnotationMirror dqListAnno = - atypeFactory.getDeclAnnotation(elt, DefaultQualifier.List.class); - if (dqListAnno != null) { - if (qualifiers == null) { - qualifiers = new DefaultSet(); - } + DefaultSet qualifiers = defaultsAtDirect(elt); - List values = - AnnotationUtils.getElementValueArray( - dqListAnno, defaultQualifierListValueElement, AnnotationMirror.class); - for (AnnotationMirror dqAnno : values) { - Set p = fromDefaultQualifier(dqAnno); - if (p != null) { - qualifiers.addAll(p); - } + DefaultSet parentDefaults; + if (elt.getKind() == ElementKind.PACKAGE) { + Element parent = ElementUtils.parentPackage((PackageElement) elt, elements); + DefaultSet origParentDefaults = defaultsAt(parent); + parentDefaults = new DefaultSet(); + for (Default d : origParentDefaults) { + if (d.applyToSubpackages) { + parentDefaults.add(d); } } - } - - Element parent; - if (elt.getKind() == ElementKind.PACKAGE) { - parent = ElementUtils.parentPackage((PackageElement) elt, elements); } else { - parent = elt.getEnclosingElement(); + Element parent = elt.getEnclosingElement(); + parentDefaults = defaultsAt(parent); } - DefaultSet parentDefaults = defaultsAt(parent); if (qualifiers == null || qualifiers.isEmpty()) { qualifiers = parentDefaults; } else { + // TODO(cpovirk): What should happen with conflicts? qualifiers.addAll(parentDefaults); } + /* TODO: it would seem more efficient to also cache null/empty as the result. + * However, doing so causes KeyFor tests to fail. + if (qualifiers == null) { + qualifiers = DefaultSet.EMPTY; + } + + elementDefaults.put(elt, qualifiers); + return qualifiers; + */ + if (qualifiers != null && !qualifiers.isEmpty()) { elementDefaults.put(elt, qualifiers); return qualifiers; @@ -710,6 +744,48 @@ private DefaultSet defaultsAt(Element elt) { } } + /** + * Returns the defaults that apply directly to the given Element, without considering enclosing + * Elements. + * + * @param elt the element + * @return the defaults + */ + private DefaultSet defaultsAtDirect(final Element elt) { + DefaultSet qualifiers = null; + + // Handle DefaultQualifier + AnnotationMirror dqAnno = atypeFactory.getDeclAnnotation(elt, DefaultQualifier.class); + + if (dqAnno != null) { + Set p = fromDefaultQualifier(dqAnno); + + if (p != null) { + qualifiers = new DefaultSet(); + qualifiers.addAll(p); + } + } + + // Handle DefaultQualifier.List + AnnotationMirror dqListAnno = atypeFactory.getDeclAnnotation(elt, DefaultQualifier.List.class); + if (dqListAnno != null) { + if (qualifiers == null) { + qualifiers = new DefaultSet(); + } + @SuppressWarnings("unchecked") + List values = + AnnotationUtils.getElementValue(dqListAnno, defaultQualifierListValueElement, List.class); + for (AnnotationMirror dqlAnno : values) { + Set p = fromDefaultQualifier(dqlAnno); + if (p != null) { + // TODO(cpovirk): What should happen with conflicts? + qualifiers.addAll(p); + } + } + } + return qualifiers; + } + /** * Given an element, returns whether the conservative default should be applied for it. Handles * elements from bytecode or source code. diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java index eb9bbf1fa14..c7169073d40 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java @@ -670,8 +670,10 @@ private BoundSet getB4(BoundSet b3, ConstraintSet c) { c.remove(subset); BoundSet newBounds = subset.reduceAdditionalArgOnce(context); if (!subset.isEmpty()) { - // The subset is not empty at this point if an additional argument constraint was found. - // In this case, a new subset needs to be picked so that dependencies of the constraints + // The subset is not empty at this point if an additional argument constraint was + // found. + // In this case, a new subset needs to be picked so that dependencies of the + // constraints // from reducing the additional argument constraint can be taken into account. c.addAll(subset); } diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java index c1014e07c32..682cc5eb3aa 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java @@ -211,7 +211,8 @@ private ReductionResult reduceSubtypeClass(Java8InferenceContext context) { // constraint reduces to the following new constraints: // for all i (1 <= i <= n), . - // Capturing is not in the JLS, but otherwise wildcards appear in the constraints against + // Capturing is not in the JLS, but otherwise wildcards appear in the constraints + // against // the type arguments, which causes crashes. AbstractType sAsSuper = S.asSuper(T.getJavaType()).capture(context); if (sAsSuper == null) { diff --git a/framework/tests/h1h2checker/pkg1/PackageDefaulting.java b/framework/tests/h1h2checker/pkg1/PackageDefaulting.java new file mode 100644 index 00000000000..81c9bc75d79 --- /dev/null +++ b/framework/tests/h1h2checker/pkg1/PackageDefaulting.java @@ -0,0 +1,23 @@ +package pkg1; + +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1S1; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1S2; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H2S1; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H2S2; + +/* Defaults from package pkg1 apply within the package. */ +public class PackageDefaulting { + // Test H1 hierarchy + void m(@H1S1 @H2S1 Object p1, @H1S2 @H2S1 Object p2) { + Object l1 = p1; + // :: error: (assignment.type.incompatible) + Object l2 = p2; + } + + // Test H2 hierarchy + void m2(@H1S1 @H2S1 Object p1, @H1S1 @H2S2 Object p2) { + Object l1 = p1; + // :: error: (assignment.type.incompatible) + Object l2 = p2; + } +} diff --git a/framework/tests/h1h2checker/pkg1/package-info.java b/framework/tests/h1h2checker/pkg1/package-info.java new file mode 100644 index 00000000000..616b07aef5f --- /dev/null +++ b/framework/tests/h1h2checker/pkg1/package-info.java @@ -0,0 +1,14 @@ +@DefaultQualifier( + value = H1S1.class, + locations = {TypeUseLocation.LOCAL_VARIABLE}, + applyToSubpackages = false) +@DefaultQualifier( + value = H2S1.class, + locations = {TypeUseLocation.LOCAL_VARIABLE}, + applyToSubpackages = true) +package pkg1; + +import org.checkerframework.framework.qual.DefaultQualifier; +import org.checkerframework.framework.qual.TypeUseLocation; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1S1; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H2S1; diff --git a/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java b/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java new file mode 100644 index 00000000000..8f0f50dba07 --- /dev/null +++ b/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java @@ -0,0 +1,22 @@ +package pkg1.pkg2; + +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1S1; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1S2; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H2S1; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H2S2; + +/* Default from package pkg1 for H1 is not applied to subpackages, whereas H2 is applied. */ +public class PackageDefaulting { + // Test H1 hierarchy + void m(@H1S1 @H2S1 Object p1, @H1S2 @H2S1 Object p2) { + Object l1 = p1; + Object l2 = p2; + } + + // Test H2 hierarchy + void m2(@H2S1 Object p1, @H2S2 Object p2) { + Object l1 = p1; + // :: error: (assignment.type.incompatible) + Object l2 = p2; + } +} From c12a7e1ffbc24e2ae38ed28a735f46f36a9ba9e0 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 12 Oct 2024 14:20:12 -0700 Subject: [PATCH 2/3] Fill comments --- .../checker/mustcall/MustCallVisitor.java | 7 +++---- .../framework/source/SourceChecker.java | 3 +-- .../framework/type/AnnotatedTypeFactory.java | 18 ++++++------------ .../framework/util/AnnotatedTypes.java | 3 +-- .../InvocationTypeInference.java | 7 +++---- .../util/typeinference8/constraint/Typing.java | 3 +-- 6 files changed, 15 insertions(+), 26 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 8da9b7af298..3bbeb0a84d9 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -264,10 +264,9 @@ protected boolean skipReceiverSubtypeCheck( // MustCall type. For example, consider the method call: // void foo(@MustCall("bar") ThisClass this) // If we now call o.foo() where o has @MustCall({"bar, baz"}), the receiver subtype check - // would - // throw an error, since o is not a subtype of @MustCall("bar"). However, since foo cannot - // take ownership of its receiver, it does not matter what it 'thinks' the @MustCall methods - // of the receiver are. Hence, it is always sound to skip this check. + // would throw an error, since o is not a subtype of @MustCall("bar"). However, since foo + // cannot take ownership of its receiver, it does not matter what it 'thinks' the @MustCall + // methods of the receiver are. Hence, it is always sound to skip this check. return true; } diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index dba01035d8c..b7044dfa92a 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -1254,8 +1254,7 @@ public void typeProcess(TypeElement e, TreePath p) { // checker threw an exception. // Update errsOnLastExit for all checkers, so that no matter which one is run next, its test - // of - // whether a Java error occurred is correct. + // of whether a Java error occurred is correct. Context context = ((JavacProcessingEnvironment) processingEnv).getContext(); Log log = Log.instance(context); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index bcf1955e451..4d8c1015659 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -2465,12 +2465,9 @@ protected ParameterizedExecutableType methodFromUse( if (typeArguments.inferenceCrash && tree instanceof MethodInvocationTree) { // If inference crashed, then the return type will not be the correct Java type. This - // can - // cause crashes elsewhere in the framework. To avoid those crashes, create an ATM with - // the - // correct Java type and default annotations. (If inference crashes an error will be - // issued - // in the BaseTypeVisitor.) + // can cause crashes elsewhere in the framework. To avoid those crashes, create an ATM + // with the correct Java type and default annotations. (If inference crashes an error + // will be issued in the BaseTypeVisitor.) TypeMirror type = TreeUtils.typeOf(tree); AnnotatedTypeMirror returnType = AnnotatedTypeMirror.createType(type, this, false); addDefaultAnnotations(returnType); @@ -2859,12 +2856,9 @@ protected ParameterizedExecutableType constructorFromUse( if (typeArguments.inferenceCrash) { // If inference crashed, then the return type will not be the correct Java type. This - // can - // cause crashes elsewhere in the framework. To avoid those crashes, create an ATM with - // the - // correct Java type and default annotations. (If inference crashes an error will be - // issued - // in the BaseTypeVisitor.) + // can cause crashes elsewhere in the framework. To avoid those crashes, create an ATM + // with the correct Java type and default annotations. (If inference crashes an error + // will be issued in the BaseTypeVisitor.) TypeMirror typeTM = TreeUtils.typeOf(tree); AnnotatedTypeMirror returnType = AnnotatedTypeMirror.createType(typeTM, this, false); addDefaultAnnotations(returnType); diff --git a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java index 022e4b7e5ab..4b03f348d8e 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -901,8 +901,7 @@ public static AnnotatedTypeMirror annotatedGLB( return type2; } // I think the only way error happens is when one of the types is a typevarible, but - // just in - // case, just return type1. + // just in case, just return type1. return type1; } Types types = atypeFactory.types; diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java index c7169073d40..df952385f33 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/InvocationTypeInference.java @@ -671,10 +671,9 @@ private BoundSet getB4(BoundSet b3, ConstraintSet c) { BoundSet newBounds = subset.reduceAdditionalArgOnce(context); if (!subset.isEmpty()) { // The subset is not empty at this point if an additional argument constraint was - // found. - // In this case, a new subset needs to be picked so that dependencies of the - // constraints - // from reducing the additional argument constraint can be taken into account. + // found. In this case, a new subset needs to be picked so that dependencies of + // the constraints from reducing the additional argument constraint can be taken + // into account. c.addAll(subset); } b3.incorporateToFixedPoint(newBounds); diff --git a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java index 682cc5eb3aa..18cac2c507b 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java +++ b/framework/src/main/java/org/checkerframework/framework/util/typeinference8/constraint/Typing.java @@ -212,8 +212,7 @@ private ReductionResult reduceSubtypeClass(Java8InferenceContext context) { // for all i (1 <= i <= n), . // Capturing is not in the JLS, but otherwise wildcards appear in the constraints - // against - // the type arguments, which causes crashes. + // against the type arguments, which causes crashes. AbstractType sAsSuper = S.asSuper(T.getJavaType()).capture(context); if (sAsSuper == null) { return ConstraintSet.FALSE; From 250e34d0dd7358252b93a2d287666cc82b9e91d3 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 12 Oct 2024 15:30:25 -0700 Subject: [PATCH 3/3] Update error message keys --- framework/tests/h1h2checker/pkg1/PackageDefaulting.java | 4 ++-- framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/framework/tests/h1h2checker/pkg1/PackageDefaulting.java b/framework/tests/h1h2checker/pkg1/PackageDefaulting.java index 81c9bc75d79..c40783eff70 100644 --- a/framework/tests/h1h2checker/pkg1/PackageDefaulting.java +++ b/framework/tests/h1h2checker/pkg1/PackageDefaulting.java @@ -10,14 +10,14 @@ public class PackageDefaulting { // Test H1 hierarchy void m(@H1S1 @H2S1 Object p1, @H1S2 @H2S1 Object p2) { Object l1 = p1; - // :: error: (assignment.type.incompatible) + // :: error: (assignment) Object l2 = p2; } // Test H2 hierarchy void m2(@H1S1 @H2S1 Object p1, @H1S1 @H2S2 Object p2) { Object l1 = p1; - // :: error: (assignment.type.incompatible) + // :: error: (assignment) Object l2 = p2; } } diff --git a/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java b/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java index 8f0f50dba07..c44d9fee003 100644 --- a/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java +++ b/framework/tests/h1h2checker/pkg1/pkg2/PackageDefaulting.java @@ -16,7 +16,7 @@ void m(@H1S1 @H2S1 Object p1, @H1S2 @H2S1 Object p2) { // Test H2 hierarchy void m2(@H2S1 Object p1, @H2S2 Object p2) { Object l1 = p1; - // :: error: (assignment.type.incompatible) + // :: error: (assignment) Object l2 = p2; } }