Cleanup src (#33)

Co-authored-by: Weitian Xing <xingweitian@gmail.com>
Co-authored-by: Baorui Zhou <b42zhou@uwaterloo.ca>
Co-authored-by: Jeff Luo <j36luo@uwaterloo.ca>
Co-authored-by: Mier Ta <topnessman@sina.com>

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);
+    }
+
+}

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));
     }
-    */
 
 }

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);
+        }
+    }
+}

src/universe/UniverseInferenceChecker.java

@@ -1,33 +1,34 @@
 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;
 import checkers.inference.InferenceVisitor;
 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;
+    }
 }