Support @EnsuresNonNullIf

[mauricioaniche]

This PR is an initial draft of a proposal to support @EnsuresNonNullIf, following the discussion on issue #1032. This annotation allows the definition of methods that ensure that fields aren't null.

An example of the annotation:

class Foo {
  @Nullable Object field;

  @EnsuresNonNullIf("field")
  boolean hasField() {
    return field != null;
  }

  void action() {
    if(!hasField()) {
      return;
    }

    // field is non-null from this point on.
  }
}

[CLAassistant]

All committers have signed the CLA.

[mauricioaniche]

Force pushing just so I can change the user name in the commit, which wasn't matching my github user.

[codecov]

Codecov Report

Attention: Patch coverage is 87.42138% with 20 lines in your changes missing coverage. Please review.

Project coverage is 87.54%. Comparing base (940c40e) to head (1c5610c).
Report is 1 commits behind head on master.

Files with missing lines	Patch %	Lines
...ontract/fieldcontract/EnsuresNonNullIfHandler.java	85.14%	7 Missing and 8 partials ⚠️
...ers/contract/fieldcontract/FieldContractUtils.java	89.28%	2 Missing and 1 partial ⚠️
...c/main/java/com/uber/nullaway/NullabilityUtil.java	90.90%	0 Missing and 1 partial ⚠️
...java/com/uber/nullaway/dataflow/NullnessStore.java	91.66%	0 Missing and 1 partial ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##             master    #1044      +/-   ##
============================================
- Coverage     87.54%   87.54%   -0.01%     
- Complexity     2138     2165      +27     
============================================
  Files            83       85       +2     
  Lines          7003     7114     +111     
  Branches       1367     1386      +19     
============================================
+ Hits           6131     6228      +97     
- Misses          451      458       +7     
- Partials        421      428       +7     

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

[msridhar]

This looks very promising, thanks! I'll just answer the questions for now and assume a full code review should wait for later.

• For now, the validation mechanism expects a precise "return field != null;". Any deviation from that will trigger a NullAway error. Is that fine?

I think we can do a bit better without too much trouble. Looking at the code here, I think the thenStore and elseStore parameters should reflect the nullability info computed by the dataflow analysis when returning true and false respectively. So, we should be able to look inside the appropriate store to see if the inferred type for the field is @NonNull. So we should be able to handle cases like, e.g., if (field != null) return true;.

• I still need to work on supporting multiple fields.

No problem. I think if needed, a first version could even skip that as long as we track multiple field support as an issue for a follow up.

• Should I support an extra parameter to the annotation, so the person can define whether the method check does == or != null?

Yes, I think that would be good for flexibility, and it shouldn't be too hard to implement.

• During validation, I need to check whether the field exists in the class.

👍 It can exist in the class itself or it can be inherited (see below).

• What to do in validateOverridingRules?

We need to prevent cases like (rough syntax):

class A {
  @Nullable Object foo;
  @EnsuresNonNullIf("this.foo")
  boolean hasFoo() { return this.foo != null; }
}
class B extends A {
  @Override
  boolean hasFoo() { return true; }
}
...
void test() {
  A a = new B();
  if (a.hasFoo()) {
    a.foo.toString(); // NPE!
  }
}

To prevent this, an overriding method should have at least as strong an @EnsuresNonNullIf annotation as the overridden method. So if the superclass method ensures f and g are non-null when returning true, the subclass method should also ensure f and g are non-null when returning true, but it can also ensure h is non-null.

[mauricioaniche]

@msridhar I believe I managed to leverage the onDataflowVisitReturn callback and extract the assessment of the data-flow engine. The expression you used as example if (field != null) return true; does work now, including validation in case the method mistakenly returns false (as seen in the automated tests).

However, as you can see in the ignored test I wrote, the engine doesn't get something like var x = field != null; return x;. At the point of the visit return data-flow callback, the stores sees the field as Nullable. Not sure if there's something I can do to improve that?

Other remarks:

• I couldn't do the full analysis within the provided validateAnnotationSemantics, given that I had to also implemente onDataflowVisitReturn. There, I needed information about the enclosing method, and so, I added two fields in the parent AbstractFieldContractHandler class.
• I need to forceRunOnMethod, otherwise the engine doesn't give me proper values. Not sure if there's a better method to use there?

[mauricioaniche]

@msridhar I added a few more features, like the post-condition check we spoke about and a trueIfNonNull boolean that inverts the condition.

The only thing missing is that if the if check is extracted to a boolean variable, the handler gets lost. See all tests that are disabled.

Thoughts?

[msridhar]

@mauricioaniche will look more closely at everything soon, but briefly:

The only thing missing is that if the if check is extracted to a boolean variable, the handler gets lost. See all tests that are disabled.

This is #98, NullAway doesn't support this yet. So don't worry about getting that working 🙂

[mauricioaniche]

@msridhar Oh, that's good to know, I thought I was making a mistake somewhere! Then, I believe I coded everything I wanted for this feature.

• The new @EnsuresNonNullIf accepts a list of fields and a boolean trueIfNonNull allowing the person to flip the outcome of the method.
• The handler takes care of semantics validation as well as post-conditions in the child classes
• A bunch of tests

Looking forward to your code review. More importantly, maybe you have some extra test cases you'd like me to try? I'm sure your eyes are way more trained than mine to spot corner cases!

[msridhar]

@mauricioaniche will try to look at this one very soon. In the meantime, are you able to sign the CLA?

[mauricioaniche]

CLA signed!

[mauricioaniche]

See this TODO

[msridhar]

Would this happen for an abstract / interface method? If so, seems best to report some kind of error?

[mauricioaniche]

The existing EnsuresNonNullHandler actually returns true in this case. I'm doing the same now, as someone probably thought deeper about it!

[mauricioaniche]

Keeping this one open for you to close it yourself, if you agree!

[mauricioaniche]

Any thoughts about this? A method with multiple returns, can we be smart about it?

[msridhar]

See comment above about checking return statements individually

[msridhar]

Thanks again for the contribution! It will take me some time to review this whole PR. I am pushing my comments in chunks when I get time, to get the feedback out faster.

[mauricioaniche]

@msridhar you were right about the store! I was under the assumption that always looking at the "thenStore" was the right thing to do, because IIUC, it represents the path that follows the return expression. However, I didn't expect that the engine would not really be 100% accurate around the "NULL". Using the "elseStore" allowed me to look at NON_NULL always, which seems to be precise. Why does that happen?

Moreover: I put it back the return default to true and fixed the minor nits as well. Would you mind giving it a final check to see if everything looks fine?

Before merging: I think it's best to squash the commits just so the history of the repository doesn't get full of "bad commits". Do you want me to squash or do you do it via github?

[msridhar]

@mauricioaniche thanks again for this amazing contribution! Will take one more look before merging. Don't worry we always squash and merge so the intermediate commits won't remain.

[msridhar]

@msridhar you were right about the store! I was under the assumption that always looking at the "thenStore" was the right thing to do, because IIUC, it represents the path that follows the return expression. However, I didn't expect that the engine would not really be 100% accurate around the "NULL". Using the "elseStore" allowed me to look at NON_NULL always, which seems to be precise. Why does that happen?

I'd have to re-read the Checker dataflow manual to be really sure, but I think what goes on is that for every expression of type boolean, the data flow framework creates a "then" and "else" store corresponding to what is known (based on the transfer functions) if the expression evaluates to true or false. These stores get propagated to any type of successor, including return statement nodes. For an assignment like x = bool_expr, I think the incoming then and else store would be merged using a LUB operator before getting propagated to the successor of the assignment. This is a nice approach since it lets you keep around information about boolean expressions in various contexts beyond using it for path sensitivity.

[mauricioaniche]

@msridhar wait a sec, I believe I found a case where it breaks

[mauricioaniche]

Take a look at the test setResultToFalse_multipleElements_correctSemantics_2 that I just pushed, which is basically setResultToFalse_multipleElements_correctSemantics_2 but with the true being returned as literal. This one should pass, right? It's failing now.

EDIT: I gotta go pick up my kid from school, will be back soon.

[mauricioaniche]

@msridhar Done. It was a corner case on when return=false and the method returned a literal boolean. I had the feeling I had to also handle it. Main change is here. I also renamed the variable and improved the documentation around it.

There was a wrong test case that was revealed after I fixed this bug! If you have the energy, please go through the test cases, and see if they are all correct!!

Thank you!

[msridhar]

Found another potential issue, see below

[msridhar]

I don't think this should be an error. The annotation means, "If this method returns true, then nullableItem is guaranteed to be non-null." If the method returns false, then the annotation says nothing about whether nullableItem will be null or not. And at callers, we should only be using nullability information from the annotation for the case where the returned boolean matches the result field of the annotation. So there is no need to perform any check within the method when we know it is not returning the result value. The error reported for the return true statement is correct. Do you agree?

[mauricioaniche]

That does make sense to me! Let me work on it!

[mauricioaniche]

Here: 56a0984

[msridhar]

Same comment as the one below.

[mauricioaniche]

Here 56a0984

[msridhar]

@mauricioaniche I think this ready to go! I made a slight simplification to the store update logic in fa7728e, based on our updated understanding of how the "then" and "else" stores work.

Out of an abundance of caution, I'm going to run our benchmarking suite with this change, which involves pushing the branch up to our main repo and creating a dummy PR. Assuming there are no red flags there I'll go ahead and squash and merge.

[msridhar]

Hrm, it seems our benchmarking server needs a new JVM version so the benchmarking job is not working 😐 I'm not too worried about the perf impact of this change, so I will go ahead and land it.

[mauricioaniche]

Great news! Thanks for your suppprt in this adventure, @msridhar !