From 2cfe035fd60415336e3d3b4ead5bc314005afc94 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Fri, 21 Jan 2022 19:14:50 -0500 Subject: [PATCH] Cleanup src (#33) Co-authored-by: Weitian Xing Co-authored-by: Baorui Zhou Co-authored-by: Jeff Luo Co-authored-by: Mier Ta --- .../UniverseAnnotatedTypeFactory.java | 357 +++++------ .../UniverseAnnotationMirrorHolder.java | 36 ++ src/universe/UniverseChecker.java | 27 +- ...UniverseInferenceAnnotatedTypeFactory.java | 147 +++-- src/universe/UniverseInferenceChecker.java | 36 +- ...UniverseInferenceConstraintSerializer.java | 30 - .../UniverseInferenceConstraintSolver.java | 13 - .../UniverseInferenceMaxSatSerializer.java | 356 ----------- src/universe/UniverseInferenceTests.java | 8 - src/universe/UniverseInferenceValidator.java | 94 +++ src/universe/UniverseInferenceVisitor.java | 579 +++++++----------- src/universe/UniverseTypeUtil.java | 113 ++++ src/universe/UniverseTypeValidator.java | 100 +++ src/universe/UniverseViewpointAdapter.java | 59 ++ src/universe/UniverseViewpointAdaptor.java | 82 --- src/universe/UniverseVisitor.java | 444 ++++++-------- src/universe/jdk.astub | 18 +- src/universe/messages.properties | 9 +- src/universe/qual/Any.java | 4 - src/universe/qual/Bottom.java | 21 +- src/universe/qual/Lost.java | 4 +- src/universe/qual/Peer.java | 2 +- src/universe/qual/Rep.java | 2 +- src/universe/qual/Self.java | 6 +- src/universe/qual/VPLost.java | 23 - .../UniverseCombineConstraintEncoder.java | 350 +++++++++++ .../solver/UniverseFormatTranslator.java | 26 + src/universe/solver/UniverseSolverEngine.java | 19 + 28 files changed, 1524 insertions(+), 1441 deletions(-) create mode 100644 src/universe/UniverseAnnotationMirrorHolder.java delete mode 100644 src/universe/UniverseInferenceConstraintSerializer.java delete mode 100644 src/universe/UniverseInferenceConstraintSolver.java delete mode 100644 src/universe/UniverseInferenceMaxSatSerializer.java delete mode 100644 src/universe/UniverseInferenceTests.java create mode 100644 src/universe/UniverseInferenceValidator.java create mode 100644 src/universe/UniverseTypeUtil.java create mode 100644 src/universe/UniverseTypeValidator.java create mode 100644 src/universe/UniverseViewpointAdapter.java delete mode 100644 src/universe/UniverseViewpointAdaptor.java delete mode 100644 src/universe/qual/VPLost.java create mode 100644 src/universe/solver/UniverseCombineConstraintEncoder.java create mode 100644 src/universe/solver/UniverseFormatTranslator.java create mode 100644 src/universe/solver/UniverseSolverEngine.java diff --git a/src/universe/UniverseAnnotatedTypeFactory.java b/src/universe/UniverseAnnotatedTypeFactory.java index eb86fd3..bc20e44 100644 --- a/src/universe/UniverseAnnotatedTypeFactory.java +++ b/src/universe/UniverseAnnotatedTypeFactory.java @@ -1,64 +1,42 @@ package universe; -import java.lang.annotation.Annotation; -import java.util.Arrays; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; -import javax.lang.model.element.ElementKind; -import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.TypeElement; -import javax.lang.model.type.TypeKind; -import javax.lang.model.type.TypeVariable; - -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.dataflow.qual.Pure; -import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; -import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; -import org.checkerframework.framework.type.AnnotatedTypeReplacer; -import org.checkerframework.framework.type.DefaultTypeHierarchy; -import org.checkerframework.framework.type.QualifierHierarchy; -import org.checkerframework.framework.type.TypeHierarchy; -import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; -import org.checkerframework.framework.type.treeannotator.TreeAnnotator; -import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator; -import org.checkerframework.framework.type.typeannotator.TypeAnnotator; -import org.checkerframework.framework.util.AnnotatedTypes; -import org.checkerframework.javacutil.AnnotationUtils; +import checkers.inference.BaseInferenceRealTypeFactory; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodTree; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.typeannotator.DefaultForTypeAnnotator; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; import org.checkerframework.javacutil.Pair; -import org.checkerframework.javacutil.TreeUtils; -import org.checkerframework.javacutil.TypesUtils; - -import com.sun.source.tree.BinaryTree; -import com.sun.source.tree.CompoundAssignmentTree; -import com.sun.source.tree.IdentifierTree; -import com.sun.source.tree.MethodInvocationTree; -import com.sun.source.tree.NewArrayTree; -import com.sun.source.tree.NewClassTree; -import com.sun.source.tree.ParameterizedTypeTree; -import com.sun.source.tree.Tree; -import com.sun.source.tree.TypeCastTree; -import com.sun.source.tree.UnaryTree; - import universe.qual.Any; import universe.qual.Bottom; import universe.qual.Lost; import universe.qual.Peer; import universe.qual.Rep; import universe.qual.Self; -import universe.qual.VPLost; +import com.sun.source.tree.BinaryTree; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.NewArrayTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.TypeCastTree; +import org.checkerframework.common.basetype.BaseTypeChecker; +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.TreeAnnotator; +import org.checkerframework.javacutil.TreeUtils; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.type.TypeKind; +import java.lang.annotation.Annotation; +import java.util.Arrays; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Set; /** * Apply viewpoint adaptation and add implicit annotations to "this" and @@ -66,27 +44,10 @@ * * @author wmdietl */ -public class UniverseAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { - - // TODO: change to getters? - protected AnnotationMirror ANY, PEER, REP, LOST, VPLOST, SELF, BOTTOM, PURE; - - public UniverseAnnotatedTypeFactory(BaseTypeChecker checker) { - super(checker, true); - ANY = AnnotationUtils.fromClass(elements, Any.class); - PEER = AnnotationUtils.fromClass(elements, Peer.class); - REP = AnnotationUtils.fromClass(elements, Rep.class); - LOST = AnnotationUtils.fromClass(elements, Lost.class); - VPLOST = AnnotationUtils.fromClass(elements, VPLost.class); - SELF = AnnotationUtils.fromClass(elements, Self.class); - BOTTOM = AnnotationUtils.fromClass(elements, Bottom.class); - PURE = AnnotationUtils.fromClass(elements, Pure.class); - - addAliasedAnnotation(org.jmlspecs.annotation.Peer.class, PEER); - addAliasedAnnotation(org.jmlspecs.annotation.Rep.class, REP); - addAliasedAnnotation(org.jmlspecs.annotation.Readonly.class, ANY); - // see UniverseVisitor.isPure for handling of pure +public class UniverseAnnotatedTypeFactory extends BaseInferenceRealTypeFactory { + public UniverseAnnotatedTypeFactory(BaseTypeChecker checker, boolean infer) { + super(checker, infer); this.postInit(); } @@ -97,47 +58,50 @@ public UniverseAnnotatedTypeFactory(BaseTypeChecker checker) { public AnnotatedDeclaredType getSelfType(Tree tree) { AnnotatedDeclaredType type = super.getSelfType(tree); if (type != null) { - type.replaceAnnotation(SELF); + type.replaceAnnotation(UniverseAnnotationMirrorHolder.SELF); } return type; } + @Override + protected ViewpointAdapter createViewpointAdapter() { + return new UniverseViewpointAdapter(this); + } + /** * Create our own TreeAnnotator. * @return the new TreeAnnotator. */ @Override protected TreeAnnotator createTreeAnnotator() { - TreeAnnotator fromAbove = super.createTreeAnnotator(); return new ListTreeAnnotator( - new UniverseTreeAnnotator(), - fromAbove - ); + new UniversePropagationTreeAnnotator(this), + new LiteralTreeAnnotator(this), + new UniverseTreeAnnotator() + ); } - /** - * Create our own TypeAnnotator. - * @return the new TreeAnnotator. - */ - @Override - protected TypeAnnotator createTypeAnnotator() { - TypeAnnotator fromAbove = super.createTypeAnnotator(); - return new ListTypeAnnotator( - fromAbove, - new UniverseTypeAnnotator() - ); + protected Set> createSupportedTypeQualifiers() { + Set> annotations = new HashSet<>( + Arrays.asList(Any.class, Lost.class, + Peer.class, Rep.class, Self.class, Bottom.class)); + return Collections.unmodifiableSet(annotations); } @Override - protected TypeHierarchy createTypeHierarchy() { - return new UniverseTypeHierarchy(checker, getQualifierHierarchy()); + public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) { + UniverseTypeUtil.defaultConstructorReturnToSelf(elt, type); + super.addComputedTypeAnnotations(elt, type); } - - protected Set> createSupportedTypeQualifiers() { - Set> annotations = new HashSet<>(Arrays.asList(Any.class, Lost.class, VPLost.class, - Peer.class, Rep.class, Self.class, Bottom.class)); - return Collections.unmodifiableSet(annotations); + /** + * Replace annotation of extends or implements clause with SELF in Universe. + */ + @Override + public AnnotatedTypeMirror getTypeOfExtendsImplements(Tree clause) { + AnnotatedTypeMirror s = super.getTypeOfExtendsImplements(clause); + s.replaceAnnotation(UniverseAnnotationMirrorHolder.SELF); + return s; } /** @@ -164,149 +128,128 @@ public Void visitIdentifier(IdentifierTree node, AnnotatedTypeMirror p) { // There's no "super" kind, so make a string comparison. if (node.getName().contentEquals("super")) { - p.replaceAnnotation(SELF); + p.replaceAnnotation(UniverseAnnotationMirrorHolder.SELF); } return super.visitIdentifier(node, p); } @Override - public Void visitParameterizedType(ParameterizedTypeTree node, AnnotatedTypeMirror p) { - // System.out.println("visitParameterizedType: " + node + " " + p); - Tree parent = getPath(node).getParentPath().getLeaf(); - if (TreeUtils.isClassTree(parent)) { - p.replaceAnnotation(SELF); - } - return super.visitParameterizedType(node, p); - } - - @Override - public Void visitBinary(BinaryTree node, AnnotatedTypeMirror p) { - // System.out.println("Binary: "); - return super.visitBinary(node, p); - } - - @Override - public Void visitUnary(UnaryTree node, AnnotatedTypeMirror p) { - // System.out.println("Unary: "); - return super.visitUnary(node, p); - } - - @Override - public Void visitCompoundAssignment(CompoundAssignmentTree node, - AnnotatedTypeMirror p) { - // System.out.println("Compound: "); - return super.visitCompoundAssignment(node, p); + public Void visitMethod(MethodTree node, AnnotatedTypeMirror p) { + ExecutableElement executableElement = TreeUtils.elementFromDeclaration(node); + UniverseTypeUtil.defaultConstructorReturnToSelf(executableElement, p); + return super.visitMethod(node, p); } + } - @Override - public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror p) { - // System.out.println("Cast: "); - return super.visitTypeCast(node, p); + private class UniversePropagationTreeAnnotator extends PropagationTreeAnnotator { + /** + * Creates a {@link DefaultForTypeAnnotator} + * from the given checker, using that checker's type hierarchy. + * + * @param atypeFactory + */ + public UniversePropagationTreeAnnotator(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); } + // TODO This is very ugly. Why is array component type from lhs propagates to rhs?! @Override public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { - // System.out.println("Array type: " + type); - super.visitNewArray(tree, type); - // ((AnnotatedArrayType)type).getComponentType().addAnnotation(GUTChecker.BOTTOM); - // System.out.println("Final Array type: " + type); - return null; - } + // Below is copied from super + assert type.getKind() == TypeKind.ARRAY + : "PropagationTreeAnnotator.visitNewArray: should be an array type"; - } + AnnotatedTypeMirror componentType = ((AnnotatedTypeMirror.AnnotatedArrayType) type).getComponentType(); - /** - */ - private class UniverseTypeAnnotator extends TypeAnnotator { + Collection prev = null; + if (tree.getInitializers() != null && tree.getInitializers().size() != 0) { + // We have initializers, either with or without an array type. - public UniverseTypeAnnotator() { - super(UniverseAnnotatedTypeFactory.this); - } -/* - @Override - public Void visitDeclared(AnnotatedDeclaredType type, Void p) { - if (!type.isAnnotatedInHierarchy(ANY)) { - if (GUTChecker.isAnyDefault(type)) { - type.addAnnotation(ANY); - } else { - type.addAnnotation(PEER); + for (ExpressionTree init : tree.getInitializers()) { + AnnotatedTypeMirror initType = atypeFactory.getAnnotatedType(init); + // initType might be a typeVariable, so use effectiveAnnotations. + Collection annos = initType.getEffectiveAnnotations(); + + prev = (prev == null) ? annos : atypeFactory.getQualifierHierarchy().leastUpperBounds(prev, annos); } + } else { + prev = componentType.getAnnotations(); } - return super.visitDeclared(type, p); - } - @Override - public Void visitArray(AnnotatedArrayType type, Void p) { - if (!type.isAnnotatedInHierarchy(ANY)) { - if (GUTChecker.isAnyDefault(type)) { - type.addAnnotation(ANY); + assert prev != null + : "PropagationTreeAnnotator.visitNewArray: violated assumption about qualifiers"; + + Pair context = + atypeFactory.getVisitorState().getAssignmentContext(); + Collection post; + + if (context != null + && context.second != null + && context.second instanceof AnnotatedTypeMirror.AnnotatedArrayType) { + AnnotatedTypeMirror contextComponentType = + ((AnnotatedTypeMirror.AnnotatedArrayType) context.second).getComponentType(); + // Only compare the qualifiers that existed in the array type + // Defaulting wasn't performed yet, so prev might have fewer qualifiers than + // contextComponentType, which would cause a failure. + // TODO: better solution? + boolean prevIsSubtype = true; + for (AnnotationMirror am : prev) { + if (contextComponentType.isAnnotatedInHierarchy(am) + && !atypeFactory.getQualifierHierarchy().isSubtype( + am, contextComponentType.getAnnotationInHierarchy(am))) { + prevIsSubtype = false; + } + } + // TODO: checking conformance of component kinds is a basic sanity check + // It fails for array initializer expressions. Those should be handled nicer. + if (contextComponentType.getKind() == componentType.getKind() + && (prev.isEmpty() + || (!contextComponentType.getAnnotations().isEmpty() + && prevIsSubtype))) { + post = contextComponentType.getAnnotations(); } else { - type.addAnnotation(PEER); + // The type of the array initializers is incompatible with the + // context type! + // Somebody else will complain. + post = prev; } + } else { + // No context is available - simply use what we have. + post = prev; } - return super.visitArray(type, p); - } - */ - } - - /* - private final class GUTQualifierHierarchy extends GraphQualifierHierarchy { - public GUTQualifierHierarchy(GraphQualifierHierarchy hierarchy) { - super(hierarchy); - } - - @Override - public boolean isSubtype(AnnotationMirror rhs, AnnotationMirror lhs) { - return rhs == null || lhs == null - || super.isSubtype(rhs, lhs); - } - } - */ - private final class UniverseTypeHierarchy extends DefaultTypeHierarchy { - public UniverseTypeHierarchy(BaseTypeChecker checker, QualifierHierarchy qualifierHierarchy) { - super(checker, qualifierHierarchy, - checker.hasOption("ignoreRawTypeArguments"), - checker.hasOption("invariantArrays")); - } - - @Override - public boolean isSubtype(AnnotatedTypeMirror sub, AnnotatedTypeMirror sup) { - if (sub.getUnderlyingType().getKind().isPrimitive() || - sup.getUnderlyingType().getKind().isPrimitive() ) { - // TODO: Ignore boxing/unboxing - return true; - } - if (TypesUtils.isString(sub.getUnderlyingType()) || - TypesUtils.isString(sup.getUnderlyingType())) { - return true; - } + // Below line is the only difference from super implementation + applyImmutableIfImplicitlyBottom(componentType); + // Above line is the only difference from super implementation + componentType.addMissingAnnotations(post); - return super.isSubtype(sub, sup); + return null; + // Above is copied from super } + /**Add immutable to the result type of a binary operation if the result type is implicitly immutable*/ @Override - protected boolean isAnnoSubtype(AnnotationMirror subtypeAnno, AnnotationMirror supertypeAnno, - boolean annosCanBeEmtpy) { - if (subtypeAnno == null || supertypeAnno == null) { - // TODO: lower bounds of wildcards in method parameters do not get defaulted correctly! - return true; - } - - return super.isAnnoSubtype(subtypeAnno, supertypeAnno, annosCanBeEmtpy); + 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 - protected boolean isSubtypeAsTypeArgument(AnnotatedTypeMirror rhs, AnnotatedTypeMirror lhs) { - return super.isSubtypeAsTypeArgument(rhs, lhs); + public Void visitTypeCast(TypeCastTree node, AnnotatedTypeMirror type) { + applyImmutableIfImplicitlyBottom(type);// Must run before calling super method to respect existing annotation + return super.visitTypeCast(node, type); } - @Override - protected boolean isSubtypeTypeArguments(AnnotatedDeclaredType rhs, AnnotatedDeclaredType lhs) { - return super.isSubtypeTypeArguments(rhs, lhs); + /**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/universe/UniverseAnnotationMirrorHolder.java b/src/universe/UniverseAnnotationMirrorHolder.java new file mode 100644 index 0000000..d40496d --- /dev/null +++ b/src/universe/UniverseAnnotationMirrorHolder.java @@ -0,0 +1,36 @@ +package universe; + +import org.checkerframework.framework.source.SourceChecker; +import universe.qual.Any; +import universe.qual.Bottom; +import universe.qual.Lost; +import universe.qual.Peer; +import universe.qual.Rep; +import universe.qual.Self; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.javacutil.AnnotationBuilder; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.util.Elements; + +/** + * Class that declares the AnnotationMirrors used by typecheck and inference + * + */ + +public class UniverseAnnotationMirrorHolder { + + public static AnnotationMirror ANY, PEER, REP, LOST, SELF, BOTTOM, PURE; + + public static void init(SourceChecker checker) { + Elements elements = checker.getElementUtils(); + ANY = AnnotationBuilder.fromClass(elements, Any.class); + PEER = AnnotationBuilder.fromClass(elements, Peer.class); + REP = AnnotationBuilder.fromClass(elements, Rep.class); + LOST = AnnotationBuilder.fromClass(elements, Lost.class); + SELF = AnnotationBuilder.fromClass(elements, Self.class); + BOTTOM = AnnotationBuilder.fromClass(elements, Bottom.class); + PURE = AnnotationBuilder.fromClass(elements, Pure.class); + } + +} diff --git a/src/universe/UniverseChecker.java b/src/universe/UniverseChecker.java index 7a7fa44..5f2f384 100644 --- a/src/universe/UniverseChecker.java +++ b/src/universe/UniverseChecker.java @@ -1,12 +1,12 @@ package universe; +import universe.UniverseAnnotationMirrorHolder; import javax.annotation.processing.SupportedOptions; import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.source.SupportedLintOptions; -import org.checkerframework.framework.type.AnnotatedTypeMirror; - /** * The main checker class for the Generic Universe Types checker. @@ -21,28 +21,15 @@ @SupportedLintOptions({"allowLost", "checkOaM", "checkStrictPurity"}) public class UniverseChecker extends BaseTypeChecker { - //TODO Clarify the purpose of this - public static boolean isAnyDefault(AnnotatedTypeMirror type) { - // if (!(type instanceof AnnotatedDeclaredType)) - return false; - /* - DeclaredType dtype = ((AnnotatedDeclaredType)type).getUnderlyingType(); - return TypesUtils.isDeclaredOfName(dtype, "java.lang.String") || - TypesUtils.isDeclaredOfName(dtype, "java.lang.Character"); - */ - } - @Override - public boolean withViewpointAdaptation() { - return true; + public void initChecker() { + super.initChecker(); + UniverseAnnotationMirrorHolder.init(this); } - /* TODO: purity/OaM checking @Override - public boolean isAssignable(AnnotatedTypeMirror varType, - AnnotatedTypeMirror receiverType, Tree varTree) { - return super.isAssignable(varType, receiverType, varTree); + protected BaseTypeVisitor createSourceVisitor() { + return new UniverseVisitor(this, new UniverseAnnotatedTypeFactory(this, false)); } - */ } diff --git a/src/universe/UniverseInferenceAnnotatedTypeFactory.java b/src/universe/UniverseInferenceAnnotatedTypeFactory.java index 063c301..7198738 100644 --- a/src/universe/UniverseInferenceAnnotatedTypeFactory.java +++ b/src/universe/UniverseInferenceAnnotatedTypeFactory.java @@ -1,58 +1,80 @@ package universe; -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; - -import com.sun.source.tree.Tree; - import checkers.inference.InferenceAnnotatedTypeFactory; import checkers.inference.InferenceChecker; -import checkers.inference.InferenceMain; +import checkers.inference.InferenceTreeAnnotator; import checkers.inference.InferrableChecker; import checkers.inference.SlotManager; import checkers.inference.VariableAnnotator; import checkers.inference.model.ConstraintManager; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; +import checkers.inference.util.InferenceViewpointAdapter; +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; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.PropagationTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.TreeAnnotator; + +import javax.lang.model.element.AnnotationMirror; + +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; public class UniverseInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory { public UniverseInferenceAnnotatedTypeFactory(InferenceChecker inferenceChecker, - boolean withCombineConstraints, - BaseAnnotatedTypeFactory realTypeFactory, - InferrableChecker realChecker, SlotManager slotManager, - ConstraintManager constraintManager) { + boolean withCombineConstraints, + BaseAnnotatedTypeFactory realTypeFactory, + InferrableChecker realChecker, SlotManager slotManager, + ConstraintManager constraintManager) { super(inferenceChecker, withCombineConstraints, realTypeFactory, realChecker, slotManager, constraintManager); + + addAliasedTypeAnnotation(org.jmlspecs.annotation.Peer.class, PEER); + addAliasedTypeAnnotation(org.jmlspecs.annotation.Rep.class, REP); + addAliasedTypeAnnotation(org.jmlspecs.annotation.Readonly.class, ANY); postInit(); } + @Override + public TreeAnnotator createTreeAnnotator() { + return new ListTreeAnnotator(new LiteralTreeAnnotator(this), + new UniverseInferencePropagationTreeAnnotater(this), + new InferenceTreeAnnotator(this, realChecker, realTypeFactory, variableAnnotator, slotManager)); + } + + @Override + public VariableAnnotator createVariableAnnotator() { + return new UniverseVariableAnnotator(this, realTypeFactory, realChecker, slotManager, constraintManager); + } + /** * The type of "this" is always "self". */ @Override public AnnotatedDeclaredType getSelfType(Tree tree) { AnnotatedDeclaredType type = super.getSelfType(tree); - if (type != null) { - UniverseAnnotatedTypeFactory univATF = (UniverseAnnotatedTypeFactory) InferenceMain - .getInstance().getRealTypeFactory(); - type.replaceAnnotation(univATF.SELF); - } + UniverseTypeUtil.applyConstant(type, SELF); return type; } -/* @Override - public VariableAnnotator createVariableAnnotator( - InferenceAnnotatedTypeFactory inferenceTypeFactory, - BaseAnnotatedTypeFactory realTypeFactory, - InferrableChecker realChecker, SlotManager slotManager, - ConstraintManager constraintManager) { - return new UniverseInferenceVariableAnnotator(inferenceTypeFactory, realTypeFactory, - realChecker, slotManager, constraintManager); - }*/ - static class UniverseInferenceVariableAnnotator extends VariableAnnotator { + @Override + protected InferenceViewpointAdapter createViewpointAdapter() { + return new UniverseInferenceViewpointAdapter(this); + } + + class UniverseVariableAnnotator extends VariableAnnotator { - public UniverseInferenceVariableAnnotator( + public UniverseVariableAnnotator( InferenceAnnotatedTypeFactory inferenceTypeFactory, AnnotatedTypeFactory realTypeFactory, InferrableChecker realChecker, SlotManager slotManager, @@ -61,18 +83,69 @@ public UniverseInferenceVariableAnnotator( slotManager, constraintManager); } -/* @Override - protected void handleClassDeclarationBound( - AnnotatedDeclaredType classType) { - return; + @Override + protected Slot getOrCreateDeclBound(AnnotatedDeclaredType type) { + // Since we don't care about class declaration annotations in universe type system. + // The superclass method would always create a source variable slot if there doesn't + // exist one for the class declaration. + return getTopConstant(); + } + + @Override + public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { + if (atm.isAnnotatedInHierarchy(getVarAnnot())) { + // Happens for binary trees whose atm is implicitly immutable and already handled by + // PICOInferencePropagationTreeAnnotator + return; + } + super.handleBinaryTree(atm, binaryTree); + } + } + + private 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 - protected void handleInstantiationConstraint(AnnotatedDeclaredType adt, - VariableSlot instantiationSlot) { - return; - }*/ + 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) { + super(atypeFactory); + } + + @Override + protected AnnotatedTypeMirror combineAnnotationWithType(AnnotationMirror receiverAnnotation, + AnnotatedTypeMirror declared) { + if (UniverseTypeUtil.isImplicitlyBottomType(declared)) { + return declared; + } + return super.combineAnnotationWithType(receiverAnnotation, declared); + } + } +} diff --git a/src/universe/UniverseInferenceChecker.java b/src/universe/UniverseInferenceChecker.java index d0655e7..632e931 100644 --- a/src/universe/UniverseInferenceChecker.java +++ b/src/universe/UniverseInferenceChecker.java @@ -1,10 +1,6 @@ package universe; -import javax.annotation.processing.SupportedOptions; - -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.framework.source.SupportedLintOptions; - +import checkers.inference.BaseInferenceRealTypeFactory; import checkers.inference.BaseInferrableChecker; import checkers.inference.InferenceAnnotatedTypeFactory; import checkers.inference.InferenceChecker; @@ -12,22 +8,27 @@ import checkers.inference.InferrableChecker; import checkers.inference.SlotManager; import checkers.inference.model.ConstraintManager; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.framework.source.SupportedLintOptions; + /** * The main checker class for the Generic Universe Types checker. * * @author wmdietl */ -// Keep these synchronized with the superclass. -@SupportedOptions( { "warn" } ) -@SupportedLintOptions({"allowLost", "checkOaM", "checkStrictPurity"}) +@SupportedLintOptions({"checkOaM", "checkStrictPurity"}) public class UniverseInferenceChecker extends BaseInferrableChecker { @Override - public BaseAnnotatedTypeFactory createRealTypeFactory() { - // Return the UniverseInferenceAnnotatedTypeFactory so that it can carry - // UniverseInferenceVariableAnnotator - return new UniverseInferenceAnnotatedTypeFactory(this); + public void initChecker() { + super.initChecker(); + UniverseAnnotationMirrorHolder.init(this); + } + + @Override + public BaseInferenceRealTypeFactory createRealTypeFactory(boolean infer) { + return new UniverseAnnotatedTypeFactory(this, infer); } @Override @@ -41,19 +42,18 @@ public boolean withCombineConstraints() { return true; } - /* @Override - public boolean withExistentialVariables() { - return false; - }*/ - @Override public InferenceAnnotatedTypeFactory createInferenceATF( InferenceChecker inferenceChecker, InferrableChecker realChecker, BaseAnnotatedTypeFactory realTypeFactory, SlotManager slotManager, ConstraintManager constraintManager) { return new UniverseInferenceAnnotatedTypeFactory(inferenceChecker, - withCombineConstraints(), realTypeFactory, realChecker, + withCombineConstraints(), realTypeFactory, realChecker, slotManager, constraintManager); } + @Override + public boolean isInsertMainModOfLocalVar() { + return true; + } } diff --git a/src/universe/UniverseInferenceConstraintSerializer.java b/src/universe/UniverseInferenceConstraintSerializer.java deleted file mode 100644 index dbb8a80..0000000 --- a/src/universe/UniverseInferenceConstraintSerializer.java +++ /dev/null @@ -1,30 +0,0 @@ -package universe; - -import java.lang.reflect.Constructor; - -import checkers.inference.model.Serializer; -import constraintsolver.ConstraintSerializer; -import constraintsolver.Lattice; - -public class UniverseInferenceConstraintSerializer extends ConstraintSerializer { - - - @SuppressWarnings("unchecked") - public UniverseInferenceConstraintSerializer(String backEndType, Lattice lattice) { - super(backEndType, lattice); - try { - String refinedBackEndType = backEndType; - if (backEndType.contains("MaxSat")) { - refinedBackEndType = backEndType.replace("maxsatbackend.", ""); - } - Class classObjectOfRealSerializer = Class.forName("universe.UniverseInference" + refinedBackEndType + "Serializer"); - Constructor constructor = (Constructor) classObjectOfRealSerializer - .getConstructor(Lattice.class); - realSerializer = (Serializer) constructor.newInstance(lattice); - } catch (Exception e) { - System.out.println("Error: Can't find constructor for: "); - e.printStackTrace(); - } - } - -} diff --git a/src/universe/UniverseInferenceConstraintSolver.java b/src/universe/UniverseInferenceConstraintSolver.java deleted file mode 100644 index 5338cce..0000000 --- a/src/universe/UniverseInferenceConstraintSolver.java +++ /dev/null @@ -1,13 +0,0 @@ -package universe; - -import checkers.inference.model.Serializer; -import constraintsolver.ConstraintSolver; -import constraintsolver.Lattice; - -public class UniverseInferenceConstraintSolver extends ConstraintSolver { - - @Override - protected Serializer createSerializer(String value, Lattice lattice) { - return new UniverseInferenceConstraintSerializer<>(value, lattice); - } -} diff --git a/src/universe/UniverseInferenceMaxSatSerializer.java b/src/universe/UniverseInferenceMaxSatSerializer.java deleted file mode 100644 index 3f98237..0000000 --- a/src/universe/UniverseInferenceMaxSatSerializer.java +++ /dev/null @@ -1,356 +0,0 @@ -package universe; - -import java.util.ArrayList; -import java.util.List; - -import javax.lang.model.element.AnnotationMirror; - -import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.ErrorReporter; -import org.sat4j.core.VecInt; - -import checkers.inference.InferenceMain; -import checkers.inference.model.CombVariableSlot; -import checkers.inference.model.CombineConstraint; -import checkers.inference.model.ConstantSlot; -import checkers.inference.model.Slot; -import checkers.inference.model.VariableSlot; -import constraintsolver.Lattice; -import constraintsolver.VariableCombos; -import maxsatbackend.MaxSatSerializer; -import util.MathUtils; -import util.VectorUtils; - -public class UniverseInferenceMaxSatSerializer extends MaxSatSerializer { - - private AnnotationMirror ANY, PEER, REP, LOST, VPLOST, BOTTOM, SELF; - private boolean allowLost; - - public UniverseInferenceMaxSatSerializer(Lattice lattice) { - super(lattice); - UniverseAnnotatedTypeFactory univATF = (UniverseAnnotatedTypeFactory) InferenceMain - .getInstance().getRealTypeFactory(); - ANY = univATF.ANY; - PEER = univATF.PEER; - REP = univATF.REP; - LOST = univATF.LOST; - VPLOST = univATF.VPLOST; - BOTTOM = univATF.BOTTOM; - SELF = univATF.SELF; - } - - @Override - public VecInt[] serialize(CombineConstraint combineConstraint) { - return new VariableCombos(new VecInt[0]) { - - public VecInt[] accept(Slot target, Slot decl, Slot result, - CombineConstraint constraint) { - - final VecInt[] resultClauses; - if (target instanceof CombVariableSlot) { - Slot realTypeWithoutClassBound = ((CombVariableSlot)target).getSecond(); - target = realTypeWithoutClassBound; - } - if (target instanceof ConstantSlot) { - if (decl instanceof ConstantSlot) { - resultClauses = constant_constant((ConstantSlot) target, - (ConstantSlot) decl, (VariableSlot) result, - constraint); - } else { - resultClauses = constant_variable((ConstantSlot) target, - (VariableSlot) decl, (VariableSlot) result, - constraint); - } - } else if (decl instanceof ConstantSlot) { - resultClauses = variable_constant((VariableSlot) target, - (ConstantSlot) decl, (VariableSlot) result, - constraint); - } else { - resultClauses = variable_variable((VariableSlot) target, - (VariableSlot) decl, (VariableSlot) result, - constraint); - } - return resultClauses; - } - - protected VecInt[] constant_constant(ConstantSlot target, - ConstantSlot decl, VariableSlot result, - CombineConstraint combineConstraint) { - List resultClauses = new ArrayList(); - if (AnnotationUtils.areSame(target.getValue(), BOTTOM)) { - ErrorReporter.errorAbort("Error: Receiver type is BOTTOM!"); - } - if (!allowLost) { - if (AnnotationUtils.areSame(target.getValue(), LOST)) { - ErrorReporter.errorAbort("Error: Receiver type contains LOST!"); - } - } - if (AnnotationUtils.areSame(decl.getValue(), PEER)) { - if (AnnotationUtils.areSame(target.getValue(), REP)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - } - if (AnnotationUtils.areSame(target.getValue(), SELF)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - } - if (AnnotationUtils.areSame(target.getValue(), PEER)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - } - if (AnnotationUtils.areSame(target.getValue(), ANY)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } - if (AnnotationUtils.areSame(target.getValue(), LOST)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } - if (AnnotationUtils.areSame(target.getValue(), VPLOST)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } - } else if (AnnotationUtils.areSame(decl.getValue(), REP)) { - if (AnnotationUtils.areSame(target.getValue(), SELF)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - } - else { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } - } else if (AnnotationUtils.areSame(decl.getValue(), ANY)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), ANY, lattice))); - } else if (AnnotationUtils.areSame(decl.getValue(), BOTTOM)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), BOTTOM, lattice))); - } else if (AnnotationUtils.areSame(decl.getValue(), LOST)) { - if (!allowLost) { - ErrorReporter.errorAbort( - "Error: Declared type contatins LOST!"); - } - else { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice)));//change lost to vplost - } - } else if (AnnotationUtils.areSame(decl.getValue(), VPLOST)) { - ErrorReporter.errorAbort( - "Error: Declared type contatins VPLOST!"); - } else if (AnnotationUtils.areSame(decl.getValue(), SELF)) { - ErrorReporter.errorAbort("Error: Declared type contatins SELF!"); - } else { - ErrorReporter.errorAbort("Error: Unknown declared type!"); - } - - return resultClauses.toArray(new VecInt[resultClauses.size()]); - } - - protected VecInt[] constant_variable(ConstantSlot target, - VariableSlot decl, VariableSlot result, - CombineConstraint combineConstraint) { - List resultClauses = new ArrayList(); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), ANY, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), ANY, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), LOST, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), LOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), SELF, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), BOTTOM, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), BOTTOM, lattice))); - - if (AnnotationUtils.areSame(target.getValue(), PEER)) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),VPLOST, lattice))); - } else if (AnnotationUtils.areSame(target.getValue(), REP)) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),VPLOST, lattice))); - } else if (AnnotationUtils.areSame(target.getValue(), ANY)) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(),PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(),REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),VPLOST, lattice))); - } else if (AnnotationUtils.areSame(target.getValue(), SELF)) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),REP, lattice))); - } else if (AnnotationUtils.areSame(target.getValue(), VPLOST)) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } else if (AnnotationUtils.areSame(target.getValue(), LOST)) { - if (!allowLost) { - ErrorReporter.errorAbort("Error: Receiver type contains LOST!"); - } - else { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(),VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } - } else if (AnnotationUtils.areSame(target.getValue(), BOTTOM)) { - ErrorReporter.errorAbort("Error: Receiver type is BOTTOM!"); - } else { - ErrorReporter.errorAbort("Error: Unknown target type!"); - } - - if (!allowLost) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), LOST, lattice))); - } - - return resultClauses.toArray(new VecInt[resultClauses.size()]); - } - - - protected VecInt[] variable_constant(VariableSlot target, - ConstantSlot decl, VariableSlot result, - CombineConstraint combineConstraint) { - - List resultClauses = new ArrayList(); - - resultClauses.add(VectorUtils.asVec(-MathUtils - .mapIdToMatrixEntry(target.getId(), BOTTOM, lattice))); - if (AnnotationUtils.areSame(decl.getValue(), PEER)) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), SELF, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), ANY, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), LOST, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), VPLOST, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - } else if (AnnotationUtils.areSame(decl.getValue(), REP)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(target.getId(), SELF, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), SELF, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - } else if (AnnotationUtils.areSame(decl.getValue(), ANY)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), ANY, lattice))); - } else if (AnnotationUtils.areSame(decl.getValue(), BOTTOM)) { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), BOTTOM, lattice))); - } else if (AnnotationUtils.areSame(decl.getValue(), LOST)) { - if (!allowLost) { - ErrorReporter.errorAbort( - "Error: Declared type contatins LOST!"); - } - else { - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice)));//change lost to vplost - } - } else if (AnnotationUtils.areSame(decl.getValue(), VPLOST)) { - ErrorReporter.errorAbort( - "Error: Declared type contatins VPLOST!"); - } else if (AnnotationUtils.areSame(decl.getValue(), SELF)) { - ErrorReporter.errorAbort("Error: Declared type contatins SELF!"); - } else { - ErrorReporter.errorAbort("Error: Unknown declared type!"); - } - - if (!allowLost) { - resultClauses.add(VectorUtils.asVec(-MathUtils - .mapIdToMatrixEntry(target.getId(), LOST, lattice))); - } - - return resultClauses.toArray(new VecInt[resultClauses.size()]); - } - - protected VecInt[] variable_variable(VariableSlot target, - VariableSlot decl, VariableSlot result, - CombineConstraint combineConstraint) { - List resultClauses = new ArrayList(); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), ANY, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), ANY, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), LOST, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), LOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), SELF, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), BOTTOM, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), BOTTOM, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), BOTTOM, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), REP, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), SELF, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), PEER, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), PEER, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), ANY, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), LOST, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), VPLOST, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), PEER, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - MathUtils.mapIdToMatrixEntry(target.getId(), SELF, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), VPLOST, lattice))); - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(target.getId(), SELF, lattice), - -MathUtils.mapIdToMatrixEntry(decl.getId(), REP, lattice), - MathUtils.mapIdToMatrixEntry(result.getId(), REP, lattice))); - if (!allowLost) { - resultClauses.add(VectorUtils.asVec( - -MathUtils.mapIdToMatrixEntry(decl.getId(), LOST, lattice))); - resultClauses.add(VectorUtils.asVec(-MathUtils - .mapIdToMatrixEntry(target.getId(), LOST, lattice))); - } - return resultClauses.toArray(new VecInt[resultClauses.size()]); - } - }.accept(combineConstraint.getTarget(), combineConstraint.getDeclared(), combineConstraint.getResult(), combineConstraint); - } -} diff --git a/src/universe/UniverseInferenceTests.java b/src/universe/UniverseInferenceTests.java deleted file mode 100644 index d57cb42..0000000 --- a/src/universe/UniverseInferenceTests.java +++ /dev/null @@ -1,8 +0,0 @@ -package universe; - -public class UniverseInferenceTests extends UniverseTests { - public static void main(String[] args) { - UniverseTests.checkerClass = universe.UniverseInferenceChecker.class; - UniverseTests.main(args); - } -} diff --git a/src/universe/UniverseInferenceValidator.java b/src/universe/UniverseInferenceValidator.java new file mode 100644 index 0000000..f058ef9 --- /dev/null +++ b/src/universe/UniverseInferenceValidator.java @@ -0,0 +1,94 @@ +package universe; + +import checkers.inference.InferenceValidator; +import checkers.inference.InferenceVisitor; +import com.sun.source.tree.ParameterizedTypeTree; +import com.sun.source.tree.Tree; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; +import org.checkerframework.javacutil.TreeUtils; + +import javax.lang.model.element.TypeElement; +import java.util.List; + +import static universe.UniverseAnnotationMirrorHolder.BOTTOM; +import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.REP; + +/** + * This type validator ensures correct usage of ownership modifiers or generates + * constraints to ensure well-formedness. + */ +public class UniverseInferenceValidator extends InferenceValidator { + + public UniverseInferenceValidator(BaseTypeChecker checker, + InferenceVisitor visitor, + AnnotatedTypeFactory atypeFactory) { + super(checker, visitor, atypeFactory); + } + + /** + * Ensure that only one ownership modifier is used, that ownership + * modifiers are correctly used in static contexts, and check for + * explicit use of lost. + */ + @Override + public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Tree p) { + if (checkTopLevelDeclaredOrPrimitiveType){ + checkImplicitlyBottomTypeError(type, p); + } + checkStaticRepError(type, p); + // @Peer is allowed in static context + + // This will be handled at higher level + // doesNotContain(type, LOST, "uts.explicit.lost.forbidden", p); + return super.visitDeclared(type, p); + } + + @Override + protected Void visitParameterizedType(AnnotatedTypeMirror.AnnotatedDeclaredType type, ParameterizedTypeTree tree) { + if (TreeUtils.isDiamondTree(tree)) { + return null; + } + final TypeElement element = (TypeElement) type.getUnderlyingType().asElement(); + if (checker.shouldSkipUses(element)) { + return null; + } + + List typeParamBounds = atypeFactory.typeVariablesFromUse(type, element); + for (AnnotatedTypeParameterBounds atpb : typeParamBounds) { + ((UniverseInferenceVisitor)visitor).doesNotContain(atpb.getLowerBound(), LOST, "uts.lost.in.bounds", tree); + ((UniverseInferenceVisitor)visitor).doesNotContain(atpb.getUpperBound(), LOST, "uts.lost.in.bounds", tree); + } + + return super.visitParameterizedType(type, tree); + } + + @Override + public Void visitArray(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree) { + checkStaticRepError(type, 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/universe/UniverseInferenceVisitor.java b/src/universe/UniverseInferenceVisitor.java index 44826aa..7656de7 100644 --- a/src/universe/UniverseInferenceVisitor.java +++ b/src/universe/UniverseInferenceVisitor.java @@ -1,50 +1,40 @@ package universe; -import java.util.List; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.TypeElement; -import javax.lang.model.type.DeclaredType; - -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -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; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; -import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; -import org.checkerframework.framework.util.AnnotatedTypes; -import org.checkerframework.javacutil.ElementUtils; -import org.checkerframework.javacutil.Pair; -import org.checkerframework.javacutil.TreeUtils; - +import checkers.inference.InferenceChecker; +import checkers.inference.InferenceMain; +import checkers.inference.InferenceVisitor; +import checkers.inference.SlotManager; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.ConstraintManager; +import checkers.inference.model.Slot; +import checkers.inference.model.VariableSlot; import com.sun.source.tree.AssignmentTree; -import com.sun.source.tree.BlockTree; +import com.sun.source.tree.ClassTree; import com.sun.source.tree.ExpressionTree; -import com.sun.source.tree.InstanceOfTree; import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.MethodTree; +import com.sun.source.tree.NewArrayTree; import com.sun.source.tree.NewClassTree; -import com.sun.source.tree.ParameterizedTypeTree; import com.sun.source.tree.Tree; import com.sun.source.tree.TypeCastTree; import com.sun.source.tree.VariableTree; -import com.sun.source.util.TreePath; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; +import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; +import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.javacutil.TreeUtils; -import checkers.inference.InferenceChecker; -import checkers.inference.InferenceMain; -import checkers.inference.InferenceValidator; -import checkers.inference.InferenceVisitor; -import checkers.inference.SlotManager; -import checkers.inference.model.ConstantSlot; -import checkers.inference.model.ConstraintManager; -import checkers.inference.model.Slot; -import checkers.inference.model.VariableSlot; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.type.TypeKind; + +import static universe.UniverseAnnotationMirrorHolder.ANY; +import static universe.UniverseAnnotationMirrorHolder.BOTTOM; +import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.REP; +import static universe.UniverseAnnotationMirrorHolder.SELF; /** * Type visitor to either enforce or infer the universe type rules. @@ -55,28 +45,12 @@ public class UniverseInferenceVisitor extends InferenceVisitor> fromUse = atypeFactory.constructorFromUse(node); - AnnotatedExecutableType constructor = fromUse.first; - - // Check for @Lost and @VPLost in combined parameter types. + ParameterizedExecutableType fromUse = atypeFactory.constructorFromUse(node); + AnnotatedExecutableType constructor = fromUse.executableType; + + // Check for @Lost in combined parameter types deeply. for (AnnotatedTypeMirror parameterType : constructor.getParameterTypes()) { - doesNotContain(parameterType, univATF.LOST, "uts.lost.parameter", node); - doesNotContain(parameterType, univATF.VPLOST, "uts.vplost.parameter", node); + doesNotContain(parameterType, LOST, "uts.lost.parameter", node); } - // Check for @Peer or @Rep as top-level modifier. - AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); - mainIsNoneOf(type, new AnnotationMirror[] { univATF.LOST, univATF.VPLOST, - univATF.ANY }, "uts.new.ownership", node); - - // Forbid rep in static context - if (isContextStatic(atypeFactory.getPath(node))) { - doesNotContain(type, univATF.REP, "uts.static.rep.forbidden", node); - } + checkNewInstanceCreation(node); + // There used to be code to check static rep error. But that's already moved to Validator. return super.visitNewClass(node, p); } - private static boolean isContextStatic(TreePath path) { - // TODO: test this. fields, methods, local vars, ... Checker.isValid? - MethodTree encm = TreeUtils.enclosingMethod(path); - if (encm!=null) { - // we are within a method - return ElementUtils.isStatic(TreeUtils.elementFromDeclaration(encm)); + @Override + public Void visitNewArray(NewArrayTree node, Void p) { + checkNewInstanceCreation(node); + return super.visitNewArray(node, p); + } + + private void checkNewInstanceCreation(Tree node) { + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); + // Check for @Peer or @Rep as top-level modifier. + // TODO I would say here by top-level, it's really main modifier instead of upper bounds of + // type variables, as there is no "new T()" to create a new instance. + if (UniverseTypeUtil.isImplicitlyBottomType(type)) { + effectiveIs(type, BOTTOM, "uts.new.ownership", node); } else { - VariableTree encv = TreeUtils.enclosingVariable(path); - if (encv!=null) { - // we are within a field initializer - return ElementUtils.isStatic(TreeUtils.elementFromDeclaration(encv)); - } else { - // is it a static initializer? - BlockTree encb = TreeUtils.enclosingTopLevelBlock(path); - if (encb!=null) { - return encb.isStatic(); - } else { - // We are somewhere in a class declaration already, e.g. the extends clause - // System.out.println("UniverseInferenceVisitor::isContextStatic: lost in the tree, help! Path leaf: " + path.getLeaf()); - return false; - } - } + mainIsNoneOf(type, new AnnotationMirror[] { LOST, ANY, SELF, BOTTOM }, "uts.new.ownership", node); } } @@ -222,52 +188,30 @@ private static boolean isContextStatic(TreePath path) { */ @Override public Void visitMethodInvocation(MethodInvocationTree node, Void p) { - assert node != null; - AnnotatedExecutableType method = atypeFactory.methodFromUse(node).first; - // Check for @Lost and @VPLost in combined parameter types. - for (AnnotatedTypeMirror parameterType : method.getParameterTypes()) { - doesNotContain(parameterType, univATF.LOST, "uts.lost.parameter", node); - doesNotContain(parameterType, univATF.VPLOST, "uts.lost.parameter", node); + + AnnotatedExecutableType methodType = atypeFactory.methodFromUse(node).executableType; + // Check for @Lost in combined parameter types deeply. + for (AnnotatedTypeMirror parameterType : methodType.getParameterTypes()) { + doesNotContain(parameterType, LOST, "uts.lost.parameter", node); } if (checkOaM) { - ExpressionTree recvTree = TreeUtils.getReceiverTree(node.getMethodSelect()); - if (recvTree != null) { - AnnotatedTypeMirror recvType = atypeFactory.getAnnotatedType(recvTree); - - if (recvType != null) { - ExecutableElement exelem = TreeUtils.elementFromUse(node); - if (!hasPure(exelem)) { - mainIsNoneOf(recvType, new AnnotationMirror[] {univATF.LOST, univATF.ANY}, - "oam.call.forbidden", node); + ExpressionTree receiverTree = TreeUtils.getReceiverTree(node.getMethodSelect()); + if (receiverTree != null) { + AnnotatedTypeMirror receiverType = atypeFactory.getAnnotatedType(receiverTree); + + if (receiverType != null) { + ExecutableElement methodElement = TreeUtils.elementFromUse(node); + if (!UniverseTypeUtil.isPure(methodElement)) { + mainIsNoneOf(receiverType, new AnnotationMirror[]{ LOST, ANY }, "oam.call.forbidden", node); } } } } - // TODO purity - return super.visitMethodInvocation(node, p); } - private static boolean hasPure(ExecutableElement meth) { - boolean hasPure = false; - java.util.List anns = meth.getAnnotationMirrors(); - for (AnnotationMirror an : anns) { - if (isPure(an.getAnnotationType())) { - hasPure = true; - break; - } - } - return hasPure; - } - - private static boolean isPure(DeclaredType anno) { - // TODO: Is this the simplest way to do this? - return anno.toString().equals(universe.qual.Pure.class.getName()) - || anno.toString().equals(org.jmlspecs.annotation.Pure.class.getName()); - } - /** * Validate an assignment. * @@ -278,28 +222,24 @@ private static boolean isPure(DeclaredType anno) { */ @Override public Void visitAssignment(AssignmentTree node, Void p) { - assert node != null; AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node.getVariable()); - // Check for @Lost and @VPLost in left hand side of assignment. - doesNotContain(type, univATF.LOST, "uts.lost.lhs", node); - doesNotContain(type, univATF.VPLOST, "uts.vplost.lhs", node); + // Check for @Lost in left hand side of assignment deeply. + doesNotContain(type, LOST, "uts.lost.lhs", node); if (checkOaM) { - ExpressionTree recvTree = TreeUtils.getReceiverTree(node.getVariable()); - if (recvTree != null) { - AnnotatedTypeMirror recvType = atypeFactory.getAnnotatedType(recvTree); - - if (recvType != null) { - // TODO: do we need to treat "this" and "super" specially? - mainIsNoneOf(recvType, - new AnnotationMirror[] { univATF.LOST, univATF.VPLOST, univATF.ANY }, - "oam.assignment.forbidden", node); + ExpressionTree receiverTree = TreeUtils.getReceiverTree(node.getVariable()); + if (receiverTree != null) { + AnnotatedTypeMirror receiverType = atypeFactory.getAnnotatedType(receiverTree); + + if (receiverType != null) { + // TODO: do we need to treat "this" and "super" specially? + mainIsNoneOf(receiverType, new AnnotationMirror[]{ LOST, ANY }, "oam.assignment.forbidden", node); } } } if (checkStrictPurity && true /* TODO environment pure */) { - checker.report(Result.failure("purity.assignment.forbidden"), node); + checker.reportError(node, "purity.assignment.forbidden"); } return super.visitAssignment(node, p); @@ -308,201 +248,114 @@ public Void visitAssignment(AssignmentTree node, Void p) { @Override public Void visitTypeCast(TypeCastTree node, Void p) { AnnotatedTypeMirror castty = atypeFactory.getAnnotatedType(node.getType()); - AnnotatedTypeMirror exprty = atypeFactory.getAnnotatedType(node.getExpression()); - - /* TODO: this warning will only be useful in type checking mode. - * Would it be helpful to somehow support such warnings for type inference, e.g. - * by reducing weighting? - */ - if ((AnnotatedTypes.containsModifier(castty, univATF.LOST) || - AnnotatedTypes.containsModifier(castty, univATF.VPLOST) || - AnnotatedTypes.containsModifier(castty, univATF.ANY)) && - !UniverseChecker.isAnyDefault(castty)) { - checker.report(Result.warning("uts.cast.type.warning", castty), node); - // checker.getProcessingEnvironment().getMessager().printMessage(javax.tools.Diagnostic.Kind.WARNING, - // "Casting to " + type + " is not recommended."); - } - areComparable(castty, exprty, "uts.cast.type.error", node); + // I would say casting to any IS allowed. + doesNotContain(castty, LOST, "uts.cast.type.warning", node); - // The only part from the super call that we want. - validateTypeOf(node.getType()); - - // calling super would check for cast safety... is there a different way - // to unset cast:unsafe? - return null; - // return super.visitTypeCast(node, p); + return super.visitTypeCast(node, p); } - @Override - public Void visitInstanceOf(InstanceOfTree node, Void p) { - AnnotatedTypeMirror ioty = atypeFactory.getAnnotatedType(node.getType()); - AnnotatedTypeMirror exprty = atypeFactory.getAnnotatedType(node.getExpression()); - - // TODO: See comment at casts above. - if ((AnnotatedTypes.containsModifier(ioty, univATF.LOST) || - AnnotatedTypes.containsModifier(ioty, univATF.VPLOST) || - AnnotatedTypes.containsModifier(ioty, univATF.ANY)) && - !UniverseChecker.isAnyDefault(ioty)) { - checker.report(Result.warning("uts.instanceof.type.warning", ioty), node); - // checker.getProcessingEnvironment().getMessager().printMessage(javax.tools.Diagnostic.Kind.WARNING, - // "Casting to " + type + " is not recommended."); + protected void checkTypecastSafety(TypeCastTree node, Void p) { + if (!checker.getLintOption("cast:unsafe", true)) { + return; } - - areComparable(ioty, exprty, "uts.instanceof.type.error", node); - - return super.visitInstanceOf(node, p); - } - - /* TODO: what do we want to enforce for strings? They don't really matter anyway. - @Override - public Void visitBinary(BinaryTree node, Void p) { - if (node.getKind() == Kind.PLUS || node.getKind() == Kind.PLUS_ASSIGNMENT) { - // TODO: only for Strings, but adding it for primitives shouldn't be a problem - - AnnotatedTypeMirror ltype = atypeFactory.getAnnotatedType(node.getLeftOperand()); - AnnotatedTypeMirror rtype = atypeFactory.getAnnotatedType(node.getRightOperand()); - - areEqual(ltype, rtype, "uts.append.type.error", node); + AnnotatedTypeMirror castType = atypeFactory.getAnnotatedType(node); + AnnotatedTypeMirror exprType = atypeFactory.getAnnotatedType(node.getExpression()); + + // We cannot do a simple test of casting, as isSubtypeOf requires + // the input types to be subtypes according to Java + if (!isTypeCastSafe(castType, exprType, node)) { + // This is only warning message, so even though enterred this line, it doesn't cause inference to exit. + checker.reportWarning(node, "cast.unsafe", exprType.toString(true), castType.toString(true)); } - return super.visitBinary(node, p); } - */ - /* TODO Do I really need this? - @Override - protected void checkTypeArguments(Tree t, - java.util.List typevars, - java.util.List typeargs, - java.util.List typeargTrees) { - super.checkTypeArguments(t, typevars, typeargs, typeargTrees); + private boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, TypeCastTree node) { + if (infer) { + return isCompatibleCastInInfer(castType, exprType, node); + } else { + // Typechecking side standard implementation - warns if not upcasting + return super.isTypeCastSafe(castType, exprType); + } } - */ - /** - * This type validator ensures correct usage of ownership modifiers. - */ - private final class UniverseInferenceValidator extends InferenceValidator { - public UniverseInferenceValidator(BaseTypeChecker checker, - InferenceVisitor visitor, - // UniverseAnnotatedTypeFactory atypeFactory) { - // Is it correct? Only debugging. - AnnotatedTypeFactory atypeFactory) { - - super(checker, visitor, atypeFactory); - // System.out.println("atypeFactory in constructor: " + - // atypeFactory); + private boolean isCompatibleCastInInfer(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, TypeCastTree node) { + // TODO: Can be shifted to CFI? + // comparablecast + final QualifierHierarchy qualHierarchy = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy(); + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + final Slot castSlot = slotManager.getSlot(castType); + final Slot exprSlot = slotManager.getSlot(exprType); + + if (castSlot instanceof ConstantSlot && exprSlot instanceof ConstantSlot) { + ConstantSlot castCSSlot = (ConstantSlot) castSlot; + ConstantSlot exprCSSlot = (ConstantSlot) exprSlot; + // Special handling for case with two ConstantSlots: even though they may not be comparable, + // but to infer more program, let this case fall back to "anycast" silently and continue + // inference. + return qualHierarchy.isSubtype(castCSSlot.getValue(), exprCSSlot.getValue()) + || qualHierarchy.isSubtype(exprCSSlot.getValue(), castCSSlot.getValue()); + } else { + // But if there is at least on Slot, inference guarantees that solutions don't include + // incomparable casts. + areComparable(castType, exprType, "uts.cast.type.error", node); + return true; } + } - /** - * Ensure that only one ownership modifier is used, that ownership - * modifiers are correctly used in static contexts, and check for - * explicit use of lost. - */ - @Override - public Void visitDeclared(AnnotatedDeclaredType type, Tree p) { - // System.out.println("==========visitDeclared in UniverseInferenceValidator is called!"); - // System.out.println( - // "UniverseInferenceValidator: visitDeclared is called!"); - // ModifiersTree mt = ((VariableTree) p).getModifiers(); - // if (mt.getFlags().contains(Modifier.STATIC)) { - // System.out.println("\n========p is: " + p); - //System.out.println("p is null: " + p == null); - // System.out.println("atypeFactory is null: "); - // System.out.println(atypeFactory == null); - // System.out.println("----------------atypeFactory.getPath(p) is: " - // + atypeFactory.getPath(p)); - if (UniverseInferenceVisitor.isContextStatic(atypeFactory.getPath(p))) { - doesNotContain(type, univATF.REP, "uts.static.rep.forbidden", p); - - if (warn_staticpeer) { - // TODO: I would really like to only give the warning if - // the modifier was explicit. - // TODO: Only want a warning, not an error. - doesNotContain(type, univATF.PEER, "uts.static.peer.warning", p); + @Override + public boolean validateTypeOf(Tree tree) { + AnnotatedTypeMirror type; + // It's quite annoying that there is no TypeTree + switch (tree.getKind()) { + case PRIMITIVE_TYPE: + case PARAMETERIZED_TYPE: + case TYPE_PARAMETER: + case ARRAY_TYPE: + case UNBOUNDED_WILDCARD: + case EXTENDS_WILDCARD: + case SUPER_WILDCARD: + case ANNOTATED_TYPE: + type = atypeFactory.getAnnotatedTypeFromTypeTree(tree); + break; + case METHOD: + type = atypeFactory.getMethodReturnType((MethodTree) tree); + if (type == null || + type.getKind() == TypeKind.VOID) { + // Nothing to do for void methods. + // Note that for a constructor the AnnotatedExecutableType does + // not use void as return type. + return true; } - } - - if (!allowLost) { - doesNotContain(type, univATF.LOST, "uts.explicit.lost.forbidden", p); - doesNotContain(type, univATF.VPLOST, "uts.explicit.lost.forbidden", p); - } - // Me: Is it allowed to have multiple universe modifiers? What does - // it mean? - if (type.getAnnotations().size() > 2) { - System.out.println( - "UniverseVisitor$UniverseInferenceValidator: Don't know if it's correct: type is: " - + type); - reportError(type, p); - } - // System.out.println("super.visitDeclared for: " + type); - // System.out.println("Reached super call!"); - return super.visitDeclared(type, p); + break; + default: + type = atypeFactory.getAnnotatedType(tree); } - @Override - protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedTypeTree tree) { - // For debuggin purpose, move the last line to here - // return super.visitParameterizedType(type, tree); - // System.out.println( - // "UniverseInferenceVaildator: visitParameterizedType is called!"); - - final TypeElement element = (TypeElement) type.getUnderlyingType().asElement(); - List typeParamBounds = atypeFactory.typeVariablesFromUse(type, element); - for (AnnotatedTypeParameterBounds atpb : typeParamBounds) { - doesNotContain(atpb.getLowerBound(), univATF.LOST, "uts.lost.in.bounds", tree); - doesNotContain(atpb.getUpperBound(), univATF.LOST, "uts.lost.in.bounds", tree); - doesNotContain(atpb.getLowerBound(), univATF.VPLOST, "uts.vplost.in.bounds", tree); - doesNotContain(atpb.getUpperBound(), univATF.VPLOST, "uts.vplost.in.bounds", tree); - } - for(AnnotatedTypeMirror atm: type.getTypeArguments()){ - doesNotContain(atm, univATF.LOST,"uts.lost.in.type.arguments",tree); - doesNotContain(atm, univATF.VPLOST,"uts.lost.in.type.arguments",tree); - } - // For debugging purpose, move the following line to first. To see if super not overridden - // method works or not. - // Overriding a method doesn't necessarily mean that it has not - // relationship with super method. If overriding version constains - // super.method, then we need to look at the super method's - // source code too! - return super.visitParameterizedType(type, tree); - // return null; - } + return validateType(tree, type); + } - /** - * Forbid explicit annotations on primitive types. - */ - @Override - public Void visitPrimitive(AnnotatedPrimitiveType type, Tree p) { - if (type.isAnnotatedInHierarchy(univATF.ANY)) { - Set ann = type.getAnnotations(); - if (ann.size() > 1 - || (ann.size() == 1 && !ann.contains(univATF.BOTTOM))) { - // the implicit default is BOTTOM, which cannot be used - // explicitly. - // if there are explicit annotations -> error. - reportError(type, p); - } - } - return super.visitPrimitive(type, p); - } + // TODO This might not be correct for infer mode. Maybe returning as it is + @Override + public boolean validateType(Tree tree, AnnotatedTypeMirror type) { - /** - * Each array dimension can only use at most one ownership modifier. The - * check of the component type is done by the super method. - */ - @Override - public Void visitArray(AnnotatedArrayType type, Tree p) { - if (type.getAnnotations().size() > 1) { - // only one Universe modifier is allowed on the array - reportError(type, p); + if (!typeValidator.isValid(type, tree)) { + if (!infer) { + return false; } - return super.visitArray(type, p); } - /* - @Override - protected void checkValidUse(AnnotatedDeclaredType type, Tree tree) { - return;// Doesn't check valid use of type in Generic Universe type system - }*/ + // The initial purpose of always returning true in validateTypeOf in inference mode + // might be that inference we want to generate constraints over all the ast location, + // but not like in typechecking mode, if something is not valid, we abort checking the + // remaining parts that are based on the invalid type. For example, in assignment, if + // rhs is not valid, we don't check the validity of assignment. But in inference, + // we always generate constraints on all places and let solver to decide if there is + // solution or not. This might be the reason why we have a always true if statement and + // validity check always returns true. + return true; } + + @Override + // Universe Type System does not need to check extends and implements + protected void checkExtendsImplements(ClassTree classTree) {} } diff --git a/src/universe/UniverseTypeUtil.java b/src/universe/UniverseTypeUtil.java new file mode 100644 index 0000000..b685e6f --- /dev/null +++ b/src/universe/UniverseTypeUtil.java @@ -0,0 +1,113 @@ +package universe; + +import checkers.inference.InferenceMain; +import checkers.inference.SlotManager; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.ConstraintManager; +import checkers.inference.model.Slot; +import com.sun.source.tree.ClassTree; +import com.sun.source.util.TreePath; +import org.checkerframework.framework.qual.DefaultFor; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TypesUtils; +import universe.qual.Bottom; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.type.DeclaredType; +import javax.lang.model.type.TypeKind; +import java.util.Arrays; +import java.util.List; + +public class UniverseTypeUtil { + + private static boolean isInTypesOfImplicitForOfBottom(AnnotatedTypeMirror atm) { + DefaultFor defaultFor = Bottom.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + assert defaultFor.typeKinds() != null; + for (org.checkerframework.framework.qual.TypeKind typeKind : defaultFor.typeKinds()) { + if (TypeKind.valueOf(typeKind.name()) == atm.getKind()) return true; + } + return false; + } + + private static boolean isInTypeNamesOfImplicitForOfBottom(AnnotatedTypeMirror atm) { + if (atm.getKind() != TypeKind.DECLARED) { + return false; + } + DefaultFor defaultFor = Bottom.class.getAnnotation(DefaultFor.class); + assert defaultFor != null; + assert defaultFor.types() != null; + Class[] typeNames = defaultFor.types(); + String fqn = TypesUtils.getQualifiedName((DeclaredType) atm.getUnderlyingType()).toString(); + for (int i = 0; i < typeNames.length; i++) { + if (typeNames[i].getCanonicalName().toString().contentEquals(fqn)) return true; + } + return false; + } + + public static boolean isImplicitlyBottomType(AnnotatedTypeMirror atm) { + return isInTypesOfImplicitForOfBottom(atm) || isInTypeNamesOfImplicitForOfBottom(atm); + } + + public static void applyConstant(AnnotatedTypeMirror type, AnnotationMirror am) { + SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + ConstraintManager constraintManager = InferenceMain.getInstance().getConstraintManager(); + // 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.getSlot(type); + ConstantSlot constant = slotManager.createConstantSlot(am); + if (shouldBeAppliedTo == null) { + type.addAnnotation(slotManager.getAnnotation(constant)); + } else { + constraintManager.addEqualityConstraint(shouldBeAppliedTo, constant); + } + } + + private static boolean isPure(DeclaredType anno) { + return anno.toString().equals(universe.qual.Pure.class.getName()) + || anno.toString().equals(org.jmlspecs.annotation.Pure.class.getName()); + } + + public static boolean isPure(ExecutableElement executableElement) { + boolean hasPure = false; + List anns = executableElement.getAnnotationMirrors(); + for (AnnotationMirror an : anns) { + if (isPure(an.getAnnotationType())) { + hasPure = true; + break; + } + } + return hasPure; + } + + public static AnnotationMirror createEquivalentVarAnnotOfRealQualifier(final AnnotationMirror am) { + final SlotManager slotManager = InferenceMain.getInstance().getSlotManager(); + ConstantSlot constantSlot = slotManager.createConstantSlot(am); + return slotManager.getAnnotation(constantSlot); + } + + public static boolean inStaticScope(TreePath treePath) { + boolean in = false; + if (TreePathUtil.isTreeInStaticScope(treePath)) { + in = true; + // Exclude case in which enclosing class is static + ClassTree classTree = TreePathUtil.enclosingClass(treePath); + if (classTree != null && classTree.getModifiers().getFlags().contains((Modifier.STATIC))) { + in = false; + } + } + return in; + } + + public static void defaultConstructorReturnToSelf(Element elt, AnnotatedTypeMirror type) { + if (elt.getKind() == ElementKind.CONSTRUCTOR && type instanceof AnnotatedTypeMirror.AnnotatedExecutableType) { + ((AnnotatedTypeMirror.AnnotatedExecutableType) type).getReturnType().addMissingAnnotations(Arrays.asList(UniverseAnnotationMirrorHolder.SELF)); + } + } +} diff --git a/src/universe/UniverseTypeValidator.java b/src/universe/UniverseTypeValidator.java new file mode 100644 index 0000000..827bcf2 --- /dev/null +++ b/src/universe/UniverseTypeValidator.java @@ -0,0 +1,100 @@ +package universe; + +import com.sun.source.tree.ParameterizedTypeTree; +import com.sun.source.tree.Tree; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeValidator; +import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; +import org.checkerframework.framework.util.AnnotatedTypes; +import org.checkerframework.javacutil.TreeUtils; + +import javax.lang.model.element.TypeElement; +import java.util.List; + +import static universe.UniverseAnnotationMirrorHolder.BOTTOM; +import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.REP; + +/** + * This type validator ensures correct usage of ownership modifiers + * to ensure well-formedness. + */ +public class UniverseTypeValidator extends BaseTypeValidator{ + + public UniverseTypeValidator(BaseTypeChecker checker, BaseTypeVisitor visitor, AnnotatedTypeFactory atypeFactory) { + super(checker, visitor, atypeFactory); + } + + /** + * Ensure that only one ownership modifier is used, that ownership + * modifiers are correctly used in static contexts, and check for + * explicit use of lost. + */ + @Override + public Void visitDeclared(AnnotatedTypeMirror.AnnotatedDeclaredType type, Tree p) { + if (checkTopLevelDeclaredOrPrimitiveType){ + checkImplicitlyBottomTypeError(type, p); + } + checkStaticRepError(type, p); + // @Peer is allowed in static context + + // This will be handled at higher level + // doesNotContain(type, LOST, "uts.explicit.lost.forbidden", p); + return super.visitDeclared(type, p); + } + + @Override + protected Void visitParameterizedType(AnnotatedTypeMirror.AnnotatedDeclaredType type, ParameterizedTypeTree tree) { + if (TreeUtils.isDiamondTree(tree)) { + return null; + } + final TypeElement element = (TypeElement) type.getUnderlyingType().asElement(); + if (checker.shouldSkipUses(element)) { + return null; + } + + List typeParamBounds = atypeFactory.typeVariablesFromUse(type, element); + for (AnnotatedTypeParameterBounds atpb : typeParamBounds) { + // Previously, here also checks two bounds are not TypeKind.NULL. What's the reason? + if ((AnnotatedTypes.containsModifier(atpb.getUpperBound(), LOST)) || + AnnotatedTypes.containsModifier(atpb.getLowerBound(), LOST)) { + checker.reportError(tree, "uts.lost.in.bounds", atpb.toString(), type.toString()); + } + } + + return super.visitParameterizedType(type, tree); + } + + @Override + public Void visitArray(AnnotatedTypeMirror.AnnotatedArrayType type, Tree tree) { + checkStaticRepError(type, 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)) { + checker.reportError(tree, "uts.static.rep.forbidden", type.getAnnotations(), type.toString()); + } + } + } + + private void checkImplicitlyBottomTypeError(AnnotatedTypeMirror type, Tree tree) { + if (UniverseTypeUtil.isImplicitlyBottomType(type)) { + if (!type.hasAnnotation(BOTTOM)) { + reportInvalidAnnotationsOnUse(type, tree); + } + } + } +} diff --git a/src/universe/UniverseViewpointAdapter.java b/src/universe/UniverseViewpointAdapter.java new file mode 100644 index 0000000..cb7b042 --- /dev/null +++ b/src/universe/UniverseViewpointAdapter.java @@ -0,0 +1,59 @@ +package universe; + +import static universe.UniverseAnnotationMirrorHolder.ANY; +import static universe.UniverseAnnotationMirrorHolder.BOTTOM; +import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.PEER; +import static universe.UniverseAnnotationMirrorHolder.REP; +import static universe.UniverseAnnotationMirrorHolder.SELF; + +import javax.lang.model.element.AnnotationMirror; + +import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; + +public class UniverseViewpointAdapter extends AbstractViewpointAdapter { + + public UniverseViewpointAdapter(AnnotatedTypeFactory atypeFactory) { + super(atypeFactory); + } + + @Override + protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { + assert atm != null; + return atm.getAnnotationInHierarchy(ANY); + } + + @Override + protected AnnotationMirror combineAnnotationWithAnnotation(AnnotationMirror receiverAnnotation, + AnnotationMirror declaredAnnotation) { + assert receiverAnnotation != null; + assert declaredAnnotation != null; + + if (AnnotationUtils.areSame(receiverAnnotation, SELF)) { + return declaredAnnotation; + } else if (AnnotationUtils.areSame(declaredAnnotation, BOTTOM)) { + return BOTTOM; + } else if (AnnotationUtils.areSame(declaredAnnotation, ANY)) { + return ANY; + } else if (AnnotationUtils.areSame(declaredAnnotation, SELF)) { + return receiverAnnotation; + } else if (AnnotationUtils.areSame(receiverAnnotation, BOTTOM)) { + // If receiver is bottom, has no ownership information. Any member + // of it from the viewpoint of self is any, except when declared + // type is bottom. + return ANY; + } else if (AnnotationUtils.areSame(declaredAnnotation, LOST)) { + return LOST; + } else if (AnnotationUtils.areSame(declaredAnnotation, PEER)) { + if (AnnotationUtils.areSame(receiverAnnotation, PEER)) { + return PEER; + } else if (AnnotationUtils.areSame(receiverAnnotation, REP)) { + return REP; + } + } + return LOST; + } +} diff --git a/src/universe/UniverseViewpointAdaptor.java b/src/universe/UniverseViewpointAdaptor.java deleted file mode 100644 index 18acabb..0000000 --- a/src/universe/UniverseViewpointAdaptor.java +++ /dev/null @@ -1,82 +0,0 @@ -package universe; - - -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; -import javax.lang.model.element.ElementKind; -import javax.lang.model.type.TypeKind; - -import org.checkerframework.framework.type.AnnotatedTypeFactory; -import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.util.FrameworkViewpointAdaptor; -import org.checkerframework.javacutil.AnnotationUtils; - -public class UniverseViewpointAdaptor extends FrameworkViewpointAdaptor{ - - @Override - protected AnnotationMirror getModifier(AnnotatedTypeMirror atm, AnnotatedTypeFactory f) { - assert atm != null; - UniverseAnnotatedTypeFactory univATF = (UniverseAnnotatedTypeFactory)f; - - if (atm.hasEffectiveAnnotation(univATF.PEER)) { - return univATF.PEER; - } - if (atm.hasEffectiveAnnotation(univATF.REP)) { - return univATF.REP; - } - if (atm.hasEffectiveAnnotation(univATF.ANY)) { - return univATF.ANY; - } - if (atm.hasEffectiveAnnotation(univATF.SELF)) { - return univATF.SELF; - } - if(atm.hasEffectiveAnnotation(univATF.BOTTOM)){ - return univATF.BOTTOM; - } - if (atm.hasEffectiveAnnotation(univATF.VPLOST)) { - return univATF.VPLOST; - } - if (atm.hasEffectiveAnnotation(univATF.LOST)) { - return univATF.LOST; - } - return null; - } - - @Override - protected AnnotationMirror combineModifierWithModifier(AnnotationMirror recvModifier, AnnotationMirror declModifier, - AnnotatedTypeFactory f) { - assert recvModifier != null; - assert declModifier != null; - - UniverseAnnotatedTypeFactory univATF = (UniverseAnnotatedTypeFactory)f; - if (AnnotationUtils.areSame(recvModifier, univATF.SELF)) { - return declModifier; - } else if (AnnotationUtils.areSame(recvModifier, univATF.PEER) && - AnnotationUtils.areSame(declModifier, univATF.PEER)) { - return univATF.PEER; - } else if (AnnotationUtils.areSame(recvModifier, univATF.REP) && - AnnotationUtils.areSame(declModifier, univATF.PEER)) { - return univATF.REP; - } else if (AnnotationUtils.areSame(declModifier, univATF.ANY)) { - return univATF.ANY; - } else if (AnnotationUtils.areSame(declModifier, univATF.LOST)) { - return univATF.VPLOST;// Always use internal representation of lost - @VPLost - } else if (AnnotationUtils.areSame(declModifier, univATF.BOTTOM)) { - return univATF.BOTTOM; - } else { - return univATF.VPLOST; - } - } - - @Override - public boolean shouldBeAdapted(AnnotatedTypeMirror type, Element element) { - if (type.getKind() != TypeKind.DECLARED && type.getKind() != TypeKind.ARRAY) { - return false; - } - if (element.getKind() == ElementKind.LOCAL_VARIABLE - || element.getKind() == ElementKind.PARAMETER) { - return false; - } - return true; - } -} diff --git a/src/universe/UniverseVisitor.java b/src/universe/UniverseVisitor.java index fa7ad08..53bbd3f 100644 --- a/src/universe/UniverseVisitor.java +++ b/src/universe/UniverseVisitor.java @@ -1,82 +1,61 @@ package universe; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.common.basetype.BaseTypeValidator; +import com.sun.source.tree.AssignmentTree; +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.NewArrayTree; +import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.TypeCastTree; +import com.sun.source.tree.VariableTree; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeVisitor; -import org.checkerframework.framework.source.Result; -import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeFactory.ParameterizedExecutableType; import org.checkerframework.framework.type.AnnotatedTypeMirror; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; -import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; -import org.checkerframework.framework.type.AnnotatedTypeParameterBounds; import org.checkerframework.framework.util.AnnotatedTypes; -import org.checkerframework.javacutil.ElementUtils; -import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; -import java.util.List; -import java.util.Set; - -import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.Modifier; -import javax.lang.model.element.TypeElement; -import javax.lang.model.type.DeclaredType; import javax.lang.model.type.TypeKind; -import com.sun.source.tree.AssignmentTree; -import com.sun.source.tree.BlockTree; -import com.sun.source.tree.ExpressionTree; -import com.sun.source.tree.MethodInvocationTree; -import com.sun.source.tree.MethodTree; -import com.sun.source.tree.ModifiersTree; -import com.sun.source.tree.NewClassTree; -import com.sun.source.tree.ParameterizedTypeTree; -import com.sun.source.tree.Tree; -import com.sun.source.tree.Tree.Kind; -import com.sun.source.tree.TypeCastTree; -import com.sun.source.tree.VariableTree; +import static universe.UniverseAnnotationMirrorHolder.ANY; +import static universe.UniverseAnnotationMirrorHolder.BOTTOM; +import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.PEER; +import static universe.UniverseAnnotationMirrorHolder.REP; +import static universe.UniverseAnnotationMirrorHolder.SELF; /** - * Type visitor to enforce the universe type rules. + * Type visitor to either enforce or infer the universe type rules. * * @author wmdietl */ public class UniverseVisitor extends BaseTypeVisitor { - public final boolean checkOaM; - public final boolean checkStrictPurity; - public final boolean allowLost; - public final boolean warn_staticpeer; + private final boolean checkOaM; + private final boolean checkStrictPurity; - public UniverseVisitor(BaseTypeChecker checker) { - super(checker); + public UniverseVisitor(UniverseChecker checker, BaseAnnotatedTypeFactory factory) { + super(checker, (UniverseAnnotatedTypeFactory) factory); - this.allowLost = checker.getLintOption("allowLost", false); - this.checkOaM = checker.getLintOption("checkOaM", false); - this.checkStrictPurity = checker.getLintOption("checkStrictPurity", false); - String warn = checker.getOption("warn", ""); - warn_staticpeer = warn.contains("staticpeer"); + checkOaM = checker.getLintOption("checkOaM", false); + checkStrictPurity = checker.getLintOption("checkStrictPurity", false); } /** * The type validator to ensure correct usage of ownership modifiers. */ @Override - protected BaseTypeValidator createTypeValidator() { + protected UniverseTypeValidator createTypeValidator() { return new UniverseTypeValidator(checker, this, atypeFactory); } - /** - * The supermethod is currently OK, it only checks for a subtype relationship between the erased types. - * Depends on what we use as default modifier. Super meth is ok for Any default, but not for peer. - * TODO Is this really correct? - */ @Override - public boolean isValidUse(AnnotatedDeclaredType elemType, AnnotatedDeclaredType use, Tree tree) { - // return super.isValidUse(elemType, use, tree); + public boolean isValidUse(AnnotatedDeclaredType declarationType, AnnotatedDeclaredType useType, Tree tree) { return true; } @@ -84,35 +63,71 @@ public boolean isValidUse(AnnotatedDeclaredType elemType, AnnotatedDeclaredType * Ignore method receiver annotations. */ @Override - protected void checkMethodInvocability(AnnotatedExecutableType method, - MethodInvocationTree node) { + protected void checkMethodInvocability(AnnotatedExecutableType method, MethodInvocationTree node) { return; } /** - * Universe type checking does not use receiver annotations, forbid them. + * Ignore constructor receiver annotations. */ @Override - public Void visitMethod(MethodTree node, Void p) { - // System.out.println("MethodTree: " + node); + protected void checkConstructorInvocation(AnnotatedDeclaredType dt, + AnnotatedExecutableType constructor, NewClassTree src) {} - if (node.getReceiverParameter() != null && - !node.getReceiverParameter().getModifiers().getAnnotations() - .isEmpty()) { - checker.report(Result.failure("uts.receiver.annotations.forbidden"),node); + @Override + public Void visitVariable(VariableTree node, Void p) { + return super.visitVariable(node, p); } + /** + * Universe does not use receiver annotations, forbid them. + */ + @Override + public Void visitMethod(MethodTree node, Void p) { + AnnotatedExecutableType executableType = atypeFactory.getAnnotatedType(node); + + if (TreeUtils.isConstructor(node)) { + AnnotatedDeclaredType constructorReturnType = (AnnotatedDeclaredType) executableType.getReturnType(); + if (!constructorReturnType.hasAnnotation(SELF)) { + checker.reportError(node, "uts.constructor.not.self"); + } + } else { + AnnotatedDeclaredType declaredReceiverType = executableType.getReceiverType(); + if (declaredReceiverType != null) { + if (!declaredReceiverType.hasAnnotation(SELF)) { + checker.reportError(node, "uts.receiver.not.self"); + } + } + } return super.visitMethod(node, p); } + @Override + protected OverrideChecker createOverrideChecker( + Tree overriderTree, AnnotatedExecutableType overrider,AnnotatedTypeMirror overridingType, + AnnotatedTypeMirror overridingReturnType, AnnotatedExecutableType overridden, AnnotatedDeclaredType overriddenType, AnnotatedTypeMirror overriddenReturnType) { + + return new OverrideChecker( + overriderTree, + overrider, + overridingType, + overridingReturnType, + overridden, + overriddenType, + overriddenReturnType) { + @Override + protected boolean checkReceiverOverride() { + return true; + } + }; + } + /** - * Ignore constructor receiver annotations. + * There is no need to issue a warning if the result type of the constructor is not top in Universe. */ @Override - protected boolean checkConstructorInvocation(AnnotatedDeclaredType dt, - AnnotatedExecutableType constructor, NewClassTree src) { - return true; - } + protected void checkConstructorResult( + AnnotatedTypeMirror.AnnotatedExecutableType constructorType, ExecutableElement constructorElement) {} /** * Validate a new object creation. @@ -124,53 +139,42 @@ protected boolean checkConstructorInvocation(AnnotatedDeclaredType dt, */ @Override public Void visitNewClass(NewClassTree node, Void p) { - assert node != null; - - Pair> fromUse = atypeFactory.constructorFromUse(node); - AnnotatedExecutableType constructor = fromUse.first; + ParameterizedExecutableType fromUse = atypeFactory.constructorFromUse(node); + AnnotatedExecutableType constructor = fromUse.executableType; - // Check for @Lost and @VPLost in combined parameter types. + // Check for @Lost in combined parameter types deeply. for (AnnotatedTypeMirror parameterType : constructor.getParameterTypes()) { - if (AnnotatedTypes.containsModifier(parameterType, atypeFactory.LOST)) { - checker.report(Result.failure("uts.lost.parameter"), node); - } else if (AnnotatedTypes.containsModifier(parameterType, atypeFactory.VPLOST)) { - checker.report(Result.failure("uts.vplost.parameter"), node); + if (AnnotatedTypes.containsModifier(parameterType, LOST)) { + checker.reportError(node, "uts.lost.parameter"); } } - // Check for @Peer or @Rep as top-level modifier. - AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); - if (!(type.hasEffectiveAnnotation(atypeFactory.PEER) || type.hasEffectiveAnnotation(atypeFactory.REP))) { - checker.report(Result.failure("uts.new.ownership"), node); - } - - // Forbid @Rep in static context - if (isInStaticContext() && type.hasEffectiveAnnotation(atypeFactory.REP)) { - checker.report(Result.failure("uts.static.rep.forbidden"), node); - } + checkNewInstanceCreation(node); + // There used to be code to check static rep error. But that's already moved to Validator. return super.visitNewClass(node, p); } - private boolean isInStaticContext(){ - boolean isstatic = false; - MethodTree meth = TreeUtils.enclosingMethod(getCurrentPath()); - if(meth != null){ - ExecutableElement methel = TreeUtils.elementFromDeclaration(meth); - isstatic = ElementUtils.isStatic(methel); + @Override + public Void visitNewArray(NewArrayTree node, Void p) { + checkNewInstanceCreation(node); + return super.visitNewArray(node, p); + } + + private void checkNewInstanceCreation(Tree node) { + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); + // Check for @Peer or @Rep as top-level modifier. + // TODO I would say here by top-level, it's really main modifier instead of upper bounds of + // type variables, as there is no "new T()" to create a new instance. + if (UniverseTypeUtil.isImplicitlyBottomType(type)) { + if (!type.hasAnnotation(BOTTOM)) { + checker.reportError(node, "uts.new.ownership"); + } } else { - VariableTree vartree = TreeUtils.enclosingVariable(getCurrentPath()); - if (vartree != null) { - ModifiersTree mt = vartree.getModifiers(); - isstatic = mt.getFlags().contains(Modifier.STATIC); - } else { - BlockTree blcktree = TreeUtils.enclosingTopLevelBlock(getCurrentPath()); - if (blcktree != null) { - isstatic = blcktree.isStatic(); - } + if (!(type.hasAnnotation(PEER) || type.hasAnnotation(REP))) { + checker.reportError(node, "uts.new.ownership"); } } - return isstatic; } /** @@ -183,52 +187,36 @@ private boolean isInStaticContext(){ */ @Override public Void visitMethodInvocation(MethodInvocationTree node, Void p) { - assert node != null; - - AnnotatedExecutableType method = atypeFactory.methodFromUse(node).first; - // Check for @VPLost in combined parameter types. - for (AnnotatedTypeMirror parameterType : method.getParameterTypes()) { - if (AnnotatedTypes.containsModifier(parameterType, atypeFactory.LOST)) { - checker.report(Result.failure("uts.lost.parameter"), node); - } else if (AnnotatedTypes.containsModifier(parameterType, atypeFactory.VPLOST)) { - checker.report(Result.failure("uts.vplost.parameter"), node); + AnnotatedExecutableType methodType = atypeFactory.methodFromUse(node).executableType; + // Check for @Lost in combined parameter types deeply. + for (AnnotatedTypeMirror parameterType : methodType.getParameterTypes()) { + if (AnnotatedTypes.containsModifier(parameterType, LOST)) { + checker.reportError(node, "uts.lost.parameter"); } } if (checkOaM) { - ExpressionTree recvTree = TreeUtils.getReceiverTree(node.getMethodSelect()); - if (recvTree != null) { - AnnotatedTypeMirror recvType = atypeFactory.getAnnotatedType(recvTree); - if (recvType.hasEffectiveAnnotation(atypeFactory.LOST) || - recvType.hasEffectiveAnnotation(atypeFactory.VPLOST) || - recvType.hasEffectiveAnnotation(atypeFactory.ANY)) { - ExecutableElement exelem = TreeUtils.elementFromUse(node); - java.util.List anns = exelem.getAnnotationMirrors(); - - // purity - boolean hasPure = false; - for (AnnotationMirror an : anns) { - if (isPure(an.getAnnotationType())) { - hasPure = true; - } - } - if (anns.isEmpty() || !hasPure) { - checker.report(Result.failure("oam.call.forbidden"), node); + ExpressionTree receiverTree = TreeUtils.getReceiverTree(node.getMethodSelect()); + if (receiverTree != null) { + AnnotatedTypeMirror receiverType = atypeFactory.getAnnotatedType(receiverTree); + + if (receiverType != null) { + ExecutableElement methodElement = TreeUtils.elementFromUse(node); + if (!UniverseTypeUtil.isPure(methodElement)) { + // I would say this non-lost and non-any restriction is really for declared + // types, not for type variables. As type variables can't have methods to invoke. + if (receiverType.hasAnnotation(LOST) || receiverType.hasAnnotation(ANY)) { + checker.reportError(node, "oam.call.forbidden"); } } + } } } return super.visitMethodInvocation(node, p); } - private boolean isPure(DeclaredType anno) { - // TODO: Is this the simplest way to do this? - return anno.toString().equals(universe.qual.Pure.class.getName()) - || anno.toString().equals(org.jmlspecs.annotation.Pure.class.getName()); - } - /** * Validate an assignment. * @@ -239,33 +227,29 @@ private boolean isPure(DeclaredType anno) { */ @Override public Void visitAssignment(AssignmentTree node, Void p) { - assert node != null; - - // Check for @Lost and @VPLost in left hand side of assignment. AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node.getVariable()); - if (AnnotatedTypes.containsModifier(type, atypeFactory.LOST)) { - checker.report(Result.failure("uts.lost.lhs"), node); - } else if (AnnotatedTypes.containsModifier(type, atypeFactory.VPLOST)) { - checker.report(Result.failure("uts.vplost.lhs"), node); + // Check for @Lost in left hand side of assignment deeply. + if (AnnotatedTypes.containsModifier(type, LOST)) { + checker.reportError(node, "uts.lost.lhs"); } if (checkOaM) { - ExpressionTree recvTree = TreeUtils.getReceiverTree(node.getVariable()); - if (recvTree != null) { - AnnotatedTypeMirror recvType = atypeFactory.getAnnotatedType(recvTree); - - if (recvType != null) { - if (recvType.hasEffectiveAnnotation(atypeFactory.LOST) || - recvType.hasEffectiveAnnotation(atypeFactory.VPLOST) - || recvType.hasEffectiveAnnotation(atypeFactory.ANY)) { - checker.report(Result.failure("oam.assignment.forbidden"), node); + ExpressionTree receiverTree = TreeUtils.getReceiverTree(node.getVariable()); + if (receiverTree != null) { + AnnotatedTypeMirror receiverType = atypeFactory.getAnnotatedType(receiverTree); + + if (receiverType != null) { + // Still, I think receiver can still only be declared types, so effectiveAnnotation + // is not needed. + if (receiverType.hasAnnotation(LOST) || receiverType.hasAnnotation(ANY)) { + checker.reportError(node, "oam.assignment.forbidden"); } } } } - if (checkStrictPurity && true /*TODO environment pure*/) { - checker.report(Result.failure("purity.assignment.forbidden"), node); + if (checkStrictPurity && true /* TODO environment pure */) { + checker.reportError(node, "purity.assignment.forbidden"); } return super.visitAssignment(node, p); @@ -273,120 +257,82 @@ public Void visitAssignment(AssignmentTree node, Void p) { @Override public Void visitTypeCast(TypeCastTree node, Void p) { - AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node.getType()); + AnnotatedTypeMirror castty = atypeFactory.getAnnotatedType(node.getType()); - if ((AnnotatedTypes.containsModifier(type, atypeFactory.LOST) - || AnnotatedTypes.containsModifier(type, atypeFactory.VPLOST) - || AnnotatedTypes.containsModifier(type, atypeFactory.ANY)) - && !UniverseChecker.isAnyDefault(type)) { - checker.report(Result.warning("uts.cast.type.warning", type), node); + if ((AnnotatedTypes.containsModifier(castty, LOST))) { + checker.reportWarning(node, "uts.cast.type.warning", castty); } - // The only part from the super call that we want. - validateTypeOf(node.getType()); - - // calling super would check for cast safety... is there a different way - // to unset cast:unsafe? - return null; - // return super.visitTypeCast(node, p); + return super.visitTypeCast(node, p); } - /** - * This type validator ensures correct usage of ownership modifiers. - * It must be run before implicits/defaults, because it should only - * validate explicitly written qualifiers. - * TODO The above statement is incorrect. Defaults are already applied. - */ - private final class UniverseTypeValidator extends BaseTypeValidator { - - public UniverseTypeValidator(BaseTypeChecker checker, - BaseTypeVisitor visitor, AnnotatedTypeFactory atypeFactory) { - super(checker, visitor, atypeFactory); + protected void checkTypecastSafety(TypeCastTree node, Void p) { + if (!checker.getLintOption("cast:unsafe", true)) { + return; } + AnnotatedTypeMirror castType = atypeFactory.getAnnotatedType(node); + AnnotatedTypeMirror exprType = atypeFactory.getAnnotatedType(node.getExpression()); - /** - * Ensure that only one ownership modifier is used, that ownership - * modifiers are correctly used in static contexts, and check for - * explicit use of lost. - */ - @Override - public Void visitDeclared(AnnotatedDeclaredType type, Tree p) { - if (p.getKind() == Kind.VARIABLE) { - if (isInStaticContext()) { - if (AnnotatedTypes.containsModifier(type, UniverseVisitor.this.atypeFactory.REP)) { - checker.report(Result.failure("uts.static.rep.forbidden", - type.getAnnotations(), type.toString()), p); - } - if (AnnotatedTypes.containsModifier(type, UniverseVisitor.this.atypeFactory.PEER) - && warn_staticpeer) { - // TODO: I would really like to only give the warning if - // the modifier was explicit. - checker.report(Result.warning("uts.static.peer.warning", - type.getAnnotations(), type.toString()), p); - } - } - } - - if (!allowLost && - AnnotatedTypes.containsModifier(type, UniverseVisitor.this.atypeFactory.LOST)) { - checker.report(Result.failure("uts.explicit.lost.forbidden", - type.getAnnotations(), type.toString()), p); - } - - if (type.getAnnotations().size() > 1) { - reportError(type, p); - } - return super.visitDeclared(type, p); + // We cannot do a simple test of casting, as isSubtypeOf requires + // the input types to be subtypes according to Java + if (!isTypeCastSafe(castType, exprType, node)) { + checker.reportWarning(node, "cast.unsafe", exprType.toString(true), castType.toString(true)); } + } - @Override - protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedTypeTree tree) { - final TypeElement element = - (TypeElement)type.getUnderlyingType().asElement(); - - List typevars = atypeFactory.typeVariablesFromUse(type, element); + private boolean isTypeCastSafe(AnnotatedTypeMirror castType, AnnotatedTypeMirror exprType, TypeCastTree node) { + // Typechecking side standard implementation - warns if not upcasting + return super.isTypeCastSafe(castType, exprType); + } - for (AnnotatedTypeParameterBounds atpb : typevars) { - if ((atpb.getUpperBound().getKind() != TypeKind.NULL && - AnnotatedTypes.containsModifier(atpb.getUpperBound(), UniverseVisitor.this.atypeFactory.VPLOST)) || - (atpb.getLowerBound().getKind() != TypeKind.NULL && - AnnotatedTypes.containsModifier(atpb.getLowerBound(), UniverseVisitor.this.atypeFactory.VPLOST))) { - checker.report(Result.failure("uts.vplost.in.bounds", - atpb.toString(), type.toString()), tree); + @Override + public boolean validateTypeOf(Tree tree) { + AnnotatedTypeMirror type; + // It's quite annoying that there is no TypeTree + switch (tree.getKind()) { + case PRIMITIVE_TYPE: + case PARAMETERIZED_TYPE: + case TYPE_PARAMETER: + case ARRAY_TYPE: + case UNBOUNDED_WILDCARD: + case EXTENDS_WILDCARD: + case SUPER_WILDCARD: + case ANNOTATED_TYPE: + type = atypeFactory.getAnnotatedTypeFromTypeTree(tree); + break; + case METHOD: + type = atypeFactory.getMethodReturnType((MethodTree) tree); + if (type == null || + type.getKind() == TypeKind.VOID) { + // Nothing to do for void methods. + // Note that for a constructor the AnnotatedExecutableType does + // not use void as return type. + return true; } - } - return super.visitParameterizedType(type, tree); + break; + default: + type = atypeFactory.getAnnotatedType(tree); } - /** - * Forbid explicit annotations on primitive types. - */ - @Override - public Void visitPrimitive(AnnotatedPrimitiveType type, Tree p) { - if (type.isAnnotatedInHierarchy(UniverseVisitor.this.atypeFactory.ANY)) { - Set ann = type.getAnnotations(); - if (ann.size() > 1 - || (ann.size() == 1 && !ann.contains(UniverseVisitor.this.atypeFactory.BOTTOM))) { - // the implicit default is BOTTOM, which cannot be used - // explicitly. - // if there are explicit annotations -> error. - reportError(type, p); - } - } - return super.visitPrimitive(type, p); - } + return validateType(tree, type); + } - /** - * Each array dimension can only use at most one ownership modifier. The - * check of the component type is done by the super method. - */ - @Override - public Void visitArray(AnnotatedArrayType type, Tree p) { - if (type.getAnnotations().size() > 1) { - // only one Universe modifier is allowed on the array - reportError(type, p); - } - return super.visitArray(type, p); - } + // TODO This might not be correct for infer mode. Maybe returning as it is + @Override + public boolean validateType(Tree tree, AnnotatedTypeMirror type) { + + return typeValidator.isValid(type, tree); + // The initial purpose of always returning true in validateTypeOf in inference mode + // might be that inference we want to generate constraints over all the ast location, + // but not like in typechecking mode, if something is not valid, we abort checking the + // remaining parts that are based on the invalid type. For example, in assignment, if + // rhs is not valid, we don't check the validity of assignment. But in inference, + // we always generate constraints on all places and let solver to decide if there is + // solution or not. This might be the reason why we have a always true if statement and + // validity check always returns true. } + + @Override + // Universe Type System does not need to check extends and implements + protected void checkExtendsImplements(ClassTree classTree) {} } diff --git a/src/universe/jdk.astub b/src/universe/jdk.astub index fe4d15d..53eed64 100644 --- a/src/universe/jdk.astub +++ b/src/universe/jdk.astub @@ -1,17 +1,25 @@ -import universe.quals.Any; +import universe.qual.Any; package java.lang; class Object { - boolean equals(@Any Object o); + boolean equals(@Any Object obj); } class String { - boolean equals(@Any Object o); + boolean equals(@Any Object anObject); } package java.util; -class List { - void add(X p); +interface List extends Collection { + public boolean add(E p); +} + +class ArrayList extends List { + public boolean add(E p); +} + +interface Collection { + boolean contains(@Any Object o); } diff --git a/src/universe/messages.properties b/src/universe/messages.properties index 9364850..c6749d8 100644 --- a/src/universe/messages.properties +++ b/src/universe/messages.properties @@ -1,14 +1,9 @@ uts.lost.parameter=Parameter type can not contain @Lost! -uts.vplost.parameter=Parameter type after viewpoint adaptation contains @Lost! uts.lost.lhs=Left-hand-side of assignment contains @Lost! -uts.vplost.lhs=Left-hand-side of assignment contains @VPLost! uts.lost.in.bounds=Bounds of a type contain @Lost!\n Bound: %s\n Type: %s -uts.vplost.in.bounds=Bounds of a type contain @VPLost!\n Bound: %s\n Type: %s -uts.new.ownership=Object creation needs a @Peer or @Rep modifier! +uts.new.ownership=Object creation needs a @Peer or @Rep modifier for non-implicitly immutable types and @Bottom for implicitly immutable types! uts.receiver.annotations.forbidden=Receiver annotations are not allowed! -uts.explicit.lost.forbidden=Explicit use of @Lost is forbidden! Type: "%s" uts.static.rep.forbidden=Use of @Rep in a static context is forbidden! -uts.static.peer.warning=Use of @Peer in a static field is discouraged. uts.cast.type.warning=Casting to "%s" is not recommended. uts.cast.type.error=Cast type mismatch:%n Found: %s%n Expected: %s%n -purity.assignment.forbidden=Assignments in pure methods are forbidden! \ No newline at end of file +purity.assignment.forbidden=Assignments in pure methods are forbidden! diff --git a/src/universe/qual/Any.java b/src/universe/qual/Any.java index 348f78f..3db0e0b 100644 --- a/src/universe/qual/Any.java +++ b/src/universe/qual/Any.java @@ -1,7 +1,5 @@ package universe.qual; -import org.checkerframework.framework.qual.DefaultFor; -import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.qual.SubtypeOf; import java.lang.annotation.Documented; @@ -20,6 +18,4 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ ElementType.TYPE_PARAMETER, ElementType.TYPE_USE }) @SubtypeOf({}) -@DefaultFor({ TypeUseLocation.LOCAL_VARIABLE, TypeUseLocation.RESOURCE_VARIABLE, - TypeUseLocation.IMPLICIT_UPPER_BOUND }) public @interface Any {} diff --git a/src/universe/qual/Bottom.java b/src/universe/qual/Bottom.java index 4e2c0f4..a6e7b5f 100644 --- a/src/universe/qual/Bottom.java +++ b/src/universe/qual/Bottom.java @@ -14,8 +14,6 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import javax.lang.model.type.TypeKind; - /** * The bottom of the type hierarchy is only used internally. * @@ -23,17 +21,14 @@ */ @Documented @Retention(RetentionPolicy.RUNTIME) -@Target({ ElementType.TYPE_PARAMETER, ElementType.TYPE_USE }) -@TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, - TypeUseLocation.EXPLICIT_UPPER_BOUND}) +@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) +@TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND}) @SubtypeOf({ Self.class, Rep.class }) -@DefaultFor(value = { TypeUseLocation.LOWER_BOUND }, - 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 } +@QualifierForLiterals({LiteralKind.ALL}) +@DefaultFor(value = {TypeUseLocation.LOWER_BOUND}, + 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} ) -@QualifierForLiterals({ LiteralKind.ALL }) public @interface Bottom {} diff --git a/src/universe/qual/Lost.java b/src/universe/qual/Lost.java index 57e936e..3b1871d 100644 --- a/src/universe/qual/Lost.java +++ b/src/universe/qual/Lost.java @@ -11,13 +11,13 @@ /** * Ownership information is not expressible from the current viewpoint. - * Can be used explicitly if allowLost is true. Otherwise forbidden. + * Can be used explicitly with {@code @Option(-Alint=allowLost)}, otherwise forbidden. * * @author wmdietl */ @Documented @Retention(RetentionPolicy.RUNTIME) -@Target({ ElementType.TYPE_PARAMETER, ElementType.TYPE_USE }) +@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) @SubtypeOf({ Any.class }) @TargetLocations({}) public @interface Lost {} diff --git a/src/universe/qual/Peer.java b/src/universe/qual/Peer.java index 3d1638b..555c6d7 100644 --- a/src/universe/qual/Peer.java +++ b/src/universe/qual/Peer.java @@ -18,5 +18,5 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ ElementType.TYPE_PARAMETER, ElementType.TYPE_USE }) @DefaultQualifierInHierarchy -@SubtypeOf({ VPLost.class }) +@SubtypeOf({ Lost.class }) public @interface Peer {} diff --git a/src/universe/qual/Rep.java b/src/universe/qual/Rep.java index c8e3299..feaac35 100644 --- a/src/universe/qual/Rep.java +++ b/src/universe/qual/Rep.java @@ -16,5 +16,5 @@ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ ElementType.TYPE_PARAMETER, ElementType.TYPE_USE }) -@SubtypeOf({ VPLost.class}) +@SubtypeOf({ Lost.class}) public @interface Rep {} diff --git a/src/universe/qual/Self.java b/src/universe/qual/Self.java index f603c7f..f81df26 100644 --- a/src/universe/qual/Self.java +++ b/src/universe/qual/Self.java @@ -1,5 +1,6 @@ package universe.qual; +import org.checkerframework.framework.qual.DefaultFor; import org.checkerframework.framework.qual.SubtypeOf; import org.checkerframework.framework.qual.TargetLocations; import org.checkerframework.framework.qual.TypeUseLocation; @@ -18,7 +19,8 @@ */ @Documented @Retention(RetentionPolicy.RUNTIME) -@Target({ ElementType.TYPE_PARAMETER, ElementType.TYPE_USE }) -@TargetLocations({TypeUseLocation.RECEIVER}) +@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) +@TargetLocations({TypeUseLocation.RECEIVER, TypeUseLocation.CONSTRUCTOR_RESULT}) @SubtypeOf({ Peer.class }) +@DefaultFor({TypeUseLocation.RECEIVER, TypeUseLocation.CONSTRUCTOR_RESULT}) public @interface Self {} diff --git a/src/universe/qual/VPLost.java b/src/universe/qual/VPLost.java deleted file mode 100644 index 65a96b6..0000000 --- a/src/universe/qual/VPLost.java +++ /dev/null @@ -1,23 +0,0 @@ -package universe.qual; - -import org.checkerframework.framework.qual.SubtypeOf; -import org.checkerframework.framework.qual.TargetLocations; - -import java.lang.annotation.Documented; -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; - -/** - * Ownership information is not expressible from the current viewpoint. Only - * used internally as intermediate lost; Forbidden to be used explicitly. - * - * @author wmdietl - */ -@Documented -@Retention(RetentionPolicy.RUNTIME) -@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) -@TargetLocations({}) -@SubtypeOf({ Lost.class }) -public @interface VPLost{} diff --git a/src/universe/solver/UniverseCombineConstraintEncoder.java b/src/universe/solver/UniverseCombineConstraintEncoder.java new file mode 100644 index 0000000..f58726c --- /dev/null +++ b/src/universe/solver/UniverseCombineConstraintEncoder.java @@ -0,0 +1,350 @@ +package universe.solver; + +import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.VariableSlot; +import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; +import checkers.inference.solver.backend.maxsat.MathUtils; +import checkers.inference.solver.backend.maxsat.VectorUtils; +import checkers.inference.solver.backend.maxsat.encoder.MaxSATAbstractConstraintEncoder; +import checkers.inference.solver.frontend.Lattice; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; +import org.sat4j.core.VecInt; + +import javax.lang.model.element.AnnotationMirror; +import java.util.ArrayList; +import java.util.List; +import java.util.Map; + +import static universe.UniverseAnnotationMirrorHolder.ANY; +import static universe.UniverseAnnotationMirrorHolder.BOTTOM; +import static universe.UniverseAnnotationMirrorHolder.LOST; +import static universe.UniverseAnnotationMirrorHolder.PEER; +import static universe.UniverseAnnotationMirrorHolder.REP; +import static universe.UniverseAnnotationMirrorHolder.SELF; + +public class UniverseCombineConstraintEncoder extends MaxSATAbstractConstraintEncoder implements CombineConstraintEncoder { + + public UniverseCombineConstraintEncoder(Lattice lattice, Map typeToInt) { + super(lattice, typeToInt); + } + + /** + * Wrapper method to get integer id of an AnnotationMirror to avoid Map get operations + */ + private final int id(AnnotationMirror am) { + return typeToInt.get(am); + } + + private final boolean is(ConstantSlot cs, AnnotationMirror am) { + return AnnotationUtils.areSame(cs.getValue(), am); + } + + @Override + public VecInt[] encodeVariable_Variable(VariableSlot target, VariableSlot declared, CombVariableSlot result) { + List resultClauses = new ArrayList(); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(ANY), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(BOTTOM), lattice))); + + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + + // declared is rep + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(PEER), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(REP), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(SELF), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(ANY), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(LOST), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + + // declared is self + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(PEER), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(REP), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(SELF), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(SELF), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(ANY), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(LOST), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + + // declared is peer + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(PEER), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(REP), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(SELF), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(ANY), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(LOST), lattice), + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + + return resultClauses.toArray(new VecInt[resultClauses.size()]); + } + + @Override + public VecInt[] encodeVariable_Constant(VariableSlot target, ConstantSlot declared, CombVariableSlot result) { + List resultClauses = new ArrayList(); + + if (is(declared, ANY)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else if (is(declared, BOTTOM)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(BOTTOM), lattice))); + } else if (is(declared, PEER)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(ANY), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else if (is(declared, REP)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(ANY), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else if (is(declared, SELF)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(SELF), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(ANY), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else if (is(declared, LOST)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(target.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else { + throw new BugInCF("Error: Unknown declared type: " + declared.getValue()); + } + + return resultClauses.toArray(new VecInt[resultClauses.size()]); + } + + @Override + public VecInt[] encodeConstant_Variable(ConstantSlot target, VariableSlot declared, CombVariableSlot result) { + List resultClauses = new ArrayList<>(); + + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(ANY), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(BOTTOM), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(BOTTOM), lattice))); + + if (is(target, PEER)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } else if (is(target, REP)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } else if (is(target, SELF)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(SELF), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } else if (is(target, ANY) || is(target, LOST)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(),id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } else if (is(target, BOTTOM)) { + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(),id(PEER), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(REP), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(SELF), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + resultClauses.add(VectorUtils.asVec( + -MathUtils.mapIdToMatrixEntry(declared.getId(), id(LOST), lattice), + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else { + throw new BugInCF("Error: Unknown target type: " + target.getValue()); + } + + return resultClauses.toArray(new VecInt[resultClauses.size()]); + } + + @Override + public VecInt[] encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, CombVariableSlot result) { + List resultClauses = new ArrayList<>(); + + if (is(declared, ANY)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else if (is(declared, BOTTOM)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(BOTTOM), lattice))); + } else if (is(target, BOTTOM)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(ANY), lattice))); + } else if (is(declared, LOST)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } else if (is(declared, PEER)) { + if (is(target, REP)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(REP), lattice))); + } else if (is(target, SELF) || + AnnotationUtils.areSame(target.getValue(), PEER)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(PEER), lattice))); + } else { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } + } else if (is(declared, REP) || is(declared, SELF)) { + if (is(target, SELF)) { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(declared.getValue()), lattice))); + } else { + resultClauses.add(VectorUtils.asVec( + MathUtils.mapIdToMatrixEntry(result.getId(), id(LOST), lattice))); + } + } else { + throw new BugInCF("Error: Unknown declared or target type: " + declared.getValue() + target.getValue()); + } + + return resultClauses.toArray(new VecInt[resultClauses.size()]); + } +} diff --git a/src/universe/solver/UniverseFormatTranslator.java b/src/universe/solver/UniverseFormatTranslator.java new file mode 100644 index 0000000..3f1d2f6 --- /dev/null +++ b/src/universe/solver/UniverseFormatTranslator.java @@ -0,0 +1,26 @@ +package universe.solver; + +import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; +import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.backend.maxsat.encoder.MaxSATConstraintEncoderFactory; +import checkers.inference.solver.frontend.Lattice; +import org.sat4j.core.VecInt; + +public class UniverseFormatTranslator extends MaxSatFormatTranslator { + + public UniverseFormatTranslator(Lattice lattice) { + super(lattice); + + } + + @Override + protected ConstraintEncoderFactory createConstraintEncoderFactory() { + return new MaxSATConstraintEncoderFactory(lattice, typeToInt, this){ + @Override + public CombineConstraintEncoder createCombineConstraintEncoder() { + return new UniverseCombineConstraintEncoder(lattice, typeToInt); + } + }; + } +} diff --git a/src/universe/solver/UniverseSolverEngine.java b/src/universe/solver/UniverseSolverEngine.java new file mode 100644 index 0000000..307bf45 --- /dev/null +++ b/src/universe/solver/UniverseSolverEngine.java @@ -0,0 +1,19 @@ +package universe.solver; + +import checkers.inference.solver.SolverEngine; +import checkers.inference.solver.backend.SolverFactory; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.backend.maxsat.MaxSatSolverFactory; +import checkers.inference.solver.frontend.Lattice; + +public class UniverseSolverEngine extends SolverEngine { + @Override + protected SolverFactory createSolverFactory() { + return new MaxSatSolverFactory(){ + @Override + public MaxSatFormatTranslator createFormatTranslator(Lattice lattice) { + return new UniverseFormatTranslator(lattice); + } + }; + } +}