Skip to content

Commit d7acb57

Browse files
erfan-arvanerfan-arvan
committed
Changed the name of the method, enhanced the body, and transferred the method to NullnessAnnotatedTypeFactory.java to make it local for Nullness-related inference rather than for all checkers. Also added a test case for the corresponding issue in the ainfer-nullness tests.
1 parent 5b642c3 commit d7acb57

File tree

6 files changed

+293
-25
lines changed

6 files changed

+293
-25
lines changed

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

Lines changed: 25 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@
5050
import org.checkerframework.dataflow.cfg.node.Node;
5151
import org.checkerframework.dataflow.util.NodeUtils;
5252
import org.checkerframework.framework.flow.CFAbstractAnalysis;
53+
import org.checkerframework.framework.qual.TypeUseLocation;
5354
import org.checkerframework.framework.type.AnnotatedTypeFactory;
5455
import org.checkerframework.framework.type.AnnotatedTypeFormatter;
5556
import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -938,6 +939,8 @@ public boolean isImmutable(TypeMirror type) {
938939
@Override
939940
public void wpiAdjustForUpdateField(
940941
Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM) {
942+
// Adjust initialization annotations first
943+
wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.FIELD);
941944
// Synthetic variable names contain "#". Ignore them.
942945
if (!rhsATM.hasPrimaryAnnotation(Nullable.class) || fieldName.contains("#")) {
943946
return;
@@ -956,28 +959,37 @@ public void wpiAdjustForUpdateField(
956959
// then change rhs to @Nullable
957960
@Override
958961
public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) {
962+
// Adjust initialization annotations first
963+
wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.OTHERWISE);
959964
if (rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class)) {
960965
rhsATM.replaceAnnotation(NULLABLE);
961966
}
962967
}
963968

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 wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) {
969+
/**
970+
* Changes the type of {@code rhsATM} when assigned to any pseudo-assignment, for use by
971+
* whole-program inference.
972+
*
973+
* <p>If {@code rhsATM} is Nullable or MonotonicNonNull and has the UnknownInitialization
974+
* annotation, replace it with {@code UnknownInitialization(java.lang.Object.class)}. This ensures
975+
* that if there is a constructor where the type hasn't been initialized, its effect is
976+
* considered. Otherwise, whole-program inference might get stuck in a loop.
977+
*
978+
* @param rhsATM the type of the right-hand side of the pseudo-assignment, which is side-effected
979+
* by this method
980+
* @param defLoc the location where the annotation will be added. It is either a FIELD or a
981+
* non-field (OTHERWISE).
982+
*/
983+
public void wpiAdjustInitializationAnnotations(
984+
AnnotatedTypeMirror rhsATM, TypeUseLocation defLoc) {
985+
// defLoc is defined to be used in the future if needed to differentiate between field and
986+
// non-field locations
972987
if ((rhsATM.hasPrimaryAnnotation(Nullable.class)
973988
|| rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) {
974989
for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) {
975990
if (AnnotationUtils.areSameByName(
976-
anno, "org.checkerframework.checker.initialization.qual.UnknownInitialization")
977-
&& !AnnotationUtils.areSameByName(
978-
anno,
979-
"org.checkerframework.checker.initialization.qual.UnderInitialization(java.lang.Object.class")) {
980-
rhsATM.replaceAnnotation(UNDER_INITALIZATION);
991+
anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) {
992+
rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION);
981993
}
982994
}
983995
}

‎checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
import org.checkerframework.checker.initialization.qual.*;
2+
import org.checkerframework.checker.nullness.qual.*;
3+
4+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
5+
interface Game {
6+
7+
@org.checkerframework.dataflow.qual.SideEffectFree
8+
void newGame();
9+
}
10+
11+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
12+
class // package-private
13+
GameImpl implements // package-private
14+
Game {
15+
16+
private MoveValidator moveValidator;
17+
18+
@org.checkerframework.dataflow.qual.Impure
19+
public GameImpl(MoveValidator mValidator) {
20+
mValidator.setGame(this);
21+
moveValidator = mValidator;
22+
}
23+
24+
@org.checkerframework.dataflow.qual.SideEffectFree
25+
public GameImpl() {
26+
}
27+
28+
@org.checkerframework.dataflow.qual.SideEffectFree
29+
public void newGame( // package-private
30+
GameImpl this) {
31+
// Implementation of starting a new game
32+
}
33+
}
34+
35+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
36+
interface MoveValidator {
37+
38+
@org.checkerframework.dataflow.qual.Impure
39+
void setGame( MoveValidator this, Game game);
40+
}
41+
42+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
43+
class // package-private
44+
PlayerDependentMoveValidator implements // package-private
45+
MoveValidator {
46+
47+
private Game game;
48+
49+
private MoveValidator blackMoveValidator = new SimpleMoveValidator();
50+
51+
@org.checkerframework.dataflow.qual.Impure
52+
public void setGame( // package-private
53+
PlayerDependentMoveValidator this, Game game) {
54+
this.game = game;
55+
}
56+
57+
@org.checkerframework.dataflow.qual.SideEffectFree
58+
public PlayerDependentMoveValidator() {
59+
}
60+
61+
@org.checkerframework.dataflow.qual.Impure
62+
public PlayerDependentMoveValidator( Game game) {
63+
this.setGame(game);
64+
blackMoveValidator.setGame(game);
65+
}
66+
}
67+
68+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker")
69+
class // package-private
70+
SimpleMoveValidator implements // package-private
71+
MoveValidator {
72+
73+
private Game game;
74+
75+
@org.checkerframework.dataflow.qual.Impure
76+
public void setGame( // package-private
77+
SimpleMoveValidator this, Game game) {
78+
this.game = game;
79+
}
80+
81+
@org.checkerframework.dataflow.qual.SideEffectFree
82+
public SimpleMoveValidator() {
83+
}
84+
85+
@org.checkerframework.dataflow.qual.Pure
86+
public MoveValidator createMoveValidator() {
87+
return new PlayerDependentMoveValidator(game);
88+
}
89+
public void test(){
90+
PlayerDependentMoveValidator g1 =
91+
new PlayerDependentMoveValidator(game);
92+
this.game = g1.game;
93+
}
94+
}

‎checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava‎

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
import org.checkerframework.checker.initialization.qual.*;
2+
import org.checkerframework.checker.nullness.qual.*;
3+
4+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
5+
interface Game {
6+
7+
@org.checkerframework.dataflow.qual.SideEffectFree
8+
void newGame();
9+
}
10+
11+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
12+
class // package-private
13+
GameImpl implements // package-private
14+
Game {
15+
16+
private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.MonotonicNonNull MoveValidator moveValidator;
17+
18+
@org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.moveValidator" })
19+
@org.checkerframework.dataflow.qual.Impure
20+
public GameImpl(MoveValidator mValidator) {
21+
mValidator.setGame(this);
22+
moveValidator = mValidator;
23+
}
24+
25+
@org.checkerframework.dataflow.qual.SideEffectFree
26+
public GameImpl() {
27+
}
28+
29+
@org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.moveValidator" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class)
30+
@org.checkerframework.dataflow.qual.SideEffectFree
31+
public void newGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private
32+
GameImpl this) {
33+
// Implementation of starting a new game
34+
}
35+
}
36+
37+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
38+
interface MoveValidator {
39+
40+
@org.checkerframework.dataflow.qual.Impure
41+
void setGame(@org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game);
42+
}
43+
44+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
45+
class // package-private
46+
PlayerDependentMoveValidator implements // package-private
47+
MoveValidator {
48+
49+
private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game;
50+
51+
private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull MoveValidator blackMoveValidator = new SimpleMoveValidator();
52+
53+
@org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.game" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class)
54+
@org.checkerframework.dataflow.qual.Impure
55+
public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private
56+
PlayerDependentMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) {
57+
this.game = game;
58+
}
59+
60+
@org.checkerframework.dataflow.qual.SideEffectFree
61+
public PlayerDependentMoveValidator() {
62+
}
63+
64+
@org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "#1" })
65+
@org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" })
66+
@org.checkerframework.dataflow.qual.Impure
67+
public PlayerDependentMoveValidator(@org.checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) {
68+
this.setGame(game);
69+
blackMoveValidator.setGame(game);
70+
}
71+
}
72+
73+
@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker")
74+
class // package-private
75+
SimpleMoveValidator implements // package-private
76+
MoveValidator {
77+
78+
private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.MonotonicNonNull Game game;
79+
80+
@org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" })
81+
@org.checkerframework.dataflow.qual.Impure
82+
public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private
83+
SimpleMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.NonNull Game game) {
84+
this.game = game;
85+
}
86+
87+
@org.checkerframework.dataflow.qual.SideEffectFree
88+
public SimpleMoveValidator() {
89+
}
90+
91+
@org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" })
92+
@org.checkerframework.dataflow.qual.Pure
93+
public @org.checkerframework.checker.initialization.qual.UnderInitialization(PlayerDependentMoveValidator.class) @org.checkerframework.checker.nullness.qual.NonNull MoveValidator createMoveValidator() {
94+
return new PlayerDependentMoveValidator(game);
95+
}
96+
public void test(){
97+
PlayerDependentMoveValidator g1 =
98+
new PlayerDependentMoveValidator(game);
99+
this.game = g1.game;
100+
}
101+
}

‎checker/tests/ainfer-nullness/non-annotated/Game.java‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
import org.checkerframework.checker.initialization.qual.*;
2+
import org.checkerframework.checker.nullness.qual.*;
3+
4+
interface Game {
5+
void newGame();
6+
}
7+
8+
class GameImpl implements Game { // package-private
9+
private MoveValidator moveValidator;
10+
11+
public GameImpl(MoveValidator mValidator) {
12+
mValidator.setGame(this);
13+
moveValidator = mValidator;
14+
}
15+
16+
public GameImpl() {}
17+
18+
@Override
19+
public void newGame() {
20+
// Implementation of starting a new game
21+
}
22+
}
23+
24+
interface MoveValidator {
25+
void setGame(Game game);
26+
}
27+
28+
class PlayerDependentMoveValidator implements MoveValidator { // package-private
29+
public Game game;
30+
private MoveValidator blackMoveValidator = new SimpleMoveValidator();
31+
32+
@SuppressWarnings({"override.param", "contracts.postcondition"})
33+
@Override
34+
public void setGame(Game game) {
35+
this.game = game;
36+
}
37+
38+
public PlayerDependentMoveValidator() {}
39+
40+
@SuppressWarnings({"contracts.postcondition", "argument", "method.invocation"})
41+
public PlayerDependentMoveValidator(Game game) {
42+
this.setGame(game);
43+
blackMoveValidator.setGame(game);
44+
}
45+
}
46+
47+
class SimpleMoveValidator implements MoveValidator { // package-private
48+
private Game game;
49+
50+
@SuppressWarnings({"override.param", "contracts.postcondition"})
51+
@Override
52+
public void setGame(Game game) {
53+
this.game = game;
54+
}
55+
56+
public SimpleMoveValidator() {}
57+
58+
@SuppressWarnings({
59+
"purity.not.deterministic.object.creation",
60+
"purity" + ".not.sideeffectfree.call",
61+
"contracts.postcondition",
62+
"return"
63+
})
64+
public MoveValidator createMoveValidator() {
65+
return new PlayerDependentMoveValidator(game);
66+
}
67+
68+
public void test() {
69+
PlayerDependentMoveValidator g1 = new PlayerDependentMoveValidator(game);
70+
// :: warning: (assignment)
71+
this.game = g1.game;
72+
}
73+
}

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1001,9 +1001,6 @@ protected void updateAnnotationSet(
10011001
return;
10021002
}
10031003

1004-
// Update the right-hand side (rhs) annotations if necessary before updating the annotation set
1005-
atypeFactory.wpiAdjustAnnotationsBeforeUpdate(rhsATM);
1006-
10071004
AnnotatedTypeMirror atmFromStorage =
10081005
storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate);
10091006
updateAtmWithLub(rhsATM, atmFromStorage);

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

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5523,15 +5523,6 @@ 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 wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) {}
5534-
55355526
/**
55365527
* Side-effects the method or constructor annotations to make any desired changes before writing
55375528
* to an annotation file.

0 commit comments

Comments
 (0)