Temp commit to store the code

opprop · Apr 13, 2024 · 8713ec6 · 8713ec6
1 parent bee540d
commit 8713ec6
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 37 deletions.
diff --git a/src/main/java/pico/typecheck/PICOChecker.java b/src/main/java/pico/typecheck/PICOChecker.java
@@ -15,7 +15,7 @@ public PICOChecker() {}
 
     @Override
     public boolean checkPrimitives() {
-        return false;
+        return true;
     }
 
     @Override

diff --git a/src/main/java/pico/typecheck/PICONoInitAnnotatedTypeFactory.java b/src/main/java/pico/typecheck/PICONoInitAnnotatedTypeFactory.java
@@ -13,6 +13,7 @@
 import com.sun.source.tree.VariableTree;
 import com.sun.source.util.TreePath;
 
+import org.checkerframework.checker.initialization.InitializationFieldAccessTreeAnnotator;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.qual.RelevantJavaTypes;
 import org.checkerframework.framework.type.*;
@@ -88,11 +89,13 @@ protected ViewpointAdapter createViewpointAdapter() {
     /** Annotators are executed by the added order. Same for Type Annotator */
     @Override
     protected TreeAnnotator createTreeAnnotator() {
-        return new ListTreeAnnotator(
-                new PICOPropagationTreeAnnotator(this),
-                new LiteralTreeAnnotator(this),
-                new PICOSuperClauseAnnotator(this),
-                new PICOTreeAnnotator(this));
+        List<TreeAnnotator> annotators = new ArrayList<>(5);
+        annotators.add(new InitializationFieldAccessTreeAnnotator(this));
+        annotators.add(new PICOPropagationTreeAnnotator(this));
+        annotators.add(new LiteralTreeAnnotator(this));
+        annotators.add(new PICOSuperClauseAnnotator(this));
+        annotators.add(new PICOTreeAnnotator(this));
+        return new ListTreeAnnotator(annotators);
     }
 
     // TODO Refactor super class to remove this duplicate code
@@ -150,14 +153,14 @@ public ParameterizedExecutableType constructorFromUse(NewClassTree tree) {
     //        return IMMUTABLE;
     //    }
     //
-    //    /** This affects what fields pico warns not initialized in constructors */
-    //    @Override
-    //    protected boolean hasFieldInvariantAnnotation(
-    //            AnnotatedTypeMirror type, VariableElement fieldElement) {
-    //        // This affects which fields should be guaranteed to be initialized:
-    //        // Fields of any immutability should be initialized.
-    //        return !PICOTypeUtil.isAssignableField(fieldElement, this);
-    //    }
+    //        /** This affects what fields pico warns not initialized in constructors */
+    //        @Override
+    //        protected boolean hasFieldInvariantAnnotation(
+    //                AnnotatedTypeMirror type, VariableElement fieldElement) {
+    //            // This affects which fields should be guaranteed to be initialized:
+    //            // Fields of any immutability should be initialized.
+    //            return !PICOTypeUtil.isAssignableField(fieldElement, this);
+    //        }
 
     /** Forbid applying top annotations to type variables if they are used on local variables */
     @Override
@@ -167,7 +170,7 @@ public boolean getShouldDefaultTypeVarLocals() {
 
     /**
      * This covers the case when static fields are used and constructor is accessed as an
-     * element(regarding to applying @Immutable on type declaration to constructor return type).
+     * element(regarding applying @Immutable on type declaration to constructor return type).
      */
     @Override
     public void addComputedTypeAnnotations(Element elt, AnnotatedTypeMirror type) {

diff --git a/src/main/java/pico/typecheck/PICONoInitStore.java b/src/main/java/pico/typecheck/PICONoInitStore.java
@@ -1,11 +1,16 @@
 package pico.typecheck;
 
+import org.checkerframework.dataflow.expression.FieldAccess;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
 import org.checkerframework.framework.flow.CFAbstractStore;
 
+import java.util.Map;
+
 /** Created by mier on 15/08/17. */
 public class PICONoInitStore extends CFAbstractStore<PICONoInitValue, PICONoInitStore> {
 
+    protected Map<FieldAccess, PICONoInitValue> initializedFields;
+
     public PICONoInitStore(
             CFAbstractAnalysis<PICONoInitValue, PICONoInitStore, ?> analysis,
             boolean sequentialSemantics) {
@@ -14,5 +19,8 @@ public PICONoInitStore(
 
     public PICONoInitStore(PICONoInitStore s) {
         super(s);
+        if (s.initializedFields != null) {
+            initializedFields = s.initializedFields;
+        }
     }
 }
diff --git a/src/main/java/pico/typecheck/PICONoInitVisitor.java b/src/main/java/pico/typecheck/PICONoInitVisitor.java
@@ -23,7 +23,6 @@
 import com.sun.source.tree.VariableTree;
 
 import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
-import org.checkerframework.checker.initialization.qual.UnderInitialization;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.common.basetype.BaseTypeVisitor;
 import org.checkerframework.common.basetype.TypeValidator;
@@ -71,9 +70,7 @@ protected TypeValidator createTypeValidator() {
 
     @Override
     protected void checkConstructorResult(
-            AnnotatedExecutableType constructorType, ExecutableElement constructorElement) {
-
-    }
+            AnnotatedExecutableType constructorType, ExecutableElement constructorElement) {}
 
     // This method is for validating usage of mutability qualifier is conformable to element
     // declaration,
@@ -392,10 +389,12 @@ private boolean allowWrite(AnnotatedTypeMirror receiverType, ExpressionTree vari
         // point
         if (PICOTypeUtil.isAssigningAssignableField(variable, atypeFactory)) {
             return isAllowedAssignableField(receiverType, variable);
-        } else if (isInitializingReceiverDependantMutableOrImmutableObject(receiverType)) {
-            return true;
         } else if (receiverType.hasAnnotation(MUTABLE)) {
+            // If the receiver is mutable, we allow assigning/reassigning
             return true;
+            //        } else if (TreeUtils.elementFromUse(variable)) {
+            //            // If the field is not initialized, we allow assigning/reassigning
+            //            return true;
         }
 
         return false;
@@ -416,22 +415,6 @@ private boolean isAllowedAssignableField(
                 && fieldType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE));
     }
 
-    private boolean isInitializingReceiverDependantMutableOrImmutableObject(
-            AnnotatedTypeMirror receiverType) {
-        if (receiverType.hasAnnotation(UnderInitialization.class)
-                && receiverType.hasAnnotation(RECEIVER_DEPENDANT_MUTABLE)) {
-            return true;
-        } else if (receiverType.hasAnnotation(UnderInitialization.class)
-                && receiverType.hasAnnotation(IMMUTABLE)) {
-            return true;
-        } else if (receiverType.hasAnnotation(UnderInitialization.class)
-                && receiverType.hasAnnotation(MUTABLE)) {
-            return true;
-        } else {
-            return false;
-        }
-    }
-
     private void reportFieldOrArrayWriteError(
             Tree node, ExpressionTree variable, AnnotatedTypeMirror receiverType) {
         if (variable.getKind() == Kind.MEMBER_SELECT) {