Skip to content

Commit aaf9f08

Browse files
armughan11msridhar
andauthored
Add support for static fields in contracts (#1118)
This PR adds support for static fields in `@EnsureNonnull`,`EnsureNonnullIf`,`@RequiresNonnull` annotations. Currently the following code will throw validation errors (as well as the annotation handlers are unable to handle static fields). However, after this change, static fields for all three annotations are supported ``` class Foo { @nullable static Item staticNullableItem; @EnsuresNonNull("staticNullableItem") public static void initializeStaticField() { staticNullableItem = new Item(); } @RequiresNonNull("staticNullableItem") public static void useStaticField() { staticNullableItem.call(); } @EnsuresNonNullIf(value="staticNullableItem", result=true) public static boolean hasStaticNullableItem() { return staticNullableItem != null; } } ``` Fixes #431 --------- Co-authored-by: Manu Sridharan <[email protected]>
1 parent 43054bb commit aaf9f08

File tree

8 files changed

+354
-25
lines changed

8 files changed

+354
-25
lines changed

nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPath.java

+13
Original file line numberDiff line numberDiff line change
@@ -369,6 +369,19 @@ public static AccessPath fromFieldElement(VariableElement element) {
369369
return new AccessPath(null, ImmutableList.of(new FieldOrMethodCallElement(element)));
370370
}
371371

372+
/**
373+
* Constructs an access path representing a static field.
374+
*
375+
* @param element element that must represent a static field
376+
* @return an access path representing the static field
377+
*/
378+
public static AccessPath fromStaticField(VariableElement element) {
379+
Preconditions.checkArgument(
380+
element.getKind().isField() && element.getModifiers().contains(Modifier.STATIC),
381+
"element must be a static field but received: " + element.getKind());
382+
return new AccessPath(element, ImmutableList.of(), null);
383+
}
384+
372385
private static boolean isBoxingMethod(Symbol.MethodSymbol methodSymbol) {
373386
if (methodSymbol.isStatic() && methodSymbol.getSimpleName().contentEquals("valueOf")) {
374387
Symbol.PackageSymbol enclosingPackage = ASTHelpers.enclosingPackage(methodSymbol.enclClass());

nullaway/src/main/java/com/uber/nullaway/dataflow/NullnessStore.java

+19
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@
3232
import java.util.stream.Collectors;
3333
import javax.lang.model.element.Element;
3434
import javax.lang.model.element.ElementKind;
35+
import javax.lang.model.element.Modifier;
3536
import org.checkerframework.nullaway.dataflow.analysis.Store;
3637
import org.checkerframework.nullaway.dataflow.cfg.node.FieldAccessNode;
3738
import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode;
@@ -272,6 +273,24 @@ public Set<Element> getNonNullReceiverFields() {
272273
return getReceiverFields(Nullness.NONNULL);
273274
}
274275

276+
/**
277+
* Return all the static fields in the store that are Non-Null.
278+
*
279+
* @return Set of static fields (represented as {@code Element}s) that are non-null
280+
*/
281+
public Set<Element> getNonNullStaticFields() {
282+
Set<AccessPath> nonnullAccessPaths = this.getAccessPathsWithValue(Nullness.NONNULL);
283+
Set<Element> result = new LinkedHashSet<>();
284+
for (AccessPath ap : nonnullAccessPaths) {
285+
if (ap.getRoot() != null) {
286+
if (ap.getRoot().getModifiers().contains(Modifier.STATIC)) {
287+
result.add(ap.getRoot());
288+
}
289+
}
290+
}
291+
return result;
292+
}
293+
275294
/**
276295
* Return all the fields in the store that hold the {@code nullness} state.
277296
*

nullaway/src/main/java/com/uber/nullaway/handlers/AbstractFieldContractHandler.java

+40-6
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,32 @@ protected boolean validateAnnotationSyntax(
163163
null));
164164
return false;
165165
} else {
166+
Symbol.ClassSymbol classSymbol =
167+
castToNonNull(ASTHelpers.enclosingClass(methodAnalysisContext.methodSymbol()));
166168
for (String fieldName : content) {
169+
if (isThisDotStaticField(classSymbol, fieldName)) {
170+
171+
message =
172+
"Cannot refer to static field "
173+
+ fieldName.substring(THIS_NOTATION.length())
174+
+ " using this.";
175+
state.reportMatch(
176+
analysis
177+
.getErrorBuilder()
178+
.createErrorDescription(
179+
new ErrorMessage(ErrorMessage.MessageTypes.ANNOTATION_VALUE_INVALID, message),
180+
tree,
181+
analysis.buildDescription(tree),
182+
state,
183+
null));
184+
return false;
185+
}
186+
VariableElement field = getFieldOfClass(classSymbol, fieldName);
187+
if (field != null) {
188+
if (field.getModifiers().contains(Modifier.STATIC)) {
189+
continue;
190+
}
191+
}
167192
if (fieldName.contains(".")) {
168193
if (!fieldName.startsWith(THIS_NOTATION)) {
169194
message =
@@ -188,9 +213,7 @@ protected boolean validateAnnotationSyntax(
188213
fieldName = fieldName.substring(fieldName.lastIndexOf(".") + 1);
189214
}
190215
}
191-
Symbol.ClassSymbol classSymbol =
192-
castToNonNull(ASTHelpers.enclosingClass(methodAnalysisContext.methodSymbol()));
193-
VariableElement field = getInstanceFieldOfClass(classSymbol, fieldName);
216+
field = getFieldOfClass(classSymbol, fieldName);
194217
if (field == null) {
195218
message =
196219
"For @"
@@ -223,20 +246,31 @@ protected boolean validateAnnotationSyntax(
223246
* @param name Name of the field.
224247
* @return The field with the given name, or {@code null} if the field cannot be found
225248
*/
226-
public static @Nullable VariableElement getInstanceFieldOfClass(
249+
public static @Nullable VariableElement getFieldOfClass(
227250
Symbol.ClassSymbol classSymbol, String name) {
228251
Preconditions.checkNotNull(classSymbol);
229252
for (Element member : getEnclosedElements(classSymbol)) {
230-
if (member.getKind().isField() && !member.getModifiers().contains(Modifier.STATIC)) {
253+
if (member.getKind().isField()) {
231254
if (member.getSimpleName().toString().equals(name)) {
232255
return (VariableElement) member;
233256
}
234257
}
235258
}
236259
Symbol.ClassSymbol superClass = (Symbol.ClassSymbol) classSymbol.getSuperclass().tsym;
237260
if (superClass != null) {
238-
return getInstanceFieldOfClass(superClass, name);
261+
return getFieldOfClass(superClass, name);
239262
}
240263
return null;
241264
}
265+
266+
protected boolean isThisDotStaticField(Symbol.ClassSymbol classSymbol, String expression) {
267+
if (expression.contains(".")) {
268+
if (expression.startsWith(THIS_NOTATION)) {
269+
String fieldName = expression.substring(THIS_NOTATION.length());
270+
VariableElement field = getFieldOfClass(classSymbol, fieldName);
271+
return field != null && field.getModifiers().contains(Modifier.STATIC);
272+
}
273+
}
274+
return false;
275+
}
242276
}

nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullHandler.java

+20-5
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,10 @@
4040
import com.uber.nullaway.handlers.MethodAnalysisContext;
4141
import com.uber.nullaway.handlers.contract.ContractUtils;
4242
import java.util.Collections;
43+
import java.util.HashSet;
4344
import java.util.Set;
4445
import java.util.stream.Collectors;
46+
import javax.lang.model.element.Modifier;
4547
import javax.lang.model.element.VariableElement;
4648
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
4749

@@ -85,14 +87,26 @@ protected boolean validateAnnotationSemantics(
8587
.stream()
8688
.map(e -> e.getSimpleName().toString())
8789
.collect(Collectors.toSet());
90+
Set<String> nonnullStaticFieldsAtExit =
91+
analysis
92+
.getNullnessAnalysis(state)
93+
.getNonnullStaticFieldsAtExit(new TreePath(state.getPath(), tree), state.context)
94+
.stream()
95+
.map(e -> e.getSimpleName().toString())
96+
.collect(Collectors.toSet());
97+
Set<String> nonnullFieldsAtExit = new HashSet<String>();
98+
nonnullFieldsAtExit.addAll(nonnullFieldsOfReceiverAtExit);
99+
nonnullFieldsAtExit.addAll(nonnullStaticFieldsAtExit);
88100
Set<String> fieldNames = getAnnotationValueArray(methodSymbol, annotName, false);
89101
if (fieldNames == null) {
90102
fieldNames = Collections.emptySet();
91103
}
92104
fieldNames = ContractUtils.trimReceivers(fieldNames);
93-
boolean isValidLocalPostCondition = nonnullFieldsOfReceiverAtExit.containsAll(fieldNames);
105+
106+
nonnullFieldsAtExit = ContractUtils.trimReceivers(nonnullFieldsAtExit);
107+
boolean isValidLocalPostCondition = nonnullFieldsAtExit.containsAll(fieldNames);
94108
if (!isValidLocalPostCondition) {
95-
fieldNames.removeAll(nonnullFieldsOfReceiverAtExit);
109+
fieldNames.removeAll(nonnullFieldsAtExit);
96110
message =
97111
String.format(
98112
"Method is annotated with @EnsuresNonNull but fails to ensure the following fields are non-null at exit: %s",
@@ -153,14 +167,15 @@ public NullnessHint onDataflowVisitMethodInvocation(
153167
fieldNames = ContractUtils.trimReceivers(fieldNames);
154168
for (String fieldName : fieldNames) {
155169
VariableElement field =
156-
getInstanceFieldOfClass(
157-
castToNonNull(ASTHelpers.enclosingClass(methodSymbol)), fieldName);
170+
getFieldOfClass(castToNonNull(ASTHelpers.enclosingClass(methodSymbol)), fieldName);
158171
if (field == null) {
159172
// Invalid annotation, will result in an error during validation. For now, skip field.
160173
continue;
161174
}
162175
AccessPath accessPath =
163-
AccessPath.fromBaseAndElement(node.getTarget().getReceiver(), field, apContext);
176+
field.getModifiers().contains(Modifier.STATIC)
177+
? AccessPath.fromStaticField(field)
178+
: AccessPath.fromBaseAndElement(node.getTarget().getReceiver(), field, apContext);
164179
if (accessPath == null) {
165180
continue;
166181
}

nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/EnsuresNonNullIfHandler.java

+11-3
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@
5151
import javax.lang.model.element.AnnotationMirror;
5252
import javax.lang.model.element.AnnotationValue;
5353
import javax.lang.model.element.ExecutableElement;
54+
import javax.lang.model.element.Modifier;
5455
import javax.lang.model.element.VariableElement;
5556
import org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode;
5657
import org.jspecify.annotations.Nullable;
@@ -184,6 +185,11 @@ public void onDataflowVisitReturn(
184185
chosenStore.getNonNullReceiverFields().stream()
185186
.map(e -> e.getSimpleName().toString())
186187
.collect(Collectors.toSet());
188+
Set<String> nonNullStaticFieldsInPath =
189+
chosenStore.getNonNullStaticFields().stream()
190+
.map(e -> e.getSimpleName().toString())
191+
.collect(Collectors.toSet());
192+
nonNullFieldsInPath.addAll(nonNullStaticFieldsInPath);
187193
boolean allFieldsAreNonNull = nonNullFieldsInPath.containsAll(fieldNames);
188194

189195
// Whether the return true expression evaluates to a boolean literal or not. If null, then not
@@ -297,14 +303,16 @@ public NullnessHint onDataflowVisitMethodInvocation(
297303
trueIfNonNull ? thenUpdates : elseUpdates;
298304
for (String fieldName : fieldNames) {
299305
VariableElement field =
300-
getInstanceFieldOfClass(
301-
castToNonNull(ASTHelpers.enclosingClass(methodSymbol)), fieldName);
306+
getFieldOfClass(castToNonNull(ASTHelpers.enclosingClass(methodSymbol)), fieldName);
302307
if (field == null) {
303308
// Invalid annotation, will result in an error during validation.
304309
continue;
305310
}
306311
AccessPath accessPath =
307-
AccessPath.fromBaseAndElement(node.getTarget().getReceiver(), field, apContext);
312+
field.getModifiers().contains(Modifier.STATIC)
313+
? AccessPath.fromStaticField(field)
314+
: AccessPath.fromFieldElement(field);
315+
308316
if (accessPath == null) {
309317
// Also likely to be an invalid annotation, will result in an error during validation.
310318
continue;

nullaway/src/main/java/com/uber/nullaway/handlers/contract/fieldcontract/RequiresNonNullHandler.java

+40-4
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,12 @@
4343
import com.uber.nullaway.handlers.MethodAnalysisContext;
4444
import com.uber.nullaway.handlers.contract.ContractUtils;
4545
import java.util.Collections;
46+
import java.util.HashSet;
4647
import java.util.Iterator;
4748
import java.util.List;
4849
import java.util.Set;
50+
import javax.lang.model.element.Element;
51+
import javax.lang.model.element.Modifier;
4952
import javax.lang.model.element.VariableElement;
5053
import org.checkerframework.nullaway.dataflow.cfg.UnderlyingAST;
5154
import org.checkerframework.nullaway.dataflow.cfg.node.LocalVariableNode;
@@ -145,11 +148,35 @@ public void onMatchMethodInvocation(
145148
Symbol.ClassSymbol classSymbol = ASTHelpers.enclosingClass(methodSymbol);
146149
Preconditions.checkNotNull(
147150
classSymbol, "Could not find the enclosing class for method symbol: " + methodSymbol);
148-
VariableElement field = getInstanceFieldOfClass(classSymbol, fieldName);
151+
VariableElement field = getFieldOfClass(classSymbol, fieldName);
149152
if (field == null) {
150153
// we will report an error on the method declaration
151154
continue;
152155
}
156+
if (field.getModifiers().contains(Modifier.STATIC)) {
157+
Set<Element> nonnullStaticFields =
158+
analysis
159+
.getNullnessAnalysis(state)
160+
.getNonnullStaticFieldsBefore(state.getPath(), state.context);
161+
162+
if (!nonnullStaticFields.contains(field)) {
163+
String message =
164+
"Expected static field "
165+
+ fieldName
166+
+ " to be non-null at call site due to @RequiresNonNull annotation on invoked method";
167+
state.reportMatch(
168+
analysis
169+
.getErrorBuilder()
170+
.createErrorDescription(
171+
new ErrorMessage(
172+
ErrorMessage.MessageTypes.PRECONDITION_NOT_SATISFIED, message),
173+
tree,
174+
analysis.buildDescription(tree),
175+
state,
176+
null));
177+
}
178+
continue;
179+
}
153180
ExpressionTree methodSelectTree = tree.getMethodSelect();
154181
Nullness nullness =
155182
analysis
@@ -195,14 +222,23 @@ public NullnessStore.Builder onDataflowInitialStore(
195222
if (fieldNames == null) {
196223
return result;
197224
}
198-
fieldNames = ContractUtils.trimReceivers(fieldNames);
225+
Set<String> filteredFieldNames = new HashSet<>();
199226
for (String fieldName : fieldNames) {
200-
VariableElement field = getInstanceFieldOfClass(ASTHelpers.getSymbol(classTree), fieldName);
227+
if (!isThisDotStaticField(ASTHelpers.getSymbol(classTree), fieldName)) {
228+
filteredFieldNames.add(fieldName);
229+
}
230+
}
231+
filteredFieldNames = ContractUtils.trimReceivers(filteredFieldNames);
232+
for (String fieldName : filteredFieldNames) {
233+
VariableElement field = getFieldOfClass(ASTHelpers.getSymbol(classTree), fieldName);
201234
if (field == null) {
202235
// Invalid annotation, will result in an error during validation. For now, skip field.
203236
continue;
204237
}
205-
AccessPath accessPath = AccessPath.fromFieldElement(field);
238+
AccessPath accessPath =
239+
field.getModifiers().contains(Modifier.STATIC)
240+
? AccessPath.fromStaticField(field)
241+
: AccessPath.fromFieldElement(field);
206242
result.setInformation(accessPath, Nullness.NONNULL);
207243
}
208244
return result;

nullaway/src/test/java/com/uber/nullaway/EnsuresNonNullIfTests.java

+55
Original file line numberDiff line numberDiff line change
@@ -893,4 +893,59 @@ public void ensuresNonNullMethodResultStoredInVariableInverse() {
893893
"Item.java", "package com.uber;", "class Item {", " public void call() { }", "}")
894894
.doTest();
895895
}
896+
897+
@Test
898+
public void staticFieldCorrectUse() {
899+
defaultCompilationHelper
900+
.addSourceLines(
901+
"Foo.java",
902+
"package com.uber;",
903+
"import javax.annotation.Nullable;",
904+
"import com.uber.nullaway.annotations.EnsuresNonNullIf;",
905+
"class Foo {",
906+
" @Nullable static Item staticNullableItem;",
907+
" @EnsuresNonNullIf(value=\"staticNullableItem\", result=true)",
908+
" public static boolean hasStaticNullableItem() {",
909+
" return staticNullableItem != null;",
910+
" }",
911+
" public static int runOk() {",
912+
" if(!hasStaticNullableItem()) {",
913+
" return 1;",
914+
" }",
915+
" staticNullableItem.call();",
916+
" return 0;",
917+
" }",
918+
"}")
919+
.addSourceLines(
920+
"Item.java", "package com.uber;", "class Item {", " public void call() { }", "}")
921+
.doTest();
922+
}
923+
924+
@Test
925+
public void staticFieldIncorrectUse() {
926+
defaultCompilationHelper
927+
.addSourceLines(
928+
"Foo.java",
929+
"package com.uber;",
930+
"import javax.annotation.Nullable;",
931+
"import com.uber.nullaway.annotations.EnsuresNonNullIf;",
932+
"class Foo {",
933+
" @Nullable static Item nullableItem;",
934+
" @EnsuresNonNullIf(value=\"nullableItem\", result=true)",
935+
" public boolean hasNullableItem() {",
936+
" return nullableItem != null;",
937+
" }",
938+
" public int runOk() {",
939+
" if(hasNullableItem()) {",
940+
" nullableItem.call();",
941+
" }",
942+
" // BUG: Diagnostic contains: dereferenced expression nullableItem is @Nullable",
943+
" nullableItem.call();",
944+
" return 0;",
945+
" }",
946+
"}")
947+
.addSourceLines(
948+
"Item.java", "package com.uber;", "class Item {", " public void call() { }", "}")
949+
.doTest();
950+
}
896951
}

0 commit comments

Comments
 (0)