JSpecify: Reason about nullability of reads from arrays #875
Conversation
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## master #875 +/- ##
============================================
- Coverage 86.98% 86.96% -0.02%
- Complexity 1959 1967 +8
============================================
Files 77 77
Lines 6330 6352 +22
Branches 1223 1231 +8
============================================
+ Hits 5506 5524 +18
- Misses 420 421 +1
- Partials 404 407 +3 ☔ View full report in Codecov by Sentry. |
| ArrayAccessTree arrayAccess = (ArrayAccessTree) expr; | ||
| ExpressionTree arrayExpr = arrayAccess.getExpression(); | ||
| Symbol arraySymbol = ASTHelpers.getSymbol(arrayExpr); | ||
| if (arraySymbol != null) { | ||
| for (Attribute.TypeCompound t : arraySymbol.getRawTypeAttributes()) { | ||
| for (TypeAnnotationPosition.TypePathEntry entry : t.position.location) { | ||
| if (entry.tag == TypeAnnotationPosition.TypePathEntryKind.ARRAY) { | ||
| return true; | ||
| } | ||
| } |
There was a problem hiding this comment.
This is a good start! I think we want to extend this logic, as follows. Move the ARRAY_ACCESS case down under this switch:
The logic should be just to set exprMayBeNull to true iff the type of the array contents is @Nullable (similar to the logic you have already written).
Then, we need to update the dataflow logic as well; that logic is here:
For now, rather than just using defaultAssumption we can again set the nullability of the expression based on the type of the array contents. So, the logic you wrote already should be extracted to a utility method that can be called from both places. Eventually, we want to extend the dataflow logic to handle null checks, so code like if (fizz[0] != null) { fizz[0].length(); } does not issue any warnings. But that doesn't need to happen in this PR.
nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java
Outdated
Show resolved
Hide resolved
| " static void foo() {", | ||
| " if (fizz != null) {", | ||
| " String s = fizz[0];", | ||
| " // TODO: This should report due to dereference of @Nullable s", |
There was a problem hiding this comment.
The failure here has nothing to do with annotations being in both places. It's because we haven't updated our dataflow support yet.
…Tests.java Co-authored-by: Manu Sridharan <[email protected]>
This reverts commit 4b640ef.
…ity' into jspecify-array-contents-nullability
| if (arraySymbol != null) { | ||
| for (Attribute.TypeCompound t : arraySymbol.getRawTypeAttributes()) { | ||
| for (TypeAnnotationPosition.TypePathEntry entry : t.position.location) { | ||
| if (entry.tag == TypeAnnotationPosition.TypePathEntryKind.ARRAY) { |
There was a problem hiding this comment.
I think we need to check whether the annotation is actually @Nullable. This just checks for the presence of some annotation. And yes this logic should be extracted to a utility method.
| boolean isElementNullable = false; | ||
| for (Attribute.TypeCompound t : arraySymbol.getRawTypeAttributes()) { | ||
| for (TypeAnnotationPosition.TypePathEntry entry : t.position.location) { | ||
| if (entry.tag == TypeAnnotationPosition.TypePathEntryKind.ARRAY) { |
There was a problem hiding this comment.
Same comment as above, check for @Nullable
msridhar
changed the title
This is a continuation of #850 where the behavior of
@Nullableannotations on the array was modified.With this PR, the aim is to allow
@Nullableannotations on array contents in JSpecify mode, and to process these annotations when handling reads from arrays. This PR does not handle checking writes to array elements, nor does it support reasoning about null checks on array elements in local type refinement.