Support @RequiresNonnull and @EnsuresNonnull for expressing field nullability pre- and post-conditions by nimakarimipour · Pull Request #423 · uber/NullAway

nimakarimipour · 2020-09-30T07:04:21Z

Adds support for expressing methods precondition and postcondition using @RequiresNonnull and @EnsuresNonnull annotation.

Annotations

@RequiresNonnull(param) expresses a method precondition which expects the class field with name param, to be @Nonnull at call site. NullAway data flow analysis is going to assume that the specified class field is @Nonnull at start point of the method. At every call site to the annotated method, NullAway checks weather the precondition is satisfied and will report an error otherwise.
@EnsuresNonnull(param) expresses a method postcondition which the class field with name param will be @Nonnull at exit point of method. The @Nonnull assumption of the class field at exit point will be validated by NullAway and will be reported if the assumption is not valid.

NOTE: At this moment, for both annotations, only class fields for the receiver object are supported.
Syntax: @Annotation(("this."|"")field_name)

Examples

class Foo {
    @Nullable Item nullItem;
    @RequiresNonnull("nullItem")
    public void run() {
            nullItem.call(); //Here NullAway does not report an error because of the assumption.
            nullItem = null;
            nullItem.call(); //Here NullAway reports an error since the assumption is no longer valid.
    }
}

class Foo {
    @Nullable Item nullItem;
    @EnsuresNonnull("nullItem") //Here NullAway injects the Nonnull value for the corresponding access path since the assumption is valid
    public void test1() {
        nullItem = new Item();
    }
    @EnsuresNonnull("nullItem") //Here NullAway reports an error since the nullItem is not Nonnull at exit point and the assumption is not valid.
    public void test2() { 
    
    }
}

class Foo {
    @Nullable Item nullItem;
    @RequiresNonnull("nullItem")
    public void run() {
        nullItem.call();
    }
    @EnsuresNonnull("nullItem")
    public void init() {
        nullItem = new Item();
    }
    public void test1() {
        init();
        run(); //Here both the precondition and postcondition are satisfied.
    }
    public void test2() {
        Foo bar = new Foo();
        bar.init();
        bar.run(); //Here both the precondition and postcondition are satisfied.
    }
    public void test3() {
        Foo bar = new Foo();
        init();
        Foo other = new Foo();
        other.init();
        bar.run();  //Here NullAway reports an error since the precondition for "run" method on "bar" instance is not satisfied.
    }
}

Updates

Addressed all comments.
Added the support for selecting multiple class fields in both annotations.
Fixed the bug where the user might choose a field from super classes fields.
Fixed the bug where a method might not be annotated as @EnsuresNonNull but its superclass does, and it was not updating the NullnessStore when the method has been invoked.
Added the inheritance support for annotations:
- @EnsuresNonNull: All sub methods, can only add new fields to the set of all fields mentioned as parameter in super class @EnsuresNonNull annotation. All selected class fields including super methods selected fields must be written explicitly as parameter in the sub methods @EnsuresNonNull annotation. If a method is not annotated as @EnsuresNonNull, still needs to guarantee all selected fields from super method are @NonNull at exit point if exists.
- @RequiresNonNull: All sub methods, can only remove fields from the set of all fields mentioned as parameter in super class @RequiresNonNull annotation. If a method is not annotated as @RequiresNonNull, it will not be processed and no check will take place when it has been invoked, even if the super method is annotated with @RequiresNonNull annotation.
Refactored the code since RequiresNonNullHandler and EnsuresNonNullHandler had a lot in common.

CLAassistant · 2020-09-30T07:04:27Z

All committers have signed the CLA.

msridhar

Overall looks great! I've finished a partial review through the EnsuresNonnullHandler. Some similar comments will apply to the other handler. I will try to finish the review soon but hopefully this is enough to get started

msridhar · 2020-10-01T18:31:44Z

+  }
+
+  @Override
+  public void onMatchMethod(


I think we need to check here for cases where this method overrides a superclass method, and the superclass method has @EnsuresNonNull? In such cases we need the overriding method to adhere to the @EnsuresNonNull spec from the superclass method, right?

Hi Manu, thank you very much for your comments, I addressed them all. I believe this is ready for another review.

Please find the latest updates below from your last review:

Addressed all comments.

Added the support for selecting multiple class fields in both annotations.

Fixed the bug where the user might choose a field from super classes fields.

Fixed the bug where a method might not be annotated as @EnsuresNonNull but its superclass does, and it was not updating the NullnessStore when the method has been invoked.

Added the inheritance support for annotations:

@EnsuresNonNull: All sub methods, can only add new fields to the set of all fields mentioned as parameter in super class @EnsuresNonNull annotation. All selected class fields including super methods selected fields must be written explicitly as parameter in the sub methods @EnsuresNonNull annotation. If a method is not annotated as @EnsuresNonNull, still needs to guarantee all selected fields from super method are @NonNull at exit point if exists.

@RequiresNonNull: All sub methods, can only remove fields from the set of all fields mentioned as parameter in super class @RequiresNonNull annotation. If a method is not annotated as @RequiresNonNull, it will not be processed and no check will take place when it has been invoked, even if the super method is annotated with @RequiresNonNull annotation.

Refactored the code since RequiresNonNullHandler and EnsuresNonNullHandler had a lot in common.

msridhar

Looking a lot better! I haven't finished looking at all the tests yet, but here is another set of comments

lazaroclapp · 2020-12-01T17:58:23Z

+   *
+   * <p>
+   *
+   * <ul>


Probably:

* <p><ul> * <li> ... * ... * </ul></p>

would be more readable. This looks like a ton of empty lines, unless GJF is enforcing it.

Thank you for your comment but actually GJF is enforcing it.

Oh, well, GJF makes sense to me 99% of the time, so I'll trust it on this one 😉

msridhar

LGTM! We just need to remember to update the wiki documentation, also with examples for the error messages one can get.

lazaroclapp

LGTM.

There are a few notes and nits, but I am fine with this landing as is. Sorry for being the bottleneck on it these past few days 😅

lazaroclapp · 2020-12-08T00:10:52Z

+   *
+   * <p>
+   *
+   * <ul>


Oh, well, GJF makes sense to me 99% of the time, so I'll trust it on this one 😉

lazaroclapp · 2020-12-08T00:14:25Z

+    Preconditions.checkNotNull(classSymbol);
+    for (Element member : classSymbol.getEnclosedElements()) {
+      if (member.getKind().isField()) {
+        if (member.getSimpleName().toString().equals(name)) {


Out of curiosity: what was the resolution here? Was it really resolved? (I see it marked as resolved by @msridhar , so I assume we are fine with static fields after all?)

lazaroclapp · 2020-12-08T00:21:08Z

+    if (fieldNames == null) {
+      return super.onDataflowVisitMethodInvocation(
+          node, types, context, inputs, thenUpdates, elseUpdates, bothUpdates);
+    }


It might be a bit cleaner to invert this condition:

if (fieldNames != null) { [All the extra handling] } return super.onDataflowVisitMethodInvocation( node, types, context, inputs, thenUpdates, elseUpdates, bothUpdates);

But it's probably fine either way :)

lazaroclapp · 2020-12-08T00:25:48Z

+    for (String fieldName : fieldNames) {
+      Symbol.ClassSymbol classSymbol = ASTHelpers.enclosingClass(methodSymbol);
+      Preconditions.checkNotNull(
+          classSymbol, "can not find the enclosing class for method symbol: " + methodSymbol);


can not and cannot are not equivalent and this one should be cannot find ("is unable to find...", rather than "it might not find..." :) )

lazaroclapp · 2020-12-08T00:29:14Z

+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+public @interface EnsuresNonNull {
+  String[] value();
+}


@msridhar Separate from this PR. Do we have an issue for creating a com.uber.nullaway:annotation or com.uber.nullaway:lib maven artifact? Would be good to have these out there, together with a canonical implementation of castToNonNull, etc.

lazaroclapp · 2020-12-08T00:31:09Z

@@ -0,0 +1,19 @@
+package com.uber.nullaway.qual;


Is this really a "Type qualifier" in the Checker Framework sense?

Shouldn't this package be "com.uber.nullaway.annotation"? (cc: @msridhar )

p.s. But I am fine landing as is if not obvious what it should be named, please let's not spend months debating whether to call it annotation or annotations 😄

Switched to annotations. 4935c00

lazaroclapp · 2020-12-08T00:33:52Z

        .doTest();
  }
+
+  @Test


Might be worth extracting this reminder into an issue before we both forget again: #430 (that said, cleaning up that issue tracker a bit is also a task to not forget 😅 )

lazaroclapp · 2020-12-08T20:55:54Z

+    Preconditions.checkNotNull(classSymbol);
+    for (Element member : classSymbol.getEnclosedElements()) {
+      if (member.getKind().isField()) {
+        if (member.getSimpleName().toString().equals(name)) {


Absolutely ok with actual handling happening as a follow-up. Let's get this landed.

That said, thanks for double-checking and adding the sanity check! :)

msridhar · 2020-12-08T21:37:39Z


 # kotlin
-annotations/
+/annotations/


@lazaroclapp this originally led to our new com.uber.nullaway.annotations package source files getting ignored. Is this the right fix?

No idea. Do we have Kotlin code in this repo?

I don't think so 🙂 Should I just remove the line then?

Let's try that :)

nimakarimipour added 3 commits September 29, 2020 22:10

add handlers

aa3390c

added comments

3f3b571

added comments

e2f2749

nimakarimipour changed the title ~~Adds support for expressing methods pre-condition and post-condition using @RequiresNonnull and @EnsuresNonnull annoatation~~ Adds support for expressing methods precondition and postcondition using @RequiresNonnull and @EnsuresNonnull annoatation Sep 30, 2020

nimakarimipour added 3 commits September 30, 2020 10:44

added this. support

8737d9e

refactored

7f90e6d

removed the map

d59912e

lazaroclapp changed the title ~~Adds support for expressing methods precondition and postcondition using @RequiresNonnull and @EnsuresNonnull annoatation~~ Adds support for expressing methods precondition and postcondition using @RequiresNonnull and @EnsuresNonnull annotation Oct 1, 2020

msridhar requested changes Oct 1, 2020

View reviewed changes

nimakarimipour added 13 commits October 2, 2020 18:56

updated some comments

dcda8e0

adapted every method to work with classSymbol

ec5ed1e

added javadoc

547c426

fixed requiresNonNull inheritance

9f01e81

update requresNonNull inheritance rule

a17ab73

update requresNonNull inheritance rule

f87e0e4

fixed all bugs

9d39b6a

refactored

f5dd245

multiple field support for EnsuresNonNull

ba470b1

refactored

417e801

refactored

e15d85c

added comments

7074e91

adapted to the latest release

8f7b4ec

nimakarimipour requested a review from msridhar October 7, 2020 10:42

nimakarimipour added 2 commits October 7, 2020 11:05

error message updated

4db692d

updated comments

4bae928

msridhar requested changes Oct 8, 2020

View reviewed changes

nimakarimipour added 3 commits October 11, 2020 23:39

fixed issue with multiple member select tree

e584f7a

updated test

9860c29

updated comments

19d46f1

nimakarimipour added 5 commits November 24, 2020 00:49

resolved issues

d07b6df

resolved issues

cffa444

resolved issues

8dda5de

resolvd remaining issues

737c911

added comments

29c4b30

lazaroclapp reviewed Dec 1, 2020

View reviewed changes

nimakarimipour added 3 commits December 3, 2020 11:40

merged new changes

8df85a6

resolved javadoc list item issue

1d195c2

refactored

591baa6

nimakarimipour requested review from lazaroclapp and msridhar December 3, 2020 20:24

msridhar approved these changes Dec 4, 2020

View reviewed changes

lazaroclapp approved these changes Dec 8, 2020

View reviewed changes

msridhar added 2 commits December 8, 2020 12:17

report errors for static fields in pre/postcondition annotations

62fb5cd

invert logic

bf8d1ad

lazaroclapp reviewed Dec 8, 2020

View reviewed changes

msridhar added 4 commits December 8, 2020 13:02

Fix assertion message and remove redundant error checking

e75b6a2

Improve error message

7053721

qual -> annotations

4935c00

re-add files

a217d78

msridhar reviewed Dec 8, 2020

View reviewed changes

Remove Kotlin-related .gitignore line

23e0dc0

This was referenced Dec 8, 2020

Support static fields in @EnsuresNonnull/@RequiresNonnull annotations #431

Closed

Create a Maven artifact for annotations (e.g. @EnsuresNonnull/@RequiresNonnull) #432

Closed

msridhar changed the title ~~Adds support for expressing methods precondition and postcondition using @RequiresNonnull and @EnsuresNonnull annotation~~ Support @RequiresNonnull and @EnsuresNonnull for expressing field nullability pre- and post-conditions Dec 8, 2020

lazaroclapp changed the title ~~Support @RequiresNonnull and @EnsuresNonnull for expressing field nullability pre- and post-conditions~~ Support expressing method pre- and postcondition using @RequiresNonnull/@EnsuresNonnull Dec 8, 2020

lazaroclapp changed the title ~~Support expressing method pre- and postcondition using @RequiresNonnull/@EnsuresNonnull~~ Add method pre- and postcondition using @RequiresNonnull/@EnsuresNonnull Dec 8, 2020

lazaroclapp changed the title ~~Add method pre- and postcondition using @RequiresNonnull/@EnsuresNonnull~~ Support @RequiresNonnull and @EnsuresNonnull for expressing field nullability pre- and post-conditions Dec 8, 2020

msridhar merged commit d7e96e4 into uber:master Dec 8, 2020

nimakarimipour deleted the require_ensures_nonnull branch March 22, 2022 00:02

Conversation

nimakarimipour commented Sep 30, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Adds support for expressing methods precondition and postcondition using @RequiresNonnull and @EnsuresNonnull annotation.

Annotations

Examples

Updates

Uh oh!

CLAassistant commented Sep 30, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

msridhar left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

msridhar left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

msridhar left a comment

Choose a reason for hiding this comment

Uh oh!

lazaroclapp left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

nimakarimipour commented Sep 30, 2020 •

edited

Loading

CLAassistant commented Sep 30, 2020 •

edited

Loading