JSpecify: Handle @Nonnull elements in @Nullable content arrays #963

armughan11 · 2024-06-03T03:40:58Z

Handles unexpected error cases in JSpecify mode where an index is asserted @Nonnull (fizz[x]!=null) but the array elements itself could be null (@Nullable String [] fizz).

Example

@Nullable String [] fizz ={"1"}
if (fizz[i] != null) {
    fizz[i].toString();
}

Current Behavior
This throws an error due to dereference of fizz[i]

New Behavior
There should be no error here unless it's outside the block. So only the latter dereference throws up an error in the below case.

@Nullable String [] fizz ={"1"}

if (fizz[i] != null) {
    fizz[i].toString();
}
fizz[i].toString();

armughan11 · 2024-06-03T03:42:06Z

@msridhar

msridhar · 2024-06-04T00:00:32Z

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

+
+public class ArrayIndexElement implements AccessPathElement {
+  private final Element javaElement;
+  @Nullable final String index;


Why is this @Nullable? Also, we shouldn't always use a String here. We want to use something like an Element for a local variable I think.

…ify-array-index

codecov · 2024-06-04T02:02:36Z

Codecov Report

Attention: Patch coverage is 86.25000% with 11 lines in your changes missing coverage. Please review.

Project coverage is 85.90%. Comparing base (a4ce249) to head (5df5697).

Files	Patch %	Lines
.../com/uber/nullaway/dataflow/ArrayIndexElement.java	56.25%	4 Missing and 3 partials ⚠️
...er/nullaway/dataflow/FieldOrMethodCallElement.java	78.94%	3 Missing and 1 partial ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##             master     #963      +/-   ##
============================================
+ Coverage     85.88%   85.90%   +0.02%     
- Complexity     2051     2067      +16     
============================================
  Files            82       83       +1     
  Lines          6806     6859      +53     
  Branches       1312     1323      +11     
============================================
+ Hits           5845     5892      +47     
- Misses          547      550       +3     
- Partials        414      417       +3

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

msridhar

Looking great! I have some comments

msridhar · 2024-06-04T19:29:06Z

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

-  public Element getJavaElement() {
-    return this.javaElement;
-  }
+public interface AccessPathElement {


Needs Javadoc

msridhar · 2024-06-04T19:29:43Z

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

-      return false;
-    }
-  }
+  String toString();


I think toString(), equals(), and hashCode() do not need to be declared here

msridhar · 2024-06-04T19:29:55Z

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

-    return this.javaElement;
-  }
+public interface AccessPathElement {
+  Element getJavaElement();


Needs Javadoc

msridhar · 2024-06-04T19:30:25Z

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

+import javax.annotation.Nullable;
+import javax.lang.model.element.Element;
+
+public class FieldOrMethodCallElement implements AccessPathElement {


Needs Javadoc (you can take it from the previous docs for AccessPathElement)

msridhar · 2024-06-04T19:35:08Z

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

+  @Nullable private final Integer constantIndex;
+  @Nullable private final Element variableElement;


Rather than having two @Nullable fields here to represent the cases, I'd prefer a single field of type Object named index for simplicity and efficiency. The API can still be type safe (i.e., you can only pass in an Integer or an Element); the fact that the same field is used internally would be a private implementation detail. You can document the expectations in a comment.

msridhar · 2024-06-04T19:38:00Z

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

+    } else if (arrayNode instanceof MethodInvocationNode) {
+      return ASTHelpers.getSymbol(((MethodInvocationNode) arrayNode).getTree());


Allowing the array itself to be the result of a method invocation is a bit more risky. Let's remove this case, and handle it later if we decide we need it

msridhar · 2024-06-04T19:39:02Z

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

+          return null;
+        }
+      }
+      result = buildAccessPathRecursive(stripCasts(arrayNode), elements, apContext, mapKey);


Why not strip the casts right at line 415?

msridhar · 2024-06-04T19:43:49Z

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

@@ -788,17 +788,30 @@ public TransferResult<Nullness, NullnessStore> visitArrayAccess(
      ArrayAccessNode node, TransferInput<Nullness, NullnessStore> input) {
    ReadableUpdates updates = new ReadableUpdates();
    setNonnullIfAnalyzeable(updates, node.getArray());
-    Nullness resultNullness;
+    Nullness resultNullness = defaultAssumption;


Let's not use defaultAssumption here; it's a bit confusing. Instead, add an explicit else at line 814 and set resultNullness to Nullness.NONNULL when we are not in JSpecify mode

Just get rid of the initializer expression here:

Suggested change

Nullness resultNullness = defaultAssumption;

Nullness resultNullness;

msridhar · 2024-06-04T19:45:03Z

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

+      if (isElementNullable) {
+        AccessPath arrayAccessPath = AccessPath.getAccessPathForNode(node, state, apContext);
+        if (arrayAccessPath != null) {
+          @Nullable
+          Nullness accessPathNullness =
+              input.getRegularStore().getNullnessOfAccessPath(arrayAccessPath);
+          if (accessPathNullness == Nullness.NULLABLE) {
+            resultNullness = Nullness.NULLABLE;
+          }
+        }


msridhar · 2024-06-04T19:49:33Z

We should add tests for the following cases:

Array expression is unhandled, like a method invocation (m()[i])
Array index is unhandled (m[i()])
Different index in conditional and deference (if (m[i] != null) { m[i+1].hashCode(); } should yield an error)

…ify-array-index

msridhar · 2024-06-08T15:53:17Z

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

@@ -788,17 +788,30 @@ public TransferResult<Nullness, NullnessStore> visitArrayAccess(
      ArrayAccessNode node, TransferInput<Nullness, NullnessStore> input) {
    ReadableUpdates updates = new ReadableUpdates();
    setNonnullIfAnalyzeable(updates, node.getArray());
-    Nullness resultNullness;
+    Nullness resultNullness = defaultAssumption;


Just get rid of the initializer expression here:

Suggested change

Nullness resultNullness = defaultAssumption;

Nullness resultNullness;

msridhar · 2024-06-08T15:53:31Z

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

+      if (isElementNullable) {
+        AccessPath arrayAccessPath = AccessPath.getAccessPathForNode(node, state, apContext);
+        if (arrayAccessPath != null) {
+          @Nullable


This annotation should not be needed

msridhar · 2024-06-08T15:55:06Z

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

+   * @param index The index used to access the array. Must be either an Integer (for constant
+   *     indices) or an Element (for variable indices).
+   */
+  public ArrayIndexElement(Element javaElement, Object index) {


We can have the field be of Object object, but we should have two separate constructors, one for integer literals and one for variables / fields, each taking the appropriate type. We shouldn't allow for passing in an arbitrary Object as the index. Alternately (and perhaps better), make the constructor private, and then write two static methods, one for each case, with appropriate names (like makeWithIntegerIndex)

627721565 · 2024-06-08T15:56:20Z

您好，邮件已经收到，查阅后会尽快给您回复！

msridhar · 2024-06-08T16:39:58Z

nullaway/src/test/java/com/uber/nullaway/jspecify/ArrayTests.java

+            "  if (fizz[i]!=null) { ",
+            "   // field access indexes aren't handled",
+            "   // BUG: Diagnostic contains: dereferenced expression fizz[i] is @Nullable",
+            "   fizz[i].toString();",


Hrm, I thought this case would be handled? What exact cases do we allow for index expressions again?

Ah my bad, this should work fine for primitives. Updated this and method invocation case accordingly.

msridhar · 2024-06-09T15:33:27Z

I realized this change might have a deeper impact than we were expecting. Right now, the creation of access path elements for array accesses is not gated on the flag for JSpecify mode, and passing the NullAway config into all relevant methods to do that would be kind of painful. But, I believe this means that code like this will pass NullAway now, when it didn't before this change:

if (arr[i].f != null) {
  arr[i].f.toString();
}

@armughan11 can you write a test to confirm this?

@lazaroclapp do you see any high-level issues with not reporting warnings for code like the above? It seems to be keeping in the spirit of NullAway, but it does potentially introduce new vectors of unsoundness, e.g.:

if (arr[i].f != null) {
  arr[j] = null; // overwrites a[i] if i == j
  arr[i].f.toString(); // still no warning from NullAway
}

Most programs don't code too much directly with arrays, but I wonder if we should do some more performance and sanity testing before landing this.

armughan11 · 2024-06-09T17:35:28Z

Just added the test and you're correct @msridhar. The test you mentioned works fine right now, but throws an error without our changes.

msridhar

Benchmarking didn't detect any perf regressions, and I rebuilt an internal code base with this change and didn't see any new errors or crashes.

I'm still hoping @lazaroclapp can give his feedback before we land this one.

msridhar · 2024-06-18T20:51:12Z

Gonna go ahead and merge this; I think we can address any concerns in follow-up PRs

This MR contains the following updates: | Package | Type | Update | Change | |---|---|---|---| | [org.tukaani:xz](https://tukaani.org/xz/java.html) ([source](https://github.com/tukaani-project/xz-java)) | compile | minor | `1.9` -> `1.10` | | [org.eclipse:yasson](https://projects.eclipse.org/projects/ee4j.yasson) ([source](https://github.com/eclipse-ee4j/yasson)) | compile | patch | `3.0.3` -> `3.0.4` | | [org.eclipse.parsson:parsson](https://github.com/eclipse-ee4j/parsson) | compile | patch | `1.1.6` -> `1.1.7` | | [com.uber.nullaway:nullaway](https://github.com/uber/NullAway) | | patch | `0.11.0` -> `0.11.1` | | [io.hosuaby:inject-resources-junit-jupiter](https://github.com/hosuaby/inject-resources) | test | patch | `0.3.3` -> `0.3.5` | | [org.codehaus.mojo:exec-maven-plugin](https://www.mojohaus.org/exec-maven-plugin) ([source](https://github.com/mojohaus/exec-maven-plugin)) | build | minor | `3.3.0` -> `3.4.0` | --- ### Release Notes <details> <summary>tukaani-project/xz-java</summary> ### [`v1.10`](https://github.com/tukaani-project/xz-java/releases/tag/v1.10): XZ for Java 1.10 [Compare Source](tukaani-project/xz-java@v1.9...v1.10) </details> <details> <summary>eclipse-ee4j/yasson</summary> ### [`v3.0.4`](eclipse-ee4j/yasson@3.0.3...3.0.4) [Compare Source](eclipse-ee4j/yasson@3.0.3...3.0.4) </details> <details> <summary>eclipse-ee4j/parsson</summary> ### [`v1.1.7`](eclipse-ee4j/parsson@1.1.6...1.1.7) [Compare Source](eclipse-ee4j/parsson@1.1.6...1.1.7) </details> <details> <summary>uber/NullAway</summary> ### [`v0.11.1`](https://github.com/uber/NullAway/blob/HEAD/CHANGELOG.md#Version-0111) [Compare Source](uber/NullAway@v0.11.0...v0.11.1) - Fix issue 1008 ([#1009](uber/NullAway#1009)) - JSpecify: read upper bound annotations from bytecode and add tests ([#1004](uber/NullAway#1004)) - Fix crash with suggested suppressions in JSpecify mode ([#1001](uber/NullAway#1001)) - Update to JSpecify 1.0 and use JSpecify annotations in NullAway code ([#1000](uber/NullAway#1000)) - Expose [@EnsuresNonNull](https://github.com/EnsuresNonNull) and [@RequiresNonNull](https://github.com/RequiresNonNull) in annotations package ([#999](uber/NullAway#999)) - Don't report initializer warnings on [@NullUnmarked](https://github.com/NullUnmarked) constructors / methods ([#997](uber/NullAway#997)) - Strip annotations from MethodSymbol strings ([#993](uber/NullAway#993)) - JSpecify: fix crashes where declared parameter / return types were raw ([#989](uber/NullAway#989)) - JSpecify: Handle [@nullable](https://github.com/nullable) elements for enhanced-for-loops on arrays ([#986](uber/NullAway#986)) - Features/944 tidy stream nullability propagator ([#985](uber/NullAway#985)) - Tests for loops over arrays ([#982](uber/NullAway#982)) - Bug fixes for array subtyping at returns / parameter passing ([#980](uber/NullAway#980)) - JSpecify: Handle [@nonnull](https://github.com/nonnull) elements in [@nullable](https://github.com/nullable) content arrays ([#963](uber/NullAway#963)) - Don't report [@nullable](https://github.com/nullable) type argument errors for unmarked classes ([#958](uber/NullAway#958)) - External Library Models: Adding support for Nullable upper bounds of Generic Type parameters ([#949](uber/NullAway#949)) - Refactoring / code cleanups: - Test on JDK 22 ([#992](uber/NullAway#992)) - Add test case for [@nullable](https://github.com/nullable) Void with override in JSpecify mode ([#990](uber/NullAway#990)) - Enable UnnecessaryFinal and PreferredInterfaceType EP checks ([#991](uber/NullAway#991)) - Add missing [@test](https://github.com/test) annotation ([#988](uber/NullAway#988)) - Fix typo in variable name ([#987](uber/NullAway#987)) - Remove AbstractConfig class ([#974](uber/NullAway#974)) - Fix Javadoc for MethodRef ([#973](uber/NullAway#973)) - Refactored data clumps with the help of LLMs (research project) ([#960](uber/NullAway#960)) - Build / CI tooling maintenance: - Various cleanups enabled by bumping minimum Java and Error Prone versions ([#962](uber/NullAway#962)) - Disable publishing of snapshot builds from CI ([#967](uber/NullAway#967)) - Update Gradle action usage in CI workflow ([#969](uber/NullAway#969)) - Update Gradle config to always compile Java code using JDK 17 ([#971](uber/NullAway#971)) - Update JavaParser to 3.26.0 ([#970](uber/NullAway#970)) - Reenable JMH benchmarking in a safer manner ([#975](uber/NullAway#975)) - Updated JMH Benchmark Comment Action ([#976](uber/NullAway#976)) - Update to Gradle 8.8 ([#981](uber/NullAway#981)) - Update to Error Prone 2.28.0 ([#984](uber/NullAway#984)) - Update to Gradle 8.9 ([#998](uber/NullAway#998)) - Update to WALA 1.6.6 ([#1003](uber/NullAway#1003)) </details> <details> <summary>hosuaby/inject-resources</summary> ### [`v0.3.5`](hosuaby/inject-resources@v0.3.4...v0.3.5) [Compare Source](hosuaby/inject-resources@v0.3.4...v0.3.5) ### [`v0.3.4`](hosuaby/inject-resources@v0.3.3...v0.3.4) [Compare Source](hosuaby/inject-resources@v0.3.3...v0.3.4) </details> <details> <summary>mojohaus/exec-maven-plugin</summary> ### [`v3.4.0`](https://github.com/mojohaus/exec-maven-plugin/releases/tag/3.4.0) [Compare Source](mojohaus/exec-maven-plugin@3.3.0...3.4.0)  #### 🚀 New features and improvements - Allow `<includePluginDependencies>` to be specified for the exec:exec goal ([#432](mojohaus/exec-maven-plugin#432)) [@sebthom](https://github.com/sebthom) #### 🐛 Bug Fixes - Do not get UPPERCASE env vars ([#427](mojohaus/exec-maven-plugin#427)) [@wheezil](https://github.com/wheezil) #### 📦 Dependency updates - Bump org.codehaus.mojo:mojo-parent from 82 to 84 ([#434](mojohaus/exec-maven-plugin#434)) [@dependabot](https://github.com/dependabot) - Bump org.codehaus.plexus:plexus-xml from 3.0.0 to 3.0.1 ([#431](mojohaus/exec-maven-plugin#431)) [@dependabot](https://github.com/dependabot) #### 👻 Maintenance - Remove Log4j 1.2.x from ITs ([#437](mojohaus/exec-maven-plugin#437)) [@slawekjaranowski](https://github.com/slawekjaranowski) #### 🔧 Build - Use Maven 3.9.7 and 4.0.0-beta-3 ([#433](mojohaus/exec-maven-plugin#433)) [@slawekjaranowski](https://github.com/slawekjaranowski) </details> --- ### Configuration 📅 **Schedule**: Branch creation - At any time (no schedule defined), Automerge - At any time (no schedule defined). 🚦 **Automerge**: Enabled. ♻ **Rebasing**: Whenever MR is behind base branch, or you tick the rebase/retry checkbox. 👻 **Immortal**: This MR will be recreated if closed unmerged. Get [config help](https://github.com/renovatebot/renovate/discussions) if that's undesired. --- - [ ] If you want to rebase/retry this MR, check this box --- This MR has been generated by [Renovate Bot](https://github.com/renovatebot/renovate).

Initial commit

8646811

armughan11 marked this pull request as draft June 3, 2024 03:41

armughan11 marked this pull request as ready for review June 3, 2024 03:41

armughan11 marked this pull request as draft June 3, 2024 03:41

armughan11 and others added 4 commits June 3, 2024 01:29

Fix instances

351005b

few more tests

0eb952e

case fix

cad529c

add failing test

da7c17b

msridhar reviewed Jun 4, 2024

View reviewed changes

msridhar and others added 3 commits June 3, 2024 20:17

Merge branch 'master' into jspecify-array-index

455cf0b

Added direct checks

07783b8

Merge remote-tracking branch 'origin/jspecify-array-index' into jspec…

919043a

…ify-array-index

armughan11 marked this pull request as ready for review June 4, 2024 01:57

armughan11 requested a review from msridhar June 4, 2024 01:57

armughan11 and others added 2 commits June 3, 2024 22:14

Added direct checks

ff78576

Merge branch 'master' into jspecify-array-index

6659cf1

msridhar reviewed Jun 4, 2024

View reviewed changes

armughan11 added 2 commits June 8, 2024 01:10

Addressed PR comments

c51136c

Merge remote-tracking branch 'origin/jspecify-array-index' into jspec…

29c208e

…ify-array-index

armughan11 requested a review from msridhar June 8, 2024 06:11

msridhar reviewed Jun 8, 2024

View reviewed changes

armughan11 added 2 commits June 8, 2024 12:54

Addressed PR comments

49d9fec

Merge branch 'master' into jspecify-array-index

3498074

armughan11 requested a review from msridhar June 8, 2024 17:56

Added test

11e8c81

msridhar added run-benchmarks and removed run-benchmarks labels Jun 12, 2024

Merge branch 'master' into jspecify-array-index

9be512b

msridhar added run-benchmarks and removed run-benchmarks labels Jun 13, 2024

msridhar approved these changes Jun 14, 2024

View reviewed changes

msridhar added the jspecify Related to support for jspecify standard (see jspecify.dev) label Jun 16, 2024

Merge branch 'master' into jspecify-array-index

5df5697

msridhar enabled auto-merge (squash) June 18, 2024 20:51

msridhar merged commit 76115d4 into uber:master Jun 18, 2024
11 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

JSpecify: Handle @Nonnull elements in @Nullable content arrays #963

JSpecify: Handle @Nonnull elements in @Nullable content arrays #963

armughan11 commented Jun 3, 2024 •

edited

Loading

armughan11 commented Jun 3, 2024

msridhar Jun 4, 2024

codecov bot commented Jun 4, 2024 •

edited

Loading

msridhar left a comment

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 4, 2024

msridhar Jun 8, 2024

msridhar Jun 4, 2024

msridhar commented Jun 4, 2024

msridhar Jun 8, 2024

msridhar Jun 8, 2024

armughan11 Jun 8, 2024

msridhar Jun 8, 2024

armughan11 Jun 8, 2024

627721565 commented Jun 8, 2024 via email

msridhar Jun 8, 2024

armughan11 Jun 8, 2024

msridhar commented Jun 9, 2024

armughan11 commented Jun 9, 2024

msridhar left a comment

msridhar commented Jun 18, 2024

		@Nullable private final Integer constantIndex;
		@Nullable private final Element variableElement;

		} else if (arrayNode instanceof MethodInvocationNode) {
		return ASTHelpers.getSymbol(((MethodInvocationNode) arrayNode).getTree());

	Nullness resultNullness = defaultAssumption;
	Nullness resultNullness;

JSpecify: Handle @Nonnull elements in @Nullable content arrays #963

JSpecify: Handle @Nonnull elements in @Nullable content arrays #963

Conversation

armughan11 commented Jun 3, 2024 • edited Loading

armughan11 commented Jun 3, 2024

Choose a reason for hiding this comment

codecov bot commented Jun 4, 2024 • edited Loading

Codecov Report

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

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

Choose a reason for hiding this comment

msridhar commented Jun 4, 2024

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

627721565 commented Jun 8, 2024 via email

Choose a reason for hiding this comment

Choose a reason for hiding this comment

msridhar commented Jun 9, 2024

armughan11 commented Jun 9, 2024

msridhar left a comment

Choose a reason for hiding this comment

msridhar commented Jun 18, 2024

armughan11 commented Jun 3, 2024 •

edited

Loading

codecov bot commented Jun 4, 2024 •

edited

Loading