Store both the initializer value and the declared value of fields

eisop · Aug 3, 2021 · c805fff · c805fff
1 parent 3d6adae
commit c805fff
Show file tree

Hide file tree

Showing 25 changed files with 235 additions and 176 deletions.
diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java
@@ -20,7 +20,6 @@
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 import javax.lang.model.element.ExecutableElement;
-import javax.lang.model.element.VariableElement;
 import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
 import org.checkerframework.checker.nullness.NullnessChecker;
 import org.checkerframework.common.basetype.BaseTypeChecker;
@@ -31,6 +30,7 @@
 import org.checkerframework.dataflow.expression.JavaExpression;
 import org.checkerframework.dataflow.expression.LocalVariable;
 import org.checkerframework.dataflow.expression.ThisReference;
+import org.checkerframework.framework.flow.CFAbstractAnalysis.FieldInitialValue;
 import org.checkerframework.framework.flow.CFAbstractStore;
 import org.checkerframework.framework.flow.CFAbstractValue;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -280,8 +280,11 @@ public void processClassTree(ClassTree node) {
         Store store = atypeFactory.getRegularExitStore(block);
 
         // Add field values for fields with an initializer.
-        for (Pair<VariableElement, Value> t : store.getAnalysis().getFieldValues()) {
-          store.addInitializedField(t.first);
+        for (FieldInitialValue<Value> fieldInitialValue :
+            store.getAnalysis().getFieldInitialValues()) {
+          if (fieldInitialValue.initializer != null) {
+            store.addInitializedField(fieldInitialValue.fieldDecl.getField());
+          }
         }
         final List<VariableTree> init =
             atypeFactory.getInitializedInvariantFields(store, getCurrentPath());
@@ -301,9 +304,13 @@ public void processClassTree(ClassTree node) {
       // the regular exit store of the class here.
       Store store = atypeFactory.getRegularExitStore(node);
       // Add field values for fields with an initializer.
-      for (Pair<VariableElement, Value> t : store.getAnalysis().getFieldValues()) {
-        store.addInitializedField(t.first);
+      for (FieldInitialValue<Value> fieldInitialValue :
+          store.getAnalysis().getFieldInitialValues()) {
+        if (fieldInitialValue.initializer != null) {
+          store.addInitializedField(fieldInitialValue.fieldDecl.getField());
+        }
       }
+
       List<AnnotationMirror> receiverAnnotations = Collections.emptyList();
       checkFieldsInitialized(node, isStatic, store, receiverAnnotations);
     }

diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnalysis.java
@@ -1,15 +1,12 @@
 package org.checkerframework.checker.lock;
 
-import java.util.List;
 import java.util.Set;
 import javax.lang.model.element.AnnotationMirror;
-import javax.lang.model.element.VariableElement;
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.javacutil.Pair;
 
 /**
  * The analysis class for the lock type system.
@@ -19,11 +16,14 @@
  */
 public class LockAnalysis extends CFAbstractAnalysis<CFValue, LockStore, LockTransfer> {
 
-  public LockAnalysis(
-      BaseTypeChecker checker,
-      LockAnnotatedTypeFactory factory,
-      List<Pair<VariableElement, CFValue>> fieldValues) {
-    super(checker, factory, fieldValues);
+  /**
+   * Creates a new {@link LockAnalysis}.
+   *
+   * @param checker the checker
+   * @param factory the factory
+   */
+  public LockAnalysis(BaseTypeChecker checker, LockAnnotatedTypeFactory factory) {
+    super(checker, factory);
   }
 
   @Override

diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java
@@ -19,7 +19,6 @@
 import javax.lang.model.element.Element;
 import javax.lang.model.element.ElementKind;
 import javax.lang.model.element.ExecutableElement;
-import javax.lang.model.element.VariableElement;
 import javax.lang.model.util.Elements;
 import org.checkerframework.checker.lock.qual.EnsuresLockHeld;
 import org.checkerframework.checker.lock.qual.EnsuresLockHeldIf;
@@ -62,7 +61,6 @@
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.ElementUtils;
-import org.checkerframework.javacutil.Pair;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypeSystemError;
 import org.plumelib.util.CollectionsPlume;
@@ -266,8 +264,8 @@ protected QualifierHierarchy createQualifierHierarchy() {
   }
 
   @Override
-  protected LockAnalysis createFlowAnalysis(List<Pair<VariableElement, CFValue>> fieldValues) {
-    return new LockAnalysis(checker, this, fieldValues);
+  protected LockAnalysis createFlowAnalysis() {
+    return new LockAnalysis(checker, this);
   }
 
   @Override

diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnalysis.java
@@ -1,31 +1,23 @@
 package org.checkerframework.checker.nullness;
 
-import java.util.List;
 import java.util.Set;
 import javax.lang.model.element.AnnotationMirror;
-import javax.lang.model.element.VariableElement;
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
 import org.checkerframework.framework.flow.CFAbstractValue;
-import org.checkerframework.javacutil.Pair;
 
 /** Boilerplate code to glue together all the parts the KeyFor dataflow classes. */
 public class KeyForAnalysis extends CFAbstractAnalysis<KeyForValue, KeyForStore, KeyForTransfer> {
 
-  public KeyForAnalysis(
-      BaseTypeChecker checker,
-      KeyForAnnotatedTypeFactory factory,
-      List<Pair<VariableElement, KeyForValue>> fieldValues,
-      int maxCountBeforeWidening) {
-    super(checker, factory, fieldValues, maxCountBeforeWidening);
-  }
-
-  public KeyForAnalysis(
-      BaseTypeChecker checker,
-      KeyForAnnotatedTypeFactory factory,
-      List<Pair<VariableElement, KeyForValue>> fieldValues) {
-    super(checker, factory, fieldValues);
+  /**
+   * Creates a new {@code KeyForAnalysis}.
+   *
+   * @param checker the checker
+   * @param factory the factory
+   */
+  public KeyForAnalysis(BaseTypeChecker checker, KeyForAnnotatedTypeFactory factory) {
+    super(checker, factory);
   }
 
   @Override

diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForAnnotatedTypeFactory.java
@@ -8,11 +8,9 @@
 import java.util.Collection;
 import java.util.Collections;
 import java.util.LinkedHashSet;
-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.VariableElement;
 import javax.lang.model.type.TypeKind;
 import org.checkerframework.checker.nullness.qual.KeyFor;
 import org.checkerframework.checker.nullness.qual.KeyForBottom;
@@ -33,7 +31,6 @@
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.AnnotationUtils;
-import org.checkerframework.javacutil.Pair;
 import org.checkerframework.javacutil.TreeUtils;
 
 public class KeyForAnnotatedTypeFactory
@@ -157,10 +154,9 @@ protected boolean isSubtype(
   }
 
   @Override
-  protected KeyForAnalysis createFlowAnalysis(
-      List<Pair<VariableElement, KeyForValue>> fieldValues) {
+  protected KeyForAnalysis createFlowAnalysis() {
     // Explicitly call the constructor instead of using reflection.
-    return new KeyForAnalysis(checker, this, fieldValues);
+    return new KeyForAnalysis(checker, this);
   }
 
   @Override

diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnalysis.java
@@ -1,14 +1,11 @@
 package org.checkerframework.checker.nullness;
 
-import java.util.List;
 import java.util.Set;
 import javax.lang.model.element.AnnotationMirror;
-import javax.lang.model.element.VariableElement;
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.flow.CFAbstractAnalysis;
 import org.checkerframework.framework.flow.CFAbstractValue;
-import org.checkerframework.javacutil.Pair;
 
 /**
  * The analysis class for the non-null type system (serves as factory for the transfer function,
@@ -17,11 +14,14 @@
 public class NullnessAnalysis
     extends CFAbstractAnalysis<NullnessValue, NullnessStore, NullnessTransfer> {
 
-  public NullnessAnalysis(
-      BaseTypeChecker checker,
-      NullnessAnnotatedTypeFactory factory,
-      List<Pair<VariableElement, NullnessValue>> fieldValues) {
-    super(checker, factory, fieldValues);
+  /**
+   * Creates a new {@code NullnessAnalysis}.
+   *
+   * @param checker the checker
+   * @param factory the factory
+   */
+  public NullnessAnalysis(BaseTypeChecker checker, NullnessAnnotatedTypeFactory factory) {
+    super(checker, factory);
   }
 
   @Override

diff --git a/...ker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/...ker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java
@@ -313,9 +313,8 @@ public Pair<List<VariableTree>, List<VariableTree>> getUninitializedFields(
   }
 
   @Override
-  protected NullnessAnalysis createFlowAnalysis(
-      List<Pair<VariableElement, NullnessValue>> fieldValues) {
-    return new NullnessAnalysis(checker, this, fieldValues);
+  protected NullnessAnalysis createFlowAnalysis() {
+    return new NullnessAnalysis(checker, this);
   }
 
   @Override

diff --git a/checker/src/main/java/org/checkerframework/checker/units/UnitsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/units/UnitsAnnotatedTypeFactory.java
@@ -609,6 +609,10 @@ protected AnnotationMirror leastUpperBoundWithElements(
     }
 
     @Override
+    @SuppressWarnings(
+        "nullness:return" // This class UnitsQualifierHierarchy is annotated for nullness, but the
+    // outer class UnitsAnnotatedTypeFactory is not, so the type of fields is @Nullable.
+    )
     protected AnnotationMirror greatestLowerBoundWithElements(
         AnnotationMirror a1,
         QualifierKind qualifierKind1,

diff --git a/checker/tests/ainfer-testchecker/non-annotated/InterfaceTest.java b/checker/tests/ainfer-testchecker/non-annotated/InterfaceTest.java
@@ -13,6 +13,7 @@ interface InterfaceTest {
   default void requireSibling1(@Sibling1 String x) {}
 
   default void testX() {
+    // :: warning: (argument)
     requireSibling1(toaster);
   }
 }
diff --git a/checker/tests/interning/ConstantsInterning.java b/checker/tests/interning/ConstantsInterning.java
@@ -27,6 +27,7 @@ void foo() {
     // :: error: (assignment.type.incompatible)
     is = is + is;
     is = Constants2.E;
+    // :: error: (assignment)
     is = (String) F;
   }
 }

diff --git a/checker/tests/interning/StringIntern.java b/checker/tests/interning/StringIntern.java
@@ -38,7 +38,8 @@ public void test(@Interned String arg) {
     internedStr = finalStringInitializedToInterned; // OK
     // :: error: (assignment.type.incompatible)
     internedStr = finalString2; // error
-    @Interned Foo internedFoo = finalFooInitializedToInterned; // OK
+    // :: error: (assignment)
+    @Interned Foo internedFoo = finalFooInitializedToInterned;
     if (arg == finalStringStatic1) {} // OK
     // :: error: (not.interned)
     if (arg == finalStringStatic2) {} // error

diff --git a/checker/tests/lock/ViewpointAdaptation.java b/checker/tests/lock/ViewpointAdaptation.java
@@ -15,8 +15,7 @@ public class ViewpointAdaptation {
 
   public void method1(final String a) {
     synchronized (a) {
-      // The expression "a" from the @GuardedBy annotation on f is not valid at the
-      // declaration site of f, but an error was already issued at the declaration of f.
+      // :: error: (expression.unparsable)
       f.counter++;
     }
   }

diff --git a/checker/tests/nullness/FinalFields.java b/checker/tests/nullness/FinalFields.java
@@ -2,13 +2,13 @@
 
 class Upper {
   @Nullable String fs = "NonNull init";
-  final @Nullable String ffs = "NonNull init";
+  private final @Nullable String ffs = "NonNull init";
 
   void access() {
     // Error, because non-final field type is not refined
     // :: error: (dereference.of.nullable)
     fs.hashCode();
-    // Final field in the same class is refined
+    // private final field is refined
     ffs.hashCode();
   }
 }
@@ -35,13 +35,13 @@ public void local() {
 
 class Lower {
   @Nullable String fs = "NonNull init, too";
-  final @Nullable String ffs = "NonNull init, too";
+  private final @Nullable String ffs = "NonNull init, too";
 
   void access() {
     // Error, because non-final field type is not refined
     // :: error: (dereference.of.nullable)
     fs.hashCode();
-    // Final field in the same class is refined
+    // private final field is refined
     ffs.hashCode();
   }
 }
diff --git a/checker/tests/nullness/FlowField.java b/checker/tests/nullness/FlowField.java
@@ -27,7 +27,7 @@ void test1() {
     nonnull.toString();
   }
 
-  static final String nonnull = new String();
+  private static final String nonnull = new String();
 
   class A {
     protected String field = null;

diff --git a/checker/tests/nullness/Initializer.java b/checker/tests/nullness/Initializer.java
@@ -13,6 +13,7 @@ public class Initializer {
 
   public String d = ("");
 
+  // :: error: (initialization.fields.uninitialized)
   public Initializer() {
     // :: error: (assignment.type.incompatible)
     a = null;
@@ -26,18 +27,21 @@ public Initializer(boolean foo) {}
   public Initializer(int foo) {
     a = "";
     c = "";
+    f = "";
   }
 
   public Initializer(float foo) {
     setField();
     c = "";
+    f = "";
   }
 
   public Initializer(double foo) {
     if (!setFieldMaybe()) {
       a = "";
     }
     c = "";
+    f = "";
   }
 
   // :: error: (initialization.fields.uninitialized)
@@ -59,7 +63,7 @@ public boolean setFieldMaybe(@UnknownInitialization Initializer this) {
     return true;
   }
 
-  String f = "";
+  String f;
 
   void t1(@UnknownInitialization Initializer this) {
     // :: error: (dereference.of.nullable)
@@ -71,7 +75,8 @@ void t1(@UnknownInitialization Initializer this) {
 
 class SubInitializer extends Initializer {
 
-  String f = "";
+  // :: error: (initialization.field.uninitialized)
+  String f;
 
   void subt1(@UnknownInitialization(Initializer.class) SubInitializer this) {
     fieldF.toString();

diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
@@ -13,9 +13,18 @@ Version 3.17.0 (August 3, 2021)
 **Implementation details:**
 
 Method renamings in `GenericAnnotatedTypeFactory`:
-* `getPreconditionAnnotation` => `getPreconditionAnnotations`
-* `getPostconditionAnnotation` => `getPostconditionAnnotations`
-* `getPreOrPostconditionAnnotation` => `getPreOrPostconditionAnnotations`
+ * `getPreconditionAnnotation` => `getPreconditionAnnotations`
+ * `getPostconditionAnnotation` => `getPostconditionAnnotations`
+ * `getPreOrPostconditionAnnotation` => `getPreOrPostconditionAnnotations`
+
+Method renamings:
+ * `CFAbstractAnalysis.getFieldValues` => `getFieldInitialValues`
+
+The following methods no longer take a `fieldValues` parameter:
+ * `GenericAnnotatedTypeFactory#createFlowAnalysis`
+ * `CFAnalysis` construtor
+ * `CFAbstractAnalysis#performAnalysis`
+ * `CFAbstractAnalysis` constructors
 
 **Closed issues:**