Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Daikon cannot pass the Nullness checking in JDK11. #3223

Closed
xingweitian opened this issue Apr 2, 2020 · 8 comments
Closed

Daikon cannot pass the Nullness checking in JDK11. #3223

xingweitian opened this issue Apr 2, 2020 · 8 comments
Assignees
Milestone

Comments

@xingweitian
Copy link
Member

Note: NullnessChecker is type-checking daikon/Daikon.java
daikon/Daikon.java:1145: error: [nullness:argument.type.incompatible] incompatible types in argument.
              classesAsObject = f.get(Thread.currentThread().getContextClassLoader());
                                                                                  ^
  found   : @Initialized @Nullable ClassLoader
  required: @UnknownInitialization @NonNull Object
Note: NullnessChecker is type-checking daikon/chicory/DaikonVariableInfo.java
daikon/chicory/DaikonVariableInfo.java:790: error: [nullness:argument.type.incompatible] incompatible types in argument.
                value = Integer.toString(System.identityHashCode(field.get(null)));
                                                                           ^
  found   : null
  required: @UnknownInitialization @NonNull Object
Note: NullnessChecker is type-checking daikon/config/ParameterDoclet.java
daikon/config/ParameterDoclet.java:229: error: [nullness:argument.type.incompatible] incompatible types in argument.
      Object value = f.get(null);
                           ^
  found   : null
  required: @UnknownInitialization @NonNull Object

They are all about Field.get(Field this, Object obj). I found that @Nullable was removed in this commit.

The current master branch can pass the pipelines is because that daikon_jdk11 is commented in azure-pipelines.yml, while it is not commented in travis.yml.

@mernst
Copy link
Member

mernst commented Apr 2, 2020

daikon_jdk11 is commented out in azure-pipelines.yml because Daikon currently requires Java 8. Since apparently Daikon compiles under Java 11, we could reinstate the daikon_jdk11 job.

These are false positive warnings. Field.get's argument is @NonNull because Field.get might throw a NullPointerException. The only way to guarantee no NullPointerException is to require the argument to be non-null.

The difference between the behavior of Java 8 and Java 11 is troubling, however. That looks like a bug. Why does Daikon type-check under Java 8 but not under Java 11? I would expect the type-checker to issue the same warnings in each case.

@xingweitian
Copy link
Member Author

Is it because that in annotated jdk8, Field.get's argument is @Nullable? Should we also update it to @NonNull?

@wmdietl
Copy link
Member

wmdietl commented Apr 2, 2020

@xingweitian All obj parameters in Field should be @NonNull. That applies to get, but also to type-specific getters like getBoolean and similarly for the set methods.
The reason is the same as described in https://github.com/typetools/jdk/blob/master/src/java.base/share/classes/java/lang/reflect/Method.java#L564 : the field that is get/set could be static (for which null is allowed) or it could be an instance field (for which obj has to be non-null). So to prevent a possible NullPointerException, we make such parameters @NonNull.

Could you prepare a PR that changes these parameters to @NonNull (which is the default and you don't need to make it explicit), both in JDK 8 and in JDK 11.

@mernst Should we add a file like https://github.com/typetools/checker-framework/blob/master/checker/src/main/java/org/checkerframework/checker/nullness/collection-object-parameters-may-be-null.readme that adds "optimistic" reflection annotations?

@mernst
Copy link
Member

mernst commented Apr 2, 2020

@xingweitian Thanks for noticing the discrepancy between JDKs. If you can make a PR, that would be great. Otherwise, I can do it. Thanks!

@wmdietl I'm inclined not to make a stub file for this.

  • It isn't almost always a false positive. (By contrast, the warnings about Collection.contains are nearly always all false positives.)
  • The warnings aren't so common or pervasive, so it isn't a great barrier for users.

We could revisit this if it's a significant problem in practice.

@xingweitian
Copy link
Member Author

Sure, I will do it.

@wmdietl
Copy link
Member

wmdietl commented Apr 2, 2020

@mernst Beginners do however run into this issue quite frequently. I'm fine with not having a relaxed stub file, for the reasons you give.
However, how about adding a paragraph somewhere in the Nullness Checker manual about this? When looking for "reflection" in the manual I didn't find anything in the Nullness Checker section.

@mernst
Copy link
Member

mernst commented Apr 5, 2020

If it is a frequent problem, then it is indeed a good idea to add the stub file you mentioned or put a mention in the manual. I'm not sure where to put a mention in the manual, since beginners will have this exact same problem with any API that accepts null in some circumstances and rejects null in other circumstances.

@mernst mernst added this to the High milestone Apr 6, 2020
@wmdietl wmdietl self-assigned this Apr 6, 2020
@wmdietl
Copy link
Member

wmdietl commented Jul 31, 2020

https://github.com/typetools/checker-framework/blob/master/azure-pipelines.yml#L116 now contains a Daikon JDK 11 target, so let's close this issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants