diff --git a/build.gradle b/build.gradle index 714c4b5..a7e2f56 100644 --- a/build.gradle +++ b/build.gradle @@ -9,7 +9,7 @@ plugins { apply plugin: 'java' ext { - assert JavaVersion.current() == JavaVersion.VERSION_1_8: "Set JAVA_HOME to JDK 8. Current version is ${JavaVersion.current()}" + assert JavaVersion.current() == JavaVersion.VERSION_11: "Set JAVA_HOME to JDK 11. Current version is ${JavaVersion.current()}" jsr308 = file(new File("..")).absolutePath cfPath = "${jsr308}/checker-framework" cfiPath = "${jsr308}/checker-framework-inference" @@ -34,17 +34,16 @@ repositories { } dependencies { - compile fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar") - compile fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar") + implementation fileTree(dir: "${cfPath}/checker/dist", include: "checker.jar") + implementation fileTree(dir: "${cfiPath}/dist", include: "checker-framework-inference.jar") // sat4j solver dependency - compile 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.4' - compile 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.4' + implementation 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.5' + implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.5' // The production code uses the SLF4J logging API at compile time - compile 'org.slf4j:slf4j-api:1.7.13' - + implementation 'org.slf4j:slf4j-api:1.7.29' // CF test lib dependency - testCompile fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar") - testCompile 'junit:junit:4.12' + testImplementation fileTree(dir: "${cfPath}/framework-test/build/libs", include: "framework-test-*.jar") + testImplementation 'junit:junit:4.12' } sourceSets { diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index be280be..6b7fd26 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -2,4 +2,4 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-4.5-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-7.3.3-bin.zip diff --git a/src/main/java/pico/common/PICOTypeUtil.java b/src/main/java/pico/common/PICOTypeUtil.java index 97f5a69..ddbc296 100644 --- a/src/main/java/pico/common/PICOTypeUtil.java +++ b/src/main/java/pico/common/PICOTypeUtil.java @@ -27,6 +27,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TypesUtils; import pico.typecheck.PICOVisitor; import qual.Assignable; @@ -119,12 +120,12 @@ public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Tree if (node instanceof MethodTree) { MethodTree methodTree = (MethodTree) node; ExecutableElement element = TreeUtils.elementFromDeclaration(methodTree); - typeElement = ElementUtils.enclosingClass(element); + typeElement = ElementUtils.enclosingTypeElement(element); } else if(node instanceof VariableTree) { VariableTree variableTree = (VariableTree) node; VariableElement variableElement = TreeUtils.elementFromDeclaration(variableTree); assert variableElement!= null && variableElement.getKind().isField(); - typeElement = ElementUtils.enclosingClass(variableElement); + typeElement = ElementUtils.enclosingTypeElement(variableElement); } if (typeElement != null) { @@ -135,7 +136,7 @@ public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Tree } public static AnnotatedDeclaredType getBoundTypeOfEnclosingTypeDeclaration(Element element, AnnotatedTypeFactory atypeFactory) { - TypeElement typeElement = ElementUtils.enclosingClass(element); + TypeElement typeElement = ElementUtils.enclosingTypeElement(element); if (typeElement != null) { return getBoundTypeOfTypeDeclaration(typeElement, atypeFactory); } @@ -255,7 +256,7 @@ public static void addDefaultForField(AnnotatedTypeFactory annotatedTypeFactory, // add RDM if bound=M and enclosingBound=M/RDM Set enclosingBound = annotatedTypeFactory.getTypeDeclarationBounds( - Objects.requireNonNull(ElementUtils.enclosingClass(element)).asType()); + Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType()); Set declBound = annotatedTypeFactory.getTypeDeclarationBounds(element.asType()); if (AnnotationUtils.containsSameByName(declBound, MUTABLE)) { if (AnnotationUtils.containsSameByName(enclosingBound, RECEIVER_DEPENDANT_MUTABLE) || @@ -311,7 +312,7 @@ public static void applyConstant(AnnotatedTypeMirror type, AnnotationMirror am) // Might be null. It's normal. In typechecking side, we use addMissingAnnotations(). Only if // there is existing annotation in code, then here is non-null. Otherwise, VariableAnnotator // hasn't come into the picture yet, so no VarAnnot exists here, which is normal. - Slot shouldBeAppliedTo = slotManager.getVariableSlot(type); + Slot shouldBeAppliedTo = slotManager.getSlot(type); ConstantSlot constant = slotManager.createConstantSlot(am); if (shouldBeAppliedTo == null) { // Here, we are adding VarAnnot that represents @Immutable. There won't be solution for this ConstantSlot for this type, @@ -380,7 +381,7 @@ public static boolean isAssigningAssignableField(ExpressionTree node, Annotation public static boolean isEnclosedByAnonymousClass(Tree tree, AnnotatedTypeFactory atypeFactory) { TreePath path = atypeFactory.getPath(tree); if (path != null) { - ClassTree classTree = TreeUtils.enclosingClass(path); + ClassTree classTree = TreePathUtil.enclosingClass(path); return classTree != null && InferenceUtil.isAnonymousClass(classTree); } return false; @@ -392,7 +393,7 @@ public static AnnotatedDeclaredType getBoundOfEnclosingAnonymousClass(Tree tree, return null; } AnnotatedDeclaredType enclosingType = null; - Tree newclassTree = TreeUtils.enclosingOfKind(path, Tree.Kind.NEW_CLASS); + Tree newclassTree = TreePathUtil.enclosingOfKind(path, Tree.Kind.NEW_CLASS); if (newclassTree != null) { enclosingType = (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(newclassTree); } @@ -407,10 +408,10 @@ public static AnnotationMirror createEquivalentVarAnnotOfRealQualifier(final Ann public static boolean inStaticScope(TreePath treePath) { boolean in = false; - if (TreeUtils.isTreeInStaticScope(treePath)) { + if (TreePathUtil.isTreeInStaticScope(treePath)) { in = true; // Exclude case in which enclosing class is static - ClassTree classTree = TreeUtils.enclosingClass(treePath); + ClassTree classTree = TreePathUtil.enclosingClass(treePath); if (classTree != null && classTree.getModifiers().getFlags().contains((Modifier.STATIC))) { in = false; } @@ -454,7 +455,7 @@ public static boolean isArrayType(AnnotatedDeclaredType type, AnnotatedTypeFacto // If it is a user-declared "Array" class without package, a class / source file should be there. // Otherwise, it is the java inner type. return ele instanceof Symbol.ClassSymbol - && ElementUtils.getVerboseName(ele).equals("Array") + && ElementUtils.getQualifiedName(ele).equals("Array") && ((Symbol.ClassSymbol) ele).classfile == null && ((Symbol.ClassSymbol) ele).sourcefile == null; } diff --git a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java index a0b0377..8106066 100644 --- a/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceAnnotatedTypeFactory.java @@ -31,6 +31,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import pico.common.ExtendedViewpointAdapter; import pico.common.ViewpointAdapterGettable; import pico.typecheck.PICOAnnotatedTypeFactory.PICODefaultForTypeAnnotator; @@ -114,7 +115,7 @@ VariableAnnotator getVariableAnnotator() { */ public AnnotatedDeclaredType getSelfType(Tree tree) { TreePath path = getPath(tree); - ClassTree enclosingClass = TreeUtils.enclosingClass(path); + ClassTree enclosingClass = TreePathUtil.enclosingClass(path); if (enclosingClass == null) { // I hope this only happens when tree is a fake tree that // we created, e.g. when desugaring enhanced-for-loops. @@ -123,7 +124,7 @@ public AnnotatedDeclaredType getSelfType(Tree tree) { // "type" is right now VarAnnot inserted to the bound of "enclosingClass" AnnotatedDeclaredType type = getAnnotatedType(enclosingClass); - MethodTree enclosingMethod = TreeUtils.enclosingMethod(path); + MethodTree enclosingMethod = TreePathUtil.enclosingMethod(path); if (enclosingClass.getSimpleName().length() != 0 && enclosingMethod != null) { AnnotatedTypeMirror.AnnotatedDeclaredType methodReceiver; if (TreeUtils.isConstructor(enclosingMethod)) { diff --git a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java index c0644ca..4d41241 100644 --- a/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java +++ b/src/main/java/pico/inference/PICOInferenceRealTypeFactory.java @@ -32,6 +32,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import com.sun.source.tree.Tree; @@ -115,7 +116,7 @@ protected TypeAnnotator createTypeAnnotator() { // annotated. typeAnnotators.add( new IrrelevantTypeAnnotator( - this, getQualifierHierarchy().getTopAnnotations(), classes)); + this, getQualifierHierarchy().getTopAnnotations())); } typeAnnotators.add(new PropagationTypeAnnotator(this)); /*Copied code ends*/ @@ -215,7 +216,7 @@ protected DefaultQualifierForUseTypeAnnotator createDefaultForUseTypeAnnotator() @Override public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) { // add default anno from class main qual, if no qual present - AnnotatedTypeMirror enclosing = getAnnotatedType(TreeUtils.enclosingClass(getPath(clause))); + AnnotatedTypeMirror enclosing = getAnnotatedType(TreePathUtil.enclosingClass(getPath(clause))); // workaround for anonymous class. // TypesUtils::isAnonymous won't work when annotation presents on new class tree! diff --git a/src/main/java/pico/inference/PICOInferenceValidator.java b/src/main/java/pico/inference/PICOInferenceValidator.java index bd282bd..5460a39 100644 --- a/src/main/java/pico/inference/PICOInferenceValidator.java +++ b/src/main/java/pico/inference/PICOInferenceValidator.java @@ -5,7 +5,6 @@ import com.sun.source.tree.Tree; import com.sun.source.tree.VariableTree; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.source.Result; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; @@ -37,7 +36,7 @@ public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) { checkOnlyOneAssignabilityModifierOnField(tree); // AnnotatedDeclaredType defaultType = // (AnnotatedDeclaredType) atypeFactory.getAnnotatedType(type.getUnderlyingType().asElement()); -// // TODO for defaulted super clause: should top anno be checked? (see shouldCheckTopLevelDeclaredType()) +// // TODO for defaulted super clause: should top anno be checked? (see shouldCheckTopLevelDeclaredOrPrimitiveType()) // if (defaultType.getAnnotationInHierarchy(READONLY) == null && !PICOTypeUtil.isEnumOrEnumConstant(defaultType)) { // defaultType = defaultType.deepCopy(); // defaultType.replaceAnnotation(MUTABLE); @@ -64,11 +63,11 @@ public Void visitPrimitive(AnnotatedPrimitiveType type, Tree tree) { } @Override - protected boolean shouldCheckTopLevelDeclaredType(AnnotatedTypeMirror type, Tree tree) { + protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType(AnnotatedTypeMirror type, Tree tree) { if (TreeUtils.isLocalVariable(tree)) { return true; } - return super.shouldCheckTopLevelDeclaredType(type, tree); + return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree); } private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, Tree tree) { @@ -121,7 +120,7 @@ private void checkOnlyOneAssignabilityModifierOnField(Tree tree) { } private void reportFieldMultipleAssignabilityModifiersError(VariableElement field) { - checker.report(Result.failure("one.assignability.invalid", field), field); + checker.reportError(field, "one.assignability.invalid", field); isValid = false; } diff --git a/src/main/java/pico/inference/PICOInferenceVisitor.java b/src/main/java/pico/inference/PICOInferenceVisitor.java index 7bcaf5c..2be5954 100644 --- a/src/main/java/pico/inference/PICOInferenceVisitor.java +++ b/src/main/java/pico/inference/PICOInferenceVisitor.java @@ -27,7 +27,6 @@ import com.sun.source.tree.VariableTree; import com.sun.source.util.TreePath; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.framework.source.Result; import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -38,6 +37,7 @@ import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TypesUtils; import pico.common.ExtendedViewpointAdapter; import pico.common.ViewpointAdapterGettable; @@ -90,12 +90,12 @@ public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclar // allow RDM on mutable fields with enclosing class bounded with mutable if (tree instanceof VariableTree && !useType.isDeclaration()) { VariableElement element = TreeUtils.elementFromDeclaration((VariableTree)tree); - if (element.getKind() == ElementKind.FIELD && ElementUtils.enclosingClass(element) != null) { + if (element.getKind() == ElementKind.FIELD && ElementUtils.enclosingTypeElement(element) != null) { // assert only 1 bound exists AnnotationMirror enclosingBound = extractVarAnnot(PICOTypeUtil.getBoundTypeOfEnclosingTypeDeclaration(element, atypeFactory)); // atypeFactory.getTypeDeclarationBounds( -// Objects.requireNonNull(ElementUtils.enclosingClass(element)).asType()).iterator().next(); +// Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType()).iterator().next(); // if enclosing bound == mutable -> (RDM or Mutable usable on mutable-bounded fields) // else -> adaptedSubtype @@ -162,8 +162,8 @@ private Constraint createAdaptedSubtypeConstraint(AnnotatedTypeMirror lhs, Annot ExtendedViewpointAdapter vpa = ((ViewpointAdapterGettable)atypeFactory).getViewpointAdapter(); AnnotatedTypeMirror adapted = vpa.rawCombineAnnotationWithType(extractVarAnnot(lhs), rhs); return constraintManager.createSubtypeConstraint( - slotManager.getVariableSlot(adapted), - slotManager.getVariableSlot(lhs) + slotManager.getSlot(adapted), + slotManager.getSlot(lhs) ); } @@ -180,8 +180,8 @@ public boolean mainIsSubtype(AnnotatedTypeMirror ty, AnnotationMirror mod) { private void addMutableImmutableRdmIncompatibleConstraints(AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType) { final ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot declSlot = slotManager.getVariableSlot(declarationType); - Slot useSlot = slotManager.getVariableSlot(useType); + Slot declSlot = slotManager.getSlot(declarationType); + Slot useSlot = slotManager.getSlot(useType); Slot mutable = slotManager.getSlot(MUTABLE); Slot immutable = slotManager.getSlot(IMMUTABLE); Slot rdm = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE); @@ -262,7 +262,7 @@ protected void checkConstructorInvocation(AnnotatedDeclaredType invocation, Anno private AnnotationMirror extractVarAnnot(final AnnotatedTypeMirror atm) { if (infer) { final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - return slotManager.getAnnotation(slotManager.getVariableSlot(atm)); + return slotManager.getAnnotation(slotManager.getSlot(atm)); } return atm.getAnnotationInHierarchy(READONLY); } @@ -346,10 +346,10 @@ private Constraint createMainIsMutableOrRdmConstraint(AnnotatedTypeMirror mainAt return constraintManager.createImplicationConstraint( Collections.singletonList(constraintManager.createInequalityConstraint( slotManager.getSlot(MUTABLE), - slotManager.getVariableSlot(mainAtm))), + slotManager.getSlot(mainAtm))), constraintManager.createEqualityConstraint( slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE), - slotManager.getVariableSlot(mainAtm) + slotManager.getSlot(mainAtm) ) ); } @@ -378,10 +378,10 @@ public boolean ifAnnoIsThenMainIsOneOf(AnnotationMirror annotation, AnnotationMi Constraint oneOfConst = constraintManager.createImplicationConstraint( Collections.singletonList(constraintManager.createInequalityConstraint( slotManager.getSlot(oneOf[0]), - slotManager.getVariableSlot(mainAtm))), + slotManager.getSlot(mainAtm))), constraintManager.createEqualityConstraint( slotManager.getSlot(oneOf[1]), - slotManager.getVariableSlot(mainAtm) + slotManager.getSlot(mainAtm) ) ); @@ -417,7 +417,7 @@ public void mainCannotInferTo(AnnotatedTypeMirror atm, AnnotationMirror anno, St if (infer) { SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); // should be constant slot if written explicitly in code - if (!(slotManager.getVariableSlot(atm) instanceof ConstantSlot)) { + if (!(slotManager.getSlot(atm) instanceof ConstantSlot)) { mainIsNot(atm, anno, errorKey, tree); } @@ -456,8 +456,8 @@ public Void visitMethod(MethodTree node, Void p) { if (infer) { ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot boundSlot = slotManager.getVariableSlot(bound); - Slot consRetSlot = slotManager.getVariableSlot(constructorReturnType); + Slot boundSlot = slotManager.getSlot(bound); + Slot consRetSlot = slotManager.getSlot(constructorReturnType); Slot rdmSlot = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE); Constraint inequalityConstraint = constraintManager.createInequalityConstraint(boundSlot, rdmSlot); Constraint subtypeConstraint = constraintManager.createSubtypeConstraint(consRetSlot, boundSlot); @@ -484,7 +484,7 @@ public Void visitMethod(MethodTree node, Void p) { if (declaredReceiverType != null) { mainIsNot(declaredReceiverType, BOTTOM, "bottom.on.receiver", node); if (!isAdaptedSubtype(declaredReceiverType, bound)){ - checker.report(Result.failure("method.receiver.incompatible", declaredReceiverType), node); + checker.reportError(node, "method.receiver.incompatible", declaredReceiverType); } } } @@ -552,9 +552,8 @@ protected void checkTypecastSafety(TypeCastTree node) { if (!isTypeCastSafe(castType, exprType, node)) { // This is only warning message, so even though enterred this line, it doesn't cause PICOInfer to exit. // Even if that was an error, PICOInfer would also not exit. - checker.report( - Result.warning("cast.unsafe", exprType.toString(true), castType.toString(true)), - node); + checker.reportWarning(node, + "cast.unsafe", exprType.toString(true), castType.toString(true)); } } @@ -624,8 +623,8 @@ private boolean isCompatibleCastInInfer(AnnotatedTypeMirror castType, AnnotatedT // Default strategy - comparablecast final QualifierHierarchy qualHierarchy = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy(); final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - final Slot castSlot = slotManager.getVariableSlot(castType); - final Slot exprSlot = slotManager.getVariableSlot(exprType); + final Slot castSlot = slotManager.getSlot(castType); + final Slot exprSlot = slotManager.getSlot(exprType); if (castSlot instanceof ConstantSlot && exprSlot instanceof ConstantSlot) { ConstantSlot castCSSlot = (ConstantSlot) castSlot; @@ -692,8 +691,8 @@ private void checkAssignableField(ExpressionTree node, ExpressionTree variable, // Break the combination of readonly receiver + rdm assignable field ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); - Slot receiverSlot = slotManager.getVariableSlot(receiverType); - Slot fieldSlot = slotManager.getVariableSlot(fieldType); + Slot receiverSlot = slotManager.getSlot(receiverType); + Slot fieldSlot = slotManager.getSlot(fieldType); Slot readonly = slotManager.getSlot(READONLY); Slot receiver_dependant_mutable = slotManager.getSlot(RECEIVER_DEPENDANT_MUTABLE); Constraint receiverReadOnly = constraintManager.createEqualityConstraint(receiverSlot, readonly); @@ -764,12 +763,12 @@ private boolean isInitializingObject(ExpressionTree variable) { TreePath treePath = atypeFactory.getPath(variable); if (treePath == null) return false; - if (TreeUtils.enclosingTopLevelBlock(treePath) != null) { + if (TreePathUtil.enclosingTopLevelBlock(treePath) != null) { // In the initialization block => always allow assigning fields! return true; } - MethodTree enclosingMethod = TreeUtils.enclosingMethod(treePath); + MethodTree enclosingMethod = TreePathUtil.enclosingMethod(treePath); // No possibility of initializing object if the assignment is not within constructor or method(both MethodTree) if (enclosingMethod == null) return false; // At this point, we already know that this assignment is field assignment within a method @@ -826,7 +825,7 @@ private void checkNewInstanceCreation(Tree node) { public Void visitMethodInvocation(MethodInvocationTree node, Void p) { // issues with getting super for anonymous class - do not check for anonymous classes. if (TreeUtils.isSuperConstructorCall(node) && - PICOTypeUtil.isAnonymousClassTree(TreeUtils.enclosingClass(atypeFactory.getPath(node)), atypeFactory)) { + PICOTypeUtil.isAnonymousClassTree(TreePathUtil.enclosingClass(atypeFactory.getPath(node)), atypeFactory)) { return null; } diff --git a/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java b/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java index 21ac92e..a03ccae 100644 --- a/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java +++ b/src/main/java/pico/inference/solver/PICOCombineConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; +import checkers.inference.model.CombVariableSlot; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; @@ -51,7 +52,7 @@ private boolean isReceiverDependantMutable(ConstantSlot cSlot) { } @Override - public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declared, VariableSlot result) { + public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); resultClauses.add(VectorUtils.asVec( -MathUtils.mapIdToMatrixEntry(declared.getId(), id(READONLY), lattice), @@ -89,7 +90,7 @@ public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declar } @Override - public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declared, VariableSlot result) { + public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); if (!isReceiverDependantMutable(declared)) { resultClauses.add(VectorUtils.asVec( @@ -116,7 +117,7 @@ public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declar } @Override - public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declared, VariableSlot result) { + public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); resultClauses.add(VectorUtils.asVec( -MathUtils.mapIdToMatrixEntry(declared.getId(), id(READONLY), lattice), @@ -137,7 +138,7 @@ public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declar } @Override - public VecInt[] encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, VariableSlot result) { + public VecInt[] encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, CombVariableSlot result) { List resultClauses = new ArrayList(); if (!isReceiverDependantMutable(declared)) { resultClauses.add(VectorUtils.asVec( diff --git a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java index b33e535..988d056 100644 --- a/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java +++ b/src/main/java/pico/typecheck/PICOAnnotatedTypeFactory.java @@ -45,6 +45,7 @@ import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ExpressionTree; @@ -126,12 +127,12 @@ protected TypeAnnotator createTypeAnnotator() { RelevantJavaTypes relevantJavaTypes = checker.getClass().getAnnotation(RelevantJavaTypes.class); if (relevantJavaTypes != null) { - Class[] classes = relevantJavaTypes.value(); +// Class[] classes = relevantJavaTypes.value(); // Must be first in order to annotated all irrelevant types that are not explicilty // annotated. typeAnnotators.add( new IrrelevantTypeAnnotator( - this, getQualifierHierarchy().getTopAnnotations(), classes)); + this, getQualifierHierarchy().getTopAnnotations())); } typeAnnotators.add(new PropagationTypeAnnotator(this)); /*Copied code ends*/ @@ -449,7 +450,7 @@ public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) { // this is still needed with PICOSuperClauseAnnotator. // maybe just use getAnnotatedType // add default anno from class main qual, if no qual present - AnnotatedTypeMirror enclosing = getAnnotatedType(TreeUtils.enclosingClass(getPath(clause))); + AnnotatedTypeMirror enclosing = getAnnotatedType(TreePathUtil.enclosingClass(getPath(clause))); AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(READONLY); AnnotatedTypeMirror fromTypeTree = this.fromTypeTree(clause); if (!fromTypeTree.isAnnotatedInHierarchy(READONLY)) { @@ -643,7 +644,7 @@ private void addDefaultFromMain(Tree tree, AnnotatedTypeMirror mirror) { if (isSuperClause(path) && (!mirror.isAnnotatedInHierarchy(READONLY) || atypeFactory.getQualifierHierarchy().findAnnotationInHierarchy(TreeUtils.typeOf(tree).getAnnotationMirrors(), READONLY) == null)) { - AnnotatedTypeMirror enclosing = atypeFactory.getAnnotatedType(TreeUtils.enclosingClass(path)); + AnnotatedTypeMirror enclosing = atypeFactory.getAnnotatedType(TreePathUtil.enclosingClass(path)); AnnotationMirror mainBound = enclosing.getAnnotationInHierarchy(READONLY); mirror.replaceAnnotation(mainBound); // System.err.println("ANNOT: ADDED DEFAULT FOR: " + mirror); diff --git a/src/main/java/pico/typecheck/PICOValidator.java b/src/main/java/pico/typecheck/PICOValidator.java index 4c6b017..b651ad8 100644 --- a/src/main/java/pico/typecheck/PICOValidator.java +++ b/src/main/java/pico/typecheck/PICOValidator.java @@ -14,6 +14,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TreePathUtil; import pico.common.PICOTypeUtil; import javax.lang.model.element.AnnotationMirror; @@ -48,7 +49,7 @@ public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) { } @Override - protected boolean shouldCheckTopLevelDeclaredType(AnnotatedTypeMirror type, Tree tree) { + protected boolean shouldCheckTopLevelDeclaredOrPrimitiveType(AnnotatedTypeMirror type, Tree tree) { // check top annotations in extends/implements clauses if ((tree.getKind() == Kind.IDENTIFIER || tree.getKind() == Kind.PARAMETERIZED_TYPE) && PICOAnnotatedTypeFactory.PICOSuperClauseAnnotator.isSuperClause(atypeFactory.getPath(tree))) { @@ -57,10 +58,10 @@ protected boolean shouldCheckTopLevelDeclaredType(AnnotatedTypeMirror type, Tree // allow RDM on mutable fields with enclosing class bounded with mutable if (tree instanceof VariableTree) { VariableElement element = TreeUtils.elementFromDeclaration((VariableTree)tree); - if (element.getKind() == ElementKind.FIELD && ElementUtils.enclosingClass(element) != null) { + if (element.getKind() == ElementKind.FIELD && ElementUtils.enclosingTypeElement(element) != null) { Set enclosingBound = atypeFactory.getTypeDeclarationBounds( - Objects.requireNonNull(ElementUtils.enclosingClass(element)).asType()); + Objects.requireNonNull(ElementUtils.enclosingTypeElement(element)).asType()); Set declaredBound = atypeFactory.getTypeDeclarationBounds(type.getUnderlyingType()); @@ -76,7 +77,7 @@ protected boolean shouldCheckTopLevelDeclaredType(AnnotatedTypeMirror type, Tree // return true; // } - return super.shouldCheckTopLevelDeclaredType(type, tree); + return super.shouldCheckTopLevelDeclaredOrPrimitiveType(type, tree); } @Override @@ -95,7 +96,7 @@ public Void visitPrimitive(AnnotatedPrimitiveType type, Tree tree) { private void checkStaticReceiverDependantMutableError(AnnotatedTypeMirror type, Tree tree) { if (!type.isDeclaration() // variables in static contexts and static fields use class decl as enclosing type && PICOTypeUtil.inStaticScope(visitor.getCurrentPath()) - && !"".contentEquals(Objects.requireNonNull(TreeUtils.enclosingClass(visitor.getCurrentPath())).getSimpleName()) // Exclude @RDM usages in anonymous classes + && !"".contentEquals(Objects.requireNonNull(TreePathUtil.enclosingClass(visitor.getCurrentPath())).getSimpleName()) // Exclude @RDM usages in anonymous classes && type.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) { reportValidityResult("static.receiverdependantmutable.forbidden", type, tree); } diff --git a/src/main/java/pico/typecheck/PICOVisitor.java b/src/main/java/pico/typecheck/PICOVisitor.java index f23a74f..071746b 100644 --- a/src/main/java/pico/typecheck/PICOVisitor.java +++ b/src/main/java/pico/typecheck/PICOVisitor.java @@ -474,7 +474,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void p) { private void saveFbcViolatedMethods(ExecutableElement method, String actualReceiver, String declaredReceiver) { if (actualReceiver.contains("@UnderInitialization") && declaredReceiver.contains("@Initialized")) { - String key = ElementUtils.enclosingClass(method) + "#" + method; + String key = ElementUtils.enclosingTypeElement(method) + "#" + method; Integer times = fbcViolatedMethods.get(key) == null ? 1 : fbcViolatedMethods.get(key) + 1; fbcViolatedMethods.put(key, times); }