From 4dec994ebf67cc734ecbf674ade63b33dfa74cf8 Mon Sep 17 00:00:00 2001 From: zcai Date: Thu, 24 Mar 2022 00:48:59 -0400 Subject: [PATCH 1/5] set bottom as the default and upperbound for the same group of types --- src/main/java/universe/qual/Bottom.java | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/main/java/universe/qual/Bottom.java b/src/main/java/universe/qual/Bottom.java index 136ecb4..21efe61 100644 --- a/src/main/java/universe/qual/Bottom.java +++ b/src/main/java/universe/qual/Bottom.java @@ -7,6 +7,7 @@ import org.checkerframework.framework.qual.TargetLocations; import org.checkerframework.framework.qual.TypeKind; import org.checkerframework.framework.qual.TypeUseLocation; +import org.checkerframework.framework.qual.UpperBoundFor; import java.lang.annotation.Documented; import java.lang.annotation.ElementType; @@ -25,6 +26,28 @@ @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND}) @SubtypeOf({Self.class, Rep.class}) @QualifierForLiterals({LiteralKind.ALL}) +@UpperBoundFor( + typeKinds = { + TypeKind.INT, + TypeKind.BYTE, + TypeKind.SHORT, + TypeKind.BOOLEAN, + TypeKind.LONG, + TypeKind.CHAR, + TypeKind.FLOAT, + TypeKind.DOUBLE + }, + types = { + String.class, + Double.class, + Boolean.class, + Byte.class, + Character.class, + Float.class, + Integer.class, + Long.class, + Short.class + }) @DefaultFor( value = {TypeUseLocation.LOWER_BOUND}, typeKinds = { From 0bcf82bece51dc89ea039ae9439fd754b6488d7f Mon Sep 17 00:00:00 2001 From: zcai Date: Thu, 24 Mar 2022 00:50:07 -0400 Subject: [PATCH 2/5] remove custom PropagationTreeAnnotaters, which were used to apply bottom annotations to certain types --- .../UniverseAnnotatedTypeFactory.java | 66 ------------------- ...UniverseInferenceAnnotatedTypeFactory.java | 43 +----------- tests/inference/InvalidString.java | 3 +- 3 files changed, 3 insertions(+), 109 deletions(-) diff --git a/src/main/java/universe/UniverseAnnotatedTypeFactory.java b/src/main/java/universe/UniverseAnnotatedTypeFactory.java index c0c584b..217b34a 100644 --- a/src/main/java/universe/UniverseAnnotatedTypeFactory.java +++ b/src/main/java/universe/UniverseAnnotatedTypeFactory.java @@ -2,22 +2,15 @@ import checkers.inference.BaseInferenceRealTypeFactory; -import com.sun.source.tree.BinaryTree; import com.sun.source.tree.IdentifierTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; -import com.sun.source.tree.TypeCastTree; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.ViewpointAdapter; -import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; -import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; -import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; -import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator; import org.checkerframework.javacutil.TreeUtils; import universe.qual.Any; @@ -63,19 +56,6 @@ protected ViewpointAdapter createViewpointAdapter() { return new UniverseViewpointAdapter(this); } - /** - * Create our own TreeAnnotator. - * - * @return the new TreeAnnotator. - */ - @Override - protected TreeAnnotator createTreeAnnotator() { - return new ListTreeAnnotator( - new UniversePropagationTreeAnnotator(this), - new LiteralTreeAnnotator(this), - new UniverseTreeAnnotator()); - } - @Override protected Set> createSupportedTypeQualifiers() { Set> annotations = @@ -137,50 +117,4 @@ public Void visitMethod(MethodTree node, AnnotatedTypeMirror p) { return super.visitMethod(node, p); } } - - private static class UniversePropagationTreeAnnotator extends PropagationTreeAnnotator { - /** - * Creates a {@link DefaultForTypeAnnotator} from the given checker, using that checker's - * type hierarchy. - * - * @param atypeFactory type factory to use - */ - public UniversePropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) { - super(atypeFactory); - } - - /** - * Add immutable to the result type of a binary operation if the result type is implicitly - * immutable - */ - @Override - public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { - applyImmutableIfImplicitlyBottom( - type); // Usually there isn't existing annotation on binary trees, but to be - // safe, run it first - super.visitBinary(node, type); - return null; - } - - /** Add immutable to the result type of a cast if the result type is implicitly immutable */ - @Override - public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { - applyImmutableIfImplicitlyBottom( - type); // Must run before calling super method to respect existing annotation - return super.visitTypeCast(node, type); - } - - /** - * Because TreeAnnotator runs before DefaultForTypeAnnotator, implicitly immutable types are - * not guaranteed to always have immutable annotation. If this happens, we manually add - * immutable to type. We use addMissingAnnotations because we want to respect existing - * annotation on type - */ - private void applyImmutableIfImplicitlyBottom(AnnotatedTypeMirror type) { - if (UniverseTypeUtil.isImplicitlyBottomType(type)) { - type.addMissingAnnotations( - new HashSet<>(Arrays.asList(UniverseAnnotationMirrorHolder.BOTTOM))); - } - } - } } diff --git a/src/main/java/universe/UniverseInferenceAnnotatedTypeFactory.java b/src/main/java/universe/UniverseInferenceAnnotatedTypeFactory.java index cd955ba..b51010f 100644 --- a/src/main/java/universe/UniverseInferenceAnnotatedTypeFactory.java +++ b/src/main/java/universe/UniverseInferenceAnnotatedTypeFactory.java @@ -1,7 +1,6 @@ package universe; import static universe.UniverseAnnotationMirrorHolder.ANY; -import static universe.UniverseAnnotationMirrorHolder.BOTTOM; import static universe.UniverseAnnotationMirrorHolder.PEER; import static universe.UniverseAnnotationMirrorHolder.REP; import static universe.UniverseAnnotationMirrorHolder.SELF; @@ -18,7 +17,6 @@ import com.sun.source.tree.BinaryTree; import com.sun.source.tree.Tree; -import com.sun.source.tree.TypeCastTree; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFactory; @@ -58,7 +56,7 @@ public UniverseInferenceAnnotatedTypeFactory( public TreeAnnotator createTreeAnnotator() { return new ListTreeAnnotator( new LiteralTreeAnnotator(this), - new UniverseInferencePropagationTreeAnnotater(this), + new PropagationTreeAnnotator(this), new InferenceTreeAnnotator( this, realChecker, realTypeFactory, variableAnnotator, slotManager)); } @@ -117,45 +115,6 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { } } - private static class UniverseInferencePropagationTreeAnnotater - extends PropagationTreeAnnotator { - public UniverseInferencePropagationTreeAnnotater(AnnotatedTypeFactory atypeFactory) { - super(atypeFactory); - } - - @Override - public Void visitBinary(BinaryTree node, AnnotatedTypeMirror type) { - applyBottomIfImplicitlyBottom( - type); // Usually there isn't existing annotation on binary trees, but to be - // safe, run it first - return super.visitBinary(node, type); - } - - @Override - public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { - applyBottomIfImplicitlyBottom( - type); // Must run before calling super method to respect existing annotation - if (type.isAnnotatedInHierarchy(ANY)) { - // VarAnnot is guarenteed to not exist on type, because PropagationTreeAnnotator has - // the highest previledge - // So VarAnnot hasn't been inserted to cast type yet. - UniverseTypeUtil.applyConstant(type, type.getAnnotationInHierarchy(ANY)); - } - return super.visitTypeCast(node, type); - } - - /** - * Because TreeAnnotator runs before ImplicitsTypeAnnotator, implicitly immutable types are - * not guaranteed to always have immutable annotation. If this happens, we manually add - * immutable to type. - */ - private void applyBottomIfImplicitlyBottom(AnnotatedTypeMirror type) { - if (UniverseTypeUtil.isImplicitlyBottomType(type)) { - UniverseTypeUtil.applyConstant(type, BOTTOM); - } - } - } - public static class UniverseInferenceViewpointAdapter extends InferenceViewpointAdapter { public UniverseInferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { diff --git a/tests/inference/InvalidString.java b/tests/inference/InvalidString.java index 737eac2..bf6441d 100644 --- a/tests/inference/InvalidString.java +++ b/tests/inference/InvalidString.java @@ -2,7 +2,8 @@ public class InvalidString { void foo() { - throwException("" + Arrays.asList("", "")); + throwException("" + Arrays.asList("", "") + ""); + throwException(3 + ""); } void throwException(String s) {} From c328988c010abb41f149254b451003019087e226 Mon Sep 17 00:00:00 2001 From: zcai Date: Fri, 25 Mar 2022 00:27:10 -0400 Subject: [PATCH 3/5] add UniverseTreeAnnotator back --- .../universe/UniverseAnnotatedTypeFactory.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/main/java/universe/UniverseAnnotatedTypeFactory.java b/src/main/java/universe/UniverseAnnotatedTypeFactory.java index 217b34a..0a9fd0f 100644 --- a/src/main/java/universe/UniverseAnnotatedTypeFactory.java +++ b/src/main/java/universe/UniverseAnnotatedTypeFactory.java @@ -10,6 +10,9 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.ViewpointAdapter; +import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.javacutil.TreeUtils; @@ -56,6 +59,19 @@ protected ViewpointAdapter createViewpointAdapter() { return new UniverseViewpointAdapter(this); } + /** + * Create our own TreeAnnotator. + * + * @return the new TreeAnnotator. + */ + @Override + protected TreeAnnotator createTreeAnnotator() { + return new ListTreeAnnotator( + new PropagationTreeAnnotator(this), + new LiteralTreeAnnotator(this), + new UniverseTreeAnnotator()); + } + @Override protected Set> createSupportedTypeQualifiers() { Set> annotations = From edb578983d7d49b59c92c05031cc65ceac2d9103 Mon Sep 17 00:00:00 2001 From: zcai Date: Fri, 25 Mar 2022 01:59:51 -0400 Subject: [PATCH 4/5] stop using custom bottom type checks --- .../universe/UniverseInferenceValidator.java | 18 ------------------ .../universe/UniverseInferenceVisitor.java | 6 ------ .../java/universe/UniverseTypeValidator.java | 19 ------------------- src/main/java/universe/UniverseVisitor.java | 6 ------ 4 files changed, 49 deletions(-) diff --git a/src/main/java/universe/UniverseInferenceValidator.java b/src/main/java/universe/UniverseInferenceValidator.java index 8740de8..79d5679 100644 --- a/src/main/java/universe/UniverseInferenceValidator.java +++ b/src/main/java/universe/UniverseInferenceValidator.java @@ -39,9 +39,6 @@ public UniverseInferenceValidator( */ @Override public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Tree p) { - if (checkTopLevelDeclaredOrPrimitiveType) { - checkImplicitlyBottomTypeError(type, p); - } checkStaticRepError(type, p); // @Peer is allowed in static context @@ -79,25 +76,10 @@ public Void visitArray(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree) { return super.visitArray(type, tree); } - @Override - public Void visitPrimitive(AnnotatedTypeMirror.AnnotatedPrimitiveType type, Tree tree) { - if (checkTopLevelDeclaredOrPrimitiveType) { - checkImplicitlyBottomTypeError(type, tree); - } - return super.visitPrimitive(type, tree); - } - private void checkStaticRepError(AnnotatedTypeMirror type, Tree tree) { if (UniverseTypeUtil.inStaticScope(visitor.getCurrentPath())) { ((UniverseInferenceVisitor) visitor) .doesNotContain(type, REP, "uts.static.rep.forbidden", tree); } } - - private void checkImplicitlyBottomTypeError(AnnotatedTypeMirror type, Tree tree) { - if (UniverseTypeUtil.isImplicitlyBottomType(type)) { - ((UniverseInferenceVisitor) visitor) - .effectiveIs(type, BOTTOM, "type.invalid.annotations.on.use", tree); - } - } } diff --git a/src/main/java/universe/UniverseInferenceVisitor.java b/src/main/java/universe/UniverseInferenceVisitor.java index 25bd4c2..14794d3 100644 --- a/src/main/java/universe/UniverseInferenceVisitor.java +++ b/src/main/java/universe/UniverseInferenceVisitor.java @@ -66,12 +66,6 @@ protected UniverseInferenceValidator createTypeValidator() { return new UniverseInferenceValidator(checker, this, atypeFactory); } - @Override - public boolean isValidUse( - AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) { - return true; - } - /** * Ignore constructor receiver annotations as result type of the constructor is always SELF for * universe. diff --git a/src/main/java/universe/UniverseTypeValidator.java b/src/main/java/universe/UniverseTypeValidator.java index f3109dd..d243b13 100644 --- a/src/main/java/universe/UniverseTypeValidator.java +++ b/src/main/java/universe/UniverseTypeValidator.java @@ -36,9 +36,6 @@ public UniverseTypeValidator( */ @Override public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Tree p) { - if (checkTopLevelDeclaredOrPrimitiveType) { - checkImplicitlyBottomTypeError(type, p); - } checkStaticRepError(type, p); // @Peer is allowed in static context @@ -77,14 +74,6 @@ public Void visitArray(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree) { return super.visitArray(type, tree); } - @Override - public Void visitPrimitive(AnnotatedTypeMirror.AnnotatedPrimitiveType type, Tree tree) { - if (checkTopLevelDeclaredOrPrimitiveType) { - checkImplicitlyBottomTypeError(type, tree); - } - return super.visitPrimitive(type, tree); - } - private void checkStaticRepError(AnnotatedTypeMirror type, Tree tree) { if (UniverseTypeUtil.inStaticScope(visitor.getCurrentPath())) { if (AnnotatedTypes.containsModifier(type, REP)) { @@ -93,12 +82,4 @@ private void checkStaticRepError(AnnotatedTypeMirror type, Tree tree) { } } } - - private void checkImplicitlyBottomTypeError(AnnotatedTypeMirror type, Tree tree) { - if (UniverseTypeUtil.isImplicitlyBottomType(type)) { - if (!type.hasAnnotation(BOTTOM)) { - reportInvalidAnnotationsOnUse(type, tree); - } - } - } } diff --git a/src/main/java/universe/UniverseVisitor.java b/src/main/java/universe/UniverseVisitor.java index b7185b5..c3d8175 100644 --- a/src/main/java/universe/UniverseVisitor.java +++ b/src/main/java/universe/UniverseVisitor.java @@ -53,12 +53,6 @@ protected UniverseTypeValidator createTypeValidator() { return new UniverseTypeValidator(checker, this, atypeFactory); } - @Override - public boolean isValidUse( - AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) { - return true; - } - /** Ignore method receiver annotations. */ @Override protected void checkMethodInvocability( From b5966217857c07ed2f3b3e9408588d6d5501335b Mon Sep 17 00:00:00 2001 From: zcai Date: Fri, 25 Mar 2022 02:00:30 -0400 Subject: [PATCH 5/5] reformat --- src/main/java/universe/UniverseInferenceValidator.java | 1 - src/main/java/universe/UniverseTypeValidator.java | 1 - 2 files changed, 2 deletions(-) diff --git a/src/main/java/universe/UniverseInferenceValidator.java b/src/main/java/universe/UniverseInferenceValidator.java index 79d5679..e54bdfd 100644 --- a/src/main/java/universe/UniverseInferenceValidator.java +++ b/src/main/java/universe/UniverseInferenceValidator.java @@ -1,6 +1,5 @@ package universe; -import static universe.UniverseAnnotationMirrorHolder.BOTTOM; import static universe.UniverseAnnotationMirrorHolder.LOST; import static universe.UniverseAnnotationMirrorHolder.REP; diff --git a/src/main/java/universe/UniverseTypeValidator.java b/src/main/java/universe/UniverseTypeValidator.java index d243b13..51ff3a9 100644 --- a/src/main/java/universe/UniverseTypeValidator.java +++ b/src/main/java/universe/UniverseTypeValidator.java @@ -1,6 +1,5 @@ package universe; -import static universe.UniverseAnnotationMirrorHolder.BOTTOM; import static universe.UniverseAnnotationMirrorHolder.LOST; import static universe.UniverseAnnotationMirrorHolder.REP;