JSpecify: Modify Array Type Use Annotation Syntax #850

armughan11 · 2023-10-18T22:11:27Z

Currently, NullAway does not support @Nullable annotations on array elements (#708). Both @Nullable String[] and String @Nullable [] are currently treated identically, and NullAway considers both annotations as the array itself might be null.

This is the first step to bring the annotation syntax in line with JSpecify norms, which treats @Nullable String[] as the array elements could be null while String @Nullable [] implies the array itself could be null.

After this change, NullAway completely ignores type-use annotations on array element types, such as @Nullable String[], and only considers type-use annotations on the top-level type, i.e., String @Nullable []. This is an intermediary change, and support for type-use annotations on array element types will be added eventually. Additionally, this only applies to JSpecify mode.

Note that for now, handling of declaration annotations is unchanged; we will very likely revisit this in the future.

Unit tests currently conform to the current behavior of NullAway after the changes and some tests have TODOs until we are able to detect the nullability of array elements.

Added Unit Tests for @nullable annotations on array in JSpecify mode and modified behaviour.

Minor changes and better documentation

codecov · 2023-10-19T01:08:53Z

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (bc94dcc) 86.90% compared to head (b6318af) 86.92%.
Report is 1 commits behind head on master.

Additional details and impacted files

@@             Coverage Diff              @@
##             master     #850      +/-   ##
============================================
+ Coverage     86.90%   86.92%   +0.02%     
- Complexity     1879     1883       +4     
============================================
  Files            74       74              
  Lines          6199     6210      +11     
  Branches       1202     1206       +4     
============================================
+ Hits           5387     5398      +11     
  Misses          405      405              
  Partials        407      407

Files	Coverage Δ
...away/src/main/java/com/uber/nullaway/NullAway.java	`89.78% <100.00%> (+<0.01%)`	⬆️
...c/main/java/com/uber/nullaway/NullabilityUtil.java	`85.71% <100.00%> (+0.39%)`	⬆️
...away/src/main/java/com/uber/nullaway/Nullness.java	`85.07% <100.00%> (ø)`
...ullaway/dataflow/CoreNullnessStoreInitializer.java	`100.00% <100.00%> (ø)`

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

msridhar · 2023-10-20T16:56:18Z

This is the first step to bring the annotation syntax in line with JSpecify norms, which treats @Nullable String[] as the array itself could be null while String @Nullable [] implies the array elements could be null.

This is actually the reverse of JSpecify, right?

After this change, NullAway completely ignores annotations on type, such as @Nullable String[], and only considers, String @Nullable []. However, this is an intermediary change, and this behavior will eventually be modified to conform to JSpecify syntax.

This change is only in JSpecify mode, correct?

msridhar

Promising start! The review is incomplete, as I think there is some confusion as to what the JSpecify spec is saying about where @Nullable annotations should go on an array type. See the comments for details.

msridhar · 2023-10-20T17:05:12Z

nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

+          // Currently we are ignoring @Nullable annotations on type in JSpecify mode.
+          // Eventually, this should return true, and array access should be handled
+          // elsewhere.


Why do we say this should eventually return true? I added some docs to the enclosing method, and I think what it is meant to do is determine whether an annotation applies to a top-level type. Given that, shouldn't this method always return false in this spot in JSpecify mode?

I think this and all subsequent comments are attributed to my fallacy that it works the other way around. All of these are actually working as we want them to. Will clean these up!

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

msridhar · 2023-10-20T17:10:03Z

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

+            "    // This currently reports an error since fizz is @Nullable,",
+            "    // but it should eventually report due to fizz[0] being @Nullable",
+            "    // BUG: Diagnostic contains: dereferenced expression fizz is @Nullable",
+            "    int bar = fizz[0].length();",


This error is correct I think.

armughan11 · 2023-10-20T17:16:11Z

This is the first step to bring the annotation syntax in line with JSpecify norms, which treats @Nullable String[] as the array itself could be null while String @Nullable [] implies the array elements could be null.

This is actually the reverse of JSpecify, right?

@msridhar, That's correct, I actually thought it was the other way around.
Most of my comments are because of this fallacy, that's why it's a tad confusing

armughan11 · 2023-10-20T17:21:45Z

This change is only in JSpecify mode, correct?

That's correct, this is the only implementation change that has been made, and it's only for JSpecify mode.

msridhar

Looking better! A few more comments

nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

msridhar · 2023-10-21T01:00:59Z

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

+        .doTest();
+  }
+
+  @Ignore("Array type annotations aren't supported currently.")


Rather than doing @Ignore let's put a TODO comment within the test. The test serves a useful purpose of checking that writing @Nullable String [] does not apply the annotation to the top-level type in JSpecify mode.

msridhar · 2023-10-21T01:01:23Z

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

+        .doTest();
+  }
+
+  @Ignore("Array type annotations aren't supported currently.")


Same comment as above about not ignoring

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

…pecify-array-handling

msridhar

Mostly LGTM, just all tests need to be renamed to be consistent with the other fixes

msridhar · 2023-10-23T04:40:07Z

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

+public class NullAwayJSpecifyArrayTests extends NullAwayTestsBase {
+
+  @Test
+  public void arrayDimensionAnnotationDereference() {


Test needs to be renamed; annotation is now on top-level type

msridhar · 2023-10-23T04:40:20Z

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

+  }
+
+  @Test
+  public void arrayDimensionAnnotationAssignment() {


another test rename

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

msridhar · 2023-10-23T04:43:30Z

@lazaroclapp it'd be good if you could take a quick look at this one when you get time. Basically, with this change, in JSpecify mode, we only recognize top-level nullability annotations on array type when they are in the right place

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

msridhar

Approved with a couple more minor renames. Would still like @lazaroclapp to take a look before we land this one

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

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

lazaroclapp

Overall, I don't have a lot of "requires changes" level comments, but I do have a few questions :)

General question, mostly for @msridhar, because I forget context: Did we decide whether JSpecify rules apply only to type use annotations or do they apply to any annotation kind as long as we are on JSpecify mode? I remember the discussion as fairly involved and subtle, but whichever one we chose, either the title or description of this PR are wrong (title says "Type Use", description makes no mention of the distinction). @msridhar I believe we said for consistency the new rules would apply to any nullability annotation, type use or not, so long as JSpecify mode was enabled? (Otherwise it might be too confusing for devs and codebases with mixed JSpecify and javax annotations should be avoided, auto-migrated, anyways...)

I understand if this PR doesn't make all the changes needed for the above all at once, but then description should provide that context.

nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

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

Co-authored-by: Lázaro Clapp <lazaro.clapp@gmail.com>

msridhar · 2023-10-25T15:53:25Z

General question, mostly for @msridhar, because I forget context: Did we decide whether JSpecify rules apply only to type use annotations or do they apply to any annotation kind as long as we are on JSpecify mode? I remember the discussion as fairly involved and subtle, but whichever one we chose, either the title or description of this PR are wrong (title says "Type Use", description makes no mention of the distinction). @msridhar I believe we said for consistency the new rules would apply to any nullability annotation, type use or not, so long as JSpecify mode was enabled? (Otherwise it might be too confusing for devs and codebases with mixed JSpecify and javax annotations should be avoided, auto-migrated, anyways...)

Hrm, I see the issue. I think what we wanted was that for JSpecify mode, we would only recognize top-level type annotations in the "right" place for arrays. But, I realize now that with this PR, we are only checking type use annotations. If someone writes @Nullable String [] foo where @Nullable is a declaration annotation (like from javax.annotation) I think we'll still pick it up as applying to the top-level type. (@armughan11 we should add a test for this.)

I'm not sure what we should do about this. It is very confusing that one could write @Nullable String [] foo in two different parts of a code base and have it mean different things depending on whether the imported @Nullable annotation is declaration vs type use. But, if we decided to just ignore declaration annotations on array variable declarations in JSpecify mode, the same problem would still be there. So maybe the approach of this PR is no worse than the alternative? Hrm, or maybe we should (eventually) add a NullAway warning in JSpecify mode for any use of an old-style declaration @Nullable annotation? @lazaroclapp thoughts welcome :-)

lazaroclapp · 2023-10-25T22:05:28Z

Hrm, or maybe we should (eventually) add a NullAway warning in JSpecify mode for any use of an old-style declaration @Nullable annotation? @lazaroclapp thoughts welcome :-)

I think this might end up being the safest bet. The other alternatives are: a) inconsistent semantics for @Nullable seemingly only dependent on the annotation FQN, or b) "ignored" @Nullable declaration annotations (guess not ignored per-se, they would just apply to the elements, no?).

Maybe (b) is still better, with the caveat that we really want to flag it as a problem for the developer if they have such mixed annotation types at all... (i.e. any javax... nullability annotation when running on JSpecify mode. Either way, I am fine with those semantics being outside of the scope of this PR.

lazaroclapp

See comment on still probably wanting a test for @Nullable String [] fizz; fizz[1];. Other than that, I think this is fine by me for this PR and the other discussion above is more long term 😀

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

This is a continuation of #850 where the behavior of `@Nullable` annotations on the array was modified. With this PR, the aim is to allow `@Nullable` annotations 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. --------- Co-authored-by: Manu Sridharan <msridhar@gmail.com>

Modify JSpecify Array Handling

f1ba82a

Added Unit Tests for @nullable annotations on array in JSpecify mode and modified behaviour.

armughan11 changed the title ~~Added unit tests & modify JSpecify Array Type Use Annotation behavior~~ JSpecify: Modify Array Type Use Annotation Syntax Oct 18, 2023

armughan11 added 2 commits October 18, 2023 17:50

Fix incorrect wildcard/inner type handling in JSpecify mode

4bdd570

Fix Unit Tests

06e816e

Minor changes and better documentation

armughan11 marked this pull request as ready for review October 19, 2023 01:04

armughan11 added 2 commits October 19, 2023 15:23

Update comment

6a19f36

Merge branch 'master' into jspecify-array-handling

d1e0cb2

msridhar added 2 commits October 20, 2023 10:03

add some documentation

2b6d746

remove extra blank line

622ecc4

msridhar reviewed Oct 20, 2023

View reviewed changes

armughan11 added 4 commits October 20, 2023 14:52

Merge branch 'uber:master' into jspecify-array-handling

96bc62b

Fixed docs

7f9947b

Fixed docs

b02eedd

remove space

0389903

armughan11 requested a review from msridhar October 20, 2023 22:38

msridhar reviewed Oct 21, 2023

View reviewed changes

armughan11 and others added 4 commits October 21, 2023 19:52

Update JSpecify escape comment

4fd6df6

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

update test cases with TODO

ac5598b

Merge remote-tracking branch 'origin/jspecify-array-handling' into js…

b1a3f5c

…pecify-array-handling

replace ignore with TODO

f037985

armughan11 requested a review from msridhar October 22, 2023 03:03

msridhar reviewed Oct 23, 2023

View reviewed changes

msridhar requested a review from lazaroclapp October 23, 2023 04:42

armughan11 and others added 2 commits October 22, 2023 21:48

FIx comment

c41de6e

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

update unit test names

49cf926

armughan11 requested a review from msridhar October 23, 2023 04:53

msridhar approved these changes Oct 23, 2023

View reviewed changes

nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java Outdated Show resolved Hide resolved

nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java Outdated Show resolved Hide resolved

armughan11 and others added 2 commits October 23, 2023 16:22

Update test names

d7783de

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

Update test name

5726080

Co-authored-by: Manu Sridharan <msridhar@gmail.com>

lazaroclapp reviewed Oct 25, 2023

View reviewed changes

msridhar and others added 3 commits October 25, 2023 16:20

Update nullaway/src/main/java/com/uber/nullaway/NullabilityUtil.java

23802f2

Co-authored-by: Lázaro Clapp <lazaro.clapp@gmail.com>

Merge branch 'master' into jspecify-array-handling

adcce63

formatting

c139e13

armughan11 added 2 commits October 25, 2023 08:53

add true negative case for element annotation

c328b82

add declaration annotation tests

48824bb

armughan11 requested a review from msridhar October 25, 2023 21:25

lazaroclapp approved these changes Oct 25, 2023

View reviewed changes

nullaway/src/test/java/com/uber/nullaway/NullAwayJSpecifyArrayTests.java Show resolved Hide resolved

msridhar added 2 commits October 25, 2023 23:19

add test for fizz[0] when fizz is @nullable

5816c99

use javadoc

b6318af

msridhar enabled auto-merge (squash) October 25, 2023 22:24

msridhar mentioned this pull request Oct 25, 2023

Handling of declaration annotations in JSpecify mode #853

Open

msridhar merged commit def015a into uber:master Oct 25, 2023
10 checks passed

armughan11 mentioned this pull request Dec 6, 2023

JSpecify: Reason about nullability of reads from arrays #875

Merged

armughan11 deleted the jspecify-array-handling branch June 3, 2024 02:02

armughan11 restored the jspecify-array-handling branch June 3, 2024 02:02

armughan11 deleted the jspecify-array-handling branch June 3, 2024 02:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

JSpecify: Modify Array Type Use Annotation Syntax #850

JSpecify: Modify Array Type Use Annotation Syntax #850

armughan11 commented Oct 18, 2023 •

edited by msridhar

Loading

codecov bot commented Oct 19, 2023 •

edited

Loading

msridhar commented Oct 20, 2023

msridhar left a comment

msridhar Oct 20, 2023

armughan11 Oct 20, 2023 •

edited

Loading

msridhar Oct 20, 2023

armughan11 commented Oct 20, 2023

armughan11 commented Oct 20, 2023 •

edited

Loading

msridhar left a comment

msridhar Oct 21, 2023

armughan11 Oct 22, 2023

msridhar Oct 21, 2023

armughan11 Oct 22, 2023

msridhar left a comment

msridhar Oct 23, 2023

armughan11 Oct 23, 2023

msridhar Oct 23, 2023

armughan11 Oct 23, 2023

msridhar commented Oct 23, 2023

msridhar left a comment

lazaroclapp left a comment

msridhar commented Oct 25, 2023

lazaroclapp commented Oct 25, 2023

lazaroclapp left a comment

JSpecify: Modify Array Type Use Annotation Syntax #850

JSpecify: Modify Array Type Use Annotation Syntax #850

Conversation

armughan11 commented Oct 18, 2023 • edited by msridhar Loading

codecov bot commented Oct 19, 2023 • edited Loading

Codecov Report

msridhar commented Oct 20, 2023

msridhar left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

armughan11 Oct 20, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

armughan11 commented Oct 20, 2023

armughan11 commented Oct 20, 2023 • edited Loading

msridhar left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

msridhar left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

msridhar commented Oct 23, 2023

msridhar left a comment

Choose a reason for hiding this comment

lazaroclapp left a comment

Choose a reason for hiding this comment

msridhar commented Oct 25, 2023

lazaroclapp commented Oct 25, 2023

lazaroclapp left a comment

Choose a reason for hiding this comment

armughan11 commented Oct 18, 2023 •

edited by msridhar

Loading

codecov bot commented Oct 19, 2023 •

edited

Loading

armughan11 Oct 20, 2023 •

edited

Loading

armughan11 commented Oct 20, 2023 •

edited

Loading