Skip to content

Commit 527ebbb

Browse files
committed
Transferred the proposed change for handling WPI loop for unknowninitialization annotations to NullnessAnnotatedTypeFactory
1 parent 62e269d commit 527ebbb

File tree

3 files changed

+36
-28
lines changed

3 files changed

+36
-28
lines changed

checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -961,6 +961,30 @@ public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) {
961961
}
962962
}
963963

964+
// For all assignments, If rhsmATM is Nullable or MonotonicNonNull and has
965+
// the UnknownInitialization annotation, and if the annotation is not
966+
// UnknownInitialization(java.lang.Object.class), replace it with
967+
// UnknownInitialization(java.lang.Object.class). This is because there is
968+
// likely a constructor where it hasn't been initialized, and we haven't
969+
// considered its effect. Otherwise, WPI might get stuck in a loop.
970+
@Override
971+
public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {
972+
if ((rhsATM.hasPrimaryAnnotation(Nullable.class)
973+
|| rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) {
974+
for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) {
975+
if (AnnotationUtils.areSameByName(
976+
anno, "org.checkerframework.checker.initialization.qual.UnknownInitialization")
977+
&& !anno.getAnnotationType()
978+
.toString()
979+
.equals(
980+
"@org"
981+
+ ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) {
982+
rhsATM.replaceAnnotation(UNDER_INITALIZATION);
983+
}
984+
}
985+
}
986+
}
987+
964988
@Override
965989
public boolean wpiShouldInferTypesForReceivers() {
966990
// All receivers must be non-null, or the dereference involved in

framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java

Lines changed: 3 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,6 @@
1818
import javax.lang.model.util.ElementFilter;
1919
import org.checkerframework.afu.scenelib.util.JVMNames;
2020
import org.checkerframework.checker.index.qual.Positive;
21-
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
22-
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
2321
import org.checkerframework.checker.nullness.qual.Nullable;
2422
import org.checkerframework.common.basetype.BaseTypeChecker;
2523
import org.checkerframework.dataflow.analysis.Analysis;
@@ -1003,32 +1001,9 @@ protected void updateAnnotationSet(
10031001
return;
10041002
}
10051003

1006-
// For parameters, If rhsmATM is Nullable or MonotonicNonNull and has the
1007-
// UnknownInitialization annotation, and if the annotation is not
1008-
// UnknownInitialization(java.lang.Object.class), replace it with
1009-
// UnknownInitialization(java.lang.Object.class). This is because there is
1010-
// likely a constructor where it hasn't been initialized, and we haven't
1011-
// considered its effect. Otherwise, WPI might get stuck in a loop.
1012-
if (defLoc == TypeUseLocation.PARAMETER
1013-
&& (rhsATM.hasPrimaryAnnotation(Nullable.class)
1014-
|| rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) {
1015-
for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) {
1016-
if (anno.getAnnotationType()
1017-
.asElement()
1018-
.getSimpleName()
1019-
.contentEquals("UnknownInitialization")
1020-
&& !anno.getAnnotationType()
1021-
.toString()
1022-
.equals(
1023-
"@org"
1024-
+ ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) {
1025-
AnnotationMirror unanno =
1026-
AnnotationBuilder.fromClass(
1027-
atypeFactory.getElementUtils(), UnknownInitialization.class);
1028-
rhsATM.replaceAnnotation(unanno);
1029-
}
1030-
}
1031-
}
1004+
// Update Initialization Annotations in WPI. It is only applied to
1005+
// Nullness-related qualifiers' inference to prevent possible loops.
1006+
atypeFactory.wpiAdjustForInitializationAnnotations(rhsATM);
10321007

10331008
AnnotatedTypeMirror atmFromStorage =
10341009
storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate);

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5523,6 +5523,15 @@ public boolean wpiShouldInferTypesForReceivers() {
55235523
return true;
55245524
}
55255525

5526+
/**
5527+
* Changes the type of {@code rhsATM} when being assigned to anything, for use by whole-program
5528+
* inference. The default implementation does nothing.
5529+
*
5530+
* @param rhsATM the type of the rhs of the pseudo-assignment, which is side-effected by this
5531+
* method
5532+
*/
5533+
public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {}
5534+
55265535
/**
55275536
* Side-effects the method or constructor annotations to make any desired changes before writing
55285537
* to an annotation file.

0 commit comments

Comments
 (0)