From c805fffa5507b0c46b9ef942bc6e3007674a5f00 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 28 Jul 2021 11:54:38 -0700 Subject: [PATCH] Store both the initializer value and the declared value of fields --- .../initialization/InitializationVisitor.java | 17 ++- .../checker/lock/LockAnalysis.java | 16 +-- .../lock/LockAnnotatedTypeFactory.java | 6 +- .../checker/nullness/KeyForAnalysis.java | 24 ++-- .../nullness/KeyForAnnotatedTypeFactory.java | 8 +- .../checker/nullness/NullnessAnalysis.java | 16 +-- .../NullnessAnnotatedTypeFactory.java | 5 +- .../units/UnitsAnnotatedTypeFactory.java | 4 + .../non-annotated/InterfaceTest.java | 1 + .../tests/interning/ConstantsInterning.java | 1 + checker/tests/interning/StringIntern.java | 3 +- checker/tests/lock/ViewpointAdaptation.java | 3 +- checker/tests/nullness/FinalFields.java | 8 +- checker/tests/nullness/FlowField.java | 2 +- checker/tests/nullness/Initializer.java | 9 +- docs/CHANGELOG.md | 15 ++- .../basetype/BaseAnnotatedTypeFactory.java | 7 +- .../value/ValueAnnotatedTypeFactory.java | 9 ++ .../framework/flow/CFAbstractAnalysis.java | 71 ++++++++--- .../framework/flow/CFAbstractTransfer.java | 115 ++++++++---------- .../framework/flow/CFAnalysis.java | 14 ++- .../framework/source/SourceChecker.java | 2 +- .../framework/type/AnnotatedTypeFactory.java | 16 +++ .../type/GenericAnnotatedTypeFactory.java | 35 +++--- framework/tests/flow2/Basic2.java | 4 +- 25 files changed, 235 insertions(+), 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 index 1a1962a8fdb..57646f3787f 100644 --- 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 t : store.getAnalysis().getFieldValues()) { - store.addInitializedField(t.first); + for (FieldInitialValue fieldInitialValue : + store.getAnalysis().getFieldInitialValues()) { + if (fieldInitialValue.initializer != null) { + store.addInitializedField(fieldInitialValue.fieldDecl.getField()); + } } final List 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 t : store.getAnalysis().getFieldValues()) { - store.addInitializedField(t.first); + for (FieldInitialValue fieldInitialValue : + store.getAnalysis().getFieldInitialValues()) { + if (fieldInitialValue.initializer != null) { + store.addInitializedField(fieldInitialValue.fieldDecl.getField()); + } } + List 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 index b1ee3775195..50e386e6af9 100644 --- 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 { - public LockAnalysis( - BaseTypeChecker checker, - LockAnnotatedTypeFactory factory, - List> 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 index 36e7b591b39..0430d7c8daa 100644 --- 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> 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 index 980d7d40bd8..49568e3586f 100644 --- 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 { - public KeyForAnalysis( - BaseTypeChecker checker, - KeyForAnnotatedTypeFactory factory, - List> fieldValues, - int maxCountBeforeWidening) { - super(checker, factory, fieldValues, maxCountBeforeWidening); - } - - public KeyForAnalysis( - BaseTypeChecker checker, - KeyForAnnotatedTypeFactory factory, - List> 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 index 35640d90b12..f4144d7482d 100644 --- 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> 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 index cec04753355..492469105a7 100644 --- 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 { - public NullnessAnalysis( - BaseTypeChecker checker, - NullnessAnnotatedTypeFactory factory, - List> 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/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java index bed0d4c6333..402e00ddb5d 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java @@ -313,9 +313,8 @@ public Pair, List> getUninitializedFields( } @Override - protected NullnessAnalysis createFlowAnalysis( - List> 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 index 5477fd4c903..a65ec03d4a2 100644 --- 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 index d9de21ce92d..8c7af17bf78 100644 --- 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 index ed8d6017b6c..073bf0d3253 100644 --- 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 index 9903803b81b..c2740bafca9 100644 --- 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 index f456addf9af..b75e4faf19e 100644 --- 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 index 9f82333c84f..e7c0febccee 100644 --- 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 index fa46ce39857..2663e1f87ce 100644 --- 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 index a952b3d33fd..6909e0d9277 100644 --- 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,11 +27,13 @@ public Initializer(boolean foo) {} public Initializer(int foo) { a = ""; c = ""; + f = ""; } public Initializer(float foo) { setField(); c = ""; + f = ""; } public Initializer(double foo) { @@ -38,6 +41,7 @@ public Initializer(double foo) { 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 index 26ef278b8f0..8e9c3f2034f 100644 --- 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:** diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseAnnotatedTypeFactory.java index c8e1d1861a7..29b9bcfe6fc 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseAnnotatedTypeFactory.java @@ -1,13 +1,10 @@ package org.checkerframework.common.basetype; -import java.util.List; -import javax.lang.model.element.VariableElement; import org.checkerframework.framework.flow.CFAnalysis; import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFTransfer; import org.checkerframework.framework.flow.CFValue; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; -import org.checkerframework.javacutil.Pair; /** * A factory that extends {@link GenericAnnotatedTypeFactory} to use the default flow-sensitive @@ -30,7 +27,7 @@ public BaseAnnotatedTypeFactory(BaseTypeChecker checker) { } @Override - protected CFAnalysis createFlowAnalysis(List> fieldValues) { - return new CFAnalysis(checker, this, fieldValues); + protected CFAnalysis createFlowAnalysis() { + return new CFAnalysis(checker, this); } } diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java index dae458a8ccc..c894352f849 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java @@ -1517,4 +1517,13 @@ public AnnotatedTypeMirror getDummyAssignedTo(ExpressionTree expressionTree) { } return null; } + + /** A fact about an array, such as its length, cannot be changed via side effects to the array. */ + @Override + public boolean isImmutable(TypeMirror type) { + if (type.getKind() == TypeKind.ARRAY) { + return true; + } + return super.isImmutable(type); + } } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index 69702e3a95e..6159d0f7c17 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -1,10 +1,10 @@ package org.checkerframework.framework.flow; +import java.util.ArrayList; import java.util.List; import java.util.Set; import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import javax.lang.model.util.Types; @@ -12,6 +12,7 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.ForwardAnalysisImpl; import org.checkerframework.dataflow.cfg.ControlFlowGraph; +import org.checkerframework.dataflow.expression.FieldAccess; import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -22,7 +23,6 @@ import org.checkerframework.framework.type.TypeHierarchy; import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper; import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TypesUtils; /** @@ -60,8 +60,38 @@ public abstract class CFAbstractAnalysis< /** A checker that contains command-line arguments and other information. */ protected final SourceChecker checker; + /** + * A triple of field, value corresponding to the annotations on its declared type, value of its + * initializer. The value of the initializer is {@code null} if the field does not have one. + * + * @param type of value + */ + public static class FieldInitialValue> { + + /** A field access that corresponds to the declaration of a field. */ + public final FieldAccess fieldDecl; + /** The value corresponding to the annotations on the declared type of the field. */ + public final V declared; + /** The value of the initializer of the field, or null if no initializer exists. */ + public final @Nullable V initializer; + + /** + * Creates a new FieldInitialValue. + * + * @param fieldDecl a field access that corresponds to the declaration of a field + * @param declared value corresponding to the annotations on the declared type of {@code field} + * @param initializer value of the initializer of {@code field}, or null if no initializer + * exists + */ + public FieldInitialValue(FieldAccess fieldDecl, V declared, @Nullable V initializer) { + this.fieldDecl = fieldDecl; + this.declared = declared; + this.initializer = initializer; + } + } + /** Initial abstract types for fields. */ - protected final List> fieldValues; + protected final List> fieldValues; /** The associated processing environment. */ protected final ProcessingEnvironment env; @@ -74,13 +104,11 @@ public abstract class CFAbstractAnalysis< * * @param checker a checker that contains command-line arguments and other information * @param factory an annotated type factory to introduce type and dataflow rules - * @param fieldValues initial abstract types for fields * @param maxCountBeforeWidening number of times a block can be analyzed before widening */ protected CFAbstractAnalysis( BaseTypeChecker checker, GenericAnnotatedTypeFactory> factory, - List> fieldValues, int maxCountBeforeWidening) { super(maxCountBeforeWidening); env = checker.getProcessingEnvironment(); @@ -91,28 +119,39 @@ protected CFAbstractAnalysis( this.atypeFactory = factory; this.checker = checker; this.transferFunction = createTransferFunction(); - // TODO: remove parameter and set to empty list. - this.fieldValues = fieldValues; + this.fieldValues = new ArrayList<>(); } + /** + * Create a CFAbstractAnalysis. + * + * @param checker a checker that contains command-line arguments and other information + * @param factory an annotated type factory to introduce type and dataflow rules + */ protected CFAbstractAnalysis( BaseTypeChecker checker, - GenericAnnotatedTypeFactory> factory, - List> fieldValues) { - this( - checker, - factory, - fieldValues, - factory.getQualifierHierarchy().numberOfIterationsBeforeWidening()); + GenericAnnotatedTypeFactory> factory) { + this(checker, factory, factory.getQualifierHierarchy().numberOfIterationsBeforeWidening()); } - public void performAnalysis(ControlFlowGraph cfg, List> fieldValues) { + /** + * Analyze the given control flow graph. + * + * @param cfg control flow graph to analyze + * @param fieldValues initial values of the fields + */ + public void performAnalysis(ControlFlowGraph cfg, List> fieldValues) { this.fieldValues.clear(); this.fieldValues.addAll(fieldValues); super.performAnalysis(cfg); } - public List> getFieldValues() { + /** + * A list of initial abstract values for the fields. + * + * @return a list of initial abstract values for the fields + */ + public List> getFieldInitialValues() { return fieldValues; } diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 02f78654f2d..16c38e75b5c 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -4,7 +4,6 @@ import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; -import com.sun.source.tree.VariableTree; import com.sun.source.util.TreePath; import com.sun.tools.javac.code.Symbol.ClassSymbol; import java.util.ArrayList; @@ -19,6 +18,8 @@ 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.element.TypeElement; import javax.lang.model.element.VariableElement; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.interning.qual.InternedDistinct; @@ -54,12 +55,11 @@ import org.checkerframework.dataflow.cfg.node.ThisNode; import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode; import org.checkerframework.dataflow.cfg.node.WideningConversionNode; -import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.LocalVariable; -import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.dataflow.util.NodeUtils; +import org.checkerframework.framework.flow.CFAbstractAnalysis.FieldInitialValue; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType; @@ -297,8 +297,7 @@ public S initialStore(UnderlyingAST underlyingAST, @Nullable List> fieldValues = analysis.getFieldValues(); - for (Pair p : fieldValues) { - VariableElement element = p.first; - V value = p.second; - if (ElementUtils.isFinal(element) || TreeUtils.isConstructor(methodTree)) { - JavaExpression receiver; - if (ElementUtils.isStatic(element)) { - receiver = new ClassName(classType); - } else { - receiver = new ThisReference(classType); - } - TypeMirror fieldType = ElementUtils.getType(element); - JavaExpression field = new FieldAccess(receiver, fieldType, element); - store.insertValue(field, value); + /** + * Add field values to the initial store before {@code methodTree}. + * + *

The initializer value is inserted into {@code store} if the field is private and final. + * + *

The declared value is inserted into {@code store} if: + * + *

    + *
  • {@code methodTree} is a constructor and the field has an initializer. (Use the + * declaration type rather than the initializer because an initialization block might have + * re-set it.) + *
  • {@code methodTree} is not a constructor and the receiver is fully initialized as + * determined by {@link #isNotFullyInitializedReceiver(MethodTree)}. + *
+ * + * @param store initial store into which field values are inserted; it may not be empty + * @param classTree the class that contains {@code methodTree} + * @param methodTree the method or constructor tree + */ + private void addInitialFieldValues(S store, ClassTree classTree, MethodTree methodTree) { + boolean isConstructor = TreeUtils.isConstructor(methodTree); + TypeElement classEle = TreeUtils.elementFromDeclaration(classTree); + for (FieldInitialValue fieldInitialValue : analysis.getFieldInitialValues()) { + VariableElement varEle = fieldInitialValue.fieldDecl.getField(); + // Insert the value from the initializer of private final fields. + if (fieldInitialValue.initializer != null + && varEle.getModifiers().contains(Modifier.PRIVATE) + && ElementUtils.isFinal(varEle) + && analysis.atypeFactory.isImmutable(ElementUtils.getType(varEle))) { + store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.initializer); } - } - // add properties about fields (static information from type) - boolean isNotFullyInitializedReceiver = isNotFullyInitializedReceiver(methodTree); - if (isNotFullyInitializedReceiver && !TreeUtils.isConstructor(methodTree)) { - // cannot add information about fields if the receiver isn't initialized - // and the method isn't a constructor - return; - } - for (Tree member : classTree.getMembers()) { - if (member instanceof VariableTree) { - VariableTree vt = (VariableTree) member; - final VariableElement element = TreeUtils.elementFromDeclaration(vt); - AnnotatedTypeMirror type = - ((GenericAnnotatedTypeFactory) factory).getAnnotatedTypeLhs(vt); - TypeMirror fieldType = ElementUtils.getType(element); - JavaExpression receiver; - if (ElementUtils.isStatic(element)) { - receiver = new ClassName(classType); - } else { - receiver = new ThisReference(classType); + // Maybe insert the declared type: + if (!isConstructor) { + // If it's not a constructor, use the declared type if the receiver of the method is fully + // initialized. + boolean isInitializedReceiver = !isNotFullyInitializedReceiver(methodTree); + if (isInitializedReceiver && varEle.getEnclosingElement().equals(classEle)) { + store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); } - V value = analysis.createAbstractValue(type); - if (value == null) { - continue; - } - if (TreeUtils.isConstructor(methodTree)) { - // If we are in a constructor, then we can still use the static type, but only - // if there is also an initializer that already does some initialization. - boolean found = false; - for (Pair fieldValue : fieldValues) { - if (fieldValue.first.equals(element)) { - value = value.leastUpperBound(fieldValue.second); - found = true; - break; - } - } - if (!found) { - // no initializer found, cannot use static type - continue; - } + } else { + // If it is a constructor, then only use the declared type if the field has been + // initialized. + if (fieldInitialValue.initializer != null + && varEle.getEnclosingElement().equals(classEle)) { + store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); } - JavaExpression field = new FieldAccess(receiver, fieldType, element); - store.insertValue(field, value); } } } @@ -524,7 +505,7 @@ private void addFinalLocalValues(S store, Element enclosingElement) { * Returns true if the receiver of a method or constructor might not yet be fully initialized. * * @param methodDeclTree the declaration of the method or constructor - * @return true if the receiver of a method or constructormight not yet be fully initialized + * @return true if the receiver of a method or constructor might not yet be fully initialized */ protected boolean isNotFullyInitializedReceiver(MethodTree methodDeclTree) { return TreeUtils.isConstructor(methodDeclTree); diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java index 92533292b31..229a99d6ee6 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAnalysis.java @@ -1,22 +1,24 @@ package org.checkerframework.framework.flow; -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.type.GenericAnnotatedTypeFactory; -import org.checkerframework.javacutil.Pair; /** The default org.checkerframework.dataflow analysis used in the Checker Framework. */ public class CFAnalysis extends CFAbstractAnalysis { + /** + * Creates a new {@code CFAnalysis}. + * + * @param checker the checker + * @param factory the factory + */ public CFAnalysis( BaseTypeChecker checker, - GenericAnnotatedTypeFactory factory, - List> fieldValues) { - super(checker, factory, fieldValues); + GenericAnnotatedTypeFactory factory) { + super(checker, factory); } @Override diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 38a85d5b13a..31aaa0e6b75 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -935,7 +935,7 @@ public void typeProcess(TypeElement e, TreePath p) { } if (!warnedAboutGarbageCollection) { - String gcUsageMessage = SystemPlume.gcUsageMessage(.30, 60); + String gcUsageMessage = SystemPlume.gcUsageMessage(.25, 60); if (gcUsageMessage != null) { messager.printMessage(Kind.WARNING, gcUsageMessage); warnedAboutGarbageCollection = true; diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 397e5c5e722..06bf86a074d 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -129,12 +129,14 @@ import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypeAnnotationUtils; import org.checkerframework.javacutil.TypeKindUtils; import org.checkerframework.javacutil.TypeSystemError; import org.checkerframework.javacutil.TypesUtils; import org.checkerframework.javacutil.UserError; import org.checkerframework.javacutil.trees.DetachedVarSymbol; import org.plumelib.util.CollectionsPlume; +import org.plumelib.util.ImmutableTypes; import org.plumelib.util.StringsPlume; import scenelib.annotations.el.AMethod; import scenelib.annotations.el.ATypeElement; @@ -5429,4 +5431,18 @@ public List getContractListValues(AnnotationMirror contractLis throw new BugInCF("Not a contract list annotation: " + contractListAnno); } } + + /** + * Returns true if the type is immutable. Subclasses can override this method to add types that + * are mutable, but the annotated type of an object is immutable. + * + * @param type type to test. + * @return true if the type is immutable + */ + public boolean isImmutable(TypeMirror type) { + if (type.getKind().isPrimitive()) { + return true; + } + return ImmutableTypes.isImmutable(TypeAnnotationUtils.unannotatedType(type).toString()); + } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 58b3b17e3d1..4c0c9c90ca3 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -66,6 +66,7 @@ import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.flow.CFAbstractAnalysis.FieldInitialValue; import org.checkerframework.framework.flow.CFAbstractStore; import org.checkerframework.framework.flow.CFAbstractTransfer; import org.checkerframework.framework.flow.CFAbstractValue; @@ -393,7 +394,7 @@ protected void postInit() { this.poly = createQualifierPolymorphism(); - this.analysis = createFlowAnalysis(new ArrayList<>()); + this.analysis = createFlowAnalysis(); this.transfer = analysis.getTransferFunction(); this.emptyStore = analysis.createEmptyStore(transfer.usesSequentialSemantics()); @@ -590,9 +591,12 @@ public DefaultForTypeAnnotator getDefaultForTypeAnnotator() { * *

Subclasses have to override this method to create the appropriate analysis if they do not * follow the checker naming convention. + * + * @return the appropriate flow analysis class that is used for the org.checkerframework.dataflow + * analysis */ @SuppressWarnings({"unchecked", "rawtypes"}) - protected FlowAnalysis createFlowAnalysis(List> fieldValues) { + protected FlowAnalysis createFlowAnalysis() { // Try to reflectively load the visitor. Class checkerClass = checker.getClass(); @@ -602,7 +606,7 @@ protected FlowAnalysis createFlowAnalysis(List> fie BaseTypeChecker.invokeConstructorFor( BaseTypeChecker.getRelatedClassName(checkerClass, "Analysis"), new Class[] {BaseTypeChecker.class, this.getClass(), List.class}, - new Object[] {checker, this, fieldValues}); + new Object[] {checker, this}); if (result != null) { return result; } @@ -610,12 +614,7 @@ protected FlowAnalysis createFlowAnalysis(List> fie } // If an analysis couldn't be loaded reflectively, return the default. - List> tmp = - CollectionsPlume.mapList( - (Pair fieldVal) -> - Pair.of(fieldVal.first, (CFValue) fieldVal.second), - fieldValues); - return (FlowAnalysis) new CFAnalysis(checker, (GenericAnnotatedTypeFactory) this, tmp); + return (FlowAnalysis) new CFAnalysis(checker, (GenericAnnotatedTypeFactory) this); } /** @@ -1281,7 +1280,7 @@ protected void performFlowAnalysis(ClassTree classTree) { } Queue> queue = new ArrayDeque<>(); - List> fieldValues = new ArrayList<>(); + List> fieldValues = new ArrayList<>(); // No captured store for top-level classes. queue.add(Pair.of(classTree, null)); @@ -1344,6 +1343,9 @@ protected void performFlowAnalysis(ClassTree classTree) { case VARIABLE: VariableTree vt = (VariableTree) m; ExpressionTree initializer = vt.getInitializer(); + AnnotatedTypeMirror declaredType = getAnnotatedTypeLhs(vt); + Value declaredValue = analysis.createAbstractValue(declaredType); + FieldAccess fieldExpr = (FieldAccess) JavaExpression.fromVariableTree(vt); // analyze initializer if present if (initializer != null) { boolean isStatic = vt.getModifiers().getFlags().contains(Modifier.STATIC); @@ -1357,13 +1359,14 @@ protected void performFlowAnalysis(ClassTree classTree) { true, isStatic, capturedStore); - Value value = flowResult.getValue(initializer); - if (value != null) { - // Store the abstract value for the field. - VariableElement element = TreeUtils.elementFromDeclaration(vt); - fieldValues.add(Pair.of(element, value)); + Value initializerValue = flowResult.getValue(initializer); + if (initializerValue != null) { + fieldValues.add( + new FieldInitialValue<>(fieldExpr, declaredValue, initializerValue)); + break; } } + fieldValues.add(new FieldInitialValue<>(fieldExpr, declaredValue, null)); break; case CLASS: case ANNOTATION_TYPE: @@ -1482,7 +1485,7 @@ protected void analyze( Queue> queue, Queue> lambdaQueue, UnderlyingAST ast, - List> fieldValues, + List> fieldValues, ClassTree currentClass, boolean isInitializationCode, boolean updateInitializationStore, diff --git a/framework/tests/flow2/Basic2.java b/framework/tests/flow2/Basic2.java index e21ec971041..6b38304cabb 100644 --- a/framework/tests/flow2/Basic2.java +++ b/framework/tests/flow2/Basic2.java @@ -224,8 +224,8 @@ void CF_t1(@Odd String p1, CF o) { // final fields with initializer class A { - final @Odd String f1 = null; - final String f2 = f1; + private final @Odd String f1 = null; + private final String f2 = f1; void A_t1() { @Odd String l1 = f2;